Metamath Proof Explorer

Theorem dvdsppwf1o

Description: A bijection between the divisors of a prime power and the integers less than or equal to the exponent. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypothesis dvdsppwf1o.f 
|- F = ( n e. ( 0 ... A ) |-> ( P ^ n ) )
Assertion dvdsppwf1o 
|- ( ( P e. Prime /\ A e. NN0 ) -> F : ( 0 ... A ) -1-1-onto-> { x e. NN | x || ( P ^ A ) } )

Proof

Step Hyp Ref Expression
1 dvdsppwf1o.f 
 |-  F = ( n e. ( 0 ... A ) |-> ( P ^ n ) )
2 breq1 
 |-  ( x = ( P ^ n ) -> ( x || ( P ^ A ) <-> ( P ^ n ) || ( P ^ A ) ) )
3 prmnn 
 |-  ( P e. Prime -> P e. NN )
4 3 adantr 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> P e. NN )
5 elfznn0 
 |-  ( n e. ( 0 ... A ) -> n e. NN0 )
6 nnexpcl 
 |-  ( ( P e. NN /\ n e. NN0 ) -> ( P ^ n ) e. NN )
7 4 5 6 syl2an 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> ( P ^ n ) e. NN )
8 prmz 
 |-  ( P e. Prime -> P e. ZZ )
9 8 ad2antrr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> P e. ZZ )
10 5 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> n e. NN0 )
11 elfzuz3 
 |-  ( n e. ( 0 ... A ) -> A e. ( ZZ>= ` n ) )
12 11 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> A e. ( ZZ>= ` n ) )
13 dvdsexp 
 |-  ( ( P e. ZZ /\ n e. NN0 /\ A e. ( ZZ>= ` n ) ) -> ( P ^ n ) || ( P ^ A ) )
14 9 10 12 13 syl3anc 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> ( P ^ n ) || ( P ^ A ) )
15 2 7 14 elrabd 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> ( P ^ n ) e. { x e. NN | x || ( P ^ A ) } )
16 simpl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> P e. Prime )
17 elrabi 
 |-  ( m e. { x e. NN | x || ( P ^ A ) } -> m e. NN )
18 pccl 
 |-  ( ( P e. Prime /\ m e. NN ) -> ( P pCnt m ) e. NN0 )
19 16 17 18 syl2an 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P pCnt m ) e. NN0 )
20 16 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> P e. Prime )
21 17 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> m e. NN )
22 21 nnzd 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> m e. ZZ )
23 8 ad2antrr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> P e. ZZ )
24 simplr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> A e. NN0 )
25 zexpcl 
 |-  ( ( P e. ZZ /\ A e. NN0 ) -> ( P ^ A ) e. ZZ )
26 23 24 25 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P ^ A ) e. ZZ )
27 breq1 
 |-  ( x = m -> ( x || ( P ^ A ) <-> m || ( P ^ A ) ) )
28 27 elrab 
 |-  ( m e. { x e. NN | x || ( P ^ A ) } <-> ( m e. NN /\ m || ( P ^ A ) ) )
29 28 simprbi 
 |-  ( m e. { x e. NN | x || ( P ^ A ) } -> m || ( P ^ A ) )
30 29 adantl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> m || ( P ^ A ) )
31 pcdvdstr 
 |-  ( ( P e. Prime /\ ( m e. ZZ /\ ( P ^ A ) e. ZZ /\ m || ( P ^ A ) ) ) -> ( P pCnt m ) <_ ( P pCnt ( P ^ A ) ) )
32 20 22 26 30 31 syl13anc 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P pCnt m ) <_ ( P pCnt ( P ^ A ) ) )
33 pcidlem 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) = A )
34 33 adantr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P pCnt ( P ^ A ) ) = A )
35 32 34 breqtrd 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P pCnt m ) <_ A )
36 fznn0 
 |-  ( A e. NN0 -> ( ( P pCnt m ) e. ( 0 ... A ) <-> ( ( P pCnt m ) e. NN0 /\ ( P pCnt m ) <_ A ) ) )
37 24 36 syl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( ( P pCnt m ) e. ( 0 ... A ) <-> ( ( P pCnt m ) e. NN0 /\ ( P pCnt m ) <_ A ) ) )
38 19 35 37 mpbir2and 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( P pCnt m ) e. ( 0 ... A ) )
39 oveq2 
 |-  ( n = A -> ( P ^ n ) = ( P ^ A ) )
40 39 breq2d 
 |-  ( n = A -> ( m || ( P ^ n ) <-> m || ( P ^ A ) ) )
41 40 rspcev 
 |-  ( ( A e. NN0 /\ m || ( P ^ A ) ) -> E. n e. NN0 m || ( P ^ n ) )
42 24 30 41 syl2anc 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> E. n e. NN0 m || ( P ^ n ) )
43 pcprmpw2 
 |-  ( ( P e. Prime /\ m e. NN ) -> ( E. n e. NN0 m || ( P ^ n ) <-> m = ( P ^ ( P pCnt m ) ) ) )
44 16 17 43 syl2an 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> ( E. n e. NN0 m || ( P ^ n ) <-> m = ( P ^ ( P pCnt m ) ) ) )
45 42 44 mpbid 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ m e. { x e. NN | x || ( P ^ A ) } ) -> m = ( P ^ ( P pCnt m ) ) )
46 45 adantrl 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ ( n e. ( 0 ... A ) /\ m e. { x e. NN | x || ( P ^ A ) } ) ) -> m = ( P ^ ( P pCnt m ) ) )
47 oveq2 
 |-  ( n = ( P pCnt m ) -> ( P ^ n ) = ( P ^ ( P pCnt m ) ) )
48 47 eqeq2d 
 |-  ( n = ( P pCnt m ) -> ( m = ( P ^ n ) <-> m = ( P ^ ( P pCnt m ) ) ) )
49 46 48 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ ( n e. ( 0 ... A ) /\ m e. { x e. NN | x || ( P ^ A ) } ) ) -> ( n = ( P pCnt m ) -> m = ( P ^ n ) ) )
50 elfzelz 
 |-  ( n e. ( 0 ... A ) -> n e. ZZ )
51 pcid 
 |-  ( ( P e. Prime /\ n e. ZZ ) -> ( P pCnt ( P ^ n ) ) = n )
52 16 50 51 syl2an 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> ( P pCnt ( P ^ n ) ) = n )
53 52 eqcomd 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ n e. ( 0 ... A ) ) -> n = ( P pCnt ( P ^ n ) ) )
54 53 adantrr 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ ( n e. ( 0 ... A ) /\ m e. { x e. NN | x || ( P ^ A ) } ) ) -> n = ( P pCnt ( P ^ n ) ) )
55 oveq2 
 |-  ( m = ( P ^ n ) -> ( P pCnt m ) = ( P pCnt ( P ^ n ) ) )
56 55 eqeq2d 
 |-  ( m = ( P ^ n ) -> ( n = ( P pCnt m ) <-> n = ( P pCnt ( P ^ n ) ) ) )
57 54 56 syl5ibrcom 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ ( n e. ( 0 ... A ) /\ m e. { x e. NN | x || ( P ^ A ) } ) ) -> ( m = ( P ^ n ) -> n = ( P pCnt m ) ) )
58 49 57 impbid 
 |-  ( ( ( P e. Prime /\ A e. NN0 ) /\ ( n e. ( 0 ... A ) /\ m e. { x e. NN | x || ( P ^ A ) } ) ) -> ( n = ( P pCnt m ) <-> m = ( P ^ n ) ) )
59 1 15 38 58 f1o2d 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> F : ( 0 ... A ) -1-1-onto-> { x e. NN | x || ( P ^ A ) } )