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

units_self_consistent

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)

 227theorem units_self_consistent :
 228    ∀ (ℏ' G' c' : ℝ), ℏ' > 0 → G' > 0 → c' > 0 →
 229    tau0 = sqrt (ℏ' * G' / (Real.pi * c' ^ 3)) / c' →
 230    ell0 = c' * tau0 →
 231    ℏ' = Real.pi * c' ^ 5 * tau0 ^ 2 / G' := by

proof body

Tactic-mode proof.

 232  intro ℏ' G' c' hℏ hG hc htau _hell
 233  have hc_ne : c' ≠ 0 := ne_of_gt hc
 234  have hG_ne : G' ≠ 0 := ne_of_gt hG
 235  have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 236  have hc3 : c' ^ 3 ≠ 0 := pow_ne_zero 3 hc_ne
 237  have hc5 : c' ^ 5 ≠ 0 := pow_ne_zero 5 hc_ne
 238  have hinner_nonneg : 0 ≤ ℏ' * G' / (Real.pi * c' ^ 3) := by
 239    apply div_nonneg (mul_nonneg (le_of_lt hℏ) (le_of_lt hG))
 240    exact le_of_lt (mul_pos Real.pi_pos (pow_pos hc 3))
 241  have hsq : tau0 ^ 2 = ℏ' * G' / (Real.pi * c' ^ 5) := by
 242    rw [htau, div_pow, sq_sqrt hinner_nonneg]
 243    field_simp
 244  rw [hsq]
 245  field_simp
 246
 247/-! ## Bridge to Foundation -/
 248

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.