:: Basic Operations on Extended Real Numbers :: by Andrzej Trybulec :: :: Received September 23, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin definition let x, y be ext-real number ; 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 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 ) ) ) ) proofend; end; :: deftheorem Def1 defines <= XXREAL_3:def_1_:_ for x, y being ext-real number 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 cluster ext-real positive non real for set ; existence ex b1 being ext-real number st ( not b1 is real & b1 is positive ) proofend; cluster ext-real negative non real for set ; existence ex b1 being ext-real number st ( not b1 is real & b1 is negative ) proofend; end; theorem Th1: :: XXREAL_3:1 for x being ext-real positive non real number holds x = +infty proofend; theorem Th2: :: XXREAL_3:2 for x being ext-real negative non real number holds x = -infty proofend; registration cluster ext-real non negative non real -> ext-real positive for set ; coherence for b1 being ext-real number st not b1 is real & not b1 is negative holds b1 is positive ; cluster ext-real non positive non real -> ext-real negative for set ; coherence for b1 being ext-real number st not b1 is real & not b1 is positive holds b1 is negative ; end; theorem Th3: :: XXREAL_3:3 for x, z being ext-real number st x < z holds ex y being real number st ( x < y & y < z ) proofend; begin definition let x, y be ext-real number ; funcx + y -> ext-real number means :Def2: :: 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 ( ( 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 b1 being ext-real number ex a, b being complex number st ( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -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 b1 being ext-real number st b1 = 0 ) ) proofend; uniqueness for b1, b2 being ext-real number holds ( ( x is real & y is real & ex a, b being complex number st ( x = a & y = b & b1 = a + b ) & ex a, b being complex number st ( x = a & y = b & b2 = a + b ) implies b1 = b2 ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( 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 b1 = 0 or not b2 = 0 or b1 = b2 ) ) ; consistency for b1 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 & b1 = a + b ) iff b1 = +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 & b1 = a + b ) iff b1 = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b1 = +infty iff b1 = -infty ) ) ) ; commutativity for b1, 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 & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b1 = -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 b1 = 0 ) holds ( ( y is real & x is real implies ex a, b being complex number st ( y = a & x = b & b1 = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b1 = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b1 = -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 b1 = 0 ) ) ; end; :: deftheorem Def2 defines + XXREAL_3:def_2_:_ for x, y, b3 being ext-real number holds ( ( x is real & y is real implies ( b3 = x + y iff ex a, b being complex number st ( x = a & y = b & b3 = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b3 = x + y iff b3 = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b3 = x + y iff b3 = -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 ( b3 = x + y iff b3 = 0 ) ) ); definition let x be ext-real number ; func - x -> ext-real number means :Def3: :: 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 b1 being ext-real number ex a being complex number st ( x = a & b1 = - a ) ) & ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) ) proofend; uniqueness for b1, b2 being ext-real number holds ( ( x is real & ex a being complex number st ( x = a & b1 = - a ) & ex a being complex number st ( x = a & b2 = - a ) implies b1 = b2 ) & ( x = +infty & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( not x is real & not x = +infty & b1 = +infty & b2 = +infty implies b1 = b2 ) ) ; consistency for b1 being ext-real number st x is real & x = +infty holds ( ex a being complex number st ( x = a & b1 = - a ) iff b1 = -infty ) ; involutiveness for b1, b2 being ext-real number st ( b2 is real implies ex a being complex number st ( b2 = a & b1 = - a ) ) & ( b2 = +infty implies b1 = -infty ) & ( not b2 is real & not b2 = +infty implies b1 = +infty ) holds ( ( b1 is real implies ex a being complex number st ( b1 = a & b2 = - a ) ) & ( b1 = +infty implies b2 = -infty ) & ( not b1 is real & not b1 = +infty implies b2 = +infty ) ) proofend; end; :: deftheorem Def3 defines - XXREAL_3:def_3_:_ for x, b2 being ext-real number holds ( ( x is real implies ( b2 = - x iff ex a being complex number st ( x = a & b2 = - a ) ) ) & ( x = +infty implies ( b2 = - x iff b2 = -infty ) ) & ( not x is real & not x = +infty implies ( b2 = - x iff b2 = +infty ) ) ); definition let x, y be ext-real number ; funcx - y -> ext-real number equals :: XXREAL_3:def 4 x + (- y); coherence x + (- y) is ext-real number ; end; :: deftheorem defines - XXREAL_3:def_4_:_ 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 ; identifyx + y with a + b when x = a, y = b; compatibility ( x = a & y = b implies x + y = a + b ) by Def2; end; registration let x be real number ; let a be complex number ; identify - x with - a when x = a; compatibility ( x = a implies - x = - a ) by Def3; end; :: for ext-real numbers registration let r be real number ; cluster - r -> ext-real real ; coherence - r is real ; end; :: for ext-real numbers registration let r, s be real number ; clusterr + s -> ext-real real ; coherence r + s is real ; clusterr - s -> ext-real real ; coherence r - s is real ; end; registration let x be real number ; let y be ext-real non real number ; clusterx + y -> non real for number ; coherence for b1 being number st b1 = x + y holds not b1 is real proofend; end; registration let x, y be ext-real positive non real number ; clusterx + y -> ext-real non real ; coherence not x + y is real proofend; end; registration let x, y be ext-real negative non real number ; clusterx + y -> ext-real non real ; coherence not x + y is real proofend; end; registration let x be ext-real negative non real number ; let y be ext-real positive non real number ; clusterx + y -> zero ext-real ; coherence x + y is zero proofend; end; registration let x, y be real number ; let a, b be complex number ; identifyx - y with a - b when x = a, y = b; compatibility ( x = a & y = b implies x - y = a - b ) ; end; theorem Th4: :: XXREAL_3:4 for x being ext-real number holds x + 0 = x proofend; theorem Th5: :: XXREAL_3:5 - -infty = +infty by Def3; theorem Th6: :: XXREAL_3:6 - +infty = -infty by Def3; Lm1: +infty + +infty = +infty by Def2; Lm2: -infty + -infty = -infty by Def2; theorem Th7: :: XXREAL_3:7 for x being ext-real number holds x + (- x) = 0 proofend; theorem :: XXREAL_3:8 for x, y being ext-real number st x + y = 0 holds x = - y proofend; Lm3: for x being ext-real number holds ( - x in REAL iff x in REAL ) proofend; Lm4: - (+infty + -infty) = +infty - +infty by Def3 .= (- -infty) - +infty by Def3 ; Lm5: - +infty = -infty by Def3; Lm6: for x being ext-real number st x in REAL holds - (x + +infty) = (- +infty) + (- x) proofend; Lm7: for x being ext-real number st x in REAL holds - (x + -infty) = (- -infty) + (- x) proofend; theorem Th9: :: XXREAL_3:9 for x, y being ext-real number holds - (x + y) = (- x) + (- y) proofend; theorem Th10: :: XXREAL_3:10 for f, g being ext-real number st - f = - g holds f = g proofend; Lm8: for x, y being ext-real number holds ( not x + y = +infty or x = +infty or y = +infty ) proofend; Lm9: for x, y being ext-real number holds ( not x + y = -infty or x = -infty or y = -infty ) proofend; theorem Th11: :: XXREAL_3:11 for r being real number for f, g being ext-real number st r + f = r + g holds f = g proofend; theorem :: XXREAL_3:12 for r being real number for f, g being ext-real number st r - f = r - g holds f = g proofend; theorem Th13: :: XXREAL_3:13 for x being ext-real number st x <> +infty holds ( +infty - x = +infty & x - +infty = -infty ) proofend; theorem Th14: :: XXREAL_3:14 for x being ext-real number st x <> -infty holds ( -infty - x = -infty & x - -infty = +infty ) proofend; theorem Th15: :: XXREAL_3:15 for x being ext-real number holds x - 0 = x proofend; theorem :: XXREAL_3:16 for x, y being ext-real number holds ( not x + y = +infty or x = +infty or y = +infty ) by Lm8; theorem :: XXREAL_3:17 for x, y being ext-real number holds ( not x + y = -infty or x = -infty or y = -infty ) by Lm9; theorem Th18: :: XXREAL_3:18 for x, y being ext-real number holds ( not x - y = +infty or x = +infty or y = -infty ) proofend; theorem Th19: :: XXREAL_3:19 for x, y being ext-real number holds ( not x - y = -infty or x = -infty or y = +infty ) proofend; theorem Th20: :: XXREAL_3:20 for x, y being ext-real number holds ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) ) proofend; theorem Th21: :: XXREAL_3:21 for x, y being ext-real number holds ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) ) proofend; theorem Th22: :: XXREAL_3:22 for x, y being ext-real number st x is real holds ( (y - x) + x = y & (y + x) - x = y ) proofend; theorem Th23: :: XXREAL_3:23 for x being ext-real number holds ( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) ) proofend; theorem :: XXREAL_3:24 for z, x being ext-real number st z is real holds x = (x + z) - z proofend; Lm10: - +infty = -infty by Def3; Lm11: for x being ext-real number st x in REAL holds - (x + -infty) = (- -infty) + (- x) proofend; theorem Th25: :: XXREAL_3:25 for x, y being ext-real number holds - (x + y) = (- y) - x proofend; theorem :: XXREAL_3:26 for x, y being ext-real number holds ( - (x - y) = (- x) + y & - (x - y) = y - x ) proofend; theorem Th27: :: XXREAL_3:27 for x, y being ext-real number holds ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) proofend; theorem :: XXREAL_3:28 for y, z being ext-real number st 0 <= y & y < +infty holds z = (z + y) - y proofend; theorem Th29: :: XXREAL_3:29 for x, y, z being ext-real number 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) proofend; theorem Th30: :: XXREAL_3:30 for x, y, z being ext-real number 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) proofend; theorem :: XXREAL_3:31 for x, y, z being ext-real number 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) proofend; theorem Th32: :: XXREAL_3:32 for x, y, z being ext-real number 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) proofend; theorem Th33: :: XXREAL_3:33 for z, x, y being ext-real number st z is real holds (z + x) - (z + y) = x - y proofend; theorem :: XXREAL_3:34 for y, z, x being ext-real number st y is real holds (z - y) + (y - x) = z - x proofend; begin Lm12: for x, y, z being ext-real number st x <= y holds x + z <= y + z proofend; Lm13: for x, y being ext-real number st x >= 0 & y > 0 holds x + y > 0 proofend; Lm14: for x, y being ext-real number st x <= 0 & y < 0 holds x + y < 0 proofend; registration let x, y be ext-real non negative number ; clusterx + y -> ext-real non negative ; coherence not x + y is negative proofend; end; registration let x, y be ext-real non positive number ; clusterx + y -> ext-real non positive ; coherence not x + y is positive proofend; end; registration let x be ext-real positive number ; let y be ext-real non negative number ; clusterx + y -> ext-real positive ; coherence x + y is positive by Lm13; clustery + x -> ext-real positive ; coherence y + x is positive ; end; registration let x be ext-real negative number ; let y be ext-real non positive number ; clusterx + y -> ext-real negative ; coherence x + y is negative by Lm14; clustery + x -> ext-real negative ; coherence y + x is negative ; end; registration let x be ext-real non positive number ; cluster - x -> ext-real non negative ; coherence not - x is negative proofend; end; registration let x be ext-real non negative number ; cluster - x -> ext-real non positive ; coherence not - x is positive proofend; end; registration let x be ext-real positive number ; cluster - x -> ext-real negative ; coherence - x is negative proofend; end; registration let x be ext-real negative number ; cluster - x -> ext-real positive ; coherence - x is positive proofend; end; registration let x be ext-real non negative number ; let y be ext-real non positive number ; clusterx - y -> ext-real non negative ; coherence not x - y is negative ; clustery - x -> ext-real non positive ; coherence not y - x is positive ; end; registration let x be ext-real positive number ; let y be ext-real non positive number ; clusterx - y -> ext-real positive ; coherence x - y is positive ; clustery - x -> ext-real negative ; coherence y - x is negative ; end; registration let x be ext-real negative number ; let y be ext-real non negative number ; clusterx - y -> ext-real negative ; coherence x - y is negative ; clustery - x -> ext-real positive ; coherence y - x is positive ; end; Lm15: for x, y being ext-real number st x <= y holds - y <= - x proofend; theorem :: XXREAL_3:35 for x, y, z being ext-real number st x <= y holds x + z <= y + z by Lm12; theorem Th36: :: XXREAL_3:36 for x, y, z, w being ext-real number st x <= y & z <= w holds x + z <= y + w proofend; theorem Th37: :: XXREAL_3:37 for x, y, z, w being ext-real number st x <= y & z <= w holds x - w <= y - z proofend; theorem Th38: :: XXREAL_3:38 for x, y being ext-real number holds ( x <= y iff - y <= - x ) proofend; theorem Th39: :: XXREAL_3:39 for z, x being ext-real number st 0 <= z holds x <= x + z proofend; theorem :: XXREAL_3:40 for x, y being ext-real number st x <= y holds y - x >= 0 proofend; theorem :: XXREAL_3:41 for z, y, x being ext-real number st ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z holds x <= z + y proofend; theorem :: XXREAL_3:42 for x, y, z being ext-real number st ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y holds x - y <= z proofend; theorem Th43: :: XXREAL_3:43 for z, x, y being ext-real number st z in REAL & x < y holds ( x + z < y + z & x - z < y - z ) proofend; theorem :: XXREAL_3:44 for x, y, z being ext-real number st 0 <= x & 0 <= y & 0 <= z holds (x + y) + z = x + (y + z) proofend; theorem Th45: :: XXREAL_3:45 for x, y, z being ext-real number st x is real holds ( y + x <= z iff y <= z - x ) proofend; theorem Th46: :: XXREAL_3:46 for x, y being ext-real number st 0 < x & x < y holds 0 < y - x proofend; theorem :: XXREAL_3:47 for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds z < y - x proofend; theorem :: XXREAL_3:48 for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds z <= y proofend; theorem Th49: :: XXREAL_3:49 for x, z being ext-real number st 0 <= x & x < z holds ex y being real number st ( 0 < y & x + y < z ) proofend; theorem :: XXREAL_3:50 for x being ext-real number st 0 < x holds ex y being real number st ( 0 < y & y + y < x ) proofend; theorem Th51: :: XXREAL_3:51 for x, y being ext-real number st x < y & x < +infty & -infty < y holds 0 < y - x proofend; theorem :: XXREAL_3:52 for x, y, z being ext-real number 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 ) ) proofend; theorem :: XXREAL_3:53 for z, y, x being ext-real number 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 ) ) proofend; theorem :: XXREAL_3:54 for x, y, z being ext-real number 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 ) ) proofend; theorem :: XXREAL_3:55 for z, y, x being ext-real number 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 ) ) proofend; theorem :: XXREAL_3:56 for x, y, z being ext-real number 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 ) ) proofend; theorem :: XXREAL_3:57 for x, y, z being ext-real number 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 ) proofend; theorem :: XXREAL_3:58 for x, y, z being ext-real number 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 ) proofend; theorem :: XXREAL_3:59 for x, y, z being ext-real number st ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y holds y <> -infty proofend; theorem :: XXREAL_3:60 for x, y being ext-real number holds ( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) ) proofend; theorem :: XXREAL_3:61 for x, y being ext-real number st ( for e being real number st 0 < e holds x < y + e ) holds x <= y proofend; theorem :: XXREAL_3:62 for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds x + t < y + t proofend; theorem :: XXREAL_3:63 for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds x - t < y - t proofend; theorem :: XXREAL_3:64 for x, y, w, z being ext-real number st x < y & w < z holds x + w < y + z proofend; theorem :: XXREAL_3:65 for x, z, y being ext-real number st 0 <= x & z + x <= y holds z <= y proofend; begin definition let x, y be ext-real number ; funcx * y -> ext-real number means :Def5: :: XXREAL_3:def 5 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 b1 being ext-real number ex a, b being complex number st ( x = a & y = b & b1 = 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 b1 being ext-real number st b1 = +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 b1 being ext-real number st b1 = -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 b1 being ext-real number st b1 = 0 ) ) proofend; uniqueness for b1, b2 being ext-real number holds ( ( x is real & y is real & ex a, b being complex number st ( x = a & y = b & b1 = a * b ) & ex a, b being complex number st ( x = a & y = b & b2 = a * b ) implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( 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 ) ) ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; consistency for b1 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 & b1 = a * b ) iff b1 = +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 & b1 = a * b ) iff b1 = -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 ( b1 = +infty iff b1 = -infty ) ) ) ; commutativity for b1, 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 & b1 = 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 b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b1 = -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 b1 = 0 ) holds ( ( y is real & x is real implies ex a, b being complex number st ( y = a & x = b & b1 = 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 b1 = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b1 = -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 b1 = 0 ) ) ; end; :: deftheorem Def5 defines * XXREAL_3:def_5_:_ for x, y, b3 being ext-real number holds ( ( x is real & y is real implies ( b3 = x * y iff ex a, b being complex number st ( x = a & y = b & b3 = 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 ( b3 = x * y iff b3 = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b3 = x * y iff b3 = -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 ( b3 = x * y iff b3 = 0 ) ) ); registration let x, y be real number ; let a, b be complex number ; identifyx * y with a * b when x = a, y = b; compatibility ( x = a & y = b implies x * y = a * b ) by Def5; end; definition let x be ext-real number ; funcx " -> ext-real number means :Def6: :: XXREAL_3:def 6 ex a being complex number st ( x = a & it = a " ) if x is real otherwise it = 0 ; existence ( ( x is real implies ex b1 being ext-real number ex a being complex number st ( x = a & b1 = a " ) ) & ( not x is real implies ex b1 being ext-real number st b1 = 0 ) ) proofend; uniqueness for b1, b2 being ext-real number holds ( ( x is real & ex a being complex number st ( x = a & b1 = a " ) & ex a being complex number st ( x = a & b2 = a " ) implies b1 = b2 ) & ( not x is real & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; consistency for b1 being ext-real number holds verum ; end; :: deftheorem Def6 defines " XXREAL_3:def_6_:_ for x, b2 being ext-real number holds ( ( x is real implies ( b2 = x " iff ex a being complex number st ( x = a & b2 = a " ) ) ) & ( not x is real implies ( b2 = x " iff b2 = 0 ) ) ); registration let x be real number ; let a be complex number ; identifyx " with a " when x = a; compatibility ( x = a implies x " = a " ) by Def6; end; definition let x, y be ext-real number ; funcx / y -> ext-real number equals :: XXREAL_3:def 7 x * (y "); coherence x * (y ") is ext-real number ; end; :: deftheorem defines / XXREAL_3:def_7_:_ 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 ; identifyx / y with a / b when x = a, y = b; compatibility ( x = a & y = b implies x / y = a / b ) proofend; end; Lm16: for x being ext-real number holds x * 0 = 0 proofend; registration let x be ext-real positive number ; let y be ext-real negative number ; clusterx * y -> ext-real negative ; coherence x * y is negative proofend; end; registration let x, y be ext-real negative number ; clusterx * y -> ext-real positive ; coherence x * y is positive proofend; end; registration let x, y be ext-real positive number ; clusterx * y -> ext-real positive ; coherence x * y is positive proofend; end; registration let x be ext-real non positive number ; let y be ext-real non negative number ; clusterx * y -> ext-real non positive ; coherence not x * y is positive proofend; end; registration let x, y be ext-real non positive number ; clusterx * y -> ext-real non negative ; coherence not x * y is negative proofend; end; registration let x, y be ext-real non negative number ; clusterx * y -> ext-real non negative ; coherence not x * y is negative proofend; end; registration let x be ext-real non positive number ; clusterx " -> ext-real non positive ; coherence not x " is positive proofend; end; registration let x be ext-real non negative number ; clusterx " -> ext-real non negative ; coherence not x " is negative proofend; end; registration let x be ext-real non negative number ; let y be ext-real non positive number ; clusterx / y -> ext-real non positive ; coherence not x / y is positive ; clustery / x -> ext-real non positive ; coherence not y / x is positive ; end; registration let x, y be ext-real non negative number ; clusterx / y -> ext-real non negative ; coherence not x / y is negative ; end; registration let x, y be ext-real non positive number ; clusterx / y -> ext-real non negative ; coherence not x / y is negative ; end; Lm17: for x, y being ext-real number st not x is real & x * y = 0 holds y = 0 proofend; registration let x, y be non zero ext-real number ; clusterx * y -> non zero ext-real ; coherence not x * y is zero proofend; end; registration let x be zero ext-real number ; let y be ext-real number ; clusterx * y -> zero ext-real for ext-real number ; coherence for b1 being ext-real number st b1 = x * y holds b1 is zero by Lm16; end; Lm18: for x, y, z being ext-real number st x = 0 holds x * (y * z) = (x * y) * z proofend; Lm19: for y, x, z being ext-real number st y = 0 holds x * (y * z) = (x * y) * z proofend; Lm20: for y, x, z being ext-real number st not y is real holds x * (y * z) = (x * y) * z proofend; Lm21: for x, y, z being ext-real number st not x is real holds x * (y * z) = (x * y) * z proofend; theorem Th66: :: XXREAL_3:66 for x, y, z being ext-real number holds x * (y * z) = (x * y) * z proofend; :: for ext-real numbers registration let r be real number ; clusterr " -> ext-real real ; coherence r " is real ; end; :: for ext-real numbers registration let r, s be real number ; clusterr * s -> ext-real real ; coherence r * s is real ; clusterr / s -> ext-real real ; coherence r / s is real ; end; registration cluster-infty " -> zero ext-real ; coherence -infty " is zero by Def6; cluster+infty " -> zero ext-real ; coherence +infty " is zero by Def6; end; theorem :: XXREAL_3:67 for f, g being ext-real number holds (f * g) " = (f ") * (g ") proofend; theorem :: XXREAL_3:68 for r being real number for f, g being ext-real number st r <> 0 & r * f = r * g holds f = g proofend; theorem Th69: :: XXREAL_3:69 for x, y being ext-real number st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds y = -infty proofend; theorem Th70: :: XXREAL_3:70 for x, y being ext-real number st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds y = -infty proofend; Lm22: for x, y being ext-real number holds ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) proofend; theorem Th71: :: XXREAL_3:71 for x, y, z being ext-real number st x <= y & 0 <= z holds x * z <= y * z proofend; theorem Th72: :: XXREAL_3:72 for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds x * z < y * z proofend; theorem :: XXREAL_3:73 for x, y being ext-real number holds ( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm22; theorem :: XXREAL_3:74 +infty " = 0 ; theorem :: XXREAL_3:75 -infty " = 0 ; theorem :: XXREAL_3:76 for x being ext-real number holds x / +infty = 0 ; theorem :: XXREAL_3:77 for x being ext-real number holds x / -infty = 0 ; theorem Th78: :: XXREAL_3:78 for x being ext-real number st x <> -infty & x <> +infty & x <> 0 holds x / x = 1 proofend; theorem :: XXREAL_3:79 for x, y, z being ext-real number st x <= y & 0 < z holds x / z <= y / z by Th71; theorem :: XXREAL_3:80 for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds x / z < y / z proofend; theorem Th81: :: XXREAL_3:81 for x being ext-real number holds 1 * x = x proofend; theorem Th82: :: XXREAL_3:82 for y being ext-real number holds ( not y " = 0 or y = +infty or y = -infty or y = 0 ) proofend; theorem Th83: :: XXREAL_3:83 for y being ext-real number st 0 < y & y <> +infty holds +infty / y = +infty proofend; theorem Th84: :: XXREAL_3:84 for y being ext-real number st y < 0 & -infty <> y holds -infty / y = +infty proofend; theorem Th85: :: XXREAL_3:85 for y being ext-real number st y < 0 & -infty <> y holds +infty / y = -infty proofend; theorem Th86: :: XXREAL_3:86 for y being ext-real number st 0 < y & y <> +infty holds -infty / y = -infty proofend; theorem :: XXREAL_3:87 for x being ext-real number st x <> +infty & x <> -infty & x <> 0 holds ( x * (1 / x) = 1 & (1 / x) * x = 1 ) proofend; theorem :: XXREAL_3:88 for y, x being ext-real number st -infty <> y & y <> +infty & y <> 0 holds ( (x * y) / y = x & x * (y / y) = x ) proofend; theorem :: XXREAL_3:89 for y being ext-real number holds ( +infty * y <> 1 & -infty * y <> 1 ) proofend; theorem :: XXREAL_3:90 for x, y being ext-real number st x * y <> +infty & x * y <> -infty & not x in REAL holds y in REAL proofend; begin theorem Th91: :: XXREAL_3:91 for x being ext-real number holds (- 1) * x = - x proofend; theorem Th92: :: XXREAL_3:92 for x, y being ext-real number holds - (x * y) = (- x) * y proofend; theorem Th93: :: XXREAL_3:93 for y, z, x being ext-real number st y = - z holds x * (y + z) = (x * y) + (x * z) proofend; theorem Th94: :: XXREAL_3:94 for x being ext-real number holds 2 * x = x + x proofend; Lm23: for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y) proofend; Lm24: for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) proofend; Lm25: for y, z being ext-real number holds 0 * (y + z) = (0 * y) + (0 * z) ; Lm26: for x, y, z being ext-real number st x is real & y is real holds x * (y + z) = (x * y) + (x * z) proofend; Lm27: for x, y, z being ext-real number st x is real & not y is real holds x * (y + z) = (x * y) + (x * z) proofend; theorem Th95: :: XXREAL_3:95 for x, y, z being ext-real number st x is real holds x * (y + z) = (x * y) + (x * z) proofend; theorem Th96: :: XXREAL_3:96 for y, z, x being ext-real number st y >= 0 & z >= 0 holds x * (y + z) = (x * y) + (x * z) proofend; theorem :: XXREAL_3:97 for y, z, x being ext-real number st y <= 0 & z <= 0 holds x * (y + z) = (x * y) + (x * z) proofend; theorem :: XXREAL_3:98 for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) by Lm24; theorem :: XXREAL_3:99 for f being ext-real number holds (- f) " = - (f ") proofend; theorem :: XXREAL_3:100 for x, y, z being ext-real number st x is real holds x * (y - z) = (x * y) - (x * z) proofend; theorem Th101: :: XXREAL_3:101 for x, y, z being ext-real number st x <= y & z <= 0 holds y * z <= x * z proofend; theorem Th102: :: XXREAL_3:102 for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds y * z < x * z proofend; theorem :: XXREAL_3:103 for x, y, z being ext-real number st x <= y & z < 0 holds y / z <= x / z by Th101; theorem :: XXREAL_3:104 for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds y / z < x / z proofend; theorem :: XXREAL_3:105 for x being ext-real number holds (x / 2) + (x / 2) = x proofend;