let x, y, z be ExtReal; :: thesis: ( x <= y & 0 <= z implies x * z <= y * z )
assume that
A1: x <= y and
A2: 0 <= z ; :: thesis: x * z <= y * z
per cases ( z = 0 or z > 0 ) by A2;
suppose z = 0 ; :: thesis: x * z <= y * z
hence x * z <= y * z ; :: thesis: verum
end;
suppose A3: z > 0 ; :: thesis: x * z <= y * z
per cases ( x = 0 or x <> 0 ) ;
suppose A4: x = 0 ; :: thesis: x * z <= y * z
then z * y >= 0 by A1, A2;
hence x * z <= y * z by A4; :: thesis: verum
end;
suppose A5: x <> 0 ; :: thesis: x * z <= y * z
per cases ( ( x * z in REAL & y * z in REAL ) or not x * z in REAL or not y * z in REAL ) ;
:: according to XXREAL_3:def 1
case A6: ( x * z in REAL & y * z in REAL ) ; :: thesis: ex p, q being Element of REAL st
( p = x * z & q = y * z & p <= q )
( y * z = 0 implies y = 0 ) by A3;
then reconsider x = x, y = y, z = z as Element of REAL by A3, A5, A6, Lm23;
reconsider p = x * z, q = y * z as Element of REAL by XREAL_0:def 1;
take p ; :: thesis: ex q being Element of REAL st
( p = x * z & q = y * z & p <= q )
take q ; :: thesis: ( p = x * z & q = y * z & p <= q )
thus ( p = x * z & q = y * z & p <= q ) by A1, A2, XREAL_1:64; :: thesis: verum
end;
case A7: ( not x * z in REAL or not y * z in REAL ) ; :: thesis: ( x * z = -infty or y * z = +infty )
per cases ( not x * z in REAL or not y * z in REAL ) by A7;
suppose A8: not x * z in REAL ; :: thesis: ( x * z = -infty or y * z = +infty )
per cases ( x * z = -infty or x * z = +infty ) by A8, XXREAL_0:14;
suppose x * z = -infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) ; :: thesis: verum
end;
suppose x * z = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
then A9: x <> -infty by A3;
A10: ( not x in REAL or not y in REAL or not z in REAL ) by A8, XREAL_0:def 1;
per cases ( y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A9, A10, XXREAL_0:14;
suppose y = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; :: thesis: verum
end;
suppose that A11: not z in REAL and
( x in REAL & y in REAL ) ; :: thesis: ( x * z = -infty or y * z = +infty )
A12: z = +infty by A3, A11, XXREAL_0:14;
per cases ( x < 0 or 0 < x ) by A5;
suppose x < 0 ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A12, Def5; :: thesis: verum
end;
suppose 0 < x ; :: thesis: ( x * z = -infty or y * z = +infty )
then 0 < y by A1;
hence ( x * z = -infty or y * z = +infty ) by A12, Def5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose not y * z in REAL ; :: thesis: ( x * z = -infty or y * z = +infty )
then A13: ( not x in REAL or not y in REAL or not z in REAL ) by XREAL_0:def 1;
per cases ( x = -infty or y = +infty or x = +infty or y = -infty or ( not z in REAL & x in REAL & y in REAL ) ) by A13, XXREAL_0:14;
suppose x = -infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; :: thesis: verum
end;
suppose y = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def5; :: thesis: verum
end;
suppose that A14: not z in REAL and
( x in REAL & y in REAL ) ; :: thesis: ( x * z = -infty or y * z = +infty )
A15: z = +infty by A3, A14, XXREAL_0:14;
per cases ( x < 0 or 0 < x ) by A5;
suppose x < 0 ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A15, Def5; :: thesis: verum
end;
suppose 0 < x ; :: thesis: ( x * z = -infty or y * z = +infty )
then 0 < y by A1;
hence ( x * z = -infty or y * z = +infty ) by A15, Def5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;