Proof of Theorem pcdvdstr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0z 12626 | . . . . . . 7
⊢ 0 ∈
ℤ | 
| 2 |  | zq 12997 | . . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ ℚ) | 
| 3 | 1, 2 | ax-mp 5 | . . . . . 6
⊢ 0 ∈
ℚ | 
| 4 |  | pcxcl 16900 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 0 ∈
ℚ) → (𝑃 pCnt 0)
∈ ℝ*) | 
| 5 | 3, 4 | mpan2 691 | . . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ∈
ℝ*) | 
| 6 | 5 | xrleidd 13195 | . . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) | 
| 7 | 6 | ad2antrr 726 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) | 
| 8 |  | simpr 484 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 = 0) | 
| 9 | 8 | oveq2d 7448 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) = (𝑃 pCnt 0)) | 
| 10 |  | simplr3 1217 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 ∥ 𝐵) | 
| 11 | 8, 10 | eqbrtrrd 5166 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 0 ∥ 𝐵) | 
| 12 |  | simplr2 1216 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 ∈ ℤ) | 
| 13 |  | 0dvds 16315 | . . . . . 6
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) | 
| 14 | 12, 13 | syl 17 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (0 ∥ 𝐵 ↔ 𝐵 = 0)) | 
| 15 | 11, 14 | mpbid 232 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 = 0) | 
| 16 | 15 | oveq2d 7448 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐵) = (𝑃 pCnt 0)) | 
| 17 | 7, 9, 16 | 3brtr4d 5174 | . 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) | 
| 18 |  | prmnn 16712 | . . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 19 | 18 | ad2antrr 726 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℕ) | 
| 20 |  | simpll 766 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℙ) | 
| 21 |  | simplr1 1215 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) | 
| 22 |  | simpr 484 | . . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) | 
| 23 |  | pczcl 16887 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈
ℕ0) | 
| 24 | 20, 21, 22, 23 | syl12anc 836 | . . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ∈
ℕ0) | 
| 25 | 19, 24 | nnexpcld 14285 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) | 
| 26 | 25 | nnzd 12642 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) | 
| 27 |  | simplr2 1216 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℤ) | 
| 28 |  | pczdvds 16902 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) | 
| 29 | 20, 21, 22, 28 | syl12anc 836 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) | 
| 30 |  | simplr3 1217 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∥ 𝐵) | 
| 31 | 26, 21, 27, 29, 30 | dvdstrd 16333 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵) | 
| 32 |  | pcdvdsb 16908 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) | 
| 33 | 20, 27, 24, 32 | syl3anc 1372 | . . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) | 
| 34 | 31, 33 | mpbird 257 | . 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) | 
| 35 | 17, 34 | pm2.61dane 3028 | 1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |