54lemma phi_pow_ge_one (n : ℕ) : 1 ≤ phi ^ n := by
proof body
Tactic-mode proof.
55 induction n with 56 | zero => simp 57 | succ k ih => 58 have : phi ^ (k + 1) = phi ^ k * phi := pow_succ phi k 59 rw [this] 60 calc 1 = 1 * 1 := by ring 61 _ ≤ phi ^ k * phi := by 62 exact mul_le_mul ih (le_of_lt one_lt_phi) (by norm_num) (by positivity) 63 64/-- φ^m < φ^n when m < n. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.