let x, y be Surreal; :: thesis: ( x, No_omega^ y are_commensurate implies ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x )
assume A1: x, No_omega^ y are_commensurate ; :: thesis: ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x
set N = No_omega^ y;
defpred S1[ object ] means ( $1 is Real & ( for r being Real st r = $1 holds
(No_omega^ y) * (uReal . r) <= x ) );
defpred S2[ object ] means ( $1 is Real & ( for r being Real st r = $1 holds
x < (No_omega^ y) * (uReal . r) ) );
A2: for r, s being ExtReal st S1[r] & S2[s] holds
r <= s
proof
let l, r be ExtReal; :: thesis: ( S1[l] & S2[r] implies l <= r )
assume A3: ( S1[l] & S2[r] ) ; :: thesis: l <= r
reconsider L = l, R = r as Real by A3;
A4: 0_No <= No_omega^ y by SURREALI:def 8;
( (No_omega^ y) * (uReal . L) <= x & x < (No_omega^ y) * (uReal . R) ) by A3;
then (No_omega^ y) * (uReal . L) < (No_omega^ y) * (uReal . R) by SURREALO:4;
hence l <= r by SURREALN:51, A4, SURREALR:75; :: thesis: verum
end;
consider s being ExtReal such that
A5: for r being ExtReal st S1[r] holds
r <= s and
A6: for r being ExtReal st S2[r] holds
s <= r from XXREAL_1:sch 1(A2);
 consider n being positive Nat such that
A7: ( x < (uInt . n) * (No_omega^ y) & No_omega^ y < (uInt . n) * x ) by A1, Th7;
A8: ( uReal . n = uDyadic . n & uDyadic . n = uInt . n ) by SURREALN:46, SURREALN:def 5;
0_No < uReal . (1 / n) by SURREALI:def 8;
then A9: (No_omega^ y) * (uReal . (1 / n)) < (x * (uReal . n)) * (uReal . (1 / n)) by A7, A8, SURREALR:70;
(x * (uReal . n)) * (uReal . (1 / n)) == x by Lm2;
then A10: S1[1 / n] by A9, SURREALO:4;
then A11: 1 / n <= s by A5;
S2[n] by A7, A8;
then A12: s <= n by A6;
( n in REAL & 1 / n in REAL ) by XREAL_0:def 1;
then s in REAL by A11, A12, XXREAL_0:45;
then reconsider s = s as Real ;
reconsider s = s as positive Real by A10, A5;
per cases ( (No_omega^ y) * (uReal . s) <= x or x < (No_omega^ y) * (uReal . s) ) ;
suppose A13: (No_omega^ y) * (uReal . s) <= x ; :: thesis: ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x
set x1 = x - ((No_omega^ y) * (uReal . s));
take s ; :: thesis: |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x
A14: 0_No + ((No_omega^ y) * (uReal . s)) <= x by A13;
then A15: 0_No <= x - ((No_omega^ y) * (uReal . s)) by SURREALR:41;
x - ((No_omega^ y) * (uReal . s)) infinitely< x
proof
given r being positive Real such that A16: x <= (x - ((No_omega^ y) * (uReal . s))) * (uReal . r) ; :: according to SURREALC:def 3 :: thesis: contradiction
consider n2 being Nat such that
A17: r < n2 by SEQ_4:3;
set n = n2 + 2;
n2 <= n2 + 2 by NAT_1:11;
then uReal . r <= uReal . (n2 + 2) by SURREALN:51, A17, XXREAL_0:2;
then (x - ((No_omega^ y) * (uReal . s))) * (uReal . r) <= (x - ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2)) by A15, SURREALR:75;
then A18: x <= (x - ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2)) by A16, SURREALO:4;
A19: - (x * (uReal . (n2 + 2))) = x * (- (uReal . (n2 + 2))) by SURREALR:58;
(x - ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2)) == (x * (uReal . (n2 + 2))) + ((- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2))) by SURREALR:67;
then x <= (x * (uReal . (n2 + 2))) + ((- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2))) by A18, SURREALO:4;
then ( x * ((uReal . 1) - (uReal . (n2 + 2))) == (x * (uReal . 1)) - (x * (uReal . (n2 + 2))) & (x * (uReal . 1)) - (x * (uReal . (n2 + 2))) <= (- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2)) ) by A19, SURREALR:67, SURREALR:42, SURREALN:48;
then x * ((uReal . 1) + (- (uReal . (n2 + 2)))) <= (- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2)) by SURREALO:4;
then A20: - ((- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2))) <= - (x * ((uReal . 1) + (- (uReal . (n2 + 2))))) by SURREALR:10;
- (uReal . (n2 + 2)) == uReal . (- (n2 + 2)) by SURREALN:56;
then ( (uReal . 1) + (- (uReal . (n2 + 2))) == (uReal . 1) + (uReal . (- (n2 + 2))) & (uReal . 1) + (uReal . (- (n2 + 2))) == uReal . (1 + (- (n2 + 2))) ) by SURREALR:43, SURREALN:55;
then (uReal . 1) + (- (uReal . (n2 + 2))) == uReal . (1 + (- (n2 + 2))) by SURREALO:4;
then ( - ((uReal . 1) + (- (uReal . (n2 + 2)))) == - (uReal . (1 + (- (n2 + 2)))) & - (uReal . (1 + (- (n2 + 2)))) == uReal . (- (1 + (- (n2 + 2)))) ) by SURREALR:10, SURREALN:56;
then - ((uReal . 1) + (- (uReal . (n2 + 2)))) == uReal . (- (1 + (- (n2 + 2)))) by SURREALO:4;
then A21: ( - (x * ((uReal . 1) + (- (uReal . (n2 + 2))))) = x * (- ((uReal . 1) + (- (uReal . (n2 + 2))))) & x * (- ((uReal . 1) + (- (uReal . (n2 + 2))))) == x * (uReal . (- (1 + (- (n2 + 2))))) ) by SURREALR:58, SURREALR:51;
A22: (n2 + 2) - 1 = n2 + 1 ;
then A23: 0_No <= uReal . (1 / ((n2 + 2) - 1)) by SURREALI:def 8;
- ((- ((No_omega^ y) * (uReal . s))) * (uReal . (n2 + 2))) = - (- (((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2)))) by SURREALR:58;
then ( ((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2)) = - (- (((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2)))) & - (- (((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2)))) <= x * (uReal . (- (1 + (- (n2 + 2))))) ) by A21, A20, SURREALO:4;
then ( (((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2))) * (uReal . (1 / ((n2 + 2) - 1))) <= (x * (uReal . ((n2 + 2) - 1))) * (uReal . (1 / ((n2 + 2) - 1))) & (x * (uReal . ((n2 + 2) - 1))) * (uReal . (1 / ((n2 + 2) - 1))) == x ) by A23, SURREALR:75, A22, Lm2;
then A24: (((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2))) * (uReal . (1 / ((n2 + 2) - 1))) <= x by SURREALO:4;
(((No_omega^ y) * (uReal . s)) * (uReal . (n2 + 2))) * (uReal . (1 / ((n2 + 2) - 1))) == (No_omega^ y) * (uReal . ((s * (n2 + 2)) * (1 / ((n2 + 2) - 1)))) by Lm3;
then S1[(s * (n2 + 2)) * (1 / ((n2 + 2) - 1))] by A24, SURREALO:4;
then (s * (n2 + 2)) * (1 / ((n2 + 2) - 1)) <= s by A5;
then ( (s * (n2 + 2)) * ((1 / ((n2 + 2) - 1)) * ((n2 + 2) - 1)) = ((s * (n2 + 2)) * (1 / ((n2 + 2) - 1))) * ((n2 + 2) - 1) & ((s * (n2 + 2)) * (1 / ((n2 + 2) - 1))) * ((n2 + 2) - 1) <= s * ((n2 + 2) - 1) & (1 / ((n2 + 2) - 1)) * ((n2 + 2) - 1) = 1 ) by A22, XCMPLX_1:106, XREAL_1:64;
then (n2 + 1) + 1 <= n2 + 1 by XREAL_1:68;
hence contradiction by NAT_1:13; :: thesis: verum
end;
hence |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x by A14, Def6, SURREALR:41; :: thesis: verum
end;
suppose A25: x < (No_omega^ y) * (uReal . s) ; :: thesis: ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x
set x1 = ((No_omega^ y) * (uReal . s)) - x;
take s ; :: thesis: |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x
A26: x + 0_No < (No_omega^ y) * (uReal . s) by A25;
then A27: 0_No < ((No_omega^ y) * (uReal . s)) - x by SURREALR:42;
A28: ((No_omega^ y) * (uReal . s)) - x infinitely< x
proof
given r being positive Real such that A29: x <= (((No_omega^ y) * (uReal . s)) - x) * (uReal . r) ; :: according to SURREALC:def 3 :: thesis: contradiction
consider n being Nat such that
A30: r < n by SEQ_4:3;
(((No_omega^ y) * (uReal . s)) - x) * (uReal . r) < (((No_omega^ y) * (uReal . s)) - x) * (uReal . n) by A30, SURREALN:51, A27, SURREALR:70;
then A31: x < (((No_omega^ y) * (uReal . s)) - x) * (uReal . n) by A29, SURREALO:4;
A32: - ((- x) * (uReal . n)) = - (- (x * (uReal . n))) by SURREALR:58;
( (x * (uReal . 1)) + (x * (uReal . n)) == x * ((uReal . 1) + (uReal . n)) & x * ((uReal . 1) + (uReal . n)) == x * (uReal . (1 + n)) ) by SURREALN:55, SURREALR:67, SURREALR:51;
then A33: (x * (uReal . 1)) + (x * (uReal . n)) == x * (uReal . (1 + n)) by SURREALO:4;
(((No_omega^ y) * (uReal . s)) - x) * (uReal . n) == (((No_omega^ y) * (uReal . s)) * (uReal . n)) + ((- x) * (uReal . n)) by SURREALR:67;
then x < (((No_omega^ y) * (uReal . s)) * (uReal . n)) + ((- x) * (uReal . n)) by A31, SURREALO:4;
then (x * (uReal . 1)) - ((- x) * (uReal . n)) < ((No_omega^ y) * (uReal . s)) * (uReal . n) by SURREALR:41, SURREALN:48;
then A34: x * (uReal . (1 + n)) < ((No_omega^ y) * (uReal . s)) * (uReal . n) by A32, A33, SURREALO:4;
0_No < uReal . (1 / (n + 1)) by SURREALI:def 8;
then A35: (x * (uReal . (1 + n))) * (uReal . (1 / (n + 1))) < (((No_omega^ y) * (uReal . s)) * (uReal . n)) * (uReal . (1 / (n + 1))) by A34, SURREALR:70;
(x * (uReal . (1 + n))) * (uReal . (1 / (n + 1))) == x by Lm2;
then A36: x < (((No_omega^ y) * (uReal . s)) * (uReal . n)) * (uReal . (1 / (n + 1))) by A35, SURREALO:4;
(((No_omega^ y) * (uReal . s)) * (uReal . n)) * (uReal . (1 / (n + 1))) == (No_omega^ y) * (uReal . ((s * n) * (1 / (n + 1)))) by Lm3;
then S2[(s * n) * (1 / (n + 1))] by A36, SURREALO:4;
then ( (s * n) * ((1 / (n + 1)) * (n + 1)) = ((s * n) * (1 / (n + 1))) * (n + 1) & ((s * n) * (1 / (n + 1))) * (n + 1) >= s * (n + 1) & (1 / (n + 1)) * (n + 1) = 1 ) by A6, XCMPLX_1:106, XREAL_1:64;
then n >= n + 1 by XREAL_1:68;
hence contradiction by NAT_1:13; :: thesis: verum
end;
A37: not ((No_omega^ y) * (uReal . s)) - x == 0_No by A26, SURREALR:42;
- (((No_omega^ y) * (uReal . s)) - x) = (- ((No_omega^ y) * (uReal . s))) + (- (- x)) by SURREALR:40
.= x + (- ((No_omega^ y) * (uReal . s))) ;
then ( ((No_omega^ y) * (uReal . s)) - x = |.(((No_omega^ y) * (uReal . s)) - x).| & |.(((No_omega^ y) * (uReal . s)) - x).| = |.(x + (- ((No_omega^ y) * (uReal . s)))).| ) by A26, SURREALR:42, A37, Th39, Def6;
hence |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x by A28; :: thesis: verum
end;
end;