Step | Hyp | Ref
| Expression |
1 | | zq 9572 |
. . 3
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℚ) |
2 | | eqid 2170 |
. . . 4
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) |
3 | | eqid 2170 |
. . . 4
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) |
4 | 2, 3 | pcval 12237 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
5 | 1, 4 | sylanr1 402 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
6 | | simprl 526 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 ∈
ℤ) |
7 | 6 | zcnd 9322 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 ∈
ℂ) |
8 | 7 | div1d 8684 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑁 / 1) = 𝑁) |
9 | 8 | eqcomd 2176 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑁 = (𝑁 / 1)) |
10 | | prmuz2 12072 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
11 | | eqid 2170 |
. . . . . . . 8
⊢ 1 =
1 |
12 | | eqid 2170 |
. . . . . . . . 9
⊢ {𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 1} = {𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 1} |
13 | | eqid 2170 |
. . . . . . . . 9
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < ) = sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
) |
14 | 12, 13 | pcpre1 12233 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 1 = 1) → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < ) =
0) |
15 | 10, 11, 14 | sylancl 411 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ →
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < ) =
0) |
16 | 15 | adantr 274 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 1}, ℝ, < ) =
0) |
17 | 16 | oveq2d 5866 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < )) = (𝑆 − 0)) |
18 | | eqid 2170 |
. . . . . . . . . 10
⊢ {𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑁} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} |
19 | | pczpre.1 |
. . . . . . . . . 10
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) |
20 | 18, 19 | pcprecl 12230 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 ∈ ℕ0 ∧ (𝑃↑𝑆) ∥ 𝑁)) |
21 | 10, 20 | sylan 281 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 ∈ ℕ0
∧ (𝑃↑𝑆) ∥ 𝑁)) |
22 | 21 | simpld 111 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑆 ∈
ℕ0) |
23 | 22 | nn0cnd 9177 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑆 ∈
ℂ) |
24 | 23 | subid1d 8206 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 − 0) = 𝑆) |
25 | 17, 24 | eqtr2d 2204 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
))) |
26 | | 1nn 8876 |
. . . . 5
⊢ 1 ∈
ℕ |
27 | | oveq1 5857 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑥 / 𝑦) = (𝑁 / 𝑦)) |
28 | 27 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑁 = (𝑥 / 𝑦) ↔ 𝑁 = (𝑁 / 𝑦))) |
29 | | breq2 3991 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑁 → ((𝑃↑𝑛) ∥ 𝑥 ↔ (𝑃↑𝑛) ∥ 𝑁)) |
30 | 29 | rabbidv 2719 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑁 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}) |
31 | 30 | supeq1d 6960 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑁 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < )) |
32 | 31, 19 | eqtr4di 2221 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = 𝑆) |
33 | 32 | oveq1d 5865 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) |
34 | 33 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
35 | 28, 34 | anbi12d 470 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (𝑁 = (𝑁 / 𝑦) ∧ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
36 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝑁 / 𝑦) = (𝑁 / 1)) |
37 | 36 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑦 = 1 → (𝑁 = (𝑁 / 𝑦) ↔ 𝑁 = (𝑁 / 1))) |
38 | | breq2 3991 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → ((𝑃↑𝑛) ∥ 𝑦 ↔ (𝑃↑𝑛) ∥ 1)) |
39 | 38 | rabbidv 2719 |
. . . . . . . . . 10
⊢ (𝑦 = 1 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}) |
40 | 39 | supeq1d 6960 |
. . . . . . . . 9
⊢ (𝑦 = 1 → sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
)) |
41 | 40 | oveq2d 5866 |
. . . . . . . 8
⊢ (𝑦 = 1 → (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
))) |
42 | 41 | eqeq2d 2182 |
. . . . . . 7
⊢ (𝑦 = 1 → (𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
)))) |
43 | 37, 42 | anbi12d 470 |
. . . . . 6
⊢ (𝑦 = 1 → ((𝑁 = (𝑁 / 𝑦) ∧ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (𝑁 = (𝑁 / 1) ∧ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, <
))))) |
44 | 35, 43 | rspc2ev 2849 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℕ ∧ (𝑁 = (𝑁 / 1) ∧ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < )))) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
(𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
45 | 26, 44 | mp3an2 1320 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 = (𝑁 / 1) ∧ 𝑆 = (𝑆 − sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 1}, ℝ, < )))) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
(𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
46 | 6, 9, 25, 45 | syl12anc 1231 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
47 | | reex 7895 |
. . . . . 6
⊢ ℝ
∈ V |
48 | | supex2g 7006 |
. . . . . 6
⊢ (ℝ
∈ V → sup({𝑛
∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) ∈
V) |
49 | 47, 48 | ax-mp 5 |
. . . . 5
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) ∈ V |
50 | 19, 49 | eqeltri 2243 |
. . . 4
⊢ 𝑆 ∈ V |
51 | 2, 3 | pceu 12236 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
52 | 1, 51 | sylanr1 402 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
53 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑧 = 𝑆 → (𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
54 | 53 | anbi2d 461 |
. . . . . 6
⊢ (𝑧 = 𝑆 → ((𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
55 | 54 | 2rexbidv 2495 |
. . . . 5
⊢ (𝑧 = 𝑆 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
56 | 55 | iota2 5186 |
. . . 4
⊢ ((𝑆 ∈ V ∧ ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = 𝑆)) |
57 | 50, 52, 56 | sylancr 412 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑆 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = 𝑆)) |
58 | 46, 57 | mpbid 146 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = 𝑆) |
59 | 5, 58 | eqtrd 2203 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = 𝑆) |