Theorem rreci_non_zero

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ ¬a = 0, hypo.
03. 3 ⊢ 1/a = 0, hypo.
04. 3 ⊢ a⋅(1/a) = a⋅0, eq_cong 3, f t = a⋅t.
05. 1, 2 ⊢ a⋅(1/a) = 1, rmul_reci_cancel 1 2.
06. 1, 2, 3 ⊢ a⋅0 = 1, eq_trans_ll 4 5.
07. 1 ⊢ a⋅0 = 0, rmul_rzero 1.
08. 1, 2, 3 ⊢ 0 = 1, eq_trans_ll 7 6.
09. ⊢ ¬0 = 1, calc.
10. 1, 2, 3 ⊢ ⊥, neg_elim 9 8.
11. 1, 2 ⊢ ¬1/a = 0, neg_intro 10.
rreci_non_zero. ⊢ a ∈ ℝ → ¬a = 0 → ¬1/a = 0,
  subj_intro_ii 11.

Dependencies
The given proof depends on 14 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rinv_closed, rmul_closed, rmul_comm, rmul_distl_add, rmul_inv, rmul_neutr, rneg_closed.