Theorem zmulcl

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

	Ref	Expression
Assertion	zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		elznn0	⊢ ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ) )
2		elznn0	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) )
3		nn0mulcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
4	3	orcd	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
5	4	a1i	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) )
6		remulcl	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 · 𝑁 ) ∈ ℝ )
7	5 6	jctild	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) ) )
8		nn0mulcl	⊢ ( ( - 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑀 · 𝑁 ) ∈ ℕ0 )
9		recn	⊢ ( 𝑀 ∈ ℝ → 𝑀 ∈ ℂ )
10		recn	⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
11		mulneg1	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - 𝑀 · 𝑁 ) = - ( 𝑀 · 𝑁 ) )
12	9 10 11	syl2an	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( - 𝑀 · 𝑁 ) = - ( 𝑀 · 𝑁 ) )
13	12	eleq1d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 · 𝑁 ) ∈ ℕ0 ↔ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
14	8 13	imbitrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
15		olc	⊢ ( - ( 𝑀 · 𝑁 ) ∈ ℕ0 → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
16	14 15	syl6	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) )
17	16 6	jctild	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) ) )
18		nn0mulcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( 𝑀 · - 𝑁 ) ∈ ℕ0 )
19		mulneg2	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 · - 𝑁 ) = - ( 𝑀 · 𝑁 ) )
20	9 10 19	syl2an	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 · - 𝑁 ) = - ( 𝑀 · 𝑁 ) )
21	20	eleq1d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 · - 𝑁 ) ∈ ℕ0 ↔ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
22	18 21	imbitrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
23	22 15	syl6	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) )
24	23 6	jctild	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) ) )
25		nn0mulcl	⊢ ( ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( - 𝑀 · - 𝑁 ) ∈ ℕ0 )
26		mul2neg	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - 𝑀 · - 𝑁 ) = ( 𝑀 · 𝑁 ) )
27	9 10 26	syl2an	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( - 𝑀 · - 𝑁 ) = ( 𝑀 · 𝑁 ) )
28	27	eleq1d	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 · - 𝑁 ) ∈ ℕ0 ↔ ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
29	25 28	imbitrid	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
30		orc	⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) )
31	29 30	syl6	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) )
32	31 6	jctild	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( - 𝑀 ∈ ℕ0 ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) ) )
33	7 17 24 32	ccased	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) → ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) ) )
34		elznn0	⊢ ( ( 𝑀 · 𝑁 ) ∈ ℤ ↔ ( ( 𝑀 · 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 · 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 · 𝑁 ) ∈ ℕ0 ) ) )
35	33 34	imbitrrdi	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ ) )
36	35	imp	⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
37	36	an4s	⊢ ( ( ( 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∨ - 𝑁 ∈ ℕ0 ) ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
38	1 2 37	syl2anb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )