This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )