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

Theorem infssuzex 10570
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 8509 . . . 4  |-  ZZ  C_  RR
2 infssuzledc.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  S )
3 infssuzledc.s . . . . . . . . . . 11  |-  S  =  { n  e.  (
ZZ>= `  M )  |  ps }
43eleq2i 2149 . . . . . . . . . 10  |-  ( A  e.  S  <->  A  e.  { n  e.  ( ZZ>= `  M )  |  ps } )
52, 4sylib 120 . . . . . . . . 9  |-  ( ph  ->  A  e.  { n  e.  ( ZZ>= `  M )  |  ps } )
6 elrabi 2754 . . . . . . . . 9  |-  ( A  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  A  e.  ( ZZ>= `  M )
)
75, 6syl 14 . . . . . . . 8  |-  ( ph  ->  A  e.  ( ZZ>= `  M ) )
8 eluzelz 8779 . . . . . . . 8  |-  ( A  e.  ( ZZ>= `  M
)  ->  A  e.  ZZ )
97, 8syl 14 . . . . . . 7  |-  ( ph  ->  A  e.  ZZ )
109znegcld 8622 . . . . . 6  |-  ( ph  -> 
-u A  e.  ZZ )
11 negeq 7438 . . . . . . 7  |-  ( m  =  -u A  ->  -u m  =  -u -u A )
1211eleq1d 2151 . . . . . 6  |-  ( m  =  -u A  ->  ( -u m  e.  S  <->  -u -u A  e.  S ) )
139zcnd 8621 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
1413negnegd 7547 . . . . . . 7  |-  ( ph  -> 
-u -u A  =  A )
1514, 2eqeltrd 2159 . . . . . 6  |-  ( ph  -> 
-u -u A  e.  S
)
16 simpr 108 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  M  <_ 
-u m )
179adantr 270 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  A  e.  ZZ )
1817zred 8620 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  A  e.  RR )
19 eluzelz 8779 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  m  e.  ZZ )
2019adantl 271 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  ZZ )
2120zred 8620 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  RR )
22 eluzle 8782 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  -u A  <_  m )
2322adantl 271 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u A  <_  m )
2418, 21, 23lenegcon1d 7764 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u m  <_  A )
2524adantr 270 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  <_  A )
2616, 25jca 300 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( M  <_  -u m  /\  -u m  <_  A ) )
2720znegcld 8622 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u m  e.  ZZ )
2827adantr 270 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  -u m  e.  ZZ )
29 infssuzledc.m . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ZZ )
3029ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  M  e.  ZZ )
319ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  A  e.  ZZ )
32 elfz 9181 . . . . . . . . . . 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 1170 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  ( M ... A )  <->  ( M  <_ 
-u m  /\  -u m  <_  A ) ) )
3426, 33mpbird 165 . . . . . . . . 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 2439 . . . . . . . . . 10  |-  ( ph  ->  A. n  e.  ( M ... A )DECID  ps )
3736ad2antrr 472 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  A. n  e.  ( M ... A
)DECID 
ps )
38 nfsbc1v 2842 . . . . . . . . . . 11  |-  F/ n [. -u m  /  n ]. ps
3938nfdc 1590 . . . . . . . . . 10  |-  F/ nDECID  [. -u m  /  n ]. ps
40 sbceq1a 2833 . . . . . . . . . . 11  |-  ( n  =  -u m  ->  ( ps 
<-> 
[. -u m  /  n ]. ps ) )
4140dcbid 782 . . . . . . . . . 10  |-  ( n  =  -u m  ->  (DECID  ps  <-> DECID  [. -u m  /  n ]. ps )
)
4239, 41rspc 2704 . . . . . . . . 9  |-  ( -u m  e.  ( M ... A )  ->  ( A. n  e.  ( M ... A )DECID  ps  -> DECID  [. -u m  /  n ]. ps )
)
4334, 37, 42sylc 61 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  -> DECID  [. -u m  /  n ]. ps )
443eleq2i 2149 . . . . . . . . . 10  |-  ( -u m  e.  S  <->  -u m  e. 
{ n  e.  (
ZZ>= `  M )  |  ps } )
45 elfzuz 9187 . . . . . . . . . . . . 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 299 . . . . . . . . . . 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 2223 . . . . . . . . . . . 12  |-  F/_ n
( ZZ>= `  M )
4948elrabsf 2861 . . . . . . . . . . 11  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  <->  ( -u m  e.  ( ZZ>= `  M )  /\  [. -u m  /  n ]. ps ) )
5047, 49syl6rbbr 197 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  <->  [. -u m  /  n ]. ps )
)
5144, 50syl5bb 190 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  ( -u m  e.  S  <->  [. -u m  /  n ]. ps )
)
5251dcbid 782 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  ->  (DECID  -u m  e.  S  <-> DECID  [. -u m  /  n ]. ps ) )
5343, 52mpbird 165 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  M  <_  -u m )  -> DECID  -u m  e.  S
)
54 simpr 108 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  ->  -.  M  <_  -u m
)
55 elrabi 2754 . . . . . . . . . . . 12  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u m  e.  ( ZZ>= `  M )
)
56 eluzle 8782 . . . . . . . . . . . 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 2177 . . . . . . . . . 10  |-  ( -u m  e.  S  ->  M  <_  -u m )
5954, 58nsyl 591 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  ->  -.  -u m  e.  S
)
6059olcd 686 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  -> 
( -u m  e.  S  \/  -.  -u m  e.  S
) )
61 df-dc 777 . . . . . . . 8  |-  (DECID  -u m  e.  S  <->  ( -u m  e.  S  \/  -.  -u m  e.  S ) )
6260, 61sylibr 132 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  -> DECID  -u m  e.  S )
6329adantr 270 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  M  e.  ZZ )
64 zdcle 8575 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  -u m  e.  ZZ )  -> DECID 
M  <_  -u m )
6563, 27, 64syl2anc 403 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  -> DECID  M  <_  -u m
)
66 exmiddc 778 . . . . . . . 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 745 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  -> DECID  -u m  e.  S
)
69 eluzle 8782 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  M
)  ->  M  <_  A )
707, 69syl 14 . . . . . . . . . 10  |-  ( ph  ->  M  <_  A )
7129zred 8620 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
729zred 8620 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
7371, 72lenegd 7761 . . . . . . . . . 10  |-  ( ph  ->  ( M  <_  A  <->  -u A  <_  -u M ) )
7470, 73mpbid 145 . . . . . . . . 9  |-  ( ph  -> 
-u A  <_  -u M
)
7529znegcld 8622 . . . . . . . . . 10  |-  ( ph  -> 
-u M  e.  ZZ )
76 eluz 8783 . . . . . . . . . 10  |-  ( (
-u A  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( -u M  e.  ( ZZ>= `  -u A )  <->  -u A  <_  -u M
) )
7710, 75, 76syl2anc 403 . . . . . . . . 9  |-  ( ph  ->  ( -u M  e.  ( ZZ>= `  -u A )  <->  -u A  <_  -u M
) )
7874, 77mpbird 165 . . . . . . . 8  |-  ( ph  -> 
-u M  e.  (
ZZ>= `  -u A ) )
79 peano2uz 8822 . . . . . . . 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 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  M  e.  RR )
8281renegcld 7621 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  e.  RR )
83 peano2re 7381 . . . . . . . . . . . 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 8779 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  ( -u M  +  1 ) )  ->  m  e.  ZZ )
8685ad2antlr 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  e.  ZZ )
8786zred 8620 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  e.  RR )
88 eluzle 8782 . . . . . . . . . . . 12  |-  ( m  e.  ( ZZ>= `  ( -u M  +  1 ) )  ->  ( -u M  +  1 )  <_  m )
8988ad2antlr 473 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  +  1 )  <_  m )
9055, 3eleq2s 2177 . . . . . . . . . . . . . . 15  |-  ( -u m  e.  S  ->  -u m  e.  ( ZZ>= `  M ) )
9190adantl 271 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -u m  e.  S )  ->  -u m  e.  ( ZZ>= `  M )
)
9291, 56syl 14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  -u m  e.  S )  ->  M  <_ 
-u m )
9392adantlr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  M  <_ 
-u m )
9481, 87, 93lenegcon2d 7765 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  <_ 
-u M )
9584, 87, 82, 89, 94letrd 7370 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  +  1 )  <_  -u M )
9675ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  e.  ZZ )
97 zltp1le 8556 . . . . . . . . . . 11  |-  ( (
-u M  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( -u M  <  -u M  <->  ( -u M  +  1 )  <_  -u M ) )
9896, 96, 97syl2anc 403 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  ( -u M  <  -u M  <->  (
-u M  +  1 )  <_  -u M ) )
9995, 98mpbird 165 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  <  -u M )
10082ltnrd 7359 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -.  -u M  <  -u M
)
10199, 100pm2.65da 620 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  ->  -.  -u m  e.  S )
102101ralrimiva 2439 . . . . . . 7  |-  ( ph  ->  A. m  e.  (
ZZ>= `  ( -u M  +  1 ) )  -.  -u m  e.  S
)
103 fveq2 5230 . . . . . . . . 9  |-  ( j  =  ( -u M  +  1 )  -> 
( ZZ>= `  j )  =  ( ZZ>= `  ( -u M  +  1 ) ) )
104103raleqdv 2560 . . . . . . . 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 2710 . . . . . . 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 403 . . . . . 6  |-  ( ph  ->  E. j  e.  (
ZZ>= `  -u A ) A. m  e.  ( ZZ>= `  j )  -.  -u m  e.  S )
10710, 12, 15, 68, 106zsupcllemex 10567 . . . . 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 8506 . . . . . . . . . . . . 13  |-  ( b  e.  ZZ  ->  b  e.  RR )
109108anim1i 333 . . . . . . . . . . . 12  |-  ( ( b  e.  ZZ  /\  -u b  e.  S )  ->  ( b  e.  RR  /\  -u b  e.  S ) )
110 elrabi 2754 . . . . . . . . . . . . . . . . 17  |-  ( -u b  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u b  e.  ( ZZ>= `  M )
)
111110, 3eleq2s 2177 . . . . . . . . . . . . . . . 16  |-  ( -u b  e.  S  ->  -u b  e.  ( ZZ>= `  M ) )
112 eluzelz 8779 . . . . . . . . . . . . . . . 16  |-  ( -u b  e.  ( ZZ>= `  M )  ->  -u b  e.  ZZ )
113111, 112syl 14 . . . . . . . . . . . . . . 15  |-  ( -u b  e.  S  ->  -u b  e.  ZZ )
114113adantl 271 . . . . . . . . . . . . . 14  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  -u b  e.  ZZ )
115 recn 7238 . . . . . . . . . . . . . . . 16  |-  ( b  e.  RR  ->  b  e.  CC )
116 znegclb 8535 . . . . . . . . . . . . . . . 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 270 . . . . . . . . . . . . . 14  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  ( b  e.  ZZ  <->  -u b  e.  ZZ ) )
119114, 118mpbird 165 . . . . . . . . . . . . 13  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  b  e.  ZZ )
120 simpr 108 . . . . . . . . . . . . 13  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  -u b  e.  S
)
121119, 120jca 300 . . . . . . . . . . . 12  |-  ( ( b  e.  RR  /\  -u b  e.  S )  ->  ( b  e.  ZZ  /\  -u b  e.  S ) )
122109, 121impbii 124 . . . . . . . . . . 11  |-  ( ( b  e.  ZZ  /\  -u b  e.  S )  <-> 
( b  e.  RR  /\  -u b  e.  S
) )
123 negeq 7438 . . . . . . . . . . . . 13  |-  ( m  =  b  ->  -u m  =  -u b )
124123eleq1d 2151 . . . . . . . . . . . 12  |-  ( m  =  b  ->  ( -u m  e.  S  <->  -u b  e.  S ) )
125124elrab 2757 . . . . . . . . . . 11  |-  ( b  e.  { m  e.  ZZ  |  -u m  e.  S }  <->  ( b  e.  ZZ  /\  -u b  e.  S ) )
126124elrab 2757 . . . . . . . . . . 11  |-  ( b  e.  { m  e.  RR  |  -u m  e.  S }  <->  ( b  e.  RR  /\  -u b  e.  S ) )
127122, 125, 1263bitr4i 210 . . . . . . . . . 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 2081 . . . . . . . 8  |-  ( ph  ->  { m  e.  ZZ  |  -u m  e.  S }  =  { m  e.  RR  |  -u m  e.  S } )
130129raleqdv 2560 . . . . . . 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 2561 . . . . . . . . 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 228 . . . . . . . 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 2373 . . . . . . 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 457 . . . . . 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 2374 . . . . 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 145 . . . 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 3068 . . . 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 64 . . 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 3088 . . . 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 8834 . 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 2754 . . . . . . 7  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  ->  a  e.  RR )
143 elrabi 2754 . . . . . . . . 9  |-  ( a  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  a  e.  ( ZZ>= `  M )
)
144143, 3eleq2s 2177 . . . . . . . 8  |-  ( a  e.  S  ->  a  e.  ( ZZ>= `  M )
)
145 eluzelre 8780 . . . . . . . 8  |-  ( a  e.  ( ZZ>= `  M
)  ->  a  e.  RR )
146144, 145syl 14 . . . . . . 7  |-  ( a  e.  S  ->  a  e.  RR )
147 negeq 7438 . . . . . . . . . 10  |-  ( w  =  a  ->  -u w  =  -u a )
148147eleq1d 2151 . . . . . . . . 9  |-  ( w  =  a  ->  ( -u w  e.  { m  e.  RR  |  -u m  e.  S }  <->  -u a  e. 
{ m  e.  RR  |  -u m  e.  S } ) )
149148elrab3 2758 . . . . . . . 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 7506 . . . . . . . . . 10  |-  ( a  e.  RR  ->  -u a  e.  RR )
151150biantrurd 299 . . . . . . . . 9  |-  ( a  e.  RR  ->  ( -u -u a  e.  S  <->  (
-u a  e.  RR  /\  -u -u a  e.  S
) ) )
152 negeq 7438 . . . . . . . . . . 11  |-  ( m  =  -u a  ->  -u m  =  -u -u a )
153152eleq1d 2151 . . . . . . . . . 10  |-  ( m  =  -u a  ->  ( -u m  e.  S  <->  -u -u a  e.  S ) )
154153elrab 2757 . . . . . . . . 9  |-  ( -u a  e.  { m  e.  RR  |  -u m  e.  S }  <->  ( -u a  e.  RR  /\  -u -u a  e.  S ) )
155151, 154syl6rbbr 197 . . . . . . . 8  |-  ( a  e.  RR  ->  ( -u a  e.  { m  e.  RR  |  -u m  e.  S }  <->  -u -u a  e.  S ) )
156 recn 7238 . . . . . . . . . 10  |-  ( a  e.  RR  ->  a  e.  CC )
157156negnegd 7547 . . . . . . . . 9  |-  ( a  e.  RR  ->  -u -u a  =  a )
158157eleq1d 2151 . . . . . . . 8  |-  ( a  e.  RR  ->  ( -u -u a  e.  S  <->  a  e.  S ) )
159149, 155, 1583bitrd 212 . . . . . . 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 653 . . . . . 6  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  <->  a  e.  S
)
161160eqriv 2080 . . . . 5  |-  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  =  S
162161raleqi 2558 . . . 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 2559 . . . . . 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 224 . . . . 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 2377 . . . 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 448 . . 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 2378 . 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 120 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 102    <-> wb 103    \/ wo 662  DECID wdc 776    = wceq 1285    e. wcel 1434   A.wral 2353   E.wrex 2354   {crab 2357   [.wsbc 2824    C_ wss 2982   class class class wbr 3805   ` cfv 4952  (class class class)co 5564   CCcc 7111   RRcr 7112   1c1 7114    + caddc 7116    < clt 7285    <_ cle 7286   -ucneg 7417   ZZcz 8502   ZZ>=cuz 8770   ...cfz 9175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-cnex 7199  ax-resscn 7200  ax-1cn 7201  ax-1re 7202  ax-icn 7203  ax-addcl 7204  ax-addrcl 7205  ax-mulcl 7206  ax-addcom 7208  ax-addass 7210  ax-distr 7212  ax-i2m1 7213  ax-0lt1 7214  ax-0id 7216  ax-rnegex 7217  ax-cnre 7219  ax-pre-ltirr 7220  ax-pre-ltwlin 7221  ax-pre-lttrn 7222  ax-pre-apti 7223  ax-pre-ltadd 7224
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-id 4076  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-fv 4960  df-riota 5520  df-ov 5567  df-oprab 5568  df-mpt2 5569  df-1st 5819  df-2nd 5820  df-pnf 7287  df-mnf 7288  df-xr 7289  df-ltxr 7290  df-le 7291  df-sub 7418  df-neg 7419  df-inn 8177  df-n0 8426  df-z 8503  df-uz 8771  df-fz 9176  df-fzo 9300
This theorem is referenced by:  infssuzledc  10571  infssuzcldc  10572
  Copyright terms: Public domain W3C validator