:: ARYTM_1 semantic presentation

theorem Th1: :: ARYTM_1:1

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

proof end;

reconsider c₁ = one as Element of REAL+ by ARYTM_2:21;

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

proof end;

theorem Th2: :: ARYTM_1:2

for b₁, b₂ being Element of REAL+ holds
( not b₁ *' b₂ = {} or b₁ = {} or b₂ = {} )

proof end;

theorem Th3: :: ARYTM_1:3

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

proof end;

theorem Th4: :: ARYTM_1:4

for b₁, b₂ being Element of REAL+ st b₁ <=' b₂ & b₂ <=' b₁ holds
b₁ = b₂

proof end;

theorem Th5: :: ARYTM_1:5

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

proof end;

theorem Th6: :: ARYTM_1:6

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

proof end;

theorem Th7: :: ARYTM_1:7

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

proof end;

theorem Th8: :: ARYTM_1:8

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

proof end;

Lemma9: 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+ ;
func c₁ -' c₂ -> Element of REAL+ means :Def1: :: ARYTM_1:def 1
a₃ + a₂ = a₁ if a₂ <=' a₁
otherwise a₃ = {} ;
existence

proof end;

correctness by ARYTM_2:12;

end;

:: deftheorem Def1 defines -' ARYTM_1:def 1 :

Lemma11: for b₁ being Element of REAL+ holds b₁ -' b₁ = {}

proof end;

theorem Th9: :: ARYTM_1:9

for b₁, b₂ being Element of REAL+ holds
( b₁ <=' b₂ or b₁ -' b₂ <> {} )

proof end;

theorem Th10: :: ARYTM_1:10

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

proof end;

theorem Th11: :: ARYTM_1:11

for b₁, b₂ being Element of REAL+ holds b₁ -' b₂ <=' b₁

proof end;

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

proof end;

Lemma15: for b₁, b₂ being Element of REAL+ holds (b₁ + b₂) -' b₂ = b₁

proof end;

Lemma16: for b₁, b₂ being Element of REAL+ st b₁ <=' b₂ holds
b₂ -' (b₂ -' b₁) = b₁

proof end;

Lemma17: for b₁, b₂, b₃ being Element of REAL+ holds
( b₁ -' b₂ <=' b₃ iff b₁ <=' b₃ + b₂ )

proof end;

Lemma18: for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
( b₃ + b₁ <=' b₂ iff b₃ <=' b₂ -' b₁ )

proof end;

Lemma19: for b₁, b₂, b₃ being Element of REAL+ holds (b₁ -' b₂) -' b₃ = b₁ -' (b₃ + b₂)

proof end;

Lemma20: for b₁, b₂, b₃ being Element of REAL+ holds (b₁ -' b₂) -' b₃ = (b₁ -' b₃) -' b₂

proof end;

theorem Th12: :: ARYTM_1:12

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₁ <=' b₃ holds
b₂ + (b₃ -' b₁) = (b₂ -' b₁) + b₃

proof end;

theorem Th13: :: ARYTM_1:13

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₃ + (b₂ -' b₁) = (b₃ + b₂) -' b₁

proof end;

Lemma22: for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₃ -' (b₂ -' b₁) = (b₃ + b₁) -' b₂

proof end;

Lemma23: for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₃ <=' b₁ holds
b₂ -' (b₁ -' b₃) = (b₂ -' b₁) + b₃

proof end;

Lemma24: for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₃ <=' b₂ holds
b₁ -' (b₂ -' b₃) = b₃ -' (b₂ -' b₁)

proof end;

theorem Th14: :: ARYTM_1:14

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₃ <=' b₁ holds
(b₂ -' b₁) + b₃ = b₂ -' (b₁ -' b₃)

proof end;

theorem Th15: :: ARYTM_1:15

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₁ <=' b₃ holds
(b₃ -' b₁) + b₂ = (b₂ -' b₁) + b₃

proof end;

theorem Th16: :: ARYTM_1:16

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₃ -' b₂ <=' b₃ -' b₁

proof end;

theorem Th17: :: ARYTM_1:17

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₁ -' b₃ <=' b₂ -' b₃

proof end;

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

proof end;

definition

let c₂, c₃ be Element of REAL+ ;
func c₁ - c₂ -> set equals :Def2: :: ARYTM_1:def 2
a₁ -' a₂ if a₂ <=' a₁
otherwise [{} ,(a₂ -' a₁)];
correctness ;

end;

:: deftheorem Def2 defines - ARYTM_1:def 2 :

theorem Th18: :: ARYTM_1:18

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

proof end;

theorem Th19: :: ARYTM_1:19

for b₁, b₂ being Element of REAL+ st b₁ = {} & b₂ <> {} holds
b₁ - b₂ = [{} ,b₂]

proof end;

theorem Th20: :: ARYTM_1:20

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₃ + (b₂ -' b₁) = (b₃ + b₂) - b₁

proof end;

theorem Th21: :: ARYTM_1:21

for b₁, b₂, b₃ being Element of REAL+ st not b₁ <=' b₂ holds
b₃ - (b₁ -' b₂) = (b₃ + b₂) - b₁

proof end;

theorem Th22: :: ARYTM_1:22

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & not b₁ <=' b₃ holds
b₂ - (b₁ -' b₃) = (b₂ -' b₁) + b₃

proof end;

theorem Th23: :: ARYTM_1:23

for b₁, b₂, b₃ being Element of REAL+ st not b₁ <=' b₂ & not b₁ <=' b₃ holds
b₂ - (b₁ -' b₃) = b₃ - (b₁ -' b₂)

proof end;

theorem Th24: :: ARYTM_1:24

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ holds
b₂ - (b₁ + b₃) = (b₂ -' b₁) - b₃

proof end;

theorem Th25: :: ARYTM_1:25

for b₁, b₂, b₃ being Element of REAL+ st b₁ <=' b₂ & b₃ <=' b₂ holds
(b₂ -' b₃) - b₁ = (b₂ -' b₁) - b₃

proof end;

theorem Th26: :: ARYTM_1:26

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

proof end;

theorem Th27: :: ARYTM_1:27

for b₁, b₂, b₃ being Element of REAL+ st not b₁ <=' b₂ & b₃ <> {} holds
[{} ,(b₃ *' (b₁ -' b₂))] = (b₃ *' b₂) - (b₃ *' b₁)

proof end;

theorem Th28: :: ARYTM_1:28

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

proof end;