theorem
proved
tactic proof
lifetime_decreases
show as:
view Lean formalization →
formal statement (Lean)
110theorem lifetime_decreases (M₁ M₂ : ℝ) (hM₁ : 1 < M₁) (h : M₁ < M₂) :
111 ms_lifetime M₂ < ms_lifetime M₁ := by
proof body
Tactic-mode proof.
112 unfold ms_lifetime luminosity_scaling nuclear_efficiency
113 have hM₁pos : 0 < M₁ := by linarith
114 have hM₂pos : 0 < M₂ := by linarith
115 have hpow : M₁ ^ (2.9 : ℝ) < M₂ ^ (2.9 : ℝ) :=
116 Real.rpow_lt_rpow (le_of_lt hM₁pos) h (by norm_num)
117 have hpow₁_pos : 0 < M₁ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₁pos _
118 have hpow₂_pos : 0 < M₂ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₂pos _
119 have hrecip : 1 / M₂ ^ (2.9 : ℝ) < 1 / M₁ ^ (2.9 : ℝ) :=
120 one_div_lt_one_div_of_lt hpow₁_pos hpow
121 have hconst : 0 < (7e-3 : ℝ) * 0.7 := by
122 norm_num
123 have hrewrite₁ : (7e-3 : ℝ) * 0.7 * M₁ / M₁ ^ (3.9 : ℝ) =
124 (7e-3 : ℝ) * 0.7 / M₁ ^ (2.9 : ℝ) := by
125 rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₁pos, Real.rpow_one]
126 field_simp [hM₁pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₁pos _)]
127 have hrewrite₂ : (7e-3 : ℝ) * 0.7 * M₂ / M₂ ^ (3.9 : ℝ) =
128 (7e-3 : ℝ) * 0.7 / M₂ ^ (2.9 : ℝ) := by
129 rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₂pos, Real.rpow_one]
130 field_simp [hM₂pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₂pos _)]
131 rw [hrewrite₂, hrewrite₁]
132 simpa [one_div] using mul_lt_mul_of_pos_left hrecip hconst
133
134/-- **SOLAR LIFETIME**: t_MS(M_sun) ≈ 10 Gyr. -/