# 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}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$

### Proof

Step Hyp Ref Expression
1 isppw ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0↔\exists !{q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\parallel {A}\right)$
2 reu6 ${⊢}\exists !{q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\parallel {A}↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)$
3 equid ${⊢}{p}={p}$
4 breq1 ${⊢}{q}={p}\to \left({q}\parallel {A}↔{p}\parallel {A}\right)$
5 equequ1 ${⊢}{q}={p}\to \left({q}={p}↔{p}={p}\right)$
6 4 5 bibi12d ${⊢}{q}={p}\to \left(\left({q}\parallel {A}↔{q}={p}\right)↔\left({p}\parallel {A}↔{p}={p}\right)\right)$
7 6 rspcva ${⊢}\left({p}\in ℙ\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \left({p}\parallel {A}↔{p}={p}\right)$
8 7 adantll ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \left({p}\parallel {A}↔{p}={p}\right)$
9 3 8 mpbiri ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {p}\parallel {A}$
10 simplr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {p}\in ℙ$
11 simpll ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {A}\in ℕ$
12 pcelnn ${⊢}\left({p}\in ℙ\wedge {A}\in ℕ\right)\to \left({p}\mathrm{pCnt}{A}\in ℕ↔{p}\parallel {A}\right)$
13 10 11 12 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \left({p}\mathrm{pCnt}{A}\in ℕ↔{p}\parallel {A}\right)$
14 9 13 mpbird ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {p}\mathrm{pCnt}{A}\in ℕ$
15 simpr ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {q}={p}$
16 15 oveq1d ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {q}\mathrm{pCnt}{A}={p}\mathrm{pCnt}{A}$
17 simpllr ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {p}\in ℙ$
18 pccl ${⊢}\left({p}\in ℙ\wedge {A}\in ℕ\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
19 18 ancoms ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
20 19 ad2antrr ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
21 20 nn0zd ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {p}\mathrm{pCnt}{A}\in ℤ$
22 pcid ${⊢}\left({p}\in ℙ\wedge {p}\mathrm{pCnt}{A}\in ℤ\right)\to {p}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}={p}\mathrm{pCnt}{A}$
23 17 21 22 syl2anc ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {p}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}={p}\mathrm{pCnt}{A}$
24 16 23 eqtr4d ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {q}\mathrm{pCnt}{A}={p}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
25 15 oveq1d ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}={p}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
26 24 25 eqtr4d ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge {q}={p}\right)\to {q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
27 simprr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to \left({q}\parallel {A}↔{q}={p}\right)$
28 27 notbid ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to \left(¬{q}\parallel {A}↔¬{q}={p}\right)$
29 28 biimpar ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to ¬{q}\parallel {A}$
30 simplrl ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {q}\in ℙ$
31 simplll ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {A}\in ℕ$
32 pceq0 ${⊢}\left({q}\in ℙ\wedge {A}\in ℕ\right)\to \left({q}\mathrm{pCnt}{A}=0↔¬{q}\parallel {A}\right)$
33 30 31 32 syl2anc ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to \left({q}\mathrm{pCnt}{A}=0↔¬{q}\parallel {A}\right)$
34 29 33 mpbird ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {q}\mathrm{pCnt}{A}=0$
35 simprl ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to {q}\in ℙ$
36 simplr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to {p}\in ℙ$
37 19 adantr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to {p}\mathrm{pCnt}{A}\in {ℕ}_{0}$
38 prmdvdsexpr ${⊢}\left({q}\in ℙ\wedge {p}\in ℙ\wedge {p}\mathrm{pCnt}{A}\in {ℕ}_{0}\right)\to \left({q}\parallel {{p}}^{{p}\mathrm{pCnt}{A}}\to {q}={p}\right)$
39 35 36 37 38 syl3anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to \left({q}\parallel {{p}}^{{p}\mathrm{pCnt}{A}}\to {q}={p}\right)$
40 39 con3dimp ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to ¬{q}\parallel {{p}}^{{p}\mathrm{pCnt}{A}}$
41 prmnn ${⊢}{p}\in ℙ\to {p}\in ℕ$
42 41 adantl ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {p}\in ℕ$
43 42 19 nnexpcld ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to {{p}}^{{p}\mathrm{pCnt}{A}}\in ℕ$
44 43 ad2antrr ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {{p}}^{{p}\mathrm{pCnt}{A}}\in ℕ$
45 pceq0 ${⊢}\left({q}\in ℙ\wedge {{p}}^{{p}\mathrm{pCnt}{A}}\in ℕ\right)\to \left({q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}=0↔¬{q}\parallel {{p}}^{{p}\mathrm{pCnt}{A}}\right)$
46 30 44 45 syl2anc ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to \left({q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}=0↔¬{q}\parallel {{p}}^{{p}\mathrm{pCnt}{A}}\right)$
47 40 46 mpbird ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}=0$
48 34 47 eqtr4d ${⊢}\left(\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\wedge ¬{q}={p}\right)\to {q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
49 26 48 pm2.61dan ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \left({q}\in ℙ\wedge \left({q}\parallel {A}↔{q}={p}\right)\right)\right)\to {q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
50 49 expr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {q}\in ℙ\right)\to \left(\left({q}\parallel {A}↔{q}={p}\right)\to {q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}\right)$
51 50 ralimdva ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}\right)$
52 51 imp ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}$
53 nnnn0 ${⊢}{A}\in ℕ\to {A}\in {ℕ}_{0}$
54 53 ad2antrr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {A}\in {ℕ}_{0}$
55 43 adantr ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {{p}}^{{p}\mathrm{pCnt}{A}}\in ℕ$
56 55 nnnn0d ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {{p}}^{{p}\mathrm{pCnt}{A}}\in {ℕ}_{0}$
57 pc11 ${⊢}\left({A}\in {ℕ}_{0}\wedge {{p}}^{{p}\mathrm{pCnt}{A}}\in {ℕ}_{0}\right)\to \left({A}={{p}}^{{p}\mathrm{pCnt}{A}}↔\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}\right)$
58 54 56 57 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \left({A}={{p}}^{{p}\mathrm{pCnt}{A}}↔\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\mathrm{pCnt}{A}={q}\mathrm{pCnt}{{p}}^{{p}\mathrm{pCnt}{A}}\right)$
59 52 58 mpbird ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to {A}={{p}}^{{p}\mathrm{pCnt}{A}}$
60 oveq2 ${⊢}{k}={p}\mathrm{pCnt}{A}\to {{p}}^{{k}}={{p}}^{{p}\mathrm{pCnt}{A}}$
61 60 rspceeqv ${⊢}\left({p}\mathrm{pCnt}{A}\in ℕ\wedge {A}={{p}}^{{p}\mathrm{pCnt}{A}}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}$
62 14 59 61 syl2anc ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}$
63 62 ex ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
64 prmdvdsexpb ${⊢}\left({q}\in ℙ\wedge {p}\in ℙ\wedge {k}\in ℕ\right)\to \left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)$
65 64 3coml ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\wedge {q}\in ℙ\right)\to \left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)$
66 65 3expa ${⊢}\left(\left({p}\in ℙ\wedge {k}\in ℕ\right)\wedge {q}\in ℙ\right)\to \left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)$
67 66 ralrimiva ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)$
68 67 adantll ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)$
69 breq2 ${⊢}{A}={{p}}^{{k}}\to \left({q}\parallel {A}↔{q}\parallel {{p}}^{{k}}\right)$
70 69 bibi1d ${⊢}{A}={{p}}^{{k}}\to \left(\left({q}\parallel {A}↔{q}={p}\right)↔\left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)\right)$
71 70 ralbidv ${⊢}{A}={{p}}^{{k}}\to \left(\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)↔\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {{p}}^{{k}}↔{q}={p}\right)\right)$
72 68 71 syl5ibrcom ${⊢}\left(\left({A}\in ℕ\wedge {p}\in ℙ\right)\wedge {k}\in ℕ\right)\to \left({A}={{p}}^{{k}}\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)$
73 72 rexlimdva ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\to \forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)\right)$
74 63 73 impbid ${⊢}\left({A}\in ℕ\wedge {p}\in ℙ\right)\to \left(\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
75 74 rexbidva ${⊢}{A}\in ℕ\to \left(\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\forall {q}\in ℙ\phantom{\rule{.4em}{0ex}}\left({q}\parallel {A}↔{q}={p}\right)↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
76 2 75 syl5bb ${⊢}{A}\in ℕ\to \left(\exists !{q}\in ℙ\phantom{\rule{.4em}{0ex}}{q}\parallel {A}↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
77 1 76 bitrd ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$