:: by Andrzej Trybulec

::

:: Received September 23, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

definition

let x, y be ExtReal;

verum ;

compatibility

( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st

( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) )

end;
redefine pred x <= y means :Def1: :: XXREAL_3:def 1

ex p, q being Element of REAL st

( p = x & q = y & p <= q ) if ( x in REAL & y in REAL )

otherwise ( x = -infty or y = +infty );

consistency ex p, q being Element of REAL st

( p = x & q = y & p <= q ) if ( x in REAL & y in REAL )

otherwise ( x = -infty or y = +infty );

verum ;

compatibility

( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st

( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) )

proof end;

:: deftheorem Def1 defines <= XXREAL_3:def 1 :

for x, y being ExtReal holds

( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st

( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) );

for x, y being ExtReal holds

( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st

( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) );

registration

existence

ex b_{1} being ExtReal st

( not b_{1} is real & b_{1} is positive )

ex b_{1} being ExtReal st

( not b_{1} is real & b_{1} is negative )

end;
ex b

( not b

proof end;

existence ex b

( not b

proof end;

registration

coherence

for b_{1} being ExtReal st not b_{1} is real & not b_{1} is negative holds

b_{1} is positive
;

coherence

for b_{1} being ExtReal st not b_{1} is real & not b_{1} is positive holds

b_{1} is negative
;

end;
for b

b

coherence

for b

b

definition

let x, y be ExtReal;

( ( x is real & y is real implies ex b_{1} being ExtReal ex a, b being Complex st

( x = a & y = b & b_{1} = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b_{1} being ExtReal st b_{1} = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b_{1} being ExtReal st b_{1} = -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_{1} being ExtReal st b_{1} = 0 ) )

for b_{1}, b_{2} being ExtReal holds

( ( x is real & y is real & ex a, b being Complex st

( x = a & y = b & b_{1} = a + b ) & ex a, b being Complex st

( x = a & y = b & b_{2} = a + b ) implies b_{1} = b_{2} ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b_{1} = -infty & b_{2} = -infty implies b_{1} = b_{2} ) & ( ( 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_{1} = 0 or not b_{2} = 0 or b_{1} = b_{2} ) )
;

consistency

for b_{1} being ExtReal holds

( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being Complex st

( x = a & y = b & b_{1} = a + b ) iff b_{1} = +infty ) ) & ( x is real & y is real & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( ex a, b being Complex st

( x = a & y = b & b_{1} = a + b ) iff b_{1} = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b_{1} = +infty iff b_{1} = -infty ) ) )
;

commutativity

for b_{1}, x, y being ExtReal st ( x is real & y is real implies ex a, b being Complex st

( x = a & y = b & b_{1} = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b_{1} = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b_{1} = -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_{1} = 0 ) holds

( ( y is real & x is real implies ex a, b being Complex st

( y = a & x = b & b_{1} = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b_{1} = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b_{1} = -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_{1} = 0 ) )
;

end;
func x + y -> ExtReal means :Def2: :: XXREAL_3:def 2

ex a, b being Complex 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 ex a, b being Complex 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 ;

( ( x is real & y is real implies ex b

( x = a & y = b & b

proof end;

uniqueness for b

( ( x is real & y is real & ex a, b being Complex st

( x = a & y = b & b

( x = a & y = b & b

consistency

for b

( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being Complex st

( x = a & y = b & b

( x = a & y = b & b

commutativity

for b

( x = a & y = b & b

( ( y is real & x is real implies ex a, b being Complex st

( y = a & x = b & b

:: deftheorem Def2 defines + XXREAL_3:def 2 :

for x, y, b_{3} being ExtReal holds

( ( x is real & y is real implies ( b_{3} = x + y iff ex a, b being Complex st

( x = a & y = b & b_{3} = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b_{3} = x + y iff b_{3} = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b_{3} = x + y iff b_{3} = -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_{3} = x + y iff b_{3} = 0 ) ) );

for x, y, b

( ( x is real & y is real implies ( b

( x = a & y = b & b

definition

let x be ExtReal;

( ( x is real implies ex b_{1} being ExtReal ex a being Complex st

( x = a & b_{1} = - a ) ) & ( x = +infty implies ex b_{1} being ExtReal st b_{1} = -infty ) & ( not x is real & not x = +infty implies ex b_{1} being ExtReal st b_{1} = +infty ) )

for b_{1}, b_{2} being ExtReal holds

( ( x is real & ex a being Complex st

( x = a & b_{1} = - a ) & ex a being Complex st

( x = a & b_{2} = - a ) implies b_{1} = b_{2} ) & ( x = +infty & b_{1} = -infty & b_{2} = -infty implies b_{1} = b_{2} ) & ( not x is real & not x = +infty & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being ExtReal st x is real & x = +infty holds

( ex a being Complex st

( x = a & b_{1} = - a ) iff b_{1} = -infty )
;

involutiveness

for b_{1}, b_{2} being ExtReal st ( b_{2} is real implies ex a being Complex st

( b_{2} = a & b_{1} = - a ) ) & ( b_{2} = +infty implies b_{1} = -infty ) & ( not b_{2} is real & not b_{2} = +infty implies b_{1} = +infty ) holds

( ( b_{1} is real implies ex a being Complex st

( b_{1} = a & b_{2} = - a ) ) & ( b_{1} = +infty implies b_{2} = -infty ) & ( not b_{1} is real & not b_{1} = +infty implies b_{2} = +infty ) )

end;
func - x -> ExtReal means :Def3: :: XXREAL_3:def 3

ex a being Complex st

( x = a & it = - a ) if x is real

it = -infty if x = +infty

otherwise it = +infty ;

existence ex a being Complex st

( x = a & it = - a ) if x is real

it = -infty if x = +infty

otherwise it = +infty ;

( ( x is real implies ex b

( x = a & b

proof end;

uniqueness for b

( ( x is real & ex a being Complex st

( x = a & b

( x = a & b

consistency

for b

( ex a being Complex st

( x = a & b

involutiveness

for b

( b

( ( b

( b

proof end;

:: deftheorem Def3 defines - XXREAL_3:def 3 :

for x, b_{2} being ExtReal holds

( ( x is real implies ( b_{2} = - x iff ex a being Complex st

( x = a & b_{2} = - a ) ) ) & ( x = +infty implies ( b_{2} = - x iff b_{2} = -infty ) ) & ( not x is real & not x = +infty implies ( b_{2} = - x iff b_{2} = +infty ) ) );

for x, b

( ( x is real implies ( b

( x = a & b

registration

let x, y be Real;

let a, b be Complex;

compatibility

( x = a & y = b implies x + y = a + b ) by Def2;

end;
let a, b be Complex;

compatibility

( x = a & y = b implies x + y = a + b ) by Def2;

registration
end;

:: for ExtReals

:: for ExtReals

registration

let x be Real;

let y be non real ExtReal;

coherence

for b_{1} being object st b_{1} = x + y holds

not b_{1} is real

end;
let y be non real ExtReal;

coherence

for b

not b

proof end;

registration

let x be negative non real ExtReal;

let y be positive non real ExtReal;

coherence

x + y is zero

end;
let y be positive non real ExtReal;

coherence

x + y is zero

proof end;

registration
end;

Lm1: +infty + +infty = +infty

by Def2;

Lm2: -infty + -infty = -infty

by Def2;

Lm3: for x being ExtReal holds

( - x in REAL iff x in REAL )

proof end;

Lm4: - (+infty + -infty) = +infty - +infty by Def3

.= (- -infty) - +infty by Def3 ;

Lm5: - +infty = -infty

by Def3;

Lm6: for x being ExtReal st x in REAL holds

- (x + +infty) = (- +infty) + (- x)

proof end;

Lm7: for x being ExtReal st x in REAL holds

- (x + -infty) = (- -infty) + (- x)

proof end;

Lm8: for x, y being ExtReal holds

( not x + y = +infty or x = +infty or y = +infty )

proof end;

Lm9: for x, y being ExtReal holds

( not x + y = -infty or x = -infty or y = -infty )

proof end;

theorem :: XXREAL_3:16

theorem :: XXREAL_3:17

theorem Th20: :: XXREAL_3:20

for x, y being ExtReal holds

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )

proof end;

theorem Th21: :: XXREAL_3:21

for x, y being ExtReal holds

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )

proof end;

theorem Th23: :: XXREAL_3:23

for x being ExtReal holds

( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )

( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )

proof end;

Lm10: - +infty = -infty

by Def3;

Lm11: for x being ExtReal st x in REAL holds

- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th29: :: XXREAL_3:29

for x, y, z being ExtReal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds

(x + y) + z = x + (y + z)

(x + y) + z = x + (y + z)

proof end;

theorem Th30: :: XXREAL_3:30

for x, y, z being ExtReal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds

(x + y) - z = x + (y - z)

(x + y) - z = x + (y - z)

proof end;

theorem :: XXREAL_3:31

for x, y, z being ExtReal st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = -infty ) & ( not y = -infty or not z = +infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds

(x - y) - z = x - (y + z)

(x - y) - z = x - (y + z)

proof end;

theorem Th32: :: XXREAL_3:32

for x, y, z being ExtReal st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = -infty ) & ( not x = -infty or not z = +infty ) holds

(x - y) + z = x - (y - z)

(x - y) + z = x - (y - z)

proof end;

Lm12: for x, y, z being ExtReal st x <= y holds

x + z <= y + z

proof end;

Lm13: for x, y being ExtReal st x >= 0 & y > 0 holds

x + y > 0

proof end;

Lm14: for x, y being ExtReal st x <= 0 & y < 0 holds

x + y < 0

proof end;

registration

let x be positive ExtReal;

let y be non negative ExtReal;

coherence

x + y is positive by Lm13;

coherence

y + x is positive ;

end;
let y be non negative ExtReal;

coherence

x + y is positive by Lm13;

coherence

y + x is positive ;

registration

let x be negative ExtReal;

let y be non positive ExtReal;

coherence

x + y is negative by Lm14;

coherence

y + x is negative ;

end;
let y be non positive ExtReal;

coherence

x + y is negative by Lm14;

coherence

y + x is negative ;

registration
end;

registration
end;

registration

let x be non negative ExtReal;

let y be non positive ExtReal;

coherence

not x - y is negative ;

coherence

not y - x is positive ;

end;
let y be non positive ExtReal;

coherence

not x - y is negative ;

coherence

not y - x is positive ;

registration

let x be positive ExtReal;

let y be non positive ExtReal;

coherence

x - y is positive ;

coherence

y - x is negative ;

end;
let y be non positive ExtReal;

coherence

x - y is positive ;

coherence

y - x is negative ;

registration

let x be negative ExtReal;

let y be non negative ExtReal;

coherence

x - y is negative ;

coherence

y - x is positive ;

end;
let y be non negative ExtReal;

coherence

x - y is negative ;

coherence

y - x is positive ;

Lm15: for x, y being ExtReal st x <= y holds

- y <= - x

proof end;

theorem :: XXREAL_3:41

for x, y, z being ExtReal st ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z holds

x <= z + y

x <= z + y

proof end;

theorem :: XXREAL_3:42

for x, y, z being ExtReal st ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y holds

x - y <= z

x - y <= z

proof end;

Lm16: 0 in REAL

by XREAL_0:def 1;

theorem :: XXREAL_3:52

for x, y, z being ExtReal holds

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) )

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) )

proof end;

theorem :: XXREAL_3:53

for x, y, z being ExtReal holds

( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )

( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )

proof end;

theorem :: XXREAL_3:54

for x, y, z being ExtReal holds

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) )

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) )

proof end;

theorem :: XXREAL_3:55

for x, y, z being ExtReal holds

( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) )

( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) )

proof end;

theorem :: XXREAL_3:56

for x, y, z being ExtReal holds

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )

( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )

proof end;

theorem :: XXREAL_3:57

for x, y, z being ExtReal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y holds

( y <> +infty & x + y <= z )

( y <> +infty & x + y <= z )

proof end;

theorem :: XXREAL_3:58

for x, y, z being ExtReal holds

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )

( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )

proof end;

theorem :: XXREAL_3:59

for x, y, z being ExtReal st ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y holds

y <> -infty

y <> -infty

proof end;

definition

let x, y be ExtReal;

( ( x is real & y is real implies ex b_{1} being ExtReal ex a, b being Complex st

( x = a & y = b & b_{1} = 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_{1} being ExtReal st b_{1} = +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_{1} being ExtReal st b_{1} = -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_{1} being ExtReal st b_{1} = 0 ) )

for b_{1}, b_{2} being ExtReal holds

( ( x is real & y is real & ex a, b being Complex st

( x = a & y = b & b_{1} = a * b ) & ex a, b being Complex st

( x = a & y = b & b_{2} = a * b ) implies b_{1} = b_{2} ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b_{1} = -infty & b_{2} = -infty implies b_{1} = b_{2} ) & ( ( 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_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being ExtReal 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 st

( x = a & y = b & b_{1} = a * b ) iff b_{1} = +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 st

( x = a & y = b & b_{1} = a * b ) iff b_{1} = -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_{1} = +infty iff b_{1} = -infty ) ) )
;

commutativity

for b_{1}, x, y being ExtReal st ( x is real & y is real implies ex a, b being Complex st

( x = a & y = b & b_{1} = 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_{1} = +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_{1} = -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_{1} = 0 ) holds

( ( y is real & x is real implies ex a, b being Complex st

( y = a & x = b & b_{1} = 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_{1} = +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_{1} = -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_{1} = 0 ) )
;

end;
func x * y -> ExtReal means :Def5: :: XXREAL_3:def 5

ex a, b being Complex 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 ex a, b being Complex 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 ;

( ( x is real & y is real implies ex b

( x = a & y = b & b

proof end;

uniqueness for b

( ( x is real & y is real & ex a, b being Complex st

( x = a & y = b & b

( x = a & y = b & b

consistency

for b

( ( 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 st

( x = a & y = b & b

( x = a & y = b & b

commutativity

for b

( x = a & y = b & b

( ( y is real & x is real implies ex a, b being Complex st

( y = a & x = b & b

:: deftheorem Def5 defines * XXREAL_3:def 5 :

for x, y, b_{3} being ExtReal holds

( ( x is real & y is real implies ( b_{3} = x * y iff ex a, b being Complex st

( x = a & y = b & b_{3} = 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_{3} = x * y iff b_{3} = +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_{3} = x * y iff b_{3} = -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_{3} = x * y iff b_{3} = 0 ) ) );

for x, y, b

( ( x is real & y is real implies ( b

( x = a & y = b & b

registration

let x, y be Real;

let a, b be Complex;

compatibility

( x = a & y = b implies x * y = a * b ) by Def5;

end;
let a, b be Complex;

compatibility

( x = a & y = b implies x * y = a * b ) by Def5;

definition

let x be ExtReal;

( ( x is real implies ex b_{1} being ExtReal ex a being Complex st

( x = a & b_{1} = a " ) ) & ( not x is real implies ex b_{1} being ExtReal st b_{1} = 0 ) )

for b_{1}, b_{2} being ExtReal holds

( ( x is real & ex a being Complex st

( x = a & b_{1} = a " ) & ex a being Complex st

( x = a & b_{2} = a " ) implies b_{1} = b_{2} ) & ( not x is real & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being ExtReal holds verum
;

end;
func x " -> ExtReal means :Def6: :: XXREAL_3:def 6

ex a being Complex st

( x = a & it = a " ) if x is real

otherwise it = 0 ;

existence ex a being Complex st

( x = a & it = a " ) if x is real

otherwise it = 0 ;

( ( x is real implies ex b

( x = a & b

proof end;

uniqueness for b

( ( x is real & ex a being Complex st

( x = a & b

( x = a & b

consistency

for b

:: deftheorem Def6 defines " XXREAL_3:def 6 :

for x, b_{2} being ExtReal holds

( ( x is real implies ( b_{2} = x " iff ex a being Complex st

( x = a & b_{2} = a " ) ) ) & ( not x is real implies ( b_{2} = x " iff b_{2} = 0 ) ) );

for x, b

( ( x is real implies ( b

( x = a & b

registration
end;

registration

let x, y be Real;

let a, b be Complex;

compatibility

( x = a & y = b implies x / y = a / b )

end;
let a, b be Complex;

compatibility

( x = a & y = b implies x / y = a / b )

proof end;

Lm17: for x being ExtReal holds x * 0 = 0

proof end;

registration
end;

registration
end;

registration
end;

registration

let x be non positive ExtReal;

let y be non negative ExtReal;

coherence

not x * y is positive

end;
let y be non negative ExtReal;

coherence

not x * y is positive

proof end;

registration

let x be non negative ExtReal;

let y be non positive ExtReal;

coherence

not x / y is positive ;

coherence

not y / x is positive ;

end;
let y be non positive ExtReal;

coherence

not x / y is positive ;

coherence

not y / x is positive ;

registration
end;

registration
end;

Lm18: for x, y being ExtReal st not x is real & x * y = 0 holds

y = 0

proof end;

registration
end;

registration

let x be zero ExtReal;

let y be ExtReal;

coherence

for b_{1} being ExtReal st b_{1} = x * y holds

b_{1} is zero
by Lm17;

end;
let y be ExtReal;

coherence

for b

b

Lm19: for x, y, z being ExtReal st x = 0 holds

x * (y * z) = (x * y) * z

proof end;

Lm20: for x, y, z being ExtReal st y = 0 holds

x * (y * z) = (x * y) * z

proof end;

Lm21: for x, y, z being ExtReal st not y is real holds

x * (y * z) = (x * y) * z

proof end;

Lm22: for x, y, z being ExtReal st not x is real holds

x * (y * z) = (x * y) * z

proof end;

:: for ExtReals

:: for ExtReals

theorem Th69: :: XXREAL_3:69

for x, y being ExtReal st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds

y = -infty

y = -infty

proof end;

theorem Th70: :: XXREAL_3:70

for x, y being ExtReal st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds

y = -infty

y = -infty

proof end;

Lm23: for x, y being ExtReal holds

( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 )

proof end;

theorem :: XXREAL_3:73

theorem :: XXREAL_3:87

for x being ExtReal st x <> +infty & x <> -infty & x <> 0 holds

( x * (1 / x) = 1 & (1 / x) * x = 1 )

( x * (1 / x) = 1 & (1 / x) * x = 1 )

proof end;

theorem :: XXREAL_3:88

for x, y being ExtReal st -infty <> y & y <> +infty & y <> 0 holds

( (x * y) / y = x & x * (y / y) = x )

( (x * y) / y = x & x * (y / y) = x )

proof end;

Lm24: for x, y being ExtReal holds x * (y + y) = (x * y) + (x * y)

proof end;

Lm25: for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z)

proof end;

Lm26: for y, z being ExtReal holds 0 * (y + z) = (0 * y) + (0 * z)

;

Lm27: for x, y, z being ExtReal st x is real & y is real holds

x * (y + z) = (x * y) + (x * z)

proof end;

Lm28: for x, y, z being ExtReal st x is real & not y is real holds

x * (y + z) = (x * y) + (x * z)

proof end;

registration
end;