Theorem imul_rzero

Proof
imul_rzero. ⊢ a ∈ ℤ → a⋅0 = 0,
  pred_restr int_incl_in_real rmul_rzero.

Dependencies
The given proof depends on 11 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_distl_add, rneg_closed.