Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. 2 ⊢ ¬a = 0, hypo. 03. 1 ⊢ 0 ≤ a⋅a, rsq_is_non_negative 1. 04. 1, 2 ⊢ ¬a⋅a = 0, rsq_non_zero 1 2. 05. 1, 2 ⊢ ¬0 = a⋅a, neq_symm 4. 06. 1, 2 ⊢ 0 < a⋅a, lt_intro 3 5. rsq_is_positive. ⊢ a ∈ ℝ → ¬a = 0 → 0 < a⋅a, subj_intro_ii 6.
Dependencies
The given proof depends on 18 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rinv_closed, rle_compat_add, rle_compat_mul, rle_total, rmul_assoc, rmul_closed, rmul_comm, rmul_distl_add, rmul_inv, rmul_neutr, rneg_closed.