Step | Hyp | Ref
| Expression |
1 | | simprl 761 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → 𝑁 ∈
ℚ) |
2 | | elq 12097 |
. . 3
⊢ (𝑁 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝑁 = (𝑥 / 𝑦)) |
3 | 1, 2 | sylib 210 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦)) |
4 | | nncn 11383 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
5 | | nnne0 11410 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
6 | 4, 5 | div0d 11150 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (0 /
𝑦) = 0) |
7 | 6 | ad2antll 719 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (0 /
𝑦) = 0) |
8 | | oveq1 6929 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦)) |
9 | 8 | eqeq1d 2780 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0)) |
10 | 7, 9 | syl5ibrcom 239 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 = 0 → (𝑥 / 𝑦) = 0)) |
11 | 10 | necon3d 2990 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0)) |
12 | | an32 636 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ↔ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈
ℕ)) |
13 | | pcdiv 15961 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
14 | | pczcl 15957 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈
ℕ0) |
15 | 14 | nn0zd 11832 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ) |
16 | 15 | 3adant3 1123 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑥) ∈ ℤ) |
17 | | nnz 11751 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
18 | 17, 5 | jca 507 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) |
19 | | pczcl 15957 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈
ℕ0) |
20 | 19 | nn0zd 11832 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ) |
21 | 18, 20 | sylan2 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) |
22 | 21 | 3adant2 1122 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) |
23 | 16, 22 | zsubcld 11839 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) ∈ ℤ) |
24 | 13, 23 | eqeltrd 2859 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
25 | 24 | 3expb 1110 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
26 | 12, 25 | sylan2b 587 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
27 | 26 | expr 450 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
28 | 11, 27 | syld 47 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
29 | | neeq1 3031 |
. . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
30 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) = (𝑃 pCnt (𝑥 / 𝑦))) |
31 | 30 | eleq1d 2844 |
. . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑃 pCnt 𝑁) ∈ ℤ ↔ (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
32 | 29, 31 | imbi12d 336 |
. . . . . . 7
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ) ↔ ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ))) |
33 | 28, 32 | syl5ibrcom 239 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ))) |
34 | 33 | com23 86 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 ≠ 0 → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
35 | 34 | impancom 445 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
36 | 35 | adantrl 706 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
37 | 36 | rexlimdvv 3220 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ)) |
38 | 3, 37 | mpd 15 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ) |