let x be Surreal; :: thesis: ( x is *real iff ex r being Real st x == uReal . r )
thus ( x is *real implies ex r being Real st x == uReal . r ) :: thesis: ( ex r being Real st x == uReal . r implies x is *real )
proof
assume A1: x is *real ; :: thesis: ex r being Real st x == uReal . r
defpred S1[ object ] means ( $1 is Real & ( for r being Real st r = $1 holds
uReal . r < x ) );
defpred S2[ object ] means ( $1 is Real & ( for r being Real st r = $1 holds
x < uReal . r ) );
A2: for r, s being ExtReal st S1[r] & S2[s] holds
r <= s
proof
let r, s be ExtReal; :: thesis: ( S1[r] & S2[s] implies r <= s )
assume A3: ( S1[r] & S2[s] ) ; :: thesis: r <= s
reconsider R = r, S = s as Real by A3;
( uReal . R < x & x <= uReal . S ) by A3;
then uReal . R < uReal . S by SURREALO:4;
hence r <= s by Th51; :: thesis: verum
end;
consider s being ExtReal such that
A4: for r being ExtReal st S1[r] holds
r <= s and
A5: for r being ExtReal st S2[r] holds
s <= r from XXREAL_1:sch 1(A2);
 consider n being Nat such that
A6: ( uInt . (- n) < x & x < uInt . n ) by A1;
( uReal . n = uDyadic . n & uDyadic . n = uInt . n & uReal . (- n) = uDyadic . (- n) & uDyadic . (- n) = uInt . (- n) ) by Th46, Def5;
then ( S1[ - n] & S2[n] ) by A6;
then ( - n <= s & s <= n & n in REAL & - n in REAL ) by A4, A5, XREAL_0:def 1;
then s in REAL by XXREAL_0:45;
then reconsider s = s as Real ;
take s ; :: thesis: x == uReal . s
set S = uReal . s;
uReal . s = Unique_No (sReal . s) by Def7;
then A7: ( sReal . s == uReal . s & x == real_qua x ) by A1, SURREALO:def 10;
A8: x <= uReal . s
proof
assume uReal . s < x ; :: thesis: contradiction
then uReal . s < real_qua x by A7, SURREALO:4;
then sReal . s < real_qua x by A7, SURREALO:4;
per cases then ( ex xR being Surreal st
( xR in R_ (sReal . s) & sReal . s < xR & xR <= real_qua x ) or ex yL being Surreal st
( yL in L_ (real_qua x) & sReal . s <= yL & yL < real_qua x ) ) by SURREALO:13;
suppose ex xR being Surreal st
( xR in R_ (sReal . s) & sReal . s < xR & xR <= real_qua x ) ; :: thesis: contradiction
then consider xR being Surreal such that
A9: ( xR in R_ (sReal . s) & sReal . s < xR & xR <= real_qua x ) ;
consider n being Nat such that
A10: xR = uDyadic . ([\((s * (2 |^ n)) + 1)/] / (2 |^ n)) by A9, Th43;
set D = [\((s * (2 |^ n)) + 1)/] / (2 |^ n);
A11: s < [\((s * (2 |^ n)) + 1)/] / (2 |^ n) by Th41;
then A12: (s + ([\((s * (2 |^ n)) + 1)/] / (2 |^ n))) / 2 < [\((s * (2 |^ n)) + 1)/] / (2 |^ n) by XREAL_1:226;
A13: xR = uReal . ([\((s * (2 |^ n)) + 1)/] / (2 |^ n)) by A10, Th46;
xR <= x by A9, A7, SURREALO:4;
then S1[(s + ([\((s * (2 |^ n)) + 1)/] / (2 |^ n))) / 2] by A12, A13, SURREALO:4, Th51;
hence contradiction by A4, A11, XREAL_1:226; :: thesis: verum
end;
suppose ex yL being Surreal st
( yL in L_ (real_qua x) & sReal . s <= yL & yL < real_qua x ) ; :: thesis: contradiction
then consider yL being Surreal such that
A14: ( yL in L_ (real_qua x) & sReal . s <= yL & yL < real_qua x ) ;
yL in { (x - ((uInt . n) ")) where n is positive Nat : verum } by Def8, A14;
then consider nL being positive Nat such that
A15: yL = x - ((uInt . nL) ") ;
1 * nL < 2 * nL by XREAL_1:68;
then ( uReal . (1 / (2 * nL)) < uReal . (1 / nL) & uReal . (1 / nL) == (uInt . nL) " ) by XREAL_1:76, Th58, Th51;
then uReal . (1 / (2 * nL)) < (uInt . nL) " by SURREALO:4;
then - ((uInt . nL) ") < - (uReal . (1 / (2 * nL))) by SURREALR:10;
then yL < x + (- (uReal . (1 / (2 * nL)))) by A15, SURREALR:44;
then sReal . s < x - (uReal . (1 / (2 * nL))) by A14, SURREALO:4;
then ( (uReal . s) + (uReal . (1 / (2 * nL))) == (sReal . s) + (uReal . (1 / (2 * nL))) & (sReal . s) + (uReal . (1 / (2 * nL))) < x ) by A7, SURREALR:42, SURREALR:66;
then ( uReal . (s + (1 / (2 * nL))) == (uReal . s) + (uReal . (1 / (2 * nL))) & (uReal . s) + (uReal . (1 / (2 * nL))) < x ) by SURREALO:4, Th55;
then S1[s + (1 / (2 * nL))] by SURREALO:4;
then s + (1 / (2 * nL)) <= s + 0 by A4;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
end;
end;
uReal . s <= x
proof
assume x < uReal . s ; :: thesis: contradiction
then real_qua x < uReal . s by A7, SURREALO:4;
then real_qua x < sReal . s by A7, SURREALO:4;
per cases then ( ex xR being Surreal st
( xR in R_ (real_qua x) & real_qua x < xR & xR <= sReal . s ) or ex yL being Surreal st
( yL in L_ (sReal . s) & real_qua x <= yL & yL < sReal . s ) ) by SURREALO:13;
suppose ex xR being Surreal st
( xR in R_ (real_qua x) & real_qua x < xR & xR <= sReal . s ) ; :: thesis: contradiction
then consider xR being Surreal such that
A16: ( xR in R_ (real_qua x) & real_qua x < xR & xR <= sReal . s ) ;
xR in { (x + ((uInt . n) ")) where n is positive Nat : verum } by Def8, A16;
then consider nL being positive Nat such that
A17: xR = x + ((uInt . nL) ") ;
1 * nL < 2 * nL by XREAL_1:68;
then ( uReal . (1 / (2 * nL)) < uReal . (1 / nL) & uReal . (1 / nL) == (uInt . nL) " ) by XREAL_1:76, Th58, Th51;
then uReal . (1 / (2 * nL)) < (uInt . nL) " by SURREALO:4;
then x + (uReal . (1 / (2 * nL))) < xR by A17, SURREALR:44;
then x + (uReal . (1 / (2 * nL))) < sReal . s by A16, SURREALO:4;
then x + (uReal . (1 / (2 * nL))) < uReal . s by A7, SURREALO:4;
then A18: x < (uReal . s) - (uReal . (1 / (2 * nL))) by SURREALR:42;
- (uReal . (1 / (2 * nL))) == uReal . (- (1 / (2 * nL))) by Th56;
then (uReal . s) + (- (uReal . (1 / (2 * nL)))) == (uReal . s) + (uReal . (- (1 / (2 * nL)))) by SURREALR:66;
then ( x < (uReal . s) + (uReal . (- (1 / (2 * nL)))) & (uReal . s) + (uReal . (- (1 / (2 * nL)))) == uReal . (s + (- (1 / (2 * nL)))) ) by Th55, A18, SURREALO:4;
then S2[s - (1 / (2 * nL))] by SURREALO:4;
then 0 + s <= s + (- (1 / (2 * nL))) by A5;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
suppose ex yL being Surreal st
( yL in L_ (sReal . s) & real_qua x <= yL & yL < sReal . s ) ; :: thesis: contradiction
then consider yL being Surreal such that
A19: ( yL in L_ (sReal . s) & real_qua x <= yL & yL < sReal . s ) ;
consider n being Nat such that
A20: yL = uDyadic . ([/((s * (2 |^ n)) - 1)\] / (2 |^ n)) by A19, Th42;
set D = [/((s * (2 |^ n)) - 1)\] / (2 |^ n);
A21: [/((s * (2 |^ n)) - 1)\] / (2 |^ n) < s by Th41;
then A22: [/((s * (2 |^ n)) - 1)\] / (2 |^ n) < (s + ([/((s * (2 |^ n)) - 1)\] / (2 |^ n))) / 2 by XREAL_1:226;
A23: yL = uReal . ([/((s * (2 |^ n)) - 1)\] / (2 |^ n)) by A20, Th46;
x <= yL by A19, A7, SURREALO:4;
then S2[(s + ([/((s * (2 |^ n)) - 1)\] / (2 |^ n))) / 2] by A22, A23, Th51, SURREALO:4;
hence contradiction by A5, A21, XREAL_1:226; :: thesis: verum
end;
end;
end;
hence x == uReal . s by A8; :: thesis: verum
end;
thus ( ex r being Real st x == uReal . r implies x is *real ) by Th61; :: thesis: verum