Metamath Proof Explorer


Theorem pcneg

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

Ref Expression
Assertion pcneg PAPpCntA=PpCntA

Proof

Step Hyp Ref Expression
1 elq AxyA=xy
2 zcn xx
3 2 ad2antrl Pxyx
4 nncn yy
5 4 ad2antll Pxyy
6 nnne0 yy0
7 6 ad2antll Pxyy0
8 3 5 7 divnegd Pxyxy=xy
9 8 oveq2d PxyPpCntxy=PpCntxy
10 neg0 0=0
11 simpr Pxyx=0x=0
12 11 negeqd Pxyx=0x=0
13 10 12 11 3eqtr4a Pxyx=0x=x
14 13 oveq1d Pxyx=0xy=xy
15 14 oveq2d Pxyx=0PpCntxy=PpCntxy
16 simpll Pxyx0P
17 simplrl Pxyx0x
18 17 znegcld Pxyx0x
19 simpr Pxyx0x0
20 2 negne0bd xx0x0
21 17 20 syl Pxyx0x0x0
22 19 21 mpbid Pxyx0x0
23 simplrr Pxyx0y
24 pcdiv Pxx0yPpCntxy=PpCntxPpCnty
25 16 18 22 23 24 syl121anc Pxyx0PpCntxy=PpCntxPpCnty
26 pcdiv Pxx0yPpCntxy=PpCntxPpCnty
27 16 17 19 23 26 syl121anc Pxyx0PpCntxy=PpCntxPpCnty
28 eqid supy0|Pyx<=supy0|Pyx<
29 28 pczpre Pxx0PpCntx=supy0|Pyx<
30 16 18 22 29 syl12anc Pxyx0PpCntx=supy0|Pyx<
31 eqid supy0|Pyx<=supy0|Pyx<
32 31 pczpre Pxx0PpCntx=supy0|Pyx<
33 prmz PP
34 zexpcl Py0Py
35 33 34 sylan Py0Py
36 simpl xx0x
37 dvdsnegb PyxPyxPyx
38 35 36 37 syl2an Py0xx0PyxPyx
39 38 an32s Pxx0y0PyxPyx
40 39 rabbidva Pxx0y0|Pyx=y0|Pyx
41 40 supeq1d Pxx0supy0|Pyx<=supy0|Pyx<
42 32 41 eqtrd Pxx0PpCntx=supy0|Pyx<
43 16 17 19 42 syl12anc Pxyx0PpCntx=supy0|Pyx<
44 30 43 eqtr4d Pxyx0PpCntx=PpCntx
45 44 oveq1d Pxyx0PpCntxPpCnty=PpCntxPpCnty
46 27 45 eqtr4d Pxyx0PpCntxy=PpCntxPpCnty
47 25 46 eqtr4d Pxyx0PpCntxy=PpCntxy
48 15 47 pm2.61dane PxyPpCntxy=PpCntxy
49 9 48 eqtrd PxyPpCntxy=PpCntxy
50 negeq A=xyA=xy
51 50 oveq2d A=xyPpCntA=PpCntxy
52 oveq2 A=xyPpCntA=PpCntxy
53 51 52 eqeq12d A=xyPpCntA=PpCntAPpCntxy=PpCntxy
54 49 53 syl5ibrcom PxyA=xyPpCntA=PpCntA
55 54 rexlimdvva PxyA=xyPpCntA=PpCntA
56 1 55 syl5bi PAPpCntA=PpCntA
57 56 imp PAPpCntA=PpCntA