This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isppw2

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion isppw2 ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 isppw ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑞 ∈ ℙ 𝑞 ∥ 𝐴 ) )
2 reu6 ⊢ ( ∃! 𝑞 ∈ ℙ 𝑞 ∥ 𝐴 ↔ ∃ 𝑝 ∈ ℙ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) )
3 equid ⊢ 𝑝 = 𝑝
4 breq1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 ∥ 𝐴 ↔ 𝑝 ∥ 𝐴 ) )
5 equequ1 ⊢ ( 𝑞 = 𝑝 → ( 𝑞 = 𝑝 ↔ 𝑝 = 𝑝 ) )
6 4 5 bibi12d ⊢ ( 𝑞 = 𝑝 → ( ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ↔ ( 𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝 ) ) )
7 6 rspcva ⊢ ( ( 𝑝 ∈ ℙ ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝 ) )
8 7 adantll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝑝 ∥ 𝐴 ↔ 𝑝 = 𝑝 ) )
9 3 8 mpbiri ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → 𝑝 ∥ 𝐴 )
10 simplr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → 𝑝 ∈ ℙ )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → 𝐴 ∈ ℕ )
12 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ 𝑝 ∥ 𝐴 ) )
13 10 11 12 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ 𝑝 ∥ 𝐴 ) )
14 9 13 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ )
15 simpr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → 𝑞 = 𝑝 )
16 15 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐴 ) )
17 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → 𝑝 ∈ ℙ )
18 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
19 18 ancoms ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
20 19 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
21 20 nn0zd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑝 pCnt 𝐴 ) ∈ ℤ )
22 pcid ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℤ ) → ( 𝑝 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = ( 𝑝 pCnt 𝐴 ) )
23 17 21 22 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑝 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = ( 𝑝 pCnt 𝐴 ) )
24 16 23 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑝 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
25 15 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = ( 𝑝 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
26 24 25 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
27 simprr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) )
28 27 notbid ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → ( ¬ 𝑞 ∥ 𝐴 ↔ ¬ 𝑞 = 𝑝 ) )
29 28 biimpar ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ¬ 𝑞 ∥ 𝐴 )
30 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → 𝑞 ∈ ℙ )
31 simplll ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → 𝐴 ∈ ℕ )
32 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑞 pCnt 𝐴 ) = 0 ↔ ¬ 𝑞 ∥ 𝐴 ) )
33 30 31 32 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( ( 𝑞 pCnt 𝐴 ) = 0 ↔ ¬ 𝑞 ∥ 𝐴 ) )
34 29 33 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = 0 )
35 simprl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → 𝑞 ∈ ℙ )
36 simplr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → 𝑝 ∈ ℙ )
37 19 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
38 prmdvdsexpr ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 ) → ( 𝑞 ∥ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) → 𝑞 = 𝑝 ) )
39 35 36 37 38 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → ( 𝑞 ∥ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) → 𝑞 = 𝑝 ) )
40 39 con3dimp ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ¬ 𝑞 ∥ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) )
41 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
42 41 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
43 42 19 nnexpcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ )
44 43 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ )
45 pceq0 ⊢ ( ( 𝑞 ∈ ℙ ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ ) → ( ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
46 30 44 45 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = 0 ↔ ¬ 𝑞 ∥ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
47 40 46 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = 0 )
48 34 47 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) ∧ ¬ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
49 26 48 pm2.61dan ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ ℙ ∧ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
50 49 expr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) → ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ) )
51 50 ralimdva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ) )
52 51 imp ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) )
53 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
54 53 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → 𝐴 ∈ ℕ0 )
55 43 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ )
56 55 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ0 )
57 pc11 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ0 ) → ( 𝐴 = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ) )
58 54 56 57 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ( 𝐴 = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 pCnt 𝐴 ) = ( 𝑞 pCnt ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ) )
59 52 58 mpbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → 𝐴 = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) )
60 oveq2 ⊢ ( 𝑘 = ( 𝑝 pCnt 𝐴 ) → ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) )
61 60 rspceeqv ⊢ ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ 𝐴 = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) → ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) )
62 14 59 61 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) → ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) )
63 62 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) → ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
64 prmdvdsexpb ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) )
65 64 3coml ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) )
66 65 3expa ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) )
67 66 ralrimiva ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) )
68 67 adantll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) )
69 breq2 ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( 𝑞 ∥ 𝐴 ↔ 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ) )
70 69 bibi1d ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ↔ ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) ) )
71 70 ralbidv ⊢ ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ( ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ ( 𝑝 ↑ 𝑘 ) ↔ 𝑞 = 𝑝 ) ) )
72 68 71 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 = ( 𝑝 ↑ 𝑘 ) → ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) )
73 72 rexlimdva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) → ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ) )
74 63 73 impbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ↔ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
75 74 rexbidva ⊢ ( 𝐴 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝐴 ↔ 𝑞 = 𝑝 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
76 2 75 bitrid ⊢ ( 𝐴 ∈ ℕ → ( ∃! 𝑞 ∈ ℙ 𝑞 ∥ 𝐴 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )
77 1 76 bitrd ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝 ↑ 𝑘 ) ) )