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

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ x ≤ y
Tactic:
by_contra! hxy
State after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
⊢ False

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
⊢ False
Tactic:
have hxmy : 0 < x - y := sub_pos.mpr hxy
State after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
⊢ False

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
⊢ False
Tactic:
have hn : ∀ n : ℕ, (x - y) * (n : ℝ) ≤ x^n - y^n := fun n ↦ by
  have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x^i * y^(n - 1 - i) := by
    intro i _
    calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
         _ = x^i * 1         := (mul_one _).symm
         _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
  calc (x - y) * (n : ℝ)
      = (n : ℝ) * (x - y) := mul_comm _ _
    _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
                               by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                  Finset.card_range]
    _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                                (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
    _ = x^n - y^n         := geom_sum₂_mul x y n
State after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
⊢ False

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
⊢ False
Tactic:
obtain ⟨N, hN⟩ := exists_nat_gt (1 / (x - y))
State after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ False

State before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ False
Tactic:
have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
State after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ False

State before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ False
Tactic:
have h1 := calc 1 = (x - y) * (1 / (x - y)) := by field_simp
             _ < (x - y) * N             := (mul_lt_mul_left hxmy).mpr hN
             _ ≤ x^N - y^N               := hn N
State after:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
h1 : 1 < x ^ N - y ^ N
⊢ False

State before:
case intro
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
h1 : 1 < x ^ N - y ^ N
⊢ False
Tactic:
linarith only [h1, h N hNp]
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
Tactic:
have hterm : ∀ i : ℕ, i ∈ Finset.range n → 1 ≤ x^i * y^(n - 1 - i) := by
  intro i _
  calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
       _ = x^i * 1         := (mul_one _).symm
       _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
State after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ↑n ≤ x ^ n - y ^ n
Tactic:
calc (x - y) * (n : ℝ)
    = (n : ℝ) * (x - y) := mul_comm _ _
  _ = (∑ _i in Finset.range n, (1 : ℝ)) * (x - y) :=
                             by simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
                                Finset.card_range]
  _ ≤ (∑ i in Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x-y) :=
                              (mul_le_mul_right hxmy).mpr (Finset.sum_le_sum hterm)
  _ = x^n - y^n         := geom_sum₂_mul x y n
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
intro i _
State after:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ x ^ i * y ^ (n - 1 - i)

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
     _ = x^i * 1         := (mul_one _).symm
     _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ x ^ i * 1 ≤ x ^ i * y ^ (n - 1 - i)
Tactic:
gcongr
State after:
case h
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ y ^ (n - 1 - i)

State before:
case h
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ y ^ (n - 1 - i)
Tactic:
apply one_le_pow_of_one_le hy.le
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n : ℕ
hterm : ∀ i ∈ Finset.range n, 1 ≤ x ^ i * y ^ (n - 1 - i)
⊢ ↑n * (x - y) = (∑ _i ∈ Finset.range n, 1) * (x - y)
Tactic:
simp only [mul_one, Finset.sum_const, nsmul_eq_mul,
Finset.card_range]
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
⊢ 0 < N
Tactic:
exact_mod_cast (one_div_pos.mpr hxmy).trans hN
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
hn : ∀ (n : ℕ), (x - y) * ↑n ≤ x ^ n - y ^ n
N : ℕ
hN : 1 / (x - y) < ↑N
hNp : 0 < N
⊢ 1 = (x - y) * (1 / (x - y))
Tactic:
field_simp
State after:
no goals