:: Introduction to Arithmetics :: by Andrzej Trybulec :: :: Received January 9, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin Lm1: {} in {{}} by TARSKI:def_1; theorem Th1: :: ARYTM_0:1 REAL+ c= REAL proofend; theorem Th2: :: ARYTM_0:2 for x being Element of REAL+ st x <> {} holds [{},x] in REAL proofend; theorem Th3: :: ARYTM_0:3 for y being set st [{},y] in REAL holds y <> {} proofend; theorem Th4: :: ARYTM_0:4 for x, y being Element of REAL+ holds x - y in REAL proofend; theorem Th5: :: ARYTM_0:5 REAL+ misses [:{{}},REAL+:] proofend; begin theorem Th6: :: ARYTM_0:6 for x, y being Element of REAL+ st x - y = {} holds x = y proofend; Lm2: for a, b being set holds not 1 = [a,b] proofend; theorem Th7: :: ARYTM_0:7 for x, y, z being Element of REAL+ st x <> {} & x *' y = x *' z holds y = z proofend; begin definition let x, y be Element of REAL ; func + (x,y) -> Element of REAL means :Def1: :: ARYTM_0:def 1 ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & it = x9 + y9 ) if ( x in REAL+ & y in REAL+ ) ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & it = x9 - y9 ) if ( x in REAL+ & y in [:{0},REAL+:] ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & it = y9 - x9 ) if ( y in REAL+ & x in [:{0},REAL+:] ) otherwise ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & it = [0,(x9 + y9)] ); existence ( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) proofend; uniqueness for b1, b2 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b2 = x9 + y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b2 = x9 - y9 ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b2 = y9 - x9 ) implies b1 = b2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b2 = [0,(x9 + y9)] ) implies b1 = b2 ) ) proofend; consistency for b1 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) ) by Th5, XBOOLE_0:3; commutativity for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) holds ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = y9 & b1 = x9 + y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = [0,y9] & b1 = x9 - y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = y9 & b1 = y9 - x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = [0,y9] & b1 = [0,(x9 + y9)] ) ) ) ; func * (x,y) -> Element of REAL means :Def2: :: ARYTM_0:def 2 ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & it = x9 *' y9 ) if ( x in REAL+ & y in REAL+ ) ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & it = [0,(x9 *' y9)] ) if ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & it = [0,(y9 *' x9)] ) if ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 ) ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & it = y9 *' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) otherwise it = 0 ; existence ( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ex b1 being Element of REAL st b1 = 0 ) ) proofend; uniqueness for b1, b2 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b2 = x9 *' y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b2 = [0,(x9 *' y9)] ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b2 = [0,(y9 *' x9)] ) implies b1 = b2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b2 = y9 *' x9 ) implies b1 = b2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; consistency for b1 being Element of REAL holds ( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) ) by Th5, XBOOLE_0:3; commutativity for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies b1 = 0 ) holds ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = y9 & b1 = x9 *' y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st ( y = x9 & x = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = y9 & b1 = [0,(y9 *' x9)] ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st ( y = [0,x9] & x = [0,y9] & b1 = y9 *' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) implies b1 = 0 ) ) ; end; :: deftheorem Def1 defines + ARYTM_0:def_1_:_ for x, y, b3 being Element of REAL holds ( ( x in REAL+ & y in REAL+ implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b3 = x9 + y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b3 = x9 - y9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b3 = y9 - x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b3 = [0,(x9 + y9)] ) ) ) ); :: deftheorem Def2 defines * ARYTM_0:def_2_:_ for x, y, b3 being Element of REAL holds ( ( x in REAL+ & y in REAL+ implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = y9 & b3 = x9 *' y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = x9 & y = [0,y9] & b3 = [0,(x9 *' y9)] ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = y9 & b3 = [0,(y9 *' x9)] ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st ( x = [0,x9] & y = [0,y9] & b3 = y9 *' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+:] or not y <> 0 ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( b3 = * (x,y) iff b3 = 0 ) ) ); definition let x be Element of REAL ; func opp x -> Element of REAL means :Def3: :: ARYTM_0:def 3 + (x,it) = 0 ; existence ex b1 being Element of REAL st + (x,b1) = 0 proofend; uniqueness for b1, b2 being Element of REAL st + (x,b1) = 0 & + (x,b2) = 0 holds b1 = b2 proofend; involutiveness for b1, b2 being Element of REAL st + (b2,b1) = 0 holds + (b1,b2) = 0 ; func inv x -> Element of REAL means :Def4: :: ARYTM_0:def 4 * (x,it) = 1 if x <> 0 otherwise it = 0 ; existence ( ( x <> 0 implies ex b1 being Element of REAL st * (x,b1) = 1 ) & ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) ) proofend; uniqueness for b1, b2 being Element of REAL holds ( ( x <> 0 & * (x,b1) = 1 & * (x,b2) = 1 implies b1 = b2 ) & ( not x <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; consistency for b1 being Element of REAL holds verum ; involutiveness for b1, b2 being Element of REAL st ( b2 <> 0 implies * (b2,b1) = 1 ) & ( not b2 <> 0 implies b1 = 0 ) holds ( ( b1 <> 0 implies * (b1,b2) = 1 ) & ( not b1 <> 0 implies b2 = 0 ) ) proofend; end; :: deftheorem Def3 defines opp ARYTM_0:def_3_:_ for x, b2 being Element of REAL holds ( b2 = opp x iff + (x,b2) = 0 ); :: deftheorem Def4 defines inv ARYTM_0:def_4_:_ for x, b2 being Element of REAL holds ( ( x <> 0 implies ( b2 = inv x iff * (x,b2) = 1 ) ) & ( not x <> 0 implies ( b2 = inv x iff b2 = 0 ) ) ); begin Lm3: for x, y, z being set st [x,y] = {z} holds ( z = {x} & x = y ) proofend; theorem Th8: :: ARYTM_0:8 for a, b being Element of REAL holds not (0,1) --> (a,b) in REAL proofend; definition let x, y be Element of REAL ; func[*x,y*] -> Element of COMPLEX equals :Def5: :: ARYTM_0:def 5 x if y = 0 otherwise (0,1) --> (x,y); consistency for b1 being Element of COMPLEX holds verum ; coherence ( ( y = 0 implies x is Element of COMPLEX ) & ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX ) ) proofend; end; :: deftheorem Def5 defines [* ARYTM_0:def_5_:_ for x, y being Element of REAL holds ( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) ); theorem :: ARYTM_0:9 for c being Element of COMPLEX ex r, s being Element of REAL st c = [*r,s*] proofend; theorem :: ARYTM_0:10 for x1, x2, y1, y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds ( x1 = y1 & x2 = y2 ) proofend; set RR = [:{0},REAL+:] \ {[0,0]}; reconsider o = 0 as Element of REAL ; theorem Th11: :: ARYTM_0:11 for x, o being Element of REAL st o = 0 holds + (x,o) = x proofend; theorem Th12: :: ARYTM_0:12 for x, o being Element of REAL st o = 0 holds * (x,o) = 0 proofend; theorem Th13: :: ARYTM_0:13 for x, y, z being Element of REAL holds * (x,(* (y,z))) = * ((* (x,y)),z) proofend; theorem Th14: :: ARYTM_0:14 for x, y, z being Element of REAL holds * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) proofend; theorem :: ARYTM_0:15 for x, y being Element of REAL holds * ((opp x),y) = opp (* (x,y)) proofend; theorem Th16: :: ARYTM_0:16 for x being Element of REAL holds * (x,x) in REAL+ proofend; theorem :: ARYTM_0:17 for x, y being Element of REAL st + ((* (x,x)),(* (y,y))) = 0 holds x = 0 proofend; theorem Th18: :: ARYTM_0:18 for x, y, z being Element of REAL st x <> 0 & * (x,y) = 1 & * (x,z) = 1 holds y = z proofend; theorem Th19: :: ARYTM_0:19 for x, y being Element of REAL st y = 1 holds * (x,y) = x proofend; reconsider j = 1 as Element of REAL ; theorem :: ARYTM_0:20 for x, y being Element of REAL st y <> 0 holds * ((* (x,y)),(inv y)) = x proofend; theorem Th21: :: ARYTM_0:21 for x, y being Element of REAL holds ( not * (x,y) = 0 or x = 0 or y = 0 ) proofend; theorem :: ARYTM_0:22 for x, y being Element of REAL holds inv (* (x,y)) = * ((inv x),(inv y)) proofend; theorem Th23: :: ARYTM_0:23 for x, y, z being Element of REAL holds + (x,(+ (y,z))) = + ((+ (x,y)),z) proofend; theorem :: ARYTM_0:24 for x, y being Element of REAL st [*x,y*] in REAL holds y = 0 proofend; theorem :: ARYTM_0:25 for x, y being Element of REAL holds opp (+ (x,y)) = + ((opp x),(opp y)) proofend;