Proof of Theorem pcdvdstr
Step | Hyp | Ref
| Expression |
1 | | 0z 11993 |
. . . . . . 7
⊢ 0 ∈
ℤ |
2 | | zq 12355 |
. . . . . . 7
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ 0 ∈
ℚ |
4 | | pcxcl 16197 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 0 ∈
ℚ) → (𝑃 pCnt 0)
∈ ℝ*) |
5 | 3, 4 | mpan2 689 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ∈
ℝ*) |
6 | 5 | xrleidd 12546 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) |
7 | 6 | ad2antrr 724 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 0) ≤ (𝑃 pCnt 0)) |
8 | | simpr 487 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 = 0) |
9 | 8 | oveq2d 7172 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) = (𝑃 pCnt 0)) |
10 | | simplr3 1213 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐴 ∥ 𝐵) |
11 | 8, 10 | eqbrtrrd 5090 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 0 ∥ 𝐵) |
12 | | simplr2 1212 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 ∈ ℤ) |
13 | | 0dvds 15630 |
. . . . . 6
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (0 ∥ 𝐵 ↔ 𝐵 = 0)) |
15 | 11, 14 | mpbid 234 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → 𝐵 = 0) |
16 | 15 | oveq2d 7172 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐵) = (𝑃 pCnt 0)) |
17 | 7, 9, 16 | 3brtr4d 5098 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 = 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
18 | | simpll 765 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℙ) |
19 | | simplr1 1211 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) |
20 | | simpr 487 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
21 | | pczdvds 16199 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
22 | 18, 19, 20, 21 | syl12anc 834 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
23 | | simplr3 1213 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐴 ∥ 𝐵) |
24 | | prmnn 16018 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
25 | 24 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝑃 ∈ ℕ) |
26 | | pczcl 16185 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
27 | 18, 19, 20, 26 | syl12anc 834 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
28 | 25, 27 | nnexpcld 13607 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
29 | 28 | nnzd 12087 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) |
30 | | simplr2 1212 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → 𝐵 ∈ ℤ) |
31 | | dvdstr 15646 |
. . . . 5
⊢ (((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
32 | 29, 19, 30, 31 | syl3anc 1367 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (((𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ 𝐵) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
33 | 22, 23, 32 | mp2and 697 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵) |
34 | | pcdvdsb 16205 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ (𝑃 pCnt 𝐴) ∈ ℕ0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
35 | 18, 30, 27, 34 | syl3anc 1367 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → ((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐵)) |
36 | 33, 35 | mpbird 259 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) ∧ 𝐴 ≠ 0) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
37 | 17, 36 | pm2.61dane 3104 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |