The abstract of the Mizar article:

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

by

Andrzej Trybulec, and

Czeslaw Bylinski

Received November 16, 1989

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);