Step | Hyp | Ref
| Expression |
1 | | pcge0 12266 |
. . . 4
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 0 ≤
(𝑝 pCnt 𝐴)) |
2 | 1 | ancoms 266 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℙ) → 0 ≤
(𝑝 pCnt 𝐴)) |
3 | 2 | ralrimiva 2543 |
. 2
⊢ (𝐴 ∈ ℤ →
∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt 𝐴)) |
4 | | elq 9581 |
. . 3
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
5 | | nnz 9231 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
6 | | dvds0 11768 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → 𝑦 ∥ 0) |
7 | 5, 6 | syl 14 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∥ 0) |
8 | 7 | ad2antlr 486 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 = 0) → 𝑦 ∥ 0) |
9 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 = 0) → 𝑥 = 0) |
10 | 8, 9 | breqtrrd 4017 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 = 0) → 𝑦 ∥ 𝑥) |
11 | 10 | a1d 22 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 = 0) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)) → 𝑦 ∥ 𝑥)) |
12 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) |
13 | | simplll 528 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈
ℤ) |
14 | | simplr 525 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑥 ≠ 0) |
15 | | simpllr 529 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑦 ∈
ℕ) |
16 | | pcdiv 12256 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ 𝑦 ∈ ℕ) → (𝑝 pCnt (𝑥 / 𝑦)) = ((𝑝 pCnt 𝑥) − (𝑝 pCnt 𝑦))) |
17 | 12, 13, 14, 15, 16 | syl121anc 1238 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑥 / 𝑦)) = ((𝑝 pCnt 𝑥) − (𝑝 pCnt 𝑦))) |
18 | 17 | breq2d 4001 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (0 ≤
(𝑝 pCnt (𝑥 / 𝑦)) ↔ 0 ≤ ((𝑝 pCnt 𝑥) − (𝑝 pCnt 𝑦)))) |
19 | | pczcl 12252 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑝 pCnt 𝑥) ∈
ℕ0) |
20 | 12, 13, 14, 19 | syl12anc 1231 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑥) ∈
ℕ0) |
21 | 20 | nn0red 9189 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑥) ∈ ℝ) |
22 | 12, 15 | pccld 12254 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑦) ∈
ℕ0) |
23 | 22 | nn0red 9189 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝑦) ∈ ℝ) |
24 | 21, 23 | subge0d 8454 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (0 ≤
((𝑝 pCnt 𝑥) − (𝑝 pCnt 𝑦)) ↔ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
25 | 18, 24 | bitrd 187 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) ∧ 𝑝 ∈ ℙ) → (0 ≤
(𝑝 pCnt (𝑥 / 𝑦)) ↔ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
26 | 25 | ralbidva 2466 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
27 | | id 19 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℤ) |
28 | | pc2dvds 12283 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑦 ∥ 𝑥 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
29 | 5, 27, 28 | syl2anr 288 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑦 ∥ 𝑥 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
30 | 29 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑦 ∥ 𝑥 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) ≤ (𝑝 pCnt 𝑥))) |
31 | 26, 30 | bitr4d 190 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)) ↔ 𝑦 ∥ 𝑥)) |
32 | 31 | biimpd 143 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)) → 𝑦 ∥ 𝑥)) |
33 | | 0zd 9224 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → 0 ∈
ℤ) |
34 | | zdceq 9287 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 0 ∈
ℤ) → DECID 𝑥 = 0) |
35 | 33, 34 | syldan 280 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) →
DECID 𝑥 =
0) |
36 | | dcne 2351 |
. . . . . . . 8
⊢
(DECID 𝑥 = 0 ↔ (𝑥 = 0 ∨ 𝑥 ≠ 0)) |
37 | 35, 36 | sylib 121 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 = 0 ∨ 𝑥 ≠ 0)) |
38 | 11, 32, 37 | mpjaodan 793 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) →
(∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt (𝑥 / 𝑦)) → 𝑦 ∥ 𝑥)) |
39 | | nnne0 8906 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
40 | | simpl 108 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → 𝑥 ∈
ℤ) |
41 | | dvdsval2 11752 |
. . . . . . 7
⊢ ((𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ∧ 𝑥 ∈ ℤ) → (𝑦 ∥ 𝑥 ↔ (𝑥 / 𝑦) ∈ ℤ)) |
42 | 5, 39, 40, 41 | syl2an23an 1294 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑦 ∥ 𝑥 ↔ (𝑥 / 𝑦) ∈ ℤ)) |
43 | 38, 42 | sylibd 148 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) →
(∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt (𝑥 / 𝑦)) → (𝑥 / 𝑦) ∈ ℤ)) |
44 | | oveq2 5861 |
. . . . . . . 8
⊢ (𝐴 = (𝑥 / 𝑦) → (𝑝 pCnt 𝐴) = (𝑝 pCnt (𝑥 / 𝑦))) |
45 | 44 | breq2d 4001 |
. . . . . . 7
⊢ (𝐴 = (𝑥 / 𝑦) → (0 ≤ (𝑝 pCnt 𝐴) ↔ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)))) |
46 | 45 | ralbidv 2470 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴) ↔ ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)))) |
47 | | eleq1 2233 |
. . . . . 6
⊢ (𝐴 = (𝑥 / 𝑦) → (𝐴 ∈ ℤ ↔ (𝑥 / 𝑦) ∈ ℤ)) |
48 | 46, 47 | imbi12d 233 |
. . . . 5
⊢ (𝐴 = (𝑥 / 𝑦) → ((∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴) → 𝐴 ∈ ℤ) ↔ (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt (𝑥 / 𝑦)) → (𝑥 / 𝑦) ∈ ℤ))) |
49 | 43, 48 | syl5ibrcom 156 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴) → 𝐴 ∈ ℤ))) |
50 | 49 | rexlimivv 2593 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → (∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴) → 𝐴 ∈ ℤ)) |
51 | 4, 50 | sylbi 120 |
. 2
⊢ (𝐴 ∈ ℚ →
(∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt 𝐴) → 𝐴 ∈ ℤ)) |
52 | 3, 51 | impbid2 142 |
1
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔
∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt 𝐴))) |