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

phi11_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)

 176private lemma phi11_gt : (198.9 : ℝ) < Constants.phi ^ (11 : ℕ) := by

proof body

Tactic-mode proof.

 177  rw [phi_eq_goldenRatio]
 178  have h8 := Numerics.phi_pow8_gt
 179  have h3 := Numerics.phi_cubed_gt
 180  have hpos : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 181  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 182  rw [heq]
 183  calc (198.9 : ℝ) < (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
 184    _ < Real.goldenRatio ^ 8 * (4.236 : ℝ) := by nlinarith
 185    _ < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by nlinarith
 186

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.