ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  infssuzex Unicode version

Theorem infssuzex 11538
Description: Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.)
Hypotheses
Ref Expression
infssuzledc.m  |-  ( ph  ->  M  e.  ZZ )
infssuzledc.s  |-  S  =  { n  e.  (
ZZ>= `  M )  |  ps }
infssuzledc.a  |-  ( ph  ->  A  e.  S )
infssuzledc.dc  |-  ( (
ph  /\  n  e.  ( M ... A ) )  -> DECID  ps )
Assertion
Ref Expression
infssuzex  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  S  -.  y  <  x  /\  A. y  e.  RR  (
x  <  y  ->  E. z  e.  S  z  <  y ) ) )
Distinct variable groups:    y, A    A, n    n, M    x, S, y, z    ph, n    ph, x, y
Allowed substitution hints:    ph( z)    ps( x, y, z, n)    A( x, z)    S( n)    M( x, y, z)

Proof of Theorem infssuzex
Dummy variables  j  m  a  w  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zssre 9012 . . . 4  |-  ZZ  C_  RR
2 infssuzledc.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  S )
3 infssuzledc.s . . . . . . . . . . 11  |-  S  =  { n  e.  (
ZZ>= `  M )  |  ps }
43eleq2i 2182 . . . . . . . . . 10  |-  ( A  e.  S  <->  A  e.  { n  e.  ( ZZ>= `  M )  |  ps } )
52, 4sylib 121 . . . . . . . . 9  |-  ( ph  ->  A  e.  { n  e.  ( ZZ>= `  M )  |  ps } )
6 elrabi 2808 . . . . . . . . 9  |-  ( A  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  A  e.  ( ZZ>= `  M )
)
75, 6syl 14 . . . . . . . 8  |-  ( ph  ->  A  e.  ( ZZ>= `  M ) )
8 eluzelz 9284 . . . . . . . 8  |-  ( A  e.  ( ZZ>= `  M
)  ->  A  e.  ZZ )
97, 8syl 14 . . . . . . 7  |-  ( ph  ->  A  e.  ZZ )
109znegcld 9126 . . . . . 6  |-  ( ph  -> 
-u A  e.  ZZ )
11 negeq 7919 . . . . . . 7  |-  ( m  =  -u A  ->  -u m  =  -u -u A )
1211eleq1d 2184 . . . . . 6  |-  ( m  =  -u A  ->  ( -u m  e.  S  <->  -u -u A  e.  S ) )
139zcnd 9125 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
1413negnegd 8028 . . . . . . 7  |-  ( ph  -> 
-u -u A  =  A )
1514, 2eqeltrd 2192 . . . . . 6  |-  ( ph  -> 
-u -u A  e.  S
)
16 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  M  <_ 
-u m )
179adantr 272 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  A  e.  ZZ )
1817zred 9124 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  A  e.  RR )
19 eluzelz 9284 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  m  e.  ZZ )
2019adantl 273 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  ZZ )
2120zred 9124 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  RR )
22 eluzle 9287 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  -u A  <_  m )
2322adantl 273 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u A  <_  m )
2418, 21, 23lenegcon1d 8252 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u m  <_  A )
2524adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  <_  A )
2616, 25jca 302 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( M  <_  -u m  /\  -u m  <_  A ) )
2720znegcld 9126 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u m  e.  ZZ )
2827adantr 272 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  e.  ZZ )
29 infssuzledc.m . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ZZ )
3029ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  M  e.  ZZ )
319ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  A  e.  ZZ )
32 elfz 9736 . . . . . . . . . . 11  |-  ( (
-u m  e.  ZZ  /\  M  e.  ZZ  /\  A  e.  ZZ )  ->  ( -u m  e.  ( M ... A
)  <->  ( M  <_  -u m  /\  -u m  <_  A ) ) )
3328, 30, 31, 32syl3anc 1199 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  ( M ... A )  <->  ( M  <_ 
-u m  /\  -u m  <_  A ) ) )
3426, 33mpbird 166 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  e.  ( M ... A
) )
35 infssuzledc.dc . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( M ... A ) )  -> DECID  ps )
3635ralrimiva 2480 . . . . . . . . . 10  |-  ( ph  ->  A. n  e.  ( M ... A )DECID  ps )
3736ad2antrr 477 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  A. n  e.  ( M ... A
)DECID 
ps )
38 nfsbc1v 2898 . . . . . . . . . . 11  |-  F/ n [. -u m  /  n ]. ps
3938nfdc 1620 . . . . . . . . . 10  |-  F/ nDECID  [. -u m  /  n ]. ps
40 sbceq1a 2889 . . . . . . . . . . 11  |-  ( n  =  -u m  ->  ( ps 
<-> 
[. -u m  /  n ]. ps ) )
4140dcbid 806 . . . . . . . . . 10  |-  ( n  =  -u m  ->  (DECID  ps  <-> DECID  [. -u m  /  n ]. ps )
)
4239, 41rspc 2755 . . . . . . . . 9  |-  ( -u m  e.  ( M ... A )  ->  ( A. n  e.  ( M ... A )DECID  ps  -> DECID  [. -u m  /  n ]. ps )
)
4334, 37, 42sylc 62 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  -> DECID  [. -u m  /  n ]. ps )
443eleq2i 2182 . . . . . . . . . 10  |-  ( -u m  e.  S  <->  -u m  e. 
{ n  e.  (
ZZ>= `  M )  |  ps } )
45 elfzuz 9742 . . . . . . . . . . . . 13  |-  ( -u m  e.  ( M ... A )  ->  -u m  e.  ( ZZ>= `  M )
)
4634, 45syl 14 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  e.  ( ZZ>= `  M )
)
4746biantrurd 301 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( [. -u m  /  n ]. ps  <->  ( -u m  e.  ( ZZ>= `  M )  /\  [. -u m  /  n ]. ps ) ) )
48 nfcv 2256 . . . . . . . . . . . 12  |-  F/_ n
( ZZ>= `  M )
4948elrabsf 2917 . . . . . . . . . . 11  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  <->  ( -u m  e.  ( ZZ>= `  M )  /\  [. -u m  /  n ]. ps ) )
5047, 49syl6rbbr 198 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  <->  [. -u m  /  n ]. ps )
)
5144, 50syl5bb 191 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  S  <->  [. -u m  /  n ]. ps )
)
5251dcbid 806 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  (DECID  -u m  e.  S  <-> DECID  [. -u m  /  n ]. ps ) )
5343, 52mpbird 166 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  -> DECID  -u m  e.  S
)
54 simpr 109 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  ->  -.  M  <_  -u m
)
55 elrabi 2808 . . . . . . . . . . . 12  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u m  e.  ( ZZ>= `  M )
)
56 eluzle 9287 . . . . . . . . . . . 12  |-  ( -u m  e.  ( ZZ>= `  M )  ->  M  <_ 
-u m )
5755, 56syl 14 . . . . . . . . . . 11  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  M  <_ 
-u m )
5857, 3eleq2s 2210 . . . . . . . . . 10  |-  ( -u m  e.  S  ->  M  <_  -u m )
5954, 58nsyl 600 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  ->  -.  -u m  e.  S
)
6059olcd 706 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  -> 
( -u m  e.  S  \/  -.  -u m  e.  S
) )
61 df-dc 803 . . . . . . . 8  |-  (DECID  -u m  e.  S  <->  ( -u m  e.  S  \/  -.  -u m  e.  S ) )
6260, 61sylibr 133 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  -> DECID  -u m  e.  S )
6329adantr 272 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  M  e.  ZZ )
64 zdcle 9078 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  -u m  e.  ZZ )  -> DECID 
M  <_  -u m )
6563, 27, 64syl2anc 406 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  -> DECID  M  <_  -u m
)
66 exmiddc 804 . . . . . . . 8  |-  (DECID  M  <_  -u m  ->  ( M  <_ 
-u m  \/  -.  M  <_  -u m ) )
6765, 66syl 14 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  ( M  <_ 
-u m  \/  -.  M  <_  -u m ) )
6853, 62, 67mpjaodan 770 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  -> DECID  -u m  e.  S
)
69 eluzle 9287 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  M
)  ->  M  <_  A )
707, 69syl 14 . . . . . . . . . 10  |-  ( ph  ->  M  <_  A )
7129zred 9124 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
729zred 9124 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
7371, 72lenegd 8249 . . . . . . . . . 10  |-  ( ph  ->  ( M  <_  A  <->  -u A  <_  -u M ) )
7470, 73mpbid 146 . . . . . . . . 9  |-  ( ph  -> 
-u A  <_  -u M
)
7529znegcld 9126 . . . . . . . . . 10  |-  ( ph  -> 
-u M  e.  ZZ )
76 eluz 9288 . . . . . . . . . 10  |-  ( (
-u A  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( -u M  e.  ( ZZ>= `  -u A )  <->  -u A  <_  -u M
) )
7710, 75, 76syl2anc 406 . . . . . . . . 9  |-  ( ph  ->  ( -u M  e.  ( ZZ>= `  -u A )  <->  -u A  <_  -u M
) )
7874, 77mpbird 166 . . . . . . . 8  |-  ( ph  -> 
-u M  e.  (
ZZ>= `  -u A ) )
79 peano2uz 9327 . . . . . . . 8  |-  ( -u M  e.  ( ZZ>= `  -u A )  ->  ( -u M  +  1 )  e.  ( ZZ>= `  -u A
) )
8078, 79syl 14 . . . . . . 7  |-  ( ph  ->  ( -u M  + 
1 )  e.  (
ZZ>= `  -u A ) )
8171ad2antrr 477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  M  e.  RR )
8281renegcld 8106 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  e.  RR )
83 peano2re 7862 . . . . . . . . . . . 12  |-  ( -u M  e.  RR  ->  (
-u M  +  1 )  e.  RR )
8482, 83syl 14 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  +  1 )  e.  RR )
85 eluzelz 9284 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  ( -u M  +  1 ) )  ->  m  e.  ZZ )
8685ad2antlr 478 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  e.  ZZ )
8786zred 9124 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  e.  RR )
88 eluzle 9287 . . . . . . . . . . . 12  |-  ( m  e.  ( ZZ>= `  ( -u M  +  1 ) )  ->  ( -u M  +  1 )  <_  m )
8988ad2antlr 478 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  +  1 )  <_  m )
9055, 3eleq2s 2210 . . . . . . . . . . . . . . 15  |-  ( -u m  e.  S  ->  -u m  e.  ( ZZ>= `  M ) )
9190adantl 273 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -u m  e.  S )  ->  -u m  e.  ( ZZ>= `  M )
)
9291, 56syl 14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -u m  e.  S )  ->  M  <_ 
-u m )
9392adantlr 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  M  <_ 
-u m )
9481, 87, 93lenegcon2d 8253 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  <_ 
-u M )
9584, 87, 82, 89, 94letrd 7850 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  +  1 )  <_  -u M )
9675ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  e.  ZZ )
97 zltp1le 9059 . . . . . . . . . . 11  |-  ( (
-u M  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( -u M  <  -u M  <->  ( -u M  +  1 )  <_  -u M ) )
9896, 96, 97syl2anc 406 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  <  -u M  <->  (
-u M  +  1 )  <_  -u M ) )
9995, 98mpbird 166 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  <  -u M )
10082ltnrd 7839 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -.  -u M  <  -u M
)
10199, 100pm2.65da 633 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  ->  -.  -u m  e.  S )
102101ralrimiva 2480 . . . . . . 7  |-  ( ph  ->  A. m  e.  (
ZZ>= `  ( -u M  +  1 ) )  -.  -u m  e.  S
)
103 fveq2 5387 . . . . . . . . 9  |-  ( j  =  ( -u M  +  1 )  -> 
( ZZ>= `  j )  =  ( ZZ>= `  ( -u M  +  1 ) ) )
104103raleqdv 2607 . . . . . . . 8  |-  ( j  =  ( -u M  +  1 )  -> 
( A. m  e.  ( ZZ>= `  j )  -.  -u m  e.  S  <->  A. m  e.  ( ZZ>= `  ( -u M  +  1 ) )  -.  -u m  e.  S ) )
105104rspcev 2761 . . . . . . 7  |-  ( ( ( -u M  + 
1 )  e.  (
ZZ>= `  -u A )  /\  A. m  e.  ( ZZ>= `  ( -u M  +  1 ) )  -.  -u m  e.  S )  ->  E. j  e.  ( ZZ>= `  -u A ) A. m  e.  (
ZZ>= `  j )  -.  -u m  e.  S
)
10680, 102, 105syl2anc 406 . . . . . 6  |-  ( ph  ->  E. j  e.  (
ZZ>= `  -u A ) A. m  e.  ( ZZ>= `  j )  -.  -u m  e.  S )
10710, 12, 15, 68, 106zsupcllemex 11535 . . . . 5  |-  ( ph  ->  E. x  e.  ZZ  ( A. y  e.  {
m  e.  ZZ  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  { m  e.  ZZ  |  -u m  e.  S } y  < 
z ) ) )
108 zre 9009 . . . . . . . . . . . . 13  |-  ( b  e.  ZZ  ->  b  e.  RR )
109108anim1i 336 . . . . . . . . . . . 12  |-  ( ( b  e.  ZZ  /\  -u b  e.  S )  ->  ( b  e.  RR  /\  -u b  e.  S ) )
110 elrabi 2808 . . . . . . . . . . . . . . . . 17  |-  ( -u b  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u b  e.  ( ZZ>= `  M )
)
111110, 3eleq2s 2210 . . . . . . . . . . . . . . . 16  |-  ( -u b  e.  S  ->  -u b  e.  ( ZZ>= `  M ) )
112 eluzelz 9284 . . . . . . . . . . . . . . . 16  |-  ( -u b  e.  ( ZZ>= `  M )  ->  -u b  e.  ZZ )
113111, 112syl 14 . . . . . . . . . . . . . . 15  |-  ( -u b  e.  S  ->  -u b  e.  ZZ )
114113adantl 273 . . . . . . . . . . . . . 14  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  -u b  e.  ZZ )
115 recn 7717 . . . . . . . . . . . . . . . 16  |-  ( b  e.  RR  ->  b  e.  CC )
116 znegclb 9038 . . . . . . . . . . . . . . . 16  |-  ( b  e.  CC  ->  (
b  e.  ZZ  <->  -u b  e.  ZZ ) )
117115, 116syl 14 . . . . . . . . . . . . . . 15  |-  ( b  e.  RR  ->  (
b  e.  ZZ  <->  -u b  e.  ZZ ) )
118117adantr 272 . . . . . . . . . . . . . 14  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  ( b  e.  ZZ  <->  -u b  e.  ZZ ) )
119114, 118mpbird 166 . . . . . . . . . . . . 13  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  b  e.  ZZ )
120 simpr 109 . . . . . . . . . . . . 13  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  -u b  e.  S
)
121119, 120jca 302 . . . . . . . . . . . 12  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  ( b  e.  ZZ  /\  -u b  e.  S ) )
122109, 121impbii 125 . . . . . . . . . . 11  |-  ( ( b  e.  ZZ  /\  -u b  e.  S )  <-> 
( b  e.  RR  /\  -u b  e.  S
) )
123 negeq 7919 . . . . . . . . . . . . 13  |-  ( m  =  b  ->  -u m  =  -u b )
124123eleq1d 2184 . . . . . . . . . . . 12  |-  ( m  =  b  ->  ( -u m  e.  S  <->  -u b  e.  S ) )
125124elrab 2811 . . . . . . . . . . 11  |-  ( b  e.  { m  e.  ZZ  |  -u m  e.  S }  <->  ( b  e.  ZZ  /\  -u b  e.  S ) )
126124elrab 2811 . . . . . . . . . . 11  |-  ( b  e.  { m  e.  RR  |  -u m  e.  S }  <->  ( b  e.  RR  /\  -u b  e.  S ) )
127122, 125, 1263bitr4i 211 . . . . . . . . . 10  |-  ( b  e.  { m  e.  ZZ  |  -u m  e.  S }  <->  b  e.  { m  e.  RR  |  -u m  e.  S }
)
128127a1i 9 . . . . . . . . 9  |-  ( ph  ->  ( b  e.  {
m  e.  ZZ  |  -u m  e.  S }  <->  b  e.  { m  e.  RR  |  -u m  e.  S } ) )
129128eqrdv 2113 . . . . . . . 8  |-  ( ph  ->  { m  e.  ZZ  |  -u m  e.  S }  =  { m  e.  RR  |  -u m  e.  S } )
130129raleqdv 2607 . . . . . . 7  |-  ( ph  ->  ( A. y  e. 
{ m  e.  ZZ  |  -u m  e.  S }  -.  x  <  y  <->  A. y  e.  { m  e.  RR  |  -u m  e.  S }  -.  x  <  y ) )
131129rexeqdv 2608 . . . . . . . . 9  |-  ( ph  ->  ( E. z  e. 
{ m  e.  ZZ  |  -u m  e.  S } y  <  z  <->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  < 
z ) )
132131imbi2d 229 . . . . . . . 8  |-  ( ph  ->  ( ( y  < 
x  ->  E. z  e.  { m  e.  ZZ  |  -u m  e.  S } y  <  z
)  <->  ( y  < 
x  ->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  <  z
) ) )
133132ralbidv 2412 . . . . . . 7  |-  ( ph  ->  ( A. y  e.  RR  ( y  < 
x  ->  E. z  e.  { m  e.  ZZ  |  -u m  e.  S } y  <  z
)  <->  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
m  e.  RR  |  -u m  e.  S }
y  <  z )
) )
134130, 133anbi12d 462 . . . . . 6  |-  ( ph  ->  ( ( A. y  e.  { m  e.  ZZ  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
m  e.  ZZ  |  -u m  e.  S }
y  <  z )
)  <->  ( A. y  e.  { m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
m  e.  RR  |  -u m  e.  S }
y  <  z )
) ) )
135134rexbidv 2413 . . . . 5  |-  ( ph  ->  ( E. x  e.  ZZ  ( A. y  e.  { m  e.  ZZ  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
m  e.  ZZ  |  -u m  e.  S }
y  <  z )
)  <->  E. x  e.  ZZ  ( A. y  e.  {
m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  < 
z ) ) ) )
136107, 135mpbid 146 . . . 4  |-  ( ph  ->  E. x  e.  ZZ  ( A. y  e.  {
m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  < 
z ) ) )
137 ssrexv 3130 . . . 4  |-  ( ZZ  C_  RR  ->  ( E. x  e.  ZZ  ( A. y  e.  { m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  ( y  < 
x  ->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  <  z
) )  ->  E. x  e.  RR  ( A. y  e.  { m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
m  e.  RR  |  -u m  e.  S }
y  <  z )
) ) )
1381, 136, 137mpsyl 65 . . 3  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  {
m  e.  RR  |  -u m  e.  S }  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  { m  e.  RR  |  -u m  e.  S } y  < 
z ) ) )
139 ssrab2 3150 . . . 4  |-  { m  e.  RR  |  -u m  e.  S }  C_  RR
140139a1i 9 . . 3  |-  ( ph  ->  { m  e.  RR  |  -u m  e.  S }  C_  RR )
141138, 140supinfneg 9339 . 2  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  {
w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  -.  y  <  x  /\  A. y  e.  RR  (
x  <  y  ->  E. z  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } } z  <  y
) ) )
142 elrabi 2808 . . . . . . 7  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  ->  a  e.  RR )
143 elrabi 2808 . . . . . . . . 9  |-  ( a  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  a  e.  ( ZZ>= `  M )
)
144143, 3eleq2s 2210 . . . . . . . 8  |-  ( a  e.  S  ->  a  e.  ( ZZ>= `  M )
)
145 eluzelre 9285 . . . . . . . 8  |-  ( a  e.  ( ZZ>= `  M
)  ->  a  e.  RR )
146144, 145syl 14 . . . . . . 7  |-  ( a  e.  S  ->  a  e.  RR )
147 negeq 7919 . . . . . . . . . 10  |-  ( w  =  a  ->  -u w  =  -u a )
148147eleq1d 2184 . . . . . . . . 9  |-  ( w  =  a  ->  ( -u w  e.  { m  e.  RR  |  -u m  e.  S }  <->  -u a  e. 
{ m  e.  RR  |  -u m  e.  S } ) )
149148elrab3 2812 . . . . . . . 8  |-  ( a  e.  RR  ->  (
a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  <->  -u a  e.  {
m  e.  RR  |  -u m  e.  S }
) )
150 renegcl 7987 . . . . . . . . . 10  |-  ( a  e.  RR  ->  -u a  e.  RR )
151150biantrurd 301 . . . . . . . . 9  |-  ( a  e.  RR  ->  ( -u -u a  e.  S  <->  (
-u a  e.  RR  /\  -u -u a  e.  S
) ) )
152 negeq 7919 . . . . . . . . . . 11  |-  ( m  =  -u a  ->  -u m  =  -u -u a )
153152eleq1d 2184 . . . . . . . . . 10  |-  ( m  =  -u a  ->  ( -u m  e.  S  <->  -u -u a  e.  S ) )
154153elrab 2811 . . . . . . . . 9  |-  ( -u a  e.  { m  e.  RR  |  -u m  e.  S }  <->  ( -u a  e.  RR  /\  -u -u a  e.  S ) )
155151, 154syl6rbbr 198 . . . . . . . 8  |-  ( a  e.  RR  ->  ( -u a  e.  { m  e.  RR  |  -u m  e.  S }  <->  -u -u a  e.  S ) )
156 recn 7717 . . . . . . . . . 10  |-  ( a  e.  RR  ->  a  e.  CC )
157156negnegd 8028 . . . . . . . . 9  |-  ( a  e.  RR  ->  -u -u a  =  a )
158157eleq1d 2184 . . . . . . . 8  |-  ( a  e.  RR  ->  ( -u -u a  e.  S  <->  a  e.  S ) )
159149, 155, 1583bitrd 213 . . . . . . 7  |-  ( a  e.  RR  ->  (
a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  <->  a  e.  S
) )
160142, 146, 159pm5.21nii 676 . . . . . 6  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  <->  a  e.  S
)
161160eqriv 2112 . . . . 5  |-  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  =  S
162161raleqi 2605 . . . 4  |-  ( A. y  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  -.  y  <  x  <->  A. y  e.  S  -.  y  <  x )
163161rexeqi 2606 . . . . . 6  |-  ( E. z  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } } z  <  y  <->  E. z  e.  S  z  <  y )
164163imbi2i 225 . . . . 5  |-  ( ( x  <  y  ->  E. z  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } } z  <  y
)  <->  ( x  < 
y  ->  E. z  e.  S  z  <  y ) )
165164ralbii 2416 . . . 4  |-  ( A. y  e.  RR  (
x  <  y  ->  E. z  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } } z  <  y
)  <->  A. y  e.  RR  ( x  <  y  ->  E. z  e.  S  z  <  y ) )
166162, 165anbi12i 453 . . 3  |-  ( ( A. y  e.  {
w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  -.  y  <  x  /\  A. y  e.  RR  (
x  <  y  ->  E. z  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } } z  <  y
) )  <->  ( A. y  e.  S  -.  y  <  x  /\  A. y  e.  RR  (
x  <  y  ->  E. z  e.  S  z  <  y ) ) )
167166rexbii 2417 . 2  |-  ( E. x  e.  RR  ( A. y  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  -.  y  <  x  /\  A. y  e.  RR  ( x  < 
y  ->  E. z  e.  { w  e.  RR  |  -u w  e.  {
m  e.  RR  |  -u m  e.  S } } z  <  y
) )  <->  E. x  e.  RR  ( A. y  e.  S  -.  y  <  x  /\  A. y  e.  RR  ( x  < 
y  ->  E. z  e.  S  z  <  y ) ) )
168141, 167sylib 121 1  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  S  -.  y  <  x  /\  A. y  e.  RR  (
x  <  y  ->  E. z  e.  S  z  <  y ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680  DECID wdc 802    = wceq 1314    e. wcel 1463   A.wral 2391   E.wrex 2392   {crab 2395   [.wsbc 2880    C_ wss 3039   class class class wbr 3897   ` cfv 5091  (class class class)co 5740   CCcc 7582   RRcr 7583   1c1 7585    + caddc 7587    < clt 7764    <_ cle 7765   -ucneg 7898   ZZcz 9005   ZZ>=cuz 9275   ...cfz 9730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-addcom 7684  ax-addass 7686  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-0id 7692  ax-rnegex 7693  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-inn 8678  df-n0 8929  df-z 9006  df-uz 9276  df-fz 9731  df-fzo 9860
This theorem is referenced by:  infssuzledc  11539  infssuzcldc  11540
  Copyright terms: Public domain W3C validator