pith. machine review for the scientific record. sign in
theorem proved tactic proof

mu_pred_upper

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  84theorem mu_pred_upper : mu_pred < (1904 : ℝ) := by

proof body

Tactic-mode proof.

  85  unfold mu_pred
  86  have he_pos : 0 < electron_pred := electron_pred_pos
  87  rw [div_lt_iff₀ he_pos]
  88  -- want: proton_binding_pred < 1904 * electron_pred
  89  have he_lo : (0.5098 : ℝ) < electron_pred := electron_mass_bounds.1
  90  have hp_hi : proton_binding_pred < (970.4 : ℝ) := proton_mass_bounds.2
  91  -- proton_binding_pred < 970.4 < 1904 * 0.5098 = 970.6592 < 1904 * electron_pred
  92  have step1 : (970.4 : ℝ) < (1904 : ℝ) * (0.5098 : ℝ) := by norm_num
  93  have step2 : (1904 : ℝ) * (0.5098 : ℝ) < (1904 : ℝ) * electron_pred := by
  94    have h1904 : (0 : ℝ) < 1904 := by norm_num
  95    exact mul_lt_mul_of_pos_left he_lo h1904
  96  linarith
  97

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.