:: Some Properties of Real Numbers. Operations: min, max, square, and square root
:: by Andrzej Trybulec and Czes{\l}aw Byli\'nski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

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

ex z being real number st
for x, y being real number st P₁[x] & P₂[y] holds
( x <= z & z <= y )

provided

A1: for x, y being real number st P₁[x] & P₂[y] holds
x <= y

proof end;

definition

let x, y be Element of REAL ;
:: original: min
redefine func min (x,y) -> Element of REAL ;
coherence
min (x,y) is Element of REAL by XREAL_0:def 1;
:: original: max
redefine func max (x,y) -> Element of REAL ;
coherence
max (x,y) is Element of REAL by XREAL_0:def 1;

end;

theorem :: SQUARE_1:1

canceled;

theorem :: SQUARE_1:2

canceled;

theorem :: SQUARE_1:3

canceled;

theorem :: SQUARE_1:4

canceled;

theorem :: SQUARE_1:5

canceled;

theorem :: SQUARE_1:6

canceled;

theorem :: SQUARE_1:7

canceled;

theorem :: SQUARE_1:8

canceled;

theorem :: SQUARE_1:9

canceled;

theorem :: SQUARE_1:10

canceled;

theorem :: SQUARE_1:11

canceled;

theorem :: SQUARE_1:12

canceled;

theorem :: SQUARE_1:13

canceled;

theorem :: SQUARE_1:14

canceled;

theorem :: SQUARE_1:15

canceled;

theorem :: SQUARE_1:16

canceled;

theorem :: SQUARE_1:17

canceled;

theorem :: SQUARE_1:18

canceled;

theorem :: SQUARE_1:19

canceled;

theorem :: SQUARE_1:20

canceled;

theorem :: SQUARE_1:21

canceled;

theorem :: SQUARE_1:22

canceled;

theorem :: SQUARE_1:23

canceled;

theorem :: SQUARE_1:24

canceled;

theorem :: SQUARE_1:25

canceled;

theorem :: SQUARE_1:26

canceled;

theorem :: SQUARE_1:27

canceled;

theorem :: SQUARE_1:28

canceled;

theorem :: SQUARE_1:29

canceled;

theorem :: SQUARE_1:30

canceled;

theorem :: SQUARE_1:31

canceled;

theorem :: SQUARE_1:32

canceled;

theorem :: SQUARE_1:33

canceled;

theorem :: SQUARE_1:34

canceled;

theorem :: SQUARE_1:35

canceled;

theorem :: SQUARE_1:36

canceled;

theorem :: SQUARE_1:37

canceled;

theorem :: SQUARE_1:38

canceled;

theorem :: SQUARE_1:39

canceled;

theorem :: SQUARE_1:40

canceled;

theorem :: SQUARE_1:41

canceled;

theorem :: SQUARE_1:42

canceled;

theorem :: SQUARE_1:43

canceled;

theorem :: SQUARE_1:44

canceled;

theorem :: SQUARE_1:45

canceled;

theorem :: SQUARE_1:46

canceled;

theorem :: SQUARE_1:47

canceled;

theorem :: SQUARE_1:48

canceled;

theorem :: SQUARE_1:49

canceled;

theorem :: SQUARE_1:50

canceled;

theorem :: SQUARE_1:51

canceled;

theorem :: SQUARE_1:52

canceled;

theorem :: SQUARE_1:53

for x, y being real number holds (min (x,y)) + (max (x,y)) = x + y

proof end;

theorem :: SQUARE_1:54

for x, y being real number st 0 <= x & 0 <= y holds
max (x,y) <= x + y

proof end;

definition

let x be complex number ;
canceled;
canceled;
func x ^2 -> set equals :: SQUARE_1:def 3
x * x;
correctness
coherence
x * x is set ;
;

end;

:: deftheorem SQUARE_1:def 1 :
canceled;

:: deftheorem SQUARE_1:def 2 :
canceled;

:: deftheorem defines ^2 SQUARE_1:def 3 :
for x being complex number holds x ^2 = x * x;

registration

let x be complex number ;
cluster x ^2 -> complex ;
coherence
x ^2 is complex ;

end;

registration

let x be real number ;
cluster x ^2 -> real ;
coherence
x ^2 is real ;

end;

definition

let x be Element of COMPLEX ;
:: original: ^2
redefine func x ^2 -> Element of COMPLEX ;
coherence
x ^2 is Element of COMPLEX by XCMPLX_0:def 2;

end;

definition

let x be Element of REAL ;
:: original: ^2
redefine func x ^2 -> Element of REAL ;
coherence
x ^2 is Element of REAL by XREAL_0:def 1;

end;

theorem :: SQUARE_1:55

canceled;

theorem :: SQUARE_1:56

canceled;

theorem :: SQUARE_1:57

canceled;

theorem :: SQUARE_1:58

canceled;

theorem :: SQUARE_1:59

canceled;

theorem :: SQUARE_1:60

canceled;

theorem :: SQUARE_1:61

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

theorem :: SQUARE_1:62

canceled;

theorem :: SQUARE_1:63

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

theorem :: SQUARE_1:64

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

theorem :: SQUARE_1:65

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

theorem :: SQUARE_1:66

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

theorem :: SQUARE_1:67

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

theorem :: SQUARE_1:68

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

theorem :: SQUARE_1:69

canceled;

theorem Th70: :: SQUARE_1:70

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

proof end;

theorem Th71: :: SQUARE_1:71

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

proof end;

theorem :: SQUARE_1:72

canceled;

theorem :: SQUARE_1:73

canceled;

theorem :: SQUARE_1:74

for a being real number st 0 <> a holds
0 < a ^2 by XREAL_1:65;

theorem Th75: :: SQUARE_1:75

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

proof end;

theorem Th76: :: SQUARE_1:76

for a being real number st 1 < a holds
a < a ^2

proof end;

Lm1: for a being real number st 0 < a holds
ex x being real number st
( 0 < x & x ^2 < a )

proof end;

theorem Th77: :: SQUARE_1:77

for x, y being real number st 0 <= x & x <= y holds
x ^2 <= y ^2

proof end;

theorem Th78: :: SQUARE_1:78

for x, y being real number st 0 <= x & x < y holds
x ^2 < y ^2

proof end;

Lm2: for x, y being real number st 0 <= x & 0 <= y & x ^2 = y ^2 holds
x = y

proof end;

definition

let a be real number ;
assume A1: 0 <= a ;
func sqrt a -> real number means :Def4: :: SQUARE_1:def 4
( 0 <= it & it ^2 = a );
existence
ex b₁ being real number st
( 0 <= b₁ & b₁ ^2 = a )

proof end;

uniqueness
for b₁, b₂ being real number st 0 <= b₁ & b₁ ^2 = a & 0 <= b₂ & b₂ ^2 = a holds
b₁ = b₂ by Lm2;

end;

:: deftheorem Def4 defines sqrt SQUARE_1:def 4 :
for a being real number st 0 <= a holds
for b₂ being real number holds
( b₂ = sqrt a iff ( 0 <= b₂ & b₂ ^2 = a ) );

definition

let a be Element of REAL ;
:: original: sqrt
redefine func sqrt a -> Element of REAL ;
coherence
sqrt a is Element of REAL by XREAL_0:def 1;

end;

theorem :: SQUARE_1:79

canceled;

theorem :: SQUARE_1:80

canceled;

theorem :: SQUARE_1:81

canceled;

theorem Th82: :: SQUARE_1:82

sqrt 0 = 0

proof end;

theorem Th83: :: SQUARE_1:83

sqrt 1 = 1

proof end;

Lm3: for x, y being real number st 0 <= x & x < y holds
sqrt x < sqrt y

proof end;

theorem :: SQUARE_1:84

1 < sqrt 2 by Lm3, Th83;

Lm4: 2 ^2 = 2 * 2
;

theorem Th85: :: SQUARE_1:85

sqrt 4 = 2 by Def4, Lm4;

theorem :: SQUARE_1:86

sqrt 2 < 2 by Lm3, Th85;

theorem :: SQUARE_1:87

canceled;

theorem :: SQUARE_1:88

canceled;

theorem :: SQUARE_1:89

for a being real number st 0 <= a holds
sqrt (a ^2) = a by Def4;

theorem :: SQUARE_1:90

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

proof end;

theorem :: SQUARE_1:91

canceled;

theorem Th92: :: SQUARE_1:92

for a being real number st 0 <= a & sqrt a = 0 holds
a = 0

proof end;

theorem Th93: :: SQUARE_1:93

for a being real number st 0 < a holds
0 < sqrt a

proof end;

theorem Th94: :: SQUARE_1:94

for x, y being real number st 0 <= x & x <= y holds
sqrt x <= sqrt y

proof end;

theorem :: SQUARE_1:95

for x, y being real number st 0 <= x & x < y holds
sqrt x < sqrt y by Lm3;

theorem Th96: :: SQUARE_1:96

for x, y being real number st 0 <= x & 0 <= y & sqrt x = sqrt y holds
x = y

proof end;

theorem Th97: :: SQUARE_1:97

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

proof end;

theorem :: SQUARE_1:98

canceled;

theorem Th99: :: SQUARE_1:99

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

proof end;

theorem :: SQUARE_1:100

for a, b being real number st 0 <= a & 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) ) by Th82, Th92;

theorem :: SQUARE_1:101

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

theorem :: SQUARE_1:102

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

proof end;

theorem :: SQUARE_1:103

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

proof end;

theorem :: SQUARE_1:104

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

proof end;

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

proof end;

theorem :: SQUARE_1:105

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

proof end;

theorem :: SQUARE_1:106

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

proof end;

theorem :: SQUARE_1:107

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

proof end;

theorem :: SQUARE_1:108

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

proof end;

theorem :: SQUARE_1:109

for x, y being complex number holds
( not x ^2 = y ^2 or x = y or x = - y )

proof end;

theorem :: SQUARE_1:110

for x being complex number holds
( not x ^2 = 1 or x = 1 or x = - 1 )

proof end;

theorem :: SQUARE_1:111

for x being real number st 0 <= x & x <= 1 holds
x ^2 <= x

proof end;

theorem :: SQUARE_1:112

for x being real number st (x ^2) - 1 <= 0 holds
( - 1 <= x & x <= 1 )

proof end;

theorem :: SQUARE_1:113

canceled;

begin

theorem Th114: :: SQUARE_1:114

for a, x being real number st a <= 0 & x < a holds
x ^2 > a ^2

proof end;

theorem :: SQUARE_1:115

for a being real number st - 1 >= a holds
- a <= a ^2

proof end;

theorem :: SQUARE_1:116

for a being real number st - 1 > a holds
- a < a ^2

proof end;

theorem :: SQUARE_1:117

for b, a being real number st b ^2 <= a ^2 & a >= 0 holds
( - a <= b & b <= a )

proof end;

theorem :: SQUARE_1:118

for b, a being real number st b ^2 < a ^2 & a >= 0 holds
( - a < b & b < a )

proof end;

theorem Th119: :: SQUARE_1:119

for a, b being real number st - a <= b & b <= a holds
b ^2 <= a ^2

proof end;

theorem :: SQUARE_1:120

for a, b being real number st - a < b & b < a holds
b ^2 < a ^2

proof end;

theorem :: SQUARE_1:121

for a being real number st a ^2 <= 1 holds
( - 1 <= a & a <= 1 )

proof end;

theorem :: SQUARE_1:122

for a being real number st a ^2 < 1 holds
( - 1 < a & a < 1 )

proof end;

theorem Th123: :: SQUARE_1:123

for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(a ^2) * (b ^2) <= 1

proof end;

theorem Th124: :: SQUARE_1:124

for a, b being real number st a >= 0 & b >= 0 holds
a * (sqrt b) = sqrt ((a ^2) * b)

proof end;

Lm6: for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(1 + (a ^2)) * (b ^2) <= 1 + (b ^2)

proof end;

theorem Th125: :: SQUARE_1:125

for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )

proof end;

theorem :: SQUARE_1:126

for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

proof end;

Lm7: for b, a being real number st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm8: for a, b being real number st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm9: for a, b being real number st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))

proof end;

theorem :: SQUARE_1:127

for a, b being real number st a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))

proof end;