let x, y be Surreal; :: thesis: for r1, r2 being Real st x, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< x & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< x holds
r2 <= r1
let r1, r2 be Real; :: thesis: ( x, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< x & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< x implies r2 <= r1 )
set N = No_omega^ y;
assume that
A1: x, No_omega^ y are_commensurate and
A2: ( |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< x & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< x ) and
A3: r1 < r2 ; :: thesis: contradiction
A4: |.((x - ((No_omega^ y) * (uReal . r1))) - (x - ((No_omega^ y) * (uReal . r2)))).| infinitely< x by A2, Th43;
A5: (x + (- ((No_omega^ y) * (uReal . r1)))) + (- (x + (- ((No_omega^ y) * (uReal . r2))))) = (x + (- ((No_omega^ y) * (uReal . r1)))) + ((- x) + (- (- ((No_omega^ y) * (uReal . r2))))) by SURREALR:40
.= x + ((- ((No_omega^ y) * (uReal . r1))) + (((No_omega^ y) * (uReal . r2)) + (- x))) by SURREALR:37
.= x + (((- ((No_omega^ y) * (uReal . r1))) + ((No_omega^ y) * (uReal . r2))) + (- x)) by SURREALR:37
.= (x + (- x)) + ((- ((No_omega^ y) * (uReal . r1))) + ((No_omega^ y) * (uReal . r2))) by SURREALR:37 ;
A6: x - x == 0_No by SURREALR:39;
( - ((No_omega^ y) * (uReal . r1)) = (No_omega^ y) * (- (uReal . r1)) & (No_omega^ y) * (- (uReal . r1)) == (No_omega^ y) * (uReal . (- r1)) ) by SURREALN:56, SURREALR:51, SURREALR:58;
then ( (- ((No_omega^ y) * (uReal . r1))) + ((No_omega^ y) * (uReal . r2)) == ((No_omega^ y) * (uReal . (- r1))) + ((No_omega^ y) * (uReal . r2)) & ((No_omega^ y) * (uReal . (- r1))) + ((No_omega^ y) * (uReal . r2)) == (No_omega^ y) * ((uReal . (- r1)) + (uReal . r2)) ) by SURREALR:43, SURREALR:67;
then ( (- ((No_omega^ y) * (uReal . r1))) + ((No_omega^ y) * (uReal . r2)) == (No_omega^ y) * ((uReal . (- r1)) + (uReal . r2)) & (No_omega^ y) * ((uReal . (- r1)) + (uReal . r2)) == (No_omega^ y) * (uReal . ((- r1) + r2)) ) by SURREALN:55, SURREALR:51, SURREALO:4;
then (- ((No_omega^ y) * (uReal . r1))) + ((No_omega^ y) * (uReal . r2)) == (No_omega^ y) * (uReal . ((- r1) + r2)) by SURREALO:4;
then ( (x + (- ((No_omega^ y) * (uReal . r1)))) + (- (x + (- ((No_omega^ y) * (uReal . r2))))) == 0_No + ((No_omega^ y) * (uReal . ((- r1) + r2))) & 0_No + ((No_omega^ y) * (uReal . ((- r1) + r2))) = (No_omega^ y) * (uReal . ((- r1) + r2)) ) by A5, A6, SURREALR:43;
then A7: |.((No_omega^ y) * (uReal . ((- r1) + r2))).| infinitely< x by Th48, A4, Th17;
consider n being positive Nat such that
A8: x < (No_omega^ y) * (uInt . n) by A1;
A9: ( uReal . n = uDyadic . n & uDyadic . n = uInt . n ) by SURREALN:46, SURREALN:def 5;
A10: 0 < r2 - r1 by A3, XREAL_1:50;
A11: 0_No < uReal . (r2 - r1) by A3, XREAL_1:50, SURREALN:47, SURREALN:51;
0_No < No_omega^ y by SURREALI:def 8;
then 0_No <= (No_omega^ y) * (uReal . (r2 - r1)) by A11, SURREALR:72;
then A12: |.((No_omega^ y) * (uReal . (r2 - r1))).| = (No_omega^ y) * (uReal . (r2 - r1)) by Def6;
(r2 - r1) * (n / (r2 - r1)) = n by A10, XCMPLX_1:87;
then ((No_omega^ y) * (uReal . (r2 - r1))) * (uReal . (n / (r2 - r1))) == (No_omega^ y) * (uReal . n) by Lm1;
then (No_omega^ y) * (uReal . n) <= x by A12, A7, A10, SURREALO:4;
hence contradiction by A8, A9; :: thesis: verum