| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. 2
⊢ (𝐴 = 0 → (𝐴 ∈ ℤ ↔ 0 ∈
ℤ)) |
| 2 | | simpll2 1214 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ) |
| 3 | 2 | nncnd 12282 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℂ) |
| 4 | 3 | mul01d 11460 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑁 · 0) = 0) |
| 5 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
| 6 | | simpll3 1215 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝐴↑𝑁) ∈ ℤ) |
| 7 | | simpll1 1213 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℚ) |
| 8 | | qcn 13005 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℂ) |
| 10 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝐴 ≠ 0) |
| 11 | 2 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ) |
| 12 | 9, 10, 11 | expne0d 14192 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝐴↑𝑁) ≠ 0) |
| 13 | | pczcl 16886 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ ((𝐴↑𝑁) ∈ ℤ ∧ (𝐴↑𝑁) ≠ 0)) → (𝑝 pCnt (𝐴↑𝑁)) ∈
ℕ0) |
| 14 | 5, 6, 12, 13 | syl12anc 837 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝐴↑𝑁)) ∈
ℕ0) |
| 15 | 14 | nn0ge0d 12590 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 0 ≤ (𝑝 pCnt (𝐴↑𝑁))) |
| 16 | | pcexp 16897 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑝 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑝 pCnt 𝐴))) |
| 17 | 5, 7, 10, 11, 16 | syl121anc 1377 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑝 pCnt 𝐴))) |
| 18 | 15, 17 | breqtrd 5169 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 0 ≤ (𝑁 · (𝑝 pCnt 𝐴))) |
| 19 | 4, 18 | eqbrtrd 5165 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑁 · 0) ≤ (𝑁 · (𝑝 pCnt 𝐴))) |
| 20 | | 0red 11264 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 0 ∈
ℝ) |
| 21 | | pcqcl 16894 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑝 pCnt 𝐴) ∈ ℤ) |
| 22 | 5, 7, 10, 21 | syl12anc 837 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℤ) |
| 23 | 22 | zred 12722 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℝ) |
| 24 | 2 | nnred 12281 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℝ) |
| 25 | 2 | nngt0d 12315 |
. . . . . 6
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 0 < 𝑁) |
| 26 | | lemul2 12120 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ (𝑝
pCnt 𝐴) ∈ ℝ
∧ (𝑁 ∈ ℝ
∧ 0 < 𝑁)) → (0
≤ (𝑝 pCnt 𝐴) ↔ (𝑁 · 0) ≤ (𝑁 · (𝑝 pCnt 𝐴)))) |
| 27 | 20, 23, 24, 25, 26 | syl112anc 1376 |
. . . . 5
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → (0 ≤ (𝑝 pCnt 𝐴) ↔ (𝑁 · 0) ≤ (𝑁 · (𝑝 pCnt 𝐴)))) |
| 28 | 19, 27 | mpbird 257 |
. . . 4
⊢ ((((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) ∧ 𝑝 ∈ ℙ) → 0 ≤ (𝑝 pCnt 𝐴)) |
| 29 | 28 | ralrimiva 3146 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) → ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴)) |
| 30 | | simpl1 1192 |
. . . 4
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℚ) |
| 31 | | pcz 16919 |
. . . 4
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔
∀𝑝 ∈ ℙ 0
≤ (𝑝 pCnt 𝐴))) |
| 32 | 30, 31 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) → (𝐴 ∈ ℤ ↔ ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴))) |
| 33 | 29, 32 | mpbird 257 |
. 2
⊢ (((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℤ) |
| 34 | | 0zd 12625 |
. 2
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 0 ∈
ℤ) |
| 35 | 1, 33, 34 | pm2.61ne 3027 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 𝐴 ∈ ℤ) |