Metamath Proof Explorer

Theorem pcdiv

Description: Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014)

Ref Expression
Assertion pcdiv 
|- ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt ( A / B ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> P e. Prime )
2 simp2l 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> A e. ZZ )
3 simp3 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> B e. NN )
4 znq 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. QQ )
5 2 3 4 syl2anc 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( A / B ) e. QQ )
6 2 zcnd 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> A e. CC )
7 3 nncnd 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> B e. CC )
8 simp2r 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> A =/= 0 )
9 3 nnne0d 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> B =/= 0 )
10 6 7 8 9 divne0d 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( A / B ) =/= 0 )
11 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < )
12 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < )
13 11 12 pcval 
 |-  ( ( P e. Prime /\ ( ( A / B ) e. QQ /\ ( A / B ) =/= 0 ) ) -> ( P pCnt ( A / B ) ) = ( iota z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
14 1 5 10 13 syl12anc 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt ( A / B ) ) = ( iota z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
15 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < )
16 15 pczpre 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( P pCnt A ) = sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) )
17 16 3adant3 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt A ) = sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) )
18 nnz 
 |-  ( B e. NN -> B e. ZZ )
19 nnne0 
 |-  ( B e. NN -> B =/= 0 )
20 18 19 jca 
 |-  ( B e. NN -> ( B e. ZZ /\ B =/= 0 ) )
21 eqid 
 |-  sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < )
22 21 pczpre 
 |-  ( ( P e. Prime /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( P pCnt B ) = sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) )
23 20 22 sylan2 
 |-  ( ( P e. Prime /\ B e. NN ) -> ( P pCnt B ) = sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) )
24 23 3adant2 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt B ) = sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) )
25 17 24 oveq12d 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) )
26 eqid 
 |-  ( A / B ) = ( A / B )
27 25 26 jctil 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( ( A / B ) = ( A / B ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) ) )
28 oveq1 
 |-  ( x = A -> ( x / y ) = ( A / y ) )
29 28 eqeq2d 
 |-  ( x = A -> ( ( A / B ) = ( x / y ) <-> ( A / B ) = ( A / y ) ) )
30 breq2 
 |-  ( x = A -> ( ( P ^ n ) || x <-> ( P ^ n ) || A ) )
31 30 rabbidv 
 |-  ( x = A -> { n e. NN0 | ( P ^ n ) || x } = { n e. NN0 | ( P ^ n ) || A } )
32 31 supeq1d 
 |-  ( x = A -> sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) )
33 32 oveq1d 
 |-  ( x = A -> ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) )
34 33 eqeq2d 
 |-  ( x = A -> ( ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
35 29 34 anbi12d 
 |-  ( x = A -> ( ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( ( A / B ) = ( A / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
36 oveq2 
 |-  ( y = B -> ( A / y ) = ( A / B ) )
37 36 eqeq2d 
 |-  ( y = B -> ( ( A / B ) = ( A / y ) <-> ( A / B ) = ( A / B ) ) )
38 breq2 
 |-  ( y = B -> ( ( P ^ n ) || y <-> ( P ^ n ) || B ) )
39 38 rabbidv 
 |-  ( y = B -> { n e. NN0 | ( P ^ n ) || y } = { n e. NN0 | ( P ^ n ) || B } )
40 39 supeq1d 
 |-  ( y = B -> sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) = sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) )
41 40 oveq2d 
 |-  ( y = B -> ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) )
42 41 eqeq2d 
 |-  ( y = B -> ( ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) ) )
43 37 42 anbi12d 
 |-  ( y = B -> ( ( ( A / B ) = ( A / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( ( A / B ) = ( A / B ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) ) ) )
44 35 43 rspc2ev 
 |-  ( ( A e. ZZ /\ B e. NN /\ ( ( A / B ) = ( A / B ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || A } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || B } , RR , < ) ) ) ) -> E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
45 2 3 27 44 syl3anc 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
46 ovex 
 |-  ( ( P pCnt A ) - ( P pCnt B ) ) e. _V
47 11 12 pceu 
 |-  ( ( P e. Prime /\ ( ( A / B ) e. QQ /\ ( A / B ) =/= 0 ) ) -> E! z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
48 1 5 10 47 syl12anc 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> E! z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
49 eqeq1 
 |-  ( z = ( ( P pCnt A ) - ( P pCnt B ) ) -> ( z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) <-> ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) )
50 49 anbi2d 
 |-  ( z = ( ( P pCnt A ) - ( P pCnt B ) ) -> ( ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
51 50 2rexbidv 
 |-  ( z = ( ( P pCnt A ) - ( P pCnt B ) ) -> ( E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) )
52 51 iota2 
 |-  ( ( ( ( P pCnt A ) - ( P pCnt B ) ) e. _V /\ E! z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) -> ( E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( iota z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) ) )
53 46 48 52 sylancr 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ ( ( P pCnt A ) - ( P pCnt B ) ) = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) <-> ( iota z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) ) )
54 45 53 mpbid 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( iota z E. x e. ZZ E. y e. NN ( ( A / B ) = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( P ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( P ^ n ) || y } , RR , < ) ) ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) )
55 14 54 eqtrd 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ B e. NN ) -> ( P pCnt ( A / B ) ) = ( ( P pCnt A ) - ( P pCnt B ) ) )