let x, y be Surreal; :: thesis: for r being Real
for s being Surreal st r <> 0 holds
( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y )
let r be Real; :: thesis: for s being Surreal st r <> 0 holds
( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y )
let s be Surreal; :: thesis: ( r <> 0 implies ( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y ) )
assume A1: r <> 0 ; :: thesis: ( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y )
set N = No_omega^ y;
set R = uReal . r;
set sRNx = (s + ((uReal . r) * (No_omega^ y))) + x;
set sRNs = (s + ((uReal . r) * (No_omega^ y))) + (- s);
s - s == 0_No by SURREALR:39;
then A2: ( (s + ((uReal . r) * (No_omega^ y))) + (- s) = ((uReal . r) * (No_omega^ y)) + (s + (- s)) & ((uReal . r) * (No_omega^ y)) + (s + (- s)) == ((uReal . r) * (No_omega^ y)) + 0_No & ((uReal . r) * (No_omega^ y)) + 0_No = (uReal . r) * (No_omega^ y) ) by SURREALR:43, SURREALR:37;
not (uReal . r) * (No_omega^ y) == 0_No by A1, Th67;
then A3: not (s + ((uReal . r) * (No_omega^ y))) + (- s) == 0_No by A2, SURREALO:4;
A4: |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).| is positive by A3, Th36;
A5: |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).|,|.((No_omega^ y) * (uReal . r)).| are_commensurate by A2, Th48, A4, Th8;
A6: |.((No_omega^ y) * (uReal . r)).|, No_omega^ y are_commensurate by A1, Th66;
then A7: |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).|, No_omega^ y are_commensurate by Th4, A5;
A8: ((s + ((uReal . r) * (No_omega^ y))) + x) + (- s) = (s + (((uReal . r) * (No_omega^ y)) + x)) + (- s) by SURREALR:37
.= (s + (- s)) + (((uReal . r) * (No_omega^ y)) + x) by SURREALR:37 ;
s - s == 0_No by SURREALR:39;
then A9: ( (s + (- s)) + (((uReal . r) * (No_omega^ y)) + x) == 0_No + (((uReal . r) * (No_omega^ y)) + x) & 0_No + (((uReal . r) * (No_omega^ y)) + x) = ((uReal . r) * (No_omega^ y)) + x ) by SURREALR:43;
((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x == ((uReal . r) * (No_omega^ y)) + x by A2, SURREALR:43;
then A10: ((s + ((uReal . r) * (No_omega^ y))) + x) + (- s) == ((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x by A9, SURREALO:4, A8;
A11: s + ((uReal . r) * (No_omega^ y)) is s,y,r _term by A1, Th69;
then A12: ( not (s + ((uReal . r) * (No_omega^ y))) + (- s) == 0_No & omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)) == y & omega-r ((s + ((uReal . r) * (No_omega^ y))) + (- s)) = r ) ;
thus ( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term implies |.x.| infinitely< No_omega^ y ) :: thesis: ( |.x.| infinitely< No_omega^ y implies (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term )

proof

assume A13: (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term ; :: thesis: |.x.| infinitely< No_omega^ y
then A14: ( not ((s + ((uReal . r) * (No_omega^ y))) + x) + (- s) == 0_No & omega-y (((s + ((uReal . r) * (No_omega^ y))) + x) + (- s)) == y & omega-r (((s + ((uReal . r) * (No_omega^ y))) + x) + (- s)) = r ) ;
A15: not ((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x == 0_No by A10, A14, SURREALO:4;
A16: ( omega-y (((s + ((uReal . r) * (No_omega^ y))) + x) + (- s)) = omega-y (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) & omega-r (((s + ((uReal . r) * (No_omega^ y))) + x) + (- s)) = omega-r (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) ) by A13, A10, Th70;
A17: omega-r (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) = omega-r ((s + ((uReal . r) * (No_omega^ y))) + (- s)) by A13, A11, A10, Th70;
omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)) == omega-y (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) by A14, A12, A16, SURREALO:4;
then omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)) = omega-y (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) by SURREALO:50;
hence |.x.| infinitely< No_omega^ y by A7, Th16, A17, A15, A11, Th62; :: thesis: verum

end;

assume |.x.| infinitely< No_omega^ y ; :: thesis: (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term
then |.x.| infinitely< |.((s + ((uReal . r) * (No_omega^ y))) + (- s)).| by A6, Th4, A5, Th16;
then A18: ( not ((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x == 0_No & omega-y ((s + ((uReal . r) * (No_omega^ y))) + (- s)) = omega-y (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) & omega-r ((s + ((uReal . r) * (No_omega^ y))) + (- s)) = omega-r (((s + ((uReal . r) * (No_omega^ y))) + (- s)) + x) ) by Th63;
then not ((s + ((uReal . r) * (No_omega^ y))) + x) + (- s) == 0_No by A10, SURREALO:4;
hence (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term by A18, A10, Th70, A11; :: thesis: verum