Proof of Theorem pc2dvds
| Step | Hyp | Ref
| Expression |
| 1 | | pcdvdstr 16914 |
. . . . 5
⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)) |
| 2 | 1 | ancoms 458 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)) |
| 3 | 2 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)) |
| 4 | 3 | 3expia 1122 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 5 | | oveq2 7439 |
. . . . . 6
⊢ (𝐴 = 0 → (𝑝 pCnt 𝐴) = (𝑝 pCnt 0)) |
| 6 | 5 | breq1d 5153 |
. . . . 5
⊢ (𝐴 = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))) |
| 7 | 6 | ralbidv 3178 |
. . . 4
⊢ (𝐴 = 0 → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵))) |
| 8 | | breq1 5146 |
. . . 4
⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵)) |
| 9 | 7, 8 | imbi12d 344 |
. . 3
⊢ (𝐴 = 0 → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵))) |
| 10 | | gcddvds 16540 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 11 | 10 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
| 12 | | gcdcl 16543 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
| 13 | 12 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ) |
| 14 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∈
ℤ) |
| 15 | | dvdsabsb 16313 |
. . . . . . . . . . . 12
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴))) |
| 16 | 13, 14, 15 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ (abs‘𝐴))) |
| 17 | 11, 16 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴)) |
| 18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ (abs‘𝐴)) |
| 19 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0) |
| 20 | 19 | necon3ai 2965 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
| 21 | | gcdn0cl 16539 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 22 | 20, 21 | sylan2 593 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 23 | 22 | nnzd 12640 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℤ) |
| 24 | 22 | nnne0d 12316 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ≠ 0) |
| 25 | | nnabscl 15364 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℕ) |
| 26 | 25 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℕ) |
| 27 | 26 | nnzd 12640 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℤ) |
| 28 | | dvdsval2 16293 |
. . . . . . . . . 10
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ (abs‘𝐴) ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 29 | 23, 24, 27, 28 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) ∥ (abs‘𝐴) ↔ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 30 | 18, 29 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ) |
| 31 | | nnre 12273 |
. . . . . . . . . . 11
⊢
((abs‘𝐴)
∈ ℕ → (abs‘𝐴) ∈ ℝ) |
| 32 | | nngt0 12297 |
. . . . . . . . . . 11
⊢
((abs‘𝐴)
∈ ℕ → 0 < (abs‘𝐴)) |
| 33 | 31, 32 | jca 511 |
. . . . . . . . . 10
⊢
((abs‘𝐴)
∈ ℕ → ((abs‘𝐴) ∈ ℝ ∧ 0 <
(abs‘𝐴))) |
| 34 | | nnre 12273 |
. . . . . . . . . . 11
⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (𝐴 gcd 𝐵) ∈ ℝ) |
| 35 | | nngt0 12297 |
. . . . . . . . . . 11
⊢ ((𝐴 gcd 𝐵) ∈ ℕ → 0 < (𝐴 gcd 𝐵)) |
| 36 | 34, 35 | jca 511 |
. . . . . . . . . 10
⊢ ((𝐴 gcd 𝐵) ∈ ℕ → ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) |
| 37 | | divgt0 12136 |
. . . . . . . . . 10
⊢
((((abs‘𝐴)
∈ ℝ ∧ 0 < (abs‘𝐴)) ∧ ((𝐴 gcd 𝐵) ∈ ℝ ∧ 0 < (𝐴 gcd 𝐵))) → 0 < ((abs‘𝐴) / (𝐴 gcd 𝐵))) |
| 38 | 33, 36, 37 | syl2an 596 |
. . . . . . . . 9
⊢
(((abs‘𝐴)
∈ ℕ ∧ (𝐴 gcd
𝐵) ∈ ℕ) → 0
< ((abs‘𝐴) /
(𝐴 gcd 𝐵))) |
| 39 | 26, 22, 38 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 0 <
((abs‘𝐴) / (𝐴 gcd 𝐵))) |
| 40 | | elnnz 12623 |
. . . . . . . 8
⊢
(((abs‘𝐴) /
(𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℤ ∧ 0 <
((abs‘𝐴) / (𝐴 gcd 𝐵)))) |
| 41 | 30, 39, 40 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 42 | | elnn1uz2 12967 |
. . . . . . 7
⊢
(((abs‘𝐴) /
(𝐴 gcd 𝐵)) ∈ ℕ ↔ (((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈
(ℤ≥‘2))) |
| 43 | 41, 42 | sylib 218 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈
(ℤ≥‘2))) |
| 44 | 10 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
| 45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∥ 𝐵) |
| 46 | | breq1 5146 |
. . . . . . . . 9
⊢ ((𝐴 gcd 𝐵) = (abs‘𝐴) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵)) |
| 47 | 45, 46 | syl5ibcom 245 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) = (abs‘𝐴) → (abs‘𝐴) ∥ 𝐵)) |
| 48 | 26 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℂ) |
| 49 | 22 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 gcd 𝐵) ∈ ℂ) |
| 50 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → 1 ∈
ℂ) |
| 51 | 48, 49, 50, 24 | divmuld 12065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ ((𝐴 gcd 𝐵) · 1) = (abs‘𝐴))) |
| 52 | 49 | mulridd 11278 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → ((𝐴 gcd 𝐵) · 1) = (𝐴 gcd 𝐵)) |
| 53 | 52 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (((𝐴 gcd 𝐵) · 1) = (abs‘𝐴) ↔ (𝐴 gcd 𝐵) = (abs‘𝐴))) |
| 54 | 51, 53 | bitrd 279 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ↔ (𝐴 gcd 𝐵) = (abs‘𝐴))) |
| 55 | | absdvdsb 16312 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵)) |
| 56 | 55 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ↔ (abs‘𝐴) ∥ 𝐵)) |
| 57 | 47, 54, 56 | 3imtr4d 294 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 → 𝐴 ∥ 𝐵)) |
| 58 | | exprmfct 16741 |
. . . . . . . 8
⊢
(((abs‘𝐴) /
(𝐴 gcd 𝐵)) ∈ (ℤ≥‘2)
→ ∃𝑝 ∈
ℙ 𝑝 ∥
((abs‘𝐴) / (𝐴 gcd 𝐵))) |
| 59 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∈ ℙ) |
| 60 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℕ) |
| 61 | 60 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℤ) |
| 62 | 60 | nnne0d 12316 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ≠ 0) |
| 63 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 64 | | pcdiv 16890 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧
((abs‘𝐴) ∈
ℤ ∧ (abs‘𝐴)
≠ 0) ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 65 | 59, 61, 62, 63, 64 | syl121anc 1377 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 66 | | simplll 775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℤ) |
| 67 | | zq 12996 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℚ) |
| 68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ∈ ℚ) |
| 69 | | pcabs 16913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴)) |
| 70 | 59, 68, 69 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (abs‘𝐴)) = (𝑝 pCnt 𝐴)) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (abs‘𝐴)) − (𝑝 pCnt (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 72 | 65, 71 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) = ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 73 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵))) |
| 74 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) |
| 75 | | pcelnn 16908 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧
((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ ℕ) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) |
| 76 | 59, 74, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) |
| 77 | 73, 76 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt ((abs‘𝐴) / (𝐴 gcd 𝐵))) ∈ ℕ) |
| 78 | 72, 77 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ) |
| 79 | 59, 63 | pccld 16888 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈
ℕ0) |
| 80 | 79 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ) |
| 81 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐴 ≠ 0) |
| 82 | | pczcl 16886 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 83 | 59, 66, 81, 82 | syl12anc 837 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 84 | 83 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℤ) |
| 85 | | znnsub 12663 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)) |
| 86 | 80, 84, 85 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ((𝑝 pCnt 𝐴) − (𝑝 pCnt (𝐴 gcd 𝐵))) ∈ ℕ)) |
| 87 | 78, 86 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴)) |
| 88 | 79 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) ∈ ℝ) |
| 89 | 83 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ∈ ℝ) |
| 90 | 88, 89 | ltnled 11408 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt (𝐴 gcd 𝐵)) < (𝑝 pCnt 𝐴) ↔ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 91 | 87, 90 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵))) |
| 92 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ∈ ℤ) |
| 93 | | nprmdvds1 16743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ℙ → ¬
𝑝 ∥
1) |
| 94 | 93 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ 1) |
| 95 | | gcdid0 16557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℤ → (𝐴 gcd 0) = (abs‘𝐴)) |
| 96 | 66, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐴 gcd 0) = (abs‘𝐴)) |
| 97 | 96 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = ((abs‘𝐴) / (abs‘𝐴))) |
| 98 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (abs‘𝐴) ∈ ℂ) |
| 99 | 98, 62 | dividd 12041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (abs‘𝐴)) = 1) |
| 100 | 97, 99 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((abs‘𝐴) / (𝐴 gcd 0)) = 1) |
| 101 | 100 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) ↔ 𝑝 ∥ 1)) |
| 102 | 94, 101 | mtbird 325 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0))) |
| 103 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 = 0 → (𝐴 gcd 𝐵) = (𝐴 gcd 0)) |
| 104 | 103 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 = 0 → ((abs‘𝐴) / (𝐴 gcd 𝐵)) = ((abs‘𝐴) / (𝐴 gcd 0))) |
| 105 | 104 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = 0 → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ↔ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))) |
| 106 | 73, 105 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝐵 = 0 → 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)))) |
| 107 | 106 | necon3bd 2954 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (¬ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 0)) → 𝐵 ≠ 0)) |
| 108 | 102, 107 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → 𝐵 ≠ 0) |
| 109 | | pczcl 16886 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈
ℕ0) |
| 110 | 59, 92, 108, 109 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈
ℕ0) |
| 111 | 110 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐵) ∈ ℝ) |
| 112 | | lemin 13234 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))) |
| 113 | 89, 89, 111, 112 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))) |
| 114 | | pcgcd 16916 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
| 115 | 59, 66, 92, 114 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
| 116 | 115 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)) ↔ (𝑝 pCnt 𝐴) ≤ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)))) |
| 117 | 89 | leidd 11829 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴)) |
| 118 | 117 | biantrurd 532 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐴) ∧ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))) |
| 119 | 113, 116,
118 | 3bitr4rd 312 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝐴 gcd 𝐵)))) |
| 120 | 91, 119 | mtbird 325 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)))) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)) |
| 121 | 120 | expr 456 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 122 | 121 | reximdva 3168 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 123 | | rexnal 3100 |
. . . . . . . . 9
⊢
(∃𝑝 ∈
ℙ ¬ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)) |
| 124 | 122, 123 | imbitrdi 251 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∃𝑝 ∈ ℙ 𝑝 ∥ ((abs‘𝐴) / (𝐴 gcd 𝐵)) → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 125 | 58, 124 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ≥‘2)
→ ¬ ∀𝑝
∈ ℙ (𝑝 pCnt
𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 126 | 57, 125 | orim12d 967 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) →
((((abs‘𝐴) / (𝐴 gcd 𝐵)) = 1 ∨ ((abs‘𝐴) / (𝐴 gcd 𝐵)) ∈ (ℤ≥‘2))
→ (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵)))) |
| 127 | 43, 126 | mpd 15 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∥ 𝐵 ∨ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 128 | 127 | ord 865 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (¬ 𝐴 ∥ 𝐵 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
| 129 | 128 | con4d 115 |
. . 3
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ≠ 0) → (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵)) |
| 130 | | 2prm 16729 |
. . . . . 6
⊢ 2 ∈
ℙ |
| 131 | 130 | ne0ii 4344 |
. . . . 5
⊢ ℙ
≠ ∅ |
| 132 | | r19.2z 4495 |
. . . . 5
⊢ ((ℙ
≠ ∅ ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) |
| 133 | 131, 132 | mpan 690 |
. . . 4
⊢
(∀𝑝 ∈
ℙ (𝑝 pCnt 0) ≤
(𝑝 pCnt 𝐵) → ∃𝑝 ∈ ℙ (𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵)) |
| 134 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
| 135 | | zq 12996 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℚ) |
| 136 | 135 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈
ℚ) |
| 137 | | pcxcl 16899 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℚ) → (𝑝 pCnt 𝐵) ∈
ℝ*) |
| 138 | 134, 136,
137 | syl2anr 597 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈
ℝ*) |
| 139 | | pnfge 13172 |
. . . . . . . . . 10
⊢ ((𝑝 pCnt 𝐵) ∈ ℝ* → (𝑝 pCnt 𝐵) ≤ +∞) |
| 140 | 138, 139 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ≤ +∞) |
| 141 | 140 | biantrurd 532 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) →
(+∞ ≤ (𝑝 pCnt
𝐵) ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵)))) |
| 142 | | pc0 16892 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 0) =
+∞) |
| 143 | 142 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 0) =
+∞) |
| 144 | 143 | breq1d 5153 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ +∞ ≤ (𝑝 pCnt 𝐵))) |
| 145 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 146 | | xrletri3 13196 |
. . . . . . . . 9
⊢ (((𝑝 pCnt 𝐵) ∈ ℝ* ∧ +∞
∈ ℝ*) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵)))) |
| 147 | 138, 145,
146 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ ↔ ((𝑝 pCnt 𝐵) ≤ +∞ ∧ +∞ ≤ (𝑝 pCnt 𝐵)))) |
| 148 | 141, 144,
147 | 3bitr4d 311 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) ↔ (𝑝 pCnt 𝐵) = +∞)) |
| 149 | | pnfnre 11302 |
. . . . . . . . . 10
⊢ +∞
∉ ℝ |
| 150 | 149 | neli 3048 |
. . . . . . . . 9
⊢ ¬
+∞ ∈ ℝ |
| 151 | | eleq1 2829 |
. . . . . . . . 9
⊢ ((𝑝 pCnt 𝐵) = +∞ → ((𝑝 pCnt 𝐵) ∈ ℝ ↔ +∞ ∈
ℝ)) |
| 152 | 150, 151 | mtbiri 327 |
. . . . . . . 8
⊢ ((𝑝 pCnt 𝐵) = +∞ → ¬ (𝑝 pCnt 𝐵) ∈ ℝ) |
| 153 | 109 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ) |
| 154 | 153 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ) |
| 155 | 154 | an4s 660 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑝 ∈ ℙ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt 𝐵) ∈ ℝ) |
| 156 | 155 | expr 456 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (𝐵 ≠ 0 → (𝑝 pCnt 𝐵) ∈ ℝ)) |
| 157 | 156 | necon1bd 2958 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → (¬
(𝑝 pCnt 𝐵) ∈ ℝ → 𝐵 = 0)) |
| 158 | 152, 157 | syl5 34 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐵) = +∞ → 𝐵 = 0)) |
| 159 | 148, 158 | sylbid 240 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0)) |
| 160 | 159 | rexlimdva 3155 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(∃𝑝 ∈ ℙ
(𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 𝐵 = 0)) |
| 161 | | 0dvds 16314 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
| 162 | 161 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
| 163 | 160, 162 | sylibrd 259 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(∃𝑝 ∈ ℙ
(𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)) |
| 164 | 133, 163 | syl5 34 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(∀𝑝 ∈ ℙ
(𝑝 pCnt 0) ≤ (𝑝 pCnt 𝐵) → 0 ∥ 𝐵)) |
| 165 | 9, 129, 164 | pm2.61ne 3027 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(∀𝑝 ∈ ℙ
(𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵) → 𝐴 ∥ 𝐵)) |
| 166 | 4, 165 | impbid 212 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |