phi_pow_140_interval

formal source

  59  exact mul_pos phi_pow_37_lo_pos phi_lo_pos
  60
  61/-- Interval for φ^140 = φ^102 * φ^38 -/
  62def phi_pow_140_interval : Interval :=
  63  mulPos phi_pow_102_interval phi_pow_38_interval phi_pow_102_lo_pos phi_pow_38_lo_pos
  64
  65lemma phi_pow_140_lo_pos : (0 : ℚ) < phi_pow_140_interval.lo := by
  66  unfold phi_pow_140_interval mulPos; dsimp
  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