# Metamath Proof Explorer

## Theorem zmulcl

Description: Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004)

Ref Expression
Assertion zmulcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\cdot {N}\in ℤ$

### Proof

Step Hyp Ref Expression
1 elznn0 ${⊢}{M}\in ℤ↔\left({M}\in ℝ\wedge \left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\right)$
2 elznn0 ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)$
3 nn0mulcl ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {M}\cdot {N}\in {ℕ}_{0}$
4 3 orcd ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)$
5 4 a1i ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)$
6 remulcl ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {M}\cdot {N}\in ℝ$
7 5 6 jctild ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)\right)$
8 nn0mulcl ${⊢}\left(-{M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to -{M}\cdot {N}\in {ℕ}_{0}$
9 recn ${⊢}{M}\in ℝ\to {M}\in ℂ$
10 recn ${⊢}{N}\in ℝ\to {N}\in ℂ$
11 mulneg1 ${⊢}\left({M}\in ℂ\wedge {N}\in ℂ\right)\to -{M}\cdot {N}=-{M}\cdot {N}$
12 9 10 11 syl2an ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to -{M}\cdot {N}=-{M}\cdot {N}$
13 12 eleq1d ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(-{M}\cdot {N}\in {ℕ}_{0}↔-{M}\cdot {N}\in {ℕ}_{0}\right)$
14 8 13 syl5ib ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to -{M}\cdot {N}\in {ℕ}_{0}\right)$
15 olc ${⊢}-{M}\cdot {N}\in {ℕ}_{0}\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)$
16 14 15 syl6 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)$
17 16 6 jctild ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)\right)$
18 nn0mulcl ${⊢}\left({M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to {M}-{N}\in {ℕ}_{0}$
19 mulneg2 ${⊢}\left({M}\in ℂ\wedge {N}\in ℂ\right)\to {M}-{N}=-{M}\cdot {N}$
20 9 10 19 syl2an ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to {M}-{N}=-{M}\cdot {N}$
21 20 eleq1d ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left({M}-{N}\in {ℕ}_{0}↔-{M}\cdot {N}\in {ℕ}_{0}\right)$
22 18 21 syl5ib ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to -{M}\cdot {N}\in {ℕ}_{0}\right)$
23 22 15 syl6 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)$
24 23 6 jctild ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)\right)$
25 nn0mulcl ${⊢}\left(-{M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to -{M}-{N}\in {ℕ}_{0}$
26 mul2neg ${⊢}\left({M}\in ℂ\wedge {N}\in ℂ\right)\to -{M}-{N}={M}\cdot {N}$
27 9 10 26 syl2an ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to -{M}-{N}={M}\cdot {N}$
28 27 eleq1d ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(-{M}-{N}\in {ℕ}_{0}↔{M}\cdot {N}\in {ℕ}_{0}\right)$
29 25 28 syl5ib ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to {M}\cdot {N}\in {ℕ}_{0}\right)$
30 orc ${⊢}{M}\cdot {N}\in {ℕ}_{0}\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)$
31 29 30 syl6 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)$
32 31 6 jctild ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(-{M}\in {ℕ}_{0}\wedge -{N}\in {ℕ}_{0}\right)\to \left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)\right)$
33 7 17 24 32 ccased ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(\left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)\to \left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)\right)$
34 elznn0 ${⊢}{M}\cdot {N}\in ℤ↔\left({M}\cdot {N}\in ℝ\wedge \left({M}\cdot {N}\in {ℕ}_{0}\vee -{M}\cdot {N}\in {ℕ}_{0}\right)\right)$
35 33 34 syl6ibr ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(\left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)\to {M}\cdot {N}\in ℤ\right)$
36 35 imp ${⊢}\left(\left({M}\in ℝ\wedge {N}\in ℝ\right)\wedge \left(\left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)\right)\to {M}\cdot {N}\in ℤ$
37 36 an4s ${⊢}\left(\left({M}\in ℝ\wedge \left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\right)\wedge \left({N}\in ℝ\wedge \left({N}\in {ℕ}_{0}\vee -{N}\in {ℕ}_{0}\right)\right)\right)\to {M}\cdot {N}\in ℤ$
38 1 2 37 syl2anb ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\cdot {N}\in ℤ$