| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | isppw 27158 | . 2
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴)) | 
| 2 |  | reu6 3731 | . . 3
⊢
(∃!𝑞 ∈
ℙ 𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) | 
| 3 |  | equid 2010 | . . . . . . . . 9
⊢ 𝑝 = 𝑝 | 
| 4 |  | breq1 5145 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝐴 ↔ 𝑝 ∥ 𝐴)) | 
| 5 |  | equequ1 2023 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 = 𝑝 ↔ 𝑝 = 𝑝)) | 
| 6 | 4, 5 | bibi12d 345 | . . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝))) | 
| 7 | 6 | rspcva 3619 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) | 
| 8 | 7 | adantll 714 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝)) | 
| 9 | 3, 8 | mpbiri 258 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∥ 𝐴) | 
| 10 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝑝 ∈ ℙ) | 
| 11 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈ ℕ) | 
| 12 |  | pcelnn 16909 | . . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) | 
| 13 | 10, 11, 12 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) | 
| 14 | 9, 13 | mpbird 257 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝 pCnt 𝐴) ∈ ℕ) | 
| 15 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑞 = 𝑝) | 
| 16 | 15 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt 𝐴)) | 
| 17 |  | simpllr 775 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → 𝑝 ∈ ℙ) | 
| 18 |  | pccl 16888 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) | 
| 19 | 18 | ancoms 458 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈
ℕ0) | 
| 21 | 20 | nn0zd 12641 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt 𝐴) ∈ ℤ) | 
| 22 |  | pcid 16912 | . . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℤ) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) | 
| 23 | 17, 21, 22 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴)) | 
| 24 | 16, 23 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 25 | 15 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = (𝑝 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 26 | 24, 25 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 27 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) | 
| 28 | 27 | notbid 318 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (¬ 𝑞 ∥ 𝐴 ↔ ¬ 𝑞 = 𝑝)) | 
| 29 | 28 | biimpar 477 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ 𝐴) | 
| 30 |  | simplrl 776 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝑞 ∈ ℙ) | 
| 31 |  | simplll 774 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → 𝐴 ∈ ℕ) | 
| 32 |  | pceq0 16910 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt 𝐴) = 0 ↔ ¬ 𝑞 ∥ 𝐴)) | 
| 34 | 29, 33 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = 0) | 
| 35 |  | simprl 770 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑞 ∈ ℙ) | 
| 36 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → 𝑝 ∈ ℙ) | 
| 37 | 19 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑝 pCnt 𝐴) ∈
ℕ0) | 
| 38 |  | prmdvdsexpr 16755 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ0) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) | 
| 39 | 35, 36, 37, 38 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)) → 𝑞 = 𝑝)) | 
| 40 | 39 | con3dimp 408 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴))) | 
| 41 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) | 
| 43 | 42, 19 | nnexpcld 14285 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) | 
| 45 |  | pceq0 16910 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℙ ∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 46 | 30, 44, 45 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → ((𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0 ↔ ¬ 𝑞 ∥ (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 47 | 40, 46 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))) = 0) | 
| 48 | 34, 47 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) ∧ ¬ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 49 | 26, 48 | pm2.61dan 812 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑞 ∈ ℙ ∧ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 50 | 49 | expr 456 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑞 ∈ ℙ) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) | 
| 51 | 50 | ralimdva 3166 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) | 
| 52 | 51 | imp 406 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴)))) | 
| 53 |  | nnnn0 12535 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) | 
| 54 | 53 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 ∈
ℕ0) | 
| 55 | 43 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ) | 
| 56 | 55 | nnnn0d 12589 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝑝↑(𝑝 pCnt 𝐴)) ∈
ℕ0) | 
| 57 |  | pc11 16919 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ (𝑝↑(𝑝 pCnt 𝐴)) ∈ ℕ0) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) | 
| 58 | 54, 56, 57 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → (𝐴 = (𝑝↑(𝑝 pCnt 𝐴)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝐴) = (𝑞 pCnt (𝑝↑(𝑝 pCnt 𝐴))))) | 
| 59 | 52, 58 | mpbird 257 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) | 
| 60 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑘 = (𝑝 pCnt 𝐴) → (𝑝↑𝑘) = (𝑝↑(𝑝 pCnt 𝐴))) | 
| 61 | 60 | rspceeqv 3644 | . . . . . . 7
⊢ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ 𝐴 = (𝑝↑(𝑝 pCnt 𝐴))) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) | 
| 62 | 14, 59, 61 | syl2anc 584 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝)) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘)) | 
| 63 | 62 | ex 412 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) → ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | 
| 64 |  | prmdvdsexpb 16754 | . . . . . . . . . . 11
⊢ ((𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) | 
| 65 | 64 | 3coml 1127 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) | 
| 66 | 65 | 3expa 1118 | . . . . . . . . 9
⊢ (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) | 
| 67 | 66 | ralrimiva 3145 | . . . . . . . 8
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) | 
| 68 | 67 | adantll 714 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) →
∀𝑞 ∈ ℙ
(𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝)) | 
| 69 |  | breq2 5146 | . . . . . . . . 9
⊢ (𝐴 = (𝑝↑𝑘) → (𝑞 ∥ 𝐴 ↔ 𝑞 ∥ (𝑝↑𝑘))) | 
| 70 | 69 | bibi1d 343 | . . . . . . . 8
⊢ (𝐴 = (𝑝↑𝑘) → ((𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) | 
| 71 | 70 | ralbidv 3177 | . . . . . . 7
⊢ (𝐴 = (𝑝↑𝑘) → (∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∀𝑞 ∈ ℙ (𝑞 ∥ (𝑝↑𝑘) ↔ 𝑞 = 𝑝))) | 
| 72 | 68, 71 | syl5ibrcom 247 | . . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) | 
| 73 | 72 | rexlimdva 3154 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∃𝑘 ∈ ℕ
𝐴 = (𝑝↑𝑘) → ∀𝑞 ∈ ℙ (𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝))) | 
| 74 | 63, 73 | impbid 212 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | 
| 75 | 74 | rexbidva 3176 | . . 3
⊢ (𝐴 ∈ ℕ →
(∃𝑝 ∈ ℙ
∀𝑞 ∈ ℙ
(𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝) ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | 
| 76 | 2, 75 | bitrid 283 | . 2
⊢ (𝐴 ∈ ℕ →
(∃!𝑞 ∈ ℙ
𝑞 ∥ 𝐴 ↔ ∃𝑝 ∈ ℙ ∃𝑘 ∈ ℕ 𝐴 = (𝑝↑𝑘))) | 
| 77 | 1, 76 | bitrd 279 | 1
⊢ (𝐴 ∈ ℕ →
((Λ‘𝐴) ≠ 0
↔ ∃𝑝 ∈
ℙ ∃𝑘 ∈
ℕ 𝐴 = (𝑝↑𝑘))) |