rdiv_self

Theorem rdiv_self

Theorem. rdiv_self
a ∈ ℝ → ¬a = 0 → a/a = 1

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ ¬a = 0, hypo.
03. ⊢ a/a = a⋅(/a), rdiv_eq.
04. 1, 2 ⊢ a⋅(/a) = 1, rmul_inv 1 2.
05. 1, 2 ⊢ a/a = 1, eq_trans 3 4.
rdiv_self. ⊢ a ∈ ℝ → ¬a = 0 → a/a = 1, subj_intro_ii 5.

Dependencies
The given proof depends on three axioms:
eq_refl, eq_subst, rmul_inv.