Step | Hyp | Ref
| Expression |
1 | | elq 12425 |
. . 3
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
2 | | zcn 12060 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
3 | 2 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑥 ∈
ℂ) |
4 | | nncn 11717 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
5 | 4 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈
ℂ) |
6 | | nnne0 11743 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
7 | 6 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑦 ≠ 0) |
8 | 3, 5, 7 | divnegd 11500 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → -(𝑥 / 𝑦) = (-𝑥 / 𝑦)) |
9 | 8 | oveq2d 7180 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (-𝑥 / 𝑦))) |
10 | | neg0 11003 |
. . . . . . . . . 10
⊢ -0 =
0 |
11 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → 𝑥 = 0) |
12 | 11 | negeqd 10951 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → -𝑥 = -0) |
13 | 10, 12, 11 | 3eqtr4a 2799 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → -𝑥 = 𝑥) |
14 | 13 | oveq1d 7179 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → (-𝑥 / 𝑦) = (𝑥 / 𝑦)) |
15 | 14 | oveq2d 7180 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
16 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑃 ∈
ℙ) |
17 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℤ) |
18 | 17 | znegcld 12163 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → -𝑥 ∈
ℤ) |
19 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑥 ≠ 0) |
20 | 2 | negne0bd 11061 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → (𝑥 ≠ 0 ↔ -𝑥 ≠ 0)) |
21 | 17, 20 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑥 ≠ 0 ↔ -𝑥 ≠ 0)) |
22 | 19, 21 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → -𝑥 ≠ 0) |
23 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑦 ∈
ℕ) |
24 | | pcdiv 16282 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (-𝑥 ∈ ℤ ∧ -𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (-𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
25 | 16, 18, 22, 23, 24 | syl121anc 1376 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
26 | | pcdiv 16282 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
27 | 16, 17, 19, 23, 26 | syl121anc 1376 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
28 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
sup({𝑦 ∈
ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < ) |
29 | 28 | pczpre 16277 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (-𝑥 ∈ ℤ ∧ -𝑥 ≠ 0)) → (𝑃 pCnt -𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
30 | 16, 18, 22, 29 | syl12anc 836 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt -𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
31 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
sup({𝑦 ∈
ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) |
32 | 31 | pczpre 16277 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < )) |
33 | | prmz 16109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
34 | | zexpcl 13529 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (𝑃↑𝑦) ∈
ℤ) |
35 | 33, 34 | sylan 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0)
→ (𝑃↑𝑦) ∈
ℤ) |
36 | | simpl 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℤ) |
37 | | dvdsnegb 15712 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃↑𝑦) ∈ ℤ ∧ 𝑥 ∈ ℤ) → ((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
38 | 35, 36, 37 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0)
∧ (𝑥 ∈ ℤ
∧ 𝑥 ≠ 0)) →
((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
39 | 38 | an32s 652 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
40 | 39 | rabbidva 3378 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑦 ∈ ℕ0
∣ (𝑃↑𝑦) ∥ 𝑥} = {𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}) |
41 | 40 | supeq1d 8976 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → sup({𝑦 ∈ ℕ0
∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
42 | 32, 41 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
43 | 16, 17, 19, 42 | syl12anc 836 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
44 | 30, 43 | eqtr4d 2776 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt -𝑥) = (𝑃 pCnt 𝑥)) |
45 | 44 | oveq1d 7179 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
46 | 27, 45 | eqtr4d 2776 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
47 | 25, 46 | eqtr4d 2776 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
48 | 15, 47 | pm2.61dane 3021 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
49 | 9, 48 | eqtrd 2773 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
50 | | negeq 10949 |
. . . . . . 7
⊢ (𝐴 = (𝑥 / 𝑦) → -𝐴 = -(𝑥 / 𝑦)) |
51 | 50 | oveq2d 7180 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt -(𝑥 / 𝑦))) |
52 | | oveq2 7172 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝑥 / 𝑦))) |
53 | 51, 52 | eqeq12d 2754 |
. . . . 5
⊢ (𝐴 = (𝑥 / 𝑦) → ((𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴) ↔ (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦)))) |
54 | 49, 53 | syl5ibrcom 250 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
55 | 54 | rexlimdvva 3203 |
. . 3
⊢ (𝑃 ∈ ℙ →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
56 | 1, 55 | syl5bi 245 |
. 2
⊢ (𝑃 ∈ ℙ → (𝐴 ∈ ℚ → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
57 | 56 | imp 410 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) |