lemma
proved
tactic proof
one_le_B_of
show as:
view Lean formalization →
formal statement (Lean)
23lemma one_le_B_of (k : Nat) : (1 : ℝ) ≤ B_of k := by
proof body
Tactic-mode proof.
24 induction k with
25 | zero => simp [B_of]
26 | succ k ih =>
27 have hmul : (2 : ℝ) ≤ 2 * B_of k := by
28 have : 2 * (1 : ℝ) ≤ 2 * B_of k := by
29 have hnonneg : 0 ≤ (2 : ℝ) := by norm_num
30 exact mul_le_mul_of_nonneg_left ih hnonneg
31 simpa using this
32 have h12 : (1 : ℝ) ≤ 2 := by norm_num
33 have : (1 : ℝ) ≤ 2 * B_of k := le_trans h12 hmul
34 simpa [B_of_succ, mul_comm] using this
35
36/-- Two to an integer power: 2^k for k ∈ ℤ. -/