Theorem rsq_non_zero

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ ¬a = 0, hypo.
03. 3 ⊢ a⋅a = 0, hypo.
04. 3 ⊢ a⋅a⋅(1/a) = 0⋅(1/a), eq_cong 3, f t = t⋅(1/a).
05. 1, 2 ⊢ 1/a ∈ ℝ, rreci_closed 1 2.
06. 1, 2 ⊢ 0⋅(1/a) = 0, rmul_lzero 5.
07. 1, 2, 3 ⊢ a⋅a⋅(1/a) = 0, eq_trans 4 6.
08. 1, 2 ⊢ a⋅a⋅(1/a) = a⋅(a⋅(1/a)), rmul_assoc 1 1 5.
09. 1, 2 ⊢ a⋅(1/a) = 1, rmul_reci_cancel 1 2.
10. 1, 2 ⊢ a⋅a⋅(1/a) = a⋅1,
  eq_subst 9 8, P t ↔ a⋅a⋅(1/a) = a⋅t.
11. 1, 2, 3 ⊢ a⋅1 = 0, eq_trans_ll 10 7.
12. 1 ⊢ a⋅1 = a, rmul_neutr 1.
13. 1, 2, 3 ⊢ a = 0, eq_trans_ll 12 11.
14. 1, 2, 3 ⊢ ⊥, neg_elim 2 13.
15. 1, 2 ⊢ ¬a⋅a = 0, neg_intro 14.
rsq_non_zero. ⊢ a ∈ ℝ → ¬a = 0 → ¬a⋅a = 0,
  subj_intro_ii 15.

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