let x, y be Surreal; :: thesis: ( not x == 0_No & not x + y == 0_No & omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) implies |.y.| infinitely< |.x.| )
set r = omega-r x;
set w = omega-y x;
set N = No_omega^ (omega-y x);
set R = uReal . (omega-r x);
assume that
A1: ( not x == 0_No & not x + y == 0_No ) and
A2: ( omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) ) ; :: thesis: |.y.| infinitely< |.x.|
let s be positive Real; :: according to SURREALC:def 3 :: thesis: |.y.| * (uReal . s) < |.x.|
A3: ( |.x.|, No_omega^ (omega-y x) are_commensurate & |.(x + y).|, No_omega^ (omega-y x) are_commensurate ) by A1, A2, Def7;
A4: 0_No <= uReal . s by SURREALI:def 8;
A5: |.(x - ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))).| infinitely< |.x.| by A1, Def8;
|.((x + y) - ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))).| infinitely< |.(x + y).| by A1, A2, Def8;
then A6: |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| infinitely< |.x.| by Th16, A3, Th4;
((No_omega^ (omega-y x)) * (uReal . (omega-r x))) - ((No_omega^ (omega-y x)) * (uReal . (omega-r x))) == 0_No by SURREALR:39;
then A7: ( (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + (((No_omega^ (omega-y x)) * (uReal . (omega-r x))) + (- x)) = ((- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + (- x) & ((- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + (- x) == 0_No + (- x) & 0_No + (- x) = - x ) by SURREALR:43, SURREALR:37;
A8: x - x == 0_No by SURREALR:39;
(x + y) + (- x) = y + (x + (- x)) by SURREALR:37;
then A9: ( (x + y) + (- x) == y + 0_No & y + 0_No = y ) by A8, SURREALR:43;
- (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) = (No_omega^ (omega-y x)) * (uReal . (omega-r x)) ;
then - (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) = ((No_omega^ (omega-y x)) * (uReal . (omega-r x))) + (- x) by SURREALR:40;
then ( ((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) + (- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))) = (x + y) + ((- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + (((No_omega^ (omega-y x)) * (uReal . (omega-r x))) + (- x))) & (x + y) + ((- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))) + (((No_omega^ (omega-y x)) * (uReal . (omega-r x))) + (- x))) == (x + y) + (- x) ) by A7, SURREALR:43, SURREALR:37;
then ((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) + (- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))) == y by A9, SURREALO:4;
then ( |.y.| == |.(((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) + (- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))))).| & |.(((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))) + (- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))))).| <= |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| ) by Th48, Th37;
then |.y.| <= |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| by SURREALO:4;
then ( |.y.| * (uReal . s) <= (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).|) * (uReal . s) & (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| + |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).|) * (uReal . s) == (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . s)) ) by A4, SURREALR:67, SURREALR:75;
then A10: |.y.| * (uReal . s) <= (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . s)) by SURREALO:4;
A11: |.x.| = |.x.| * (uReal . 1) by SURREALN:48;
|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . (s * 2)) < |.x.| by A6;
then A12: |.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . ((s * 2) * (1 / 2))) <= |.x.| * (uReal . (1 * (1 / 2))) by Th59, A11;
|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . (s * 2)) < |.x.| by A5;
then A13: |.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . ((s * 2) * (1 / 2))) < |.x.| * (uReal . (1 * (1 / 2))) by Th59, A11;
|.(x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s) == |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . s) by SURREALR:51, Th40;
then |.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . ((s * 2) * (1 / 2))) < |.x.| * (uReal . (1 * (1 / 2))) by A13, SURREALO:4;
then A14: (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . s)) < (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) by A12, SURREALR:44;
( (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) == |.x.| * ((uReal . (1 / 2)) + (uReal . (1 / 2))) & |.x.| * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == |.x.| * (uReal . ((1 / 2) + (1 / 2))) ) by SURREALR:67, SURREALR:51, SURREALN:55;
then ( (|.x.| * (uReal . (1 * (1 / 2)))) + (|.x.| * (uReal . (1 * (1 / 2)))) == |.x.| * (uReal . 1) & |.x.| * (uReal . 1) = |.x.| ) by SURREALN:48, SURREALO:4;
then (|.((x + y) + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x))))).| * (uReal . s)) + (|.(- (x + (- ((No_omega^ (omega-y x)) * (uReal . (omega-r x)))))).| * (uReal . s)) < |.x.| by A14, SURREALO:4;
hence |.y.| * (uReal . s) < |.x.| by A10, SURREALO:4; :: thesis: verum