radd_neutl

Theorem radd_neutl

Theorem. radd_neutl
a ∈ ℝ → 0 + a = a

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. ⊢ 0 ∈ ℝ, calc.
03. 1 ⊢ a + 0 = a, radd_neutr 1.
04. 1 ⊢ 0 + a = a + 0, radd_comm 2 1.
05. 1 ⊢ 0 + a = a, eq_trans 4 3.
radd_neutl. ⊢ a ∈ ℝ → 0 + a = a, subj_intro 5.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, radd_comm, radd_neutr.