let x, y be Surreal; :: thesis: ( ( ( x < 0_No & y < 0_No ) or ( 0_No < x & 0_No < y ) ) iff 0_No < x * y )
thus ( not 0_No < x * y or ( x < 0_No & y < 0_No ) or ( 0_No < x & 0_No < y ) ) :: thesis: ( ( ( x < 0_No & y < 0_No ) or ( 0_No < x & 0_No < y ) ) implies 0_No < x * y )

proof

assume that
A1: 0_No < x * y and
A2: ( ( not x < 0_No or not y < 0_No ) & ( not 0_No < x or not 0_No < y ) ) ; :: thesis: contradiction
A3: 0_No <= x * y by A1;
A4: ( 0_No < y or y < 0_No )

proof

assume ( not 0_No < y & not y < 0_No ) ; :: thesis: contradiction
then 0_No == y ;
then 0_No * x == x * y by Th51;
hence contradiction by A1; :: thesis: verum

end;

per cases ( x == 0_No or 0_No < x or x < 0_No ) ;

suppose x == 0_No ; :: thesis: contradiction

then 0_No * y == x * y by Th51;
hence contradiction by A1; :: thesis: verum

end;

suppose A5: 0_No < x ; :: thesis: contradiction

then - 0_No < - y by A2, A4, Th10;
then ( - 0_No = 0_No & 0_No < x * (- y) & x * (- y) = - (x * y) ) by A5, Lm9, Th58;
hence contradiction by A3, Th10; :: thesis: verum

end;

suppose A6: x < 0_No ; :: thesis: contradiction

then 0_No < - x by Th10, Th23;
then ( - 0_No = 0_No & 0_No < (- x) * y & (- x) * y = - (x * y) ) by A6, A2, A4, Lm9, Th58;
hence contradiction by Th10, A3; :: thesis: verum

end;

end;

end;

assume ( ( x < 0_No & y < 0_No ) or ( 0_No < x & 0_No < y ) ) ; :: thesis: 0_No < x * y

per cases then ( ( x < 0_No & y < 0_No ) or ( 0_No < x & 0_No < y ) ) ;

suppose ( x < 0_No & y < 0_No ) ; :: thesis: 0_No < x * y

then ( - 0_No < - x & - 0_No < - y & - 0_No = 0_No ) by Th10;
then ( 0_No < (- x) * (- y) & (- x) * (- y) = - ((- x) * y) ) by Lm9, Th58;
hence 0_No < x * y by Th58; :: thesis: verum

end;

suppose ( 0_No < x & 0_No < y ) ; :: thesis: 0_No < x * y

hence 0_No < x * y by Lm9; :: thesis: verum

end;

end;