:: 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-2016 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;
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;
:: registration
:: let x,y be real number;
:: cluster min(x,y) -> real;
:: coherence by XREAL_0:def 1;
:: cluster max(x,y) -> real;
:: coherence by XREAL_0:def 1;
:: end;
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 -> set 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;
registration
let a be Real;
cluster sqrt a -> real;
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;