Theorem: float_pow_int_eq_le (HOLFloat/Float_theorem.lean)

State before:
r : ℤ
x : ℝ
m e : ℤ
⊢ x ≠ 0 → 1 ≤ m → abs x = ↑m * ↑r ^ e → ↑r ^ e ≤ abs x
Tactic:
intro hx hm he
State after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ abs x

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ abs x
Tactic:
rw [he]
State after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ ↑m * ↑r ^ e

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ ↑m * ↑r ^ e
Tactic:
apply float_real_le_1_le
State after:
case a
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e

case a
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 1 ≤ m

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e
Tactic:
case a =>
  norm_cast
  suffices abs x > 0 by simp_all only [lt_self_iff_false, ne_eq, Int.cast_lt_zero, Int.one_lt_zero_le_iff, Int.cast_eq_zero, gt_iff_lt, Int.cast_pos, zero_add, zero_lt_mul_left]
  simp; exact hx
State after:
no goals

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 1 ≤ m
Tactic:
case a =>
  exact hm
State after:
no goals

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e
Tactic:
suffices abs x > 0 by simp_all only [lt_self_iff_false, ne_eq, Int.cast_lt_zero, Int.one_lt_zero_le_iff, Int.cast_eq_zero, gt_iff_lt, Int.cast_pos, zero_add, zero_lt_mul_left]
State after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ abs x > 0

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ abs x > 0
Tactic:
simp
State after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ¬x = 0

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ¬x = 0
Tactic:
exact hx
State after:
no goals

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
this : abs x > 0
⊢ 0 < ↑r ^ e
Tactic:
simp_all only [lt_self_iff_false, ne_eq, Int.cast_lt_zero, Int.one_lt_zero_le_iff, Int.cast_eq_zero, gt_iff_lt, Int.cast_pos, zero_add, zero_lt_mul_left]
State after:
no goals

State before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 1 ≤ m
Tactic:
exact hm
State after:
no goals