Step | Hyp | Ref
| Expression |
1 | | simplr 525 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝐴 ∈ ℕ) |
2 | 1 | nnnn0d 9177 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝐴 ∈
ℕ0) |
3 | | prmnn 12053 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 3 | ad2antrr 485 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝑃 ∈ ℕ) |
5 | | pccl 12242 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
6 | 5 | adantr 274 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt 𝐴) ∈
ℕ0) |
7 | 4, 6 | nnexpcld 10620 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
8 | 7 | nnnn0d 9177 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃↑(𝑃 pCnt 𝐴)) ∈
ℕ0) |
9 | 6 | nn0red 9178 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt 𝐴) ∈ ℝ) |
10 | 9 | leidd 8422 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐴)) |
11 | | simpll 524 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝑃 ∈ ℙ) |
12 | 6 | nn0zd 9321 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt 𝐴) ∈ ℤ) |
13 | | pcid 12266 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 pCnt 𝐴) ∈ ℤ) → (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝐴))) = (𝑃 pCnt 𝐴)) |
14 | 11, 12, 13 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝐴))) = (𝑃 pCnt 𝐴)) |
15 | 10, 14 | breqtrrd 4015 |
. . . . . . . . 9
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
16 | 15 | ad2antrr 485 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
17 | | simpr 109 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
18 | 17 | oveq1d 5866 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt 𝐴) = (𝑃 pCnt 𝐴)) |
19 | 17 | oveq1d 5866 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴))) = (𝑃 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
20 | 16, 18, 19 | 3brtr4d 4019 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 = 𝑃) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
21 | | simplrr 531 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝐴 ∥ (𝑃↑𝑛)) |
22 | | prmz 12054 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
23 | 22 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ) |
24 | 1 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℕ) |
25 | 24 | nnzd 9322 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ) |
26 | | simprl 526 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝑛 ∈ ℕ0) |
27 | 4, 26 | nnexpcld 10620 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃↑𝑛) ∈ ℕ) |
28 | 27 | adantr 274 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑃↑𝑛) ∈ ℕ) |
29 | 28 | nnzd 9322 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑃↑𝑛) ∈ ℤ) |
30 | | dvdstr 11779 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑃↑𝑛) ∈ ℤ) → ((𝑝 ∥ 𝐴 ∧ 𝐴 ∥ (𝑃↑𝑛)) → 𝑝 ∥ (𝑃↑𝑛))) |
31 | 23, 25, 29, 30 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 ∧ 𝐴 ∥ (𝑃↑𝑛)) → 𝑝 ∥ (𝑃↑𝑛))) |
32 | 21, 31 | mpan2d 426 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ 𝐴 → 𝑝 ∥ (𝑃↑𝑛))) |
33 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
34 | 11 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝑃 ∈ ℙ) |
35 | | simplrl 530 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝑛 ∈ ℕ0) |
36 | | prmdvdsexpr 12093 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℕ0)
→ (𝑝 ∥ (𝑃↑𝑛) → 𝑝 = 𝑃)) |
37 | 33, 34, 35, 36 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (𝑃↑𝑛) → 𝑝 = 𝑃)) |
38 | 32, 37 | syld 45 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ 𝐴 → 𝑝 = 𝑃)) |
39 | 38 | necon3ad 2382 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 ≠ 𝑃 → ¬ 𝑝 ∥ 𝐴)) |
40 | 39 | imp 123 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ¬ 𝑝 ∥ 𝐴) |
41 | | simplr 525 |
. . . . . . . . . 10
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 𝑝 ∈ ℙ) |
42 | 1 | ad2antrr 485 |
. . . . . . . . . 10
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 𝐴 ∈ ℕ) |
43 | | pceq0 12264 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑝 pCnt 𝐴) = 0 ↔ ¬ 𝑝 ∥ 𝐴)) |
44 | 41, 42, 43 | syl2anc 409 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → ((𝑝 pCnt 𝐴) = 0 ↔ ¬ 𝑝 ∥ 𝐴)) |
45 | 40, 44 | mpbird 166 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt 𝐴) = 0) |
46 | 7 | ad2antrr 485 |
. . . . . . . . . 10
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
47 | 41, 46 | pccld 12243 |
. . . . . . . . 9
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴))) ∈
ℕ0) |
48 | 47 | nn0ge0d 9180 |
. . . . . . . 8
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → 0 ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
49 | 45, 48 | eqbrtrd 4009 |
. . . . . . 7
⊢
(((((𝑃 ∈
ℙ ∧ 𝐴 ∈
ℕ) ∧ (𝑛 ∈
ℕ0 ∧ 𝐴
∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≠ 𝑃) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
50 | | prmz 12054 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
51 | 50 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → 𝑃 ∈
ℤ) |
52 | 51 | ad2antrr 485 |
. . . . . . . . 9
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → 𝑃 ∈ ℤ) |
53 | | zdceq 9276 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℤ ∧ 𝑃 ∈ ℤ) →
DECID 𝑝 =
𝑃) |
54 | 23, 52, 53 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → DECID
𝑝 = 𝑃) |
55 | | dcne 2351 |
. . . . . . . 8
⊢
(DECID 𝑝 = 𝑃 ↔ (𝑝 = 𝑃 ∨ 𝑝 ≠ 𝑃)) |
56 | 54, 55 | sylib 121 |
. . . . . . 7
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 = 𝑃 ∨ 𝑝 ≠ 𝑃)) |
57 | 20, 49, 56 | mpjaodan 793 |
. . . . . 6
⊢ ((((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
58 | 57 | ralrimiva 2543 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴)))) |
59 | 1 | nnzd 9322 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝐴 ∈ ℤ) |
60 | 7 | nnzd 9322 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) |
61 | | pc2dvds 12272 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) → (𝐴 ∥ (𝑃↑(𝑃 pCnt 𝐴)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴))))) |
62 | 59, 60, 61 | syl2anc 409 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝐴 ∥ (𝑃↑(𝑃 pCnt 𝐴)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝐴))))) |
63 | 58, 62 | mpbird 166 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝐴 ∥ (𝑃↑(𝑃 pCnt 𝐴))) |
64 | | pcdvds 12257 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
65 | 64 | adantr 274 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴) |
66 | | dvdseq 11797 |
. . . 4
⊢ (((𝐴 ∈ ℕ0
∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ0) ∧ (𝐴 ∥ (𝑃↑(𝑃 pCnt 𝐴)) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∥ 𝐴)) → 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))) |
67 | 2, 8, 63, 65, 66 | syl22anc 1234 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) ∧ (𝑛 ∈ ℕ0
∧ 𝐴 ∥ (𝑃↑𝑛))) → 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))) |
68 | 67 | rexlimdvaa 2588 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) →
(∃𝑛 ∈
ℕ0 𝐴
∥ (𝑃↑𝑛) → 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |
69 | 3 | adantr 274 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → 𝑃 ∈
ℕ) |
70 | 69, 5 | nnexpcld 10620 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℕ) |
71 | 70 | nnzd 9322 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ) |
72 | | iddvds 11755 |
. . . . 5
⊢ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℤ → (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑(𝑃 pCnt 𝐴))) |
73 | 71, 72 | syl 14 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑(𝑃 pCnt 𝐴))) |
74 | | oveq2 5859 |
. . . . . 6
⊢ (𝑛 = (𝑃 pCnt 𝐴) → (𝑃↑𝑛) = (𝑃↑(𝑃 pCnt 𝐴))) |
75 | 74 | breq2d 3999 |
. . . . 5
⊢ (𝑛 = (𝑃 pCnt 𝐴) → ((𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑𝑛) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑(𝑃 pCnt 𝐴)))) |
76 | 75 | rspcev 2834 |
. . . 4
⊢ (((𝑃 pCnt 𝐴) ∈ ℕ0 ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑(𝑃 pCnt 𝐴))) → ∃𝑛 ∈ ℕ0 (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑𝑛)) |
77 | 5, 73, 76 | syl2anc 409 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) →
∃𝑛 ∈
ℕ0 (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑𝑛)) |
78 | | breq1 3990 |
. . . 4
⊢ (𝐴 = (𝑃↑(𝑃 pCnt 𝐴)) → (𝐴 ∥ (𝑃↑𝑛) ↔ (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑𝑛))) |
79 | 78 | rexbidv 2471 |
. . 3
⊢ (𝐴 = (𝑃↑(𝑃 pCnt 𝐴)) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ ∃𝑛 ∈ ℕ0 (𝑃↑(𝑃 pCnt 𝐴)) ∥ (𝑃↑𝑛))) |
80 | 77, 79 | syl5ibrcom 156 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝐴 = (𝑃↑(𝑃 pCnt 𝐴)) → ∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛))) |
81 | 68, 80 | impbid 128 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) →
(∃𝑛 ∈
ℕ0 𝐴
∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |