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


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

theorem :: SQUARE_1:2
for x, y being real number st 0 <= x & 0 <= y holds
max (x,y) <= x + y
proof end;

definition
let x be complex number ;
func x ^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 ;
cluster x ^2 -> complex ;
coherence
x ^2 is complex ;
end;

registration
let x be real number ;
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;

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;

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

theorem Th14: :: SQUARE_1:14
for a being real number st 1 < a holds
a < a ^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;

theorem Th15: :: SQUARE_1:15
for x, y being real number st 0 <= x & x <= y holds
x ^2 <= y ^2
proof end;

theorem Th16: :: SQUARE_1:16
for x, y being real number st 0 <= x & x < y holds
x ^2 < y ^2
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 ;
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 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 end;

theorem Th18: :: SQUARE_1:18
sqrt 1 = 1
proof end;

Lm3: for x, y being real number 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 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 end;

theorem Th24: :: SQUARE_1:24
for a being real number st 0 <= a & sqrt a = 0 holds
a = 0
proof end;

theorem Th25: :: SQUARE_1:25
for a being real number st 0 < a holds
0 < sqrt a
proof end;

theorem Th26: :: SQUARE_1:26
for x, y being real number st 0 <= x & x <= y holds
sqrt x <= sqrt y
proof 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 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 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 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 end;

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

theorem :: SQUARE_1:40
for x, y being complex number holds
( not x ^2 = y ^2 or x = y or x = - y )
proof end;

theorem :: SQUARE_1:41
for x being complex number holds
( not x ^2 = 1 or x = 1 or x = - 1 )
proof end;

theorem :: SQUARE_1:42
for x being real number st 0 <= x & x <= 1 holds
x ^2 <= x
proof end;

theorem :: SQUARE_1:43
for x being real number st (x ^2) - 1 <= 0 holds
( - 1 <= x & x <= 1 )
proof end;

begin

:: from JGRAPH_5, 2006.08.13, A.T.
theorem Th44: :: SQUARE_1:44
for a, x being real number 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 number st - 1 >= a holds
- a <= a ^2
proof end;

theorem :: SQUARE_1:46
for a being real number st - 1 > a holds
- a < a ^2
proof end;

theorem :: SQUARE_1:47
for b, a being real number st b ^2 <= a ^2 & a >= 0 holds
( - a <= b & b <= a )
proof end;

theorem :: SQUARE_1:48
for b, a being real number st b ^2 < a ^2 & a >= 0 holds
( - a < b & b < a )
proof end;

theorem Th49: :: SQUARE_1:49
for a, b being real number st - a <= b & b <= a holds
b ^2 <= a ^2
proof end;

theorem :: SQUARE_1:50
for a, b being real number 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 number st a ^2 <= 1 holds
( - 1 <= a & a <= 1 )
proof end;

theorem :: SQUARE_1:52
for a being real number 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 number 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 number st a >= 0 & b >= 0 holds
a * (sqrt b) = sqrt ((a ^2) * b)
proof 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 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 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 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;

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

theorem :: SQUARE_1:58
for a, b being real number 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 number st 0 <= a & 0 <= b holds
sqrt (a + b) <= (sqrt a) + (sqrt b)
proof end;