Step | Hyp | Ref
| Expression |
1 | | isppw 24640 |
. 2
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴)) |
2 | | reu6 3362 |
. . 3
⊢
(∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) |
3 | | equid 1926 |
. . . . . . . . 9
⊢ 𝑝 = 𝑝 |
4 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝐴 ↔ 𝑝 ∥ 𝐴)) |
5 | | equequ1 1939 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 = 𝑝 ↔ 𝑝 = 𝑝)) |
6 | 4, 5 | bibi12d 334 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝))) |
7 | 6 | rspcva 3280 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) |
8 | 7 | adantll 746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) |
9 | 3, 8 | mpbiri 247 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∥ 𝐴) |
10 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∈ ℙ) |
11 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈ ℕ) |
12 | | pcelnn 15412 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
14 | 9, 13 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 pCnt 𝐴) ∈ ℕ) |
15 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑞 = 𝑝) |
16 | 15 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt 𝐴)) |
17 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑝 ∈ ℙ) |
18 | | pccl 15392 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
19 | 18 | ancoms 468 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
21 | 20 | nn0zd 11356 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈ ℤ) |
22 | | pcid 15415 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
23 | 17, 21, 22 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) |
24 | 16, 23 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
25 | 15 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
26 | 24, 25 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
27 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) |
28 | 27 | notbid 307 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (¬ 𝑞 ∥ 𝐴 ↔ ¬ 𝑞 = 𝑝)) |
29 | 28 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ 𝐴) |
30 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝑞 ∈ ℙ) |
31 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝐴 ∈ ℕ) |
32 | | pceq0 15413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) |
33 | 30, 31, 32 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) |
34 | 29, 33 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = 0) |
35 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑞 ∈ ℙ) |
36 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑝 ∈ ℙ) |
37 | 19 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
38 | | prmdvdsexpr 15267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ0) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) |
39 | 35, 36, 37, 38 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) |
40 | 39 | con3dimp 456 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴))) |
41 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
42 | 41 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
43 | 42, 19 | nnexpcld 12892 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
45 | | pceq0 15413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) |
46 | 30, 44, 45 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) |
47 | 40, 46 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0) |
48 | 34, 47 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
49 | 26, 48 | pm2.61dan 828 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
50 | 49 | expr 641 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
51 | 50 | ralimdva 2945 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
52 | 51 | imp 444 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) |
53 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
54 | 53 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈
ℕ0) |
55 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) |
56 | 55 | nnnn0d 11228 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈
ℕ0) |
57 | | pc11 15422 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ0) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
58 | 54, 56, 57 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) |
59 | 52, 58 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) |
60 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = (𝑝 pCnt 𝐴) → (𝑝↑𝑘) = (𝑝↑(𝑝 pCnt 𝐴))) |
61 | 60 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑘 = (𝑝 pCnt 𝐴) → (𝐴 = (𝑝↑𝑘) ↔ 𝐴 = (𝑝↑(𝑝 pCnt 𝐴)))) |
62 | 61 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) |
63 | 14, 59, 62 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) |
64 | 63 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
65 | | prmdvdsexpb 15266 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
66 | 65 | 3coml 1264 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
67 | 66 | 3expa 1257 |
. . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
68 | 67 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
69 | 68 | adantll 746 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) |
70 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝐴 = (𝑝↑𝑘) → (𝑞 ∥ 𝐴 ↔ 𝑞 ∥ (𝑝↑𝑘))) |
71 | 70 | bibi1d 332 |
. . . . . . . 8
⊢ (𝐴 = (𝑝↑𝑘) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) |
72 | 71 | ralbidv 2969 |
. . . . . . 7
⊢ (𝐴 = (𝑝↑𝑘) → (∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∀𝑞 ∈ ℙ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) |
73 | 69, 72 | syl5ibrcom 236 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) |
74 | 73 | rexlimdva 3013 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∃𝑘 ∈ ℕ
𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) |
75 | 64, 74 | impbid 201 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
76 | 75 | rexbidva 3031 |
. . 3
⊢ (𝐴 ∈ ℕ →
(∃𝑝 ∈ ℙ
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
77 | 2, 76 | syl5bb 271 |
. 2
⊢ (𝐴 ∈ ℕ →
(∃!𝑞 ∈ ℙ
𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) |
78 | 1, 77 | bitrd 267 |
1
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝐴 = (𝑝↑𝑘))) |