Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Some Properties of Real Numbers Operations: min, max, square, and square root

by
Andrzej Trybulec, and
Czeslaw Bylinski

MML identifier: SQUARE_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, ARYTM_3, RELAT_1, ARYTM_1, ABSVALUE, SQUARE_1;
notation TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, ABSVALUE;
constructors REAL_1, ABSVALUE, XCMPLX_0, XREAL_0, XBOOLE_0;
clusters XREAL_0, REAL_1, NUMBERS, ARYTM_3, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve a,b,c,x,y,z for real number;

canceled;

theorem :: SQUARE_1:2
1 < x implies 1/x < 1;

canceled 8;

theorem :: SQUARE_1:11
x < y implies 0 < y - x;

theorem :: SQUARE_1:12
x <= y implies 0 <= y - x;

canceled 6;

theorem :: SQUARE_1:19
0 <= x & 0 <= y implies 0 <= x*y;

theorem :: SQUARE_1:20
x <= 0 & y <= 0 implies 0 <= x*y;

theorem :: SQUARE_1:21
0 < x & 0 < y implies 0 < x*y;

theorem :: SQUARE_1:22
x < 0 & y < 0 implies 0 < x*y;

theorem :: SQUARE_1:23
0 <= x & y <= 0 implies x*y <= 0;

theorem :: SQUARE_1:24
0 < x & y < 0 implies x*y < 0;

theorem :: SQUARE_1:25
0 <= x*y implies 0 <= x & 0 <= y or x <= 0 & y <= 0;

theorem :: SQUARE_1:26
0 < x*y implies 0 < x & 0 < y or x < 0 & y < 0;

theorem :: SQUARE_1:27
0 <= a & 0 <= b implies 0 <= a/b;

canceled;

theorem :: SQUARE_1:29
0 < x implies y - x < y;

scheme RealContinuity { P[set], Q[set] } :
ex z st
for x,y st P[x] & Q[y] holds x <= z & z <= y
provided
for x,y st P[x] & Q[y] holds x <= y;

definition let x,y;
func min(x,y) -> real number equals
:: SQUARE_1:def 1
x if x <= y otherwise y;
commutativity;
idempotence;
func max(x,y) -> real number equals
:: SQUARE_1:def 2
x if y <= x otherwise y;
commutativity;
idempotence;
end;

definition let x,y be Element of REAL;
redefine func min(x,y) -> Element of REAL;
redefine func max(x,y) -> Element of REAL;
end;

canceled 4;

theorem :: SQUARE_1:34
min(x,y) = (x + y - abs(x - y)) / 2;

theorem :: SQUARE_1:35
min(x,y) <= x;

canceled 2;

theorem :: SQUARE_1:38
min(x,y) = x or min(x,y) = y;

theorem :: SQUARE_1:39
x <= y & x <= z iff x <= min(y,z);

theorem :: SQUARE_1:40
min(x,min(y,z)) = min(min(x,y),z);

canceled 4;

theorem :: SQUARE_1:45
max(x,y) = (x + y + abs(x-y)) / 2;

theorem :: SQUARE_1:46
x <= max(x,y);

canceled 2;

theorem :: SQUARE_1:49
max(x,y) = x or max(x,y) = y;

theorem :: SQUARE_1:50
y <= x & z <= x iff max(y,z) <= x;

theorem :: SQUARE_1:51
max(x,max(y,z)) = max(max(x,y),z);

canceled;

theorem :: SQUARE_1:53
min(x,y) + max(x,y) = x + y;

theorem :: SQUARE_1:54
max(x,min(x,y)) = x;

theorem :: SQUARE_1:55
min(x,max(x,y)) = x;

theorem :: SQUARE_1:56
min(x,max(y,z)) = max(min(x,y),min(x,z));

theorem :: SQUARE_1:57
max(x,min(y,z)) = min(max(x,y),max(x,z));

definition let x;
func x^2 equals
:: SQUARE_1:def 3
x * x;
end;

definition let x;
cluster x^2 -> real;
end;

definition let x be Element of REAL;
redefine func x^2 -> Element of REAL;
end;

canceled;

theorem :: SQUARE_1:59
1^2 = 1;

theorem :: SQUARE_1:60
0^2 = 0;

theorem :: SQUARE_1:61
a^2 = (-a)^2;

theorem :: SQUARE_1:62
(abs(a))^2 = a^2;

theorem :: SQUARE_1:63
(a + b)^2 = a^2 + 2*a*b + b^2;

theorem :: SQUARE_1:64
(a - b)^2 = a^2 - 2*a*b + b^2;

theorem :: SQUARE_1:65
(a + 1)^2 = a^2 + 2*a + 1;

theorem :: SQUARE_1:66
(a - 1)^2 = a^2 - 2*a + 1;

theorem :: SQUARE_1:67
(a - b)*(a + b) = a^2 - b^2 & (a + b)*(a - b) = a^2 - b^2;

theorem :: SQUARE_1:68
(a*b)^2 = a^2*b^2;

theorem :: SQUARE_1:69
(a/b)^2 = a^2/b^2;

theorem :: SQUARE_1:70
a^2-b^2 <> 0 implies 1/(a+b) = (a-b)/(a^2-b^2);

theorem :: SQUARE_1:71
a^2-b^2 <> 0 implies 1/(a-b) = (a+b)/(a^2-b^2);

theorem :: SQUARE_1:72
0 <= a^2;

theorem :: SQUARE_1:73
a^2 = 0 implies a = 0;

theorem :: SQUARE_1:74
0 <> a implies 0 < a^2;

theorem :: SQUARE_1:75
0 < a & a < 1 implies a^2 < a;

theorem :: SQUARE_1:76
1 < a implies a < a^2;

theorem :: SQUARE_1:77
0 <= x & x <= y implies x^2 <= y^2;

theorem :: SQUARE_1:78
0 <= x & x < y implies x^2 < y^2;

definition let a;
assume  0 <= a;
func sqrt a -> real number means
:: SQUARE_1:def 4
0 <= it & it^2 = a;
end;

definition let a be Element of REAL;
redefine func sqrt a -> Element of REAL;
end;

canceled 3;

theorem :: SQUARE_1:82
sqrt 0 = 0;

theorem :: SQUARE_1:83
sqrt 1 = 1;

theorem :: SQUARE_1:84
1 < sqrt 2;

theorem :: SQUARE_1:85
sqrt 4 = 2;

theorem :: SQUARE_1:86
sqrt 2 < 2;

canceled 2;

theorem :: SQUARE_1:89
0 <= a implies sqrt a^2 = a;

theorem :: SQUARE_1:90
a <= 0 implies sqrt a^2 = -a;

theorem :: SQUARE_1:91
sqrt a^2 = abs(a);

theorem :: SQUARE_1:92
0 <= a & sqrt a = 0 implies a = 0;

theorem :: SQUARE_1:93
0 < a implies 0 < sqrt a;

theorem :: SQUARE_1:94
0 <= x & x <= y implies sqrt x <= sqrt y;

theorem :: SQUARE_1:95
0 <= x & x < y implies sqrt x < sqrt y;

theorem :: SQUARE_1:96
0 <= x & 0 <= y & sqrt x = sqrt y implies x = y;

theorem :: SQUARE_1:97
0 <= a & 0 <= b implies sqrt (a*b) = sqrt a * sqrt b;

theorem :: SQUARE_1:98
0 <= a*b implies sqrt (a*b) = sqrt abs(a)*sqrt abs(b);

theorem :: SQUARE_1:99
0 <= a & 0 <= b implies sqrt (a/b) = sqrt a/sqrt b;

theorem :: SQUARE_1:100
0 < a/b implies sqrt (a/b) = sqrt abs(a) / sqrt abs(b);

theorem :: SQUARE_1:101
0 < a implies sqrt (1/a) = 1/sqrt a;

theorem :: SQUARE_1:102
0 < a implies sqrt a/a = 1/sqrt a;

theorem :: SQUARE_1:103
0 < a implies a /sqrt a = sqrt a;

theorem :: SQUARE_1:104
0 <= a & 0 <= b implies (sqrt a - sqrt b)*(sqrt a + sqrt b) = a - b;

theorem :: SQUARE_1:105
0 <= a & 0 <= b & a <>b implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b
);

theorem :: SQUARE_1:106
0 <= b & b < a implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b);

theorem :: SQUARE_1:107
0 <= a & 0 <= b & a <> b implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-
b
);

theorem :: SQUARE_1:108
0 <= b & b < a implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b);
```