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

phi_pow_8_in_interval

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)

 147theorem phi_pow_8_in_interval : phi_pow_8_interval.contains (((1 + Real.sqrt 5) / 2) ^ (8 : ℝ)) := by

proof body

Tactic-mode proof.

 148  simp only [Interval.contains, phi_pow_8_interval]
 149  rw [← phi_eq_formula]
 150  have h : goldenRatio ^ (8 : ℝ) = goldenRatio ^ 8 := by
 151    have : (8 : ℝ) = (8 : ℕ) := by norm_num
 152    rw [this, Real.rpow_natCast]
 153  rw [h]
 154  have hcontains := phi_pow8_in_interval_proven
 155  simp only [Interval.contains, phi_pow8_interval_proven] at hcontains
 156  exact hcontains
 157
 158/-- φ^5 interval ≈ 11.09 - PROVEN -/

depends on (9)

Lean names referenced from this declaration's body.