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

Theorem infssuzex 11027
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 8727 . . . 4  |-  ZZ  C_  RR
2 infssuzledc.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  S )
3 infssuzledc.s . . . . . . . . . . 11  |-  S  =  { n  e.  (
ZZ>= `  M )  |  ps }
43eleq2i 2154 . . . . . . . . . 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 2766 . . . . . . . . 9  |-  ( A  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  A  e.  ( ZZ>= `  M )
)
75, 6syl 14 . . . . . . . 8  |-  ( ph  ->  A  e.  ( ZZ>= `  M ) )
8 eluzelz 8997 . . . . . . . 8  |-  ( A  e.  ( ZZ>= `  M
)  ->  A  e.  ZZ )
97, 8syl 14 . . . . . . 7  |-  ( ph  ->  A  e.  ZZ )
109znegcld 8840 . . . . . 6  |-  ( ph  -> 
-u A  e.  ZZ )
11 negeq 7654 . . . . . . 7  |-  ( m  =  -u A  ->  -u m  =  -u -u A )
1211eleq1d 2156 . . . . . 6  |-  ( m  =  -u A  ->  ( -u m  e.  S  <->  -u -u A  e.  S ) )
139zcnd 8839 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
1413negnegd 7763 . . . . . . 7  |-  ( ph  -> 
-u -u A  =  A )
1514, 2eqeltrd 2164 . . . . . 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 8838 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  A  e.  RR )
19 eluzelz 8997 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  m  e.  ZZ )
2019adantl 271 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  ZZ )
2120zred 8838 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  m  e.  RR )
22 eluzle 9000 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  -u A
)  ->  -u A  <_  m )
2322adantl 271 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  ->  -u A  <_  m )
2418, 21, 23lenegcon1d 7980 . . . . . . . . . . . 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 8840 . . . . . . . . . . . 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 9399 . . . . . . . . . . 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 1174 . . . . . . . . . 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 2446 . . . . . . . . . 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 2856 . . . . . . . . . . 11  |-  F/ n [. -u m  /  n ]. ps
3938nfdc 1594 . . . . . . . . . 10  |-  F/ nDECID  [. -u m  /  n ]. ps
40 sbceq1a 2847 . . . . . . . . . . 11  |-  ( n  =  -u m  ->  ( ps 
<-> 
[. -u m  /  n ]. ps ) )
4140dcbid 786 . . . . . . . . . 10  |-  ( n  =  -u m  ->  (DECID  ps  <-> DECID  [. -u m  /  n ]. ps )
)
4239, 41rspc 2716 . . . . . . . . 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 2154 . . . . . . . . . 10  |-  ( -u m  e.  S  <->  -u m  e. 
{ n  e.  (
ZZ>= `  M )  |  ps } )
45 elfzuz 9405 . . . . . . . . . . . . 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 2228 . . . . . . . . . . . 12  |-  F/_ n
( ZZ>= `  M )
4948elrabsf 2875 . . . . . . . . . . 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 786 . . . . . . . 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 2766 . . . . . . . . . . . 12  |-  ( -u m  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u m  e.  ( ZZ>= `  M )
)
56 eluzle 9000 . . . . . . . . . . . 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 2182 . . . . . . . . . 10  |-  ( -u m  e.  S  ->  M  <_  -u m )
5954, 58nsyl 593 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  ->  -.  -u m  e.  S
)
6059olcd 688 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  -u A ) )  /\  -.  M  <_ 
-u m )  -> 
( -u m  e.  S  \/  -.  -u m  e.  S
) )
61 df-dc 781 . . . . . . . 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 8793 . . . . . . . . 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 782 . . . . . . . 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 747 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  -u A ) )  -> DECID  -u m  e.  S
)
69 eluzle 9000 . . . . . . . . . . 11  |-  ( A  e.  ( ZZ>= `  M
)  ->  M  <_  A )
707, 69syl 14 . . . . . . . . . 10  |-  ( ph  ->  M  <_  A )
7129zred 8838 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
729zred 8838 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
7371, 72lenegd 7977 . . . . . . . . . 10  |-  ( ph  ->  ( M  <_  A  <->  -u A  <_  -u M ) )
7470, 73mpbid 145 . . . . . . . . 9  |-  ( ph  -> 
-u A  <_  -u M
)
7529znegcld 8840 . . . . . . . . . 10  |-  ( ph  -> 
-u M  e.  ZZ )
76 eluz 9001 . . . . . . . . . 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 9040 . . . . . . . 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 7837 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -u M  e.  RR )
83 peano2re 7597 . . . . . . . . . . . 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 8997 . . . . . . . . . . . . 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 8838 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  e.  RR )
88 eluzle 9000 . . . . . . . . . . . 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 2182 . . . . . . . . . . . . . . 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 7981 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  m  <_ 
-u M )
9584, 87, 82, 89, 94letrd 7586 . . . . . . . . . 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 8774 . . . . . . . . . . 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 7575 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  /\  -u m  e.  S )  ->  -.  -u M  <  -u M
)
10199, 100pm2.65da 622 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( -u M  +  1 ) ) )  ->  -.  -u m  e.  S )
102101ralrimiva 2446 . . . . . . 7  |-  ( ph  ->  A. m  e.  (
ZZ>= `  ( -u M  +  1 ) )  -.  -u m  e.  S
)
103 fveq2 5289 . . . . . . . . 9  |-  ( j  =  ( -u M  +  1 )  -> 
( ZZ>= `  j )  =  ( ZZ>= `  ( -u M  +  1 ) ) )
104103raleqdv 2568 . . . . . . . 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 2722 . . . . . . 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 11024 . . . . 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 8724 . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . 17  |-  ( -u b  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  -u b  e.  ( ZZ>= `  M )
)
111110, 3eleq2s 2182 . . . . . . . . . . . . . . . 16  |-  ( -u b  e.  S  ->  -u b  e.  ( ZZ>= `  M ) )
112 eluzelz 8997 . . . . . . . . . . . . . . . 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 7454 . . . . . . . . . . . . . . . 16  |-  ( b  e.  RR  ->  b  e.  CC )
116 znegclb 8753 . . . . . . . . . . . . . . . 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 7654 . . . . . . . . . . . . 13  |-  ( m  =  b  ->  -u m  =  -u b )
124123eleq1d 2156 . . . . . . . . . . . 12  |-  ( m  =  b  ->  ( -u m  e.  S  <->  -u b  e.  S ) )
125124elrab 2769 . . . . . . . . . . 11  |-  ( b  e.  { m  e.  ZZ  |  -u m  e.  S }  <->  ( b  e.  ZZ  /\  -u b  e.  S ) )
126124elrab 2769 . . . . . . . . . . 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 2086 . . . . . . . 8  |-  ( ph  ->  { m  e.  ZZ  |  -u m  e.  S }  =  { m  e.  RR  |  -u m  e.  S } )
130129raleqdv 2568 . . . . . . 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 2569 . . . . . . . . 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 2380 . . . . . . 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 2381 . . . . 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 3084 . . . 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 3104 . . . 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 9052 . 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 2766 . . . . . . 7  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  ->  a  e.  RR )
143 elrabi 2766 . . . . . . . . 9  |-  ( a  e.  { n  e.  ( ZZ>= `  M )  |  ps }  ->  a  e.  ( ZZ>= `  M )
)
144143, 3eleq2s 2182 . . . . . . . 8  |-  ( a  e.  S  ->  a  e.  ( ZZ>= `  M )
)
145 eluzelre 8998 . . . . . . . 8  |-  ( a  e.  ( ZZ>= `  M
)  ->  a  e.  RR )
146144, 145syl 14 . . . . . . 7  |-  ( a  e.  S  ->  a  e.  RR )
147 negeq 7654 . . . . . . . . . 10  |-  ( w  =  a  ->  -u w  =  -u a )
148147eleq1d 2156 . . . . . . . . 9  |-  ( w  =  a  ->  ( -u w  e.  { m  e.  RR  |  -u m  e.  S }  <->  -u a  e. 
{ m  e.  RR  |  -u m  e.  S } ) )
149148elrab3 2770 . . . . . . . 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 7722 . . . . . . . . . 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 7654 . . . . . . . . . . 11  |-  ( m  =  -u a  ->  -u m  =  -u -u a )
153152eleq1d 2156 . . . . . . . . . 10  |-  ( m  =  -u a  ->  ( -u m  e.  S  <->  -u -u a  e.  S ) )
154153elrab 2769 . . . . . . . . 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 7454 . . . . . . . . . 10  |-  ( a  e.  RR  ->  a  e.  CC )
157156negnegd 7763 . . . . . . . . 9  |-  ( a  e.  RR  ->  -u -u a  =  a )
158157eleq1d 2156 . . . . . . . 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 655 . . . . . 6  |-  ( a  e.  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  <->  a  e.  S
)
161160eqriv 2085 . . . . 5  |-  { w  e.  RR  |  -u w  e.  { m  e.  RR  |  -u m  e.  S } }  =  S
162161raleqi 2566 . . . 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 2567 . . . . . 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 2384 . . . 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 2385 . 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 664  DECID wdc 780    = wceq 1289    e. wcel 1438   A.wral 2359   E.wrex 2360   {crab 2363   [.wsbc 2838    C_ wss 2997   class class class wbr 3837   ` cfv 5002  (class class class)co 5634   CCcc 7327   RRcr 7328   1c1 7330    + caddc 7332    < clt 7501    <_ cle 7502   -ucneg 7633   ZZcz 8720   ZZ>=cuz 8988   ...cfz 9393
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-cnex 7415  ax-resscn 7416  ax-1cn 7417  ax-1re 7418  ax-icn 7419  ax-addcl 7420  ax-addrcl 7421  ax-mulcl 7422  ax-addcom 7424  ax-addass 7426  ax-distr 7428  ax-i2m1 7429  ax-0lt1 7430  ax-0id 7432  ax-rnegex 7433  ax-cnre 7435  ax-pre-ltirr 7436  ax-pre-ltwlin 7437  ax-pre-lttrn 7438  ax-pre-apti 7439  ax-pre-ltadd 7440
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-id 4111  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-fv 5010  df-riota 5590  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-pnf 7503  df-mnf 7504  df-xr 7505  df-ltxr 7506  df-le 7507  df-sub 7634  df-neg 7635  df-inn 8395  df-n0 8644  df-z 8721  df-uz 8989  df-fz 9394  df-fzo 9519
This theorem is referenced by:  infssuzledc  11028  infssuzcldc  11029
  Copyright terms: Public domain W3C validator