Step | Hyp | Ref
| Expression |
1 | | prmuz2 16137 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2))) |
3 | 2 | anim1d 614 |
. . . . 5
⊢ (𝜑 → ((𝑝 ∈ ℙ ∧ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) → (𝑝 ∈ (ℤ≥‘2)
∧ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)))) |
4 | 3 | reximdv2 3181 |
. . . 4
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → ∃𝑝 ∈
(ℤ≥‘2)(𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵))) |
5 | | breq1 5033 |
. . . . . 6
⊢ (𝑝 = 𝑖 → (𝑝 ∥ 𝐴 ↔ 𝑖 ∥ 𝐴)) |
6 | | breq1 5033 |
. . . . . 6
⊢ (𝑝 = 𝑖 → (𝑝 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵)) |
7 | 5, 6 | anbi12d 634 |
. . . . 5
⊢ (𝑝 = 𝑖 → ((𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) ↔ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
8 | 7 | cbvrexvw 3350 |
. . . 4
⊢
(∃𝑝 ∈
(ℤ≥‘2)(𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) ↔ ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
9 | 4, 8 | syl6ib 254 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) → ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
10 | | exprmfct 16145 |
. . . . . 6
⊢ (𝑖 ∈
(ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑖) |
11 | 10 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑖) |
12 | | prmnn 16115 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
13 | 12 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑝 ∈ ℕ) |
14 | 13 | nnzd 12167 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑝 ∈ ℤ) |
15 | | eluzelz 12334 |
. . . . . . . . . . 11
⊢ (𝑖 ∈
(ℤ≥‘2) → 𝑖 ∈ ℤ) |
16 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) ∧ 𝑝 ∥ 𝑖) → 𝑖 ∈ ℤ) |
17 | 16 | ad4ant24 754 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑖 ∈ ℤ) |
18 | | prmdvdsncoprmbd.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℕ) |
19 | 18 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝐴 ∈ ℕ) |
20 | 19 | nnzd 12167 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝐴 ∈ ℤ) |
21 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑝 ∥ 𝑖) |
22 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) → 𝑖 ∥ 𝐴) |
23 | 22 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑖 ∥ 𝐴) |
24 | 14, 17, 20, 21, 23 | dvdstrd 15740 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑝 ∥ 𝐴) |
25 | | prmdvdsncoprmbd.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℕ) |
26 | 25 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝐵 ∈ ℕ) |
27 | 26 | nnzd 12167 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝐵 ∈ ℤ) |
28 | | simprrr 782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) → 𝑖 ∥ 𝐵) |
29 | 28 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑖 ∥ 𝐵) |
30 | 14, 17, 27, 21, 29 | dvdstrd 15740 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → 𝑝 ∥ 𝐵) |
31 | 24, 30 | jca 515 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑖) → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) |
32 | 31 | ex 416 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ 𝑖 → (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵))) |
33 | 32 | reximdva 3184 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) → (∃𝑝 ∈ ℙ 𝑝 ∥ 𝑖 → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵))) |
34 | 11, 33 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵)) |
35 | 34 | rexlimdvaa 3195 |
. . 3
⊢ (𝜑 → (∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵))) |
36 | 9, 35 | impbid 215 |
. 2
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) ↔ ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
37 | | ncoprmgcdne1b 16091 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |
38 | 18, 25, 37 | syl2anc 587 |
. 2
⊢ (𝜑 → (∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |
39 | 36, 38 | bitrd 282 |
1
⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |