Metamath Proof Explorer

Theorem pcneg

Description: The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion pcneg 
|- ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt -u A ) = ( P pCnt A ) )

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2 zcn 
 |-  ( x e. ZZ -> x e. CC )
3 2 ad2antrl 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> x e. CC )
4 nncn 
 |-  ( y e. NN -> y e. CC )
5 4 ad2antll 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> y e. CC )
6 nnne0 
 |-  ( y e. NN -> y =/= 0 )
7 6 ad2antll 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> y =/= 0 )
8 3 5 7 divnegd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> -u ( x / y ) = ( -u x / y ) )
9 8 oveq2d 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( P pCnt -u ( x / y ) ) = ( P pCnt ( -u x / y ) ) )
10 neg0 
 |-  -u 0 = 0
11 simpr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x = 0 ) -> x = 0 )
12 11 negeqd 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x = 0 ) -> -u x = -u 0 )
13 10 12 11 3eqtr4a 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x = 0 ) -> -u x = x )
14 13 oveq1d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x = 0 ) -> ( -u x / y ) = ( x / y ) )
15 14 oveq2d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x = 0 ) -> ( P pCnt ( -u x / y ) ) = ( P pCnt ( x / y ) ) )
16 simpll 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> P e. Prime )
17 simplrl 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> x e. ZZ )
18 17 znegcld 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> -u x e. ZZ )
19 simpr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> x =/= 0 )
20 2 negne0bd 
 |-  ( x e. ZZ -> ( x =/= 0 <-> -u x =/= 0 ) )
21 17 20 syl 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( x =/= 0 <-> -u x =/= 0 ) )
22 19 21 mpbid 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> -u x =/= 0 )
23 simplrr 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> y e. NN )
24 pcdiv 
 |-  ( ( P e. Prime /\ ( -u x e. ZZ /\ -u x =/= 0 ) /\ y e. NN ) -> ( P pCnt ( -u x / y ) ) = ( ( P pCnt -u x ) - ( P pCnt y ) ) )
25 16 18 22 23 24 syl121anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt ( -u x / y ) ) = ( ( P pCnt -u x ) - ( P pCnt y ) ) )
26 pcdiv 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
27 16 17 19 23 26 syl121anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
28 eqid 
 |-  sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < )
29 28 pczpre 
 |-  ( ( P e. Prime /\ ( -u x e. ZZ /\ -u x =/= 0 ) ) -> ( P pCnt -u x ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) )
30 16 18 22 29 syl12anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt -u x ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) )
31 eqid 
 |-  sup ( { y e. NN0 | ( P ^ y ) || x } , RR , < ) = sup ( { y e. NN0 | ( P ^ y ) || x } , RR , < )
32 31 pczpre 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( P pCnt x ) = sup ( { y e. NN0 | ( P ^ y ) || x } , RR , < ) )
33 prmz 
 |-  ( P e. Prime -> P e. ZZ )
34 zexpcl 
 |-  ( ( P e. ZZ /\ y e. NN0 ) -> ( P ^ y ) e. ZZ )
35 33 34 sylan 
 |-  ( ( P e. Prime /\ y e. NN0 ) -> ( P ^ y ) e. ZZ )
36 simpl 
 |-  ( ( x e. ZZ /\ x =/= 0 ) -> x e. ZZ )
37 dvdsnegb 
 |-  ( ( ( P ^ y ) e. ZZ /\ x e. ZZ ) -> ( ( P ^ y ) || x <-> ( P ^ y ) || -u x ) )
38 35 36 37 syl2an 
 |-  ( ( ( P e. Prime /\ y e. NN0 ) /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( ( P ^ y ) || x <-> ( P ^ y ) || -u x ) )
39 38 an32s 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) /\ y e. NN0 ) -> ( ( P ^ y ) || x <-> ( P ^ y ) || -u x ) )
40 39 rabbidva 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> { y e. NN0 | ( P ^ y ) || x } = { y e. NN0 | ( P ^ y ) || -u x } )
41 40 supeq1d 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> sup ( { y e. NN0 | ( P ^ y ) || x } , RR , < ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) )
42 32 41 eqtrd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( P pCnt x ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) )
43 16 17 19 42 syl12anc 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt x ) = sup ( { y e. NN0 | ( P ^ y ) || -u x } , RR , < ) )
44 30 43 eqtr4d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt -u x ) = ( P pCnt x ) )
45 44 oveq1d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( ( P pCnt -u x ) - ( P pCnt y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
46 27 45 eqtr4d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt -u x ) - ( P pCnt y ) ) )
47 25 46 eqtr4d 
 |-  ( ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) /\ x =/= 0 ) -> ( P pCnt ( -u x / y ) ) = ( P pCnt ( x / y ) ) )
48 15 47 pm2.61dane 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( P pCnt ( -u x / y ) ) = ( P pCnt ( x / y ) ) )
49 9 48 eqtrd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( P pCnt -u ( x / y ) ) = ( P pCnt ( x / y ) ) )
50 negeq 
 |-  ( A = ( x / y ) -> -u A = -u ( x / y ) )
51 50 oveq2d 
 |-  ( A = ( x / y ) -> ( P pCnt -u A ) = ( P pCnt -u ( x / y ) ) )
52 oveq2 
 |-  ( A = ( x / y ) -> ( P pCnt A ) = ( P pCnt ( x / y ) ) )
53 51 52 eqeq12d 
 |-  ( A = ( x / y ) -> ( ( P pCnt -u A ) = ( P pCnt A ) <-> ( P pCnt -u ( x / y ) ) = ( P pCnt ( x / y ) ) ) )
54 49 53 syl5ibrcom 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( A = ( x / y ) -> ( P pCnt -u A ) = ( P pCnt A ) ) )
55 54 rexlimdvva 
 |-  ( P e. Prime -> ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( P pCnt -u A ) = ( P pCnt A ) ) )
56 1 55 syl5bi 
 |-  ( P e. Prime -> ( A e. QQ -> ( P pCnt -u A ) = ( P pCnt A ) ) )
57 56 imp 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt -u A ) = ( P pCnt A ) )