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 * B * 0 B C * 0 C A 𝑒 B + 𝑒 C = A 𝑒 B + 𝑒 A 𝑒 C

Proof

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