# Metamath Proof Explorer

## Theorem dvdsppwf1o

Description: A bijection from the divisors of a prime power to the integers less than the prime count. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypothesis dvdsppwf1o.f ${⊢}{F}=\left({n}\in \left(0\dots {A}\right)⟼{{P}}^{{n}}\right)$
Assertion dvdsppwf1o ${⊢}\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\to {F}:\left(0\dots {A}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}$

### Proof

Step Hyp Ref Expression
1 dvdsppwf1o.f ${⊢}{F}=\left({n}\in \left(0\dots {A}\right)⟼{{P}}^{{n}}\right)$
2 breq1 ${⊢}{x}={{P}}^{{n}}\to \left({x}\parallel {{P}}^{{A}}↔{{P}}^{{n}}\parallel {{P}}^{{A}}\right)$
3 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
4 3 adantr ${⊢}\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\to {P}\in ℕ$
5 elfznn0 ${⊢}{n}\in \left(0\dots {A}\right)\to {n}\in {ℕ}_{0}$
6 nnexpcl ${⊢}\left({P}\in ℕ\wedge {n}\in {ℕ}_{0}\right)\to {{P}}^{{n}}\in ℕ$
7 4 5 6 syl2an ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {{P}}^{{n}}\in ℕ$
8 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
9 8 ad2antrr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {P}\in ℤ$
10 5 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {n}\in {ℕ}_{0}$
11 elfzuz3 ${⊢}{n}\in \left(0\dots {A}\right)\to {A}\in {ℤ}_{\ge {n}}$
12 11 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {A}\in {ℤ}_{\ge {n}}$
13 dvdsexp ${⊢}\left({P}\in ℤ\wedge {n}\in {ℕ}_{0}\wedge {A}\in {ℤ}_{\ge {n}}\right)\to {{P}}^{{n}}\parallel {{P}}^{{A}}$
14 9 10 12 13 syl3anc ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {{P}}^{{n}}\parallel {{P}}^{{A}}$
15 2 7 14 elrabd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {{P}}^{{n}}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}$
16 simpl ${⊢}\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\to {P}\in ℙ$
17 elrabi ${⊢}{m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\to {m}\in ℕ$
18 pccl ${⊢}\left({P}\in ℙ\wedge {m}\in ℕ\right)\to {P}\mathrm{pCnt}{m}\in {ℕ}_{0}$
19 16 17 18 syl2an ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\mathrm{pCnt}{m}\in {ℕ}_{0}$
20 16 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\in ℙ$
21 17 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {m}\in ℕ$
22 21 nnzd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {m}\in ℤ$
23 8 ad2antrr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\in ℤ$
24 simplr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {A}\in {ℕ}_{0}$
25 zexpcl ${⊢}\left({P}\in ℤ\wedge {A}\in {ℕ}_{0}\right)\to {{P}}^{{A}}\in ℤ$
26 23 24 25 syl2anc ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {{P}}^{{A}}\in ℤ$
27 breq1 ${⊢}{x}={m}\to \left({x}\parallel {{P}}^{{A}}↔{m}\parallel {{P}}^{{A}}\right)$
28 27 elrab ${⊢}{m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}↔\left({m}\in ℕ\wedge {m}\parallel {{P}}^{{A}}\right)$
29 28 simprbi ${⊢}{m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\to {m}\parallel {{P}}^{{A}}$
30 29 adantl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {m}\parallel {{P}}^{{A}}$
31 pcdvdstr ${⊢}\left({P}\in ℙ\wedge \left({m}\in ℤ\wedge {{P}}^{{A}}\in ℤ\wedge {m}\parallel {{P}}^{{A}}\right)\right)\to {P}\mathrm{pCnt}{m}\le {P}\mathrm{pCnt}{{P}}^{{A}}$
32 20 22 26 30 31 syl13anc ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\mathrm{pCnt}{m}\le {P}\mathrm{pCnt}{{P}}^{{A}}$
33 pcidlem ${⊢}\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\to {P}\mathrm{pCnt}{{P}}^{{A}}={A}$
34 33 adantr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\mathrm{pCnt}{{P}}^{{A}}={A}$
35 32 34 breqtrd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\mathrm{pCnt}{m}\le {A}$
36 fznn0 ${⊢}{A}\in {ℕ}_{0}\to \left({P}\mathrm{pCnt}{m}\in \left(0\dots {A}\right)↔\left({P}\mathrm{pCnt}{m}\in {ℕ}_{0}\wedge {P}\mathrm{pCnt}{m}\le {A}\right)\right)$
37 24 36 syl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to \left({P}\mathrm{pCnt}{m}\in \left(0\dots {A}\right)↔\left({P}\mathrm{pCnt}{m}\in {ℕ}_{0}\wedge {P}\mathrm{pCnt}{m}\le {A}\right)\right)$
38 19 35 37 mpbir2and ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {P}\mathrm{pCnt}{m}\in \left(0\dots {A}\right)$
39 oveq2 ${⊢}{n}={A}\to {{P}}^{{n}}={{P}}^{{A}}$
40 39 breq2d ${⊢}{n}={A}\to \left({m}\parallel {{P}}^{{n}}↔{m}\parallel {{P}}^{{A}}\right)$
41 40 rspcev ${⊢}\left({A}\in {ℕ}_{0}\wedge {m}\parallel {{P}}^{{A}}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{m}\parallel {{P}}^{{n}}$
42 24 30 41 syl2anc ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{m}\parallel {{P}}^{{n}}$
43 pcprmpw2 ${⊢}\left({P}\in ℙ\wedge {m}\in ℕ\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{m}\parallel {{P}}^{{n}}↔{m}={{P}}^{{P}\mathrm{pCnt}{m}}\right)$
44 16 17 43 syl2an ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{m}\parallel {{P}}^{{n}}↔{m}={{P}}^{{P}\mathrm{pCnt}{m}}\right)$
45 42 44 mpbid ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\to {m}={{P}}^{{P}\mathrm{pCnt}{m}}$
46 45 adantrl ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge \left({n}\in \left(0\dots {A}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\right)\to {m}={{P}}^{{P}\mathrm{pCnt}{m}}$
47 oveq2 ${⊢}{n}={P}\mathrm{pCnt}{m}\to {{P}}^{{n}}={{P}}^{{P}\mathrm{pCnt}{m}}$
48 47 eqeq2d ${⊢}{n}={P}\mathrm{pCnt}{m}\to \left({m}={{P}}^{{n}}↔{m}={{P}}^{{P}\mathrm{pCnt}{m}}\right)$
49 46 48 syl5ibrcom ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge \left({n}\in \left(0\dots {A}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\right)\to \left({n}={P}\mathrm{pCnt}{m}\to {m}={{P}}^{{n}}\right)$
50 elfzelz ${⊢}{n}\in \left(0\dots {A}\right)\to {n}\in ℤ$
51 pcid ${⊢}\left({P}\in ℙ\wedge {n}\in ℤ\right)\to {P}\mathrm{pCnt}{{P}}^{{n}}={n}$
52 16 50 51 syl2an ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {P}\mathrm{pCnt}{{P}}^{{n}}={n}$
53 52 eqcomd ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge {n}\in \left(0\dots {A}\right)\right)\to {n}={P}\mathrm{pCnt}{{P}}^{{n}}$
54 53 adantrr ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge \left({n}\in \left(0\dots {A}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\right)\to {n}={P}\mathrm{pCnt}{{P}}^{{n}}$
55 oveq2 ${⊢}{m}={{P}}^{{n}}\to {P}\mathrm{pCnt}{m}={P}\mathrm{pCnt}{{P}}^{{n}}$
56 55 eqeq2d ${⊢}{m}={{P}}^{{n}}\to \left({n}={P}\mathrm{pCnt}{m}↔{n}={P}\mathrm{pCnt}{{P}}^{{n}}\right)$
57 54 56 syl5ibrcom ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge \left({n}\in \left(0\dots {A}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\right)\to \left({m}={{P}}^{{n}}\to {n}={P}\mathrm{pCnt}{m}\right)$
58 49 57 impbid ${⊢}\left(\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\wedge \left({n}\in \left(0\dots {A}\right)\wedge {m}\in \left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}\right)\right)\to \left({n}={P}\mathrm{pCnt}{m}↔{m}={{P}}^{{n}}\right)$
59 1 15 38 58 f1o2d ${⊢}\left({P}\in ℙ\wedge {A}\in {ℕ}_{0}\right)\to {F}:\left(0\dots {A}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℕ|{x}\parallel {{P}}^{{A}}\right\}$