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

phi11_lt

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)

 187private lemma phi11_lt : Constants.phi ^ (11 : ℕ) < (200 : ℝ) := by

proof body

Tactic-mode proof.

 188  rw [phi_eq_goldenRatio]
 189  have h8 := Numerics.phi_pow8_lt
 190  have h3 := Numerics.phi_cubed_lt
 191  have hpos : (0 : ℝ) < Real.goldenRatio ^ 3 := by positivity
 192  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 193  rw [heq]
 194  calc Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3
 195      < (46.99 : ℝ) * Real.goldenRatio ^ 3 := by nlinarith
 196    _ < (46.99 : ℝ) * (4.237 : ℝ) := by nlinarith
 197    _ < (200 : ℝ) := by norm_num
 198

used by (2)

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.