# Metamath Proof Explorer

## Theorem dvdsprmpweqnn

Description: If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion dvdsprmpweqnn ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$

### Proof

Step Hyp Ref Expression
1 eluz2nn ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℕ$
2 dvdsprmpweq ${⊢}\left({P}\in ℙ\wedge {A}\in ℕ\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
3 1 2 syl3an2 ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
4 3 imp ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}$
5 df-n0 ${⊢}{ℕ}_{0}=ℕ\cup \left\{0\right\}$
6 5 rexeqi ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}↔\exists {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}$
7 rexun ${⊢}\exists {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}↔\left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\vee \exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
8 6 7 bitri ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}↔\left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\vee \exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
9 0z ${⊢}0\in ℤ$
10 oveq2 ${⊢}{n}=0\to {{P}}^{{n}}={{P}}^{0}$
11 10 eqeq2d ${⊢}{n}=0\to \left({A}={{P}}^{{n}}↔{A}={{P}}^{0}\right)$
12 11 rexsng ${⊢}0\in ℤ\to \left(\exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}↔{A}={{P}}^{0}\right)$
13 9 12 ax-mp ${⊢}\exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}↔{A}={{P}}^{0}$
14 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
15 14 nncnd ${⊢}{P}\in ℙ\to {P}\in ℂ$
16 15 exp0d ${⊢}{P}\in ℙ\to {{P}}^{0}=1$
17 16 3ad2ant1 ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to {{P}}^{0}=1$
18 17 eqeq2d ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}={{P}}^{0}↔{A}=1\right)$
19 eluz2b3 ${⊢}{A}\in {ℤ}_{\ge 2}↔\left({A}\in ℕ\wedge {A}\ne 1\right)$
20 eqneqall ${⊢}{A}=1\to \left({A}\ne 1\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
21 20 com12 ${⊢}{A}\ne 1\to \left({A}=1\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
22 19 21 simplbiim ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({A}=1\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
23 22 3ad2ant2 ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}=1\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
24 18 23 sylbid ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}={{P}}^{0}\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
25 24 com12 ${⊢}{A}={{P}}^{0}\to \left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\right)$
26 25 impd ${⊢}{A}={{P}}^{0}\to \left(\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
27 13 26 sylbi ${⊢}\exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\to \left(\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
28 27 jao1i ${⊢}\left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\vee \exists {n}\in \left\{0\right\}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)\to \left(\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
29 8 28 sylbi ${⊢}\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\to \left(\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$
30 4 29 mpcom ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\wedge {A}\parallel {{P}}^{{N}}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}$
31 30 ex ${⊢}\left({P}\in ℙ\wedge {A}\in {ℤ}_{\ge 2}\wedge {N}\in {ℕ}_{0}\right)\to \left({A}\parallel {{P}}^{{N}}\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{P}}^{{n}}\right)$