let x be Surreal; :: thesis: for r being Real st x is positive & r > 0 holds
(uReal . r) * x,x are_commensurate
let r be Real; :: thesis: ( x is positive & r > 0 implies (uReal . r) * x,x are_commensurate )
assume A1: ( x is positive & r > 0 ) ; :: thesis: (uReal . r) * x,x are_commensurate
consider n being Nat such that
A2: r < n by SEQ_4:3;
n < n + 1 by NAT_1:13;
then A3: r < n + 1 by A2, XXREAL_0:2;
( uReal . (n + 1) = uDyadic . (n + 1) & uDyadic . (n + 1) = uInt . (n + 1) ) by SURREALN:46, SURREALN:def 5;
then A4: (uReal . r) * x < x * (uInt . (n + 1)) by A3, SURREALN:51, SURREALR:70, A1;
consider k being Nat such that
A5: 1 / r < k by SEQ_4:3;
k < k + 1 by NAT_1:13;
then A6: 1 / r < k + 1 by A5, XXREAL_0:2;
0_No < (uReal . r) * x by A1, SURREALI:def 8;
then A7: (uReal . (1 / r)) * ((uReal . r) * x) < (uReal . (k + 1)) * ((uReal . r) * x) by A6, SURREALN:51, SURREALR:70;
A8: ( uReal . (k + 1) = uDyadic . (k + 1) & uDyadic . (k + 1) = uInt . (k + 1) ) by SURREALN:46, SURREALN:def 5;
(uReal . (1 / r)) * ((uReal . r) * x) == x by Lm2, A1;
then x < ((uReal . r) * x) * (uInt . (k + 1)) by A8, A7, SURREALO:4;
hence (uReal . r) * x,x are_commensurate by A4; :: thesis: verum