theorem
proved
tactic proof
E_PBM_is_rung_6
show as:
view Lean formalization →
formal statement (Lean)
112theorem E_PBM_is_rung_6 : E_PBM = phi_energy_rung 6 := by
proof body
Tactic-mode proof.
113 unfold E_PBM phi_energy_rung E_base
114 have key : phi ^ (-(5 : ℝ)) * phi ^ (6 : ℝ) = phi := by
115 rw [← Real.rpow_add phi_pos,
116 (by norm_num : (-(5 : ℝ) + (6 : ℝ) : ℝ) = (1 : ℝ)),
117 Real.rpow_one]
118 have h : phi ^ (-(5 : ℝ)) * eV_to_J * phi ^ (6 : ℝ) = phi * eV_to_J := by
119 calc phi ^ (-(5 : ℝ)) * eV_to_J * phi ^ (6 : ℝ)
120 = phi ^ (-(5 : ℝ)) * phi ^ (6 : ℝ) * eV_to_J := by ring
121 _ = phi * eV_to_J := by rw [key]
122 exact h.symm
123
124/-- Division bounds helper: transfers E_PBM bounds to any positive numerator. -/