let x, y be ExtReal; :: thesis: ( ( ( 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 ; :: thesis: |.(x / y).| = |.x.| / |.y.|

reconsider y = y as R_eal by XXREAL_0:def 1;

assume that

A1: ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) and

A2: y <> 0 ; :: thesis: |.(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 ) )
;

end;

suppose A3:
x = +infty
; :: thesis: |.(x / y).| = |.x.| / |.y.|

A4:
-infty < y
by A1, A3, XXREAL_0:12, XXREAL_0:14;

end;per cases
( 0 < y or y < 0 )
by A2;

end;

suppose A5:
0 < y
; :: thesis: |.(x / y).| = |.x.| / |.y.|

then
x / y = +infty
by A3, A1, XXREAL_3:83;

then A6: |.(x / y).| = +infty by Def1;

|.y.| = y by A5, Def1;

hence |.(x / y).| = |.x.| / |.y.| by A3, A1, A5, A6, XXREAL_3:83; :: thesis: verum

end;then A6: |.(x / y).| = +infty by Def1;

|.y.| = y by A5, Def1;

hence |.(x / y).| = |.x.| / |.y.| by A3, A1, A5, A6, XXREAL_3:83; :: thesis: verum

suppose A7:
y < 0
; :: thesis: |.(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; :: thesis: verum

end;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; :: thesis: verum

suppose A9:
x = -infty
; :: thesis: |.(x / y).| = |.x.| / |.y.|

A10:
-infty < y
by A1, A9, XXREAL_0:12, XXREAL_0:14;

end;per cases
( 0 < y or y < 0 )
by A2;

end;

suppose A11:
0 < y
; :: thesis: |.(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; :: thesis: verum

end;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; :: thesis: verum

suppose A14:
y < 0
; :: thesis: |.(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; :: thesis: verum

end;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; :: thesis: verum

suppose
( x <> +infty & x <> -infty )
; :: thesis: |.(x / y).| = |.x.| / |.y.|

then reconsider a = x as Element of REAL by XXREAL_0:14;

end;per cases
( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) )
;

end;

suppose
y = +infty
; :: thesis: |.(x / y).| = |.x.| / |.y.|

then
( |.(x / y).| = 0 & |.y.| = +infty )
by Def1;

hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum

end;hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum

suppose
y = -infty
; :: thesis: |.(x / y).| = |.x.| / |.y.|

then
( |.(x / y).| = 0 & |.y.| = +infty )
by Def1, XXREAL_3:5;

hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum

end;hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum

suppose
( y <> +infty & y <> -infty )
; :: thesis: |.(x / y).| = |.x.| / |.y.|

then reconsider b = y as Element of REAL by XXREAL_0:14;

( |.x.| = |.a.| & |.y.| = |.b.| ) by Th1;

then A17: |.x.| / |.y.| = |.a.| / |.b.| ;

|.(x / y).| = |.(a / b).| by Th1;

hence |.(x / y).| = |.x.| / |.y.| by A17, COMPLEX1:67; :: thesis: verum

end;( |.x.| = |.a.| & |.y.| = |.b.| ) by Th1;

then A17: |.x.| / |.y.| = |.a.| / |.b.| ;

|.(x / y).| = |.(a / b).| by Th1;

hence |.(x / y).| = |.x.| / |.y.| by A17, COMPLEX1:67; :: thesis: verum