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 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
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 addid1d ⊢ ( 𝜑 → ( 𝐴 + 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 ( 𝐴 + 𝐵 ) ) )