This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xlt2addrd

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 
|- ( ph -> A e. RR )
xlt2addrd.2 
|- ( ph -> B e. RR* )
xlt2addrd.3 
|- ( ph -> C e. RR* )
xlt2addrd.4 
|- ( ph -> B =/= -oo )
xlt2addrd.5 
|- ( ph -> C =/= -oo )
xlt2addrd.6 
|- ( ph -> A < ( B +e C ) )
Assertion xlt2addrd 
|- ( ph -> E. b e. RR* E. c e. RR* ( A = ( b +e c ) /\ b < B /\ c < C ) )

Proof

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