Proof of Theorem zmulcl
Step | Hyp | Ref
| Expression |
1 | | elznn0 8366 |
. 2
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0))) |
2 | | elznn0 8366 |
. 2
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
3 | | nn0mulcl 8324 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0) |
4 | 3 | orcd 684 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
5 | 4 | a1i 9 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
6 | | remulcl 7101 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 · 𝑁) ∈ ℝ) |
7 | 5, 6 | jctild 309 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
8 | | nn0mulcl 8324 |
. . . . . . . . 9
⊢ ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (-𝑀 · 𝑁) ∈
ℕ0) |
9 | | recn 7106 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ → 𝑀 ∈
ℂ) |
10 | | recn 7106 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
11 | | mulneg1 7499 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
12 | 9, 10, 11 | syl2an 283 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
13 | 12 | eleq1d 2147 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 · 𝑁) ∈ ℕ0 ↔ -(𝑀 · 𝑁) ∈
ℕ0)) |
14 | 8, 13 | syl5ib 152 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → -(𝑀 · 𝑁) ∈
ℕ0)) |
15 | | olc 664 |
. . . . . . . 8
⊢ (-(𝑀 · 𝑁) ∈ ℕ0 → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
16 | 14, 15 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
17 | 16, 6 | jctild 309 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
18 | | nn0mulcl 8324 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (𝑀 · -𝑁) ∈
ℕ0) |
19 | | mulneg2 7500 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
20 | 9, 10, 19 | syl2an 283 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
21 | 20 | eleq1d 2147 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 · -𝑁) ∈ ℕ0 ↔ -(𝑀 · 𝑁) ∈
ℕ0)) |
22 | 18, 21 | syl5ib 152 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → -(𝑀 · 𝑁) ∈
ℕ0)) |
23 | 22, 15 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
24 | 23, 6 | jctild 309 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
25 | | nn0mulcl 8324 |
. . . . . . . . 9
⊢ ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (-𝑀 · -𝑁) ∈
ℕ0) |
26 | | mul2neg 7502 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (-𝑀 · -𝑁) = (𝑀 · 𝑁)) |
27 | 9, 10, 26 | syl2an 283 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (-𝑀 · -𝑁) = (𝑀 · 𝑁)) |
28 | 27 | eleq1d 2147 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 · -𝑁) ∈ ℕ0 ↔ (𝑀 · 𝑁) ∈
ℕ0)) |
29 | 25, 28 | syl5ib 152 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → (𝑀 · 𝑁) ∈
ℕ0)) |
30 | | orc 665 |
. . . . . . . 8
⊢ ((𝑀 · 𝑁) ∈ ℕ0 → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)) |
31 | 29, 30 | syl6 33 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
32 | 31, 6 | jctild 309 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0) → ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
33 | 7, 17, 24, 32 | ccased 906 |
. . . . 5
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0)))) |
34 | | elznn0 8366 |
. . . . 5
⊢ ((𝑀 · 𝑁) ∈ ℤ ↔ ((𝑀 · 𝑁) ∈ ℝ ∧ ((𝑀 · 𝑁) ∈ ℕ0 ∨ -(𝑀 · 𝑁) ∈
ℕ0))) |
35 | 33, 34 | syl6ibr 160 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
→ (𝑀 · 𝑁) ∈
ℤ)) |
36 | 35 | imp 122 |
. . 3
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ ((𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
→ (𝑀 · 𝑁) ∈
ℤ) |
37 | 36 | an4s 552 |
. 2
⊢ (((𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0)) ∧ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
→ (𝑀 · 𝑁) ∈
ℤ) |
38 | 1, 2, 37 | syl2anb 285 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 · 𝑁) ∈ ℤ) |