phi_pow_8_in_interval

formal source

 144  hi := 4699 / 100
 145  valid := by norm_num
 146
 147theorem phi_pow_8_in_interval : phi_pow_8_interval.contains (((1 + Real.sqrt 5) / 2) ^ (8 : ℝ)) := by
 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 -/
 159def phi_pow_5_interval : Interval where
 160  lo := 1109 / 100
 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