:: 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{ P1[ set ], P2[ set ] } :
ex z being real number st
for x, y being real number st P1[x] & P2[y] holds
( x <= z & z <= y )
provided
A1: for x, y being real number st P1[x] & P2[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 b1 being real number st
( 0 <= b1 & b1 ^2 = a )
proof end;
uniqueness
for b1, b2 being real number st 0 <= b1 & b1 ^2 = a & 0 <= b2 & b2 ^2 = a holds
b1 = b2
by Lm2;
end;

:: deftheorem Def4 defines sqrt SQUARE_1:def 4 :
for a being real number st 0 <= a holds
for b2 being real number holds
( b2 = sqrt a iff ( 0 <= b2 & b2 ^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;