# Metamath Proof Explorer

Description: If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017)

Ref Expression
Hypotheses xlt2addrd.1 ${⊢}{\phi }\to {A}\in ℝ$
xlt2addrd.2 ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
xlt2addrd.3 ${⊢}{\phi }\to {C}\in {ℝ}^{*}$
xlt2addrd.4 ${⊢}{\phi }\to {B}\ne \mathrm{-\infty }$
xlt2addrd.5 ${⊢}{\phi }\to {C}\ne \mathrm{-\infty }$
xlt2addrd.6 ${⊢}{\phi }\to {A}<{B}{+}_{𝑒}{C}$
Assertion xlt2addrd ${⊢}{\phi }\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$

### Proof

Step Hyp Ref Expression
1 xlt2addrd.1 ${⊢}{\phi }\to {A}\in ℝ$
2 xlt2addrd.2 ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
3 xlt2addrd.3 ${⊢}{\phi }\to {C}\in {ℝ}^{*}$
4 xlt2addrd.4 ${⊢}{\phi }\to {B}\ne \mathrm{-\infty }$
5 xlt2addrd.5 ${⊢}{\phi }\to {C}\ne \mathrm{-\infty }$
6 xlt2addrd.6 ${⊢}{\phi }\to {A}<{B}{+}_{𝑒}{C}$
7 1 rexrd ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
8 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}\in {ℝ}^{*}$
9 0xr ${⊢}0\in {ℝ}^{*}$
10 9 a1i ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to 0\in {ℝ}^{*}$
11 xaddid1 ${⊢}{A}\in {ℝ}^{*}\to {A}{+}_{𝑒}0={A}$
12 11 eqcomd ${⊢}{A}\in {ℝ}^{*}\to {A}={A}{+}_{𝑒}0$
13 8 12 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}={A}{+}_{𝑒}0$
14 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}\in ℝ$
15 ltpnf ${⊢}{A}\in ℝ\to {A}<\mathrm{+\infty }$
16 14 15 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}<\mathrm{+\infty }$
17 simplr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}=\mathrm{+\infty }$
18 16 17 breqtrrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}<{B}$
19 0ltpnf ${⊢}0<\mathrm{+\infty }$
20 simpr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {C}=\mathrm{+\infty }$
21 19 20 breqtrrid ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to 0<{C}$
22 oveq1 ${⊢}{b}={A}\to {b}{+}_{𝑒}{c}={A}{+}_{𝑒}{c}$
23 22 eqeq2d ${⊢}{b}={A}\to \left({A}={b}{+}_{𝑒}{c}↔{A}={A}{+}_{𝑒}{c}\right)$
24 breq1 ${⊢}{b}={A}\to \left({b}<{B}↔{A}<{B}\right)$
25 23 24 3anbi12d ${⊢}{b}={A}\to \left(\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)↔\left({A}={A}{+}_{𝑒}{c}\wedge {A}<{B}\wedge {c}<{C}\right)\right)$
26 oveq2 ${⊢}{c}=0\to {A}{+}_{𝑒}{c}={A}{+}_{𝑒}0$
27 26 eqeq2d ${⊢}{c}=0\to \left({A}={A}{+}_{𝑒}{c}↔{A}={A}{+}_{𝑒}0\right)$
28 breq1 ${⊢}{c}=0\to \left({c}<{C}↔0<{C}\right)$
29 27 28 3anbi13d ${⊢}{c}=0\to \left(\left({A}={A}{+}_{𝑒}{c}\wedge {A}<{B}\wedge {c}<{C}\right)↔\left({A}={A}{+}_{𝑒}0\wedge {A}<{B}\wedge 0<{C}\right)\right)$
30 25 29 rspc2ev ${⊢}\left({A}\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge \left({A}={A}{+}_{𝑒}0\wedge {A}<{B}\wedge 0<{C}\right)\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
31 8 10 13 18 21 30 syl113anc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
32 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}\in {ℝ}^{*}$
33 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\in {ℝ}^{*}$
34 1xr ${⊢}1\in {ℝ}^{*}$
35 34 a1i ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to 1\in {ℝ}^{*}$
36 35 xnegcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -1\in {ℝ}^{*}$
37 33 36 xaddcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}$
38 37 xnegcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -\left({C}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}$
39 32 38 xaddcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\in {ℝ}^{*}$
40 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}\in ℝ$
41 40 renemnfd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}\ne \mathrm{-\infty }$
42 xrnepnf ${⊢}\left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{+\infty }\right)↔\left({C}\in ℝ\vee {C}=\mathrm{-\infty }\right)$
43 42 biimpi ${⊢}\left({C}\in {ℝ}^{*}\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}\in ℝ\vee {C}=\mathrm{-\infty }\right)$
44 33 43 sylancom ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}\in ℝ\vee {C}=\mathrm{-\infty }\right)$
45 44 orcomd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}=\mathrm{-\infty }\vee {C}\in ℝ\right)$
46 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\ne \mathrm{-\infty }$
47 46 neneqd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to ¬{C}=\mathrm{-\infty }$
48 pm2.53 ${⊢}\left({C}=\mathrm{-\infty }\vee {C}\in ℝ\right)\to \left(¬{C}=\mathrm{-\infty }\to {C}\in ℝ\right)$
49 45 47 48 sylc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\in ℝ$
50 1re ${⊢}1\in ℝ$
51 rexsub ${⊢}\left({C}\in ℝ\wedge 1\in ℝ\right)\to {C}{+}_{𝑒}\left(-1\right)={C}-1$
52 49 50 51 sylancl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}{+}_{𝑒}\left(-1\right)={C}-1$
53 resubcl ${⊢}\left({C}\in ℝ\wedge 1\in ℝ\right)\to {C}-1\in ℝ$
54 49 50 53 sylancl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}-1\in ℝ$
55 52 54 eqeltrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}{+}_{𝑒}\left(-1\right)\in ℝ$
56 rexneg ${⊢}{C}{+}_{𝑒}\left(-1\right)\in ℝ\to -\left({C}{+}_{𝑒}\left(-1\right)\right)=-\left({C}{+}_{𝑒}\left(-1\right)\right)$
57 55 56 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -\left({C}{+}_{𝑒}\left(-1\right)\right)=-\left({C}{+}_{𝑒}\left(-1\right)\right)$
58 55 renegcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -\left({C}{+}_{𝑒}\left(-1\right)\right)\in ℝ$
59 57 58 eqeltrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -\left({C}{+}_{𝑒}\left(-1\right)\right)\in ℝ$
60 59 renemnfd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to -\left({C}{+}_{𝑒}\left(-1\right)\right)\ne \mathrm{-\infty }$
61 55 renemnfd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}{+}_{𝑒}\left(-1\right)\ne \mathrm{-\infty }$
62 xaddass ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}\wedge -\left({C}{+}_{𝑒}\left(-1\right)\right)\ne \mathrm{-\infty }\right)\wedge \left({C}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\wedge {C}{+}_{𝑒}\left(-1\right)\ne \mathrm{-\infty }\right)\right)\to \left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)={A}{+}_{𝑒}\left(\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\right)$
63 32 41 38 60 37 61 62 syl222anc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)={A}{+}_{𝑒}\left(\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\right)$
64 xaddcom ${⊢}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}\wedge {C}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\right)\to \left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)=\left({C}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)$
65 38 37 64 syl2anc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)=\left({C}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)$
66 xnegid ${⊢}{C}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\to \left({C}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)=0$
67 37 66 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)=0$
68 65 67 eqtrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)=0$
69 68 oveq2d ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\right)={A}{+}_{𝑒}0$
70 32 11 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}0={A}$
71 63 69 70 3eqtrrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)$
72 40 54 resubcld ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}-\left({C}-1\right)\in ℝ$
73 ltpnf ${⊢}{A}-\left({C}-1\right)\in ℝ\to {A}-\left({C}-1\right)<\mathrm{+\infty }$
74 72 73 syl ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}-\left({C}-1\right)<\mathrm{+\infty }$
75 rexsub ${⊢}\left({A}\in ℝ\wedge {C}{+}_{𝑒}\left(-1\right)\in ℝ\right)\to {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({C}{+}_{𝑒}\left(-1\right)\right)$
76 40 55 75 syl2anc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({C}{+}_{𝑒}\left(-1\right)\right)$
77 52 oveq2d ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}-\left({C}{+}_{𝑒}\left(-1\right)\right)={A}-\left({C}-1\right)$
78 76 77 eqtrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({C}-1\right)$
79 simplr ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}=\mathrm{+\infty }$
80 74 78 79 3brtr4d ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}$
81 49 ltm1d ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}-1<{C}$
82 52 81 eqbrtrd ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}{+}_{𝑒}\left(-1\right)<{C}$
83 oveq1 ${⊢}{b}={A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\to {b}{+}_{𝑒}{c}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}$
84 83 eqeq2d ${⊢}{b}={A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\to \left({A}={b}{+}_{𝑒}{c}↔{A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}\right)$
85 breq1 ${⊢}{b}={A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\to \left({b}<{B}↔{A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}\right)$
86 84 85 3anbi12d ${⊢}{b}={A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\to \left(\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)↔\left({A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}\wedge {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}\wedge {c}<{C}\right)\right)$
87 oveq2 ${⊢}{c}={C}{+}_{𝑒}\left(-1\right)\to \left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)$
88 87 eqeq2d ${⊢}{c}={C}{+}_{𝑒}\left(-1\right)\to \left({A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}↔{A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\right)$
89 breq1 ${⊢}{c}={C}{+}_{𝑒}\left(-1\right)\to \left({c}<{C}↔{C}{+}_{𝑒}\left(-1\right)<{C}\right)$
90 88 89 3anbi13d ${⊢}{c}={C}{+}_{𝑒}\left(-1\right)\to \left(\left({A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}{c}\wedge {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}\wedge {c}<{C}\right)↔\left({A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\wedge {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}\wedge {C}{+}_{𝑒}\left(-1\right)<{C}\right)\right)$
91 86 90 rspc2ev ${⊢}\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\in {ℝ}^{*}\wedge {C}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\wedge \left({A}=\left({A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({C}{+}_{𝑒}\left(-1\right)\right)\wedge {A}{+}_{𝑒}\left(-\left({C}{+}_{𝑒}\left(-1\right)\right)\right)<{B}\wedge {C}{+}_{𝑒}\left(-1\right)<{C}\right)\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
92 39 37 71 80 82 91 syl113anc ${⊢}\left(\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
93 31 92 pm2.61dane ${⊢}\left({\phi }\wedge {B}=\mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
94 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}\in {ℝ}^{*}$
95 34 a1i ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to 1\in {ℝ}^{*}$
96 95 xnegcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -1\in {ℝ}^{*}$
97 94 96 xaddcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}$
98 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}\in {ℝ}^{*}$
99 97 xnegcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -\left({B}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}$
100 98 99 xaddcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\in {ℝ}^{*}$
101 xaddcom ${⊢}\left({B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\wedge {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\in {ℝ}^{*}\right)\to \left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)=\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)$
102 97 100 101 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)=\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)$
103 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}\in ℝ$
104 103 renemnfd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}\ne \mathrm{-\infty }$
105 simplr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}\ne \mathrm{+\infty }$
106 xrnepnf ${⊢}\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{+\infty }\right)↔\left({B}\in ℝ\vee {B}=\mathrm{-\infty }\right)$
107 106 biimpi ${⊢}\left({B}\in {ℝ}^{*}\wedge {B}\ne \mathrm{+\infty }\right)\to \left({B}\in ℝ\vee {B}=\mathrm{-\infty }\right)$
108 94 105 107 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({B}\in ℝ\vee {B}=\mathrm{-\infty }\right)$
109 108 orcomd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({B}=\mathrm{-\infty }\vee {B}\in ℝ\right)$
110 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}\ne \mathrm{-\infty }$
111 110 neneqd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to ¬{B}=\mathrm{-\infty }$
112 pm2.53 ${⊢}\left({B}=\mathrm{-\infty }\vee {B}\in ℝ\right)\to \left(¬{B}=\mathrm{-\infty }\to {B}\in ℝ\right)$
113 109 111 112 sylc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}\in ℝ$
114 rexsub ${⊢}\left({B}\in ℝ\wedge 1\in ℝ\right)\to {B}{+}_{𝑒}\left(-1\right)={B}-1$
115 113 50 114 sylancl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}\left(-1\right)={B}-1$
116 resubcl ${⊢}\left({B}\in ℝ\wedge 1\in ℝ\right)\to {B}-1\in ℝ$
117 113 50 116 sylancl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}-1\in ℝ$
118 115 117 eqeltrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}\left(-1\right)\in ℝ$
119 rexneg ${⊢}{B}{+}_{𝑒}\left(-1\right)\in ℝ\to -\left({B}{+}_{𝑒}\left(-1\right)\right)=-\left({B}{+}_{𝑒}\left(-1\right)\right)$
120 118 119 syl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -\left({B}{+}_{𝑒}\left(-1\right)\right)=-\left({B}{+}_{𝑒}\left(-1\right)\right)$
121 118 renegcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -\left({B}{+}_{𝑒}\left(-1\right)\right)\in ℝ$
122 120 121 eqeltrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -\left({B}{+}_{𝑒}\left(-1\right)\right)\in ℝ$
123 122 renemnfd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to -\left({B}{+}_{𝑒}\left(-1\right)\right)\ne \mathrm{-\infty }$
124 118 renemnfd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}\left(-1\right)\ne \mathrm{-\infty }$
125 xaddass ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)\wedge \left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}\wedge -\left({B}{+}_{𝑒}\left(-1\right)\right)\ne \mathrm{-\infty }\right)\wedge \left({B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\wedge {B}{+}_{𝑒}\left(-1\right)\ne \mathrm{-\infty }\right)\right)\to \left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)={A}{+}_{𝑒}\left(\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)\right)$
126 98 104 99 123 97 124 125 syl222anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)={A}{+}_{𝑒}\left(\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)\right)$
127 xaddcom ${⊢}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\in {ℝ}^{*}\wedge {B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\right)\to \left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)$
128 99 97 127 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)$
129 xnegid ${⊢}{B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\to \left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)=0$
130 97 129 syl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)=0$
131 128 130 eqtrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)=0$
132 131 oveq2d ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)\right)={A}{+}_{𝑒}0$
133 98 11 syl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}0={A}$
134 132 133 eqtrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right){+}_{𝑒}\left({B}{+}_{𝑒}\left(-1\right)\right)\right)={A}$
135 102 126 134 3eqtrrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)$
136 113 ltm1d ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}-1<{B}$
137 115 136 eqbrtrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {B}{+}_{𝑒}\left(-1\right)<{B}$
138 103 117 resubcld ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}-\left({B}-1\right)\in ℝ$
139 ltpnf ${⊢}{A}-\left({B}-1\right)\in ℝ\to {A}-\left({B}-1\right)<\mathrm{+\infty }$
140 138 139 syl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}-\left({B}-1\right)<\mathrm{+\infty }$
141 rexsub ${⊢}\left({A}\in ℝ\wedge {B}{+}_{𝑒}\left(-1\right)\in ℝ\right)\to {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({B}{+}_{𝑒}\left(-1\right)\right)$
142 103 118 141 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({B}{+}_{𝑒}\left(-1\right)\right)$
143 115 oveq2d ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}-\left({B}{+}_{𝑒}\left(-1\right)\right)={A}-\left({B}-1\right)$
144 142 143 eqtrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)={A}-\left({B}-1\right)$
145 simpr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {C}=\mathrm{+\infty }$
146 140 144 145 3brtr4d ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)<{C}$
147 oveq1 ${⊢}{b}={B}{+}_{𝑒}\left(-1\right)\to {b}{+}_{𝑒}{c}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}$
148 147 eqeq2d ${⊢}{b}={B}{+}_{𝑒}\left(-1\right)\to \left({A}={b}{+}_{𝑒}{c}↔{A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}\right)$
149 breq1 ${⊢}{b}={B}{+}_{𝑒}\left(-1\right)\to \left({b}<{B}↔{B}{+}_{𝑒}\left(-1\right)<{B}\right)$
150 148 149 3anbi12d ${⊢}{b}={B}{+}_{𝑒}\left(-1\right)\to \left(\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)↔\left({A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}\wedge {B}{+}_{𝑒}\left(-1\right)<{B}\wedge {c}<{C}\right)\right)$
151 oveq2 ${⊢}{c}={A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\to \left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)$
152 151 eqeq2d ${⊢}{c}={A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\to \left({A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}↔{A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)\right)$
153 breq1 ${⊢}{c}={A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\to \left({c}<{C}↔{A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)<{C}\right)$
154 152 153 3anbi13d ${⊢}{c}={A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\to \left(\left({A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}{c}\wedge {B}{+}_{𝑒}\left(-1\right)<{B}\wedge {c}<{C}\right)↔\left({A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)\wedge {B}{+}_{𝑒}\left(-1\right)<{B}\wedge {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)<{C}\right)\right)$
155 150 154 rspc2ev ${⊢}\left({B}{+}_{𝑒}\left(-1\right)\in {ℝ}^{*}\wedge {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\in {ℝ}^{*}\wedge \left({A}=\left({B}{+}_{𝑒}\left(-1\right)\right){+}_{𝑒}\left({A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)\right)\wedge {B}{+}_{𝑒}\left(-1\right)<{B}\wedge {A}{+}_{𝑒}\left(-\left({B}{+}_{𝑒}\left(-1\right)\right)\right)<{C}\right)\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
156 97 100 135 137 146 155 syl113anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}=\mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
157 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}\in ℝ$
158 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}\in {ℝ}^{*}$
159 simplr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}\ne \mathrm{+\infty }$
160 158 159 107 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({B}\in ℝ\vee {B}=\mathrm{-\infty }\right)$
161 160 orcomd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({B}=\mathrm{-\infty }\vee {B}\in ℝ\right)$
162 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}\ne \mathrm{-\infty }$
163 162 neneqd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to ¬{B}=\mathrm{-\infty }$
164 161 163 112 sylc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}\in ℝ$
165 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\in {ℝ}^{*}$
166 165 43 sylancom ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}\in ℝ\vee {C}=\mathrm{-\infty }\right)$
167 166 orcomd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \left({C}=\mathrm{-\infty }\vee {C}\in ℝ\right)$
168 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\ne \mathrm{-\infty }$
169 168 neneqd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to ¬{C}=\mathrm{-\infty }$
170 167 169 48 sylc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {C}\in ℝ$
171 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}<{B}{+}_{𝑒}{C}$
172 rexadd ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
173 164 170 172 syl2anc ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
174 171 173 breqtrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to {A}<{B}+{C}$
175 157 164 170 174 lt2addrd ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}+{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
176 rexadd ${⊢}\left({b}\in ℝ\wedge {c}\in ℝ\right)\to {b}{+}_{𝑒}{c}={b}+{c}$
177 176 eqeq2d ${⊢}\left({b}\in ℝ\wedge {c}\in ℝ\right)\to \left({A}={b}{+}_{𝑒}{c}↔{A}={b}+{c}\right)$
178 177 3anbi1d ${⊢}\left({b}\in ℝ\wedge {c}\in ℝ\right)\to \left(\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)↔\left({A}={b}+{c}\wedge {b}<{B}\wedge {c}<{C}\right)\right)$
179 178 2rexbiia ${⊢}\exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)↔\exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}+{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
180 175 179 sylibr ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
181 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
182 ssrexv ${⊢}ℝ\subseteq {ℝ}^{*}\to \left(\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\to \exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\right)$
183 181 182 ax-mp ${⊢}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\to \exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
184 183 reximi ${⊢}\exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in ℝ\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
185 ssrexv ${⊢}ℝ\subseteq {ℝ}^{*}\to \left(\exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\right)$
186 181 185 ax-mp ${⊢}\exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
187 180 184 186 3syl ${⊢}\left(\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\wedge {C}\ne \mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
188 156 187 pm2.61dane ${⊢}\left({\phi }\wedge {B}\ne \mathrm{+\infty }\right)\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$
189 93 188 pm2.61dane ${⊢}{\phi }\to \exists {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\exists {c}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({A}={b}{+}_{𝑒}{c}\wedge {b}<{B}\wedge {c}<{C}\right)$