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

Theorem suplesup 37637
Description: If any element of  A can be approximated from below by members of  B, then the supremum of  A is smaller or equal to the supremum of  B. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
suplesup.a  |-  ( ph  ->  A  C_  RR )
suplesup.b  |-  ( ph  ->  B  C_  RR* )
suplesup.c  |-  ( ph  ->  A. x  e.  A  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  < 
z )
Assertion
Ref Expression
suplesup  |-  ( ph  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
Distinct variable groups:    x, A, z    x, B, y, z    ph, x, z
Allowed substitution hints:    ph( y)    A( y)

Proof of Theorem suplesup
Dummy variables  r  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplesup.a . . . . . 6  |-  ( ph  ->  A  C_  RR )
2 ressxr 9715 . . . . . 6  |-  RR  C_  RR*
31, 2syl6ss 3456 . . . . 5  |-  ( ph  ->  A  C_  RR* )
4 supxrcl 11634 . . . . 5  |-  ( A 
C_  RR*  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
53, 4syl 17 . . . 4  |-  ( ph  ->  sup ( A ,  RR* ,  <  )  e. 
RR* )
65adantr 471 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
7 eqidd 2463 . . . 4  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  -> +oo  = +oo )
8 simpr 467 . . . 4  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  = +oo )
9 peano2re 9837 . . . . . . . . . 10  |-  ( w  e.  RR  ->  (
w  +  1 )  e.  RR )
109adantl 472 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  ( w  +  1 )  e.  RR )
113adantr 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  A  C_  RR* )
12 supxrunb2 11640 . . . . . . . . . . . 12  |-  ( A 
C_  RR*  ->  ( A. r  e.  RR  E. x  e.  A  r  <  x  <->  sup ( A ,  RR* ,  <  )  = +oo ) )
1311, 12syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( A. r  e.  RR  E. x  e.  A  r  <  x  <->  sup ( A ,  RR* ,  <  )  = +oo ) )
148, 13mpbird 240 . . . . . . . . . 10  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  A. r  e.  RR  E. x  e.  A  r  <  x )
1514adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  A. r  e.  RR  E. x  e.  A  r  <  x )
16 breq1 4421 . . . . . . . . . . 11  |-  ( r  =  ( w  + 
1 )  ->  (
r  <  x  <->  ( w  +  1 )  < 
x ) )
1716rexbidv 2913 . . . . . . . . . 10  |-  ( r  =  ( w  + 
1 )  ->  ( E. x  e.  A  r  <  x  <->  E. x  e.  A  ( w  +  1 )  < 
x ) )
1817rspcva 3160 . . . . . . . . 9  |-  ( ( ( w  +  1 )  e.  RR  /\  A. r  e.  RR  E. x  e.  A  r  <  x )  ->  E. x  e.  A  ( w  +  1 )  < 
x )
1910, 15, 18syl2anc 671 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  E. x  e.  A  ( w  +  1
)  <  x )
20 1rp 11340 . . . . . . . . . . . . . . . 16  |-  1  e.  RR+
2120a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  1  e.  RR+ )
22 suplesup.c . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. x  e.  A  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  < 
z )
2322r19.21bi 2769 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  <  z
)
24 oveq2 6328 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  1  ->  (
x  -  y )  =  ( x  - 
1 ) )
2524breq1d 4428 . . . . . . . . . . . . . . . . 17  |-  ( y  =  1  ->  (
( x  -  y
)  <  z  <->  ( x  -  1 )  < 
z ) )
2625rexbidv 2913 . . . . . . . . . . . . . . . 16  |-  ( y  =  1  ->  ( E. z  e.  B  ( x  -  y
)  <  z  <->  E. z  e.  B  ( x  -  1 )  < 
z ) )
2726rspcva 3160 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR+  /\  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  < 
z )  ->  E. z  e.  B  ( x  -  1 )  < 
z )
2821, 23, 27syl2anc 671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  E. z  e.  B  ( x  -  1 )  < 
z )
2928adantlr 726 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A )  ->  E. z  e.  B  ( x  -  1 )  < 
z )
30293adant3 1034 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  ->  E. z  e.  B  ( x  -  1
)  <  z )
31 nfv 1772 . . . . . . . . . . . . 13  |-  F/ z ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )
32 simp11r 1126 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  w  e.  RR )
332, 32sseldi 3442 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  w  e.  RR* )
341sselda 3444 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  RR )
35 1red 9689 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  1  e.  RR )
3634, 35resubcld 10080 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  (
x  -  1 )  e.  RR )
3736adantlr 726 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A )  ->  (
x  -  1 )  e.  RR )
38373adant3 1034 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
( x  -  1 )  e.  RR )
39383ad2ant1 1035 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  ( x  - 
1 )  e.  RR )
402, 39sseldi 3442 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  ( x  - 
1 )  e.  RR* )
41 suplesup.b . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  C_  RR* )
4241sselda 3444 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  z  e.  B )  ->  z  e.  RR* )
4342adantlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B )  ->  z  e.  RR* )
44433ad2antl1 1176 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B
)  ->  z  e.  RR* )
45443adant3 1034 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  z  e.  RR* )
46 simp3 1016 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
( w  +  1 )  <  x )
47 simp1r 1039 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  ->  w  e.  RR )
48 1red 9689 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
1  e.  RR )
4934adantlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A )  ->  x  e.  RR )
50493adant3 1034 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  ->  x  e.  RR )
5147, 48, 50ltaddsubd 10246 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
( ( w  + 
1 )  <  x  <->  w  <  ( x  - 
1 ) ) )
5246, 51mpbid 215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  ->  w  <  ( x  - 
1 ) )
53523ad2ant1 1035 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  w  <  (
x  -  1 ) )
54 simp3 1016 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  ( x  - 
1 )  <  z
)
5533, 40, 45, 53, 54xrlttrd 11490 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  ( w  +  1 )  <  x )  /\  z  e.  B  /\  ( x  -  1 )  <  z )  ->  w  <  z
)
56553exp 1214 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
( z  e.  B  ->  ( ( x  - 
1 )  <  z  ->  w  <  z ) ) )
5731, 56reximdai 2868 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  -> 
( E. z  e.  B  ( x  - 
1 )  <  z  ->  E. z  e.  B  w  <  z ) )
5830, 57mpd 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  w  e.  RR )  /\  x  e.  A  /\  (
w  +  1 )  <  x )  ->  E. z  e.  B  w  <  z )
59583exp 1214 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  RR )  ->  ( x  e.  A  ->  (
( w  +  1 )  <  x  ->  E. z  e.  B  w  <  z ) ) )
6059adantlr 726 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  ( x  e.  A  ->  ( ( w  + 
1 )  <  x  ->  E. z  e.  B  w  <  z ) ) )
6160rexlimdv 2889 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  ( E. x  e.  A  ( w  + 
1 )  <  x  ->  E. z  e.  B  w  <  z ) )
6219, 61mpd 15 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  E. z  e.  B  w  <  z )
632a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  C_  RR* )
6463sselda 3444 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  RR )  ->  w  e. 
RR* )
6564ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B
)  /\  w  <  z )  ->  w  e.  RR* )
6643adantr 471 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B
)  /\  w  <  z )  ->  z  e.  RR* )
67 simpr 467 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B
)  /\  w  <  z )  ->  w  <  z )
6865, 66, 67xrltled 37559 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B
)  /\  w  <  z )  ->  w  <_  z )
6968ex 440 . . . . . . . . 9  |-  ( ( ( ph  /\  w  e.  RR )  /\  z  e.  B )  ->  (
w  <  z  ->  w  <_  z ) )
7069adantllr 730 . . . . . . . 8  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  /\  z  e.  B
)  ->  ( w  <  z  ->  w  <_  z ) )
7170reximdva 2874 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  ( E. z  e.  B  w  <  z  ->  E. z  e.  B  w  <_  z ) )
7262, 71mpd 15 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  /\  w  e.  RR )  ->  E. z  e.  B  w  <_  z )
7372ralrimiva 2814 . . . . 5  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  A. w  e.  RR  E. z  e.  B  w  <_  z )
74 supxrunb1 11639 . . . . . . 7  |-  ( B 
C_  RR*  ->  ( A. w  e.  RR  E. z  e.  B  w  <_  z  <->  sup ( B ,  RR* ,  <  )  = +oo ) )
7541, 74syl 17 . . . . . 6  |-  ( ph  ->  ( A. w  e.  RR  E. z  e.  B  w  <_  z  <->  sup ( B ,  RR* ,  <  )  = +oo ) )
7675adantr 471 . . . . 5  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( A. w  e.  RR  E. z  e.  B  w  <_  z  <->  sup ( B ,  RR* ,  <  )  = +oo ) )
7773, 76mpbid 215 . . . 4  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( B ,  RR* ,  <  )  = +oo )
787, 8, 773eqtr4d 2506 . . 3  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  =  sup ( B ,  RR* ,  <  ) )
796, 78xreqled 37628 . 2  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
80 supeq1 7990 . . . . . . 7  |-  ( A  =  (/)  ->  sup ( A ,  RR* ,  <  )  =  sup ( (/) , 
RR* ,  <  ) )
81 xrsup0 11643 . . . . . . . 8  |-  sup ( (/)
,  RR* ,  <  )  = -oo
8281a1i 11 . . . . . . 7  |-  ( A  =  (/)  ->  sup ( (/)
,  RR* ,  <  )  = -oo )
8380, 82eqtrd 2496 . . . . . 6  |-  ( A  =  (/)  ->  sup ( A ,  RR* ,  <  )  = -oo )
8483adantl 472 . . . . 5  |-  ( (
ph  /\  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  = -oo )
85 supxrcl 11634 . . . . . . . 8  |-  ( B 
C_  RR*  ->  sup ( B ,  RR* ,  <  )  e.  RR* )
8641, 85syl 17 . . . . . . 7  |-  ( ph  ->  sup ( B ,  RR* ,  <  )  e. 
RR* )
87 mnfle 11469 . . . . . . 7  |-  ( sup ( B ,  RR* ,  <  )  e.  RR*  -> -oo  <_  sup ( B ,  RR* ,  <  ) )
8886, 87syl 17 . . . . . 6  |-  ( ph  -> -oo  <_  sup ( B ,  RR* ,  <  ) )
8988adantr 471 . . . . 5  |-  ( (
ph  /\  A  =  (/) )  -> -oo  <_  sup ( B ,  RR* ,  <  ) )
9084, 89eqbrtrd 4439 . . . 4  |-  ( (
ph  /\  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
9190adantlr 726 . . 3  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
92 simpll 765 . . . 4  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  ph )
931adantr 471 . . . . . . . 8  |-  ( (
ph  /\  -.  A  =  (/) )  ->  A  C_  RR )
94 neqne 2643 . . . . . . . . 9  |-  ( -.  A  =  (/)  ->  A  =/=  (/) )
9594adantl 472 . . . . . . . 8  |-  ( (
ph  /\  -.  A  =  (/) )  ->  A  =/=  (/) )
96 supxrgtmnf 11649 . . . . . . . 8  |-  ( ( A  C_  RR  /\  A  =/=  (/) )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
9793, 95, 96syl2anc 671 . . . . . . 7  |-  ( (
ph  /\  -.  A  =  (/) )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
9897adantlr 726 . . . . . 6  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  -> -oo  <  sup ( A ,  RR* ,  <  ) )
99 simpr 467 . . . . . . . . 9  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  sup ( A ,  RR* ,  <  )  = +oo )
100 simpl 463 . . . . . . . . . 10  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  ph )
101 nltpnft 11495 . . . . . . . . . 10  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  ->  ( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
102100, 5, 1013syl 18 . . . . . . . . 9  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  -> 
( sup ( A ,  RR* ,  <  )  = +oo  <->  -.  sup ( A ,  RR* ,  <  )  < +oo ) )
10399, 102mtbid 306 . . . . . . . 8  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  -.  -.  sup ( A ,  RR* ,  <  )  < +oo )
104 notnot2 117 . . . . . . . 8  |-  ( -. 
-.  sup ( A ,  RR* ,  <  )  < +oo  ->  sup ( A ,  RR* ,  <  )  < +oo )
105103, 104syl 17 . . . . . . 7  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  < +oo )
106105adantr 471 . . . . . 6  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  < +oo )
10798, 106jca 539 . . . . 5  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  ( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) )
10892, 5syl 17 . . . . . 6  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  e.  RR* )
109 xrrebnd 11497 . . . . . 6  |-  ( sup ( A ,  RR* ,  <  )  e.  RR*  ->  ( sup ( A ,  RR* ,  <  )  e.  RR  <->  ( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) ) )
110108, 109syl 17 . . . . 5  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  ( sup ( A ,  RR* ,  <  )  e.  RR  <->  ( -oo  <  sup ( A ,  RR* ,  <  )  /\  sup ( A ,  RR* ,  <  )  < +oo ) ) )
111107, 110mpbird 240 . . . 4  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
112 nfv 1772 . . . . 5  |-  F/ w
( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )
11341adantr 471 . . . . 5  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  B  C_  RR* )
114 simpr 467 . . . . 5  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
115114adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
116 simpr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  ->  w  e.  RR+ )
117116rphalfcld 11387 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( w  /  2
)  e.  RR+ )
118115, 117ltsubrpd 11404 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  <  sup ( A ,  RR* ,  <  ) )
1193ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  ->  A  C_  RR* )
120 rpre 11342 . . . . . . . . . . . 12  |-  ( w  e.  RR+  ->  w  e.  RR )
121 2re 10712 . . . . . . . . . . . . 13  |-  2  e.  RR
122121a1i 11 . . . . . . . . . . . 12  |-  ( w  e.  RR+  ->  2  e.  RR )
123 2ne0 10735 . . . . . . . . . . . . 13  |-  2  =/=  0
124123a1i 11 . . . . . . . . . . . 12  |-  ( w  e.  RR+  ->  2  =/=  0 )
125120, 122, 124redivcld 10468 . . . . . . . . . . 11  |-  ( w  e.  RR+  ->  ( w  /  2 )  e.  RR )
126125adantl 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( w  /  2
)  e.  RR )
127115, 126resubcld 10080 . . . . . . . . 9  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  e.  RR )
1282, 127sseldi 3442 . . . . . . . 8  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  e. 
RR* )
129 supxrlub 11645 . . . . . . . 8  |-  ( ( A  C_  RR*  /\  ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  e.  RR* )  ->  ( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  <  sup ( A ,  RR* ,  <  )  <->  E. x  e.  A  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x ) )
130119, 128, 129syl2anc 671 . . . . . . 7  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  <  sup ( A ,  RR* ,  <  )  <->  E. x  e.  A  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x ) )
131118, 130mpbid 215 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  ->  E. x  e.  A  ( sup ( A ,  RR* ,  <  )  -  ( w  /  2
) )  <  x
)
132 rphalfcl 11361 . . . . . . . . . . . 12  |-  ( w  e.  RR+  ->  ( w  /  2 )  e.  RR+ )
1331323ad2ant2 1036 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  RR+ 
/\  x  e.  A
)  ->  ( w  /  2 )  e.  RR+ )
134233adant2 1033 . . . . . . . . . . 11  |-  ( (
ph  /\  w  e.  RR+ 
/\  x  e.  A
)  ->  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  <  z
)
135 oveq2 6328 . . . . . . . . . . . . . 14  |-  ( y  =  ( w  / 
2 )  ->  (
x  -  y )  =  ( x  -  ( w  /  2
) ) )
136135breq1d 4428 . . . . . . . . . . . . 13  |-  ( y  =  ( w  / 
2 )  ->  (
( x  -  y
)  <  z  <->  ( x  -  ( w  / 
2 ) )  < 
z ) )
137136rexbidv 2913 . . . . . . . . . . . 12  |-  ( y  =  ( w  / 
2 )  ->  ( E. z  e.  B  ( x  -  y
)  <  z  <->  E. z  e.  B  ( x  -  ( w  / 
2 ) )  < 
z ) )
138137rspcva 3160 . . . . . . . . . . 11  |-  ( ( ( w  /  2
)  e.  RR+  /\  A. y  e.  RR+  E. z  e.  B  ( x  -  y )  < 
z )  ->  E. z  e.  B  ( x  -  ( w  / 
2 ) )  < 
z )
139133, 134, 138syl2anc 671 . . . . . . . . . 10  |-  ( (
ph  /\  w  e.  RR+ 
/\  x  e.  A
)  ->  E. z  e.  B  ( x  -  ( w  / 
2 ) )  < 
z )
140139ad5ant134 1263 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  <  x )  ->  E. z  e.  B  ( x  -  (
w  /  2 ) )  <  z )
141 recn 9660 . . . . . . . . . . . . . . . . . 18  |-  ( sup ( A ,  RR* ,  <  )  e.  RR  ->  sup ( A ,  RR* ,  <  )  e.  CC )
142141adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  sup ( A ,  RR* ,  <  )  e.  CC )
143120recnd 9700 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  RR+  ->  w  e.  CC )
144143adantl 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  w  e.  CC )
145144halfcld 10891 . . . . . . . . . . . . . . . . 17  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  ( w  /  2 )  e.  CC )
146142, 145, 145subsub4d 10048 . . . . . . . . . . . . . . . 16  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  ( ( sup ( A ,  RR* ,  <  )  -  ( w  /  2
) )  -  (
w  /  2 ) )  =  ( sup ( A ,  RR* ,  <  )  -  (
( w  /  2
)  +  ( w  /  2 ) ) ) )
1471432halvesd 10892 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  RR+  ->  ( ( w  /  2 )  +  ( w  / 
2 ) )  =  w )
148147oveq2d 6336 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  RR+  ->  ( sup ( A ,  RR* ,  <  )  -  (
( w  /  2
)  +  ( w  /  2 ) ) )  =  ( sup ( A ,  RR* ,  <  )  -  w
) )
149148adantl 472 . . . . . . . . . . . . . . . 16  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  ( sup ( A ,  RR* ,  <  )  -  (
( w  /  2
)  +  ( w  /  2 ) ) )  =  ( sup ( A ,  RR* ,  <  )  -  w
) )
150146, 149eqtr2d 2497 . . . . . . . . . . . . . . 15  |-  ( ( sup ( A ,  RR* ,  <  )  e.  RR  /\  w  e.  RR+ )  ->  ( sup ( A ,  RR* ,  <  )  -  w
)  =  ( ( sup ( A ,  RR* ,  <  )  -  ( w  /  2
) )  -  (
w  /  2 ) ) )
151150adantll 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( sup ( A ,  RR* ,  <  )  -  w )  =  ( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) ) )
152151adantr 471 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A
)  ->  ( sup ( A ,  RR* ,  <  )  -  w )  =  ( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) ) )
153152ad3antrrr 741 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( sup ( A ,  RR* ,  <  )  -  w )  =  ( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) ) )
154127, 126resubcld 10080 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) )  e.  RR )
155154adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A
)  ->  ( ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  -  ( w  /  2 ) )  e.  RR )
156155ad3antrrr 741 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) )  e.  RR )
1572, 156sseldi 3442 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) )  e.  RR* )
158120, 49sylanl2 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR+ )  /\  x  e.  A )  ->  x  e.  RR )
159125ad2antlr 738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  w  e.  RR+ )  /\  x  e.  A )  ->  (
w  /  2 )  e.  RR )
160158, 159resubcld 10080 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  w  e.  RR+ )  /\  x  e.  A )  ->  (
x  -  ( w  /  2 ) )  e.  RR )
161160adantllr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A
)  ->  ( x  -  ( w  / 
2 ) )  e.  RR )
162161ad3antrrr 741 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( x  -  (
w  /  2 ) )  e.  RR )
1632, 162sseldi 3442 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( x  -  (
w  /  2 ) )  e.  RR* )
164 simp-6l 785 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  ->  ph )
165 simplr 767 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
z  e.  B )
166164, 165, 42syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
z  e.  RR* )
167 simp-6r 786 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  ->  sup ( A ,  RR* ,  <  )  e.  RR )
168120ad5antlr 746 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  ->  w  e.  RR )
169168rehalfcld 10893 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( w  /  2
)  e.  RR )
170167, 169resubcld 10080 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  e.  RR )
171 simp-4r 782 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  ->  x  e.  A )
172164, 171, 34syl2anc 671 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  ->  x  e.  RR )
173 simpllr 774 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )
174170, 172, 169, 173ltsub1dd 10258 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) )  <  (
x  -  ( w  /  2 ) ) )
175 simpr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( x  -  (
w  /  2 ) )  <  z )
176157, 163, 166, 174, 175xrlttrd 11490 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  -  ( w  /  2
) )  <  z
)
177153, 176eqbrtrd 4439 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  /\  (
x  -  ( w  /  2 ) )  <  z )  -> 
( sup ( A ,  RR* ,  <  )  -  w )  <  z
)
178177ex 440 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x )  /\  z  e.  B )  ->  (
( x  -  (
w  /  2 ) )  <  z  -> 
( sup ( A ,  RR* ,  <  )  -  w )  <  z
) )
179178reximdva 2874 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  <  x )  ->  ( E. z  e.  B  ( x  -  ( w  / 
2 ) )  < 
z  ->  E. z  e.  B  ( sup ( A ,  RR* ,  <  )  -  w )  < 
z ) )
180140, 179mpd 15 . . . . . . . 8  |-  ( ( ( ( ( ph  /\ 
sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A )  /\  ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  <  x )  ->  E. z  e.  B  ( sup ( A ,  RR* ,  <  )  -  w )  <  z
)
181180ex 440 . . . . . . 7  |-  ( ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  /\  x  e.  A
)  ->  ( ( sup ( A ,  RR* ,  <  )  -  (
w  /  2 ) )  <  x  ->  E. z  e.  B  ( sup ( A ,  RR* ,  <  )  -  w )  <  z
) )
182181rexlimdva 2891 . . . . . 6  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  -> 
( E. x  e.  A  ( sup ( A ,  RR* ,  <  )  -  ( w  / 
2 ) )  < 
x  ->  E. z  e.  B  ( sup ( A ,  RR* ,  <  )  -  w )  < 
z ) )
183131, 182mpd 15 . . . . 5  |-  ( ( ( ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  /\  w  e.  RR+ )  ->  E. z  e.  B  ( sup ( A ,  RR* ,  <  )  -  w )  <  z
)
184112, 113, 114, 183supxrgere 37631 . . . 4  |-  ( (
ph  /\  sup ( A ,  RR* ,  <  )  e.  RR )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
18592, 111, 184syl2anc 671 . . 3  |-  ( ( ( ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  /\  -.  A  =  (/) )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
18691, 185pm2.61dan 805 . 2  |-  ( (
ph  /\  -.  sup ( A ,  RR* ,  <  )  = +oo )  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
18779, 186pm2.61dan 805 1  |-  ( ph  ->  sup ( A ,  RR* ,  <  )  <_  sup ( B ,  RR* ,  <  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750    C_ wss 3416   (/)c0 3743   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    / cdiv 10302   2c2 10692   RR+crp 11336
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-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-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-div 10303  df-2 10701  df-rp 11337
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator