pcadd2

Description: The inequality of pcadd becomes an equality when one of the factors has prime count strictly less than the other. (Contributed by Mario Carneiro, 16-Jan-2015) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	pcadd2.1	$⊢ φ \to P \in ℙ$
	pcadd2.2	$⊢ φ \to A \in ℚ$
	pcadd2.3	$⊢ φ \to B \in ℚ$
	pcadd2.4	$⊢ φ \to P pCnt A < P pCnt B$
Assertion	pcadd2	$⊢ φ \to P pCnt A = P pCnt (A + B)$

Proof

Step	Hyp	Ref	Expression
1		pcadd2.1	$⊢ φ \to P \in ℙ$
2		pcadd2.2	$⊢ φ \to A \in ℚ$
3		pcadd2.3	$⊢ φ \to B \in ℚ$
4		pcadd2.4	$⊢ φ \to P pCnt A < P pCnt B$
5		pcxcl	$⊢ (P \in ℙ \land A \in ℚ) \to P pCnt A \in ℝ^{*}$
6	1 2 5	syl2anc	$⊢ φ \to P pCnt A \in ℝ^{*}$
7		qaddcl	$⊢ (A \in ℚ \land B \in ℚ) \to A + B \in ℚ$
8	2 3 7	syl2anc	$⊢ φ \to A + B \in ℚ$
9		pcxcl	$⊢ (P \in ℙ \land A + B \in ℚ) \to P pCnt (A + B) \in ℝ^{*}$
10	1 8 9	syl2anc	$⊢ φ \to P pCnt (A + B) \in ℝ^{*}$
11		pcxcl	$⊢ (P \in ℙ \land B \in ℚ) \to P pCnt B \in ℝ^{*}$
12	1 3 11	syl2anc	$⊢ φ \to P pCnt B \in ℝ^{*}$
13	6 12 4	xrltled	$⊢ φ \to P pCnt A \leq P pCnt B$
14	1 2 3 13	pcadd	$⊢ φ \to P pCnt A \leq P pCnt (A + B)$
15		qnegcl	$⊢ B \in ℚ \to - B \in ℚ$
16	3 15	syl	$⊢ φ \to - B \in ℚ$
17		xrltnle	$⊢ (P pCnt A \in ℝ^{} \land P pCnt B \in ℝ^{}) \to (P pCnt A < P pCnt B \leftrightarrow \neg P pCnt B \leq P pCnt A)$
18	6 12 17	syl2anc	$⊢ φ \to (P pCnt A < P pCnt B \leftrightarrow \neg P pCnt B \leq P pCnt A)$
19	4 18	mpbid	$⊢ φ \to \neg P pCnt B \leq P pCnt A$
20	1	adantr	$⊢ (φ \land P pCnt B \leq P pCnt (A + B)) \to P \in ℙ$
21	16	adantr	$⊢ (φ \land P pCnt B \leq P pCnt (A + B)) \to - B \in ℚ$
22	8	adantr	$⊢ (φ \land P pCnt B \leq P pCnt (A + B)) \to A + B \in ℚ$
23		pcneg	$⊢ (P \in ℙ \land B \in ℚ) \to P pCnt (- B) = P pCnt B$
24	1 3 23	syl2anc	$⊢ φ \to P pCnt (- B) = P pCnt B$
25	24	breq1d	$⊢ φ \to (P pCnt (- B) \leq P pCnt (A + B) \leftrightarrow P pCnt B \leq P pCnt (A + B))$
26	25	biimpar	$⊢ (φ \land P pCnt B \leq P pCnt (A + B)) \to P pCnt (- B) \leq P pCnt (A + B)$
27	20 21 22 26	pcadd	$⊢ (φ \land P pCnt B \leq P pCnt (A + B)) \to P pCnt (- B) \leq P pCnt ((- B) + A + B)$
28	27	ex	$⊢ φ \to (P pCnt B \leq P pCnt (A + B) \to P pCnt (- B) \leq P pCnt ((- B) + A + B))$
29		qcn	$⊢ B \in ℚ \to B \in ℂ$
30	3 29	syl	$⊢ φ \to B \in ℂ$
31	30	negcld	$⊢ φ \to - B \in ℂ$
32		qcn	$⊢ A \in ℚ \to A \in ℂ$
33	2 32	syl	$⊢ φ \to A \in ℂ$
34	31 33 30	add12d	$⊢ φ \to (- B) + A + B = A + (- B) + B$
35	31 30	addcomd	$⊢ φ \to - B + B = B + (- B)$
36	30	negidd	$⊢ φ \to B + (- B) = 0$
37	35 36	eqtrd	$⊢ φ \to - B + B = 0$
38	37	oveq2d	$⊢ φ \to A + (- B) + B = A + 0$
39	33	addridd	$⊢ φ \to A + 0 = A$
40	34 38 39	3eqtrd	$⊢ φ \to (- B) + A + B = A$
41	40	oveq2d	$⊢ φ \to P pCnt ((- B) + A + B) = P pCnt A$
42	24 41	breq12d	$⊢ φ \to (P pCnt (- B) \leq P pCnt ((- B) + A + B) \leftrightarrow P pCnt B \leq P pCnt A)$
43	28 42	sylibd	$⊢ φ \to (P pCnt B \leq P pCnt (A + B) \to P pCnt B \leq P pCnt A)$
44	19 43	mtod	$⊢ φ \to \neg P pCnt B \leq P pCnt (A + B)$
45		xrltnle	$⊢ (P pCnt (A + B) \in ℝ^{} \land P pCnt B \in ℝ^{}) \to (P pCnt (A + B) < P pCnt B \leftrightarrow \neg P pCnt B \leq P pCnt (A + B))$
46	10 12 45	syl2anc	$⊢ φ \to (P pCnt (A + B) < P pCnt B \leftrightarrow \neg P pCnt B \leq P pCnt (A + B))$
47	44 46	mpbird	$⊢ φ \to P pCnt (A + B) < P pCnt B$
48	10 12 47	xrltled	$⊢ φ \to P pCnt (A + B) \leq P pCnt B$
49	48 24	breqtrrd	$⊢ φ \to P pCnt (A + B) \leq P pCnt (- B)$
50	1 8 16 49	pcadd	$⊢ φ \to P pCnt (A + B) \leq P pCnt (A + B + (- B))$
51	33 30 31	addassd	$⊢ φ \to A + B + (- B) = A + B + (- B)$
52	36	oveq2d	$⊢ φ \to A + B + (- B) = A + 0$
53	51 52 39	3eqtrd	$⊢ φ \to A + B + (- B) = A$
54	53	oveq2d	$⊢ φ \to P pCnt (A + B + (- B)) = P pCnt A$
55	50 54	breqtrd	$⊢ φ \to P pCnt (A + B) \leq P pCnt A$
56	6 10 14 55	xrletrid	$⊢ φ \to P pCnt A = P pCnt (A + B)$

Metamath Proof Explorer

Theorem pcadd2

Proof