IMO 2009 A3 (P5)

Find all functions $f : ℕ → ℕ$ such that for any $x, y ∈ ℕ$, the non-negative integers $x$, $f(y)$, and $f(y + f(x))$ form the sides of a possibly degenerate triangle.

Extra notes

The original version using signature $ℕ^+ → ℕ^+$ is that $x$, $f(y)$, and $f(y + f(x) - 1)$ for the sides of a non-degenerate triangle.

Extra structure

structure IMOSL.IMO2009A3.isNatTriangleSide (x y z : ℕ) : Prop

• side_x : x ≤ y + z
• side_y : y ≤ z + x
• side_z : z ≤ x + y

theorem IMOSL.IMO2009A3.isNatTriangleSide_iff (x y z : ℕ) : isNatTriangleSide x y z ↔ x ≤ y + z ∧ y ≤ z + x ∧ z ≤ x + y

theorem IMOSL.IMO2009A3.isNatTriangleSide.rotate {x y z : ℕ} (h : isNatTriangleSide x y z) : isNatTriangleSide y z x

theorem IMOSL.IMO2009A3.isNatTriangleSide.zero_left_imp {x y : ℕ} (h : isNatTriangleSide 0 x y) : x = y

Nat version

def IMOSL.IMO2009A3.good (f : ℕ → ℕ) : Prop

Equations

• IMOSL.IMO2009A3.good f = ∀ (x y : ℕ), IMOSL.IMO2009A3.isNatTriangleSide x (f y) (f (y + f x))

theorem IMOSL.IMO2009A3.final_solution_Nat {f : ℕ → ℕ} : good f ↔ f = fun (x : ℕ) => x

Final solution, Nat version

PNat version

theorem IMOSL.IMO2009A3.PNat_to_Nat_Prop {P : ℕ+ → Prop} : (∀ (n : ℕ+), P n) ↔ ∀ (n : ℕ), P n.succPNat

theorem IMOSL.IMO2009A3.PNat_to_Nat_Prop2 {P : ℕ+ → ℕ+ → Prop} : (∀ (m n : ℕ+), P m n) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat

structure IMOSL.IMO2009A3.isPNatTriangleSide (x y z : ℕ+) : Prop

• side_x : x < y + z
• side_y : y < z + x
• side_z : z < x + y

theorem IMOSL.IMO2009A3.isPNatTriangleSide_iff (x y z : ℕ+) : isPNatTriangleSide x y z ↔ x < y + z ∧ y < z + x ∧ z < x + y

theorem IMOSL.IMO2009A3.succPNat_add_succPNat (x y : ℕ) : x.succPNat + y.succPNat = (x + y + 1).succPNat

theorem IMOSL.IMO2009A3.le_add_iff_lt_succPNat_add {x y z : ℕ} : x ≤ y + z ↔ x.succPNat < y.succPNat + z.succPNat

theorem IMOSL.IMO2009A3.isNatTriangleSide_iff_isPNatTriangleSide {x y z : ℕ} : isNatTriangleSide x y z ↔ isPNatTriangleSide x.succPNat y.succPNat z.succPNat

def IMOSL.IMO2009A3.goodPNat (f : ℕ+ → ℕ+) : Prop

Equations

• IMOSL.IMO2009A3.goodPNat f = ∀ (x y : ℕ+), IMOSL.IMO2009A3.isPNatTriangleSide x (f y) (f (y + f x - 1))

theorem IMOSL.IMO2009A3.goodPNat_iff_good {f : ℕ+ → ℕ+} : goodPNat f ↔ good fun (x : ℕ) => (f x.succPNat).natPred

theorem IMOSL.IMO2009A3.final_solution {f : ℕ+ → ℕ+} : goodPNat f ↔ f = fun (x : ℕ+) => x

Final solution