Proof of Theorem pcdvdstr
Step | Hyp | Ref
| Expression |
1 | | 0z 11801 |
. . . . . . 7
⊢ 0 ∈
ℤ |
2 | | zq 12165 |
. . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ 0 ∈
ℚ |
4 | | pcxcl 16047 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 0 ∈
ℚ) → (𝑃 pCnt 0)
∈ ℝ*) |
5 | 3, 4 | mpan2 678 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ∈
ℝ*) |
6 | 5 | xrleidd 12359 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) |
7 | 6 | ad2antrr 713 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) |
8 | | simpr 477 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 = 0) |
9 | 8 | oveq2d 6990 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) = (𝑃 pCnt 0)) |
10 | | simplr3 1197 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 ∥ 𝐵) |
11 | 8, 10 | eqbrtrrd 4951 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 0 ∥ 𝐵) |
12 | | simplr2 1196 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 ∈ ℤ) |
13 | | 0dvds 15484 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (0 ∥ 𝐵 ↔ 𝐵 = 0)) |
15 | 11, 14 | mpbid 224 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 = 0) |
16 | 15 | oveq2d 6990 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐵) = (𝑃 pCnt 0)) |
17 | 7, 9, 16 | 3brtr4d 4959 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
18 | | simpll 754 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℙ) |
19 | | simplr1 1195 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) |
20 | | simpr 477 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
21 | | pczdvds 16049 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
22 | 18, 19, 20, 21 | syl12anc 824 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
23 | | simplr3 1197 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∥ 𝐵) |
24 | | prmnn 15868 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
25 | 24 | ad2antrr 713 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℕ) |
26 | | pczcl 16035 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
27 | 18, 19, 20, 26 | syl12anc 824 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
28 | 25, 27 | nnexpcld 13418 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
29 | 28 | nnzd 11896 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) |
30 | | simplr2 1196 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℤ) |
31 | | dvdstr 15500 |
. . . . 5
⊢ (((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
32 | 29, 19, 30, 31 | syl3anc 1351 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
33 | 22, 23, 32 | mp2and 686 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵) |
34 | | pcdvdsb 16055 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
35 | 18, 30, 27, 34 | syl3anc 1351 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
36 | 33, 35 | mpbird 249 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
37 | 17, 36 | pm2.61dane 3052 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |