Theorem imul_distr_sub

Theorem. imul_distr_sub
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a - b)⋅c = a⋅c - b⋅c
Proof
imul_distr_sub. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a - b)⋅c = a⋅c - b⋅c,
  pred_iii_restr int_incl_in_real rmul_distr_sub.

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