Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ ¬a = 0, hypo. 03. 1, 2 ⊢ /a ∈ ℝ, rinv_closed 1 2. 04. ⊢ 1/a = 1⋅(/a), rdiv_eq. 05. 1, 2 ⊢ 1⋅(/a) = /a, rmul_neutl 3. 06. 1, 2 ⊢ 1/a = /a, eq_trans 4 5. rdiv_reci. ⊢ a ∈ ℝ → ¬a = 0 → 1/a = /a, subj_intro_ii 6.
Dependencies
The given proof depends on five axioms:
eq_refl, eq_subst, rinv_closed, rmul_comm, rmul_neutr.