alphaG_pred_eq

formal source

  88    simpa [h1over, mul_assoc, mul_comm, mul_left_comm]
  89  rw [hA]
  90
  91theorem alphaG_pred_eq :
  92    row_alphaG_pred = electron_structural_mass ^ 2 * phi ^ (10 : ℝ) / Real.pi := by
  93  have hc : hbar * c = hbar := hbar_c_eq_hbar
  94  rw [row_alphaG_pred, hc]
  95  have h1 : G * electron_structural_mass ^ 2 / hbar
  96        = (G / hbar) * electron_structural_mass ^ 2 := by
  97    have hh : hbar ≠ 0 := ne_of_gt hbar_pos
  98    field_simp [hh]
  99  rw [h1, G_div_hbar]
 100  ring
 101
 102theorem alphaG_pred_closed :
 103    row_alphaG_pred = ((2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ)) / Real.pi := by
 104  have hme : electron_structural_mass = (2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ) := electron_structural_mass_forced
 105  have h2n : (2 : ℝ) ≠ 0 := by norm_num
 106  have hA2 : ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) := by
 107    rw [pow_two, ← zpow_add₀ h2n]
 108    norm_num
 109  have h0 : (phi : ℝ) ≠ 0 := phi_ne_zero
 110  have hBz : (phi : ℝ) ^ (51 : ℤ) * (phi : ℝ) ^ (51 : ℤ) = (phi : ℝ) ^ (102 : ℤ) := by
 111    rw [← zpow_add₀ h0]
 112    norm_num
 113  have hφsq : ((phi : ℝ) ^ (51 : ℤ)) ^ 2 = (phi : ℝ) ^ (102 : ℤ) := by
 114    rw [pow_two]
 115    exact hBz
 116  have hsq : (electron_structural_mass) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ) := by
 117    rw [hme, pow_two]
 118    have hre :
 119        ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ)) * ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ))
 120          = ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 * ((phi : ℝ) ^ (51 : ℤ)) ^ 2 := by
 121      ring