mu_pred_lower

formal source

  67arithmetic.
  68-/
  69
  70theorem mu_pred_lower : (1898 : ℝ) < mu_pred := by
  71  unfold mu_pred
  72  have he_pos : 0 < electron_pred := electron_pred_pos
  73  rw [lt_div_iff₀ he_pos]
  74  -- want: 1898 * electron_pred < proton_binding_pred
  75  have he_hi : electron_pred < (0.5102 : ℝ) := electron_mass_bounds.2
  76  have hp_lo : (969 : ℝ) < proton_binding_pred := proton_mass_bounds.1
  77  -- 1898 * electron_pred < 1898 * 0.5102 = 968.3596 < 969 < proton_binding_pred
  78  have step1 : (1898 : ℝ) * electron_pred < (1898 : ℝ) * (0.5102 : ℝ) := by
  79    have h1898 : (0 : ℝ) < 1898 := by norm_num
  80    exact mul_lt_mul_of_pos_left he_hi h1898
  81  have step2 : (1898 : ℝ) * (0.5102 : ℝ) < (969 : ℝ) := by norm_num
  82  linarith
  83
  84theorem mu_pred_upper : mu_pred < (1904 : ℝ) := by
  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
  98theorem mu_pred_bracket : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ) :=
  99  ⟨mu_pred_lower, mu_pred_upper⟩
 100