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 xaddridd ⊢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 xaddlid ⊢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 xaddlid ⊢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