let x, y be ExtReal; ( ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 implies |.(x / y).| = |.x.| / |.y.| )
assume that
A1:
( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) )
and
A2:
y <> 0
; |.(x / y).| = |.x.| / |.y.|
reconsider y = y as R_eal by XXREAL_0:def 1;
per cases
( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) )
;
suppose A3:
x = +infty
;
|.(x / y).| = |.x.| / |.y.|A4:
-infty < y
by A1, A3, XXREAL_0:12, XXREAL_0:14;
per cases
( 0 < y or y < 0 )
by A2;
suppose A7:
y < 0
;
|.(x / y).| = |.x.| / |.y.|then
|.y.| = - y
by Def1;
then A8:
|.y.| < +infty
by A4, XXREAL_3:5, XXREAL_3:38;
x / y = -infty
by A3, A1, A7, XXREAL_3:85;
then
|.(x / y).| = +infty
by Def1, XXREAL_3:5;
hence
|.(x / y).| = |.x.| / |.y.|
by A8, A2, A3, Th4, XXREAL_3:83;
verum end; end; end; suppose A9:
x = -infty
;
|.(x / y).| = |.x.| / |.y.|A10:
-infty < y
by A1, A9, XXREAL_0:12, XXREAL_0:14;
per cases
( 0 < y or y < 0 )
by A2;
suppose A11:
0 < y
;
|.(x / y).| = |.x.| / |.y.|then A12:
x / y = -infty
by A9, A1, XXREAL_3:86;
A13:
|.x.| = +infty
by A9, Def1, XXREAL_3:5;
|.y.| = y
by A11, Def1;
hence
|.(x / y).| = |.x.| / |.y.|
by A9, A1, A11, A12, A13, XXREAL_3:83;
verum end; suppose A14:
y < 0
;
|.(x / y).| = |.x.| / |.y.|then
|.y.| = - y
by Def1;
then A15:
|.y.| < +infty
by A10, XXREAL_3:5, XXREAL_3:38;
A16:
x / y = +infty
by A9, A1, A14, XXREAL_3:84;
(
0 < |.y.| &
|.x.| = +infty )
by A2, A9, Th4, Def1, XXREAL_3:5;
hence
|.(x / y).| = |.x.| / |.y.|
by A15, A16, XXREAL_3:83;
verum end; end; end; end;