let x, y, z be R_eal; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( ex a, b being Real st
( x = a & y = b & x * y = a * b ) or ( 0. < x & y = +infty & x * y = +infty ) or ( 0. < y & x = +infty & x * y = +infty ) or ( x < 0. & y = -infty & x * y = +infty ) or ( y < 0. & x = -infty & x * y = +infty ) or ( x < 0. & y = +infty & x * y = -infty ) or ( y < 0. & x = +infty & x * y = -infty ) or ( 0. < x & y = -infty & x * y = -infty ) or ( 0. < y & x = -infty & x * y = -infty ) or ( x = 0. & x * y = 0. ) or ( y = 0. & x * y = 0. ) ) by Def1;

suppose ex a, b being Real st
( x = a & y = b & x * y = a * b ) ; :: thesis: (x * y) * z = x * (y * z)

then consider a, b being Real such that
A1: ( x = a & y = b & x * y = a * b ) ;

now

per cases ( ex b1, c being Real st
( y = b1 & z = c & y * z = b1 * c ) or ( 0. < y & z = +infty & y * z = +infty ) or ( y < 0. & z = -infty & y * z = +infty ) or ( y < 0. & z = +infty & y * z = -infty ) or ( 0. < y & z = -infty & y * z = -infty ) or ( y = 0. & y * z = 0. ) or ( z = 0. & y * z = 0. ) ) by A1, Def1;

suppose ex b1, c being Real st
( y = b1 & z = c & y * z = b1 * c ) ; :: thesis: (x * y) * z = x * (y * z)

then consider b1, c being Real such that
A2: ( y = b1 & z = c & y * z = b1 * c ) ;
A3: (x * y) * z = (a * b) * c by A1, A2, Th13;
x * (y * z) = a * (b * c) by A1, A2, Th13;
hence (x * y) * z = x * (y * z) by A3; :: thesis: verum

end;

suppose A4: ( 0. < y & z = +infty & y * z = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( a > 0 or a = 0 or a < 0 ) ;

suppose A5: a > 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b > 0 by A1, A4, XREAL_1:131;
then (x * y) * z = +infty by A1, A4, Def1;
hence (x * y) * z = x * (y * z) by A1, A4, A5, Def1; :: thesis: verum

end;

suppose A6: a = 0 ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by A1, Def1;
hence (x * y) * z = x * (y * z) by A1, A6, Def1; :: thesis: verum

end;

suppose A7: a < 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b < 0 by A1, A4, XREAL_1:134;
then (x * y) * z = -infty by A1, A4, Def1;
hence (x * y) * z = x * (y * z) by A1, A4, A7, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A8: ( y < 0. & z = -infty & y * z = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( a > 0 or a = 0 or a < 0 ) ;

suppose A9: a > 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b < 0 by A1, A8, XREAL_1:134;
then (x * y) * z = +infty by A1, A8, Def1;
hence (x * y) * z = x * (y * z) by A1, A8, A9, Def1; :: thesis: verum

end;

suppose A10: a = 0 ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by A1, Def1;
hence (x * y) * z = x * (y * z) by A1, A10, Def1; :: thesis: verum

end;

suppose A11: a < 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b > 0 by A1, A8, XREAL_1:132;
then (x * y) * z = -infty by A1, A8, Def1;
hence (x * y) * z = x * (y * z) by A1, A8, A11, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A12: ( y < 0. & z = +infty & y * z = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( a > 0 or a = 0 or a < 0 ) ;

suppose A13: a > 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b < 0 by A1, A12, XREAL_1:134;
then (x * y) * z = -infty by A1, A12, Def1;
hence (x * y) * z = x * (y * z) by A1, A12, A13, Def1; :: thesis: verum

end;

suppose A14: a = 0 ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by A1, Def1;
hence (x * y) * z = x * (y * z) by A1, A14, Def1; :: thesis: verum

end;

suppose A15: a < 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b > 0 by A1, A12, XREAL_1:132;
then (x * y) * z = +infty by A1, A12, Def1;
hence (x * y) * z = x * (y * z) by A1, A12, A15, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A16: ( 0. < y & z = -infty & y * z = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( a > 0 or a = 0 or a < 0 ) ;

suppose A17: a > 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b > 0 by A1, A16, XREAL_1:131;
then (x * y) * z = -infty by A1, A16, Def1;
hence (x * y) * z = x * (y * z) by A1, A16, A17, Def1; :: thesis: verum

end;

suppose A18: a = 0 ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by A1, Def1;
hence (x * y) * z = x * (y * z) by A1, A18, Def1; :: thesis: verum

end;

suppose A19: a < 0 ; :: thesis: (x * y) * z = x * (y * z)

then a * b < 0 by A1, A16, XREAL_1:134;
then (x * y) * z = +infty by A1, A16, Def1;
hence (x * y) * z = x * (y * z) by A1, A16, A19, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A20: ( y = 0. & y * z = 0. ) ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by Def1;
hence (x * y) * z = x * (y * z) by A20, Def1; :: thesis: verum

end;

suppose A21: ( z = 0. & y * z = 0. ) ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by Def1;
hence (x * y) * z = x * (y * z) by A21, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A22: ( 0. < x & y = +infty & x * y = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then y * z = +infty by A22, Def1;
hence (x * y) * z = x * (y * z) by A22; :: thesis: verum

end;

suppose A23: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A24: (x * y) * z = 0. by Def1;
y * z = 0. by A23, Def1;
hence (x * y) * z = x * (y * z) by A24, Def1; :: thesis: verum

end;

suppose z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then y * z = -infty by A22, Def1;
hence (x * y) * z = x * (y * z) by A22, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A25: ( 0. < y & x = +infty & x * y = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A26: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then A27: (x * y) * z = +infty by A25, Def1;
0. < y * z by A25, A26, Th20;
hence (x * y) * z = x * (y * z) by A25, A27, Def1; :: thesis: verum

end;

suppose A28: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A29: (x * y) * z = 0. by Def1;
y * z = 0. by A28, Def1;
hence (x * y) * z = x * (y * z) by A29, Def1; :: thesis: verum

end;

suppose A30: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A31: (x * y) * z = -infty by A25, Def1;
y * z < 0. by A25, A30, Th21;
hence (x * y) * z = x * (y * z) by A25, A31, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A32: ( x < 0. & y = -infty & x * y = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A33: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = +infty by A32, Def1;
hence (x * y) * z = x * (y * z) by A32, A33, Def1; :: thesis: verum

end;

suppose A34: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A35: (x * y) * z = 0. by Def1;
y * z = 0. by A34, Def1;
hence (x * y) * z = x * (y * z) by A35, Def1; :: thesis: verum

end;

suppose A36: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A37: (x * y) * z = -infty by A32, Def1;
y * z = +infty by A32, A36, Def1;
hence (x * y) * z = x * (y * z) by A32, A37, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A38: ( y < 0. & x = -infty & x * y = +infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A39: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then A40: (x * y) * z = +infty by A38, Def1;
y * z < 0. by A38, A39, Th21;
hence (x * y) * z = x * (y * z) by A38, A40, Def1; :: thesis: verum

end;

suppose A41: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A42: (x * y) * z = 0. by Def1;
y * z = 0. by A41, Def1;
hence (x * y) * z = x * (y * z) by A42, Def1; :: thesis: verum

end;

suppose A43: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A44: (x * y) * z = -infty by A38, Def1;
0. < y * z by A38, A43, Th20;
hence (x * y) * z = x * (y * z) by A38, A44, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A45: ( x < 0. & y = +infty & x * y = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A46: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then y * z = +infty by A45, Def1;
hence (x * y) * z = x * (y * z) by A45, A46, Def1; :: thesis: verum

end;

suppose A47: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A48: (x * y) * z = 0. by Def1;
y * z = 0. by A47, Def1;
hence (x * y) * z = x * (y * z) by A48, Def1; :: thesis: verum

end;

suppose A49: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A50: (x * y) * z = +infty by A45, Def1;
y * z = -infty by A45, A49, Def1;
hence (x * y) * z = x * (y * z) by A45, A50, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A51: ( y < 0. & x = +infty & x * y = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A52: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then A53: (x * y) * z = -infty by A51, Def1;
y * z < 0. by A51, A52, Th21;
hence (x * y) * z = x * (y * z) by A51, A53, Def1; :: thesis: verum

end;

suppose A54: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A55: (x * y) * z = 0. by Def1;
y * z = 0. by A54, Def1;
hence (x * y) * z = x * (y * z) by A55, Def1; :: thesis: verum

end;

suppose A56: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A57: (x * y) * z = +infty by A51, Def1;
0. < y * z by A51, A56, Th20;
hence (x * y) * z = x * (y * z) by A51, A57, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A58: ( 0. < x & y = -infty & x * y = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then y * z = -infty by A58, Def1;
hence (x * y) * z = x * (y * z) by A58; :: thesis: verum

end;

suppose A59: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A60: (x * y) * z = 0. by Def1;
y * z = 0. by A59, Def1;
hence (x * y) * z = x * (y * z) by A60, Def1; :: thesis: verum

end;

suppose z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then y * z = +infty by A58, Def1;
hence (x * y) * z = x * (y * z) by A58, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A61: ( 0. < y & x = -infty & x * y = -infty ) ; :: thesis: (x * y) * z = x * (y * z)

now

per cases ( 0. < z or 0. = z or z < 0. ) ;

suppose A62: 0. < z ; :: thesis: (x * y) * z = x * (y * z)

then A63: (x * y) * z = -infty by A61, Def1;
0. < y * z by A61, A62, Th20;
hence (x * y) * z = x * (y * z) by A61, A63, Def1; :: thesis: verum

end;

suppose A64: 0. = z ; :: thesis: (x * y) * z = x * (y * z)

then A65: (x * y) * z = 0. by Def1;
y * z = 0. by A64, Def1;
hence (x * y) * z = x * (y * z) by A65, Def1; :: thesis: verum

end;

suppose A66: z < 0. ; :: thesis: (x * y) * z = x * (y * z)

then A67: (x * y) * z = +infty by A61, Def1;
y * z < 0. by A61, A66, Th21;
hence (x * y) * z = x * (y * z) by A61, A67, Def1; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

suppose A68: ( x = 0. & x * y = 0. ) ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by Def1;
hence (x * y) * z = x * (y * z) by A68, Def1; :: thesis: verum

end;

suppose A69: ( y = 0. & x * y = 0. ) ; :: thesis: (x * y) * z = x * (y * z)

then (x * y) * z = 0. by Def1;
hence (x * y) * z = x * (y * z) by A69; :: thesis: verum

end;

end;

end;

hence (x * y) * z = x * (y * z) ; :: thesis: verum