alphaG_pred_upper

proof body

Tactic-mode proof.

 170  have hφ : phi < (1.6185 : ℝ) := by
 171    simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_lt_16185
 172  have hpiLB : (3.1415 : ℝ) < (Real.pi : ℝ) := by
 173    linarith [Real.pi_gt_d6, Real.pi_pos]
 174  have hN : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) := by
 175    have hr112 : (phi : ℝ) ^ (112 : ℝ) < (1.6185 : ℝ) ^ (112 : ℝ) := by
 176      exact Real.rpow_lt_rpow (by nlinarith [phi_pos, hφ]) hφ (by nlinarith)
 177    nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 178  have h0 :
 179      (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) < (4.85e9 : ℝ) * (3.1415 : ℝ) := by
 180    nlinarith
 181  have h1 : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi < (4.85e9 : ℝ) := by
 182    have hltNum : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (4.85e9 : ℝ) * Real.pi := by
 183      nlinarith [h0, hN, hpiLB, Real.pi_pos]
 184    rw [div_lt_iff₀ Real.pi_pos]
 185    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 186  simpa [alphaG_pred_closed] using h1
 187