:: SQUARE_1 semantic presentation

registration

cluster -> complex Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem Th1: :: SQUARE_1:1

canceled;

theorem Th2: :: SQUARE_1:2

for b₁ being real number st 1 < b₁ holds
1 / b₁ < 1

proof end;

Lemma1: for b₁, b₂ being real number st b₁ < b₂ holds
0 < b₂ - b₁
by XREAL_1:52;

Lemma2: for b₁, b₂ being real number st b₁ <= b₂ holds
0 <= b₂ - b₁
by XREAL_1:50;

Lemma3: for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
0 <= b₁ * b₂
by XREAL_1:129;

Lemma4: for b₁, b₂ being real number st 0 < b₁ & 0 < b₂ holds
0 < b₁ * b₂
by XREAL_1:131;

Lemma5: for b₁, b₂ being real number st 0 < b₁ & b₂ < 0 holds
b₁ * b₂ < 0
by XREAL_1:134;

theorem Th3: :: SQUARE_1:3

canceled;

theorem Th4: :: SQUARE_1:4

canceled;

theorem Th5: :: SQUARE_1:5

canceled;

theorem Th6: :: SQUARE_1:6

canceled;

theorem Th7: :: SQUARE_1:7

canceled;

theorem Th8: :: SQUARE_1:8

canceled;

theorem Th9: :: SQUARE_1:9

canceled;

theorem Th10: :: SQUARE_1:10

canceled;

theorem Th11: :: SQUARE_1:11

canceled;

theorem Th12: :: SQUARE_1:12

canceled;

theorem Th13: :: SQUARE_1:13

canceled;

theorem Th14: :: SQUARE_1:14

canceled;

theorem Th15: :: SQUARE_1:15

canceled;

theorem Th16: :: SQUARE_1:16

canceled;

theorem Th17: :: SQUARE_1:17

canceled;

theorem Th18: :: SQUARE_1:18

canceled;

theorem Th19: :: SQUARE_1:19

canceled;

theorem Th20: :: SQUARE_1:20

canceled;

theorem Th21: :: SQUARE_1:21

canceled;

theorem Th22: :: SQUARE_1:22

canceled;

theorem Th23: :: SQUARE_1:23

canceled;

theorem Th24: :: SQUARE_1:24

canceled;

theorem Th25: :: SQUARE_1:25

for b₁, b₂ being real number holds
( not 0 <= b₁ * b₂ or ( 0 <= b₁ & 0 <= b₂ ) or ( b₁ <= 0 & b₂ <= 0 ) ) by Lemma5;

Lemma6: for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
0 <= b₁ / b₂
by XREAL_1:138;

Lemma7: for b₁, b₂ being real number st 0 < b₁ holds
b₂ - b₁ < b₂
by XREAL_1:46;

scheme :: SQUARE_1:sch 1
s1{ P₁[ set ], P₂[ set ] } :

ex b₁ being real number st
for b₂, b₃ being real number st P₁[b₂] & P₂[b₃] holds
( b₂ <= b₁ & b₁ <= b₃ )

provided

E8: for b₁, b₂ being real number st P₁[b₁] & P₂[b₂] holds
b₁ <= b₂

proof end;

definition

let c₁, c₂ be real number ;
func min c₁,c₂ -> real number equals :Def1: :: SQUARE_1:def 1
a₁ if a₁ <= a₂
otherwise a₂;
correctness ;
commutativity by XREAL_1:1;
idempotence ;
func max c₁,c₂ -> real number equals :Def2: :: SQUARE_1:def 2
a₁ if a₂ <= a₁
otherwise a₂;
correctness ;
commutativity by XREAL_1:1;
idempotence ;

end;

:: deftheorem Def1 defines min SQUARE_1:def 1 :

:: deftheorem Def2 defines max SQUARE_1:def 2 :

definition

let c₁, c₂ be Element of REAL ;
redefine func min as min c₁,c₂ -> Element of REAL ;
coherence by XREAL_0:def 1;
redefine func max as max c₁,c₂ -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

theorem Th26: :: SQUARE_1:26

canceled;

theorem Th27: :: SQUARE_1:27

canceled;

theorem Th28: :: SQUARE_1:28

canceled;

theorem Th29: :: SQUARE_1:29

canceled;

theorem Th30: :: SQUARE_1:30

canceled;

theorem Th31: :: SQUARE_1:31

canceled;

theorem Th32: :: SQUARE_1:32

canceled;

theorem Th33: :: SQUARE_1:33

canceled;

theorem Th34: :: SQUARE_1:34

canceled;

theorem Th35: :: SQUARE_1:35

for b₁, b₂ being real number holds min b₁,b₂ <= b₁

proof end;

theorem Th36: :: SQUARE_1:36

canceled;

theorem Th37: :: SQUARE_1:37

canceled;

theorem Th38: :: SQUARE_1:38

for b₁, b₂ being real number holds
( min b₁,b₂ = b₁ or min b₁,b₂ = b₂ )

proof end;

theorem Th39: :: SQUARE_1:39

for b₁, b₂, b₃ being real number holds
( ( b₁ <= b₂ & b₁ <= b₃ ) iff b₁ <= min b₂,b₃ )

proof end;

theorem Th40: :: SQUARE_1:40

for b₁, b₂, b₃ being real number holds min b₁,(min b₂,b₃) = min (min b₁,b₂),b₃

proof end;

theorem Th41: :: SQUARE_1:41

canceled;

theorem Th42: :: SQUARE_1:42

canceled;

theorem Th43: :: SQUARE_1:43

canceled;

theorem Th44: :: SQUARE_1:44

canceled;

theorem Th45: :: SQUARE_1:45

canceled;

theorem Th46: :: SQUARE_1:46

for b₁, b₂ being real number holds b₁ <= max b₁,b₂

proof end;

theorem Th47: :: SQUARE_1:47

canceled;

theorem Th48: :: SQUARE_1:48

canceled;

theorem Th49: :: SQUARE_1:49

for b₁, b₂ being real number holds
( max b₁,b₂ = b₁ or max b₁,b₂ = b₂ )

proof end;

theorem Th50: :: SQUARE_1:50

for b₁, b₂, b₃ being real number holds
( ( b₁ <= b₂ & b₃ <= b₂ ) iff max b₁,b₃ <= b₂ )

proof end;

theorem Th51: :: SQUARE_1:51

for b₁, b₂, b₃ being real number holds max b₁,(max b₂,b₃) = max (max b₁,b₂),b₃

proof end;

theorem Th52: :: SQUARE_1:52

canceled;

theorem Th53: :: SQUARE_1:53

for b₁, b₂ being real number holds (min b₁,b₂) + (max b₁,b₂) = b₁ + b₂

proof end;

theorem Th54: :: SQUARE_1:54

for b₁, b₂ being real number holds max b₁,(min b₁,b₂) = b₁

proof end;

theorem Th55: :: SQUARE_1:55

for b₁, b₂ being real number holds min b₁,(max b₁,b₂) = b₁

proof end;

theorem Th56: :: SQUARE_1:56

for b₁, b₂, b₃ being real number holds min b₁,(max b₂,b₃) = max (min b₁,b₂),(min b₁,b₃)

proof end;

theorem Th57: :: SQUARE_1:57

for b₁, b₂, b₃ being real number holds max b₁,(min b₂,b₃) = min (max b₁,b₂),(max b₁,b₃)

proof end;

definition

let c₁ be complex number ;
func c₁ ^2 -> set equals :: SQUARE_1:def 3
a₁ * a₁;
correctness ;

end;

:: deftheorem Def3 defines ^2 SQUARE_1:def 3 :

registration

let c₁ be complex number ;
cluster a₁ ^2 -> complex ;
correctness ;

end;

registration

let c₁ be real number ;
cluster a₁ ^2 -> complex real ;
correctness ;

end;

definition

let c₁ be Element of COMPLEX ;
redefine func ^2 as c₁ ^2 -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;

end;

definition

let c₁ be Element of REAL ;
redefine func ^2 as c₁ ^2 -> Element of REAL ;
correctness by XREAL_0:def 1;

end;

theorem Th58: :: SQUARE_1:58

canceled;

theorem Th59: :: SQUARE_1:59

1 ^2 = 1 ;

theorem Th60: :: SQUARE_1:60

0 ^2 = 0 ;

theorem Th61: :: SQUARE_1:61

for b₁ being complex number holds b₁ ^2 = (- b₁) ^2 ;

theorem Th62: :: SQUARE_1:62

canceled;

theorem Th63: :: SQUARE_1:63

for b₁, b₂ being complex number holds (b₁ + b₂) ^2 = ((b₁ ^2 ) + ((2 * b₁) * b₂)) + (b₂ ^2 ) ;

theorem Th64: :: SQUARE_1:64

for b₁, b₂ being complex number holds (b₁ - b₂) ^2 = ((b₁ ^2 ) - ((2 * b₁) * b₂)) + (b₂ ^2 ) ;

theorem Th65: :: SQUARE_1:65

for b₁ being complex number holds (b₁ + 1) ^2 = ((b₁ ^2 ) + (2 * b₁)) + 1 ;

theorem Th66: :: SQUARE_1:66

for b₁ being complex number holds (b₁ - 1) ^2 = ((b₁ ^2 ) - (2 * b₁)) + 1 ;

theorem Th67: :: SQUARE_1:67

for b₁, b₂ being complex number holds (b₁ - b₂) * (b₁ + b₂) = (b₁ ^2 ) - (b₂ ^2 ) ;

theorem Th68: :: SQUARE_1:68

for b₁, b₂ being complex number holds (b₁ * b₂) ^2 = (b₁ ^2 ) * (b₂ ^2 ) ;

theorem Th69: :: SQUARE_1:69

for b₁, b₂ being complex number holds (b₁ / b₂) ^2 = (b₁ ^2 ) / (b₂ ^2 ) by XCMPLX_1:77;

theorem Th70: :: SQUARE_1:70

for b₁, b₂ being complex number st (b₁ ^2 ) - (b₂ ^2 ) <> 0 holds
1 / (b₁ + b₂) = (b₁ - b₂) / ((b₁ ^2 ) - (b₂ ^2 ))

proof end;

theorem Th71: :: SQUARE_1:71

for b₁, b₂ being complex number st (b₁ ^2 ) - (b₂ ^2 ) <> 0 holds
1 / (b₁ - b₂) = (b₁ + b₂) / ((b₁ ^2 ) - (b₂ ^2 ))

proof end;

theorem Th72: :: SQUARE_1:72

for b₁ being real number holds 0 <= b₁ ^2 by XREAL_1:65;

theorem Th73: :: SQUARE_1:73

for b₁ being complex number st b₁ ^2 = 0 holds
b₁ = 0 by XCMPLX_1:6;

theorem Th74: :: SQUARE_1:74

for b₁ being real number st 0 <> b₁ holds
0 < b₁ ^2

proof end;

theorem Th75: :: SQUARE_1:75

for b₁ being real number st 0 < b₁ & b₁ < 1 holds
b₁ ^2 < b₁

proof end;

theorem Th76: :: SQUARE_1:76

for b₁ being real number st 1 < b₁ holds
b₁ < b₁ ^2

proof end;

Lemma25: for b₁ being real number st 0 < b₁ holds
ex b₂ being real number st
( 0 < b₂ & b₂ ^2 < b₁ )

proof end;

theorem Th77: :: SQUARE_1:77

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= b₂ holds
b₁ ^2 <= b₂ ^2

proof end;

theorem Th78: :: SQUARE_1:78

for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
b₁ ^2 < b₂ ^2

proof end;

Lemma28: for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ & b₁ ^2 = b₂ ^2 holds
b₁ = b₂

proof end;

definition

let c₁ be real number ;
assume E29: 0 <= c₁ ;
func sqrt c₁ -> real number means :Def4: :: SQUARE_1:def 4
( 0 <= a₂ & a₂ ^2 = a₁ );
existence

proof end;

uniqueness by Lemma28;

end;

:: deftheorem Def4 defines sqrt SQUARE_1:def 4 :

definition

let c₁ be Element of REAL ;
redefine func sqrt as sqrt c₁ -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

theorem Th79: :: SQUARE_1:79

canceled;

theorem Th80: :: SQUARE_1:80

canceled;

theorem Th81: :: SQUARE_1:81

canceled;

theorem Th82: :: SQUARE_1:82

sqrt 0 = 0 by Def4, Th60;

theorem Th83: :: SQUARE_1:83

sqrt 1 = 1 by Def4, Th59;

Lemma31: for b₁ being real number st 0 <= b₁ holds
sqrt (b₁ ^2 ) = b₁

proof end;

Lemma32: for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
sqrt b₁ < sqrt b₂

proof end;

theorem Th84: :: SQUARE_1:84

1 < sqrt 2 by Lemma32, Th83;

Lemma33: 2 ^2 = 2 * 2
;

theorem Th85: :: SQUARE_1:85

sqrt 4 = 2 by Def4, Lemma33;

theorem Th86: :: SQUARE_1:86

sqrt 2 < 2 by Lemma32, Th85;

theorem Th87: :: SQUARE_1:87

canceled;

theorem Th88: :: SQUARE_1:88

canceled;

theorem Th89: :: SQUARE_1:89

for b₁ being real number st 0 <= b₁ holds
sqrt (b₁ ^2 ) = b₁ by Lemma31;

theorem Th90: :: SQUARE_1:90

for b₁ being real number st b₁ <= 0 holds
sqrt (b₁ ^2 ) = - b₁

proof end;

theorem Th91: :: SQUARE_1:91

canceled;

theorem Th92: :: SQUARE_1:92

for b₁ being real number st 0 <= b₁ & sqrt b₁ = 0 holds
b₁ = 0 by Def4, Th60;

theorem Th93: :: SQUARE_1:93

for b₁ being real number st 0 < b₁ holds
0 < sqrt b₁

proof end;

theorem Th94: :: SQUARE_1:94

for b₁, b₂ being real number st 0 <= b₁ & b₁ <= b₂ holds
sqrt b₁ <= sqrt b₂

proof end;

theorem Th95: :: SQUARE_1:95

for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
sqrt b₁ < sqrt b₂ by Lemma32;

theorem Th96: :: SQUARE_1:96

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ & sqrt b₁ = sqrt b₂ holds
b₁ = b₂

proof end;

theorem Th97: :: SQUARE_1:97

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
sqrt (b₁ * b₂) = (sqrt b₁) * (sqrt b₂)

proof end;

theorem Th98: :: SQUARE_1:98

canceled;

theorem Th99: :: SQUARE_1:99

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
sqrt (b₁ / b₂) = (sqrt b₁) / (sqrt b₂)

proof end;

theorem Th100: :: SQUARE_1:100

canceled;

theorem Th101: :: SQUARE_1:101

for b₁ being real number st 0 < b₁ holds
sqrt (1 / b₁) = 1 / (sqrt b₁) by Th83, Th99;

theorem Th102: :: SQUARE_1:102

for b₁ being real number st 0 < b₁ holds
(sqrt b₁) / b₁ = 1 / (sqrt b₁)

proof end;

theorem Th103: :: SQUARE_1:103

for b₁ being real number st 0 < b₁ holds
b₁ / (sqrt b₁) = sqrt b₁

proof end;

theorem Th104: :: SQUARE_1:104

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
((sqrt b₁) - (sqrt b₂)) * ((sqrt b₁) + (sqrt b₂)) = b₁ - b₂

proof end;

Lemma37: for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ & b₁ <> b₂ holds
((sqrt b₁) ^2 ) - ((sqrt b₂) ^2 ) <> 0

proof end;

theorem Th105: :: SQUARE_1:105

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ & b₁ <> b₂ holds
1 / ((sqrt b₁) + (sqrt b₂)) = ((sqrt b₁) - (sqrt b₂)) / (b₁ - b₂)

proof end;

theorem Th106: :: SQUARE_1:106

for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
1 / ((sqrt b₂) + (sqrt b₁)) = ((sqrt b₂) - (sqrt b₁)) / (b₂ - b₁)

proof end;

theorem Th107: :: SQUARE_1:107

for b₁, b₂ being real number st 0 <= b₁ & 0 <= b₂ holds
1 / ((sqrt b₁) - (sqrt b₂)) = ((sqrt b₁) + (sqrt b₂)) / (b₁ - b₂)

proof end;

theorem Th108: :: SQUARE_1:108

for b₁, b₂ being real number st 0 <= b₁ & b₁ < b₂ holds
1 / ((sqrt b₂) - (sqrt b₁)) = ((sqrt b₂) + (sqrt b₁)) / (b₂ - b₁)

proof end;