:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received September 23, 2008
:: Copyright (c) 2008 Association of Mizar Users

definition

let x, y be ext-real number ;
func x + y -> ext-real number means :Def3: :: XXREAL_3:def 1
ex a, b being complex number st
( x = a & y = b & it = a + b ) if ( x is real & y is real )
it = +infty if ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) )
it = -infty if ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) )
otherwise it = 0 ;
existence
( ( x is real & y is real implies ex b₁ being ext-real number ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b₁ being ext-real number st b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b₁ being ext-real number st b₁ = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) & ex a, b being complex number st
( x = a & y = b & b₂ = a + b ) implies b₁ = b₂ ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or not b₁ = 0 or not b₂ = 0 or b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number holds
( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) iff b₁ = +infty ) ) & ( x is real & y is real & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) iff b₁ = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b₁ = +infty iff b₁ = -infty ) ) ) ;
commutativity
for b₁, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b₁ = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b₁ = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b₁ = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or b₁ = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b₁ = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b₁ = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b₁ = -infty ) & ( ( y is real & x is real ) or ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) or ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) or b₁ = 0 ) ) ;
func x * y -> ext-real number means :Def4: :: XXREAL_3:def 2
ex a, b being complex number st
( x = a & y = b & it = a * b ) if ( x is real & y is real )
it = +infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) )
it = -infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) )
otherwise it = 0 ;
existence
( ( x is real & y is real implies ex b₁ being ext-real number ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b₁ being ext-real number st b₁ = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b₁ being ext-real number st b₁ = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) & ex a, b being complex number st
( x = a & y = b & b₂ = a * b ) implies b₁ = b₂ ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number holds
( ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) iff b₁ = +infty ) ) & ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) iff b₁ = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b₁ = +infty iff b₁ = -infty ) ) ) ;
commutativity
for b₁, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b₁ = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies b₁ = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b₁ = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies b₁ = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b₁ = a * b ) ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is positive ) or ( y is negative & x is negative ) ) implies b₁ = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b₁ = -infty ) & ( ( not y is real or not x is real ) & ( ( y is real & x is real ) or ( not ( y is positive & x is positive ) & not ( y is negative & x is negative ) ) ) & ( ( y is real & x is real ) or ( not ( y is positive & x is negative ) & not ( y is negative & x is positive ) ) ) implies b₁ = 0 ) ) ;

end;

:: deftheorem Def3 defines + XXREAL_3:def 1 :

for x, y, b₃ being ext-real number holds
( ( x is real & y is real implies ( b₃ = x + y iff ex a, b being complex number st
( x = a & y = b & b₃ = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b₃ = x + y iff b₃ = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b₃ = x + y iff b₃ = -infty ) ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( b₃ = x + y iff b₃ = 0 ) ) );

:: deftheorem Def4 defines * XXREAL_3:def 2 :

for x, y, b₃ being ext-real number holds
( ( x is real & y is real implies ( b₃ = x * y iff ex a, b being complex number st
( x = a & y = b & b₃ = a * b ) ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( b₃ = x * y iff b₃ = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b₃ = x * y iff b₃ = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ( b₃ = x * y iff b₃ = 0 ) ) );

registration

let x, y be real number ;
let a, b be complex number ;
real set real set complex set complex set a₁ + a₂ a₃ + a₄ compatibility
( x = a & y = b implies x + y = a + b ) by Def3;
real set real set complex set complex set a₁ * a₂ a₃ * a₄ compatibility
( x = a & y = b implies x * y = a * b ) by Def4;

end;

definition

let x be ext-real number ;
func - x -> ext-real number means :Def5: :: XXREAL_3:def 3
ex a being complex number st
( x = a & it = - a ) if x is real
it = -infty if x = +infty
otherwise it = +infty ;
existence
( ( x is real implies ex b₁ being ext-real number ex a being complex number st
( x = a & b₁ = - a ) ) & ( x = +infty implies ex b₁ being ext-real number st b₁ = -infty ) & ( not x is real & not x = +infty implies ex b₁ being ext-real number st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b₁ = - a ) & ex a being complex number st
( x = a & b₂ = - a ) implies b₁ = b₂ ) & ( x = +infty & b₁ = -infty & b₂ = -infty implies b₁ = b₂ ) & ( not x is real & not x = +infty & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number st x is real & x = +infty holds
( ex a being complex number st
( x = a & b₁ = - a ) iff b₁ = -infty ) ;
involutiveness
for b₁, b₂ being ext-real number st ( b₂ is real implies ex a being complex number st
( b₂ = a & b₁ = - a ) ) & ( b₂ = +infty implies b₁ = -infty ) & ( not b₂ is real & not b₂ = +infty implies b₁ = +infty ) holds
( ( b₁ is real implies ex a being complex number st
( b₁ = a & b₂ = - a ) ) & ( b₁ = +infty implies b₂ = -infty ) & ( not b₁ is real & not b₁ = +infty implies b₂ = +infty ) )

proof end;

end;

:: deftheorem Def5 defines - XXREAL_3:def 3 :

for x, b₂ being ext-real number holds
( ( x is real implies ( b₂ = - x iff ex a being complex number st
( x = a & b₂ = - a ) ) ) & ( x = +infty implies ( b₂ = - x iff b₂ = -infty ) ) & ( not x is real & not x = +infty implies ( b₂ = - x iff b₂ = +infty ) ) );

definition

let x be ext-real number ;
func x " -> ext-real number means :Def6: :: XXREAL_3:def 4
ex a being complex number st
( x = a & it = a " ) if x is real
otherwise it = 0 ;
existence
( ( x is real implies ex b₁ being ext-real number ex a being complex number st
( x = a & b₁ = a " ) ) & ( not x is real implies ex b₁ being ext-real number st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b₁ = a " ) & ex a being complex number st
( x = a & b₂ = a " ) implies b₁ = b₂ ) & ( not x is real & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ;
consistency
for b₁ being ext-real number holds verum ;

end;

:: deftheorem Def6 defines " XXREAL_3:def 4 :

for x, b₂ being ext-real number holds
( ( x is real implies ( b₂ = x " iff ex a being complex number st
( x = a & b₂ = a " ) ) ) & ( not x is real implies ( b₂ = x " iff b₂ = 0 ) ) );

registration

let x be real number ;
let a be complex number ;
real set complex set - a₁ - a₂ compatibility
( x = a implies - x = - a ) by Def5;
real set complex set a₁ " a₂ " compatibility
( x = a implies x " = a " ) by Def6;

end;

definition

let x, y be ext-real number ;
func x - y -> ext-real number equals :: XXREAL_3:def 5
x + (- y);
coherence
x + (- y) is ext-real number ;
func x / y -> ext-real number equals :: XXREAL_3:def 6
x * (y " );
coherence
x * (y " ) is ext-real number ;

end;

:: deftheorem defines - XXREAL_3:def 5 :

for x, y being ext-real number holds x - y = x + (- y);

:: deftheorem defines / XXREAL_3:def 6 :

for x, y being ext-real number holds x / y = x * (y " );

registration

let x, y be real number ;
let a, b be complex number ;
real set real set complex set complex set a₁ - a₂ a₃ - a₄ compatibility
( x = a & y = b implies x - y = a - b )

proof end;

real set real set complex set complex set a₁ / a₂ a₃ / a₄ compatibility
( x = a & y = b implies x / y = a / b )

proof end;

end;

theorem :: XXREAL_3:1

for x being ext-real number holds x * 0 = 0

proof end;