Metamath Proof Explorer

Theorem suplesup

Description: If any element of A can be approximated from below by members of B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses 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 suplesup 
|- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )

Proof

Step Hyp Ref Expression
1 suplesup.a 
 |-  ( ph -> A C_ RR )
2 suplesup.b 
 |-  ( ph -> B C_ RR* )
3 suplesup.c 
 |-  ( ph -> A. x e. A A. y e. RR+ E. z e. B ( x - y ) < z )
4 ressxr 
 |-  RR C_ RR*
5 1 4 sstrdi 
 |-  ( ph -> A C_ RR* )
6 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
7 5 6 syl 
 |-  ( ph -> sup ( A , RR* , < ) e. RR* )
8 7 adantr 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) e. RR* )
9 eqidd 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> +oo = +oo )
10 simpr 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) = +oo )
11 peano2re 
 |-  ( w e. RR -> ( w + 1 ) e. RR )
12 11 adantl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> ( w + 1 ) e. RR )
13 5 adantr 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> A C_ RR* )
14 supxrunb2 
 |-  ( A C_ RR* -> ( A. r e. RR E. x e. A r < x <-> sup ( A , RR* , < ) = +oo ) )
15 13 14 syl 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> ( A. r e. RR E. x e. A r < x <-> sup ( A , RR* , < ) = +oo ) )
16 10 15 mpbird 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> A. r e. RR E. x e. A r < x )
17 16 adantr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> A. r e. RR E. x e. A r < x )
18 breq1 
 |-  ( r = ( w + 1 ) -> ( r < x <-> ( w + 1 ) < x ) )
19 18 rexbidv 
 |-  ( r = ( w + 1 ) -> ( E. x e. A r < x <-> E. x e. A ( w + 1 ) < x ) )
20 19 rspcva 
 |-  ( ( ( w + 1 ) e. RR /\ A. r e. RR E. x e. A r < x ) -> E. x e. A ( w + 1 ) < x )
21 12 17 20 syl2anc 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> E. x e. A ( w + 1 ) < x )
22 1rp 
 |-  1 e. RR+
23 22 a1i 
 |-  ( ( ph /\ x e. A ) -> 1 e. RR+ )
24 3 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> A. y e. RR+ E. z e. B ( x - y ) < z )
25 oveq2 
 |-  ( y = 1 -> ( x - y ) = ( x - 1 ) )
26 25 breq1d 
 |-  ( y = 1 -> ( ( x - y ) < z <-> ( x - 1 ) < z ) )
27 26 rexbidv 
 |-  ( y = 1 -> ( E. z e. B ( x - y ) < z <-> E. z e. B ( x - 1 ) < z ) )
28 27 rspcva 
 |-  ( ( 1 e. RR+ /\ A. y e. RR+ E. z e. B ( x - y ) < z ) -> E. z e. B ( x - 1 ) < z )
29 23 24 28 syl2anc 
 |-  ( ( ph /\ x e. A ) -> E. z e. B ( x - 1 ) < z )
30 29 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> E. z e. B ( x - 1 ) < z )
31 30 3adant3 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> E. z e. B ( x - 1 ) < z )
32 nfv 
 |-  F/ z ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x )
33 simp11r 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> w e. RR )
34 4 33 sseldi 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> w e. RR* )
35 1 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
36 1red 
 |-  ( ( ph /\ x e. A ) -> 1 e. RR )
37 35 36 resubcld 
 |-  ( ( ph /\ x e. A ) -> ( x - 1 ) e. RR )
38 37 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> ( x - 1 ) e. RR )
39 38 3adant3 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> ( x - 1 ) e. RR )
40 39 3ad2ant1 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> ( x - 1 ) e. RR )
41 4 40 sseldi 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> ( x - 1 ) e. RR* )
42 2 sselda 
 |-  ( ( ph /\ z e. B ) -> z e. RR* )
43 42 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. B ) -> z e. RR* )
44 43 3ad2antl1 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B ) -> z e. RR* )
45 44 3adant3 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> z e. RR* )
46 simp3 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> ( w + 1 ) < x )
47 simp1r 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> w e. RR )
48 1red 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> 1 e. RR )
49 35 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> x e. RR )
50 49 3adant3 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> x e. RR )
51 47 48 50 ltaddsubd 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> ( ( w + 1 ) < x <-> w < ( x - 1 ) ) )
52 46 51 mpbid 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> w < ( x - 1 ) )
53 52 3ad2ant1 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> w < ( x - 1 ) )
54 simp3 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> ( x - 1 ) < z )
55 34 41 45 53 54 xrlttrd 
 |-  ( ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) /\ z e. B /\ ( x - 1 ) < z ) -> w < z )
56 55 3exp 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> ( z e. B -> ( ( x - 1 ) < z -> w < z ) ) )
57 32 56 reximdai 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> ( E. z e. B ( x - 1 ) < z -> E. z e. B w < z ) )
58 31 57 mpd 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ ( w + 1 ) < x ) -> E. z e. B w < z )
59 58 3exp 
 |-  ( ( ph /\ w e. RR ) -> ( x e. A -> ( ( w + 1 ) < x -> E. z e. B w < z ) ) )
60 59 adantlr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> ( x e. A -> ( ( w + 1 ) < x -> E. z e. B w < z ) ) )
61 60 rexlimdv 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> ( E. x e. A ( w + 1 ) < x -> E. z e. B w < z ) )
62 21 61 mpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> E. z e. B w < z )
63 4 a1i 
 |-  ( ph -> RR C_ RR* )
64 63 sselda 
 |-  ( ( ph /\ w e. RR ) -> w e. RR* )
65 64 ad2antrr 
 |-  ( ( ( ( ph /\ w e. RR ) /\ z e. B ) /\ w < z ) -> w e. RR* )
66 43 adantr 
 |-  ( ( ( ( ph /\ w e. RR ) /\ z e. B ) /\ w < z ) -> z e. RR* )
67 simpr 
 |-  ( ( ( ( ph /\ w e. RR ) /\ z e. B ) /\ w < z ) -> w < z )
68 65 66 67 xrltled 
 |-  ( ( ( ( ph /\ w e. RR ) /\ z e. B ) /\ w < z ) -> w <_ z )
69 68 ex 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. B ) -> ( w < z -> w <_ z ) )
70 69 adantllr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) /\ z e. B ) -> ( w < z -> w <_ z ) )
71 70 reximdva 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> ( E. z e. B w < z -> E. z e. B w <_ z ) )
72 62 71 mpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) = +oo ) /\ w e. RR ) -> E. z e. B w <_ z )
73 72 ralrimiva 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> A. w e. RR E. z e. B w <_ z )
74 supxrunb1 
 |-  ( B C_ RR* -> ( A. w e. RR E. z e. B w <_ z <-> sup ( B , RR* , < ) = +oo ) )
75 2 74 syl 
 |-  ( ph -> ( A. w e. RR E. z e. B w <_ z <-> sup ( B , RR* , < ) = +oo ) )
76 75 adantr 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> ( A. w e. RR E. z e. B w <_ z <-> sup ( B , RR* , < ) = +oo ) )
77 73 76 mpbid 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> sup ( B , RR* , < ) = +oo )
78 9 10 77 3eqtr4d 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) = sup ( B , RR* , < ) )
79 8 78 xreqled 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
80 supeq1 
 |-  ( A = (/) -> sup ( A , RR* , < ) = sup ( (/) , RR* , < ) )
81 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
82 81 a1i 
 |-  ( A = (/) -> sup ( (/) , RR* , < ) = -oo )
83 80 82 eqtrd 
 |-  ( A = (/) -> sup ( A , RR* , < ) = -oo )
84 83 adantl 
 |-  ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -oo )
85 supxrcl 
 |-  ( B C_ RR* -> sup ( B , RR* , < ) e. RR* )
86 2 85 syl 
 |-  ( ph -> sup ( B , RR* , < ) e. RR* )
87 mnfle 
 |-  ( sup ( B , RR* , < ) e. RR* -> -oo <_ sup ( B , RR* , < ) )
88 86 87 syl 
 |-  ( ph -> -oo <_ sup ( B , RR* , < ) )
89 88 adantr 
 |-  ( ( ph /\ A = (/) ) -> -oo <_ sup ( B , RR* , < ) )
90 84 89 eqbrtrd 
 |-  ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
91 90 adantlr 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ A = (/) ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
92 simpll 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> ph )
93 1 adantr 
 |-  ( ( ph /\ -. A = (/) ) -> A C_ RR )
94 neqne 
 |-  ( -. A = (/) -> A =/= (/) )
95 94 adantl 
 |-  ( ( ph /\ -. A = (/) ) -> A =/= (/) )
96 supxrgtmnf 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> -oo < sup ( A , RR* , < ) )
97 93 95 96 syl2anc 
 |-  ( ( ph /\ -. A = (/) ) -> -oo < sup ( A , RR* , < ) )
98 97 adantlr 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> -oo < sup ( A , RR* , < ) )
99 simpr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. sup ( A , RR* , < ) = +oo )
100 simpl 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ph )
101 nltpnft 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
102 100 7 101 3syl 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
103 99 102 mtbid 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. -. sup ( A , RR* , < ) < +oo )
104 notnotr 
 |-  ( -. -. sup ( A , RR* , < ) < +oo -> sup ( A , RR* , < ) < +oo )
105 103 104 syl 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) < +oo )
106 105 adantr 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> sup ( A , RR* , < ) < +oo )
107 98 106 jca 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) )
108 92 7 syl 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> sup ( A , RR* , < ) e. RR* )
109 xrrebnd 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
110 108 109 syl 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
111 107 110 mpbird 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> sup ( A , RR* , < ) e. RR )
112 nfv 
 |-  F/ w ( ph /\ sup ( A , RR* , < ) e. RR )
113 2 adantr 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> B C_ RR* )
114 simpr 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) e. RR )
115 114 adantr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> sup ( A , RR* , < ) e. RR )
116 simpr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> w e. RR+ )
117 116 rphalfcld 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( w / 2 ) e. RR+ )
118 115 117 ltsubrpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - ( w / 2 ) ) < sup ( A , RR* , < ) )
119 5 ad2antrr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> A C_ RR* )
120 rpre 
 |-  ( w e. RR+ -> w e. RR )
121 2re 
 |-  2 e. RR
122 121 a1i 
 |-  ( w e. RR+ -> 2 e. RR )
123 2ne0 
 |-  2 =/= 0
124 123 a1i 
 |-  ( w e. RR+ -> 2 =/= 0 )
125 120 122 124 redivcld 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR )
126 125 adantl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( w / 2 ) e. RR )
127 115 126 resubcld 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - ( w / 2 ) ) e. RR )
128 4 127 sseldi 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - ( w / 2 ) ) e. RR* )
129 supxrlub 
 |-  ( ( 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 ) )
130 119 128 129 syl2anc 
 |-  ( ( ( 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 ) )
131 118 130 mpbid 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> E. x e. A ( sup ( A , RR* , < ) - ( w / 2 ) ) < x )
132 rphalfcl 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR+ )
133 132 3ad2ant2 
 |-  ( ( ph /\ w e. RR+ /\ x e. A ) -> ( w / 2 ) e. RR+ )
134 24 3adant2 
 |-  ( ( ph /\ w e. RR+ /\ x e. A ) -> A. y e. RR+ E. z e. B ( x - y ) < z )
135 oveq2 
 |-  ( y = ( w / 2 ) -> ( x - y ) = ( x - ( w / 2 ) ) )
136 135 breq1d 
 |-  ( y = ( w / 2 ) -> ( ( x - y ) < z <-> ( x - ( w / 2 ) ) < z ) )
137 136 rexbidv 
 |-  ( y = ( w / 2 ) -> ( E. z e. B ( x - y ) < z <-> E. z e. B ( x - ( w / 2 ) ) < z ) )
138 137 rspcva 
 |-  ( ( ( w / 2 ) e. RR+ /\ A. y e. RR+ E. z e. B ( x - y ) < z ) -> E. z e. B ( x - ( w / 2 ) ) < z )
139 133 134 138 syl2anc 
 |-  ( ( ph /\ w e. RR+ /\ x e. A ) -> E. z e. B ( x - ( w / 2 ) ) < z )
140 139 ad5ant134 
 |-  ( ( ( ( ( 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 
 |-  ( sup ( A , RR* , < ) e. RR -> sup ( A , RR* , < ) e. CC )
142 141 adantr 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> sup ( A , RR* , < ) e. CC )
143 120 recnd 
 |-  ( w e. RR+ -> w e. CC )
144 143 adantl 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> w e. CC )
145 144 halfcld 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> ( w / 2 ) e. CC )
146 142 145 145 subsub4d 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) = ( sup ( A , RR* , < ) - ( ( w / 2 ) + ( w / 2 ) ) ) )
147 143 2halvesd 
 |-  ( w e. RR+ -> ( ( w / 2 ) + ( w / 2 ) ) = w )
148 147 oveq2d 
 |-  ( w e. RR+ -> ( sup ( A , RR* , < ) - ( ( w / 2 ) + ( w / 2 ) ) ) = ( sup ( A , RR* , < ) - w ) )
149 148 adantl 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - ( ( w / 2 ) + ( w / 2 ) ) ) = ( sup ( A , RR* , < ) - w ) )
150 146 149 eqtr2d 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - w ) = ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) )
151 150 adantll 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( sup ( A , RR* , < ) - w ) = ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) )
152 151 adantr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) /\ x e. A ) -> ( sup ( A , RR* , < ) - w ) = ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) )
153 152 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 ) ) )
154 127 126 resubcld 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) e. RR )
155 154 adantr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) /\ x e. A ) -> ( ( sup ( A , RR* , < ) - ( w / 2 ) ) - ( w / 2 ) ) e. RR )
156 155 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 )
157 4 156 sseldi 
 |-  ( ( ( ( ( ( ( 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* )
158 120 49 sylanl2 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. A ) -> x e. RR )
159 125 ad2antlr 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. A ) -> ( w / 2 ) e. RR )
160 158 159 resubcld 
 |-  ( ( ( ph /\ w e. RR+ ) /\ x e. A ) -> ( x - ( w / 2 ) ) e. RR )
161 160 adantllr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) /\ x e. A ) -> ( x - ( w / 2 ) ) e. RR )
162 161 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 )
163 4 162 sseldi 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 )
166 164 165 42 syl2anc 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 )
168 120 ad5antlr 
 |-  ( ( ( ( ( ( ( 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 )
169 168 rehalfcld 
 |-  ( ( ( ( ( ( ( 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 )
170 167 169 resubcld 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 )
172 164 171 35 syl2anc 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 )
174 170 172 169 173 ltsub1dd 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( ( 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 )
176 157 163 166 174 175 xrlttrd 
 |-  ( ( ( ( ( ( ( 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 )
177 153 176 eqbrtrd 
 |-  ( ( ( ( ( ( ( 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 )
178 177 ex 
 |-  ( ( ( ( ( ( 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 ) )
179 178 reximdva 
 |-  ( ( ( ( ( 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 ) )
180 140 179 mpd 
 |-  ( ( ( ( ( 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 )
181 180 rexlimdva2 
 |-  ( ( ( 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 ) )
182 131 181 mpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ w e. RR+ ) -> E. z e. B ( sup ( A , RR* , < ) - w ) < z )
183 112 113 114 182 supxrgere 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
184 92 111 183 syl2anc 
 |-  ( ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) /\ -. A = (/) ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
185 91 184 pm2.61dan 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
186 79 185 pm2.61dan 
 |-  ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )