:: EXTREAL2 semantic presentation

begin

     begin

theorem Th1: :: EXTREAL2:1
for x being R_eal
for a being Real st x = a holds
|.x.| = abs a
proof
let x be R_eal; ::_thesis: for a being Real st x = a holds
|.x.| = abs a
let a be Real; ::_thesis: ( x = a implies |.x.| = abs a )
assume A1: x = a ; ::_thesis: |.x.| = abs a
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: |.x.| = abs a
then  |.x.| = a by A1, EXTREAL1:def_1;
hence  |.x.| = abs a by ABSVALUE:def_1; ::_thesis: verum
end;
supposeA2: not 0 <= x ; ::_thesis: |.x.| = abs a
then |.x.| = - x by EXTREAL1:4
.= - a by A1, SUPINF_2:2 ;
hence  |.x.| = abs a by A1, A2, ABSVALUE:def_1; ::_thesis: verum
end;
end;
end;

theorem :: EXTREAL2:2
for x being R_eal holds
( |.x.| = x or |.x.| = - x ) by EXTREAL1:def_1;

theorem :: EXTREAL2:3
for x being R_eal holds 0 <= |.x.| ;

theorem Th4: :: EXTREAL2:4
for x being R_eal st x <> 0 holds
0 < |.x.|
proof
let x be R_eal; ::_thesis: ( x <> 0 implies 0 < |.x.| )
assume A1: x <> 0 ; ::_thesis: 0 < |.x.|
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: 0 < |.x.|
hence  0 < |.x.| by A1, EXTREAL1:def_1; ::_thesis: verum
end;
supposeA2: not 0 <= x ; ::_thesis: 0 < |.x.|
then  0 < - x ;
hence  0 < |.x.| by A2, EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;

theorem :: EXTREAL2:5
for x being R_eal holds
( x = 0 iff |.x.| = 0 ) by Th4, EXTREAL1:def_1;

theorem :: EXTREAL2:6
for x being R_eal st |.x.| = - x & x <> 0 holds
x < 0 ;

theorem Th7: :: EXTREAL2:7
for x being R_eal st x <= 0 holds
|.x.| = - x
proof
let x be R_eal; ::_thesis: ( x <= 0 implies |.x.| = - x )
assume A1: x <= 0 ; ::_thesis: |.x.| = - x
percases ( x < 0 or x = 0 ) by A1;
suppose x < 0 ; ::_thesis: |.x.| = - x
hence  |.x.| = - x by EXTREAL1:def_1; ::_thesis: verum
end;
supposeA2: x = 0 ; ::_thesis: |.x.| = - x
then  - 0 = - x ;
hence  |.x.| = - x by A2, EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;

theorem :: EXTREAL2:8
for x, y being R_eal holds |.(x * y).| = |.x.| * |.y.|
proof
let x, y be R_eal; ::_thesis: |.(x * y).| = |.x.| * |.y.|
percases ( x = 0 or 0 < x or x < 0 ) ;
suppose x = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then  ( |.x.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1;
hence  |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum
end;
supposeA1: 0 < x ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
percases ( y = 0 or 0 < y or y < 0 ) ;
suppose y = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then  ( |.y.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1;
hence  |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum
end;
suppose 0 < y ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then A2: |.y.| = y by EXTREAL1:def_1;
 |.x.| = x by A1, EXTREAL1:def_1;
hence  |.(x * y).| = |.x.| * |.y.| by A2, EXTREAL1:def_1; ::_thesis: verum
end;
supposeA3: y < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then A4: |.y.| = - y by EXTREAL1:def_1;
 |.x.| = x by A1, EXTREAL1:def_1;
then  |.x.| * |.y.| = - (x * y) by A4, XXREAL_3:92;
hence  |.(x * y).| = |.x.| * |.y.| by A1, A3, EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;
supposeA5: x < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
percases ( y = 0 or 0 < y or y < 0 ) ;
suppose y = 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then  ( |.y.| = 0 & |.(x * y).| = 0 ) by EXTREAL1:def_1;
hence  |.(x * y).| = |.x.| * |.y.| ; ::_thesis: verum
end;
supposeA6: 0 < y ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then  |.y.| = y by EXTREAL1:def_1;
then A7: |.x.| * |.y.| = (- x) * y by A5, EXTREAL1:def_1;
 |.(x * y).| = - (x * y) by A5, A6, EXTREAL1:def_1;
hence  |.(x * y).| = |.x.| * |.y.| by A7, XXREAL_3:92; ::_thesis: verum
end;
suppose y < 0 ; ::_thesis: |.(x * y).| = |.x.| * |.y.|
then  |.y.| = - y by EXTREAL1:def_1;
then  |.x.| * |.y.| = (- x) * (- y) by A5, EXTREAL1:def_1;
then |.x.| * |.y.| = - (x * (- y)) by XXREAL_3:92
.= - (- (x * y)) by XXREAL_3:92 ;
hence  |.(x * y).| = |.x.| * |.y.| by EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th9: :: EXTREAL2:9
for x being R_eal holds
( - |.x.| <= x & x <= |.x.| )
proof
let x be R_eal; ::_thesis: ( - |.x.| <= x & x <= |.x.| )
percases ( 0 <= x or not 0 <= x ) ;
supposeA1: 0 <= x ; ::_thesis: ( - |.x.| <= x & x <= |.x.| )
thus  ( - |.x.| <= x & x <= |.x.| ) by A1, EXTREAL1:def_1; ::_thesis: verum
end;
suppose not 0 <= x ; ::_thesis: ( - |.x.| <= x & x <= |.x.| )
then  |.x.| = - x by EXTREAL1:def_1;
hence  ( - |.x.| <= x & x <= |.x.| ) ; ::_thesis: verum
end;
end;
end;

theorem Th10: :: EXTREAL2:10
for x, y being R_eal st |.x.| < y holds
( - y < x & x < y )
proof
let x, y be R_eal; ::_thesis: ( |.x.| < y implies ( - y < x & x < y ) )
assume A1: |.x.| < y ; ::_thesis: ( - y < x & x < y )
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: ( - y < x & x < y )
hence  ( - y < x & x < y ) by A1, EXTREAL1:def_1; ::_thesis: verum
end;
supposeA2: not 0 <= x ; ::_thesis: ( - y < x & x < y )
then  |.x.| = - x by EXTREAL1:def_1;
hence  ( - y < x & x < y ) by A1, A2, XXREAL_3:60; ::_thesis: verum
end;
end;
end;

theorem Th11: :: EXTREAL2:11
for y, x being R_eal st - y < x & x < y holds
( 0 < y & |.x.| < y )
proof
let y, x be R_eal; ::_thesis: ( - y < x & x < y implies ( 0 < y & |.x.| < y ) )
assume that
A1: - y < x and
A2: x < y ; ::_thesis: ( 0 < y & |.x.| < y )
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: ( 0 < y & |.x.| < y )
hence  ( 0 < y & |.x.| < y ) by A2, EXTREAL1:def_1; ::_thesis: verum
end;
supposeA3: not 0 <= x ; ::_thesis: ( 0 < y & |.x.| < y )
 - x < y by A1, XXREAL_3:60;
hence  ( 0 < y & |.x.| < y ) by A3, EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;

theorem Th12: :: EXTREAL2:12
for y, x being R_eal holds
( ( - y <= x & x <= y ) iff |.x.| <= y )
proof
let y, x be R_eal; ::_thesis: ( ( - y <= x & x <= y ) iff |.x.| <= y )
A1: ( - y <= x & x <= y implies |.x.| <= y )
proof
assume that
A2: - y <= x and
A3: x <= y ; ::_thesis: |.x.| <= y
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: |.x.| <= y
hence  |.x.| <= y by A3, EXTREAL1:def_1; ::_thesis: verum
end;
supposeA4: not 0 <= x ; ::_thesis: |.x.| <= y
 - x <= y by A2, XXREAL_3:60;
hence  |.x.| <= y by A4, EXTREAL1:def_1; ::_thesis: verum
end;
end;
end;
 ( |.x.| <= y implies ( - y <= x & x <= y ) )
proof
assume A5: |.x.| <= y ; ::_thesis: ( - y <= x & x <= y )
percases ( |.x.| = y or |.x.| < y ) by A5, XXREAL_0:1;
suppose |.x.| = y ; ::_thesis: ( - y <= x & x <= y )
hence  ( - y <= x & x <= y ) by Th9; ::_thesis: verum
end;
suppose |.x.| < y ; ::_thesis: ( - y <= x & x <= y )
hence  ( - y <= x & x <= y ) by Th10; ::_thesis: verum
end;
end;
end;
hence  ( ( - y <= x & x <= y ) iff |.x.| <= y ) by A1; ::_thesis: verum
end;

theorem Th13: :: EXTREAL2:13
for x, y being R_eal holds |.(x + y).| <= |.x.| + |.y.|
proof
let x, y be R_eal; ::_thesis: |.(x + y).| <= |.x.| + |.y.|
A1: ( - |.x.| <= x & - |.y.| <= y ) by Th9;
A2: ( x <= |.x.| & y <= |.y.| ) by Th9;
A3: (- |.x.|) - |.y.| = - (|.x.| + |.y.|) by XXREAL_3:25;
 ( x + y <= |.x.| + |.y.| & (- |.x.|) + (- |.y.|) <= x + y ) by A1, A2, XXREAL_3:36;
hence  |.(x + y).| <= |.x.| + |.y.| by A3, Th12; ::_thesis: verum
end;

theorem Th14: :: EXTREAL2:14
for x being R_eal st -infty < x & x < +infty & x <> 0 holds
|.x.| * |.(1. / x).| = 1.
proof
let x be R_eal; ::_thesis: ( -infty < x & x < +infty & x <> 0 implies |.x.| * |.(1. / x).| = 1. )
assume that
A1: ( -infty < x & x < +infty ) and
A2: x <> 0 ; ::_thesis: |.x.| * |.(1. / x).| = 1.
reconsider a = x as Real by A1, XXREAL_0:14;
A3: 1. / x = 1 / a by EXTREAL1:2, MESFUNC1:def_8;
percases ( 0 <= x or not 0 <= x ) ;
suppose 0 <= x ; ::_thesis: |.x.| * |.(1. / x).| = 1.
then  ( |.x.| = a & |.(1. / x).| = 1 / a ) by A3, EXTREAL1:def_1;
then  |.x.| * |.(1. / x).| = a * (1 / a) by EXTREAL1:1;
hence  |.x.| * |.(1. / x).| = 1. by A2, MESFUNC1:def_8, XCMPLX_1:106; ::_thesis: verum
end;
supposeA4: not 0 <= x ; ::_thesis: |.x.| * |.(1. / x).| = 1.
then A5: |.x.| = - x by EXTREAL1:def_1
.= - a by SUPINF_2:2 ;
|.(1. / x).| = - (1. / x) by A3, A4, EXTREAL1:4, XREAL_1:142
.= - (1 / a) by A3, SUPINF_2:2 ;
then |.x.| * |.(1. / x).| = (- a) * (- (1 / a)) by A5, EXTREAL1:1
.= a * (1 / a) ;
hence  |.x.| * |.(1. / x).| = 1. by A4, MESFUNC1:def_8, XCMPLX_1:106; ::_thesis: verum
end;
end;
end;

theorem :: EXTREAL2:15
for x being R_eal st ( x = +infty or x = -infty ) holds
|.x.| * |.(1. / x).| = 0
proof
let x be R_eal; ::_thesis: ( ( x = +infty or x = -infty ) implies |.x.| * |.(1. / x).| = 0 )
assume  ( x = +infty or x = -infty ) ; ::_thesis: |.x.| * |.(1. / x).| = 0
then  |.(1. / x).| = 0 by EXTREAL1:def_1;
hence  |.x.| * |.(1. / x).| = 0 ; ::_thesis: verum
end;

theorem :: EXTREAL2:16
for x being R_eal st x <> 0 holds
|.(1. / x).| = 1. / |.x.|
proof
let x be R_eal; ::_thesis: ( x <> 0 implies |.(1. / x).| = 1. / |.x.| )
assume A1: x <> 0 ; ::_thesis: |.(1. / x).| = 1. / |.x.|
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
supposeA2: x = +infty ; ::_thesis: |.(1. / x).| = 1. / |.x.|
then  |.(1. / x).| = 0 by EXTREAL1:def_1;
hence  |.(1. / x).| = 1. / |.x.| by A2, EXTREAL1:3; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: |.(1. / x).| = 1. / |.x.|
then  ( |.(1. / x).| = 0 & |.x.| = +infty ) by EXTREAL1:def_1, XXREAL_3:5;
hence  |.(1. / x).| = 1. / |.x.| ; ::_thesis: verum
end;
supposeA3: ( x <> +infty & x <> -infty ) ; ::_thesis: |.(1. / x).| = 1. / |.x.|
A4: 0 < |.x.| by A1, Th4;
A5: x < +infty by A3, XXREAL_0:4;
 -infty <= x by XXREAL_0:5;
then A6: -infty < x by A3, XXREAL_0:1;
then  - +infty < x by XXREAL_3:def_3;
then A7: |.x.| < +infty by A5, Th11;
 |.(1. / x).| * |.x.| = 1. by A1, A6, A5, Th14;
hence  |.(1. / x).| = 1. / |.x.| by A4, A7, XXREAL_3:88; ::_thesis: verum
end;
end;
end;

theorem :: EXTREAL2:17
for x, y being R_eal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 holds
|.(x / y).| = |.x.| / |.y.|
proof
let x, y be R_eal; ::_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.|
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
supposeA3: x = +infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
A4: -infty < y by A1, A3, XXREAL_0:12, XXREAL_0:14;
percases ( 0 < y or y < 0 ) by A2;
supposeA5: 0 < y ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then  x / y = +infty by A3, A1, XXREAL_3:83;
then A6: |.(x / y).| = +infty by EXTREAL1:3;
 |.y.| = y by A5, EXTREAL1:3;
hence  |.(x / y).| = |.x.| / |.y.| by A3, A1, A5, A6, XXREAL_3:83; ::_thesis: verum
end;
supposeA7: y < 0 ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then  |.y.| = - y by EXTREAL1:4;
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 EXTREAL1:4, XXREAL_3:5;
hence  |.(x / y).| = |.x.| / |.y.| by A8, A2, A3, Th4, XXREAL_3:83; ::_thesis: verum
end;
end;
end;
supposeA9: x = -infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
A10: -infty < y by A1, A9, XXREAL_0:12, XXREAL_0:14;
percases ( 0 < y or y < 0 ) by A2;
supposeA11: 0 < y ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then A12: x / y = -infty by A9, A1, XXREAL_3:86;
A13: |.x.| = +infty by A9, EXTREAL1:4, XXREAL_3:5;
 |.y.| = y by A11, EXTREAL1:3;
hence  |.(x / y).| = |.x.| / |.y.| by A9, A1, A11, A12, A13, XXREAL_3:83; ::_thesis: verum
end;
supposeA14: y < 0 ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then  |.y.| = - y by EXTREAL1:4;
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, EXTREAL1:4, XXREAL_3:5;
hence  |.(x / y).| = |.x.| / |.y.| by A15, A16, XXREAL_3:83; ::_thesis: verum
end;
end;
end;
suppose ( x <> +infty & x <> -infty ) ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then reconsider a = x as Real by XXREAL_0:14;
percases ( 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 EXTREAL1:def_1;
hence  |.(x / y).| = |.x.| / |.y.| ; ::_thesis: verum
end;
suppose y = -infty ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then  ( |.(x / y).| = 0 & |.y.| = +infty ) by EXTREAL1:def_1, XXREAL_3:5;
hence  |.(x / y).| = |.x.| / |.y.| ; ::_thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.(x / y).| = |.x.| / |.y.|
then reconsider b = y as Real by XXREAL_0:14;
 ( |.x.| = abs a & |.y.| = abs b ) by Th1;
then A17: |.x.| / |.y.| = (abs a) / (abs b) by EXTREAL1:2;
 x / y = a / b by EXTREAL1:2;
then  |.(x / y).| = abs (a / b) by Th1;
hence  |.(x / y).| = |.x.| / |.y.| by A17, COMPLEX1:67; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th18: :: EXTREAL2:18
for x being R_eal holds |.x.| = |.(- x).|
proof
let x be R_eal; ::_thesis: |.x.| = |.(- x).|
percases ( 0 < x or x < 0 or x = 0 ) ;
suppose 0 < x ; ::_thesis: |.x.| = |.(- x).|
then |.(- x).| = - (- x) by EXTREAL1:4
.= x ;
hence  |.x.| = |.(- x).| ; ::_thesis: verum
end;
suppose x < 0 ; ::_thesis: |.x.| = |.(- x).|
then  |.x.| = - x by EXTREAL1:4;
hence  |.x.| = |.(- x).| ; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: |.x.| = |.(- x).|
hence  |.x.| = |.(- x).| ; ::_thesis: verum
end;
end;
end;

theorem Th19: :: EXTREAL2:19
( |.+infty.| = +infty & |.-infty.| = +infty )
proof
thus  |.+infty.| = +infty by EXTREAL1:3; ::_thesis: |.-infty.| = +infty
 - -infty = +infty by XXREAL_3:23;
hence  |.-infty.| = +infty by EXTREAL1:4; ::_thesis: verum
end;

theorem Th20: :: EXTREAL2:20
for x, y being R_eal st ( x is Real or y is Real ) holds
|.x.| - |.y.| <= |.(x - y).|
proof
let x, y be R_eal; ::_thesis: ( ( x is Real or y is Real ) implies |.x.| - |.y.| <= |.(x - y).| )
assume A1: ( x is Real or y is Real ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).|
percases ( y is Real or x is Real ) by A1;
supposeA2: y is Real ; ::_thesis: |.x.| - |.y.| <= |.(x - y).|
then  (x - y) + y = x by XXREAL_3:22;
then A3: |.x.| <= |.(x - y).| + |.y.| by Th13;
reconsider b = y as Real by A2;
thus  |.x.| - |.y.| <= |.(x - y).| by A3, XXREAL_3:42; ::_thesis: verum
end;
suppose x is Real ; ::_thesis: |.x.| - |.y.| <= |.(x - y).|
then reconsider a = x as Real ;
A4: |.x.| = abs a by Th1;
percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
suppose ( y = +infty or y = -infty ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).|
hence  |.x.| - |.y.| <= |.(x - y).| by A4, Th19, XXREAL_3:13; ::_thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.x.| - |.y.| <= |.(x - y).|
then reconsider b = y as Real by XXREAL_0:14;
 x - y = a - b by SUPINF_2:3;
then A5: |.(x - y).| = abs (a - b) by Th1;
 |.y.| = abs b by Th1;
then  |.x.| - |.y.| = (abs a) - (abs b) by A4, SUPINF_2:3;
hence  |.x.| - |.y.| <= |.(x - y).| by A5, COMPLEX1:59; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: EXTREAL2:21
for x, y being R_eal holds |.(x - y).| <= |.x.| + |.y.|
proof
let x, y be R_eal; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
percases ( x = +infty or x = -infty or ( x <> +infty & x <> -infty ) ) ;
suppose ( x = +infty or x = -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
then  |.x.| + |.y.| = +infty by XXREAL_3:def_2, Th19;
hence  |.(x - y).| <= |.x.| + |.y.| by XXREAL_0:3; ::_thesis: verum
end;
supposeA1: ( x <> +infty & x <> -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
then reconsider a = x as Real by XXREAL_0:14;
percases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;
supposeA2: y = +infty ; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
 x - y = -infty by A1, A2, XXREAL_3:13;
hence  |.(x - y).| <= |.x.| + |.y.| by A2, Th19, XXREAL_3:def_2; ::_thesis: verum
end;
supposeA3: y = -infty ; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
 x - y = +infty by A1, A3, XXREAL_3:14;
hence  |.(x - y).| <= |.x.| + |.y.| by A3, Th19, XXREAL_3:def_2; ::_thesis: verum
end;
suppose ( y <> +infty & y <> -infty ) ; ::_thesis: |.(x - y).| <= |.x.| + |.y.|
then reconsider b = y as Real by XXREAL_0:14;
 ( |.x.| = abs a & |.y.| = abs b ) by Th1;
then A4: |.x.| + |.y.| = (abs a) + (abs b) by SUPINF_2:1;
 x - y = a - b by SUPINF_2:3;
then  |.(x - y).| = abs (a - b) by Th1;
hence  |.(x - y).| <= |.x.| + |.y.| by A4, COMPLEX1:57; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: EXTREAL2:22
canceled;

theorem :: EXTREAL2:23
for x, z, y, w being R_eal st |.x.| <= z & |.y.| <= w holds
|.(x + y).| <= z + w
proof
let x, z, y, w be R_eal; ::_thesis: ( |.x.| <= z & |.y.| <= w implies |.(x + y).| <= z + w )
assume A1: ( |.x.| <= z & |.y.| <= w ) ; ::_thesis: |.(x + y).| <= z + w
then  ( - z <= x & - w <= y ) by Th12;
then A2: (- z) + (- w) <= x + y by XXREAL_3:36;
 ( x <= z & y <= w ) by A1, Th12;
then A3: x + y <= z + w by XXREAL_3:36;
 (- z) - w = - (z + w) by XXREAL_3:25;
hence  |.(x + y).| <= z + w by A3, A2, Th12; ::_thesis: verum
end;

theorem :: EXTREAL2:24
for x, y being R_eal st ( x is Real or y is Real ) holds
|.(|.x.| - |.y.|).| <= |.(x - y).|
proof
let x, y be R_eal; ::_thesis: ( ( x is Real or y is Real ) implies |.(|.x.| - |.y.|).| <= |.(x - y).| )
A1: |.y.| - |.x.| = - (|.x.| - |.y.|) by XXREAL_3:26;
assume A2: ( x is Real or y is Real ) ; ::_thesis: |.(|.x.| - |.y.|).| <= |.(x - y).|
then A3: |.x.| - |.y.| <= |.(x - y).| by Th20;
 y - x = - (x - y) by XXREAL_3:26;
then A4: |.(y - x).| = |.(x - y).| by Th18;
 |.y.| - |.x.| <= |.(y - x).| by A2, Th20;
then  - |.(x - y).| <= - (- (|.x.| - |.y.|)) by A4, A1, XXREAL_3:38;
hence  |.(|.x.| - |.y.|).| <= |.(x - y).| by A3, Th12; ::_thesis: verum
end;

theorem :: EXTREAL2:25
for x, y being R_eal st 0 <= x * y holds
|.(x + y).| = |.x.| + |.y.|
proof
let x, y be R_eal; ::_thesis: ( 0 <= x * y implies |.(x + y).| = |.x.| + |.y.| )
assume A1: 0 <= x * y ; ::_thesis: |.(x + y).| = |.x.| + |.y.|
percases ( ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) or ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ) by A1;
suppose ( ( 0 <= x or 0 < x ) & ( 0 <= y or 0 < y ) ) ; ::_thesis: |.(x + y).| = |.x.| + |.y.|
then  ( |.x.| = x & |.y.| = y ) by EXTREAL1:def_1;
hence  |.(x + y).| = |.x.| + |.y.| by EXTREAL1:def_1; ::_thesis: verum
end;
supposeA2: ( ( x <= 0 or x < 0 ) & ( y <= 0 or y < 0 ) ) ; ::_thesis: |.(x + y).| = |.x.| + |.y.|
then A3: |.(x + y).| = - (x + y) by Th7
.= (- x) - y by XXREAL_3:25 ;
 |.x.| = - x by A2, Th7;
hence  |.(x + y).| = |.x.| + |.y.| by A2, A3, Th7; ::_thesis: verum
end;
end;
end;

begin

theorem :: EXTREAL2:26
for x, y being R_eal st x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds
min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
proof
let x, y be R_eal; ::_thesis: ( x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) )
assume that
A1: x <> +infty and
A2: y <> +infty and
A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
percases ( x = -infty or x <> -infty ) ;
supposeA4: x = -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
then  ( x + y = -infty & x - y = -infty ) by A2, A3, XXREAL_3:14, XXREAL_3:def_2;
then A5: (x + y) - |.(x - y).| = -infty by XXREAL_3:14;
A6: min (x,y) = -infty by A4, XXREAL_0:44;
 R_EAL 2 = 2 by MEASURE6:def_1;
hence  min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A6, A5, XXREAL_3:86; ::_thesis: verum
end;
suppose x <> -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
then reconsider a = x as Real by A1, XXREAL_0:14;
percases ( y = -infty or y <> -infty ) ;
supposeA7: y = -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
then  ( x + y = -infty & x - y = +infty ) by A1, A3, XXREAL_3:14, XXREAL_3:def_2;
then A8: (x + y) - |.(x - y).| = -infty by XXREAL_3:14;
A9: min (x,y) = -infty by A7, XXREAL_0:44;
 R_EAL 2 = 2 by MEASURE6:def_1;
hence  min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by A9, A8, XXREAL_3:86; ::_thesis: verum
end;
suppose y <> -infty ; ::_thesis: min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2)
then reconsider b = y as Real by A2, XXREAL_0:14;
 x - y = a - b by SUPINF_2:3;
then  ( x + y = a + b & |.(x - y).| = abs (a - b) ) by Th1, SUPINF_2:1;
then A10: (x + y) - |.(x - y).| = (a + b) - (abs (a - b)) by SUPINF_2:3;
 R_EAL 2 = 2 by MEASURE6:def_1;
then  ((x + y) - |.(x - y).|) / (R_EAL 2) = ((a + b) - (abs (a - b))) / 2 by A10, EXTREAL1:2;
hence  min (x,y) = ((x + y) - |.(x - y).|) / (R_EAL 2) by COMPLEX1:73; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: EXTREAL2:27
for x, y being R_eal st x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds
max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
proof
let x, y be R_eal; ::_thesis: ( x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) implies max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) )
assume that
A1: x <> -infty and
A2: y <> -infty and
A3: ( not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) ) ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
percases ( x = +infty or x <> +infty ) ;
supposeA4: x = +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
then  ( x + y = +infty & x - y = +infty ) by A2, A3, XXREAL_3:13, XXREAL_3:def_2;
then A5: (x + y) + |.(x - y).| = +infty by XXREAL_3:def_2;
A6: max (x,y) = +infty by A4, XXREAL_0:41;
 R_EAL 2 = 2 by MEASURE6:def_1;
hence  max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by A6, A5, XXREAL_3:83; ::_thesis: verum
end;
suppose x <> +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
then reconsider a = x as Real by A1, XXREAL_0:14;
percases ( y = +infty or y <> +infty ) ;
supposeA7: y = +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
then  ( x + y = +infty & x - y = -infty ) by A1, A3, XXREAL_3:13, XXREAL_3:def_2;
then A8: (x + y) + |.(x - y).| = +infty by XXREAL_3:def_2;
A9: max (x,y) = +infty by A7, XXREAL_0:41;
 R_EAL 2 = 2 by MEASURE6:def_1;
hence  max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by A9, A8, XXREAL_3:83; ::_thesis: verum
end;
suppose y <> +infty ; ::_thesis: max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2)
then reconsider b = y as Real by A2, XXREAL_0:14;
 x - y = a - b by SUPINF_2:3;
then  ( x + y = a + b & |.(x - y).| = abs (a - b) ) by Th1, SUPINF_2:1;
then A10: (x + y) + |.(x - y).| = (a + b) + (abs (a - b)) by SUPINF_2:1;
 R_EAL 2 = 2 by MEASURE6:def_1;
then  ((x + y) + |.(x - y).|) / (R_EAL 2) = ((a + b) + (abs (a - b))) / 2 by A10, EXTREAL1:2;
hence  max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 2) by COMPLEX1:74; ::_thesis: verum
end;
end;
end;
end;
end;

definition
let x, y be R_eal;
:: original: max
redefine func max (x,y) ->  R_eal;
coherence
 max (x,y) is R_eal by XXREAL_0:def_1;
:: original: min
redefine func min (x,y) ->  R_eal;
coherence
 min (x,y) is R_eal by XXREAL_0:def_1;
end;

theorem :: EXTREAL2:28
for x, y being R_eal holds (min (x,y)) + (max (x,y)) = x + y
proof
let x, y be R_eal; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
percases ( x <= y or not x <= y ) ;
supposeA1: x <= y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
then  min (x,y) = x by XXREAL_0:def_9;
hence  (min (x,y)) + (max (x,y)) = x + y by A1, XXREAL_0:def_10; ::_thesis: verum
end;
supposeA2: not x <= y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
then  min (x,y) = y by XXREAL_0:def_9;
hence  (min (x,y)) + (max (x,y)) = x + y by A2, XXREAL_0:def_10; ::_thesis: verum
end;
end;
end;

begin

theorem Th29: :: EXTREAL2:29
for x being R_eal holds
( not |.x.| = +infty or x = +infty or x = -infty )
proof
let x be R_eal; ::_thesis: ( not |.x.| = +infty or x = +infty or x = -infty )
A1: ( |.x.| = x or - |.x.| = - (- x) ) by EXTREAL1:def_1;
assume  |.x.| = +infty ; ::_thesis: ( x = +infty or x = -infty )
hence  ( x = +infty or x = -infty ) by A1, XXREAL_3:5; ::_thesis: verum
end;

theorem :: EXTREAL2:30
for x being R_eal holds
( |.x.| < +infty iff x in REAL )
proof
let x be R_eal; ::_thesis: ( |.x.| < +infty iff x in REAL )
thus  ( |.x.| < +infty implies x in REAL ) by Th19, XXREAL_0:14; ::_thesis: ( x in REAL implies |.x.| < +infty )
assume A1: x in REAL ; ::_thesis: |.x.| < +infty
assume  |.x.| >= +infty ; ::_thesis: contradiction
hence  contradiction by A1, Th29, XXREAL_0:4; ::_thesis: verum
end;