Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. ⊢ 0 ∈ ℝ, calc. 03. 1 ⊢ 0 ≤ a ∨ a ≤ 0, rle_total 2 1. 04. 4 ⊢ 0 ≤ a, hypo. 05. 1, 4 ⊢ 0 ≤ a⋅a, rle_compat_mul 1 1 4 4. 06. 6 ⊢ a ≤ 0, hypo. 07. 1, 6 ⊢ -0 ≤ -a, rle_neg_swaps 1 2 6. 08. ⊢ 0 = -0, calc. 09. 1, 6 ⊢ 0 ≤ -a, eq_le_trans 8 7. 10. 1 ⊢ -a ∈ ℝ, rneg_closed 1. 11. 1, 6 ⊢ 0 ≤ (-a)⋅(-a), rle_compat_mul 10 10 9 9. 12. 1 ⊢ (-a)⋅(-a) = a⋅a, rmul_cancel_neg 1 1. 13. 1, 6 ⊢ 0 ≤ a⋅a, le_eq_trans 11 12. 14. 1 ⊢ 0 ≤ a⋅a, disj_elim 3 5 13. rsq_is_non_negative. ⊢ a ∈ ℝ → 0 ≤ a⋅a, subj_intro 14.
Dependencies
The given proof depends on 14 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_compat_add, rle_compat_mul, rle_total, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.