Metamath Proof Explorer


Theorem xlesubadd

Description: Under certain conditions, the conclusion of lesubadd is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Assertion xlesubadd A * B * C * 0 A B −∞ 0 C A + 𝑒 B C A C + 𝑒 B

Proof

Step Hyp Ref Expression
1 simpl1 A * B * C * 0 A B −∞ 0 C A *
2 simpl2 A * B * C * 0 A B −∞ 0 C B *
3 xnegcl B * B *
4 2 3 syl A * B * C * 0 A B −∞ 0 C B *
5 xaddcl A * B * A + 𝑒 B *
6 1 4 5 syl2anc A * B * C * 0 A B −∞ 0 C A + 𝑒 B *
7 6 adantr A * B * C * 0 A B −∞ 0 C B A + 𝑒 B *
8 simpll3 A * B * C * 0 A B −∞ 0 C B C *
9 simpr A * B * C * 0 A B −∞ 0 C B B
10 xleadd1 A + 𝑒 B * C * B A + 𝑒 B C A + 𝑒 B + 𝑒 B C + 𝑒 B
11 7 8 9 10 syl3anc A * B * C * 0 A B −∞ 0 C B A + 𝑒 B C A + 𝑒 B + 𝑒 B C + 𝑒 B
12 xnpcan A * B A + 𝑒 B + 𝑒 B = A
13 1 12 sylan A * B * C * 0 A B −∞ 0 C B A + 𝑒 B + 𝑒 B = A
14 13 breq1d A * B * C * 0 A B −∞ 0 C B A + 𝑒 B + 𝑒 B C + 𝑒 B A C + 𝑒 B
15 11 14 bitrd A * B * C * 0 A B −∞ 0 C B A + 𝑒 B C A C + 𝑒 B
16 simpr3 A * B * C * 0 A B −∞ 0 C 0 C
17 oveq1 A = +∞ A + 𝑒 −∞ = +∞ + 𝑒 −∞
18 pnfaddmnf +∞ + 𝑒 −∞ = 0
19 17 18 eqtrdi A = +∞ A + 𝑒 −∞ = 0
20 19 breq1d A = +∞ A + 𝑒 −∞ C 0 C
21 16 20 syl5ibrcom A * B * C * 0 A B −∞ 0 C A = +∞ A + 𝑒 −∞ C
22 xaddmnf1 A * A +∞ A + 𝑒 −∞ = −∞
23 22 ex A * A +∞ A + 𝑒 −∞ = −∞
24 1 23 syl A * B * C * 0 A B −∞ 0 C A +∞ A + 𝑒 −∞ = −∞
25 simpl3 A * B * C * 0 A B −∞ 0 C C *
26 mnfle C * −∞ C
27 25 26 syl A * B * C * 0 A B −∞ 0 C −∞ C
28 breq1 A + 𝑒 −∞ = −∞ A + 𝑒 −∞ C −∞ C
29 27 28 syl5ibrcom A * B * C * 0 A B −∞ 0 C A + 𝑒 −∞ = −∞ A + 𝑒 −∞ C
30 24 29 syld A * B * C * 0 A B −∞ 0 C A +∞ A + 𝑒 −∞ C
31 21 30 pm2.61dne A * B * C * 0 A B −∞ 0 C A + 𝑒 −∞ C
32 pnfge A * A +∞
33 1 32 syl A * B * C * 0 A B −∞ 0 C A +∞
34 ge0nemnf C * 0 C C −∞
35 25 16 34 syl2anc A * B * C * 0 A B −∞ 0 C C −∞
36 xaddpnf1 C * C −∞ C + 𝑒 +∞ = +∞
37 25 35 36 syl2anc A * B * C * 0 A B −∞ 0 C C + 𝑒 +∞ = +∞
38 33 37 breqtrrd A * B * C * 0 A B −∞ 0 C A C + 𝑒 +∞
39 31 38 2thd A * B * C * 0 A B −∞ 0 C A + 𝑒 −∞ C A C + 𝑒 +∞
40 xnegeq B = +∞ B = +∞
41 xnegpnf +∞ = −∞
42 40 41 eqtrdi B = +∞ B = −∞
43 42 oveq2d B = +∞ A + 𝑒 B = A + 𝑒 −∞
44 43 breq1d B = +∞ A + 𝑒 B C A + 𝑒 −∞ C
45 oveq2 B = +∞ C + 𝑒 B = C + 𝑒 +∞
46 45 breq2d B = +∞ A C + 𝑒 B A C + 𝑒 +∞
47 44 46 bibi12d B = +∞ A + 𝑒 B C A C + 𝑒 B A + 𝑒 −∞ C A C + 𝑒 +∞
48 39 47 syl5ibrcom A * B * C * 0 A B −∞ 0 C B = +∞ A + 𝑒 B C A C + 𝑒 B
49 48 imp A * B * C * 0 A B −∞ 0 C B = +∞ A + 𝑒 B C A C + 𝑒 B
50 simpr2 A * B * C * 0 A B −∞ 0 C B −∞
51 2 50 jca A * B * C * 0 A B −∞ 0 C B * B −∞
52 xrnemnf B * B −∞ B B = +∞
53 51 52 sylib A * B * C * 0 A B −∞ 0 C B B = +∞
54 15 49 53 mpjaodan A * B * C * 0 A B −∞ 0 C A + 𝑒 B C A C + 𝑒 B