phi_pow_5_in_interval

formal source

 161  hi := 111 / 10
 162  valid := by norm_num
 163
 164theorem phi_pow_5_in_interval : phi_pow_5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (5 : ℝ)) := by
 165  simp only [Interval.contains, phi_pow_5_interval]
 166  rw [← phi_eq_formula]
 167  have h : goldenRatio ^ (5 : ℝ) = goldenRatio ^ 5 := by
 168    have : (5 : ℝ) = (5 : ℕ) := by norm_num
 169    rw [this, Real.rpow_natCast]
 170  rw [h]
 171  constructor
 172  · have h1 := phi_pow5_gt
 173    calc ((1109 / 100 : ℚ) : ℝ) = (11.09 : ℝ) := by norm_num
 174      _ ≤ goldenRatio ^ 5 := le_of_lt h1
 175  · have h1 := phi_pow5_lt
 176    calc goldenRatio ^ 5 ≤ (11.1 : ℝ) := le_of_lt h1
 177      _ = ((111 / 10 : ℚ) : ℝ) := by norm_num
 178
 179/-- φ^16 interval ≈ 2207 - PROVEN -/
 180def phi_pow_16_interval : Interval where
 181  lo := 22069 / 10
 182  hi := 22075 / 10
 183  valid := by norm_num
 184
 185theorem phi_pow_16_in_interval : phi_pow_16_interval.contains (((1 + Real.sqrt 5) / 2) ^ (16 : ℝ)) := by
 186  simp only [Interval.contains, phi_pow_16_interval]
 187  rw [← phi_eq_formula]
 188  have h : goldenRatio ^ (16 : ℝ) = goldenRatio ^ 16 := by
 189    have : (16 : ℝ) = (16 : ℕ) := by norm_num
 190    rw [this, Real.rpow_natCast]
 191  rw [h]
 192  constructor
 193  · have h1 := phi_pow16_gt
 194    calc ((22069 / 10 : ℚ) : ℝ) = (2206.9 : ℝ) := by norm_num