theorem
proved
tactic proof
npow_contains_pow
show as:
view Lean formalization →
formal statement (Lean)
149theorem npow_contains_pow {x : ℝ} {I : Interval} {n : ℕ}
150 (hIpos : 0 < I.lo) (hx : I.contains x) : (npow I n hIpos).contains (x ^ n) := by
proof body
Tactic-mode proof.
151 have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
152 have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
153 constructor
154 · simp only [npow, Rat.cast_pow]
155 exact pow_le_pow_left₀ (le_of_lt hIlo_pos) hx.1 n
156 · simp only [npow, Rat.cast_pow]
157 exact pow_le_pow_left₀ (le_of_lt hx_pos) hx.2 n
158
159/-! ## Bounds Checking -/
160
161/-- If b < I.lo, then all x in I satisfy b < x -/