:: ARYTM_0 semantic presentation

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

E2: now

let c₁ be set ;
assume E3: one = [0,c₁] ;
{0} = 0 \/ {0}
.= succ 0 by ORDINAL1:def 1
.= {{0},{0,c₁}} by E3, ORDINAL2:def 4, TARSKI:def 5 ;
then {0} in {0} by TARSKI:def 2;
hence contradiction ;

end;

theorem Th1: :: ARYTM_0:1

proof end;

theorem Th2: :: ARYTM_0:2

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

proof end;

theorem Th3: :: ARYTM_0:3

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

proof end;

theorem Th4: :: ARYTM_0:4

for b₁, b₂ being Element of REAL+ holds b₁ - b₂ in REAL

proof end;

theorem Th5: :: ARYTM_0:5

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

proof end;

theorem Th6: :: ARYTM_0:6

for b₁, b₂ being Element of REAL+ st b₁ - b₂ = {} holds
b₁ = b₂

proof end;

theorem Th7: :: ARYTM_0:7

for b₁, b₂ being set holds not one = [b₁,b₂]

proof end;

theorem Th8: :: ARYTM_0:8

for b₁, b₂, b₃ being Element of REAL+ st b₁ <> {} & b₁ *' b₂ = b₁ *' b₃ holds
b₂ = b₃

proof end;

definition

let c₁, c₂ be Element of REAL ;
canceled;
func + c₁,c₂ -> Element of REAL means :Def2: :: ARYTM_0:def 2
ex b₁, b₂ being Element of REAL+ st
( a₁ = b₁ & a₂ = b₂ & a₃ = b₁ + b₂ ) if ( a₁ in REAL+ & a₂ in REAL+ )
ex b₁, b₂ being Element of REAL+ st
( a₁ = b₁ & a₂ = [0,b₂] & a₃ = b₁ - b₂ ) if ( a₁ in REAL+ & a₂ in [:{0},REAL+ :] )
ex b₁, b₂ being Element of REAL+ st
( a₁ = [0,b₁] & a₂ = b₂ & a₃ = b₂ - b₁ ) if ( a₂ in REAL+ & a₁ in [:{0},REAL+ :] )
otherwise ex b₁, b₂ being Element of REAL+ st
( a₁ = [0,b₁] & a₂ = [0,b₂] & a₃ = [0,(b₁ + b₂)] );
existence

proof end;

proof end;

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

proof end;

proof end;

consistency by Th5, XBOOLE_0:3;
commutativity ;

end;

:: deftheorem Def1 ARYTM_0:def 1 :

:: deftheorem Def2 defines + ARYTM_0:def 2 :

:: deftheorem Def3 defines * ARYTM_0:def 3 :

definition

let c₁ be Element of REAL ;
func opp c₁ -> Element of REAL means :Def4: :: ARYTM_0:def 4
+ a₁,a₂ = 0;
existence

proof end;

proof end;

involutiveness ;
func inv c₁ -> Element of REAL means :Def5: :: ARYTM_0:def 5
* a₁,a₂ = one if a₁ <> 0
otherwise a₂ = 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 :

Lemma15: for b₁, b₂, b₃ being set st [b₁,b₂] = {b₃} holds
( b₃ = {b₁} & b₁ = b₂ )

proof end;

theorem Th9: :: ARYTM_0:9

canceled;

theorem Th10: :: ARYTM_0:10

for b₁, b₂ being Element of REAL holds not 0,one --> b₁,b₂ in REAL

proof end;

definition

let c₁, c₂ be Element of REAL ;
canceled;
func [*c₁,c₂*] -> Element of COMPLEX equals :Def7: :: ARYTM_0:def 7
a₁ if a₂ = 0
otherwise 0,one --> a₁,a₂;
consistency ;
coherence

proof end;

end;

:: deftheorem Def6 ARYTM_0:def 6 :

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

theorem Th11: :: ARYTM_0:11

for b₁ being Element of COMPLEX ex b₂, b₃ being Element of REAL st b₁ = [*b₂,b₃*]

proof end;

theorem Th12: :: ARYTM_0:12

for b₁, b₂, b₃, b₄ being Element of REAL st [*b₁,b₂*] = [*b₃,b₄*] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

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

reconsider c₂ = 0 as Element of REAL by Th1, ARYTM_2:21;

theorem Th13: :: ARYTM_0:13

for b₁, b₂ being Element of REAL st b₂ = 0 holds
+ b₁,b₂ = b₁

proof end;

theorem Th14: :: ARYTM_0:14

for b₁, b₂ being Element of REAL st b₂ = 0 holds
* b₁,b₂ = 0

proof end;

theorem Th15: :: ARYTM_0:15

for b₁, b₂, b₃ being Element of REAL holds * b₁,(* b₂,b₃) = * (* b₁,b₂),b₃

proof end;

theorem Th16: :: ARYTM_0:16

for b₁, b₂, b₃ being Element of REAL holds * b₁,(+ b₂,b₃) = + (* b₁,b₂),(* b₁,b₃)

proof end;

theorem Th17: :: ARYTM_0:17

for b₁, b₂ being Element of REAL holds * (opp b₁),b₂ = opp (* b₁,b₂)

proof end;

theorem Th18: :: ARYTM_0:18

for b₁ being Element of REAL holds * b₁,b₁ in REAL+

proof end;

theorem Th19: :: ARYTM_0:19

for b₁, b₂ being Element of REAL st + (* b₁,b₁),(* b₂,b₂) = 0 holds
b₁ = 0

proof end;

theorem Th20: :: ARYTM_0:20

for b₁, b₂, b₃ being Element of REAL st b₁ <> 0 & * b₁,b₂ = one & * b₁,b₃ = one holds
b₂ = b₃

proof end;

theorem Th21: :: ARYTM_0:21

for b₁, b₂ being Element of REAL st b₂ = one holds
* b₁,b₂ = b₁

proof end;

reconsider c₃ = one as Element of REAL by Th1, ARYTM_2:21;

theorem Th22: :: ARYTM_0:22

for b₁, b₂ being Element of REAL st b₂ <> 0 holds
* (* b₁,b₂),(inv b₂) = b₁

proof end;

theorem Th23: :: ARYTM_0:23

for b₁, b₂ being Element of REAL holds
( not * b₁,b₂ = 0 or b₁ = 0 or b₂ = 0 )

proof end;

theorem Th24: :: ARYTM_0:24

for b₁, b₂ being Element of REAL holds inv (* b₁,b₂) = * (inv b₁),(inv b₂)

proof end;

theorem Th25: :: ARYTM_0:25

for b₁, b₂, b₃ being Element of REAL holds + b₁,(+ b₂,b₃) = + (+ b₁,b₂),b₃

proof end;

theorem Th26: :: ARYTM_0:26

for b₁, b₂ being Element of REAL st [*b₁,b₂*] in REAL holds
b₂ = 0

proof end;

theorem Th27: :: ARYTM_0:27

for b₁, b₂ being Element of REAL holds opp (+ b₁,b₂) = + (opp b₁),(opp b₂)

proof end;