phi_pow_145_interval

formal source

  67  exact mul_pos phi_pow_102_lo_pos phi_pow_38_lo_pos
  68
  69/-- Interval for φ^145 = φ^140 * φ^5 -/
  70def phi_pow_145_interval : Interval :=
  71  mulPos phi_pow_140_interval phi_pow_5_interval phi_pow_140_lo_pos phi_pow_5_lo_pos
  72
  73theorem phi_pow_140_in_interval : phi_pow_140_interval.contains (goldenRatio ^ (140 : ℝ)) := by
  74  have h_in_51 : phi_pow_51_interval.contains (goldenRatio ^ (51 : ℝ)) := phi_pow_51_in_interval
  75  have h_in_102 : phi_pow_102_interval.contains (goldenRatio ^ (102 : ℝ)) := by
  76    unfold phi_pow_102_interval
  77    have : goldenRatio ^ (102 : ℝ) = goldenRatio ^ (51 : ℝ) * goldenRatio ^ (51 : ℝ) := by
  78      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  79    rw [this]
  80    apply mulPos_contains_mul phi_pow_51_lo_pos phi_pow_51_lo_pos h_in_51 h_in_51
  81
  82  have h_in_16 : phi_pow_16_interval.contains (goldenRatio ^ (16 : ℝ)) := phi_pow_16_in_interval
  83  have h_in_32 : phi_pow_32_interval.contains (goldenRatio ^ (32 : ℝ)) := by
  84    unfold phi_pow_32_interval
  85    have : goldenRatio ^ (32 : ℝ) = goldenRatio ^ (16 : ℝ) * goldenRatio ^ (16 : ℝ) := by
  86      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  87    rw [this]
  88    apply mulPos_contains_mul phi_pow_16_lo_pos phi_pow_16_lo_pos h_in_16 h_in_16
  89
  90  have h_in_5 : phi_pow_5_interval.contains (goldenRatio ^ (5 : ℝ)) := phi_pow_5_in_interval
  91  have h_in_37 : phi_pow_37_interval.contains (goldenRatio ^ (37 : ℝ)) := by
  92    unfold phi_pow_37_interval
  93    have : goldenRatio ^ (37 : ℝ) = goldenRatio ^ (32 : ℝ) * goldenRatio ^ (5 : ℝ) := by
  94      rw [← Real.rpow_add goldenRatio_pos]; norm_num
  95    rw [this]
  96    apply mulPos_contains_mul phi_pow_32_lo_pos phi_pow_5_lo_pos h_in_32 h_in_5
  97
  98  have h_in_1 : phiInterval.contains goldenRatio := phi_in_phiInterval
  99  have h_in_38 : phi_pow_38_interval.contains (goldenRatio ^ (38 : ℝ)) := by
 100    unfold phi_pow_38_interval