# Metamath Proof Explorer

## Theorem pcneg

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

Ref Expression
Assertion pcneg ${⊢}\left({P}\in ℙ\wedge {A}\in ℚ\right)\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}$

### Proof

Step Hyp Ref Expression
1 elq ${⊢}{A}\in ℚ↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}$
2 zcn ${⊢}{x}\in ℤ\to {x}\in ℂ$
3 2 ad2antrl ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {x}\in ℂ$
4 nncn ${⊢}{y}\in ℕ\to {y}\in ℂ$
5 4 ad2antll ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {y}\in ℂ$
6 nnne0 ${⊢}{y}\in ℕ\to {y}\ne 0$
7 6 ad2antll ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {y}\ne 0$
8 3 5 7 divnegd ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to -\frac{{x}}{{y}}=\frac{-{x}}{{y}}$
9 8 oveq2d ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {P}\mathrm{pCnt}\left(-\frac{{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)$
10 neg0 ${⊢}-0=0$
11 simpr ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}=0\right)\to {x}=0$
12 11 negeqd ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}=0\right)\to -{x}=-0$
13 10 12 11 3eqtr4a ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}=0\right)\to -{x}={x}$
14 13 oveq1d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}=0\right)\to \frac{-{x}}{{y}}=\frac{{x}}{{y}}$
15 14 oveq2d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}=0\right)\to {P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)$
16 simpll ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\in ℙ$
17 simplrl ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {x}\in ℤ$
18 17 znegcld ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to -{x}\in ℤ$
19 simpr ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {x}\ne 0$
20 2 negne0bd ${⊢}{x}\in ℤ\to \left({x}\ne 0↔-{x}\ne 0\right)$
21 17 20 syl ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to \left({x}\ne 0↔-{x}\ne 0\right)$
22 19 21 mpbid ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to -{x}\ne 0$
23 simplrr ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {y}\in ℕ$
24 pcdiv ${⊢}\left({P}\in ℙ\wedge \left(-{x}\in ℤ\wedge -{x}\ne 0\right)\wedge {y}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)=\left({P}\mathrm{pCnt}\left(-{x}\right)\right)-\left({P}\mathrm{pCnt}{y}\right)$
25 16 18 22 23 24 syl121anc ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)=\left({P}\mathrm{pCnt}\left(-{x}\right)\right)-\left({P}\mathrm{pCnt}{y}\right)$
26 pcdiv ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\wedge {y}\in ℕ\right)\to {P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)=\left({P}\mathrm{pCnt}{x}\right)-\left({P}\mathrm{pCnt}{y}\right)$
27 16 17 19 23 26 syl121anc ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)=\left({P}\mathrm{pCnt}{x}\right)-\left({P}\mathrm{pCnt}{y}\right)$
28 eqid ${⊢}sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
29 28 pczpre ${⊢}\left({P}\in ℙ\wedge \left(-{x}\in ℤ\wedge -{x}\ne 0\right)\right)\to {P}\mathrm{pCnt}\left(-{x}\right)=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
30 16 18 22 29 syl12anc ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(-{x}\right)=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
31 eqid ${⊢}sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel {x}\right\},ℝ,<\right)=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel {x}\right\},ℝ,<\right)$
32 31 pczpre ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\to {P}\mathrm{pCnt}{x}=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel {x}\right\},ℝ,<\right)$
33 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
34 zexpcl ${⊢}\left({P}\in ℤ\wedge {y}\in {ℕ}_{0}\right)\to {{P}}^{{y}}\in ℤ$
35 33 34 sylan ${⊢}\left({P}\in ℙ\wedge {y}\in {ℕ}_{0}\right)\to {{P}}^{{y}}\in ℤ$
36 simpl ${⊢}\left({x}\in ℤ\wedge {x}\ne 0\right)\to {x}\in ℤ$
37 dvdsnegb ${⊢}\left({{P}}^{{y}}\in ℤ\wedge {x}\in ℤ\right)\to \left({{P}}^{{y}}\parallel {x}↔{{P}}^{{y}}\parallel \left(-{x}\right)\right)$
38 35 36 37 syl2an ${⊢}\left(\left({P}\in ℙ\wedge {y}\in {ℕ}_{0}\right)\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\to \left({{P}}^{{y}}\parallel {x}↔{{P}}^{{y}}\parallel \left(-{x}\right)\right)$
39 38 an32s ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\wedge {y}\in {ℕ}_{0}\right)\to \left({{P}}^{{y}}\parallel {x}↔{{P}}^{{y}}\parallel \left(-{x}\right)\right)$
40 39 rabbidva ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\to \left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel {x}\right\}=\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\}$
41 40 supeq1d ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\to sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel {x}\right\},ℝ,<\right)=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
42 32 41 eqtrd ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {x}\ne 0\right)\right)\to {P}\mathrm{pCnt}{x}=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
43 16 17 19 42 syl12anc ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}{x}=sup\left(\left\{{y}\in {ℕ}_{0}|{{P}}^{{y}}\parallel \left(-{x}\right)\right\},ℝ,<\right)$
44 30 43 eqtr4d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(-{x}\right)={P}\mathrm{pCnt}{x}$
45 44 oveq1d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to \left({P}\mathrm{pCnt}\left(-{x}\right)\right)-\left({P}\mathrm{pCnt}{y}\right)=\left({P}\mathrm{pCnt}{x}\right)-\left({P}\mathrm{pCnt}{y}\right)$
46 27 45 eqtr4d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)=\left({P}\mathrm{pCnt}\left(-{x}\right)\right)-\left({P}\mathrm{pCnt}{y}\right)$
47 25 46 eqtr4d ${⊢}\left(\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\wedge {x}\ne 0\right)\to {P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)$
48 15 47 pm2.61dane ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {P}\mathrm{pCnt}\left(\frac{-{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)$
49 9 48 eqtrd ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to {P}\mathrm{pCnt}\left(-\frac{{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)$
50 negeq ${⊢}{A}=\frac{{x}}{{y}}\to -{A}=-\frac{{x}}{{y}}$
51 50 oveq2d ${⊢}{A}=\frac{{x}}{{y}}\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}\left(-\frac{{x}}{{y}}\right)$
52 oveq2 ${⊢}{A}=\frac{{x}}{{y}}\to {P}\mathrm{pCnt}{A}={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)$
53 51 52 eqeq12d ${⊢}{A}=\frac{{x}}{{y}}\to \left({P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}↔{P}\mathrm{pCnt}\left(-\frac{{x}}{{y}}\right)={P}\mathrm{pCnt}\left(\frac{{x}}{{y}}\right)\right)$
54 49 53 syl5ibrcom ${⊢}\left({P}\in ℙ\wedge \left({x}\in ℤ\wedge {y}\in ℕ\right)\right)\to \left({A}=\frac{{x}}{{y}}\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}\right)$
55 54 rexlimdvva ${⊢}{P}\in ℙ\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}\right)$
56 1 55 syl5bi ${⊢}{P}\in ℙ\to \left({A}\in ℚ\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}\right)$
57 56 imp ${⊢}\left({P}\in ℙ\wedge {A}\in ℚ\right)\to {P}\mathrm{pCnt}\left(-{A}\right)={P}\mathrm{pCnt}{A}$