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

Theorem supxrgelem 37514
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 11439 . . . . 5  |-  ( B  e.  RR*  ->  B  <_ +oo )
31, 2syl 17 . . . 4  |-  ( ph  ->  B  <_ +oo )
43adantr 466 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_ +oo )
5 id 22 . . . . 5  |-  ( sup ( A ,  RR* ,  <  )  = +oo  ->  sup ( A ,  RR* ,  <  )  = +oo )
65eqcomd 2430 . . . 4  |-  ( sup ( A ,  RR* ,  <  )  = +oo  -> +oo  =  sup ( A ,  RR* ,  <  ) )
76adantl 467 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  -> +oo  =  sup ( A ,  RR* ,  <  ) )
84, 7breqtrd 4448 . 2  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
9 simpl 458 . . 3  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  ph )
10 1rp 11313 . . . . . . . 8  |-  1  e.  RR+
11 nfcv 2580 . . . . . . . . . 10  |-  F/_ x
1
12 supxrgelem.xph . . . . . . . . . . . 12  |-  F/ x ph
13 nfv 1755 . . . . . . . . . . . 12  |-  F/ x
1  e.  RR+
1412, 13nfan 1988 . . . . . . . . . . 11  |-  F/ x
( ph  /\  1  e.  RR+ )
15 nfv 1755 . . . . . . . . . . 11  |-  F/ x E. y  e.  A  B  <  ( y +e 1 )
1614, 15nfim 1980 . . . . . . . . . 10  |-  F/ x
( ( ph  /\  1  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e 1 ) )
17 eleq1 2495 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
x  e.  RR+  <->  1  e.  RR+ ) )
1817anbi2d 708 . . . . . . . . . . 11  |-  ( x  =  1  ->  (
( ph  /\  x  e.  RR+ )  <->  ( ph  /\  1  e.  RR+ )
) )
19 oveq2 6313 . . . . . . . . . . . . 13  |-  ( x  =  1  ->  (
y +e x )  =  ( y +e 1 ) )
2019breq2d 4435 . . . . . . . . . . . 12  |-  ( x  =  1  ->  ( B  <  ( y +e x )  <->  B  <  ( y +e 1 ) ) )
2120rexbidv 2936 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( E. y  e.  A  B  <  ( y +e x )  <->  E. y  e.  A  B  <  ( y +e 1 ) ) )
2218, 21imbi12d 321 . . . . . . . . . 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 3137 . . . . . . . . 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 675 . . . . . . 7  |-  ( ph  ->  E. y  e.  A  B  <  ( y +e 1 ) )
2726adantr 466 . . . . . 6  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  E. y  e.  A  B  <  ( y +e 1 ) )
28 mnfxr 11421 . . . . . . . . . . 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 3464 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  RR* )
32313adant3 1025 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  y  e.  RR* )
33 supxrcl 11607 . . . . . . . . . . . 12  |-  ( A 
C_  RR*  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
3430, 33syl 17 . . . . . . . . . . 11  |-  ( ph  ->  sup ( A ,  RR* ,  <  )  e. 
RR* )
35343ad2ant1 1026 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
36 simpl3 1010 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  B  <  ( y +e 1 ) )
37 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  ->  -. -oo  <  y )
3831adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
y  e.  RR* )
39 ngtmnft 11469 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR*  ->  ( y  = -oo  <->  -. -oo  <  y ) )
4038, 39syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y  = -oo  <->  -. -oo 
<  y ) )
4137, 40mpbird 235 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
y  = -oo )
4241oveq1d 6320 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y +e 1 )  =  ( -oo +e 1 ) )
43 1re 9649 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
4443rexri 9700 . . . . . . . . . . . . . . . 16  |-  1  e.  RR*
4544a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
1  e.  RR* )
46 renepnf 9695 . . . . . . . . . . . . . . . . 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 11529 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR*  /\  1  =/= +oo )  ->  ( -oo +e 1 )  = -oo )
5045, 48, 49syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( -oo +e 1 )  = -oo )
5142, 50eqtrd 2463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  A )  /\  -. -oo 
<  y )  -> 
( y +e 1 )  = -oo )
52513adantl3 1163 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  ( y +e 1 )  = -oo )
5336, 52breqtrd 4448 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  B  < -oo )
54 nltmnf 11438 . . . . . . . . . . . . . 14  |-  ( B  e.  RR*  ->  -.  B  < -oo )
551, 54syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  B  < -oo )
5655adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  -. -oo  <  y )  ->  -.  B  < -oo )
57563ad2antl1 1167 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  A  /\  B  < 
( y +e 1 ) )  /\  -. -oo  <  y )  ->  -.  B  < -oo )
5853, 57condan 801 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> -oo  <  y )
5930adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  A  C_ 
RR* )
60 simpr 462 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  A )
61 supxrub 11617 . . . . . . . . . . . 12  |-  ( ( A  C_  RR*  /\  y  e.  A )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
6259, 60, 61syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
63623adant3 1025 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  y  <_  sup ( A ,  RR* ,  <  ) )
6429, 32, 35, 58, 63xrltletrd 11465 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
65643exp 1204 . . . . . . . 8  |-  ( ph  ->  ( y  e.  A  ->  ( B  <  (
y +e 1 )  -> -oo  <  sup ( A ,  RR* ,  <  ) ) ) )
6665adantr 466 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( y  e.  A  ->  ( B  <  (
y +e 1 )  -> -oo  <  sup ( A ,  RR* ,  <  ) ) ) )
6766rexlimdv 2912 . . . . . 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 462 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  sup ( A ,  RR* ,  <  )  = +oo )
70 nltpnft 11468 . . . . . . . . 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 466 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
7369, 72mtbid 301 . . . . . 6  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  -.  sup ( A ,  RR* ,  <  )  < +oo )
7473notnotrd 116 . . . . 5  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  < +oo )
7568, 74jca 534 . . . 4  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) )
7634adantr 466 . . . . 5  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
77 xrrebnd 11470 . . . . 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 235 . . 3  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
80 simpl 458 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR ) )
81 simpr 462 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  -.  B  <_  sup ( A ,  RR* ,  <  ) )
8234adantr 466 . . . . . . . 8  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  sup ( A ,  RR* ,  <  )  e. 
RR* )
831adantr 466 . . . . . . . 8  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  B  e.  RR* )
84 xrltnle 9708 . . . . . . . 8  |-  ( ( sup ( A ,  RR* ,  <  )  e. 
RR*  /\  B  e.  RR* )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8582, 83, 84syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8685adantlr 719 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  -.  B  <_  sup ( A ,  RR* ,  <  ) ) )
8781, 86mpbird 235 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  sup ( A ,  RR* ,  <  )  <  B )
88 simpll 758 . . . . . . 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 11442 . . . . . . . . . . . . . 14  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
9334, 92syl 17 . . . . . . . . . . . . 13  |-  ( ph  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
9493ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  -> -oo  <_  sup ( A ,  RR* ,  <  ) )
95 simpr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  sup ( A ,  RR* ,  <  )  <  B )
9689, 90, 91, 94, 95xrlelttrd 11464 . . . . . . . . . . 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 665 . . . . . . . . . . . . 13  |-  ( ph  ->  E. y  e.  A  B  <  ( y +e 1 ) )
10099ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  E. y  e.  A  B  <  ( y +e 1 ) )
10113ad2ant1 1026 . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  (
y  e.  RR*  /\  1  e.  RR* ) )
104 xaddcl 11537 . . . . . . . . . . . . . . . . 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 11419 . . . . . . . . . . . . . . . . 17  |- +oo  e.  RR*
107106a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  -> +oo  e.  RR* )
108 simp3 1007 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  B  <  ( y +e 1 ) )
10931, 44, 104sylancl 666 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  A )  ->  (
y +e 1 )  e.  RR* )
110 pnfge 11439 . . . . . . . . . . . . . . . . . 18  |-  ( ( y +e 1 )  e.  RR*  ->  ( y +e 1 )  <_ +oo )
111109, 110syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A )  ->  (
y +e 1 )  <_ +oo )
1121113adant3 1025 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  (
y +e 1 )  <_ +oo )
113101, 105, 107, 108, 112xrltletrd 11465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A  /\  B  <  (
y +e 1 ) )  ->  B  < +oo )
1141133exp 1204 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  e.  A  ->  ( B  <  (
y +e 1 )  ->  B  < +oo ) ) )
115114rexlimdv 2912 . . . . . . . . . . . . 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 534 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( -oo  <  B  /\  B  < +oo ) )
119 xrrebnd 11470 . . . . . . . . . . 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 235 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  RR )
122 simpr 462 . . . . . . . . . 10  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
123122adantr 466 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  sup ( A ,  RR* ,  <  )  e.  RR )
124121, 123resubcld 10054 . . . . . . . 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 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  < +oo )
12796, 126jca 534 . . . . . . . . . . 11  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( -oo  <  B  /\  B  < +oo ) )
128127, 120mpbird 235 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  RR )
129123, 128posdifd 10207 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( sup ( A ,  RR* ,  <  )  <  B  <->  0  <  ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
13095, 129mpbid 213 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  0  <  ( B  -  sup ( A ,  RR* ,  <  ) ) )
131124, 130elrpd 11345 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
132 ovex 6333 . . . . . . . 8  |-  ( B  -  sup ( A ,  RR* ,  <  )
)  e.  _V
133 nfcv 2580 . . . . . . . . 9  |-  F/_ x
( B  -  sup ( A ,  RR* ,  <  ) )
134 nfv 1755 . . . . . . . . . . 11  |-  F/ x
( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+
13512, 134nfan 1988 . . . . . . . . . 10  |-  F/ x
( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
136 nfv 1755 . . . . . . . . . 10  |-  F/ x E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )
137135, 136nfim 1980 . . . . . . . . 9  |-  F/ x
( ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
138 eleq1 2495 . . . . . . . . . . 11  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( x  e.  RR+  <->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
)
139138anbi2d 708 . . . . . . . . . 10  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( ( ph  /\  x  e.  RR+ )  <->  ( ph  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR+ )
) )
140 oveq2 6313 . . . . . . . . . . . 12  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( y +e
x )  =  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
141140breq2d 4435 . . . . . . . . . . 11  |-  ( x  =  ( B  -  sup ( A ,  RR* ,  <  ) )  -> 
( B  <  (
y +e x )  <->  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) ) )
142141rexbidv 2936 . . . . . . . . . 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 321 . . . . . . . . 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 3137 . . . . . . . 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 665 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  E. y  e.  A  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
147 ltpnf 11429 . . . . . . . . . . . . 13  |-  ( sup ( A ,  RR* ,  <  )  e.  RR  ->  sup ( A ,  RR* ,  <  )  < +oo )
148147adantr 466 . . . . . . . . . . . 12  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < +oo )
149 id 22 . . . . . . . . . . . . . 14  |-  ( y  = +oo  ->  y  = +oo )
150149eqcomd 2430 . . . . . . . . . . . . 13  |-  ( y  = +oo  -> +oo  =  y )
151150adantl 467 . . . . . . . . . . . 12  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  -> +oo  =  y )
152148, 151breqtrd 4448 . . . . . . . . . . 11  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  <  y )
153152adantll 718 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  = +oo )  ->  sup ( A ,  RR* ,  <  )  < 
y )
154153ad5ant15 1241 . . . . . . . . 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 766 . . . . . . . . . 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 458 . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  /\  -. -oo  <  y
)  ->  y  = -oo )
158157adantlr 719 . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . 18  |-  ( y  = -oo  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( -oo +e ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
161160adantl 467 . . . . . . . . . . . . . . . . 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 10054 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )
163162rexrd 9697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR* )
164163ad3antrrr 734 . . . . . . . . . . . . . . . . . 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 9695 . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . 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 11529 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR*  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  =/= +oo )  ->  ( -oo +e
( B  -  sup ( A ,  RR* ,  <  ) ) )  = -oo )
169164, 167, 168syl2anc 665 . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . 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 4448 . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . 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 801 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  A )  /\  B  <  ( y +e ( B  -  sup ( A ,  RR* ,  <  )
) ) )  -> -oo  <  y )
175174adantr 466 . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  -.  y  = +oo )
177313adant3 1025 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  e.  RR* )
178 nltpnft 11468 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  RR*  ->  ( y  = +oo  <->  -.  y  < +oo ) )
179177, 178syl 17 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  (
y  = +oo  <->  -.  y  < +oo ) )
180176, 179mtbid 301 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  -.  -.  y  < +oo )
181180notnotrd 116 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  < +oo )
1821813adant1r 1257 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  e.  A  /\  -.  y  = +oo )  ->  y  < +oo )
183182ad5ant135 1252 . . . . . . . . . . . 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 534 . . . . . . . . . . 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 719 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  y  e.  A )  ->  y  e.  RR* )
186185ad5ant13 1239 . . . . . . . . . . . 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 11470 . . . . . . . . . . . 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 235 . . . . . . . . . 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 760 . . . . . . . . . 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 730 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  y  e.  RR )
193124adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )
194 rexadd 11532 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  RR  /\  ( B  -  sup ( A ,  RR* ,  <  ) )  e.  RR )  ->  ( y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  =  ( y  +  ( B  -  sup ( A ,  RR* ,  <  ) ) ) )
195192, 193, 194syl2anc 665 . . . . . . . . . . . . . . 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 9677 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y  +  ( B  -  sup ( A ,  RR* ,  <  )
) )  e.  RR )
197195, 196eqeltrd 2507 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y +e ( B  -  sup ( A ,  RR* ,  <  ) ) )  e.  RR )
198197adantr 466 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 10232 . . . . . . . . . . . 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 9676 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  B  e.  CC )
202201subidd 9981 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B
)  ->  ( B  -  B )  =  0 )
203202ad2antrr 730 . . . . . . . . . . . . 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 9676 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  y  e.  CC )
205201adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  B  e.  CC )
206122recnd 9676 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  CC )
207206ad2antrr 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  CC )
208204, 205, 207addsub12d 10016 . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . 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 6320 . . . . . . . . . . . . . . 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 9993 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  sup ( A ,  RR* ,  <  )  <  B )  /\  y  e.  RR )  ->  (
y  -  sup ( A ,  RR* ,  <  ) )  e.  CC )
212205, 211pncan2d 9995 . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . 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 4436 . . . . . . . . . . . 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 213 . . . . . . . . . . 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 730 . . . . . . . . . . . 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 760 . . . . . . . . . . . 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 10207 . . . . . . . . . . 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 235 . . . . . . . . . 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 1263 . . . . . . . . 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 798 . . . . . . . 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 435 . . . . . . 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 2897 . . . . . 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 665 . . . 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 9707 . . . . . . . 8  |-  ( (
ph  /\  y  e.  A )  ->  (
y  <_  sup ( A ,  RR* ,  <  )  <->  -.  sup ( A ,  RR* ,  <  )  < 
y ) )
22962, 228mpbid 213 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  -.  sup ( A ,  RR* ,  <  )  <  y
)
230229ralrimiva 2836 . . . . . 6  |-  ( ph  ->  A. y  e.  A  -.  sup ( A ,  RR* ,  <  )  < 
y )
231 ralnex 2868 . . . . . 6  |-  ( A. y  e.  A  -.  sup ( A ,  RR* ,  <  )  <  y  <->  -. 
E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y
)
232230, 231sylib 199 . . . . 5  |-  ( ph  ->  -.  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
233232ad2antrr 730 . . . 4  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  -.  B  <_  sup ( A ,  RR* ,  <  ) )  ->  -.  E. y  e.  A  sup ( A ,  RR* ,  <  )  <  y )
234226, 233condan 801 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
2359, 79, 234syl2anc 665 . 2  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  B  <_  sup ( A ,  RR* ,  <  ) )
2368, 235pm2.61dan 798 1  |-  ( ph  ->  B  <_  sup ( A ,  RR* ,  <  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   F/wnf 1661    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080    C_ wss 3436   class class class wbr 4423  (class class class)co 6305   supcsup 7963   CCcc 9544   RRcr 9545   0cc0 9546   1c1 9547    + caddc 9549   +oocpnf 9679   -oocmnf 9680   RR*cxr 9681    < clt 9682    <_ cle 9683    - cmin 9867   RR+crp 11309   +ecxad 11414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-sup 7965  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-rp 11310  df-xadd 11417
This theorem is referenced by:  supxrge  37515
  Copyright terms: Public domain W3C validator