theorem
proved
tactic proof
phi_pow_neg3_in_interval
show as:
view Lean formalization →
formal statement (Lean)
104theorem phi_pow_neg3_in_interval : phi_pow_neg3_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-3 : ℝ)) := by
proof body
Tactic-mode proof.
105 simp only [Interval.contains, phi_pow_neg3_interval]
106 rw [← phi_eq_formula]
107 have hpos : (0 : ℝ) < goldenRatio := Real.goldenRatio_pos
108 have h : goldenRatio ^ (-3 : ℝ) = goldenRatio⁻¹ ^ 3 := by
109 rw [Real.rpow_neg (le_of_lt hpos)]
110 have : (3 : ℝ) = (3 : ℕ) := by norm_num
111 rw [this, Real.rpow_natCast, inv_pow]
112 rw [h]
113 have hcontains := phi_inv3_in_interval_proven
114 simp only [Interval.contains, phi_inv3_interval_proven] at hcontains
115 constructor
116 · have h1 : ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
117 linarith [hcontains.1]
118 · have h1 : ((237 / 1000 : ℚ) : ℝ) = (0.237 : ℝ) := by norm_num
119 linarith [hcontains.2]
120
121/-- φ^51 interval - using proven bounds from PhiBounds -/