pcneg

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

		Ref	Expression
	Assertion	pcneg	$⊢ (P \in ℙ \land A \in ℚ) \to P pCnt (- A) = P pCnt A$

Proof

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

Metamath Proof Explorer

Theorem pcneg

Proof