This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> P e. Prime )
pcadd2.2 
|- ( ph -> A e. QQ )
pcadd2.3 
|- ( ph -> B e. QQ )
pcadd2.4 
|- ( ph -> ( P pCnt A ) < ( P pCnt B ) )
Assertion pcadd2 
|- ( ph -> ( P pCnt A ) = ( P pCnt ( A + B ) ) )

Proof

Step Hyp Ref Expression
1 pcadd2.1 
 |-  ( ph -> P e. Prime )
2 pcadd2.2 
 |-  ( ph -> A e. QQ )
3 pcadd2.3 
 |-  ( ph -> B e. QQ )
4 pcadd2.4 
 |-  ( ph -> ( P pCnt A ) < ( P pCnt B ) )
5 pcxcl 
 |-  ( ( P e. Prime /\ A e. QQ ) -> ( P pCnt A ) e. RR* )
6 1 2 5 syl2anc 
 |-  ( ph -> ( P pCnt A ) e. RR* )
7 qaddcl 
 |-  ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )
8 2 3 7 syl2anc 
 |-  ( ph -> ( A + B ) e. QQ )
9 pcxcl 
 |-  ( ( P e. Prime /\ ( A + B ) e. QQ ) -> ( P pCnt ( A + B ) ) e. RR* )
10 1 8 9 syl2anc 
 |-  ( ph -> ( P pCnt ( A + B ) ) e. RR* )
11 pcxcl 
 |-  ( ( P e. Prime /\ B e. QQ ) -> ( P pCnt B ) e. RR* )
12 1 3 11 syl2anc 
 |-  ( ph -> ( P pCnt B ) e. RR* )
13 6 12 4 xrltled 
 |-  ( ph -> ( P pCnt A ) <_ ( P pCnt B ) )
14 1 2 3 13 pcadd 
 |-  ( ph -> ( P pCnt A ) <_ ( P pCnt ( A + B ) ) )
15 qnegcl 
 |-  ( B e. QQ -> -u B e. QQ )
16 3 15 syl 
 |-  ( ph -> -u B e. QQ )
17 xrltnle 
 |-  ( ( ( P pCnt A ) e. RR* /\ ( P pCnt B ) e. RR* ) -> ( ( P pCnt A ) < ( P pCnt B ) <-> -. ( P pCnt B ) <_ ( P pCnt A ) ) )
18 6 12 17 syl2anc 
 |-  ( ph -> ( ( P pCnt A ) < ( P pCnt B ) <-> -. ( P pCnt B ) <_ ( P pCnt A ) ) )
19 4 18 mpbid 
 |-  ( ph -> -. ( P pCnt B ) <_ ( P pCnt A ) )
20 1 adantr 
 |-  ( ( ph /\ ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) -> P e. Prime )
21 16 adantr 
 |-  ( ( ph /\ ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) -> -u B e. QQ )
22 8 adantr 
 |-  ( ( ph /\ ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) -> ( A + B ) e. QQ )
23 pcneg 
 |-  ( ( P e. Prime /\ B e. QQ ) -> ( P pCnt -u B ) = ( P pCnt B ) )
24 1 3 23 syl2anc 
 |-  ( ph -> ( P pCnt -u B ) = ( P pCnt B ) )
25 24 breq1d 
 |-  ( ph -> ( ( P pCnt -u B ) <_ ( P pCnt ( A + B ) ) <-> ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) )
26 25 biimpar 
 |-  ( ( ph /\ ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) -> ( P pCnt -u B ) <_ ( P pCnt ( A + B ) ) )
27 20 21 22 26 pcadd 
 |-  ( ( ph /\ ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) -> ( P pCnt -u B ) <_ ( P pCnt ( -u B + ( A + B ) ) ) )
28 27 ex 
 |-  ( ph -> ( ( P pCnt B ) <_ ( P pCnt ( A + B ) ) -> ( P pCnt -u B ) <_ ( P pCnt ( -u B + ( A + B ) ) ) ) )
29 qcn 
 |-  ( B e. QQ -> B e. CC )
30 3 29 syl 
 |-  ( ph -> B e. CC )
31 30 negcld 
 |-  ( ph -> -u B e. CC )
32 qcn 
 |-  ( A e. QQ -> A e. CC )
33 2 32 syl 
 |-  ( ph -> A e. CC )
34 31 33 30 add12d 
 |-  ( ph -> ( -u B + ( A + B ) ) = ( A + ( -u B + B ) ) )
35 31 30 addcomd 
 |-  ( ph -> ( -u B + B ) = ( B + -u B ) )
36 30 negidd 
 |-  ( ph -> ( B + -u B ) = 0 )
37 35 36 eqtrd 
 |-  ( ph -> ( -u B + B ) = 0 )
38 37 oveq2d 
 |-  ( ph -> ( A + ( -u B + B ) ) = ( A + 0 ) )
39 33 addridd 
 |-  ( ph -> ( A + 0 ) = A )
40 34 38 39 3eqtrd 
 |-  ( ph -> ( -u B + ( A + B ) ) = A )
41 40 oveq2d 
 |-  ( ph -> ( P pCnt ( -u B + ( A + B ) ) ) = ( P pCnt A ) )
42 24 41 breq12d 
 |-  ( ph -> ( ( P pCnt -u B ) <_ ( P pCnt ( -u B + ( A + B ) ) ) <-> ( P pCnt B ) <_ ( P pCnt A ) ) )
43 28 42 sylibd 
 |-  ( ph -> ( ( P pCnt B ) <_ ( P pCnt ( A + B ) ) -> ( P pCnt B ) <_ ( P pCnt A ) ) )
44 19 43 mtod 
 |-  ( ph -> -. ( P pCnt B ) <_ ( P pCnt ( A + B ) ) )
45 xrltnle 
 |-  ( ( ( P pCnt ( A + B ) ) e. RR* /\ ( P pCnt B ) e. RR* ) -> ( ( P pCnt ( A + B ) ) < ( P pCnt B ) <-> -. ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) )
46 10 12 45 syl2anc 
 |-  ( ph -> ( ( P pCnt ( A + B ) ) < ( P pCnt B ) <-> -. ( P pCnt B ) <_ ( P pCnt ( A + B ) ) ) )
47 44 46 mpbird 
 |-  ( ph -> ( P pCnt ( A + B ) ) < ( P pCnt B ) )
48 10 12 47 xrltled 
 |-  ( ph -> ( P pCnt ( A + B ) ) <_ ( P pCnt B ) )
49 48 24 breqtrrd 
 |-  ( ph -> ( P pCnt ( A + B ) ) <_ ( P pCnt -u B ) )
50 1 8 16 49 pcadd 
 |-  ( ph -> ( P pCnt ( A + B ) ) <_ ( P pCnt ( ( A + B ) + -u B ) ) )
51 33 30 31 addassd 
 |-  ( ph -> ( ( A + B ) + -u B ) = ( A + ( B + -u B ) ) )
52 36 oveq2d 
 |-  ( ph -> ( A + ( B + -u B ) ) = ( A + 0 ) )
53 51 52 39 3eqtrd 
 |-  ( ph -> ( ( A + B ) + -u B ) = A )
54 53 oveq2d 
 |-  ( ph -> ( P pCnt ( ( A + B ) + -u B ) ) = ( P pCnt A ) )
55 50 54 breqtrd 
 |-  ( ph -> ( P pCnt ( A + B ) ) <_ ( P pCnt A ) )
56 6 10 14 55 xrletrid 
 |-  ( ph -> ( P pCnt A ) = ( P pCnt ( A + B ) ) )