ARYTM_0: Introduction to Arithmetics

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

begin

Lm1: {} in {{} }
by TARSKI:def 1;

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;

begin

theorem Th6: :: ARYTM_0:6

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

proof end;

theorem :: ARYTM_0:7

canceled;

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

proof end;

theorem Th8: :: ARYTM_0:8

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

proof end;

begin

definition

let x, y be Element of REAL ;
canceled;
func + x,y -> Element of REAL means :Def2: :: ARYTM_0:def 2
ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' + y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & it = x' - y' ) if ( x in REAL+ & y in [:{0 },REAL+ :] )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & it = y' - x' ) if ( y in REAL+ & x in [:{0 },REAL+ :] )
otherwise ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & it = [0 ,(x' + y')] );
existence

proof end;

proof end;

consistency by Th5, XBOOLE_0:3;
commutativity ;
func * x,y -> Element of REAL means :Def3: :: ARYTM_0:def 3
ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' *' y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0 ,y'] & it = [0 ,(x' *' y')] ) if ( x in REAL+ & y in [:{0 },REAL+ :] & x <> 0 )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = y' & it = [0 ,(y' *' x')] ) if ( y in REAL+ & x in [:{0 },REAL+ :] & y <> 0 )
ex x', y' being Element of REAL+ st
( x = [0 ,x'] & y = [0 ,y'] & it = y' *' x' ) if ( x in [:{0 },REAL+ :] & y in [:{0 },REAL+ :] )
otherwise it = 0 ;
existence

proof end;

proof end;

consistency by Th5, XBOOLE_0:3;
commutativity ;

end;

:: deftheorem ARYTM_0:def 1 :

:: deftheorem Def2 defines + ARYTM_0:def 2 :

:: deftheorem Def3 defines * ARYTM_0:def 3 :

definition

let x be Element of REAL ;
func opp x -> Element of REAL means :Def4: :: ARYTM_0:def 4
+ x,it = 0 ;
existence

proof end;

proof end;

involutiveness ;
func inv x -> Element of REAL means :Def5: :: ARYTM_0:def 5
* x,it = 1 if x <> 0
otherwise it = 0 ;
existence

proof end;

proof end;

consistency ;
involutiveness

proof end;

end;

:: deftheorem Def4 defines opp ARYTM_0:def 4 :

:: deftheorem Def5 defines inv ARYTM_0:def 5 :

begin

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

proof end;

theorem :: ARYTM_0:9

canceled;

theorem Th10: :: ARYTM_0:10

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 ;
canceled;
func [*x,y*] -> Element of COMPLEX equals :Def7: :: ARYTM_0:def 7
x if y = 0
otherwise 0 ,1 --> x,y;
consistency ;
coherence

proof end;

end;

:: deftheorem ARYTM_0:def 6 :

:: deftheorem Def7 defines [* ARYTM_0:def 7 :

theorem :: ARYTM_0:11

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

proof end;

theorem :: ARYTM_0:12

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 ;

theorem Th13: :: ARYTM_0:13

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

proof end;

theorem Th14: :: ARYTM_0:14

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

proof end;

theorem Th15: :: ARYTM_0:15

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

proof end;

theorem Th16: :: ARYTM_0:16

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

proof end;

theorem :: ARYTM_0:17

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

proof end;

theorem Th18: :: ARYTM_0:18

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

proof end;

theorem :: ARYTM_0:19

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

proof end;

theorem Th20: :: ARYTM_0:20

for x, y, z being Element of REAL st x <> 0 & * x,y = 1 & * x,z = 1 holds
y = z

proof end;

theorem Th21: :: ARYTM_0:21

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

proof end;

reconsider j = 1 as Element of REAL ;

theorem :: ARYTM_0:22

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

proof end;

theorem Th23: :: ARYTM_0:23

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

proof end;

theorem :: ARYTM_0:24

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

proof end;

theorem Th25: :: ARYTM_0:25

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

proof end;

theorem :: ARYTM_0:26

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

proof end;

theorem :: ARYTM_0:27

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

proof end;