Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  supxrgelem Structured version   Visualization version   Unicode version

Theorem supxrgelem 37635
Description: If an extended real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
supxrgelem.xph  |-  F/ x ph
supxrgelem.a  |-  ( ph  ->  A  C_  RR* )
supxrgelem.b  |-  ( ph  ->  B  e.  RR* )
supxrgelem.y  |-  ( (
ph  /\  x  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e x ) )
Assertion
Ref Expression
supxrgelem  |-  ( ph  ->  B  <_  sup ( A ,  RR* ,  <  ) )
Distinct variable groups:    x, A, y    x, B, y    ph, y
Allowed substitution hint:    ph( x)

Proof of Theorem supxrgelem
StepHypRef Expression
1 supxrgelem.b . . . . 5  |-  ( ph  ->  B  e.  RR* )
2 pnfge 11466 . . . . 5  |-  ( B  e.  RR*  ->  B  <_ +oo )
31, 2syl 17 . . . 4  |-  ( ph  ->  B  <_ +oo )
43adantr 471 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_ +oo )
5 id 22 . . . . 5  |-  ( sup ( A ,  RR* ,  <  )  = +oo  ->  sup ( A ,  RR* ,  <  )  = +oo )
65eqcomd 2468 . . . 4  |-  ( sup ( A ,  RR* ,  <  )  = +oo  -> +oo  =  sup ( A ,  RR* ,  <  ) )
76adantl 472 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  -> +oo  =  sup ( A ,  RR* ,  <  ) )
84, 7breqtrd 4443 . 2  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
9 simpl 463 . . 3  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  ph )
10 1rp 11340 . . . . . . . 8  |-  1  e.  RR+
11 nfcv 2603 . . . . . . . . . 10  |-  F/_ x
1
12 supxrgelem.xph . . . . . . . . . . . 12  |-  F/ x ph
13 nfv 1772 . . . . . . . . . . . 12  |-  F/ x
1  e.  RR+
1412, 13nfan 2022 . . . . . . . . . . 11  |-  F/ x
( ph  /\  1  e.  RR+ )
15 nfv 1772 . . . . . . . . . . 11  |-  F/ x E. y  e.  A  B  <  ( y +e 1 )
1614, 15nfim 2014 . . . . . . . . . 10  |-  F/ x
( ( ph  /\  1  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e 1 ) )
17 eleq1 2528 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
x  e.  RR+  <->  1  e.  RR+ ) )
1817anbi2d 715 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
( ph  /\  x  e.  RR+ )  <->  ( ph  /\  1  e.  RR+ )
) )
19 oveq2 6328 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (
y +e x )  =  ( y +e 1 ) )
2019breq2d 4430 . . . . . . . . . . . 12  |-  ( x  =  1  ->  ( B  <  ( y +e x )  <->  B  <  ( y +e 1 ) ) )
2120rexbidv 2913 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( E. y  e.  A  B  <  ( y +e x )  <->  E. y  e.  A  B  <  ( y +e 1 ) ) )
2218, 21imbi12d 326 . . . . . . . . . 10  |-  ( x  =  1  ->  (
( ( ph  /\  x  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e x ) )  <-> 
( ( ph  /\  1  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e 1 ) ) ) )
23 supxrgelem.y . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e x ) )
2411, 16, 22, 23vtoclgf 3117 . . . . . . . . 9  |-  ( 1  e.  RR+  ->  ( (
ph  /\  1  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e 1 ) ) )
2510, 24ax-mp 5 . . . . . . . 8  |-  ( (
ph  /\  1  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e 1 ) )
2610, 25mpan2 682 . . . . . . 7  |-  ( ph  ->  E. y  e.  A  B  <  ( y +e 1 ) )
2726adantr 471 . . . . . 6  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  E. y  e.  A  B  <  ( y +e 1 ) )
28 mnfxr 11448 . . . . . . . . . . 11  |- -oo  e.  RR*
2928a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> -oo  e.  RR* )
30 supxrgelem.a . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  RR* )
3130sselda 3444 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  RR* )
32313adant3 1034 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  y  e.  RR* )
33 supxrcl 11634 . . . . . . . . . . . 12  |-  ( A 
C_  RR*  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
3430, 33syl 17 . . . . . . . . . . 11  |-  ( ph  ->  sup ( A ,  RR* ,  <  )  e. 
RR* )
35343ad2ant1 1035 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
36 simpl3 1019 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  B  <  ( y +e 1 ) )
37 simpr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  ->  -. -oo  <  y )
3831adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
y  e.  RR* )
39 ngtmnft 11496 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR*  ->  ( y  = -oo  <->  -. -oo  <  y ) )
4038, 39syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y  = -oo  <->  -. -oo 
<  y ) )
4137, 40mpbird 240 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
y  = -oo )
4241oveq1d 6335 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y +e 1 )  =  ( -oo +e 1 ) )
43 1re 9673 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
4443rexri 9724 . . . . . . . . . . . . . . . 16  |-  1  e.  RR*
4544a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
1  e.  RR* )
46 renepnf 9719 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  1  =/= +oo )
4743, 46ax-mp 5 . . . . . . . . . . . . . . . 16  |-  1  =/= +oo
4847a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
1  =/= +oo )
49 xaddmnf2 11556 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR*  /\  1  =/= +oo )  ->  ( -oo +e 1 )  = -oo )
5045, 48, 49syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( -oo +e 1 )  = -oo )
5142, 50eqtrd 2496 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y +e 1 )  = -oo )
52513adantl3 1172 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  ( y +e 1 )  = -oo )
5336, 52breqtrd 4443 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  B  < -oo )
54 nltmnf 11465 . . . . . . . . . . . . . 14  |-  ( B  e.  RR*  ->  -.  B  < -oo )
551, 54syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  B  < -oo )
5655adantr 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  -. -oo  <  y )  ->  -.  B  < -oo )
57563ad2antl1 1176 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  -.  B  < -oo )
5853, 57condan 808 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> -oo  <  y )
5930adantr 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  A  C_ 
RR* )
60 simpr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  A )
61 supxrub 11644 . . . . . . . . . . . 12  |-  ( ( A  C_  RR*  /\  y  e.  A )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
6259, 60, 61syl2anc 671 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
63623adant3 1034 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
6429, 32, 35, 58, 63xrltletrd 11492 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
65643exp 1214 . . . . . . . 8  |-  ( ph  ->  ( y  e.  A  ->  ( B  <  (
y +e 1 )  -> -oo  <  sup ( A ,  RR* ,  <  ) ) ) )
6665adantr 471 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( y  e.  A  ->  ( B  <  (
y +e 1 )  -> -oo  <  sup ( A ,  RR* ,  <  ) ) ) )
6766rexlimdv 2889 . . . . . 6  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( E. y  e.  A  B  <  (
y +e 1 )  -> -oo  <  sup ( A ,  RR* ,  <  ) ) )
6827, 67mpd 15 . . . . 5  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
69 simpr 467 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  sup ( A ,  RR* ,  <  )  = +oo )
70 nltpnft 11495 . . . . . . . . 9  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  ->  ( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
7134, 70syl 17 . . . . . . . 8  |-  ( ph  ->  ( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
7271adantr 471 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
7369, 72mtbid 306 . . . . . 6  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  -.  sup ( A ,  RR* ,  <  )  < +oo )
7473notnotrd 118 . . . . 5  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  < +oo )
7568, 74jca 539 . . . 4  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) )
7634adantr 471 . . . . 5  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
77 xrrebnd 11497 . . . . 5  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  ->  ( sup ( A ,  RR* ,  <  )  e.  RR  <->  ( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) ) )
7876, 77syl 17 . . . 4  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( sup ( A ,  RR* ,  <  )  e.  RR  <->  ( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) ) )
7975, 78mpbird 240 . . 3  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
80 simpl 463 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR ) )
81 simpr 467 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  -.  B  <_  sup ( A ,  RR* ,  <  ) )
8234adantr 471 . . . . . . . 8  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  sup ( A ,  RR* ,  <  )  e. 
RR* )
831adantr 471 . . . . . . . 8  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  B  e.  RR* )
84 xrltnle 9732 . . . . . . . 8  |-  ( ( sup ( A ,  RR* ,  <  )  e. 
RR*  /\  B  e.  RR* )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8582, 83, 84syl2anc 671 . . . . . . 7  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8685adantlr 726 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8781, 86mpbird 240 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  sup ( A ,  RR* ,  <  )  <  B )
88 simpll 765 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ph )
8928a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  -> -oo  e.  RR* )
9088, 34syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
9188, 1syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  RR* )
92 mnfle 11469 . . . . . . . . . . . . . 14  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
9334, 92syl 17 . . . . . . . . . . . . 13  |-  ( ph  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
9493ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
95 simpr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  sup ( A ,  RR* ,  <  )  <  B )
9689, 90, 91, 94, 95xrlelttrd 11491 . . . . . . . . . . 11  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  -> -oo  <  B
)
97 id 22 . . . . . . . . . . . . . 14  |-  ( ph  ->  ph )
9810a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  RR+ )
9997, 98, 25syl2anc 671 . . . . . . . . . . . . 13  |-  ( ph  ->  E. y  e.  A  B  <  ( y +e 1 ) )
10099ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  E. y  e.  A  B  <  ( y +e 1 ) )
10113ad2ant1 1035 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  B  e.  RR* )
10244a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  1  e.  RR* )
10332, 102jca 539 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  (
y  e.  RR*  /\  1  e.  RR* ) )
104 xaddcl 11564 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  RR*  /\  1  e.  RR* )  ->  (
y +e 1 )  e.  RR* )
105103, 104syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  (
y +e 1 )  e.  RR* )
106 pnfxr 11446 . . . . . . . . . . . . . . . . 17  |- +oo  e.  RR*
107106a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> +oo  e.  RR* )
108 simp3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  B  <  ( y +e 1 ) )
10931, 44, 104sylancl 673 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  A )  ->  (
y +e 1 )  e.  RR* )
110 pnfge 11466 . . . . . . . . . . . . . . . . . 18  |-  ( ( y +e 1 )  e.  RR*  ->  ( y +e 1 )  <_ +oo )
111109, 110syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A )  ->  (
y +e 1 )  <_ +oo )
1121113adant3 1034 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  (
y +e 1 )  <_ +oo )
113101, 105, 107, 108, 112xrltletrd 11492 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  B  < +oo )
1141133exp 1214 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  e.  A  ->  ( B  <  (
y +e 1 )  ->  B  < +oo ) ) )
115114rexlimdv 2889 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E. y  e.  A  B  <  (
y +e 1 )  ->  B  < +oo ) )
11688, 115syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( E. y  e.  A  B  <  ( y +e 1 )  ->  B  < +oo ) )
117100, 116mpd 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  < +oo )
11896, 117jca 539 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( -oo  <  B  /\  B  < +oo ) )
119 xrrebnd 11497 . . . . . . . . . . 11  |-  ( B  e.  RR*  ->  ( B  e.  RR  <->  ( -oo  <  B  /\  B  < +oo ) ) )
12091, 119syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  e.  RR  <->  ( -oo  <  B  /\  B  < +oo ) ) )
121118, 120mpbird 240 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  RR )
122 simpr 467 . . . . . . . . . 10  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
123122adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  sup ( A ,  RR* ,  <  )  e.  RR )
124121, 123resubcld 10080 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )
12526, 115mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  B  < +oo )
126125ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  < +oo )
12796, 126jca 539 . . . . . . . . . . 11  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( -oo  <  B  /\  B  < +oo ) )
128127, 120mpbird 240 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  RR )
129123, 128posdifd 10233 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  0  <  ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
13095, 129mpbid 215 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  0  <  ( B  -  sup ( A ,  RR* ,  <  ) ) )
131124, 130elrpd 11372 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
132 ovex 6348 . . . . . . . 8  |-  ( B  -  sup ( A ,  RR* ,  <  )
)  e.  _V
133 nfcv 2603 . . . . . . . . 9  |-  F/_ x
( B  -  sup ( A ,  RR* ,  <  ) )
134 nfv 1772 . . . . . . . . . . 11  |-  F/ x
( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+
13512, 134nfan 2022 . . . . . . . . . 10  |-  F/ x
( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
136 nfv 1772 . . . . . . . . . 10  |-  F/ x E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )
137135, 136nfim 2014 . . . . . . . . 9  |-  F/ x
( ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
138 eleq1 2528 . . . . . . . . . . 11  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( x  e.  RR+  <->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
)
139138anbi2d 715 . . . . . . . . . 10  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( ( ph  /\  x  e.  RR+ )  <->  ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
) )
140 oveq2 6328 . . . . . . . . . . . 12  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( y +e
x )  =  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
141140breq2d 4430 . . . . . . . . . . 11  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( B  <  (
y +e x )  <->  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) ) )
142141rexbidv 2913 . . . . . . . . . 10  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( E. y  e.  A  B  <  (
y +e x )  <->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) ) )
143139, 142imbi12d 326 . . . . . . . . 9  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( ( ( ph  /\  x  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e x ) )  <-> 
( ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) ) ) )
144133, 137, 143, 23vtoclgf 3117 . . . . . . . 8  |-  ( ( B  -  sup ( A ,  RR* ,  <  ) )  e.  _V  ->  ( ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) ) )
145132, 144ax-mp 5 . . . . . . 7  |-  ( (
ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
14688, 131, 145syl2anc 671 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
147 ltpnf 11456 . . . . . . . . . . . . 13  |-  ( sup ( A ,  RR* ,  <  )  e.  RR  ->  sup ( A ,  RR* ,  <  )  < +oo )
148147adantr 471 . . . . . . . . . . . 12  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < +oo )
149 id 22 . . . . . . . . . . . . . 14  |-  ( y  = +oo  ->  y  = +oo )
150149eqcomd 2468 . . . . . . . . . . . . 13  |-  ( y  = +oo  -> +oo  =  y )
151150adantl 472 . . . . . . . . . . . 12  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  -> +oo  =  y )
152148, 151breqtrd 4443 . . . . . . . . . . 11  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  <  y )
153152adantll 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < 
y )
154153ad5ant15 1253 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < 
y )
155 simplll 773 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B ) )
156 simpl 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -. -oo  <  y )  ->  ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) ) )
15788, 41sylanl1 660 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  /\  -. -oo  <  y
)  ->  y  = -oo )
158157adantlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -. -oo  <  y )  ->  y  = -oo )
159 simplr 767 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )
160 oveq1 6327 . . . . . . . . . . . . . . . . . 18  |-  ( y  = -oo  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( -oo +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
161160adantl 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( -oo +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
162128, 123resubcld 10080 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )
163162rexrd 9721 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR* )
164163ad3antrrr 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR* )
165 renepnf 9719 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  =/= +oo )
166124, 165syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  =/= +oo )
167166ad3antrrr 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  =/= +oo )
168 xaddmnf2 11556 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR*  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  =/= +oo )  ->  ( -oo +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  = -oo )
169164, 167, 168syl2anc 671 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  ( -oo +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  = -oo )
170161, 169eqtrd 2496 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  = -oo )
171159, 170breqtrd 4443 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  y  = -oo )  ->  B  < -oo )
172156, 158, 171syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -. -oo  <  y )  ->  B  < -oo )
17355ad5antr 745 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -. -oo  <  y )  ->  -.  B  < -oo )
174172, 173condan 808 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> -oo  <  y )
175174adantr 471 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  -> -oo  <  y )
176 simp3 1016 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  -.  y  = +oo )
177313adant3 1034 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  e.  RR* )
178 nltpnft 11495 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR*  ->  ( y  = +oo  <->  -.  y  < +oo ) )
179177, 178syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  (
y  = +oo  <->  -.  y  < +oo ) )
180176, 179mtbid 306 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  -.  -.  y  < +oo )
181180notnotrd 118 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  < +oo )
1821813adant1r 1269 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  < +oo )
183182ad5ant135 1264 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  y  < +oo )
184175, 183jca 539 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  ( -oo  <  y  /\  y  < +oo ) )
18531adantlr 726 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  e.  A )  ->  y  e.  RR* )
186185ad5ant13 1251 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  y  e.  RR* )
187 xrrebnd 11497 . . . . . . . . . . . 12  |-  ( y  e.  RR*  ->  ( y  e.  RR  <->  ( -oo  <  y  /\  y  < +oo ) ) )
188186, 187syl 17 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  ( y  e.  RR  <->  ( -oo  <  y  /\  y  < +oo ) ) )
189184, 188mpbird 240 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  y  e.  RR )
190 simplr 767 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  B  <  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
191121ad2antrr 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  ->  B  e.  RR )
192 simpr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  y  e.  RR )
193124adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )
194 rexadd 11559 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  RR  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )  ->  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( y  +  ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
195192, 193, 194syl2anc 671 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( y  +  ( B  -  sup ( A ,  RR* ,  <  )
) ) )
196192, 193readdcld 9701 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y  +  ( B  -  sup ( A ,  RR* ,  <  )
) )  e.  RR )
197195, 196eqeltrd 2540 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  e.  RR )
198197adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  e.  RR )
199 simpr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  ->  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
200191, 198, 191, 199ltsub1dd 10258 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( B  -  B
)  <  ( (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  -  B
) )
201121recnd 9700 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  CC )
202201subidd 10005 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  B )  =  0 )
203202ad2antrr 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( B  -  B
)  =  0 )
204192recnd 9700 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  y  e.  CC )
205201adantr 471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  B  e.  CC )
206122recnd 9700 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  CC )
207206ad2antrr 737 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  CC )
208204, 205, 207addsub12d 10040 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y  +  ( B  -  sup ( A ,  RR* ,  <  )
) )  =  ( B  +  ( y  -  sup ( A ,  RR* ,  <  )
) ) )
209195, 208eqtrd 2496 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( B  +  ( y  -  sup ( A ,  RR* ,  <  )
) ) )
210209oveq1d 6335 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  -  B
)  =  ( ( B  +  ( y  -  sup ( A ,  RR* ,  <  )
) )  -  B
) )
211204, 207subcld 10017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y  -  sup ( A ,  RR* ,  <  ) )  e.  CC )
212205, 211pncan2d 10019 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
( B  +  ( y  -  sup ( A ,  RR* ,  <  ) ) )  -  B
)  =  ( y  -  sup ( A ,  RR* ,  <  )
) )
213210, 212eqtrd 2496 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  -  B
)  =  ( y  -  sup ( A ,  RR* ,  <  )
) )
214213adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  -  B )  =  ( y  -  sup ( A ,  RR* ,  <  ) ) )
215203, 214breq12d 4431 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( ( B  -  B )  <  (
( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  -  B
)  <->  0  <  (
y  -  sup ( A ,  RR* ,  <  ) ) ) )
216200, 215mpbid 215 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
0  <  ( y  -  sup ( A ,  RR* ,  <  ) ) )
217123ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
218 simplr 767 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
y  e.  RR )
219217, 218posdifd 10233 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> 
( sup ( A ,  RR* ,  <  )  <  y  <->  0  <  (
y  -  sup ( A ,  RR* ,  <  ) ) ) )
220216, 219mpbird 240 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  ->  sup ( A ,  RR* ,  <  )  <  y
)
221155, 189, 190, 220syl21anc 1275 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  /\  y  e.  A )  /\  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) ) )  /\  -.  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < 
y )
222154, 221pm2.61dan 805 . . . . . . . 8  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  ->  sup ( A ,  RR* ,  <  )  <  y
)
223222ex 440 . . . . . . 7  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  ->  ( B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  ->  sup ( A ,  RR* ,  <  )  < 
y ) )
224223reximdva 2874 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( E. y  e.  A  B  <  ( y +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  ->  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y ) )
225146, 224mpd 15 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
22680, 87, 225syl2anc 671 . . . 4  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
22759, 33syl 17 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  A )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
22831, 227xrlenltd 9731 . . . . . . . 8  |-  ( (
ph  /\  y  e.  A )  ->  (
y  <_  sup ( A ,  RR* ,  <  )  <->  -.  sup ( A ,  RR* ,  <  )  < 
y ) )
22962, 228mpbid 215 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  -.  sup ( A ,  RR* ,  <  )  <  y
)
230229ralrimiva 2814 . . . . . 6  |-  ( ph  ->  A. y  e.  A  -.  sup ( A ,  RR* ,  <  )  < 
y )
231 ralnex 2846 . . . . . 6  |-  ( A. y  e.  A  -.  sup ( A ,  RR* ,  <  )  <  y  <->  -. 
E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y
)
232230, 231sylib 201 . . . . 5  |-  ( ph  ->  -.  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
233232ad2antrr 737 . . . 4  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  -.  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
234226, 233condan 808 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
2359, 79, 234syl2anc 671 . 2  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
2368, 235pm2.61dan 805 1  |-  ( ph  ->  B  <_  sup ( A ,  RR* ,  <  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455   F/wnf 1678    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057    C_ wss 3416   class class class wbr 4418  (class class class)co 6320   supcsup 7985   CCcc 9568   RRcr 9569   0cc0 9570   1c1 9571    + caddc 9573   +oocpnf 9703   -oocmnf 9704   RR*cxr 9705    < clt 9706    <_ cle 9707    - cmin 9891   RR+crp 11336   +ecxad 11441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-pre-sup 9648
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-po 4777  df-so 4778  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-sup 7987  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-rp 11337  df-xadd 11444
This theorem is referenced by:  supxrge  37636
  Copyright terms: Public domain W3C validator