Proof of Theorem zmulcl
Step | Hyp | Ref
| Expression |
1 | | elznn0 9182 |
. 2
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0))) |
2 | | elznn0 9182 |
. 2
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
3 | | nn0mulcl 9126 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0) |
4 | 3 | orcd 723 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
5 | 4 | a1i 9 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
6 | | remulcl 7860 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 · 𝑁) ∈ ℝ) |
7 | 5, 6 | jctild 314 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
8 | | nn0mulcl 9126 |
. . . . . . . . 9
⊢ ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (-𝑀 · 𝑁) ∈
ℕ0) |
9 | | recn 7865 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → 𝑀 ∈
ℂ) |
10 | | recn 7865 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
11 | | mulneg1 8270 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
12 | 9, 10, 11 | syl2an 287 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
13 | 12 | eleq1d 2226 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 · 𝑁) ∈ ℕ0 ↔ -(𝑀 · 𝑁) ∈
ℕ0)) |
14 | 8, 13 | syl5ib 153 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → -(𝑀 · 𝑁) ∈
ℕ0)) |
15 | | olc 701 |
. . . . . . . 8
⊢ (-(𝑀 · 𝑁) ∈ ℕ0 → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
16 | 14, 15 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
17 | 16, 6 | jctild 314 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
18 | | nn0mulcl 9126 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (𝑀 · -𝑁) ∈
ℕ0) |
19 | | mulneg2 8271 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
20 | 9, 10, 19 | syl2an 287 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
21 | 20 | eleq1d 2226 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 · -𝑁) ∈ ℕ0 ↔ -(𝑀 · 𝑁) ∈
ℕ0)) |
22 | 18, 21 | syl5ib 153 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → -(𝑀 · 𝑁) ∈
ℕ0)) |
23 | 22, 15 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
24 | 23, 6 | jctild 314 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
25 | | nn0mulcl 9126 |
. . . . . . . . 9
⊢ ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (-𝑀 · -𝑁) ∈
ℕ0) |
26 | | mul2neg 8273 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (-𝑀 · -𝑁) = (𝑀 · 𝑁)) |
27 | 9, 10, 26 | syl2an 287 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (-𝑀 · -𝑁) = (𝑀 · 𝑁)) |
28 | 27 | eleq1d 2226 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 · -𝑁) ∈ ℕ0 ↔ (𝑀 · 𝑁) ∈
ℕ0)) |
29 | 25, 28 | syl5ib 153 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0)) |
30 | | orc 702 |
. . . . . . . 8
⊢ ((𝑀 · 𝑁) ∈ ℕ0 → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
31 | 29, 30 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
32 | 31, 6 | jctild 314 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
33 | 7, 17, 24, 32 | ccased 950 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
34 | | elznn0 9182 |
. . . . 5
⊢ ((𝑀 · 𝑁) ∈ ℤ ↔ ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
35 | 33, 34 | syl6ibr 161 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
→ (𝑀 · 𝑁) ∈
ℤ)) |
36 | 35 | imp 123 |
. . 3
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ ((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
→ (𝑀 · 𝑁) ∈
ℤ) |
37 | 36 | an4s 578 |
. 2
⊢ (((𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0)) ∧ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
→ (𝑀 · 𝑁) ∈
ℤ) |
38 | 1, 2, 37 | syl2anb 289 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) |