| Step | Hyp | Ref
| Expression |
| 1 | | elq 12992 |
. . 3
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
| 2 | | zcn 12618 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 3 | 2 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑥 ∈
ℂ) |
| 4 | | nncn 12274 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 5 | 4 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑦 ∈
ℂ) |
| 6 | | nnne0 12300 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
| 7 | 6 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → 𝑦 ≠ 0) |
| 8 | 3, 5, 7 | divnegd 12056 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → -(𝑥 / 𝑦) = (-𝑥 / 𝑦)) |
| 9 | 8 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (-𝑥 / 𝑦))) |
| 10 | | neg0 11555 |
. . . . . . . . . 10
⊢ -0 =
0 |
| 11 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → 𝑥 = 0) |
| 12 | 11 | negeqd 11502 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → -𝑥 = -0) |
| 13 | 10, 12, 11 | 3eqtr4a 2803 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → -𝑥 = 𝑥) |
| 14 | 13 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → (-𝑥 / 𝑦) = (𝑥 / 𝑦)) |
| 15 | 14 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 = 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
| 16 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑃 ∈
ℙ) |
| 17 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℤ) |
| 18 | 17 | znegcld 12724 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → -𝑥 ∈
ℤ) |
| 19 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑥 ≠ 0) |
| 20 | 2 | negne0bd 11613 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → (𝑥 ≠ 0 ↔ -𝑥 ≠ 0)) |
| 21 | 17, 20 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑥 ≠ 0 ↔ -𝑥 ≠ 0)) |
| 22 | 19, 21 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → -𝑥 ≠ 0) |
| 23 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → 𝑦 ∈
ℕ) |
| 24 | | pcdiv 16890 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (-𝑥 ∈ ℤ ∧ -𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (-𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
| 25 | 16, 18, 22, 23, 24 | syl121anc 1377 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
| 26 | | pcdiv 16890 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
| 27 | 16, 17, 19, 23, 26 | syl121anc 1377 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
sup({𝑦 ∈
ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < ) |
| 29 | 28 | pczpre 16885 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (-𝑥 ∈ ℤ ∧ -𝑥 ≠ 0)) → (𝑃 pCnt -𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
| 30 | 16, 18, 22, 29 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt -𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
sup({𝑦 ∈
ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) |
| 32 | 31 | pczpre 16885 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < )) |
| 33 | | prmz 16712 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 34 | | zexpcl 14117 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (𝑃↑𝑦) ∈
ℤ) |
| 35 | 33, 34 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0)
→ (𝑃↑𝑦) ∈
ℤ) |
| 36 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → 𝑥 ∈
ℤ) |
| 37 | | dvdsnegb 16311 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃↑𝑦) ∈ ℤ ∧ 𝑥 ∈ ℤ) → ((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
| 38 | 35, 36, 37 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ0)
∧ (𝑥 ∈ ℤ
∧ 𝑥 ≠ 0)) →
((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
| 39 | 38 | an32s 652 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ 𝑦 ∈ ℕ0)
→ ((𝑃↑𝑦) ∥ 𝑥 ↔ (𝑃↑𝑦) ∥ -𝑥)) |
| 40 | 39 | rabbidva 3443 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑦 ∈ ℕ0
∣ (𝑃↑𝑦) ∥ 𝑥} = {𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}) |
| 41 | 40 | supeq1d 9486 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → sup({𝑦 ∈ ℕ0
∣ (𝑃↑𝑦) ∥ 𝑥}, ℝ, < ) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
| 42 | 32, 41 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
| 43 | 16, 17, 19, 42 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt 𝑥) = sup({𝑦 ∈ ℕ0 ∣ (𝑃↑𝑦) ∥ -𝑥}, ℝ, < )) |
| 44 | 30, 43 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt -𝑥) = (𝑃 pCnt 𝑥)) |
| 45 | 44 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
| 46 | 27, 45 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt -𝑥) − (𝑃 pCnt 𝑦))) |
| 47 | 25, 46 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) ∧ 𝑥 ≠ 0) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
| 48 | 15, 47 | pm2.61dane 3029 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt (-𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
| 49 | 9, 48 | eqtrd 2777 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦))) |
| 50 | | negeq 11500 |
. . . . . . 7
⊢ (𝐴 = (𝑥 / 𝑦) → -𝐴 = -(𝑥 / 𝑦)) |
| 51 | 50 | oveq2d 7447 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt -(𝑥 / 𝑦))) |
| 52 | | oveq2 7439 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝑥 / 𝑦))) |
| 53 | 51, 52 | eqeq12d 2753 |
. . . . 5
⊢ (𝐴 = (𝑥 / 𝑦) → ((𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴) ↔ (𝑃 pCnt -(𝑥 / 𝑦)) = (𝑃 pCnt (𝑥 / 𝑦)))) |
| 54 | 49, 53 | syl5ibrcom 247 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
| 55 | 54 | rexlimdvva 3213 |
. . 3
⊢ (𝑃 ∈ ℙ →
(∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
| 56 | 1, 55 | biimtrid 242 |
. 2
⊢ (𝑃 ∈ ℙ → (𝐴 ∈ ℚ → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))) |
| 57 | 56 | imp 406 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) |