Metamath Proof Explorer

Theorem 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 ⊢ φ → P ∈ ℙ
pcadd2.2 ⊢ φ → A ∈ ℚ
pcadd2.3 ⊢ φ → B ∈ ℚ
pcadd2.4 ⊢ φ → P pCnt A < P pCnt B
Assertion pcadd2 ⊢ φ → P pCnt A = P pCnt A + B

Proof

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