Step | Hyp | Ref
| Expression |
1 | | simpr 108 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) |
2 | | breq1 3788 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → (𝑧 ∥ 𝐷 ↔ 𝑤 ∥ 𝐷)) |
3 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑧 ∥ 𝐴 ↔ 𝑤 ∥ 𝐴)) |
4 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑧 ∥ 𝐵 ↔ 𝑤 ∥ 𝐵)) |
5 | 3, 4 | anbi12d 456 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵))) |
6 | 2, 5 | bibi12d 233 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → ((𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ↔ (𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵)))) |
7 | | equcom 1633 |
. . . . . . 7
⊢ (𝑧 = 𝑤 ↔ 𝑤 = 𝑧) |
8 | | bicom 138 |
. . . . . . 7
⊢ (((𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ↔ (𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵))) ↔ ((𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵)) ↔ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))) |
9 | 6, 7, 8 | 3imtr3i 198 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵)) ↔ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))) |
10 | | bezoutlemgcd.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) |
11 | 6 | cbvralv 2577 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ↔ ∀𝑤 ∈ ℤ (𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵))) |
12 | 10, 11 | sylib 120 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ ℤ (𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵))) |
13 | 12 | ad2antrr 471 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → ∀𝑤 ∈ ℤ (𝑤 ∥ 𝐷 ↔ (𝑤 ∥ 𝐴 ∧ 𝑤 ∥ 𝐵))) |
14 | | simplr 496 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝑧 ∈ ℤ) |
15 | 9, 13, 14 | rspcdva 2707 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) |
16 | 1, 15 | mpbird 165 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝑧 ∥ 𝐷) |
17 | | bezoutlemgcd.3 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
18 | 17 | ad2antrr 471 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐷 ∈
ℕ0) |
19 | | bezoutlemgcd.5 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
20 | 19 | ad2antrr 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
21 | | breq1 3788 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → (𝑧 ∥ 𝐷 ↔ 0 ∥ 𝐷)) |
22 | | breq1 3788 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧 ∥ 𝐴 ↔ 0 ∥ 𝐴)) |
23 | | breq1 3788 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧 ∥ 𝐵 ↔ 0 ∥ 𝐵)) |
24 | 22, 23 | anbi12d 456 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) ↔ (0 ∥ 𝐴 ∧ 0 ∥ 𝐵))) |
25 | 21, 24 | bibi12d 233 |
. . . . . . . . . . 11
⊢ (𝑧 = 0 → ((𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ↔ (0 ∥ 𝐷 ↔ (0 ∥ 𝐴 ∧ 0 ∥ 𝐵)))) |
26 | | 0zd 8363 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
27 | 25, 10, 26 | rspcdva 2707 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ∥ 𝐷 ↔ (0 ∥ 𝐴 ∧ 0 ∥ 𝐵))) |
28 | 27 | ad2antrr 471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (0 ∥ 𝐷 ↔ (0 ∥ 𝐴 ∧ 0 ∥ 𝐵))) |
29 | 18 | nn0zd 8467 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐷 ∈ ℤ) |
30 | | 0dvds 10215 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ → (0
∥ 𝐷 ↔ 𝐷 = 0)) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (0 ∥ 𝐷 ↔ 𝐷 = 0)) |
32 | | bezoutlemgcd.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
33 | 32 | ad2antrr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐴 ∈ ℤ) |
34 | | 0dvds 10215 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (0
∥ 𝐴 ↔ 𝐴 = 0)) |
35 | 33, 34 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (0 ∥ 𝐴 ↔ 𝐴 = 0)) |
36 | | bezoutlemgcd.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℤ) |
37 | 36 | ad2antrr 471 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐵 ∈ ℤ) |
38 | | 0dvds 10215 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
39 | 37, 38 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (0 ∥ 𝐵 ↔ 𝐵 = 0)) |
40 | 35, 39 | anbi12d 456 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → ((0 ∥ 𝐴 ∧ 0 ∥ 𝐵) ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
41 | 28, 31, 40 | 3bitr3d 216 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (𝐷 = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
42 | 20, 41 | mtbird 630 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → ¬ 𝐷 = 0) |
43 | 42 | neqned 2252 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐷 ≠ 0) |
44 | | elnnne0 8302 |
. . . . . 6
⊢ (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0
∧ 𝐷 ≠
0)) |
45 | 18, 43, 44 | sylanbrc 408 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝐷 ∈ ℕ) |
46 | | dvdsle 10244 |
. . . . 5
⊢ ((𝑧 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑧 ∥ 𝐷 → 𝑧 ≤ 𝐷)) |
47 | 14, 45, 46 | syl2anc 403 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → (𝑧 ∥ 𝐷 → 𝑧 ≤ 𝐷)) |
48 | 16, 47 | mpd 13 |
. . 3
⊢ (((𝜑 ∧ 𝑧 ∈ ℤ) ∧ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) → 𝑧 ≤ 𝐷) |
49 | 48 | ex 113 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) → 𝑧 ≤ 𝐷)) |
50 | 49 | ralrimiva 2434 |
1
⊢ (𝜑 → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) → 𝑧 ≤ 𝐷)) |