Metamath Proof Explorer

Theorem xadddi2

Description: The assumption that the multiplier be real in xadddi can be relaxed if the addends have the same sign. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xadddi2 
|- ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A e. RR ) -> A e. RR )
2 simp2l 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> B e. RR* )
3 2 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A e. RR ) -> B e. RR* )
4 simp3l 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> C e. RR* )
5 4 ad2antrr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A e. RR ) -> C e. RR* )
6 xadddi 
 |-  ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A e. RR ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
8 pnfxr 
 |-  +oo e. RR*
9 4 adantr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> C e. RR* )
10 xmulcl 
 |-  ( ( +oo e. RR* /\ C e. RR* ) -> ( +oo *e C ) e. RR* )
11 8 9 10 sylancr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( +oo *e C ) e. RR* )
12 simpl3r 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> 0 <_ C )
13 0lepnf 
 |-  0 <_ +oo
14 xmulge0 
 |-  ( ( ( +oo e. RR* /\ 0 <_ +oo ) /\ ( C e. RR* /\ 0 <_ C ) ) -> 0 <_ ( +oo *e C ) )
15 8 13 14 mpanl12 
 |-  ( ( C e. RR* /\ 0 <_ C ) -> 0 <_ ( +oo *e C ) )
16 4 12 15 syl2an2r 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> 0 <_ ( +oo *e C ) )
17 ge0nemnf 
 |-  ( ( ( +oo *e C ) e. RR* /\ 0 <_ ( +oo *e C ) ) -> ( +oo *e C ) =/= -oo )
18 11 16 17 syl2anc 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( +oo *e C ) =/= -oo )
19 18 adantr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = +oo ) -> ( +oo *e C ) =/= -oo )
20 xaddpnf2 
 |-  ( ( ( +oo *e C ) e. RR* /\ ( +oo *e C ) =/= -oo ) -> ( +oo +e ( +oo *e C ) ) = +oo )
21 11 19 20 syl2an2r 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = +oo ) -> ( +oo +e ( +oo *e C ) ) = +oo )
22 oveq1 
 |-  ( A = +oo -> ( A *e B ) = ( +oo *e B ) )
23 oveq1 
 |-  ( A = +oo -> ( A *e C ) = ( +oo *e C ) )
24 22 23 oveq12d 
 |-  ( A = +oo -> ( ( A *e B ) +e ( A *e C ) ) = ( ( +oo *e B ) +e ( +oo *e C ) ) )
25 xmulpnf2 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( +oo *e B ) = +oo )
26 2 25 sylan 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( +oo *e B ) = +oo )
27 26 oveq1d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( ( +oo *e B ) +e ( +oo *e C ) ) = ( +oo +e ( +oo *e C ) ) )
28 24 27 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = +oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( +oo +e ( +oo *e C ) ) )
29 oveq1 
 |-  ( A = +oo -> ( A *e ( B +e C ) ) = ( +oo *e ( B +e C ) ) )
30 xaddcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B +e C ) e. RR* )
31 2 4 30 syl2anc 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( B +e C ) e. RR* )
32 0xr 
 |-  0 e. RR*
33 32 a1i 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> 0 e. RR* )
34 2 adantr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> B e. RR* )
35 31 adantr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( B +e C ) e. RR* )
36 simpr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> 0 < B )
37 34 xaddid1d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( B +e 0 ) = B )
38 xleadd2a 
 |-  ( ( ( 0 e. RR* /\ C e. RR* /\ B e. RR* ) /\ 0 <_ C ) -> ( B +e 0 ) <_ ( B +e C ) )
39 33 9 34 12 38 syl31anc 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( B +e 0 ) <_ ( B +e C ) )
40 37 39 eqbrtrrd 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> B <_ ( B +e C ) )
41 33 34 35 36 40 xrltletrd 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> 0 < ( B +e C ) )
42 xmulpnf2 
 |-  ( ( ( B +e C ) e. RR* /\ 0 < ( B +e C ) ) -> ( +oo *e ( B +e C ) ) = +oo )
43 31 41 42 syl2an2r 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( +oo *e ( B +e C ) ) = +oo )
44 29 43 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = +oo ) -> ( A *e ( B +e C ) ) = +oo )
45 21 28 44 3eqtr4rd 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = +oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
46 mnfxr 
 |-  -oo e. RR*
47 xmulcl 
 |-  ( ( -oo e. RR* /\ C e. RR* ) -> ( -oo *e C ) e. RR* )
48 46 9 47 sylancr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -oo *e C ) e. RR* )
49 xmulneg1 
 |-  ( ( -oo e. RR* /\ C e. RR* ) -> ( -e -oo *e C ) = -e ( -oo *e C ) )
50 46 9 49 sylancr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -e -oo *e C ) = -e ( -oo *e C ) )
51 xnegmnf 
 |-  -e -oo = +oo
52 51 oveq1i 
 |-  ( -e -oo *e C ) = ( +oo *e C )
53 50 52 eqtr3di 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> -e ( -oo *e C ) = ( +oo *e C ) )
54 xnegpnf 
 |-  -e +oo = -oo
55 54 a1i 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> -e +oo = -oo )
56 53 55 eqeq12d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -e ( -oo *e C ) = -e +oo <-> ( +oo *e C ) = -oo ) )
57 xneg11 
 |-  ( ( ( -oo *e C ) e. RR* /\ +oo e. RR* ) -> ( -e ( -oo *e C ) = -e +oo <-> ( -oo *e C ) = +oo ) )
58 48 8 57 sylancl 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -e ( -oo *e C ) = -e +oo <-> ( -oo *e C ) = +oo ) )
59 56 58 bitr3d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( ( +oo *e C ) = -oo <-> ( -oo *e C ) = +oo ) )
60 59 necon3bid 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( ( +oo *e C ) =/= -oo <-> ( -oo *e C ) =/= +oo ) )
61 18 60 mpbid 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -oo *e C ) =/= +oo )
62 xaddmnf2 
 |-  ( ( ( -oo *e C ) e. RR* /\ ( -oo *e C ) =/= +oo ) -> ( -oo +e ( -oo *e C ) ) = -oo )
63 48 61 62 syl2anc 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -oo +e ( -oo *e C ) ) = -oo )
64 63 adantr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = -oo ) -> ( -oo +e ( -oo *e C ) ) = -oo )
65 oveq1 
 |-  ( A = -oo -> ( A *e B ) = ( -oo *e B ) )
66 oveq1 
 |-  ( A = -oo -> ( A *e C ) = ( -oo *e C ) )
67 65 66 oveq12d 
 |-  ( A = -oo -> ( ( A *e B ) +e ( A *e C ) ) = ( ( -oo *e B ) +e ( -oo *e C ) ) )
68 xmulmnf2 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( -oo *e B ) = -oo )
69 2 68 sylan 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -oo *e B ) = -oo )
70 69 oveq1d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( ( -oo *e B ) +e ( -oo *e C ) ) = ( -oo +e ( -oo *e C ) ) )
71 67 70 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = -oo ) -> ( ( A *e B ) +e ( A *e C ) ) = ( -oo +e ( -oo *e C ) ) )
72 oveq1 
 |-  ( A = -oo -> ( A *e ( B +e C ) ) = ( -oo *e ( B +e C ) ) )
73 xmulmnf2 
 |-  ( ( ( B +e C ) e. RR* /\ 0 < ( B +e C ) ) -> ( -oo *e ( B +e C ) ) = -oo )
74 31 41 73 syl2an2r 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( -oo *e ( B +e C ) ) = -oo )
75 72 74 sylan9eqr 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = -oo ) -> ( A *e ( B +e C ) ) = -oo )
76 64 71 75 3eqtr4rd 
 |-  ( ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) /\ A = -oo ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
77 simpl1 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> A e. RR* )
78 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
79 77 78 sylib 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
80 7 45 76 79 mpjao3dan 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 < B ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
81 simp1 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> A e. RR* )
82 xmulcl 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A *e C ) e. RR* )
83 81 4 82 syl2anc 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A *e C ) e. RR* )
84 83 adantr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( A *e C ) e. RR* )
85 xaddid2 
 |-  ( ( A *e C ) e. RR* -> ( 0 +e ( A *e C ) ) = ( A *e C ) )
86 84 85 syl 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( 0 +e ( A *e C ) ) = ( A *e C ) )
87 oveq2 
 |-  ( 0 = B -> ( A *e 0 ) = ( A *e B ) )
88 87 eqcomd 
 |-  ( 0 = B -> ( A *e B ) = ( A *e 0 ) )
89 xmul01 
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )
90 89 3ad2ant1 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A *e 0 ) = 0 )
91 88 90 sylan9eqr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( A *e B ) = 0 )
92 91 oveq1d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( ( A *e B ) +e ( A *e C ) ) = ( 0 +e ( A *e C ) ) )
93 oveq1 
 |-  ( 0 = B -> ( 0 +e C ) = ( B +e C ) )
94 93 eqcomd 
 |-  ( 0 = B -> ( B +e C ) = ( 0 +e C ) )
95 xaddid2 
 |-  ( C e. RR* -> ( 0 +e C ) = C )
96 4 95 syl 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( 0 +e C ) = C )
97 94 96 sylan9eqr 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( B +e C ) = C )
98 97 oveq2d 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( A *e ( B +e C ) ) = ( A *e C ) )
99 86 92 98 3eqtr4rd 
 |-  ( ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) /\ 0 = B ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )
100 simp2r 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> 0 <_ B )
101 xrleloe 
 |-  ( ( 0 e. RR* /\ B e. RR* ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
102 32 2 101 sylancr 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
103 100 102 mpbid 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( 0 < B \/ 0 = B ) )
104 80 99 103 mpjaodan 
 |-  ( ( A e. RR* /\ ( B e. RR* /\ 0 <_ B ) /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A *e ( B +e C ) ) = ( ( A *e B ) +e ( A *e C ) ) )