:: Basic Operations on Extended Real Numbers :: by Andrzej Trybulec :: :: Received September 23, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_0, ORDINAL1, XREAL_0, SUBSET_1, CARD_1, ARYTM_3, XCMPLX_0, ARYTM_1, RELAT_1, NAT_1, REAL_1, INT_1; notations ORDINAL1, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NUMBERS, INT_1; constructors XBOOLE_0, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_2, INT_1; registrations XXREAL_0, XREAL_0, ORDINAL1, XCMPLX_0, NAT_1, INT_1; requirements SUBSET, NUMERALS, ARITHM, REAL; begin reserve x,y,z,w for ExtReal, r for Real; definition let x,y; redefine pred x <= y means :: 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; end; registration cluster non real positive for ExtReal; cluster non real negative for ExtReal; end; theorem :: XXREAL_3:1 for x being non real positive ExtReal holds x = +infty; theorem :: XXREAL_3:2 for x being non real negative ExtReal holds x = -infty; registration cluster non real non negative -> positive for ExtReal; cluster non real non positive -> negative for ExtReal; end; theorem :: XXREAL_3:3 x < z implies ex y being Real st x < y & y < z; begin :: addition definition let x,y be ExtReal; func x + y -> ExtReal means :: 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; commutativity; end; definition let x be ExtReal; func -x -> ExtReal means :: 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; involutiveness; end; definition let x,y be ExtReal; func x - y -> ExtReal equals :: XXREAL_3:def 4 x + -y; end; registration let x,y be Real, a,b be Complex; identify x+y with a+b when x = a, y = b; end; registration let x be Real, a be Complex; identify -x with -a when x = a; end; :: for ExtReals registration let r be Real; cluster -r -> real; end; :: for ExtReals registration let r,s be Real; cluster r+s -> real; cluster r-s -> real; end; registration let x be Real, y be non real ExtReal; cluster x+y -> non real for object; end; registration let x,y be non real positive ExtReal; cluster x+y -> non real; end; registration let x,y be non real negative ExtReal; cluster x+y -> non real; end; registration let x be non real negative ExtReal, y be non real positive ExtReal; cluster x+y -> zero; end; registration let x,y be Real, a,b be Complex; identify x-y with a-b when x = a, y = b; end; theorem :: XXREAL_3:4 x + 0 = x; theorem :: XXREAL_3:5 --infty = +infty; theorem :: XXREAL_3:6 -+infty = -infty; theorem :: XXREAL_3:7 x + -x = 0; theorem :: XXREAL_3:8 x+y = 0 implies x = -y; theorem :: XXREAL_3:9 -(x+y) = -x + -y; reserve f,g for ExtReal; theorem :: XXREAL_3:10 :: MEMBER_1:3 -f = -g implies f = g; theorem :: XXREAL_3:11 :: MEMBER_1:4 r+f = r+g implies f = g; theorem :: XXREAL_3:12 :: MEMBER_1:5 r-f = r-g implies f = g; theorem :: XXREAL_3:13 x <> +infty implies +infty - x = +infty & x - +infty = -infty; theorem :: XXREAL_3:14 x <> -infty implies -infty - x = -infty & x - -infty = +infty; theorem :: XXREAL_3:15 x - 0 = x; theorem :: XXREAL_3:16 x + y = +infty implies x = +infty or y = +infty; theorem :: XXREAL_3:17 x + y = -infty implies (x = -infty or y = -infty); theorem :: XXREAL_3:18 x - y = +infty implies (x = +infty or y = -infty); theorem :: XXREAL_3:19 x - y = -infty implies (x = -infty or y = +infty); theorem :: XXREAL_3:20 not ( x = +infty & y = -infty or x = -infty & y = +infty ) & x + y in REAL implies x in REAL & y in REAL; theorem :: XXREAL_3:21 not ( x = +infty & y = +infty or x = -infty & y = -infty ) & x - y in REAL implies x in REAL & y in REAL; theorem :: XXREAL_3:22 x is real implies y - x + x = y & y + x - x = y; theorem :: XXREAL_3:23 (x = +infty iff -x = -infty) & (x = -infty iff -x = +infty); theorem :: XXREAL_3:24 z is real implies x = x + z - z; theorem :: XXREAL_3:25 -(x + y) = -y - x; theorem :: XXREAL_3:26 -(x - y) = -x + y & -(x - y) = y - x; theorem :: XXREAL_3:27 -(-x + y) = x - y & -(-x + y) = x + -y; theorem :: XXREAL_3:28 0 <= y & y < +infty implies z = z + y - y; theorem :: XXREAL_3:29 not (x = +infty & y = -infty) & not (x = -infty & y = +infty) & not ( y = +infty & z = -infty or y = -infty & z = +infty ) & not ( x = +infty & z = -infty or x = -infty & z = +infty ) implies x + y + z = x + (y + z); theorem :: XXREAL_3:30 not (x = +infty & y = -infty) & not (x = -infty & y = +infty) & not (y = +infty & z = +infty) & not (y = -infty & z = -infty) & not (x = +infty & z = +infty) & not (x = -infty & z = -infty) implies x + y - z = x + (y - z) ; theorem :: XXREAL_3:31 :: extension of REAL_1:27 not (x = +infty & y = +infty) & not (x = -infty & y = -infty) & not (y = +infty & z = -infty) & not (y = -infty & z = +infty) & not (x = +infty & z = +infty) & not (x = -infty & z = -infty) implies x - y - z = x - (y + z); theorem :: XXREAL_3:32 not (x = +infty & y = +infty) & not (x = -infty & y = -infty) & not (y = +infty & z = +infty) & not (y = -infty & z = -infty) & not (x = +infty & z = -infty) & not (x = -infty & z = +infty) implies x - y + z = x - (y - z) ; theorem :: XXREAL_3:33 z is real implies (z + x) - (z + y) = x - y; theorem :: XXREAL_3:34 y is real implies (z - y) + (y - x) = z - x; begin registration let x,y be non negative ExtReal; cluster x + y -> non negative; end; registration let x,y be non positive ExtReal; cluster x + y -> non positive; end; registration let x be positive ExtReal; let y be non negative ExtReal; cluster x + y -> positive; cluster y + x -> positive; end; registration let x be negative ExtReal; let y be non positive ExtReal; cluster x + y -> negative; cluster y + x -> negative; end; registration let x be non positive ExtReal; cluster -x -> non negative; end; registration let x be non negative ExtReal; cluster -x -> non positive; end; registration let x be positive ExtReal; cluster -x -> negative; end; registration let x be negative ExtReal; cluster -x -> positive; end; registration let x be non negative ExtReal, y be non positive ExtReal; cluster x - y -> non negative; cluster y - x -> non positive; end; registration let x be positive ExtReal; let y be non positive ExtReal; cluster x - y -> positive; cluster y - x -> negative; end; registration let x be negative ExtReal; let y be non negative ExtReal; cluster x - y -> negative; cluster y - x -> positive; end; theorem :: XXREAL_3:35 x <= y implies x + z <= y + z; theorem :: XXREAL_3:36 x <= y & z <= w implies x + z <= y + w; theorem :: XXREAL_3:37 x <= y & z <= w implies x - w <= y - z; theorem :: XXREAL_3:38 x <= y iff - y <= - x; theorem :: XXREAL_3:39 0 <= z implies x <= x + z; theorem :: XXREAL_3:40 x <= y implies y-x >= 0; theorem :: XXREAL_3:41 (z = -infty & y = +infty implies x <= 0) & (z = +infty & y = -infty implies x <= 0) implies (x - y <= z implies x <= z + y); theorem :: XXREAL_3:42 (x = +infty & y = +infty implies 0 <= z) & (x = -infty & y = -infty implies 0 <= z) implies (x <= z + y implies x - y <= z); theorem :: XXREAL_3:43 z in REAL & x < y implies x + z < y + z & x - z < y - z; theorem :: XXREAL_3:44 0<= x & 0<= y & 0<= z implies (x + y) + z = x + (y + z); theorem :: XXREAL_3:45 x is real implies (y + x <= z iff y <= z - x); theorem :: XXREAL_3:46 0 < x & x < y implies 0 < y - x; theorem :: XXREAL_3:47 0 <= x & 0 <= z & z + x < y implies z < y - x; theorem :: XXREAL_3:48 0 <= x & 0 <= z & z + x < y implies z <= y; theorem :: XXREAL_3:49 0 <= x & x < z implies ex y being Real st 0 < y & x + y < z; theorem :: XXREAL_3:50 0 < x implies ex y being Real st 0 < y & y + y < x; theorem :: XXREAL_3:51 x < y & x < +infty & -infty < y implies 0 < y- x; theorem :: XXREAL_3:52 not ( x = +infty & y = -infty or x = -infty & y = +infty ) & x + y < z implies x <> +infty & y <> +infty & z <> -infty & x < z - y; theorem :: XXREAL_3:53 not ( z = +infty & y = +infty or z = -infty & y = -infty ) & x < z - y implies x <> +infty & y <> +infty & z <> -infty & x + y < z; theorem :: XXREAL_3:54 not ( x = +infty & y = +infty or x = -infty & y = -infty ) & x - y < z implies x <> +infty & y <> -infty & z <> -infty & x < z + y; theorem :: XXREAL_3:55 not ( z = +infty & y = -infty or z = -infty & y = +infty ) & x < z + y implies x <> +infty & y <> -infty & z <> -infty & x - y < z; theorem :: XXREAL_3:56 not ( x = +infty & y = -infty or x = -infty & y = +infty or y = +infty & z = +infty or y = -infty & z = -infty ) & x + y <= z implies y <> +infty & x <= z - y; theorem :: XXREAL_3:57 not (x = +infty & y = -infty) & not (x = -infty & y = +infty) & not (y = +infty & z = +infty) & x <= z - y implies y <> +infty & x + y <= z; theorem :: XXREAL_3:58 not ( x = +infty & y = +infty or x = -infty & y = -infty or y = +infty & z = -infty or y = -infty & z = +infty ) & x - y <= z implies y <> -infty; theorem :: XXREAL_3:59 not (x = -infty & y = -infty) & not (y = -infty & z = +infty) & x <= z + y implies y <> -infty; theorem :: XXREAL_3:60 (x <= -y implies y <= -x) & (-x <= y implies -y <= x); theorem :: XXREAL_3:61 (for e be Real st 0 < e holds x < y + e) implies x <= y; reserve t for ExtReal; theorem :: XXREAL_3:62 t <> -infty & t <> +infty & x < y implies x + t < y + t; theorem :: XXREAL_3:63 t <> -infty & t <> +infty & x < y implies x - t < y - t; theorem :: XXREAL_3:64 x < y & w < z implies x + w < y + z; theorem :: XXREAL_3:65 0 <= x & z + x <= y implies z <= y; begin :: multiplication definition let x,y be ExtReal; func x * y -> ExtReal means :: 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 (x is not real or y is not real) & (x is positive & y is positive or x is negative & y is negative), it = -infty if (x is not real or y is not real) & (x is positive & y is negative or x is negative & y is positive) otherwise it = 0; commutativity; end; registration let x,y be Real, a,b be Complex; identify x*y with a*b when x = a, y = b; end; definition let x be ExtReal; func x" -> ExtReal means :: XXREAL_3:def 6 ex a being Complex st x = a & it = a" if x is real otherwise it = 0; end; registration let x be Real, a be Complex; identify x" with a" when x = a; end; definition let x,y be ExtReal; func x / y -> ExtReal equals :: XXREAL_3:def 7 x * y"; end; registration let x,y be Real, a,b be Complex; identify x/y with a/b when x = a, y = b; end; registration let x be positive ExtReal, y be negative ExtReal; cluster x*y -> negative; end; registration let x,y be negative ExtReal; cluster x*y -> positive; end; registration let x,y be positive ExtReal; cluster x*y -> positive; end; registration let x be non positive ExtReal, y be non negative ExtReal; cluster x*y -> non positive; end; registration let x,y be non positive ExtReal; cluster x*y -> non negative; end; registration let x,y be non negative ExtReal; cluster x*y -> non negative; end; registration let x be non positive ExtReal; cluster x" -> non positive; end; registration let x be non negative ExtReal; cluster x" -> non negative; end; registration let x be non negative ExtReal, y be non positive ExtReal; cluster x/y -> non positive; cluster y/x -> non positive; end; registration let x,y be non negative ExtReal; cluster x/y -> non negative; end; registration let x,y be non positive ExtReal; cluster x/y -> non negative; end; registration let x,y be non zero ExtReal; cluster x*y -> non zero; end; registration let x be zero ExtReal, y be ExtReal; cluster x*y -> zero for ExtReal; end; theorem :: XXREAL_3:66 x*(y*z) = (x*y)*z; :: for ExtReals registration let r be Real; cluster r" -> real; end; :: for ExtReals registration let r,s be Real; cluster r*s -> real; cluster r/s -> real; end; registration cluster -infty" -> zero; cluster +infty" -> zero; end; theorem :: XXREAL_3:67 :: MEMBER_1:2 (f*g)" = f"*g"; theorem :: XXREAL_3:68 :: MEMBER_1:6 r <> 0 & r*f = r*g implies f = g; theorem :: XXREAL_3:69 x <> +infty & x <> -infty & x * y = +infty implies y = +infty or y = -infty; theorem :: XXREAL_3:70 x <> +infty & x <> -infty & x * y = -infty implies y = +infty or y = -infty; theorem :: XXREAL_3:71 x <= y & 0 <= z implies x*z <= y*z; theorem :: XXREAL_3:72 x < y & 0 < z & z <> +infty implies x*z < y*z; theorem :: XXREAL_3:73 x*y in REAL implies x in REAL & y in REAL or x*y = 0; theorem :: XXREAL_3:74 +infty" = 0; theorem :: XXREAL_3:75 -infty" = 0; theorem :: XXREAL_3:76 x/+infty = 0; theorem :: XXREAL_3:77 x/-infty = 0; theorem :: XXREAL_3:78 x <> -infty & x <> +infty & x <> 0 implies x / x = 1; theorem :: XXREAL_3:79 x <= y & 0 < z implies x/z <= y/z; theorem :: XXREAL_3:80 x < y & 0 < z & z <> +infty implies x/z < y/z; theorem :: XXREAL_3:81 1*x = x; theorem :: XXREAL_3:82 y" = 0 implies y = +infty or y = -infty or y = 0; theorem :: XXREAL_3:83 0 < y & y <> +infty implies +infty / y = +infty; theorem :: XXREAL_3:84 y < 0 & -infty <> y implies -infty / y = +infty; theorem :: XXREAL_3:85 y < 0 & -infty <> y implies +infty / y = -infty; theorem :: XXREAL_3:86 0 < y & y <> +infty implies -infty / y = -infty; theorem :: XXREAL_3:87 :: extension of REAL_1:34 x <> +infty & x <> -infty & x <> 0 implies x*(1/x) = 1 & (1/x)*x = 1; theorem :: XXREAL_3:88 -infty <> y & y <> +infty & y <> 0 implies x * y / y = x & x * (y / y) = x; theorem :: XXREAL_3:89 +infty * y <> 1 & -infty * y <> 1; theorem :: XXREAL_3:90 x * y <> +infty & x * y <> -infty implies x in REAL or y in REAL; begin :: distributivity theorem :: XXREAL_3:91 (-1)*x = -x; theorem :: XXREAL_3:92 - x*y = (-x)*y; theorem :: XXREAL_3:93 y = -z implies x*(y+z) = x*y +x*z; theorem :: XXREAL_3:94 2*x = x+x; theorem :: XXREAL_3:95 x is real implies x*(y+z) = x*y +x*z; theorem :: XXREAL_3:96 y>=0 & z>=0 implies x*(y+z) = x*y +x*z; theorem :: XXREAL_3:97 y<=0 & z<=0 implies x*(y+z) = x*y +x*z; theorem :: XXREAL_3:98 x*(0+z) = x*0 +x*z; theorem :: XXREAL_3:99 :: MEMBER_1:1 (-f)" = -f"; theorem :: XXREAL_3:100 x is real implies x * (y - z) = x * y - x * z; theorem :: XXREAL_3:101 x <= y & z <= 0 implies y*z <= x*z; theorem :: XXREAL_3:102 x < y & z < 0 & z <> -infty implies y*z < x*z; theorem :: XXREAL_3:103 x <= y & z < 0 implies y/z <= x/z; theorem :: XXREAL_3:104 x < y & z < 0 & z <> -infty implies y/z < x/z; theorem :: XXREAL_3:105 x/2 + x/2 = x; registration let x,y be Nat; cluster x+y -> natural; cluster x*y -> natural; end; registration cluster -1 -> dim-like; let n be dim-like number; cluster n+1 -> natural; end;