:: 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-2021 Association of Mizar Users

scheme :: SQUARE_1:sch 1
RealContinuity{ P₁[ object ], P₂[ object ] } :

ex z being Real st
for x, y being Real st P₁[x] & P₂[y] holds
( x <= z & z <= y )

provided

A1: for x, y being Real st P₁[x] & P₂[y] holds
x <= y

proof end;

theorem :: SQUARE_1:1

for x, y being Real holds (min (x,y)) + (max (x,y)) = x + y

proof end;

theorem :: SQUARE_1:2

for x, y being Real st 0 <= x & 0 <= y holds
max (x,y) <= x + y

proof end;

definition

let x be Complex;

func x ^2 -> number equals :: SQUARE_1:def 1
x * x;

correctness
coherence
x * x is number ;
;

end;

:: deftheorem defines ^2 SQUARE_1:def 1 :
for x being Complex holds x ^2 = x * x;

registration

let x be Complex;

cluster x ^2 -> complex ;

coherence
x ^2 is complex ;

end;

registration

let x be Real;

cluster x ^2 -> real ;

coherence
x ^2 is real ;

end;

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;

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 Th10: :: SQUARE_1:10

for a, b being Complex st (a ^2) - (b ^2) <> 0 holds
1 / (a + b) = (a - b) / ((a ^2) - (b ^2))

proof end;

theorem Th11: :: SQUARE_1:11

for a, b being Complex st (a ^2) - (b ^2) <> 0 holds
1 / (a - b) = (a + b) / ((a ^2) - (b ^2))

proof end;

theorem :: SQUARE_1:12

for a being Real st 0 <> a holds
0 < a ^2 by XREAL_1:63;

theorem Th13: :: SQUARE_1:13

for a being Real st 0 < a & a < 1 holds
a ^2 < a

proof end;

theorem Th14: :: SQUARE_1:14

for a being Real st 1 < a holds
a < a ^2

proof end;

Lm1: for a being Real st 0 < a holds
ex x being Real st
( 0 < x & x ^2 < a )

proof end;

theorem Th15: :: SQUARE_1:15

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

proof end;

theorem Th16: :: SQUARE_1:16

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

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 ;

func sqrt a -> Real means :Def2: :: SQUARE_1:def 2
( 0 <= it & it ^2 = a );

existence
ex b₁ being Real st
( 0 <= b₁ & b₁ ^2 = a )

proof end;

uniqueness
for b₁, b₂ being Real st 0 <= b₁ & b₁ ^2 = a & 0 <= b₂ & b₂ ^2 = a holds
b₁ = b₂ by Lm2;

end;

:: deftheorem Def2 defines sqrt SQUARE_1:def 2 :
for a being Real st 0 <= a holds
for b₂ being Real holds
( b₂ = sqrt a iff ( 0 <= b₂ & b₂ ^2 = a ) );

theorem Th17: :: SQUARE_1:17

sqrt 0 = 0

proof end;

theorem Th18: :: SQUARE_1:18

sqrt 1 = 1

proof end;

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

proof 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 :: SQUARE_1:22

for a being Real st 0 <= a holds
sqrt (a ^2) = a by Def2;

theorem :: SQUARE_1:23

for a being Real st a <= 0 holds
sqrt (a ^2) = - a

proof end;

theorem Th24: :: SQUARE_1:24

for a being Real st 0 <= a & sqrt a = 0 holds
a = 0

proof end;

theorem Th25: :: SQUARE_1:25

for a being Real st 0 < a holds
0 < sqrt a

proof end;

theorem Th26: :: SQUARE_1:26

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

proof end;

theorem :: SQUARE_1:27

for x, y being Real st 0 <= x & x < y holds
sqrt x < sqrt y by Lm3;

theorem Th28: :: SQUARE_1:28

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

proof end;

theorem Th29: :: SQUARE_1:29

for a, b being Real st 0 <= a & 0 <= b holds
sqrt (a * b) = (sqrt a) * (sqrt b)

proof end;

theorem Th30: :: SQUARE_1:30

for a, b being Real st 0 <= a & 0 <= b holds
sqrt (a / b) = (sqrt a) / (sqrt b)

proof end;

theorem :: SQUARE_1:31

for a, b being Real 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 st 0 < a holds
sqrt (1 / a) = 1 / (sqrt a) by Th18, Th30;

theorem :: SQUARE_1:33

for a being Real st 0 < a holds
(sqrt a) / a = 1 / (sqrt a)

proof end;

theorem :: SQUARE_1:34

for a being Real st 0 < a holds
a / (sqrt a) = sqrt a

proof end;

theorem :: SQUARE_1:35

for a, b being Real st 0 <= a & 0 <= b holds
((sqrt a) - (sqrt b)) * ((sqrt a) + (sqrt b)) = a - b

proof end;

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)

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)

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)

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)

proof end;

theorem :: SQUARE_1:40

for x, y being Complex holds
( not x ^2 = y ^2 or x = y or x = - y )

proof end;

theorem :: SQUARE_1:41

for x being Complex holds
( not x ^2 = 1 or x = 1 or x = - 1 )

proof end;

theorem :: SQUARE_1:42

for x being Real st 0 <= x & x <= 1 holds
x ^2 <= x

proof end;

theorem :: SQUARE_1:43

for x being Real st (x ^2) - 1 <= 0 holds
( - 1 <= x & x <= 1 )

proof end;

:: from JGRAPH_5, 2006.08.13, A.T.

theorem Th44: :: SQUARE_1:44

for a, x being Real st a <= 0 & x < a holds
x ^2 > a ^2

proof end;

:: from JGRAPH_2, 2006.12.29, AK

theorem :: SQUARE_1:45

for a being Real st - 1 >= a holds
- a <= a ^2

proof end;

theorem :: SQUARE_1:46

for a being Real st - 1 > a holds
- a < a ^2

proof end;

theorem :: SQUARE_1:47

for a, b being Real st b ^2 <= a ^2 & a >= 0 holds
( - a <= b & b <= a )

proof end;

theorem :: SQUARE_1:48

for a, b being Real st b ^2 < a ^2 & a >= 0 holds
( - a < b & b < a )

proof end;

theorem Th49: :: SQUARE_1:49

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

proof end;

theorem :: SQUARE_1:50

for a, b being Real st - a < b & b < a holds
b ^2 < a ^2

proof end;

:: from JGRAPH_4, 2006.12.29, AK

theorem :: SQUARE_1:51

for a being Real st a ^2 <= 1 holds
( - 1 <= a & a <= 1 )

proof end;

theorem :: SQUARE_1:52

for a being Real st a ^2 < 1 holds
( - 1 < a & a < 1 )

proof end;

:: from JGRAPH_6, 2006.12.29, AK

theorem Th53: :: SQUARE_1:53

for a, b being Real st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(a ^2) * (b ^2) <= 1

proof end;

theorem Th54: :: SQUARE_1:54

for a, b being Real st a >= 0 & b >= 0 holds
a * (sqrt b) = sqrt ((a ^2) * b)

proof end;

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

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

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;

theorem :: SQUARE_1:57

for a, b being Real st a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))

proof end;

theorem :: SQUARE_1:58

for a, b being Real st a >= 0 holds
sqrt (a + (b ^2)) >= b

proof end;

:: from TOPREAL6, 201.07.31, A.T.

theorem :: SQUARE_1:59

for a, b being Real st 0 <= a & 0 <= b holds
sqrt (a + b) <= (sqrt a) + (sqrt b)

proof end;