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;
per cases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
suppose A3: x = +infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|
A4: -infty < y by ;
per cases ( 0 < y or y < 0 ) by A2;
suppose A5: 0 < y ; :: thesis: |.(x / y).| = |.x.| / |.y.|
then x / y = +infty by ;
then A6: |.(x / y).| = +infty by Def1;
|.y.| = y by ;
hence |.(x / y).| = |.x.| / |.y.| by ; :: thesis: verum
end;
suppose A7: y < 0 ; :: thesis: |.(x / y).| = |.x.| / |.y.|
then |.y.| = - y by Def1;
then A8: |.y.| < +infty by ;
x / y = -infty by ;
then |.(x / y).| = +infty by ;
hence |.(x / y).| = |.x.| / |.y.| by ; :: thesis: verum
end;
end;
end;
suppose A9: x = -infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|
A10: -infty < y by ;
per cases ( 0 < y or y < 0 ) by A2;
end;
end;
suppose ( x <> +infty & x <> -infty ) ; :: thesis: |.(x / y).| = |.x.| / |.y.|
then reconsider a = x as Element of REAL by XXREAL_0:14;
per cases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
suppose y = -infty ; :: thesis: |.(x / y).| = |.x.| / |.y.|
then ( |.(x / y).| = 0 & |.y.| = +infty ) by ;
hence |.(x / y).| = |.x.| / |.y.| ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
end;
end;
end;