Proof of Theorem pcdvdsb
| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . 4
⊢ (𝑁 = 0 → (𝑃 pCnt 𝑁) = (𝑃 pCnt 0)) |
| 2 | 1 | breq2d 5155 |
. . 3
⊢ (𝑁 = 0 → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ 𝐴 ≤ (𝑃 pCnt 0))) |
| 3 | | breq2 5147 |
. . 3
⊢ (𝑁 = 0 → ((𝑃↑𝐴) ∥ 𝑁 ↔ (𝑃↑𝐴) ∥ 0)) |
| 4 | 2, 3 | bibi12d 345 |
. 2
⊢ (𝑁 = 0 → ((𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁) ↔ (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0))) |
| 5 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝐴 ∈
ℕ0) |
| 6 | 5 | nn0zd 12639 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝐴 ∈
ℤ) |
| 7 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝑃 ∈
ℙ) |
| 8 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝑁 ∈
ℤ) |
| 9 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝑁 ≠ 0) |
| 10 | | pczcl 16886 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈
ℕ0) |
| 11 | 7, 8, 9, 10 | syl12anc 837 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃 pCnt 𝑁) ∈
ℕ0) |
| 12 | 11 | nn0zd 12639 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃 pCnt 𝑁) ∈ ℤ) |
| 13 | | eluz 12892 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 pCnt 𝑁) ∈ ℤ) → ((𝑃 pCnt 𝑁) ∈ (ℤ≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁))) |
| 14 | 6, 12, 13 | syl2anc 584 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃 pCnt 𝑁) ∈ (ℤ≥‘𝐴) ↔ 𝐴 ≤ (𝑃 pCnt 𝑁))) |
| 15 | | prmnn 16711 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 16 | 7, 15 | syl 17 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝑃 ∈
ℕ) |
| 17 | 16 | nnzd 12640 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
𝑃 ∈
ℤ) |
| 18 | | dvdsexp 16365 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0
∧ (𝑃 pCnt 𝑁) ∈
(ℤ≥‘𝐴)) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁))) |
| 19 | 18 | 3expia 1122 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ ((𝑃 pCnt 𝑁) ∈
(ℤ≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))) |
| 20 | 17, 5, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃 pCnt 𝑁) ∈ (ℤ≥‘𝐴) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))) |
| 21 | 14, 20 | sylbird 260 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)))) |
| 22 | | pczdvds 16901 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) |
| 23 | 7, 8, 9, 22 | syl12anc 837 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) |
| 24 | | nnexpcl 14115 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∈
ℕ) |
| 25 | 15, 24 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∈
ℕ) |
| 26 | 25 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∈
ℕ) |
| 27 | 26 | nnzd 12640 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∈
ℤ) |
| 28 | 27 | adantr 480 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑𝐴) ∈ ℤ) |
| 29 | 16, 11 | nnexpcld 14284 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑(𝑃 pCnt 𝑁)) ∈ ℕ) |
| 30 | 29 | nnzd 12640 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ) |
| 31 | | dvdstr 16331 |
. . . . . 6
⊢ (((𝑃↑𝐴) ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁)) |
| 32 | 28, 30, 8, 31 | syl3anc 1373 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) ∧ (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) → (𝑃↑𝐴) ∥ 𝑁)) |
| 33 | 23, 32 | mpan2d 694 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃↑𝐴) ∥ (𝑃↑(𝑃 pCnt 𝑁)) → (𝑃↑𝐴) ∥ 𝑁)) |
| 34 | 21, 33 | syld 47 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝐴 ≤ (𝑃 pCnt 𝑁) → (𝑃↑𝐴) ∥ 𝑁)) |
| 35 | | nn0re 12535 |
. . . . . . 7
⊢ ((𝑃 pCnt 𝑁) ∈ ℕ0 → (𝑃 pCnt 𝑁) ∈ ℝ) |
| 36 | | nn0re 12535 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
| 37 | | ltnle 11340 |
. . . . . . 7
⊢ (((𝑃 pCnt 𝑁) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁))) |
| 38 | 35, 36, 37 | syl2an 596 |
. . . . . 6
⊢ (((𝑃 pCnt 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑃 pCnt 𝑁) < 𝐴 ↔ ¬ 𝐴 ≤ (𝑃 pCnt 𝑁))) |
| 39 | | nn0ltp1le 12676 |
. . . . . 6
⊢ (((𝑃 pCnt 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ ((𝑃 pCnt 𝑁) < 𝐴 ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴)) |
| 40 | 38, 39 | bitr3d 281 |
. . . . 5
⊢ (((𝑃 pCnt 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0)
→ (¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴)) |
| 41 | 11, 5, 40 | syl2anc 584 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(¬ 𝐴 ≤ (𝑃 pCnt 𝑁) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴)) |
| 42 | | peano2nn0 12566 |
. . . . . . . . 9
⊢ ((𝑃 pCnt 𝑁) ∈ ℕ0 → ((𝑃 pCnt 𝑁) + 1) ∈
ℕ0) |
| 43 | 11, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃 pCnt 𝑁) + 1) ∈
ℕ0) |
| 44 | 43 | nn0zd 12639 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃 pCnt 𝑁) + 1) ∈ ℤ) |
| 45 | | eluz 12892 |
. . . . . . 7
⊢ ((((𝑃 pCnt 𝑁) + 1) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈
(ℤ≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴)) |
| 46 | 44, 6, 45 | syl2anc 584 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝐴 ∈
(ℤ≥‘((𝑃 pCnt 𝑁) + 1)) ↔ ((𝑃 pCnt 𝑁) + 1) ≤ 𝐴)) |
| 47 | | dvdsexp 16365 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ0 ∧
𝐴 ∈
(ℤ≥‘((𝑃 pCnt 𝑁) + 1))) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴)) |
| 48 | 47 | 3expia 1122 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 pCnt 𝑁) + 1) ∈ ℕ0) →
(𝐴 ∈
(ℤ≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))) |
| 49 | 17, 43, 48 | syl2anc 584 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝐴 ∈
(ℤ≥‘((𝑃 pCnt 𝑁) + 1)) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))) |
| 50 | 46, 49 | sylbird 260 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴))) |
| 51 | | pczndvds 16903 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) |
| 52 | 7, 8, 9, 51 | syl12anc 837 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) |
| 53 | 16, 43 | nnexpcld 14284 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℕ) |
| 54 | 53 | nnzd 12640 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ) |
| 55 | | dvdstr 16331 |
. . . . . . . 8
⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∈ ℤ ∧ (𝑃↑𝐴) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)) |
| 56 | 54, 28, 8, 55 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁) → (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)) |
| 57 | 52, 56 | mtod 198 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁)) |
| 58 | | imnan 399 |
. . . . . 6
⊢ (((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁) ↔ ¬ ((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) ∧ (𝑃↑𝐴) ∥ 𝑁)) |
| 59 | 57, 58 | sylibr 234 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
((𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ (𝑃↑𝐴) → ¬ (𝑃↑𝐴) ∥ 𝑁)) |
| 60 | 50, 59 | syld 47 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(((𝑃 pCnt 𝑁) + 1) ≤ 𝐴 → ¬ (𝑃↑𝐴) ∥ 𝑁)) |
| 61 | 41, 60 | sylbid 240 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(¬ 𝐴 ≤ (𝑃 pCnt 𝑁) → ¬ (𝑃↑𝐴) ∥ 𝑁)) |
| 62 | 34, 61 | impcon4bid 227 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
∧ 𝑁 ≠ 0) →
(𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) |
| 63 | 36 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ∈
ℝ) |
| 64 | 63 | rexrd 11311 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ∈
ℝ*) |
| 65 | | pnfge 13172 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤
+∞) |
| 66 | 64, 65 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ≤
+∞) |
| 67 | | pc0 16892 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) =
+∞) |
| 68 | 67 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝑃 pCnt 0) =
+∞) |
| 69 | 66, 68 | breqtrrd 5171 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ 𝐴 ≤ (𝑃 pCnt 0)) |
| 70 | | dvds0 16309 |
. . . 4
⊢ ((𝑃↑𝐴) ∈ ℤ → (𝑃↑𝐴) ∥ 0) |
| 71 | 27, 70 | syl 17 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∥ 0) |
| 72 | 69, 71 | 2thd 265 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ≤ (𝑃 pCnt 0) ↔ (𝑃↑𝐴) ∥ 0)) |
| 73 | 4, 62, 72 | pm2.61ne 3027 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) |