:: by Andrzej Trybulec and Czes{\l}aw Byli\'nski

::

:: Received November 16, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let x be Element of COMPLEX ;

:: original: ^2

redefine func x ^2 -> Element of COMPLEX ;

coherence

x ^2 is Element of COMPLEX by XCMPLX_0:def 2;

end;
:: original: ^2

redefine func x ^2 -> Element of COMPLEX ;

coherence

x ^2 is Element of COMPLEX by XCMPLX_0:def 2;

Lm1: for a being Real st 0 < a holds

ex x being Real st

( 0 < x & x ^2 < a )

proof end;

Lm2: for x, y being Real st 0 <= x & 0 <= y & x ^2 = y ^2 holds

x = y

proof end;

definition

let a be Real;

assume A1: 0 <= a ;

existence

ex b_{1} being Real st

( 0 <= b_{1} & b_{1} ^2 = a )

for b_{1}, b_{2} being Real st 0 <= b_{1} & b_{1} ^2 = a & 0 <= b_{2} & b_{2} ^2 = a holds

b_{1} = b_{2}
by Lm2;

end;
assume A1: 0 <= a ;

existence

ex b

( 0 <= b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines sqrt SQUARE_1:def 2 :

for a being Real st 0 <= a holds

for b_{2} being Real holds

( b_{2} = sqrt a iff ( 0 <= b_{2} & b_{2} ^2 = a ) );

for a being Real st 0 <= a holds

for b

( b

Lm3: for x, y being Real st 0 <= x & x < y holds

sqrt x < sqrt y

proof end;

Lm4: 2 ^2 = 2 * 2

;

theorem :: SQUARE_1:31

Lm5: for a, b being Real st 0 <= a & 0 <= b & a <> b holds

((sqrt a) ^2) - ((sqrt b) ^2) <> 0

proof end;

theorem :: SQUARE_1:36

for a, b being Real st 0 <= a & 0 <= b & a <> b holds

1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)

1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)

proof end;

theorem :: SQUARE_1:37

for a, b being Real st 0 <= b & b < a holds

1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)

1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)

proof end;

theorem :: SQUARE_1:38

for a, b being Real st 0 <= a & 0 <= b holds

1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

proof end;

theorem :: SQUARE_1:39

for a, b being Real st 0 <= b & b < a holds

1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

1 / ((sqrt a) - (sqrt b)) = ((sqrt a) + (sqrt b)) / (a - b)

proof end;

:: from JGRAPH_5, 2006.08.13, A.T.

:: from JGRAPH_2, 2006.12.29, AK

:: from JGRAPH_4, 2006.12.29, AK

:: from JGRAPH_6, 2006.12.29, AK

Lm6: for a, b being Real st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds

(1 + (a ^2)) * (b ^2) <= 1 + (b ^2)

proof end;

theorem Th55: :: SQUARE_1:55

for a, b being Real 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))) )

( (- b) * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2)) & - (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) )

proof end;

theorem :: SQUARE_1:56

for a, b being Real st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds

b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

b * (sqrt (1 + (a ^2))) <= sqrt (1 + (b ^2))

proof end;

Lm7: for a, b being Real st b <= 0 & a <= b holds

a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm8: for a, b being Real st a <= 0 & a <= b holds

a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm9: for a, b being Real st a >= 0 & a >= b holds

a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))

proof end;

:: from TOPREAL6, 201.07.31, A.T.

:: 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;