Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

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

Back to top