Step | Hyp | Ref
| Expression |
1 | | simp1 992 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝑃 ∈ ℙ) |
2 | | simp2l 1018 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℤ) |
3 | | simp3 994 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ) |
4 | | znq 9570 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
5 | 2, 3, 4 | syl2anc 409 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
6 | 2 | zcnd 9322 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐴 ∈ ℂ) |
7 | 3 | nncnd 8879 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℂ) |
8 | | simp2r 1019 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐴 ≠ 0) |
9 | | 0z 9210 |
. . . . . . 7
⊢ 0 ∈
ℤ |
10 | | zapne 9273 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) → (𝐴 # 0
↔ 𝐴 ≠
0)) |
11 | 2, 9, 10 | sylancl 411 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝐴 # 0 ↔ 𝐴 ≠ 0)) |
12 | 8, 11 | mpbird 166 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐴 # 0) |
13 | 3 | nnap0d 8911 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → 𝐵 # 0) |
14 | 6, 7, 12, 13 | divap0d 8710 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) # 0) |
15 | | zq 9572 |
. . . . . 6
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
16 | 9, 15 | ax-mp 5 |
. . . . 5
⊢ 0 ∈
ℚ |
17 | | qapne 9585 |
. . . . 5
⊢ (((𝐴 / 𝐵) ∈ ℚ ∧ 0 ∈ ℚ)
→ ((𝐴 / 𝐵) # 0 ↔ (𝐴 / 𝐵) ≠ 0)) |
18 | 5, 16, 17 | sylancl 411 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) # 0 ↔ (𝐴 / 𝐵) ≠ 0)) |
19 | 14, 18 | mpbid 146 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≠ 0) |
20 | | eqid 2170 |
. . . 4
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) |
21 | | eqid 2170 |
. . . 4
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) |
22 | 20, 21 | pcval 12237 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / 𝐵) ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
23 | 1, 5, 19, 22 | syl12anc 1231 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
24 | | eqid 2170 |
. . . . . . . 8
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) |
25 | 24 | pczpre 12238 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < )) |
26 | 25 | 3adant3 1012 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐴) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < )) |
27 | | nnz 9218 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
28 | | nnne0 8893 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
29 | 27, 28 | jca 304 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) |
30 | | eqid 2170 |
. . . . . . . . 9
⊢
sup({𝑛 ∈
ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ) |
31 | 30 | pczpre 12238 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt 𝐵) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
32 | 29, 31 | sylan2 284 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐵) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
33 | 32 | 3adant2 1011 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐵) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
34 | 26, 33 | oveq12d 5868 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ))) |
35 | | eqid 2170 |
. . . . 5
⊢ (𝐴 / 𝐵) = (𝐴 / 𝐵) |
36 | 34, 35 | jctil 310 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) = (𝐴 / 𝐵) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )))) |
37 | | oveq1 5857 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 / 𝑦) = (𝐴 / 𝑦)) |
38 | 37 | eqeq2d 2182 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐴 / 𝐵) = (𝑥 / 𝑦) ↔ (𝐴 / 𝐵) = (𝐴 / 𝑦))) |
39 | | breq2 3991 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ((𝑃↑𝑛) ∥ 𝑥 ↔ (𝑃↑𝑛) ∥ 𝐴)) |
40 | 39 | rabbidv 2719 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}) |
41 | 40 | supeq1d 6960 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < )) |
42 | 41 | oveq1d 5865 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) = (sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) |
43 | 42 | eqeq2d 2182 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
44 | 38, 43 | anbi12d 470 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ ((𝐴 / 𝐵) = (𝐴 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
45 | | oveq2 5858 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝐴 / 𝑦) = (𝐴 / 𝐵)) |
46 | 45 | eqeq2d 2182 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝐴 / 𝐵) = (𝐴 / 𝑦) ↔ (𝐴 / 𝐵) = (𝐴 / 𝐵))) |
47 | | breq2 3991 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → ((𝑃↑𝑛) ∥ 𝑦 ↔ (𝑃↑𝑛) ∥ 𝐵)) |
48 | 47 | rabbidv 2719 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦} = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}) |
49 | 48 | supeq1d 6960 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )) |
50 | 49 | oveq2d 5866 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) = (sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ))) |
51 | 50 | eqeq2d 2182 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )))) |
52 | 46, 51 | anbi12d 470 |
. . . . 5
⊢ (𝑦 = 𝐵 → (((𝐴 / 𝐵) = (𝐴 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ ((𝐴 / 𝐵) = (𝐴 / 𝐵) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < ))))) |
53 | 44, 52 | rspc2ev 2849 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ∧ ((𝐴 / 𝐵) = (𝐴 / 𝐵) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝐴}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝐵}, ℝ, < )))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
54 | 2, 3, 36, 53 | syl3anc 1233 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
55 | | pczcl 12239 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
56 | 55 | 3adant3 1012 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
57 | 56 | nn0zd 9319 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐴) ∈ ℤ) |
58 | 1, 3 | pccld 12241 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐵) ∈
ℕ0) |
59 | 58 | nn0zd 9319 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt 𝐵) ∈ ℤ) |
60 | 57, 59 | zsubcld 9326 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) ∈ ℤ) |
61 | 20, 21 | pceu 12236 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / 𝐵) ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
62 | 1, 5, 19, 61 | syl12anc 1231 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
63 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑧 = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) → (𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )) ↔ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) |
64 | 63 | anbi2d 461 |
. . . . . 6
⊢ (𝑧 = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) → (((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
65 | 64 | 2rexbidv 2495 |
. . . . 5
⊢ (𝑧 = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))))) |
66 | 65 | iota2 5186 |
. . . 4
⊢ ((((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) ∈ ℤ ∧ ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))) |
67 | 60, 62, 66 | syl2anc 409 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)) = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ))) ↔ (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))) |
68 | 54, 67 | mpbid 146 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ ((𝐴 / 𝐵) = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0
∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )))) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) |
69 | 23, 68 | eqtrd 2203 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) |