:: 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-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XREAL_0, XXREAL_0, SUBSET_1, TARSKI, ARYTM_3, XCMPLX_0, RELAT_1, ARYTM_1, CARD_1, SQUARE_1, REAL_1, ORDINAL1; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0; constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0; registrations NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve a,b,c,x,y,z for Real; scheme :: SQUARE_1:sch 1 RealContinuity { P,Q[object] } : 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; theorem :: SQUARE_1:1 min(x,y) + max(x,y) = x + y; theorem :: SQUARE_1:2 for x,y being Real st 0 <= x & 0 <= y holds max(x,y) <= x + y; definition let x be Complex; func x^2 -> number equals :: SQUARE_1:def 1 x * x; end; registration let x be Complex; cluster x^2 -> complex; end; registration let x be Real; cluster x^2 -> real; end; definition let x be Element of COMPLEX; redefine func x^2 -> Element of COMPLEX; end; theorem :: SQUARE_1:3 for a being Complex holds a^2 = (-a)^2; theorem :: SQUARE_1:4 for a, b being Complex holds (a + b)^2 = a^2 + 2*a*b + b^2; theorem :: SQUARE_1:5 for a, b being Complex holds (a - b)^2 = a^2 - 2*a*b + b^2; theorem :: SQUARE_1:6 for a being Complex holds (a + 1)^2 = a^2 + 2*a + 1; theorem :: SQUARE_1:7 for a being Complex holds (a - 1)^2 = a^2 - 2*a + 1; theorem :: SQUARE_1:8 for a, b being Complex holds (a - b)*(a + b) = a^2 - b^2; theorem :: SQUARE_1:9 for a, b being Complex holds (a*b)^2 = a^2*b^2; theorem :: SQUARE_1:10 for a, b being Complex st a^2 - b^2 <> 0 holds 1/(a+b) = (a-b)/(a^2-b^2); theorem :: SQUARE_1:11 for a, b being Complex st a^2-b^2 <> 0 holds 1/(a-b) = (a+b)/(a^2-b^2); theorem :: SQUARE_1:12 0 <> a implies 0 < a^2; theorem :: SQUARE_1:13 0 < a & a < 1 implies a^2 < a; theorem :: SQUARE_1:14 1 < a implies a < a^2; theorem :: SQUARE_1:15 0 <= x & x <= y implies x^2 <= y^2; theorem :: SQUARE_1:16 0 <= x & x < y implies x^2 < y^2; definition let a be Real; assume 0 <= a; func sqrt a -> Real means :: SQUARE_1:def 2 0 <= it & it^2 = a; end; theorem :: SQUARE_1:17 sqrt 0 = 0; theorem :: SQUARE_1:18 sqrt 1 = 1; theorem :: SQUARE_1:19 1 < sqrt 2; theorem :: SQUARE_1:20 sqrt 4 = 2; theorem :: SQUARE_1:21 sqrt 2 < 2; theorem :: SQUARE_1:22 0 <= a implies sqrt a^2 = a; theorem :: SQUARE_1:23 a <= 0 implies sqrt a^2 = -a; theorem :: SQUARE_1:24 0 <= a & sqrt a = 0 implies a = 0; theorem :: SQUARE_1:25 0 < a implies 0 < sqrt a; theorem :: SQUARE_1:26 0 <= x & x <= y implies sqrt x <= sqrt y; theorem :: SQUARE_1:27 0 <= x & x < y implies sqrt x < sqrt y; theorem :: SQUARE_1:28 0 <= x & 0 <= y & sqrt x = sqrt y implies x = y; theorem :: SQUARE_1:29 0 <= a & 0 <= b implies sqrt (a*b) = sqrt a * sqrt b; theorem :: SQUARE_1:30 0 <= a & 0 <= b implies sqrt (a/b) = sqrt a/sqrt b; theorem :: SQUARE_1:31 for a,b being Real st 0 <= a & 0 <= b holds sqrt(a + b) = 0 iff a = 0 & b = 0; theorem :: SQUARE_1:32 0 < a implies sqrt (1/a) = 1/sqrt a; theorem :: SQUARE_1:33 0 < a implies sqrt a/a = 1/sqrt a; theorem :: SQUARE_1:34 0 < a implies a / sqrt a = sqrt a; theorem :: SQUARE_1:35 0 <= a & 0 <= b implies (sqrt a - sqrt b)*(sqrt a + sqrt b) = a - b; theorem :: SQUARE_1:36 0 <= a & 0 <= b & a <>b implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/ (a-b); theorem :: SQUARE_1:37 0 <= b & b < a implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b); theorem :: SQUARE_1:38 0 <= a & 0 <= b implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b); theorem :: SQUARE_1:39 0 <= b & b < a implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b); theorem :: SQUARE_1:40 for x,y being Complex st x^2=y^2 holds x=y or x=-y; theorem :: SQUARE_1:41 for x being Complex st x^2=1 holds x=1 or x=-1; theorem :: SQUARE_1:42 0<=x & x<=1 implies x^2<=x; theorem :: SQUARE_1:43 x^2-1<=0 implies -1<=x & x<=1; begin :: Addenda :: from JGRAPH_5, 2006.08.13, A.T. theorem :: SQUARE_1:44 a <= 0 & x < a implies x^2 > a^2; :: from JGRAPH_2, 2006.12.29, AK theorem :: SQUARE_1:45 -1 >= a implies -a <= a^2; theorem :: SQUARE_1:46 -1 > a implies -a < a^2; theorem :: SQUARE_1:47 b^2 <= a^2 & a >= 0 implies -a <= b & b <= a; theorem :: SQUARE_1:48 b^2 < a^2 & a >= 0 implies -a < b & b < a; theorem :: SQUARE_1:49 -a <= b & b <= a implies b^2 <= a^2; theorem :: SQUARE_1:50 -a < b & b < a implies b^2 < a^2; :: from JGRAPH_4, 2006.12.29, AK theorem :: SQUARE_1:51 a^2 <= 1 implies -1 <= a & a <= 1; theorem :: SQUARE_1:52 a^2 < 1 implies -1 < a & a < 1; :: from JGRAPH_6, 2006.12.29, AK theorem :: SQUARE_1:53 -1 <= a & a <= 1 & -1 <= b & b <= 1 implies a^2*b^2 <= 1; theorem :: SQUARE_1:54 a >= 0 & b >= 0 implies a*sqrt(b) = sqrt(a^2*b); theorem :: SQUARE_1:55 -1 <= a & a <= 1 & -1 <= b & b <= 1 implies (-b)*sqrt(1+a^2) <= sqrt(1+b^2) & -sqrt(1+b^2) <= b*sqrt(1+a^2); theorem :: SQUARE_1:56 -1 <= a & a <= 1 & -1 <= b & b <= 1 implies b*sqrt(1+a^2) <= sqrt(1+b^2); theorem :: SQUARE_1:57 a >= b implies a*sqrt(1+b^2) >= b*sqrt(1+a^2); theorem :: SQUARE_1:58 a >= 0 implies sqrt(a+b^2) >= b; :: from TOPREAL6, 201.07.31, A.T. theorem :: SQUARE_1:59 0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b;