Step | Hyp | Ref
| Expression |
1 | | simprl 526 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → 𝑁 ∈
ℚ) |
2 | | elq 9581 |
. . 3
⊢ (𝑁 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝑁 = (𝑥 / 𝑦)) |
3 | 1, 2 | sylib 121 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦)) |
4 | | nncn 8886 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
5 | | nnap0 8907 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 # 0) |
6 | 4, 5 | div0apd 8704 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (0 /
𝑦) = 0) |
7 | 6 | ad2antll 488 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (0 /
𝑦) = 0) |
8 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 / 𝑦) = (0 / 𝑦)) |
9 | 8 | eqeq1d 2179 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → ((𝑥 / 𝑦) = 0 ↔ (0 / 𝑦) = 0)) |
10 | 7, 9 | syl5ibrcom 156 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 = 0 → (𝑥 / 𝑦) = 0)) |
11 | 10 | necon3d 2384 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → 𝑥 ≠ 0)) |
12 | | an32 557 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ↔ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈
ℕ)) |
13 | | pcdiv 12256 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) = ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦))) |
14 | | pczcl 12252 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈
ℕ0) |
15 | 14 | nn0zd 9332 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑃 pCnt 𝑥) ∈ ℤ) |
16 | 15 | 3adant3 1012 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑥) ∈ ℤ) |
17 | | nnz 9231 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
18 | | nnne0 8906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
19 | 17, 18 | jca 304 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) |
20 | | pczcl 12252 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈
ℕ0) |
21 | 20 | nn0zd 9332 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ ℙ ∧ (𝑦 ∈ ℤ ∧ 𝑦 ≠ 0)) → (𝑃 pCnt 𝑦) ∈ ℤ) |
22 | 19, 21 | sylan2 284 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) |
23 | 22 | 3adant2 1011 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt 𝑦) ∈ ℤ) |
24 | 16, 23 | zsubcld 9339 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → ((𝑃 pCnt 𝑥) − (𝑃 pCnt 𝑦)) ∈ ℤ) |
25 | 13, 24 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
26 | 25 | 3expb 1199 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
27 | 12, 26 | sylan2b 285 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0)) → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ) |
28 | 27 | expr 373 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑥 ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
29 | 11, 28 | syld 45 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
30 | | neeq1 2353 |
. . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
31 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) = (𝑃 pCnt (𝑥 / 𝑦))) |
32 | 31 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑃 pCnt 𝑁) ∈ ℤ ↔ (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ)) |
33 | 30, 32 | imbi12d 233 |
. . . . . . 7
⊢ (𝑁 = (𝑥 / 𝑦) → ((𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ) ↔ ((𝑥 / 𝑦) ≠ 0 → (𝑃 pCnt (𝑥 / 𝑦)) ∈ ℤ))) |
34 | 29, 33 | syl5ibrcom 156 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 = (𝑥 / 𝑦) → (𝑁 ≠ 0 → (𝑃 pCnt 𝑁) ∈ ℤ))) |
35 | 34 | com23 78 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) → (𝑁 ≠ 0 → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
36 | 35 | impancom 258 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ≠ 0) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
37 | 36 | adantrl 475 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ))) |
38 | 37 | rexlimdvv 2594 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝑁 = (𝑥 / 𝑦) → (𝑃 pCnt 𝑁) ∈ ℤ)) |
39 | 3, 38 | mpd 13 |
1
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ) |