pith. machine review for the scientific record. sign in
lemma proved tactic proof

phi17_gt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 199private lemma phi17_gt : (3569 : ℝ) < Constants.phi ^ (17 : ℕ) := by

proof body

Tactic-mode proof.

 200  rw [phi_eq_goldenRatio]
 201  have h8_lo := Numerics.phi_pow8_gt
 202  have hφ_lo := Numerics.phi_gt_1618
 203  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 204  have hpos16 : (0 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 := by positivity
 205  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 206  rw [heq]
 207  have h16_lo : (46.97 : ℝ) * (46.97 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 :=
 208    mul_lt_mul h8_lo (le_of_lt h8_lo) (by norm_num) (le_of_lt hpos8)
 209  have h17_lo : (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) <
 210      Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio :=
 211    mul_lt_mul h16_lo (le_of_lt hφ_lo) (by norm_num) (le_of_lt hpos16)
 212  linarith [show (3569 : ℝ) < (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) from by norm_num]
 213

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.