Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ ¬a = 0, hypo. 03. ⊢ 1 ∈ ℝ, calc. 04. 1, 2 ⊢ 1/a ∈ ℝ, rdiv_closed 3 1 2. rreci_closed. ⊢ a ∈ ℝ → ¬a = 0 → 1/a ∈ ℝ, subj_intro_ii 4.
Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rinv_closed, rmul_closed.