let x, y, z be ext-real number ; :: 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 S: x = 0 ; :: thesis: x * z <= y * z
then z * y >= 0 by A1, A2;
hence x * z <= y * z by S; :: thesis: verum
end;
suppose SS: 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 that C1: x * z in REAL and
C2: 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 C1, LM1, A3, C2, SS;
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:66; :: thesis: verum
end;
case C: ( 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 C;
suppose C: not x * z in REAL ; :: thesis: ( x * z = -infty or y * z = +infty )
per cases ( x * z = -infty or x * z = +infty ) by C, 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 S: x * z = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
A: x <> -infty by S, A3;
pc: ( not x in REAL or not y in REAL or not z in REAL ) by C, 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 pc, XXREAL_0:14, A;
suppose y = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def4; :: thesis: verum
end;
suppose that S1: not z in REAL and
( x in REAL & y in REAL ) ; :: thesis: ( x * z = -infty or y * z = +infty )
G: z = +infty by A3, XXREAL_0:14, S1;
per cases ( x < 0 or 0 < x ) by SS;
suppose x < 0 ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by G, Def4; :: thesis: verum
end;
suppose 0 < x ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by G, Def4, A1; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose C: not y * z in REAL ; :: thesis: ( x * z = -infty or y * z = +infty )
pc: ( not x in REAL or not y in REAL or not z in REAL ) by C, 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 pc, XXREAL_0:14;
suppose x = -infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def4; :: thesis: verum
end;
suppose y = +infty ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by A3, Def4; :: thesis: verum
end;
suppose that S1: not z in REAL and
( x in REAL & y in REAL ) ; :: thesis: ( x * z = -infty or y * z = +infty )
G: z = +infty by A3, XXREAL_0:14, S1;
per cases ( x < 0 or 0 < x ) by SS;
suppose x < 0 ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by G, Def4; :: thesis: verum
end;
suppose 0 < x ; :: thesis: ( x * z = -infty or y * z = +infty )
hence ( x * z = -infty or y * z = +infty ) by G, Def4, A1; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;