Proof of Theorem nnproddivdvdsd
Step | Hyp | Ref
| Expression |
1 | | nnproddivdvdsd.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℂ) |
3 | 2 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑁 ∈ ℂ) |
4 | | nnproddivdvdsd.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℕ) |
5 | 4 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) |
6 | 5 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝐾 ∈ ℂ) |
7 | | nnproddivdvdsd.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
8 | 7 | nncnd 11675 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
9 | 8 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑀 ∈ ℂ) |
10 | 4 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝐾 ∈ ℕ) |
11 | | nnne0 11693 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝐾 ≠ 0) |
13 | 7 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑀 ∈ ℕ) |
14 | 13 | nnne0d 11709 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑀 ≠ 0) |
15 | 3, 6, 9, 12, 14 | divdiv1d 11470 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → ((𝑁 / 𝐾) / 𝑀) = (𝑁 / (𝐾 · 𝑀))) |
16 | 15 | eqcomd 2765 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝑁 / (𝐾 · 𝑀)) = ((𝑁 / 𝐾) / 𝑀)) |
17 | 3, 6, 9, 12, 14 | divdiv32d 11464 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → ((𝑁 / 𝐾) / 𝑀) = ((𝑁 / 𝑀) / 𝐾)) |
18 | 16, 17 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝑁 / (𝐾 · 𝑀)) = ((𝑁 / 𝑀) / 𝐾)) |
19 | 4, 7 | nnmulcld 11712 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · 𝑀) ∈ ℕ) |
20 | 19, 1 | nndivdvdsd 39552 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 ↔ (𝑁 / (𝐾 · 𝑀)) ∈ ℕ)) |
21 | 20 | biimpd 232 |
. . . . . 6
⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 → (𝑁 / (𝐾 · 𝑀)) ∈ ℕ)) |
22 | 21 | imp 411 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝑁 / (𝐾 · 𝑀)) ∈ ℕ) |
23 | 18, 22 | eqeltrrd 2852 |
. . . 4
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → ((𝑁 / 𝑀) / 𝐾) ∈ ℕ) |
24 | 4 | nnzd 12110 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) |
25 | 7 | nnzd 12110 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
26 | 1 | nnzd 12110 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
27 | 24, 25, 26 | 3jca 1126 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
28 | | muldvds2 15668 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁)) |
30 | 29 | imp 411 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑀 ∥ 𝑁) |
31 | 1 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝑁 ∈ ℕ) |
32 | 13, 31 | nndivdvdsd 39552 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ)) |
33 | 30, 32 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝑁 / 𝑀) ∈ ℕ) |
34 | 10, 33 | nndivdvdsd 39552 |
. . . 4
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → (𝐾 ∥ (𝑁 / 𝑀) ↔ ((𝑁 / 𝑀) / 𝐾) ∈ ℕ)) |
35 | 23, 34 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ (𝐾 · 𝑀) ∥ 𝑁) → 𝐾 ∥ (𝑁 / 𝑀)) |
36 | 35 | ex 417 |
. 2
⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ (𝑁 / 𝑀))) |
37 | | dvdszrcl 15645 |
. . . . . . 7
⊢ (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 ∈ ℤ ∧ (𝑁 / 𝑀) ∈ ℤ)) |
38 | 37 | simprd 500 |
. . . . . 6
⊢ (𝐾 ∥ (𝑁 / 𝑀) → (𝑁 / 𝑀) ∈ ℤ) |
39 | 38 | adantl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∥ (𝑁 / 𝑀)) → (𝑁 / 𝑀) ∈ ℤ) |
40 | | dvdsmulc 15670 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀))) |
41 | 24, 40 | syl3an1 1161 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀))) |
42 | 25, 41 | syl3an3 1163 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 / 𝑀) ∈ ℤ ∧ 𝜑) → (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀))) |
43 | 42 | 3anidm13 1418 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 / 𝑀) ∈ ℤ) → (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀))) |
44 | 43 | impancom 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∥ (𝑁 / 𝑀)) → ((𝑁 / 𝑀) ∈ ℤ → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀))) |
45 | 39, 44 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∥ (𝑁 / 𝑀)) → (𝐾 · 𝑀) ∥ ((𝑁 / 𝑀) · 𝑀)) |
46 | 7 | nnne0d 11709 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≠ 0) |
47 | 2, 8, 46 | divcan1d 11440 |
. . . . 5
⊢ (𝜑 → ((𝑁 / 𝑀) · 𝑀) = 𝑁) |
48 | 47 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∥ (𝑁 / 𝑀)) → ((𝑁 / 𝑀) · 𝑀) = 𝑁) |
49 | 45, 48 | breqtrd 5051 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∥ (𝑁 / 𝑀)) → (𝐾 · 𝑀) ∥ 𝑁) |
50 | 49 | ex 417 |
. 2
⊢ (𝜑 → (𝐾 ∥ (𝑁 / 𝑀) → (𝐾 · 𝑀) ∥ 𝑁)) |
51 | 36, 50 | impbid 215 |
1
⊢ (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁 ↔ 𝐾 ∥ (𝑁 / 𝑀))) |