rmul_neutl

Theorem rmul_neutl

Theorem. rmul_neutl
a ∈ ℝ → 1⋅a = a

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. ⊢ 1 ∈ ℝ, calc.
03. 1 ⊢ a⋅1 = a, rmul_neutr 1.
04. 1 ⊢ 1⋅a = a⋅1, rmul_comm 2 1.
05. 1 ⊢ 1⋅a = a, eq_trans 4 3.
rmul_neutl. ⊢ a ∈ ℝ → 1⋅a = a, subj_intro 5.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rmul_comm, rmul_neutr.