Theorem: Imo2013P5.fixed_point_of_gt_1 (Compfiles/Imo2013P5.lean)

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
⊢ f x = ↑x
Tactic:
obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt (1 + x) ha1
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
⊢ f x = ↑x
Tactic:
have h_big_enough : (1:ℚ) < a^N - x := lt_sub_iff_add_lt.mpr hN
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
⊢ f x = ↑x
Tactic:
have h1 := calc (x : ℝ) + ((a^N - x) : ℚ)
              ≤ f x + ((a^N - x) : ℚ) := add_le_add_right (H5 x hx) _
            _ ≤ f x + f (a^N - x)     := add_le_add_left (H5 _ h_big_enough) _
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
⊢ f x = ↑x
Tactic:
have hxp : 0 < x := zero_lt_one.trans hx
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ f x = ↑x
Tactic:
have hNp : 0 < N := by
  by_contra H; push_neg at H; rw [le_zero_iff.mp H] at hN; linarith
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f x = ↑x
Tactic:
have h2 := calc f x + f (a^N - x)
              ≤ f (x + (a^N - x)) := H2 x (a^N - x) hxp (zero_lt_one.trans h_big_enough)
            _ = f (a^N)           := by ring_nf
            _ = (a^N : ℝ)         := fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae
            _ = (x:ℝ) + ((a^N:ℝ) - (x:ℝ))     := by ring
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x = ↑x
Tactic:
have heq := h1.antisymm (by exact_mod_cast h2)
State after:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
heq : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x)
⊢ f x = ↑x

State before:
case intro
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
heq : ↑x + ↑(a ^ N - x) = f x + f (a ^ N - x)
⊢ f x = ↑x
Tactic:
linarith [H5 x hx, H5 _ h_big_enough]
State after:
no goals

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
⊢ 0 < N
Tactic:
by_contra H
State after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : ¬0 < N
⊢ False

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : ¬0 < N
⊢ False
Tactic:
push_neg at H
State after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Tactic:
rw [le_zero_iff.mp H] at hN
State after:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ 0
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ 0
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
H : N ≤ 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ f (x + (a ^ N - x)) = f (a ^ N)
Tactic:
ring_nf
State after:
no goals

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
⊢ ↑a ^ N = ↑x + (↑a ^ N - ↑x)
Tactic:
ring
State after:
no goals

State before:
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
H5 : ∀ (x : ℚ), 1 < x → ↑x ≤ f x
a : ℚ
ha1 : 1 < a
hae : f a = ↑a
N : ℕ
hN : 1 + x < a ^ N
h_big_enough : 1 < a ^ N - x
h1 : ↑x + ↑(a ^ N - x) ≤ f x + f (a ^ N - x)
hxp : 0 < x
hNp : 0 < N
h2 : f x + f (a ^ N - x) ≤ ↑x + (↑a ^ N - ↑x)
⊢ f x + f (a ^ N - x) ≤ ↑x + ↑(a ^ N - x)
Tactic:
exact_mod_cast h2
State after:
no goals