Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. ⊢ 0 ∈ ℝ, calc. 03. 1 ⊢ 0⋅a = a⋅0, rmul_comm 2 1. 04. 1 ⊢ a⋅0 = 0, rmul_rzero 1. 05. 1 ⊢ 0⋅a = 0, eq_trans 3 4. rmul_lzero. ⊢ a ∈ ℝ → 0⋅a = 0, subj_intro 5.
Dependencies
The given proof depends on 11 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.