Step | Hyp | Ref
| Expression |
1 | | dvdsppwf1o.f |
. 2
⊢ 𝐹 = (𝑛 ∈ (0...𝐴) ↦ (𝑃↑𝑛)) |
2 | | prmnn 15226 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
3 | 2 | adantr 480 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ 𝑃 ∈
ℕ) |
4 | | elfznn0 12302 |
. . . 4
⊢ (𝑛 ∈ (0...𝐴) → 𝑛 ∈ ℕ0) |
5 | | nnexpcl 12735 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝑛 ∈ ℕ0)
→ (𝑃↑𝑛) ∈
ℕ) |
6 | 3, 4, 5 | syl2an 493 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → (𝑃↑𝑛) ∈ ℕ) |
7 | | prmz 15227 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
8 | 7 | ad2antrr 758 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → 𝑃 ∈ ℤ) |
9 | 4 | adantl 481 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → 𝑛 ∈ ℕ0) |
10 | | elfzuz3 12210 |
. . . . 5
⊢ (𝑛 ∈ (0...𝐴) → 𝐴 ∈ (ℤ≥‘𝑛)) |
11 | 10 | adantl 481 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → 𝐴 ∈ (ℤ≥‘𝑛)) |
12 | | dvdsexp 14887 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧ 𝑛 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘𝑛)) → (𝑃↑𝑛) ∥ (𝑃↑𝐴)) |
13 | 8, 9, 11, 12 | syl3anc 1318 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → (𝑃↑𝑛) ∥ (𝑃↑𝐴)) |
14 | | breq1 4586 |
. . . 4
⊢ (𝑥 = (𝑃↑𝑛) → (𝑥 ∥ (𝑃↑𝐴) ↔ (𝑃↑𝑛) ∥ (𝑃↑𝐴))) |
15 | 14 | elrab 3331 |
. . 3
⊢ ((𝑃↑𝑛) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)} ↔ ((𝑃↑𝑛) ∈ ℕ ∧ (𝑃↑𝑛) ∥ (𝑃↑𝐴))) |
16 | 6, 13, 15 | sylanbrc 695 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → (𝑃↑𝑛) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) |
17 | | simpl 472 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ 𝑃 ∈
ℙ) |
18 | | elrabi 3328 |
. . . 4
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)} → 𝑚 ∈ ℕ) |
19 | | pccl 15392 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈ ℕ) → (𝑃 pCnt 𝑚) ∈
ℕ0) |
20 | 17, 18, 19 | syl2an 493 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃 pCnt 𝑚) ∈
ℕ0) |
21 | 17 | adantr 480 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑃 ∈ ℙ) |
22 | 18 | adantl 481 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑚 ∈ ℕ) |
23 | 22 | nnzd 11357 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑚 ∈ ℤ) |
24 | 7 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑃 ∈ ℤ) |
25 | | simplr 788 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝐴 ∈
ℕ0) |
26 | | zexpcl 12737 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℕ0)
→ (𝑃↑𝐴) ∈
ℤ) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃↑𝐴) ∈ ℤ) |
28 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → (𝑥 ∥ (𝑃↑𝐴) ↔ 𝑚 ∥ (𝑃↑𝐴))) |
29 | 28 | elrab 3331 |
. . . . . . 7
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)} ↔ (𝑚 ∈ ℕ ∧ 𝑚 ∥ (𝑃↑𝐴))) |
30 | 29 | simprbi 479 |
. . . . . 6
⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)} → 𝑚 ∥ (𝑃↑𝐴)) |
31 | 30 | adantl 481 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑚 ∥ (𝑃↑𝐴)) |
32 | | pcdvdstr 15418 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑚 ∈ ℤ ∧ (𝑃↑𝐴) ∈ ℤ ∧ 𝑚 ∥ (𝑃↑𝐴))) → (𝑃 pCnt 𝑚) ≤ (𝑃 pCnt (𝑃↑𝐴))) |
33 | 21, 23, 27, 31, 32 | syl13anc 1320 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃 pCnt 𝑚) ≤ (𝑃 pCnt (𝑃↑𝐴))) |
34 | | pcidlem 15414 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
35 | 34 | adantr 480 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
36 | 33, 35 | breqtrd 4609 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃 pCnt 𝑚) ≤ 𝐴) |
37 | | fznn0 12301 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ ((𝑃 pCnt 𝑚) ∈ (0...𝐴) ↔ ((𝑃 pCnt 𝑚) ∈ ℕ0 ∧ (𝑃 pCnt 𝑚) ≤ 𝐴))) |
38 | 25, 37 | syl 17 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → ((𝑃 pCnt 𝑚) ∈ (0...𝐴) ↔ ((𝑃 pCnt 𝑚) ∈ ℕ0 ∧ (𝑃 pCnt 𝑚) ≤ 𝐴))) |
39 | 20, 36, 38 | mpbir2and 959 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (𝑃 pCnt 𝑚) ∈ (0...𝐴)) |
40 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 𝐴 → (𝑃↑𝑛) = (𝑃↑𝐴)) |
41 | 40 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑛 = 𝐴 → (𝑚 ∥ (𝑃↑𝑛) ↔ 𝑚 ∥ (𝑃↑𝐴))) |
42 | 41 | rspcev 3282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝑚 ∥ (𝑃↑𝐴)) → ∃𝑛 ∈ ℕ0 𝑚 ∥ (𝑃↑𝑛)) |
43 | 25, 31, 42 | syl2anc 691 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → ∃𝑛 ∈ ℕ0 𝑚 ∥ (𝑃↑𝑛)) |
44 | | pcprmpw2 15424 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑚 ∈ ℕ) →
(∃𝑛 ∈
ℕ0 𝑚
∥ (𝑃↑𝑛) ↔ 𝑚 = (𝑃↑(𝑃 pCnt 𝑚)))) |
45 | 17, 18, 44 | syl2an 493 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → (∃𝑛 ∈ ℕ0 𝑚 ∥ (𝑃↑𝑛) ↔ 𝑚 = (𝑃↑(𝑃 pCnt 𝑚)))) |
46 | 43, 45 | mpbid 221 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) → 𝑚 = (𝑃↑(𝑃 pCnt 𝑚))) |
47 | 46 | adantrl 748 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ (𝑛 ∈ (0...𝐴) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})) → 𝑚 = (𝑃↑(𝑃 pCnt 𝑚))) |
48 | | oveq2 6557 |
. . . . 5
⊢ (𝑛 = (𝑃 pCnt 𝑚) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt 𝑚))) |
49 | 48 | eqeq2d 2620 |
. . . 4
⊢ (𝑛 = (𝑃 pCnt 𝑚) → (𝑚 = (𝑃↑𝑛) ↔ 𝑚 = (𝑃↑(𝑃 pCnt 𝑚)))) |
50 | 47, 49 | syl5ibrcom 236 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ (𝑛 ∈ (0...𝐴) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})) → (𝑛 = (𝑃 pCnt 𝑚) → 𝑚 = (𝑃↑𝑛))) |
51 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑛 ∈ (0...𝐴) → 𝑛 ∈ ℤ) |
52 | | pcid 15415 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑛 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝑛)) = 𝑛) |
53 | 17, 51, 52 | syl2an 493 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → (𝑃 pCnt (𝑃↑𝑛)) = 𝑛) |
54 | 53 | eqcomd 2616 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ 𝑛 ∈ (0...𝐴)) → 𝑛 = (𝑃 pCnt (𝑃↑𝑛))) |
55 | 54 | adantrr 749 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ (𝑛 ∈ (0...𝐴) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})) → 𝑛 = (𝑃 pCnt (𝑃↑𝑛))) |
56 | | oveq2 6557 |
. . . . 5
⊢ (𝑚 = (𝑃↑𝑛) → (𝑃 pCnt 𝑚) = (𝑃 pCnt (𝑃↑𝑛))) |
57 | 56 | eqeq2d 2620 |
. . . 4
⊢ (𝑚 = (𝑃↑𝑛) → (𝑛 = (𝑃 pCnt 𝑚) ↔ 𝑛 = (𝑃 pCnt (𝑃↑𝑛)))) |
58 | 55, 57 | syl5ibrcom 236 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ (𝑛 ∈ (0...𝐴) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})) → (𝑚 = (𝑃↑𝑛) → 𝑛 = (𝑃 pCnt 𝑚))) |
59 | 50, 58 | impbid 201 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
∧ (𝑛 ∈ (0...𝐴) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)})) → (𝑛 = (𝑃 pCnt 𝑚) ↔ 𝑚 = (𝑃↑𝑛))) |
60 | 1, 16, 39, 59 | f1o2d 6785 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0)
→ 𝐹:(0...𝐴)–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑃↑𝐴)}) |