Proof 01. 1 ⊢ a ∈ ℝ, hypo. 02. ⊢ 0 ∈ ℝ, calc. 03. ⊢ 0 + 0 = 0, radd_neutr 2. 04. ⊢ a⋅(0 + 0) = a⋅0, eq_cong 3, f t = a⋅t. 05. 1 ⊢ a⋅(0 + 0) = a⋅0 + a⋅0, rmul_distl_add 1 2 2. 06. 1 ⊢ a⋅0 + a⋅0 = a⋅0, eq_trans_ll 5 4. 07. 1 ⊢ a⋅0 ∈ ℝ, rmul_closed 1 2. 08. 1 ⊢ a⋅0 + 0 = a⋅0, radd_neutr 7. 09. 1 ⊢ a⋅0 + a⋅0 = a⋅0 + 0, eq_trans_rr 6 8. 10. 1 ⊢ a⋅0 = 0, radd_cancel_ll 7 2 7 9. rmul_rzero. ⊢ a ∈ ℝ → a⋅0 = 0, subj_intro 10.
Dependencies
The given proof depends on 10 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_distl_add, rneg_closed.