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

::

:: Received November 16, 1989

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

begin

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

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;

definition

let x be Element of REAL ;

:: original: ^2

redefine func x ^2 -> Element of REAL ;

coherence

x ^2 is Element of REAL by XREAL_0:def 1;

end;
:: original: ^2

redefine func x ^2 -> Element of REAL ;

coherence

x ^2 is Element of REAL by XREAL_0:def 1;

theorem :: SQUARE_1:4

theorem :: SQUARE_1:5

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))

1 / (a + b) = (a - b) / ((a ^2) - (b ^2))

proof 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))

1 / (a - b) = (a + b) / ((a ^2) - (b ^2))

proof end;

Lm1: for a being real number st 0 < a holds

ex x being real number st

( 0 < x & x ^2 < a )

proof end;

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

x = y

proof end;

definition

let a be real number ;

assume A1: 0 <= a ;

existence

ex b_{1} being real number st

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

for b_{1}, b_{2} being real number 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 number st 0 <= a holds

for b_{2} being real number holds

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

for a being real number st 0 <= a holds

for b

( b

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

redefine func sqrt a -> Element of REAL ;

coherence

sqrt a is Element of REAL by XREAL_0:def 1;

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

sqrt x < sqrt y

proof end;

Lm4: 2 ^2 = 2 * 2

;

theorem :: SQUARE_1:31

theorem :: SQUARE_1:32

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

((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b

proof end;

Lm5: for a, b being real number 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 number 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 b, a being real number 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 number 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 b, a being real number 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;

begin

:: 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 number 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 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))) )

( (- 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 number 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 b, a being real number st b <= 0 & a <= b holds

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

proof 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 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 end;

:: from TOPREAL6, 201.07.31, A.T.