| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprl 770 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → 𝑁 ∈
ℚ) | 
| 2 |  | elq 12993 | . . 3
⊢ (𝑁 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝑁 = (𝑥 / 𝑦)) | 
| 3 | 1, 2 | sylib 218 | . 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦)) | 
| 4 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) | 
| 5 |  | nnne0 12301 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) | 
| 6 | 4, 5 | div0d 12043 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (0 /
𝑦) = 0) | 
| 7 | 6 | ad2antll 729 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (0 /
𝑦) = 0) | 
| 8 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦)) | 
| 9 | 8 | eqeq1d 2738 | . . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0)) | 
| 10 | 7, 9 | syl5ibrcom 247 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 = 0 → (𝑥 / 𝑦) = 0)) | 
| 11 | 10 | necon3d 2960 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0)) | 
| 12 |  | an32 646 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ↔ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈
ℕ)) | 
| 13 |  | pcdiv 16891 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) | 
| 14 |  | pczcl 16887 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈
ℕ0) | 
| 15 | 14 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ) | 
| 16 | 15 | 3adant3 1132 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑥) ∈ ℤ) | 
| 17 |  | nnz 12636 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) | 
| 18 | 17, 5 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) | 
| 19 |  | pczcl 16887 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈
ℕ0) | 
| 20 | 19 | nn0zd 12641 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ) | 
| 21 | 18, 20 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) | 
| 22 | 21 | 3adant2 1131 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) | 
| 23 | 16, 22 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) ∈ ℤ) | 
| 24 | 13, 23 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) | 
| 25 | 24 | 3expb 1120 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) | 
| 26 | 12, 25 | sylan2b 594 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) | 
| 27 | 26 | expr 456 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) | 
| 28 | 11, 27 | syld 47 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) | 
| 29 |  | neeq1 3002 | . . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) | 
| 30 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) = (𝑃 pCnt (𝑥 / 𝑦))) | 
| 31 | 30 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑃 pCnt 𝑁) ∈ ℤ ↔ (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) | 
| 32 | 29, 31 | imbi12d 344 | . . . . . . 7
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ) ↔ ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ))) | 
| 33 | 28, 32 | syl5ibrcom 247 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ))) | 
| 34 | 33 | com23 86 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 ≠ 0 → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) | 
| 35 | 34 | impancom 451 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) | 
| 36 | 35 | adantrl 716 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) | 
| 37 | 36 | rexlimdvv 3211 | . 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ)) | 
| 38 | 3, 37 | mpd 15 | 1
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ) |