let x, y be Surreal; :: thesis: for n being positive Nat st |.y.| * (uReal . ((n + 1) / n)) < |.x.| holds
|.x.|,|.(x + y).| are_commensurate
let n be positive Nat; :: thesis: ( |.y.| * (uReal . ((n + 1) / n)) < |.x.| implies |.x.|,|.(x + y).| are_commensurate )
assume A1: |.y.| * (uReal . ((n + 1) / n)) < |.x.| ; :: thesis: |.x.|,|.(x + y).| are_commensurate
( 0_No <= |.y.| & 0_No <= uReal . ((n + 1) / n) ) by SURREALI:def 8, Th31;
then ( 0_No = 0_No * |.y.| & 0_No * |.y.| <= (uReal . ((n + 1) / n)) * |.y.| ) by SURREALR:75;
then A2: 0_No < |.x.| by A1, SURREALO:4;
A3: 0_No < uReal . (n / (n + 1)) by SURREALI:def 8;
A4: 1 / ((n + 1) / n) = n / (n + 1) by XCMPLX_1:57;
( |.y.| == (|.y.| * (uReal . ((n + 1) / n))) * (uReal . (n / (n + 1))) & (|.y.| * (uReal . ((n + 1) / n))) * (uReal . (n / (n + 1))) < |.x.| * (uReal . (n / (n + 1))) ) by A1, A4, Lm2, A3, SURREALR:70;
then A5: ( |.(- y).| == |.y.| & |.y.| < |.x.| * (uReal . (n / (n + 1))) ) by SURREALO:4, Th39, Th38;
then |.(- y).| < |.x.| * (uReal . (n / (n + 1))) by SURREALO:4;
then - (|.x.| * (uReal . (n / (n + 1)))) < - |.(- y).| by SURREALR:10;
then A6: |.x.| + (- (|.x.| * (uReal . (n / (n + 1))))) < |.x.| + (- |.(- y).|) by SURREALR:44;
A7: ( - (|.x.| * (uReal . (n / (n + 1)))) = |.x.| * (- (uReal . (n / (n + 1)))) & |.x.| * (- (uReal . (n / (n + 1)))) == |.x.| * (uReal . (- (n / (n + 1)))) ) by SURREALN:56, SURREALR:51, SURREALR:58;
1 - (n / (n + 1)) = ((n + 1) / (n + 1)) - (n / (n + 1)) by XCMPLX_1:60
.= ((n + 1) - n) / (n + 1) by XCMPLX_1:120 ;
then A8: 1 + (- (n / (n + 1))) = 1 / (n + 1) ;
A9: |.x.| = |.x.| * (uReal . 1) by SURREALN:48;
( |.x.| + (- (|.x.| * (uReal . (n / (n + 1))))) == (|.x.| * (uReal . 1)) + (|.x.| * (uReal . (- (n / (n + 1))))) & (|.x.| * (uReal . 1)) + (|.x.| * (uReal . (- (n / (n + 1))))) == |.x.| * ((uReal . 1) + (uReal . (- (n / (n + 1))))) ) by A7, SURREALR:43, SURREALR:67, SURREALN:48;
then ( |.x.| + (- (|.x.| * (uReal . (n / (n + 1))))) == |.x.| * ((uReal . 1) + (uReal . (- (n / (n + 1))))) & |.x.| * ((uReal . 1) + (uReal . (- (n / (n + 1))))) == |.x.| * (uReal . (1 / (n + 1))) ) by A8, SURREALN:55, SURREALR:51, SURREALO:4;
then A10: |.x.| + (- (|.x.| * (uReal . (n / (n + 1))))) == |.x.| * (uReal . (1 / (n + 1))) by SURREALO:4;
n < n + 1 by NAT_1:13;
then n / (n + 1) < 1 by XREAL_1:189;
then ( |.x.| * (uReal . (n / (n + 1))) <= |.x.| * 1_No & |.x.| * 1_No = |.x.| ) by SURREALN:48, SURREALN:51, A2, SURREALR:70;
then A11: ( |.(- y).| == |.y.| & |.y.| < |.x.| ) by A5, SURREALO:4;
then ( |.(- y).| + 0_No = |.(- y).| & |.(- y).| < |.x.| ) by SURREALO:4;
then 0_No <= |.x.| - |.(- y).| by SURREALR:42;
then A12: |.(|.x.| + (- |.(- y).|)).| = |.x.| + (- |.(- y).|) by Def6;
A13: |.x.| * (uReal . (1 / (n + 1))) < |.(|.x.| + (- |.(- y).|)).| by A10, A12, A6, SURREALO:4;
A14: ( uInt . (n + 1) = uDyadic . (n + 1) & uDyadic . (n + 1) = uReal . (n + 1) ) by SURREALN:46, SURREALN:def 5;
A15: ( uInt . 2 = uDyadic . 2 & uDyadic . 2 = uReal . 2 ) by SURREALN:46, SURREALN:def 5;
A16: 0_No < uReal . (n + 1) by SURREALI:def 8;
A17: 1 / (1 / (n + 1)) = n + 1 by XCMPLX_1:56;
|.(|.x.| - |.(- y).|).| <= |.(x - (- y)).| by Th49;
then |.x.| * (uReal . (1 / (n + 1))) < |.(x + y).| by A13, SURREALO:4;
then ( |.x.| == (|.x.| * (uReal . (1 / (n + 1)))) * (uReal . (n + 1)) & (|.x.| * (uReal . (1 / (n + 1)))) * (uReal . (n + 1)) < |.(x + y).| * (uReal . (n + 1)) ) by A16, SURREALR:70, A17, Lm2;
then A18: |.x.| < |.(x + y).| * (uInt . (n + 1)) by SURREALO:4, A14;
A19: |.y.| + |.x.| < |.x.| + |.x.| by A11, SURREALR:44;
(uReal . 1) + (uReal . 1) == uReal . (1 + 1) by SURREALN:55;
then ( |.x.| + |.x.| == |.x.| * ((uReal . 1) + (uReal . 1)) & |.x.| * ((uReal . 1) + (uReal . 1)) == |.x.| * (uReal . 2) ) by A9, SURREALR:67, SURREALR:51;
then |.x.| + |.x.| == |.x.| * (uReal . 2) by SURREALO:4;
then A20: |.y.| + |.x.| < |.x.| * (uReal . 2) by A19, SURREALO:4;
|.(x + y).| <= |.x.| + |.y.| by Th37;
then |.(x + y).| < |.x.| * (uInt . 2) by A15, A20, SURREALO:4;
hence |.x.|,|.(x + y).| are_commensurate by A18; :: thesis: verum