:: SQUARE_1 semantic presentation

begin


scheme :: SQUARE_1:sch 1
RealContinuity{ P1[ set ], P2[ set ] } :
 ex z being real number st
for x, y being real number st P1[x] & P2[y] holds
( x <= z & z <= y )
provided
A1: for x, y being real number st P1[x] & P2[y] holds
x <= y
proof
set Y =  {  z where z is Element of REAL : P2[z]  }  ;
set X =  {  z where z is Element of REAL : P1[z]  }  ;
A2:  {  z where z is Element of REAL : P1[z]  }  c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  z where z is Element of REAL : P1[z]  }  or x in REAL )
assume  x in  {  z where z is Element of REAL : P1[z]  }  ; ::_thesis: x in REAL
then  ex z being Element of REAL st
( z = x & P1[z] ) ;
hence  x in REAL ; ::_thesis: verum
end;
  {  z where z is Element of REAL : P2[z]  }  c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  z where z is Element of REAL : P2[z]  }  or x in REAL )
assume  x in  {  z where z is Element of REAL : P2[z]  }  ; ::_thesis: x in REAL
then  ex z being Element of REAL st
( z = x & P2[z] ) ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider X =  {  z where z is Element of REAL : P1[z]  }  , Y =  {  z where z is Element of REAL : P2[z]  }  as Subset of REAL by A2;
 for x, y being real number st x in X & y in Y holds
x <= y
proof
let x, y be real number ; ::_thesis: ( x in X & y in Y implies x <= y )
assume that
A3: x in X and
A4: y in Y ; ::_thesis: x <= y
A5: ex z being Element of REAL st
( z = y & P2[z] ) by A4;
 ex z being Element of REAL st
( z = x & P1[z] ) by A3;
hence  x <= y by A1, A5; ::_thesis: verum
end;
then consider z being real number  such that
A6: for x, y being real number st x in X & y in Y holds
( x <= z & z <= y ) by AXIOMS:1;
take  z ; ::_thesis: for x, y being real number st P1[x] & P2[y] holds
( x <= z & z <= y )
let x, y be real number ; ::_thesis: ( P1[x] & P2[y] implies ( x <= z & z <= y ) )
assume that
A7: P1[x] and
A8: P2[y] ; ::_thesis: ( x <= z & z <= 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  ( x <= z & z <= y ) by A6, A9; ::_thesis: verum
end;

definition
let x, y be Element of REAL ;
:: original: min
redefine func min (x,y) ->  Element of REAL ;
coherence
 min (x,y) is Element of REAL by XREAL_0:def_1;
:: original: max
redefine func max (x,y) ->  Element of REAL ;
coherence
 max (x,y) is Element of REAL by XREAL_0:def_1;
end;

theorem :: SQUARE_1:1
for x, y being real number holds (min (x,y)) + (max (x,y)) = x + y
proof
let x, y be real number ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
percases ( x <= y or x > y ) ;
supposeA1: x <= y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
then  min (x,y) = x by XXREAL_0:def_9;
hence  (min (x,y)) + (max (x,y)) = x + y by A1, XXREAL_0:def_10; ::_thesis: verum
end;
supposeA2: x > y ; ::_thesis: (min (x,y)) + (max (x,y)) = x + y
then  min (x,y) = y by XXREAL_0:def_9;
hence  (min (x,y)) + (max (x,y)) = x + y by A2, XXREAL_0:def_10; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:2
for x, y being real number st 0 <= x & 0 <= y holds
max (x,y) <= x + y
proof
let x, y be real number ; ::_thesis: ( 0 <= x & 0 <= y implies max (x,y) <= x + y )
assume that
A1: 0 <= x and
A2: 0 <= y ; ::_thesis: max (x,y) <= x + y
now__::_thesis:_max_(x,y)_<=_x_+_y
percases ( max (x,y) = x or max (x,y) = y ) by XXREAL_0:16;
supposeA3: max (x,y) = x ; ::_thesis: max (x,y) <= x + y
 x + 0 <= x + y by A2, XREAL_1:7;
hence  max (x,y) <= x + y by A3; ::_thesis: verum
end;
supposeA4: max (x,y) = y ; ::_thesis: max (x,y) <= x + y
 y + 0 <= y + x by A1, XREAL_1:7;
hence  max (x,y) <= x + y by A4; ::_thesis: verum
end;
end;
end;
hence  max (x,y) <= x + y ; ::_thesis: verum
end;

definition
let x be complex number ;
funcx ^2  ->  set  equals :: SQUARE_1:def 1
x * x;
correctness
coherence
x * x is set ;
;
end;

:: deftheorem  defines ^2 SQUARE_1:def_1_:_
 for x being complex number holds x ^2 = x * x;

registration
let x be complex number ;
clusterx ^2  ->  complex ;
coherence
 x ^2 is complex ;
end;

registration
let x be real number ;
clusterx ^2  ->  real ;
coherence
 x ^2 is real ;
end;

definition
let x be Element of COMPLEX ;
:: original: ^2
redefine funcx ^2  ->  Element of COMPLEX ;
coherence
 x ^2 is Element of COMPLEX by XCMPLX_0:def_2;
end;

definition
let x be Element of REAL ;
:: original: ^2
redefine funcx ^2  ->  Element of REAL ;
coherence
 x ^2 is Element of REAL by XREAL_0:def_1;
end;

theorem :: SQUARE_1:3
for a being complex number holds a ^2 = (- a) ^2 ;

theorem :: SQUARE_1:4
for a, b being complex number holds (a + b) ^2 = ((a ^2) + ((2 * a) * b)) + (b ^2) ;

theorem :: SQUARE_1:5
for a, b being complex number holds (a - b) ^2 = ((a ^2) - ((2 * a) * b)) + (b ^2) ;

theorem :: SQUARE_1:6
for a being complex number holds (a + 1) ^2 = ((a ^2) + (2 * a)) + 1 ;

theorem :: SQUARE_1:7
for a being complex number holds (a - 1) ^2 = ((a ^2) - (2 * a)) + 1 ;

theorem :: SQUARE_1:8
for a, b being complex number holds (a - b) * (a + b) = (a ^2) - (b ^2) ;

theorem :: SQUARE_1:9
for a, b being complex number holds (a * b) ^2 = (a ^2) * (b ^2) ;

theorem Th10: :: SQUARE_1:10
for a, b being complex number st (a ^2) - (b ^2) <> 0 holds
1 / (a + b) = (a - b) / ((a ^2) - (b ^2))
proof
let a, b be complex number ; ::_thesis: ( (a ^2) - (b ^2) <> 0 implies 1 / (a + b) = (a - b) / ((a ^2) - (b ^2)) )
assume  (a ^2) - (b ^2) <> 0 ; ::_thesis: 1 / (a + b) = (a - b) / ((a ^2) - (b ^2))
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)) ;
::_thesis: verum
end;

theorem Th11: :: SQUARE_1:11
for a, b being complex number st (a ^2) - (b ^2) <> 0 holds
1 / (a - b) = (a + b) / ((a ^2) - (b ^2))
proof
let a, b be complex number ; ::_thesis: ( (a ^2) - (b ^2) <> 0 implies 1 / (a - b) = (a + b) / ((a ^2) - (b ^2)) )
assume  (a ^2) - (b ^2) <> 0 ; ::_thesis: 1 / (a - b) = (a + b) / ((a ^2) - (b ^2))
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)) ;
::_thesis: verum
end;

theorem :: SQUARE_1:12
for a being real number st 0 <> a holds
0 < a ^2 by XREAL_1:63;

theorem Th13: :: SQUARE_1:13
for a being real number st 0 < a & a < 1 holds
a ^2 < a
proof
let a be real number ; ::_thesis: ( 0 < a & a < 1 implies a ^2 < a )
assume that
A1: 0 < a and
A2: a < 1 ; ::_thesis: a ^2 < a
 a * a < a * 1 by A1, A2, XREAL_1:68;
hence  a ^2 < a ; ::_thesis: verum
end;

theorem Th14: :: SQUARE_1:14
for a being real number st 1 < a holds
a < a ^2
proof
let a be real number ; ::_thesis: ( 1 < a implies a < a ^2 )
assume  1 < a ; ::_thesis: a < a ^2
then  a * 1 < a * a by XREAL_1:68;
hence  a < a ^2 ; ::_thesis: verum
end;

Lm1:  for a being real number st 0 < a holds
ex x being real number st
( 0 < x & x ^2 < a )
proof
let a be real number ; ::_thesis: ( 0 < a implies ex x being real number st
( 0 < x & x ^2 < a ) )
assume A1: 0 < a ; ::_thesis: ex x being real number st
( 0 < x & x ^2 < a )
percases ( 1 <= a or a < 1 ) ;
supposeA2: 1 <= a ; ::_thesis: ex x being real number st
( 0 < x & x ^2 < a )
reconsider x = 2 " as real number ;
take  x ; ::_thesis: ( 0 < x & x ^2 < a )
thus  0 < x ; ::_thesis: x ^2 < a
thus  x ^2 < a by A2, XXREAL_0:2; ::_thesis: verum
end;
supposeA3: a < 1 ; ::_thesis: ex x being real number st
( 0 < x & x ^2 < a )
take x = a; ::_thesis: ( 0 < x & x ^2 < a )
thus  0 < x by A1; ::_thesis: x ^2 < a
thus  x ^2 < a by A1, A3, Th13; ::_thesis: verum
end;
end;
end;

theorem Th15: :: SQUARE_1:15
for x, y being real number st 0 <= x & x <= y holds
x ^2 <= y ^2
proof
let x, y be real number ; ::_thesis: ( 0 <= x & x <= y implies x ^2 <= y ^2 )
assume that
A1: 0 <= x and
A2: x <= y ; ::_thesis: x ^2 <= y ^2
A3: x * y <= y * y by A1, A2, XREAL_1:64;
 x * x <= x * y by A1, A2, XREAL_1:64;
hence  x ^2 <= y ^2 by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem Th16: :: SQUARE_1:16
for x, y being real number st 0 <= x & x < y holds
x ^2 < y ^2
proof
let x, y be real number ; ::_thesis: ( 0 <= x & x < y implies x ^2 < y ^2 )
assume that
A1: 0 <= x and
A2: x < y ; ::_thesis: x ^2 < y ^2
A3: x * y < y * y by A1, A2, XREAL_1:68;
 x * x <= x * y by A1, A2, XREAL_1:64;
hence  x ^2 < y ^2 by A3, XXREAL_0:2; ::_thesis: verum
end;

Lm2:  for x, y being real number st 0 <= x & 0 <= y & x ^2 = y ^2 holds
x = y
proof
let x, y be real number ; ::_thesis: ( 0 <= x & 0 <= y & x ^2 = y ^2 implies x = y )
assume that
A1: 0 <= x and
A2: 0 <= y ; ::_thesis: ( not x ^2 = y ^2 or x = y )
assume A3: x ^2 = y ^2 ; ::_thesis: x = y
then A4: y <= x by A1, Th16;
 x <= y by A2, A3, Th16;
hence  x = y by A4, XXREAL_0:1; ::_thesis: verum
end;

definition
let a be real number ;
assume A1: 0 <= a ;
func sqrt a ->  real number  means :Def2: :: SQUARE_1:def 2
( 0 <= it & it ^2 = a );
existence
 ex b1 being real number st
( 0 <= b1 & b1 ^2 = a )
proof
defpred S1[ real number ] means ( 0 <= $1 & a <= $1 ^2 );
defpred S2[ real number ] 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__::_thesis:_for_x,_y_being_real_number_st_S2[x]_&_S1[y]_holds_
x_<=_y
let x, y be real number ; ::_thesis: ( S2[x] & S1[y] implies b1 <= b2 )
assume that
A4: S2[x] and
A5: S1[y] ; ::_thesis: b1 <= b2
percases ( x <= 0 or not x <= 0 ) ;
suppose x <= 0 ; ::_thesis: b1 <= b2
hence  x <= y by A5; ::_thesis: verum
end;
suppose not x <= 0 ; ::_thesis: b1 <= b2
then  x ^2 <= y ^2 by A4, A5, XXREAL_0:2;
hence  x <= y by A5, Th16; ::_thesis: verum
end;
end;
end;
consider z being real number  such that
A6: for x, y being real number st S2[x] & S1[y] holds
( x <= z & z <= y ) from SQUARE_1:sch_1(A3);
take  z ; ::_thesis: ( 0 <= z & z ^2 = a )
A7: (a + 1) ^2 = ((a ^2) + a) + (a + 1) ;
hence  0 <= z by A1, A2, A6; ::_thesis: z ^2 = a
assume A8: z ^2 <> a ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( z <= 0 or ( z ^2 < a & not z <= 0 ) or ( a < z ^2 & not z <= 0 ) ) by A8, XXREAL_0:1;
supposeA9: z <= 0 ; ::_thesis: contradiction
then  z = 0 by A1, A7, A2, A6;
then  ex c being real number st
( 0 < c & c ^2 < a ) by A1, A8, Lm1;
hence  contradiction by A1, A7, A2, A6, A9; ::_thesis: verum
end;
supposeA10: ( z ^2 < a & not z <= 0 ) ; ::_thesis: contradiction
set b = a - (z ^2);
A11: 0 < a - (z ^2) by A10, XREAL_1:50;
then consider c being real number  such that
A12: 0 < c and
A13: c ^2 < (a - (z ^2)) / 2 by Lm1;
set eps = min (c,((a - (z ^2)) / (4 * z)));
A14: 0 < min (c,((a - (z ^2)) / (4 * z))) by A10, A11, A12, XXREAL_0:15;
then A15: z < z + (min (c,((a - (z ^2)) / (4 * z)))) by XREAL_1:29;
 (min (c,((a - (z ^2)) / (4 * z)))) * (2 * z) <= ((a - (z ^2)) / (2 * (2 * z))) * (2 * z) by A10, XREAL_1:64, XXREAL_0:17;
then  (min (c,((a - (z ^2)) / (4 * z)))) * (2 * z) <= (((a - (z ^2)) / 2) / (2 * z)) * (2 * z) by XCMPLX_1:78;
then A16: (2 * z) * (min (c,((a - (z ^2)) / (4 * z)))) <= (a - (z ^2)) / 2 by A10, XCMPLX_1:87;
 (min (c,((a - (z ^2)) / (4 * z)))) ^2 <= c ^2 by A14, Th15, XXREAL_0:17;
then  (min (c,((a - (z ^2)) / (4 * z)))) ^2 <= (a - (z ^2)) / 2 by A13, XXREAL_0:2;
then A17: ((2 * z) * (min (c,((a - (z ^2)) / (4 * z))))) + ((min (c,((a - (z ^2)) / (4 * z)))) ^2) <= ((a - (z ^2)) / 2) + ((a - (z ^2)) / 2) by A16, XREAL_1:7;
A18: (z + (min (c,((a - (z ^2)) / (4 * z))))) ^2 = (z ^2) + (((2 * z) * (min (c,((a - (z ^2)) / (4 * z))))) + ((min (c,((a - (z ^2)) / (4 * z)))) ^2)) ;
 a = (z ^2) + (a - (z ^2)) ;
then  (z + (min (c,((a - (z ^2)) / (4 * z))))) ^2 <= a by A18, A17, XREAL_1:6;
hence  contradiction by A1, A7, A2, A6, A15; ::_thesis: verum
end;
supposeA19: ( a < z ^2 & not z <= 0 ) ; ::_thesis: contradiction
set b = (z ^2) - a;
set eps = min ((((z ^2) - a) / (2 * z)),z);
A20: (z - (min ((((z ^2) - a) / (2 * z)),z))) ^2 = (z ^2) - (((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2)) ;
 0 < (z ^2) - a by A19, XREAL_1:50;
then  0 < min ((((z ^2) - a) / (2 * z)),z) by A19, XXREAL_0:15;
then A21: z - (min ((((z ^2) - a) / (2 * z)),z)) < z by XREAL_1:44;
 0 <= (min ((((z ^2) - a) / (2 * z)),z)) ^2 by XREAL_1:63;
then A22: ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2) <= ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - 0 by XREAL_1:13;
 (min ((((z ^2) - a) / (2 * z)),z)) * (2 * z) <= (((z ^2) - a) / (2 * z)) * (2 * z) by A19, XREAL_1:64, XXREAL_0:17;
then  (2 * z) * (min ((((z ^2) - a) / (2 * z)),z)) <= (z ^2) - a by A19, XCMPLX_1:87;
then A23: ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2) <= (z ^2) - a by A22, XXREAL_0:2;
A24: 0 <= z - (min ((((z ^2) - a) / (2 * z)),z)) by XREAL_1:48, XXREAL_0:17;
 a = (z ^2) - ((z ^2) - a) ;
then  a <= (z - (min ((((z ^2) - a) / (2 * z)),z))) ^2 by A20, A23, XREAL_1:13;
hence  contradiction by A6, A24, A21; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being real number st 0 <= b1 & b1 ^2 = a & 0 <= b2 & b2 ^2 = a holds
b1 = b2 by Lm2;
end;

:: deftheorem Def2 defines sqrt SQUARE_1:def_2_:_
 for a being real number st 0 <= a holds
for b2 being real number holds
( b2 = sqrt a iff ( 0 <= b2 & b2 ^2 = a ) );

definition
let a be Element of REAL ;
:: original: sqrt
redefine func sqrt a ->  Element of REAL ;
coherence
 sqrt a is Element of REAL by XREAL_0:def_1;
end;

theorem Th17: :: SQUARE_1:17
sqrt 0 = 0
proof
 sqrt (0 ^2) = 0 by Def2;
hence  sqrt 0 = 0 ; ::_thesis: verum
end;

theorem Th18: :: SQUARE_1:18
sqrt 1 = 1
proof
 sqrt (1 ^2) = 1 by Def2;
hence  sqrt 1 = 1 ; ::_thesis: verum
end;

Lm3:  for x, y being real number st 0 <= x & x < y holds
sqrt x < sqrt y
proof
let x, y be real number ; ::_thesis: ( 0 <= x & x < y implies sqrt x < sqrt y )
assume that
A1: 0 <= x and
A2: x < y ; ::_thesis: sqrt x < sqrt 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  sqrt x < sqrt y by A2, A4, A3, Th15; ::_thesis: verum
end;

theorem :: SQUARE_1:19
1 < sqrt 2 by Lm3, Th18;

Lm4:  2 ^2 = 2 * 2
;

theorem Th20: :: SQUARE_1:20
sqrt 4 = 2 by Def2, Lm4;

theorem :: SQUARE_1:21
sqrt 2 < 2 by Lm3, Th20;

theorem Th22: :: SQUARE_1:22
for a being real number st 0 <= a holds
sqrt (a ^2) = a by Def2;

theorem :: SQUARE_1:23
for a being real number st a <= 0 holds
sqrt (a ^2) = - a
proof
let a be real number ; ::_thesis: ( a <= 0 implies sqrt (a ^2) = - a )
A1: a ^2 = (- a) ^2 ;
assume  a <= 0 ; ::_thesis: sqrt (a ^2) = - a
hence  sqrt (a ^2) = - a by A1, Def2; ::_thesis: verum
end;

theorem Th24: :: SQUARE_1:24
for a being real number st 0 <= a & sqrt a = 0 holds
a = 0
proof
let a be real number ; ::_thesis: ( 0 <= a & sqrt a = 0 implies a = 0 )
 ( 0 <= a & sqrt a = 0 implies a = 0 ^2 ) by Def2;
hence  ( 0 <= a & sqrt a = 0 implies a = 0 ) ; ::_thesis: verum
end;

theorem Th25: :: SQUARE_1:25
for a being real number st 0 < a holds
0 < sqrt a
proof
let a be real number ; ::_thesis: ( 0 < a implies 0 < sqrt a )
assume A1: 0 < a ; ::_thesis: 0 < sqrt a
then  sqrt a <> 0 ^2 by Def2;
hence  0 < sqrt a by A1, Def2; ::_thesis: verum
end;

theorem Th26: :: SQUARE_1:26
for x, y being real number st 0 <= x & x <= y holds
sqrt x <= sqrt y
proof
let x, y be real number ; ::_thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )
hence  ( 0 <= x & x <= y implies sqrt x <= sqrt y ) ; ::_thesis: verum
end;
supposeA1: x <> y ; ::_thesis: ( 0 <= x & x <= y implies sqrt x <= sqrt y )
assume A2: 0 <= x ; ::_thesis: ( not x <= y or sqrt x <= sqrt y )
assume  x <= y ; ::_thesis: sqrt x <= sqrt y
then  x < y by A1, XXREAL_0:1;
hence  sqrt x <= sqrt y by A2, Lm3; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:27
for x, y being real number st 0 <= x & x < y holds
sqrt x < sqrt y by Lm3;

theorem Th28: :: SQUARE_1:28
for x, y being real number st 0 <= x & 0 <= y & sqrt x = sqrt y holds
x = y
proof
let x, y be real number ; ::_thesis: ( 0 <= x & 0 <= y & sqrt x = sqrt y implies x = y )
assume that
A1: 0 <= x and
A2: 0 <= y and
A3: sqrt x = sqrt y ; ::_thesis: x = y
assume  x <> y ; ::_thesis: contradiction
then  ( x < y or y < x ) by XXREAL_0:1;
hence  contradiction by A1, A2, A3, Lm3; ::_thesis: verum
end;

theorem Th29: :: SQUARE_1:29
for a, b being real number st 0 <= a & 0 <= b holds
sqrt (a * b) = (sqrt a) * (sqrt b)
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b implies sqrt (a * b) = (sqrt a) * (sqrt b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; ::_thesis: sqrt (a * b) = (sqrt a) * (sqrt 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 ;
::_thesis: verum
end;

theorem Th30: :: SQUARE_1:30
for a, b being real number st 0 <= a & 0 <= b holds
sqrt (a / b) = (sqrt a) / (sqrt b)
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b implies sqrt (a / b) = (sqrt a) / (sqrt b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; ::_thesis: sqrt (a / b) = (sqrt a) / (sqrt 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  sqrt (a / b) = (sqrt a) / (sqrt b) by A5, A4, Def2; ::_thesis: verum
end;

theorem :: SQUARE_1:31
for a, b being real number st 0 <= a & 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) ) by Th17, Th24;

theorem :: SQUARE_1:32
for a being real number st 0 < a holds
sqrt (1 / a) = 1 / (sqrt a) by Th18, Th30;

theorem :: SQUARE_1:33
for a being real number st 0 < a holds
(sqrt a) / a = 1 / (sqrt a)
proof
let a be real number ; ::_thesis: ( 0 < a implies (sqrt a) / a = 1 / (sqrt a) )
assume A1: 0 < a ; ::_thesis: (sqrt a) / a = 1 / (sqrt 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 ;
::_thesis: verum
end;

theorem :: SQUARE_1:34
for a being real number st 0 < a holds
a / (sqrt a) = sqrt a
proof
let a be real number ; ::_thesis: ( 0 < a implies a / (sqrt a) = sqrt a )
assume A1: 0 < a ; ::_thesis: a / (sqrt a) = sqrt 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 ;
::_thesis: verum
end;

theorem :: SQUARE_1:35
for a, b being real number st 0 <= a & 0 <= b holds
((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b implies ((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b )
assume that
A1: 0 <= a and
A2: 0 <= b ; ::_thesis: ((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - 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 ; ::_thesis: verum
end;

Lm5:  for a, b being real number st 0 <= a & 0 <= b & a <> b holds
((sqrt a) ^2) - ((sqrt b) ^2) <> 0
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b & a <> b implies ((sqrt a) ^2) - ((sqrt b) ^2) <> 0 )
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: a <> b ; ::_thesis: ((sqrt a) ^2) - ((sqrt b) ^2) <> 0
A4: 0 <= sqrt a by A1, Def2;
A5: 0 <= sqrt b by A2, Def2;
 sqrt a <> sqrt b by A1, A2, A3, Th28;
hence  ((sqrt a) ^2) - ((sqrt b) ^2) <> 0 by A4, A5, Lm2; ::_thesis: verum
end;

theorem :: SQUARE_1:36
for a, b being real number st 0 <= a & 0 <= b & a <> b holds
1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b & a <> b implies 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b) )
assume that
A1: 0 <= a and
A2: 0 <= b and
A3: a <> b ; ::_thesis: 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (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 ; ::_thesis: verum
end;

theorem :: SQUARE_1:37
for b, a being real number st 0 <= b & b < a holds
1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)
proof
let b, a be real number ; ::_thesis: ( 0 <= b & b < a implies 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b) )
assume that
A1: 0 <= b and
A2: b < a ; ::_thesis: 1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)
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 ; ::_thesis: verum
end;

theorem :: SQUARE_1:38
for a, b being real number st 0 <= a & 0 <= b holds
1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b implies 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; ::_thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)
percases ( a <> b or a = b ) ;
suppose a <> b ; ::_thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (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 ;
::_thesis: verum
end;
supposeA3: a = b ; ::_thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)
then  1 / ((sqrt a) - (sqrt b)) = 0 ;
hence  1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) by A3; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:39
for b, a being real number st 0 <= b & b < a holds
1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)
proof
let b, a be real number ; ::_thesis: ( 0 <= b & b < a implies 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b) )
assume that
A1: 0 <= b and
A2: b < a ; ::_thesis: 1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)
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 ; ::_thesis: verum
end;

theorem :: SQUARE_1:40
for x, y being complex number holds
( not x ^2 = y ^2 or x = y or x = - y )
proof
let x, y be complex number ; ::_thesis: ( not x ^2 = y ^2 or x = y or x = - y )
assume  x ^2 = y ^2 ; ::_thesis: ( x = y or x = - y )
then  (x - y) * (x + y) = 0 ;
then  ( x - y = 0 or x + y = 0 ) ;
hence  ( x = y or x = - y ) ; ::_thesis: verum
end;

theorem :: SQUARE_1:41
for x being complex number holds
( not x ^2 = 1 or x = 1 or x = - 1 )
proof
let x be complex number ; ::_thesis: ( not x ^2 = 1 or x = 1 or x = - 1 )
assume  x ^2 = 1 ; ::_thesis: ( x = 1 or x = - 1 )
then  (x - 1) * (x + 1) = 0 ;
then  ( x - 1 = 0 or x + 1 = 0 ) ;
hence  ( x = 1 or x = - 1 ) ; ::_thesis: verum
end;

theorem :: SQUARE_1:42
for x being real number st 0 <= x & x <= 1 holds
x ^2 <= x
proof
let x be real number ; ::_thesis: ( 0 <= x & x <= 1 implies x ^2 <= x )
assume that
A1: 0 <= x and
A2: x <= 1 ; ::_thesis: x ^2 <= x
percases ( 0 = x or 0 < x ) by A1;
suppose 0 = x ; ::_thesis: x ^2 <= x
hence  x ^2 <= x ; ::_thesis: verum
end;
supposeA3: 0 < x ; ::_thesis: x ^2 <= x
percases ( x = 1 or x < 1 ) by A2, XXREAL_0:1;
suppose x = 1 ; ::_thesis: x ^2 <= x
hence  x ^2 <= x ; ::_thesis: verum
end;
suppose x < 1 ; ::_thesis: x ^2 <= x
hence  x ^2 <= x by A3, Th13; ::_thesis: verum
end;
end;
end;
end;
end;

theorem :: SQUARE_1:43
for x being real number st (x ^2) - 1 <= 0 holds
( - 1 <= x & x <= 1 )
proof
let x be real number ; ::_thesis: ( (x ^2) - 1 <= 0 implies ( - 1 <= x & x <= 1 ) )
assume  (x ^2) - 1 <= 0 ; ::_thesis: ( - 1 <= x & x <= 1 )
then  (x - 1) * (x + 1) <= 0 ;
hence  ( - 1 <= x & x <= 1 ) by XREAL_1:93; ::_thesis: verum
end;

begin

theorem Th44: :: SQUARE_1:44
for a, x being real number st a <= 0 & x < a holds
x ^2 > a ^2
proof
let a, x be real number ; ::_thesis: ( a <= 0 & x < a implies x ^2 > a ^2 )
assume that
A1: a <= 0 and
A2: x < a ; ::_thesis: x ^2 > a ^2
 - x > - a by A2, XREAL_1:24;
then  (- x) ^2 > (- a) ^2 by A1, Th16;
hence  x ^2 > a ^2 ; ::_thesis: verum
end;

theorem :: SQUARE_1:45
for a being real number st - 1 >= a holds
- a <= a ^2
proof
let a be real number ; ::_thesis: ( - 1 >= a implies - a <= a ^2 )
assume  - 1 >= a ; ::_thesis: - a <= a ^2
then  - (- 1) <= - a by XREAL_1:24;
then  - a <= (- a) ^2 by XREAL_1:151;
hence  - a <= a ^2 ; ::_thesis: verum
end;

theorem :: SQUARE_1:46
for a being real number st - 1 > a holds
- a < a ^2
proof
let a be real number ; ::_thesis: ( - 1 > a implies - a < a ^2 )
assume  - 1 > a ; ::_thesis: - a < a ^2
then  - (- 1) < - a by XREAL_1:24;
then  - a < (- a) ^2 by Th14;
hence  - a < a ^2 ; ::_thesis: verum
end;

theorem :: SQUARE_1:47
for b, a being real number st b ^2 <= a ^2 & a >= 0 holds
( - a <= b & b <= a )
proof
let b, a be real number ; ::_thesis: ( b ^2 <= a ^2 & a >= 0 implies ( - a <= b & b <= a ) )
assume that
A1: b ^2 <= a ^2 and
A2: a >= 0 ; ::_thesis: ( - a <= b & b <= a )
now__::_thesis:_(_not_-_a_>_b_&_not_b_>_a_)
assume A3: ( - a > b or b > a ) ; ::_thesis: contradiction
now__::_thesis:_(_(_-_a_>_b_&_contradiction_)_or_(_b_>_a_&_contradiction_)_)
percases ( - a > b or b > a ) by A3;
case - a > b ; ::_thesis: contradiction
then  - (- a) < - b by XREAL_1:24;
then  a ^2 < (- b) ^2 by A2, Th16;
hence  contradiction by A1; ::_thesis: verum
end;
case b > a ; ::_thesis: contradiction
hence  contradiction by A1, A2, Th16; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( - a <= b & b <= a ) ; ::_thesis: verum
end;

theorem :: SQUARE_1:48
for b, a being real number st b ^2 < a ^2 & a >= 0 holds
( - a < b & b < a )
proof
let b, a be real number ; ::_thesis: ( b ^2 < a ^2 & a >= 0 implies ( - a < b & b < a ) )
assume that
A1: b ^2 < a ^2 and
A2: a >= 0 ; ::_thesis: ( - a < b & b < a )
now__::_thesis:_(_not_-_a_>=_b_&_not_b_>=_a_)
assume A3: ( - a >= b or b >= a ) ; ::_thesis: contradiction
now__::_thesis:_(_(_-_a_>=_b_&_contradiction_)_or_(_b_>=_a_&_contradiction_)_)
percases ( - a >= b or b >= a ) by A3;
case - a >= b ; ::_thesis: contradiction
then  - (- a) <= - b by XREAL_1:24;
then  a ^2 <= (- b) ^2 by A2, Th15;
hence  contradiction by A1; ::_thesis: verum
end;
case b >= a ; ::_thesis: contradiction
hence  contradiction by A1, A2, Th15; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
hence  ( - a < b & b < a ) ; ::_thesis: verum
end;

theorem Th49: :: SQUARE_1:49
for a, b being real number st - a <= b & b <= a holds
b ^2 <= a ^2
proof
let a, b be real number ; ::_thesis: ( - a <= b & b <= a implies b ^2 <= a ^2 )
assume that
A1: - a <= b and
A2: b <= a ; ::_thesis: b ^2 <= a ^2
percases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; ::_thesis: b ^2 <= a ^2
hence  b ^2 <= a ^2 by A2, Th15; ::_thesis: verum
end;
supposeA3: b < 0 ; ::_thesis: b ^2 <= a ^2
 - (- a) >= - b by A1, XREAL_1:24;
then  (- b) ^2 <= a ^2 by A3, Th15;
hence  b ^2 <= a ^2 ; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:50
for a, b being real number st - a < b & b < a holds
b ^2 < a ^2
proof
let a, b be real number ; ::_thesis: ( - a < b & b < a implies b ^2 < a ^2 )
assume that
A1: - a < b and
A2: b < a ; ::_thesis: b ^2 < a ^2
percases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; ::_thesis: b ^2 < a ^2
hence  b ^2 < a ^2 by A2, Th16; ::_thesis: verum
end;
supposeA3: b < 0 ; ::_thesis: b ^2 < a ^2
 - (- a) > - b by A1, XREAL_1:24;
then  (- b) ^2 < a ^2 by A3, Th16;
hence  b ^2 < a ^2 ; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:51
for a being real number st a ^2 <= 1 holds
( - 1 <= a & a <= 1 )
proof
let a be real number ; ::_thesis: ( a ^2 <= 1 implies ( - 1 <= a & a <= 1 ) )
assume  a ^2 <= 1 ; ::_thesis: ( - 1 <= a & a <= 1 )
then  (a ^2) - (1 ^2) <= (1 ^2) - (1 ^2) by XREAL_1:9;
then  (a - 1) * (a + 1) <= 0 ;
hence  ( - 1 <= a & a <= 1 ) by XREAL_1:93; ::_thesis: verum
end;

theorem :: SQUARE_1:52
for a being real number st a ^2 < 1 holds
( - 1 < a & a < 1 )
proof
let a be real number ; ::_thesis: ( a ^2 < 1 implies ( - 1 < a & a < 1 ) )
assume  a ^2 < 1 ; ::_thesis: ( - 1 < a & a < 1 )
then  (a ^2) - (1 ^2) < (1 ^2) - (1 ^2) by XREAL_1:9;
then  (a - 1) * (a + 1) < 0 ;
hence  ( - 1 < a & a < 1 ) by XREAL_1:94; ::_thesis: verum
end;

theorem Th53: :: SQUARE_1:53
for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(a ^2) * (b ^2) <= 1
proof
let a, b be real number ; ::_thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (a ^2) * (b ^2) <= 1 )
assume that
A1: - 1 <= a and
A2: a <= 1 and
A3: - 1 <= b and
A4: b <= 1 ; ::_thesis: (a ^2) * (b ^2) <= 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  (a ^2) * (b ^2) <= 1 by A6, XXREAL_0:2; ::_thesis: verum
end;

theorem Th54: :: SQUARE_1:54
for a, b being real number st a >= 0 & b >= 0 holds
a * (sqrt b) = sqrt ((a ^2) * b)
proof
let a, b be real number ; ::_thesis: ( a >= 0 & b >= 0 implies a * (sqrt b) = sqrt ((a ^2) * b) )
assume that
A1: a >= 0 and
A2: b >= 0 ; ::_thesis: a * (sqrt b) = sqrt ((a ^2) * b)
 sqrt (a ^2) = a by A1, Def2;
hence  a * (sqrt b) = sqrt ((a ^2) * b) by A1, A2, Th29; ::_thesis: verum
end;

Lm6:  for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(1 + (a ^2)) * (b ^2) <= 1 + (b ^2)
proof
let a, b be real number ; ::_thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (1 + (a ^2)) * (b ^2) <= 1 + (b ^2) )
assume that
A1: - 1 <= a and
A2: a <= 1 and
A3: - 1 <= b and
A4: b <= 1 ; ::_thesis: (1 + (a ^2)) * (b ^2) <= 1 + (b ^2)
 (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  (1 + (a ^2)) * (b ^2) <= 1 + (b ^2) ; ::_thesis: verum
end;

theorem Th55: :: SQUARE_1:55
for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
proof
let a, b be real number ; ::_thesis: ( - 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))) ) )
assume that
A1: - 1 <= a and
A2: a <= 1 and
A3: - 1 <= b and
A4: b <= 1 ; ::_thesis: ( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
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__::_thesis:_(-_b)_*_(sqrt_(1_+_(a_^2)))_<=_sqrt_(1_+_(b_^2))
percases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; ::_thesis: (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))
hence  (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) by A8, A7; ::_thesis: verum
end;
supposeA10: b < 0 ; ::_thesis: (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))
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; ::_thesis: verum
end;
end;
end;
then  - ((- b) * (sqrt (1 + (a ^2)))) >= - (sqrt (1 + (b ^2))) by XREAL_1:24;
hence  ( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ) by A9; ::_thesis: verum
end;

theorem :: SQUARE_1:56
for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))
proof
let a, b be real number ; ::_thesis: ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) )
assume that
A1: - 1 <= a and
A2: a <= 1 and
A3: - 1 <= b and
A4: b <= 1 ; ::_thesis: b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))
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  b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) ; ::_thesis: verum
end;

Lm7:  for b, a being real number st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
proof
let b, a be real number ; ::_thesis: ( b <= 0 & a <= b implies a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
assume that
A1: b <= 0 and
A2: a <= b ; ::_thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
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  a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by XREAL_1:24; ::_thesis: verum
end;

Lm8:  for a, b being real number st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
proof
let a, b be real number ; ::_thesis: ( a <= 0 & a <= b implies a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )
assume that
A1: a <= 0 and
A2: a <= b ; ::_thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
now__::_thesis:_(_(_b_<=_0_&_a_*_(sqrt_(1_+_(b_^2)))_<=_b_*_(sqrt_(1_+_(a_^2)))_)_or_(_b_>_0_&_a_*_(sqrt_(1_+_(b_^2)))_<=_b_*_(sqrt_(1_+_(a_^2)))_)_)
percases ( b <= 0 or b > 0 ) ;
case b <= 0 ; ::_thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
hence  a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A2, Lm7; ::_thesis: verum
end;
caseA3: b > 0 ; ::_thesis: a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
 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  a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) by A3, A4; ::_thesis: verum
end;
end;
end;
hence  a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) ; ::_thesis: verum
end;

Lm9:  for a, b being real number st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
proof
let a, b be real number ; ::_thesis: ( a >= 0 & a >= b implies a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) )
assume that
A1: a >= 0 and
A2: a >= b ; ::_thesis: a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
 - 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  a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) by XREAL_1:24; ::_thesis: verum
end;

theorem :: SQUARE_1:57
for a, b being real number st a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
proof
let a, b be real number ; ::_thesis: ( a >= b implies a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) )
assume A1: a >= b ; ::_thesis: a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
hence  a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) by A1, Lm9; ::_thesis: verum
end;
suppose a < 0 ; ::_thesis: a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
hence  a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) by A1, Lm7; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:58
for a, b being real number st a >= 0 holds
sqrt (a + (b ^2)) >= b
proof
let a, b be real number ; ::_thesis: ( a >= 0 implies sqrt (a + (b ^2)) >= b )
assume A1: a >= 0 ; ::_thesis: sqrt (a + (b ^2)) >= b
percases ( b < 0 or b >= 0 ) ;
suppose b < 0 ; ::_thesis: sqrt (a + (b ^2)) >= b
hence  sqrt (a + (b ^2)) >= b by A1, Def2; ::_thesis: verum
end;
supposeA2: b >= 0 ; ::_thesis: sqrt (a + (b ^2)) >= b
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; ::_thesis: verum
end;
end;
end;

theorem :: SQUARE_1:59
for a, b being real number st 0 <= a & 0 <= b holds
sqrt (a + b) <= (sqrt a) + (sqrt b)
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 0 <= b implies sqrt (a + b) <= (sqrt a) + (sqrt b) )
assume that
A1: 0 <= a and
A2: 0 <= b ; ::_thesis: sqrt (a + b) <= (sqrt a) + (sqrt 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, Th22 ;
hence  sqrt (a + b) <= (sqrt a) + (sqrt b) by A1, A2, A4, Th26; ::_thesis: verum
end;