let x1, x2, y, z be Surreal; :: thesis: ( not x2 == 0_No & y = x1 * (x2 ") implies ( ( y * y < z implies x1 * x1 < z * (x2 * x2) ) & ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) ) )
assume A1: ( not x2 == 0_No & y = x1 * (x2 ") ) ; :: thesis: ( ( y * y < z implies x1 * x1 < z * (x2 * x2) ) & ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) )
x2 * (x2 ") == 1_No by A1, SURREALI:33;
then ( (x2 * (x2 ")) * (x2 * (x2 ")) == 1_No * (x2 * (x2 ")) & 1_No * (x2 * (x2 ")) == 1_No * 1_No & 1_No * 1_No = 1_No ) by SURREALR:54;
then A2: (x2 * (x2 ")) * (x2 * (x2 ")) == 1_No by SURREALO:4;
( ((x2 ") * (x2 ")) * (x2 * x2) == (x2 ") * ((x2 ") * (x2 * x2)) & (x2 ") * ((x2 ") * (x2 * x2)) == (x2 ") * (((x2 ") * x2) * x2) ) by SURREALR:54, SURREALR:69;
then ( ((x2 ") * (x2 ")) * (x2 * x2) == (x2 ") * (((x2 ") * x2) * x2) & (x2 ") * (((x2 ") * x2) * x2) == ((x2 ") * x2) * ((x2 ") * x2) ) by SURREALO:4, SURREALR:69;
then ((x2 ") * (x2 ")) * (x2 * x2) == ((x2 ") * x2) * ((x2 ") * x2) by SURREALO:4;
then A3: ((x2 ") * (x2 ")) * (x2 * x2) == 1_No by A2, SURREALO:4;
( y * y == x1 * ((x2 ") * ((x2 ") * x1)) & x1 * ((x2 ") * ((x2 ") * x1)) == x1 * (x1 * ((x2 ") * (x2 "))) ) by SURREALR:54, SURREALR:69, A1;
then ( y * y == x1 * (x1 * ((x2 ") * (x2 "))) & x1 * (x1 * ((x2 ") * (x2 "))) == (x1 * x1) * ((x2 ") * (x2 ")) ) by SURREALO:4, SURREALR:69;
then y * y == (x1 * x1) * ((x2 ") * (x2 ")) by SURREALO:4;
then ( (y * y) * (x2 * x2) == ((x1 * x1) * ((x2 ") * (x2 "))) * (x2 * x2) & ((x1 * x1) * ((x2 ") * (x2 "))) * (x2 * x2) == (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) ) by SURREALR:54, SURREALR:69;
then ( (y * y) * (x2 * x2) == (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) & (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) == (x1 * x1) * 1_No & (x1 * x1) * 1_No = x1 * x1 ) by A3, SURREALO:4, SURREALR:54;
then A4: (y * y) * (x2 * x2) == x1 * x1 by SURREALO:4;
A5: 0_No < x2 * x2 by A1, SURREALR:72;
thus ( y * y < z implies x1 * x1 < z * (x2 * x2) ) :: thesis: ( ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) )

proof

assume y * y < z ; :: thesis: x1 * x1 < z * (x2 * x2)
then (y * y) * (x2 * x2) < z * (x2 * x2) by A5, SURREALR:70;
hence x1 * x1 < z * (x2 * x2) by A4, SURREALO:4; :: thesis: verum

end;

A6: 0_No <= x2 * x2 by A1, SURREALR:72;
thus ( x1 * x1 < z * (x2 * x2) implies y * y < z ) :: thesis: ( z < y * y iff z * (x2 * x2) < x1 * x1 )

proof

assume x1 * x1 < z * (x2 * x2) ; :: thesis: y * y < z
then (y * y) * (x2 * x2) < z * (x2 * x2) by A4, SURREALO:4;
hence y * y < z by A6, SURREALR:75; :: thesis: verum

end;

thus ( z < y * y implies z * (x2 * x2) < x1 * x1 ) :: thesis: ( z * (x2 * x2) < x1 * x1 implies z < y * y )

proof

assume z < y * y ; :: thesis: z * (x2 * x2) < x1 * x1
then z * (x2 * x2) < (y * y) * (x2 * x2) by A5, SURREALR:70;
hence z * (x2 * x2) < x1 * x1 by A4, SURREALO:4; :: thesis: verum

end;

assume z * (x2 * x2) < x1 * x1 ; :: thesis: z < y * y
then z * (x2 * x2) < (y * y) * (x2 * x2) by A4, SURREALO:4;
hence z < y * y by A6, SURREALR:75; :: thesis: verum