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 ⊢A∈ℕ→Λ⁡A≠0↔∃p∈ℙ∃k∈ℕA=pk

Proof

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