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	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	pcadd2.2	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
	pcadd2.3	⊢ ( 𝜑 → 𝐵 ∈ ℚ )
	pcadd2.4	⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) < ( 𝑃 pCnt 𝐵 ) )
Assertion	pcadd2	⊢ ( 𝜑 → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt ( 𝐴 + 𝐵 ) ) )

Proof

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

Metamath Proof Explorer

Theorem pcadd2

Proof