:: SQUARE_1 semantic presentation

registration

cluster -> complex Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem :: SQUARE_1:1

canceled;

theorem :: SQUARE_1:2

for x being real number st 1 < x holds
1 / x < 1

proof end;

Lm1: for x, y being real number st x < y holds
0 < y - x
by XREAL_1:52;

Lm2: for x, y being real number st x <= y holds
0 <= y - x
by XREAL_1:50;

Lm3: for x, y being real number st 0 <= x & 0 <= y holds
0 <= x * y
by XREAL_1:129;

Lm4: for x, y being real number st 0 < x & 0 < y holds
0 < x * y
by XREAL_1:131;

Lm5: for x, y being real number st 0 < x & y < 0 holds
x * y < 0
by XREAL_1:134;

theorem :: SQUARE_1:3

canceled;

theorem :: SQUARE_1:4

canceled;

theorem :: SQUARE_1:5

canceled;

theorem :: SQUARE_1:6

canceled;

theorem :: SQUARE_1:7

canceled;

theorem :: SQUARE_1:8

canceled;

theorem :: SQUARE_1:9

canceled;

theorem :: SQUARE_1:10

canceled;

theorem :: SQUARE_1:11

canceled;

theorem :: SQUARE_1:12

canceled;

theorem :: SQUARE_1:13

canceled;

theorem :: SQUARE_1:14

canceled;

theorem :: SQUARE_1:15

canceled;

theorem :: SQUARE_1:16

canceled;

theorem :: SQUARE_1:17

canceled;

theorem :: SQUARE_1:18

canceled;

theorem :: SQUARE_1:19

canceled;

theorem :: SQUARE_1:20

canceled;

theorem :: SQUARE_1:21

canceled;

theorem :: SQUARE_1:22

canceled;

theorem :: SQUARE_1:23

canceled;

theorem :: SQUARE_1:24

canceled;

theorem :: SQUARE_1:25

for x, y being real number holds
( not 0 <= x * y or ( 0 <= x & 0 <= y ) or ( x <= 0 & y <= 0 ) ) by Lm5;

Lm6: for a, b being real number st 0 <= a & 0 <= b holds
0 <= a / b
by XREAL_1:138;

Lm7: for x, y being real number st 0 < x holds
y - x < y
by XREAL_1:46;

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

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

provided

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

proof end;

definition

let x, y be real number ;
func min x,y -> real number equals :Def1: :: SQUARE_1:def 1
x if x <= y
otherwise y;
correctness ;
commutativity by XREAL_1:1;
idempotence ;
func max x,y -> real number equals :Def2: :: SQUARE_1:def 2
x if y <= x
otherwise y;
correctness ;
commutativity by XREAL_1:1;
idempotence ;

end;

:: deftheorem Def1 defines min SQUARE_1:def 1 :

:: deftheorem Def2 defines max SQUARE_1:def 2 :

definition

let x, y be Element of REAL ;
:: original: min
redefine func min x,y -> Element of REAL ;
coherence by XREAL_0:def 1;
:: original: max
redefine func max x,y -> Element of REAL ;
coherence by XREAL_0:def 1;

end;

theorem :: SQUARE_1:26

canceled;

theorem :: SQUARE_1:27

canceled;

theorem :: SQUARE_1:28

canceled;

theorem :: SQUARE_1:29

canceled;

theorem :: SQUARE_1:30

canceled;

theorem :: SQUARE_1:31

canceled;

theorem :: SQUARE_1:32

canceled;

theorem :: SQUARE_1:33

canceled;

theorem :: SQUARE_1:34

canceled;

theorem Th35: :: SQUARE_1:35

for x, y being real number holds min x,y <= x

proof end;

theorem :: SQUARE_1:36

canceled;

theorem :: SQUARE_1:37

canceled;

theorem Th38: :: SQUARE_1:38

for x, y being real number holds
( min x,y = x or min x,y = y )

proof end;

theorem Th39: :: SQUARE_1:39

for x, y, z being real number holds
( ( x <= y & x <= z ) iff x <= min y,z )

proof end;

theorem :: SQUARE_1:40

for x, y, z being real number holds min x,(min y,z) = min (min x,y),z

proof end;

theorem :: SQUARE_1:41

canceled;

theorem :: SQUARE_1:42

canceled;

theorem :: SQUARE_1:43

canceled;

theorem :: SQUARE_1:44

canceled;

theorem :: SQUARE_1:45

canceled;

theorem Th46: :: SQUARE_1:46

for x, y being real number holds x <= max x,y

proof end;

theorem :: SQUARE_1:47

canceled;

theorem :: SQUARE_1:48

canceled;

theorem Th49: :: SQUARE_1:49

for x, y being real number holds
( max x,y = x or max x,y = y )

proof end;

theorem :: SQUARE_1:50

for y, x, z being real number holds
( ( y <= x & z <= x ) iff max y,z <= x )

proof end;

theorem :: SQUARE_1:51

for x, y, z being real number holds max x,(max y,z) = max (max x,y),z

proof end;

theorem :: SQUARE_1:52

canceled;

theorem :: SQUARE_1:53

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

proof end;

theorem Th54: :: SQUARE_1:54

for x, y being real number holds max x,(min x,y) = x

proof end;

theorem Th55: :: SQUARE_1:55

for x, y being real number holds min x,(max x,y) = x

proof end;

theorem :: SQUARE_1:56

for x, y, z being real number holds min x,(max y,z) = max (min x,y),(min x,z)

proof end;

theorem :: SQUARE_1:57

for x, y, z being real number holds max x,(min y,z) = min (max x,y),(max x,z)

proof end;

definition

let x be complex number ;
func x ^2 -> set equals :: SQUARE_1:def 3
x * x;
correctness ;

end;

:: deftheorem defines ^2 SQUARE_1:def 3 :

registration

let x be complex number ;
cluster x ^2 -> complex ;
correctness ;

end;

registration

let x be real number ;
cluster x ^2 -> complex real ;
correctness ;

end;

definition

let x be Element of COMPLEX ;
:: original: ^2
redefine func x ^2 -> Element of COMPLEX ;
correctness by XCMPLX_0:def 2;

end;

definition

let x be Element of REAL ;
:: original: ^2
redefine func x ^2 -> Element of REAL ;
correctness by XREAL_0:def 1;

end;

theorem :: SQUARE_1:58

canceled;

theorem Th59: :: SQUARE_1:59

1 ^2 = 1 ;

theorem Th60: :: SQUARE_1:60

0 ^2 = 0 ;

theorem :: SQUARE_1:61

for a being complex number holds a ^2 = (- a) ^2 ;

theorem :: SQUARE_1:62

canceled;

theorem :: SQUARE_1:63

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

theorem :: SQUARE_1:64

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

theorem :: SQUARE_1:65

for a being complex number holds (a + 1) ^2 = ((a ^2 ) + (2 * a)) + 1 ;

theorem :: SQUARE_1:66

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

theorem :: SQUARE_1:67

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

theorem :: SQUARE_1:68

for a, b being complex number holds (a * b) ^2 = (a ^2 ) * (b ^2 ) ;

theorem Th69: :: SQUARE_1:69

for a, b being complex number holds (a / b) ^2 = (a ^2 ) / (b ^2 ) by XCMPLX_1:77;

theorem Th70: :: SQUARE_1:70

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 Th71: :: SQUARE_1:71

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 Th72: :: SQUARE_1:72

for a being real number holds 0 <= a ^2 by XREAL_1:65;

theorem Th73: :: SQUARE_1:73

for a being complex number st a ^2 = 0 holds
a = 0 by XCMPLX_1:6;

theorem :: SQUARE_1:74

for a being real number st 0 <> a holds
0 < a ^2

proof end;

theorem Th75: :: SQUARE_1:75

for a being real number st 0 < a & a < 1 holds
a ^2 < a

proof end;

theorem :: SQUARE_1:76

for a being real number st 1 < a holds
a < a ^2

proof end;

Lm8: for a being real number st 0 < a holds
ex x being real number st
( 0 < x & x ^2 < a )

proof end;

theorem Th77: :: SQUARE_1:77

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

proof end;

theorem Th78: :: SQUARE_1:78

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

proof end;

Lm9: 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 :Def4: :: SQUARE_1:def 4
( 0 <= it & it ^2 = a );
existence

proof end;