imul_neutl

Theorem. imul_neutl
a ∈ ℤ → 1⋅a = a

Proof
imul_neutl. ⊢ a ∈ ℤ → 1⋅a = a,
  pred_restr int_incl_in_real rmul_neutl.

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