:: 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-2026 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;
definitions TARSKI;
equalities XCMPLX_0;
theorems AXIOMS, XREAL_0, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0;
begin
reserve a,b,c,x,y,z for Real;
scheme
RealContinuity { P,Q[object] } :
ex z st for x,y st P[x] & Q[y] holds x <= z & z <= y
provided
A1: for x,y st P[x] & Q[y] holds x <= y
proof
set Y = { z where z is Element of REAL: Q[z] };
set X = { z where z is Element of REAL : P[z] };
A2: X c= REAL
proof
let x be object;
assume x in X;
then ex z being Element of REAL st z = x & P[z];
hence thesis;
end;
Y c= REAL
proof
let x be object;
assume x in Y;
then ex z being Element of REAL st z = x & Q[z];
hence thesis;
end;
then reconsider X, Y as Subset of REAL by A2;
for x,y being Real st x in X & y in Y holds x <= y
proof
let x,y be Real;
assume that
A3: x in X and
A4: y in Y;
A5: ex z being Element of REAL st z = y & Q[z] by A4;
ex z being Element of REAL st z = x & P[z] by A3;
hence thesis by A1,A5;
end;
then consider z being Real such that
A6: for x,y being Real st x in X & y in Y holds x <= z & z <= y
by AXIOMS:1;
take z;
let x,y;
assume that
A7: P[x] and
A8: Q[y];
y is Element of REAL by XREAL_0:def 1;
then
A9: y in Y by A8;
x is Element of REAL by XREAL_0:def 1;
then x in X by A7;
hence thesis by A6,A9;
end;
theorem
min(x,y) + max(x,y) = x + y
proof
per cases;
suppose
A1: x <= y;
then min(x,y) = x by XXREAL_0:def 9;
hence thesis by A1,XXREAL_0:def 10;
end;
suppose
A2: x > y;
then min(x,y) = y by XXREAL_0:def 9;
hence thesis by A2,XXREAL_0:def 10;
end;
end;
theorem
for x,y being Real st 0 <= x & 0 <= y holds max(x,y) <= x + y
proof
let x,y be Real;
assume that
A1: 0 <= x and
A2: 0 <= y;
now
per cases by XXREAL_0:16;
suppose
A3: max(x,y) = x;
x + 0 <= x + y by A2,XREAL_1:7;
hence thesis by A3;
end;
suppose
A4: max(x,y) = y;
y + 0 <= y + x by A1,XREAL_1:7;
hence thesis by A4;
end;
end;
hence thesis;
end;
definition
let x be Complex;
func x^2 -> number equals
x * x;
correctness;
end;
registration
let x be Complex;
cluster x^2 -> complex;
coherence;
end;
registration
let x be Real;
cluster x^2 -> real;
coherence;
end;
definition
let x be Element of COMPLEX;
redefine func x^2 -> Element of COMPLEX; :: redefines ^2 (SQUARE_1, definition)
coherence by XCMPLX_0:def 2;
end;
theorem
for a being Complex holds a^2 = (-a)^2;
theorem
for a, b being Complex holds (a + b)^2 = a^2 + 2*a*b + b^2;
theorem
for a, b being Complex holds (a - b)^2 = a^2 - 2*a*b + b^2;
theorem
for a being Complex holds (a + 1)^2 = a^2 + 2*a + 1;
theorem
for a being Complex holds (a - 1)^2 = a^2 - 2*a + 1;
theorem
for a, b being Complex holds (a - b)*(a + b) = a^2 - b^2;
theorem
for a, b being Complex holds (a*b)^2 = a^2*b^2;
theorem Th10:
for a, b being Complex st a^2 - b^2 <> 0 holds
1/(a+b) = (a-b)/(a^2-b^2)
proof
let a, b be Complex;
assume a^2-b^2 <> 0;
then (a-b) <> 0;
hence 1/(a+b) = (1*(a-b))/((a+b)*(a-b)) by XCMPLX_1:91
.= (a-b)/(a^2-b^2);
end;
theorem Th11:
for a, b being Complex st a^2-b^2 <> 0 holds 1/(a-b) = (a+b)/(a^2-b^2)
proof
let a, b be Complex;
assume a^2-b^2 <> 0;
then (a+b)*(a-b) <> 0;
then (a+b) <> 0;
hence 1/(a-b) = (1*(a+b))/((a-b)*(a+b)) by XCMPLX_1:91
.= (a+b)/(a^2-b^2);
end;
theorem
0 <> a implies 0 < a^2 by XREAL_1:63;
theorem Th13:
0 < a & a < 1 implies a^2 < a
proof
assume that
A1: 0 < a and
A2: a < 1;
a*a < a*1 by A1,A2,XREAL_1:68;
hence thesis;
end;
theorem Th14:
1 < a implies a < a^2
proof
assume 1 < a;
then a*1 < a*a by XREAL_1:68;
hence thesis;
end;
Lm1: 0 < a implies ex x st 0 < x & x^2 < a
proof
assume
A1: 0 < a;
per cases;
suppose
A2: 1 <= a;
reconsider x = 2" as Real;
take x;
thus 0 < x;
thus thesis by A2,XXREAL_0:2;
end;
suppose
A3: a < 1;
take x = a;
thus 0 < x by A1;
thus thesis by A1,A3,Th13;
end;
end;
theorem Th15:
0 <= x & x <= y implies x^2 <= y^2
proof
assume that
A1: 0 <= x and
A2: x <= y;
A3: x*y <= y*y by A1,A2,XREAL_1:64;
x*x <= x*y by A1,A2,XREAL_1:64;
hence thesis by A3,XXREAL_0:2;
end;
theorem Th16:
0 <= x & x < y implies x^2 < y^2
proof
assume that
A1: 0 <= x and
A2: x < y;
A3: x*y < y*y by A1,A2,XREAL_1:68;
x*x <= x*y by A1,A2,XREAL_1:64;
hence thesis by A3,XXREAL_0:2;
end;
Lm2: 0 <= x & 0 <= y & x^2 = y^2 implies x = y
proof
assume that
A1: 0 <= x and
A2: 0 <= y;
assume
A3: x^2 = y ^2;
then
A4: y <= x by A1,Th16;
x <= y by A2,A3,Th16;
hence thesis by A4,XXREAL_0:1;
end;
definition
let a be Real;
assume
A1: 0 <= a;
func sqrt a -> Real means
:Def2:
0 <= it & it^2 = a;
existence
proof
defpred Y[Real] means 0 <= $1 & a <= $1^2;
defpred X[Real] means $1 <= 0 or $1^2 <= a;
a <= a + 1 by XREAL_1:29;
then
A2: 0 + a <= a^2 + a + (a + 1) by A1,XREAL_1:7;
A3: now
let x,y such that
A4: X[x] and
A5: Y[y];
per cases;
suppose
x <= 0;
hence x <= y by A5;
end;
suppose
not x <= 0;
then x^2 <= y^2 by A4,A5,XXREAL_0:2;
hence x <= y by A5,Th16;
end;
end;
consider z such that
A6: for x,y st X[x] & Y[y] holds x <= z & z <= y from RealContinuity(A3);
take z;
A7: (a + 1)^2 = a^2 + a + (a + 1);
hence 0 <= z by A1,A2,A6;
assume
A8: z^2 <> a;
now
per cases by A8,XXREAL_0:1;
suppose
A9: z <= 0;
then z = 0 by A1,A7,A2,A6;
then ex c st 0 < c & c^2 < a by A1,A8,Lm1;
hence contradiction by A1,A7,A2,A6,A9;
end;
suppose
A10: z^2 < a & not z <= 0;
set b = a - z^2;
A11: 0 < b by A10,XREAL_1:50;
then consider c such that
A12: 0 < c and
A13: c^2 < b/2 by Lm1;
set eps = min(c, b/(4*z));
A14: 0 < eps by A10,A11,A12,XXREAL_0:15;
then
A15: z < z + eps by XREAL_1:29;
eps*(2*z) <= b/(2*(2*z))*(2*z) by A10,XREAL_1:64,XXREAL_0:17;
then eps*(2*z) <= b/2/(2*z)*(2*z) by XCMPLX_1:78;
then
A16: 2*z*eps <= b/2 by A10,XCMPLX_1:87;
eps^2 <= c^2 by A14,Th15,XXREAL_0:17;
then eps^2 <= b/2 by A13,XXREAL_0:2;
then
A17: 2*z*eps + eps^2 <= b/2 + b/2 by A16,XREAL_1:7;
A18: (z + eps)^2 = z^2 + (2*z*eps + eps^2);
a = z^2 + b;
then (z + eps)^2 <= a by A18,A17,XREAL_1:6;
hence contradiction by A1,A7,A2,A6,A15;
end;
suppose
A19: a < z^2 & not z <= 0;
set b = z^2 - a;
set eps = min(b/(2*z),z);
A20: (z - eps)^2 = z^2 - (2*z*eps - eps^2);
0 < b by A19,XREAL_1:50;
then 0 < eps by A19,XXREAL_0:15;
then
A21: z - eps < z by XREAL_1:44;
0 <= eps^2 by XREAL_1:63;
then
A22: 2*z*eps - eps^2 <= 2*z*eps - 0 by XREAL_1:13;
eps*(2*z) <= b/(2*z)*(2*z) by A19,XREAL_1:64,XXREAL_0:17;
then 2*z*eps <= b by A19,XCMPLX_1:87;
then
A23: 2*z*eps - eps^2 <= b by A22,XXREAL_0:2;
A24: 0 <= z - eps by XREAL_1:48,XXREAL_0:17;
a = z^2 - b;
then a <= (z - eps)^2 by A20,A23,XREAL_1:13;
hence contradiction by A6,A24,A21;
end;
end;
hence contradiction;
end;
uniqueness by Lm2;
end;
theorem Th17:
sqrt 0 = 0
proof
sqrt 0^2 = 0 by Def2;
hence thesis;
end;
theorem Th18:
sqrt 1 = 1
proof
sqrt 1^2 = 1 by Def2;
hence thesis;
end;
registration
reduce sqrt 0 to 0;
reducibility by Th17;
reduce sqrt 1 to 1;
reducibility by Th18;
end;
Lm3: 0 <= x & x < y implies sqrt x < sqrt y
proof
assume that
A1: 0 <= x and
A2: x < y;
A3: (sqrt y)^2 = y by A1,A2,Def2;
A4: (sqrt x)^2 = x by A1,Def2;
0 <= sqrt y by A1,A2,Def2;
hence thesis by A2,A4,A3,Th15;
end;
theorem
1 < sqrt 2 by Lm3,Th18;
Lm4: 2^2 = 2*2;
theorem Th20:
sqrt 4 = 2 by Def2,Lm4;
theorem
sqrt 2 < 2 by Lm3,Th20;
theorem
0 <= a implies sqrt a^2 = a by Def2;
theorem
a <= 0 implies sqrt a^2 = -a
proof
A1: a^2 = (-a)^2;
assume a <= 0;
hence thesis by A1,Def2;
end;
theorem Th24:
0 <= a & sqrt a = 0 implies a = 0
proof
0 <= a & sqrt a = 0 implies a = 0^2 by Def2;
hence thesis;
end;
theorem Th25:
0 < a implies 0 < sqrt a
proof
assume
A1: 0 < a;
then sqrt a <> 0^2 by Def2;
hence thesis by A1,Def2;
end;
theorem Th26:
0 <= x & x <= y implies sqrt x <= sqrt y
proof
per cases;
suppose
x = y;
hence thesis;
end;
suppose
A1: x <> y;
assume
A2: 0 <= x;
assume x <= y;
then x < y by A1,XXREAL_0:1;
hence thesis by A2,Lm3;
end;
end;
theorem
0 <= x & x < y implies sqrt x < sqrt y by Lm3;
theorem Th28:
0 <= x & 0 <= y & sqrt x = sqrt y implies x = y
proof
assume that
A1: 0 <= x and
A2: 0 <= y and
A3: sqrt x = sqrt y;
assume x <> y;
then x < y or y < x by XXREAL_0:1;
hence contradiction by A1,A2,A3,Lm3;
end;
theorem Th29:
0 <= a & 0 <= b implies sqrt (a*b) = sqrt a * sqrt b
proof
assume that
A1: 0 <= a and
A2: 0 <= b;
A3: 0 <= sqrt a by A1,Def2;
A4: 0 <= sqrt b by A2,Def2;
(sqrt(a*b))^2 = a*b by A1,A2,Def2
.= (sqrt a)^2*b by A1,Def2
.= (sqrt a)^2*(sqrt b)^2 by A2,Def2
.= (sqrt a*sqrt b)^2;
hence sqrt(a*b) = sqrt(sqrt a*sqrt b)^2 by A1,A2,Def2
.= sqrt a*sqrt b by A3,A4,Def2;
end;
theorem Th30:
0 <= a & 0 <= b implies sqrt (a/b) = sqrt a/sqrt b
proof
assume that
A1: 0 <= a and
A2: 0 <= b;
A3: (sqrt b)^2 = b by A2,Def2;
(sqrt a)^2 = a by A1,Def2;
then
A4: (sqrt a/sqrt b)^2 = a/b by A3,XCMPLX_1:76;
A5: 0 <= sqrt b by A2,Def2;
0 <= sqrt a by A1,Def2;
hence thesis by A5,A4,Def2;
end;
theorem
for a,b being Real st 0 <= a & 0 <= b holds
sqrt(a + b) = 0 iff a = 0 & b = 0 by Th24;
theorem
0 < a implies sqrt (1/a) = 1/sqrt a by Th18,Th30;
theorem
0 < a implies sqrt a/a = 1/sqrt a
proof
assume
A1: 0 < a;
then sqrt a <> 0^2 by Def2;
hence sqrt a/a = (sqrt a)^2/(a*sqrt a) by XCMPLX_1:91
.= (1*a)/(sqrt a*a) by A1,Def2
.= 1/sqrt a by A1,XCMPLX_1:91;
end;
theorem
0 < a implies a / sqrt a = sqrt a
proof
assume
A1: 0 < a;
then sqrt a <> 0^2 by Def2;
hence a /sqrt a = (a*sqrt a) /(sqrt a)^2 by XCMPLX_1:91
.= (sqrt a*a) /(1*a) by A1,Def2
.= sqrt a/1 by A1,XCMPLX_1:91
.= sqrt a;
end;
theorem
0 <= a & 0 <= b implies (sqrt a - sqrt b)*(sqrt a + sqrt b) = a - b
proof
assume that
A1: 0 <= a and
A2: 0 <= b;
thus (sqrt a - sqrt b)*(sqrt a + sqrt b) = (sqrt a)^2 - (sqrt b)^2
.= a - (sqrt b)^2 by A1,Def2
.= a - b by A2,Def2;
end;
Lm5: 0 <= a & 0 <= b & a <> b implies (sqrt a)^2-(sqrt b)^2 <> 0
proof
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: a <> b;
A4: 0 <= sqrt a by A1,Def2;
A5: 0 <= sqrt b by A2,Def2;
sqrt a <> sqrt b by A1,A2,A3,Th28;
hence thesis by A4,A5,Lm2;
end;
theorem
0 <= a & 0 <= b & a <>b implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/ (a-b)
proof
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: a <>b;
thus 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/((sqrt a)^2-(sqrt b)^2) by A1,A2
,A3,Lm5,Th10
.= (sqrt a - sqrt b)/(a-(sqrt b)^2) by A1,Def2
.= (sqrt a - sqrt b)/(a-b) by A2,Def2;
end;
theorem
0 <= b & b < a implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b)
proof
assume that
A1: 0 <= b and
A2: b < a;
thus 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/((sqrt a)^2-(sqrt b)^2) by A1,A2
,Lm5,Th10
.= (sqrt a - sqrt b)/(a-(sqrt b)^2) by A1,A2,Def2
.= (sqrt a - sqrt b)/(a-b) by A1,Def2;
end;
theorem
0 <= a & 0 <= b implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b)
proof
assume that
A1: 0 <= a and
A2: 0 <= b;
per cases;
suppose
a <> b;
hence 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/((sqrt a)^2-(sqrt b)^2) by A1
,A2,Lm5,Th11
.= (sqrt a + sqrt b)/(a-(sqrt b)^2) by A1,Def2
.= (sqrt a + sqrt b)/(a-b) by A2,Def2;
end;
suppose
A3: a = b;
then 1/(sqrt a-sqrt b) = 0;
hence thesis by A3;
end;
end;
theorem
0 <= b & b < a implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b)
proof
assume that
A1: 0 <= b and
A2: b < a;
thus 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/((sqrt a)^2-(sqrt b)^2) by A1,A2
,Lm5,Th11
.= (sqrt a + sqrt b)/(a-(sqrt b)^2) by A1,A2,Def2
.= (sqrt a + sqrt b)/(a-b) by A1,Def2;
end;
theorem
for x,y being Complex st x^2=y^2 holds x=y or x=-y
proof
let x,y be Complex;
assume x^2=y^2;
then (x-y)*(x+y)=0;
then x-y=0 or x+y=0;
hence thesis;
end;
theorem
for x being Complex st x^2=1 holds x=1 or x=-1
proof
let x be Complex;
assume x^2=1;
then (x-1)*(x+1)=0;
then x-1=0 or x+1=0;
hence thesis;
end;
theorem
0<=x & x<=1 implies x^2<=x
proof
assume that
A1: 0<=x and
A2: x<=1;
per cases by A1;
suppose
0=x;
hence thesis;
end;
suppose
A3: 0<x;
per cases by A2,XXREAL_0:1;
suppose
x=1;
hence thesis;
end;
suppose
x<1;
hence thesis by A3,Th13;
end;
end;
end;
theorem
x^2-1<=0 implies -1<=x & x<=1
proof
assume x^2-1<=0;
then (x-1)*(x+1)<=0;
hence thesis by XREAL_1:93;
end;
begin :: Addenda
:: from JGRAPH_5, 2006.08.13, A.T.
theorem Th44:
a <= 0 & x < a implies x^2 > a^2
proof
assume that
A1: a<=0 and
A2: x<a;
-x>-a by A2,XREAL_1:24;
then (-x)^2>(-a)^2 by A1,Th16;
hence thesis;
end;
:: from JGRAPH_2, 2006.12.29, AK
theorem
-1 >= a implies -a <= a^2
proof
assume -1 >= a;
then --1<=-a by XREAL_1:24;
then -a<= (-a)^2 by XREAL_1:151;
hence thesis;
end;
theorem
-1 > a implies -a < a^2
proof
assume -1 > a;
then --1< -a by XREAL_1:24;
then -a< (-a)^2 by Th14;
hence thesis;
end;
theorem
b^2 <= a^2 & a >= 0 implies -a <= b & b <= a
proof
assume that
A1: b^2<= a^2 and
A2: a>=0;
now
assume
A3: -a>b or b>a;
now
per cases by A3;
case
-a>b;
then --a<-b by XREAL_1:24;
then a^2<(-b)^2 by A2,Th16;
hence contradiction by A1;
end;
case
b>a;
hence contradiction by A1,A2,Th16;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem
b^2 < a^2 & a >= 0 implies -a < b & b < a
proof
assume that
A1: b^2< a^2 and
A2: a>=0;
now
assume
A3: -a>=b or b>=a;
now
per cases by A3;
case
-a>=b;
then --a<= -b by XREAL_1:24;
then a^2<=(-b)^2 by A2,Th15;
hence contradiction by A1;
end;
case
b>=a;
hence contradiction by A1,A2,Th15;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th49:
-a <= b & b <= a implies b^2 <= a^2
proof
assume that
A1: -a<=b and
A2: b<=a;
per cases;
suppose
b>=0;
hence thesis by A2,Th15;
end;
suppose
A3: b<0;
--a>=-b by A1,XREAL_1:24;
then (-b)^2<= a^2 by A3,Th15;
hence thesis;
end;
end;
theorem
-a < b & b < a implies b^2 < a^2
proof
assume that
A1: -a<b and
A2: b<a;
per cases;
suppose
b>=0;
hence thesis by A2,Th16;
end;
suppose
A3: b<0;
--a>-b by A1,XREAL_1:24;
then (-b)^2< a^2 by A3,Th16;
hence thesis;
end;
end;
:: from JGRAPH_4, 2006.12.29, AK
theorem
a^2 <= 1 implies -1 <= a & a <= 1
proof
assume a^2<=1;
then a^2-1^2<=1^2-1^2 by XREAL_1:9;
then (a-1)*(a+1)<=0;
hence thesis by XREAL_1:93;
end;
theorem
a^2 < 1 implies -1 < a & a < 1
proof
assume a^2<1;
then a^2-1^2<1^2-1^2 by XREAL_1:9;
then (a-1)*(a+1)<0;
hence thesis by XREAL_1:94;
end;
:: from JGRAPH_6, 2006.12.29, AK
theorem Th53:
-1 <= a & a <= 1 & -1 <= b & b <= 1 implies a^2*b^2 <= 1
proof
assume that
A1: -1<=a and
A2: a<=1 and
A3: -1<=b and
A4: b<=1;
A5: 0<=b^2 by XREAL_1:63;
a^2<=1^2 by A1,A2,Th49;
then
A6: a^2*b^2 <= 1*b^2 by A5,XREAL_1:64;
b^2<=1^2 by A3,A4,Th49;
hence thesis by A6,XXREAL_0:2;
end;
theorem Th54:
a >= 0 & b >= 0 implies a*sqrt(b) = sqrt(a^2*b)
proof
assume that
A1: a>=0 and
A2: b>=0;
sqrt(a^2)=a by A1,Def2;
hence thesis by A1,A2,Th29;
end;
Lm6: -1<=a & a<=1 & -1<=b & b<=1 implies (1+a^2)*b^2<=1+b^2
proof
assume that
A1: -1<=a and
A2: a<=1 and
A3: -1<=b and
A4: b<=1;
a^2*b^2<=1 by A1,A2,A3,A4,Th53;
then 1*b^2+a^2*b^2<=1+b^2 by XREAL_1:7;
hence thesis;
end;
theorem Th55:
-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)
proof
assume that
A1: -1<=a and
A2: a<=1 and
A3: -1<=b and
A4: b<=1;
A5: a^2>=0 by XREAL_1:63;
then
A6: 1+a^2>=1+0 by XREAL_1:7;
b^2>=0 by XREAL_1:63;
then
A7: sqrt(1+b^2)>=0 by Def2;
A8: sqrt(1+a^2)>=0 by A5,Def2;
A9: now
per cases;
suppose
b>=0;
hence (-b)*sqrt(1+a^2)<=sqrt(1+b^2) by A8,A7;
end;
suppose
A10: b<0;
A11: (-b)^2>=0 by XREAL_1:63;
(-b)*sqrt(1+a^2)=sqrt((-b)^2*(1+a^2)) by A5,A10,Th54;
hence (-b)*sqrt(1+a^2)<=sqrt(1+b^2) by A1,A2,A3,A4,A6,A11,Lm6,Th26;
end;
end;
then -((-b)*sqrt(1+a^2)) >= - sqrt(1+b^2) by XREAL_1:24;
hence thesis by A9;
end;
theorem
-1 <= a & a <= 1 & -1 <= b & b <= 1 implies b*sqrt(1+a^2) <= sqrt(1+b^2)
proof
assume that
A1: -1<=a and
A2: a<=1 and
A3: -1<=b and
A4: b<=1;
A5: -1<=-b by A4,XREAL_1:24;
--1>=-b by A3,XREAL_1:24;
then (--b)*sqrt(1+a^2)<=sqrt(1+(-b)^2) by A1,A2,A5,Th55;
hence thesis;
end;
Lm7: b<=0 & a<=b implies a*sqrt(1+b^2)<= b*sqrt(1+a^2)
proof
assume that
A1: b<=0 and
A2: a<=b;
A3: (-a)*sqrt(1+b^2)=sqrt((-a)^2*(1+b^2)) by A1,A2,Th54;
a<b or a=b by A2,XXREAL_0:1;
then b^2<a^2 or a=b by A1,Th44;
then
A4: b^2*1+b^2*a^2<=a^2*1+a^2*b^2 by XREAL_1:7;
A5: (b)^2>=0 by XREAL_1:63;
A6: a^2>=0 by XREAL_1:63;
then (-b)*sqrt(1+a^2)=sqrt((-b)^2*(1+a^2)) by A1,Th54;
then -(a*sqrt(1+b^2))>= -(b*sqrt(1+a^2)) by A6,A3,A4,A5,Th26;
hence thesis by XREAL_1:24;
end;
Lm8: for a,b being Real st a<=0 & a<=b holds a*sqrt(1+b^2)<= b*sqrt(1+a
^2)
proof
let a,b be Real;
assume that
A1: a<=0 and
A2: a<=b;
now
per cases;
case
b<=0;
hence thesis by A2,Lm7;
end;
case
A3: b>0;
(b)^2 >=0 by XREAL_1:63;
then sqrt(1+(b)^2)>0 by Th25;
then
A4: a*sqrt(1+b^2)<=0 by A1;
(a)^2 >=0 by XREAL_1:63;
then sqrt(1+(a)^2)>0 by Th25;
hence thesis by A3,A4;
end;
end;
hence thesis;
end;
Lm9: for a,b being Real st a>=0 & a>=b holds a*sqrt(1+b^2)>= b*sqrt(1+a
^2)
proof
let a,b be Real;
assume that
A1: a>=0 and
A2: a>=b;
-a <= -b by A2,XREAL_1:24;
then (-a)*sqrt(1+(-b)^2)<= (-b)*sqrt(1+(-a)^2) by A1,Lm8;
then -(a*sqrt(1+(b)^2))<= -(b*sqrt(1+(a)^2));
hence thesis by XREAL_1:24;
end;
theorem
a >= b implies a*sqrt(1+b^2) >= b*sqrt(1+a^2)
proof
assume
A1: a>=b;
per cases;
suppose
a>=0;
hence thesis by A1,Lm9;
end;
suppose
a<0;
hence thesis by A1,Lm7;
end;
end;
theorem
a >= 0 implies sqrt(a+b^2) >= b
proof
assume
A1: a >= 0;
per cases;
suppose b < 0;
hence thesis by A1,Def2;
end;
suppose
A2: b >= 0;
A3: b^2 >= 0 by XREAL_1:63;
a+b^2 >= 0+b^2 by A1,XREAL_1:6;
then sqrt(a+b^2) >= sqrt(b^2) by A3,Th26;
hence sqrt(a+b^2) >= b by A2,Def2;
end;
end;
:: from TOPREAL6, 201.07.31, A.T.
theorem
0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b
proof
assume that
A1: 0 <= a and
A2: 0 <= b;
A3: 0 <= sqrt a by A1,Def2;
0 <= sqrt(a*b) by A1,A2,Def2;
then 0 <= sqrt a*sqrt b by A1,A2,Th29;
then 0 <= 2*(sqrt a*sqrt b);
then a + 0 <= a + 2*sqrt a*sqrt b by XREAL_1:6;
then
A4: a + b <= a + 2*sqrt a*sqrt b + b by XREAL_1:6;
A5: 0 <= sqrt b by A2,Def2;
sqrt(a + 2*sqrt a*sqrt b + b) = sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + b)
by A1,Def2
.= sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + (sqrt b)^2) by A2,Def2
.= sqrt((sqrt a + sqrt b)^2)
.= sqrt a + sqrt b by A3,A5,Def2;
hence thesis by A1,A2,A4,Th26;
end;