Step | Hyp | Ref
| Expression |
1 | | isppw 25996 |
. 2
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴)) |
2 | | reu6 3639 |
. . 3
⊢
(∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) |
3 | | equid 2020 |
. . . . . . . . 9
⊢ 𝑝 = 𝑝 |
4 | | breq1 5056 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝐴 ↔ 𝑝 ∥ 𝐴)) |
5 | | equequ1 2033 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 = 𝑝 ↔ 𝑝 = 𝑝)) |
6 | 4, 5 | bibi12d 349 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝))) |
7 | 6 | rspcva 3535 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) |
8 | 7 | adantll 714 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) |
9 | 3, 8 | mpbiri 261 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∥ 𝐴) |
10 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∈ ℙ) |
11 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈ ℕ) |
12 | | pcelnn 16423 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
13 | 10, 11, 12 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
14 | 9, 13 | mpbird 260 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 pCnt 𝐴) ∈ ℕ) |
15 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑞 = 𝑝) |
16 | 15 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt 𝐴)) |
17 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑝 ∈ ℙ) |
18 | | pccl 16402 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
19 | 18 | ancoms 462 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
20 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
21 | 20 | nn0zd 12280 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈ ℤ) |
22 | | pcid 16426 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
23 | 17, 21, 22 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
24 | 16, 23 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
25 | 15 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
26 | 24, 25 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
27 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) |
28 | 27 | notbid 321 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (¬ 𝑞 ∥ 𝐴 ↔ ¬ 𝑞 = 𝑝)) |
29 | 28 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ 𝐴) |
30 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝑞 ∈ ℙ) |
31 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝐴 ∈ ℕ) |
32 | | pceq0 16424 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) |
33 | 30, 31, 32 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) |
34 | 29, 33 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = 0) |
35 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑞 ∈ ℙ) |
36 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑝 ∈ ℙ) |
37 | 19 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
38 | | prmdvdsexpr 16274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ0) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) |
39 | 35, 36, 37, 38 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) |
40 | 39 | con3dimp 412 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴))) |
41 | | prmnn 16231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
43 | 42, 19 | nnexpcld 13812 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
44 | 43 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
45 | | pceq0 16424 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) |
46 | 30, 44, 45 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) |
47 | 40, 46 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0) |
48 | 34, 47 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
49 | 26, 48 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
50 | 49 | expr 460 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
51 | 50 | ralimdva 3100 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
52 | 51 | imp 410 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
53 | | nnnn0 12097 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
54 | 53 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈
ℕ0) |
55 | 43 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
56 | 55 | nnnn0d 12150 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈
ℕ0) |
57 | | pc11 16433 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ0) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
58 | 54, 56, 57 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
59 | 52, 58 | mpbird 260 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) |
60 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑘 = (𝑝 pCnt 𝐴) → (𝑝↑𝑘) = (𝑝↑(𝑝 pCnt 𝐴))) |
61 | 60 | rspceeqv 3552 |
. . . . . . 7
⊢ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) |
62 | 14, 59, 61 | syl2anc 587 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) |
63 | 62 | ex 416 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
64 | | prmdvdsexpb 16273 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
65 | 64 | 3coml 1129 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
66 | 65 | 3expa 1120 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
67 | 66 | ralrimiva 3105 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
68 | 67 | adantll 714 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
69 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝐴 = (𝑝↑𝑘) → (𝑞 ∥ 𝐴 ↔ 𝑞 ∥ (𝑝↑𝑘))) |
70 | 69 | bibi1d 347 |
. . . . . . . 8
⊢ (𝐴 = (𝑝↑𝑘) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) |
71 | 70 | ralbidv 3118 |
. . . . . . 7
⊢ (𝐴 = (𝑝↑𝑘) → (∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∀𝑞 ∈ ℙ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) |
72 | 68, 71 | syl5ibrcom 250 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) |
73 | 72 | rexlimdva 3203 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∃𝑘 ∈ ℕ
𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) |
74 | 63, 73 | impbid 215 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
75 | 74 | rexbidva 3215 |
. . 3
⊢ (𝐴 ∈ ℕ →
(∃𝑝 ∈ ℙ
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
76 | 2, 75 | syl5bb 286 |
. 2
⊢ (𝐴 ∈ ℕ →
(∃!𝑞 ∈ ℙ
𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
77 | 1, 76 | bitrd 282 |
1
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝐴 = (𝑝↑𝑘))) |