ARYTM_0: Introduction to Arithmetics

:: Introduction to Arithmetics
:: by Andrzej Trybulec
::
:: Received January 9, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users

environ

vocabularies HIDDEN, XBOOLE_0, ARYTM_2, TARSKI, NUMBERS, ZFMISC_1, SUBSET_1, ARYTM_1, ARYTM_3, CARD_1, RELAT_1, FUNCOP_1, ORDINAL1, FUNCT_2, FUNCT_1, ARYTM_0, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS;
definitions ORDINAL1;
theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, XBOOLE_1, ORDINAL3, ARYTM_3, FUNCT_2, FUNCT_4, FUNCT_1, ENUMSET1, NUMBERS, XTUPLE_0;
schemes ;
registrations XBOOLE_0, ORDINAL1, FUNCT_2, FUNCT_4, ARYTM_2, FUNCT_1, NUMBERS;
constructors HIDDEN, FUNCT_4, ARYTM_1, NUMBERS, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities NUMBERS, TARSKI, ARYTM_3, ORDINAL1;
expansions TARSKI, ORDINAL1;

Lm1: for x being Element of REAL+ holds [0,x] in [:{0},REAL+:]

proof end;

theorem Th1: :: ARYTM_0:1

proof end;

theorem Th2: :: ARYTM_0:2

for x being Element of REAL+ st x <> {} holds
[{},x] in REAL

proof end;

theorem Th3: :: ARYTM_0:3

for y being set st [{},y] in REAL holds
y <> {}

proof end;

theorem Th4: :: ARYTM_0:4

for x, y being Element of REAL+ holds x - y in REAL

proof end;

theorem Th5: :: ARYTM_0:5

REAL+ misses [:{{}},REAL+:]

proof end;

registration

let x, y be object ;

cluster [x,y] -> non zero ;

end;

theorem Th6: :: ARYTM_0:6

for x, y being Element of REAL+ st x - y = {} holds
x = y

proof end;

Lm2: for a, b being set holds not 1 = [a,b]

proof end;

theorem Th7: :: ARYTM_0:7

for x, y, z being Element of REAL+ st x <> {} & x *' y = x *' z holds
y = z

proof end;

Lm3: 0 in REAL
by NUMBERS:19;

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)] );

proof end;

proof end;

consistency by Th5, XBOOLE_0:3;
commutativity ;

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 ;

proof end;

proof end;

consistency by Th5, XBOOLE_0:3;
commutativity ;

end;

:: deftheorem Def1 defines + ARYTM_0:def 1 :

:: deftheorem Def2 defines * ARYTM_0:def 2 :

reconsider jj = 1 as Element of REAL by NUMBERS:19;

definition

let x be Element of REAL ;

func opp x -> Element of REAL means :Def3: :: ARYTM_0:def 3
+ (x,it) = 0 ;

proof end;

proof end;

involutiveness ;

func inv x -> Element of REAL means :Def4: :: ARYTM_0:def 4
* (x,it) = 1 if x <> 0
otherwise it = 0 ;

proof end;

proof end;

consistency ;
involutiveness

proof end;

end;

:: deftheorem Def3 defines opp ARYTM_0:def 3 :

:: deftheorem Def4 defines inv ARYTM_0:def 4 :

Lm4: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )

proof end;

theorem Th8: :: ARYTM_0:8

for a, b being Element of REAL holds not (0,1) --> (a,b) in REAL

proof end;

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 ;
coherence

proof end;

end;

:: deftheorem Def5 defines [* ARYTM_0:def 5 :

theorem :: ARYTM_0:9

for c being Element of COMPLEX ex r, s being Element of REAL st c = [*r,s*]

proof end;

theorem :: ARYTM_0:10

for x1, x2, y1, y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds
( x1 = y1 & x2 = y2 )

proof end;

set RR = [:{0},REAL+:] \ {[0,0]};

reconsider o = 0 as Element of REAL by Lm3;

theorem Th11: :: ARYTM_0:11

for x, o being Element of REAL st o = 0 holds
+ (x,o) = x

proof end;

theorem Th12: :: ARYTM_0:12

for x, o being Element of REAL st o = 0 holds
* (x,o) = 0

proof end;

theorem Th13: :: ARYTM_0:13

for x, y, z being Element of REAL holds * (x,(* (y,z))) = * ((* (x,y)),z)

proof end;

theorem Th14: :: ARYTM_0:14

for x, y, z being Element of REAL holds * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))

proof end;

theorem :: ARYTM_0:15

for x, y being Element of REAL holds * ((opp x),y) = opp (* (x,y))

proof end;

theorem Th16: :: ARYTM_0:16

for x being Element of REAL holds * (x,x) in REAL+

proof end;

theorem :: ARYTM_0:17

for x, y being Element of REAL st + ((* (x,x)),(* (y,y))) = 0 holds
x = 0

proof end;

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

proof end;

theorem Th19: :: ARYTM_0:19

for x, y being Element of REAL st y = 1 holds
* (x,y) = x

proof end;

theorem :: ARYTM_0:20

for x, y being Element of REAL st y <> 0 holds
* ((* (x,y)),(inv y)) = x

proof end;

theorem Th21: :: ARYTM_0:21

for x, y being Element of REAL holds
( not * (x,y) = 0 or x = 0 or y = 0 )

proof end;

theorem :: ARYTM_0:22

for x, y being Element of REAL holds inv (* (x,y)) = * ((inv x),(inv y))

proof end;

theorem Th23: :: ARYTM_0:23

for x, y, z being Element of REAL holds + (x,(+ (y,z))) = + ((+ (x,y)),z)

proof end;

theorem :: ARYTM_0:24

for x, y being Element of REAL st [*x,y*] in REAL holds
y = 0

proof end;

theorem :: ARYTM_0:25

for x, y being Element of REAL holds opp (+ (x,y)) = + ((opp x),(opp y))

proof end;