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

::

:: Received November 16, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

scheme :: SQUARE_1:sch 1

RealContinuity{ P_{1}[ set ], P_{2}[ set ] } :

RealContinuity{ P

ex z being real number st

for x, y being real number st P_{1}[x] & P_{2}[y] holds

( x <= z & z <= y )

provided
for x, y being real number st P

( x <= z & z <= 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;
:: 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;

theorem :: SQUARE_1:1

canceled;

theorem :: SQUARE_1:2

canceled;

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

canceled;

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 :: SQUARE_1:35

canceled;

theorem :: SQUARE_1:36

canceled;

theorem :: SQUARE_1:37

canceled;

theorem :: SQUARE_1:38

canceled;

theorem :: SQUARE_1:39

canceled;

theorem :: SQUARE_1:40

canceled;

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 :: SQUARE_1:46

canceled;

theorem :: SQUARE_1:47

canceled;

theorem :: SQUARE_1:48

canceled;

theorem :: SQUARE_1:49

canceled;

theorem :: SQUARE_1:50

canceled;

theorem :: SQUARE_1:51

canceled;

theorem :: SQUARE_1:52

canceled;

theorem :: SQUARE_1:53

proof end;

theorem :: SQUARE_1:54

proof end;

definition

let x be complex number ;

canceled;

canceled;

func x ^2 -> set equals :: SQUARE_1:def 3

x * x;

correctness

coherence

x * x is set ;

;

end;
canceled;

canceled;

func x ^2 -> set equals :: SQUARE_1:def 3

x * x;

correctness

coherence

x * x is set ;

;

:: deftheorem SQUARE_1:def 1 :

canceled;

:: deftheorem SQUARE_1:def 2 :

canceled;

:: deftheorem defines ^2 SQUARE_1:def 3 :

for x being complex number holds x ^2 = x * x;

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

canceled;

theorem :: SQUARE_1:56

canceled;

theorem :: SQUARE_1:57

canceled;

theorem :: SQUARE_1:58

canceled;

theorem :: SQUARE_1:59

canceled;

theorem :: SQUARE_1:60

canceled;

theorem :: SQUARE_1:61

theorem :: SQUARE_1:62

canceled;

theorem :: SQUARE_1:63

theorem :: SQUARE_1:64

theorem :: SQUARE_1:65

theorem :: SQUARE_1:66

theorem :: SQUARE_1:67

theorem :: SQUARE_1:68

theorem :: SQUARE_1:69

canceled;

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

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

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

proof end;

theorem :: SQUARE_1:72

canceled;

theorem :: SQUARE_1:73

canceled;

theorem :: SQUARE_1:74

theorem Th75: :: SQUARE_1:75

proof end;

theorem Th76: :: SQUARE_1:76

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 Th77: :: SQUARE_1:77

proof end;

theorem Th78: :: SQUARE_1:78

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 :Def4: :: SQUARE_1:def 4

( 0 <= it & it ^2 = 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 ;

func sqrt a -> real number means :Def4: :: SQUARE_1:def 4

( 0 <= it & it ^2 = a );

existence

ex b

( 0 <= b

proof end;

uniqueness for b

b

:: deftheorem Def4 defines sqrt SQUARE_1:def 4 :

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;

theorem :: SQUARE_1:79

canceled;

theorem :: SQUARE_1:80

canceled;

theorem :: SQUARE_1:81

canceled;

theorem Th82: :: SQUARE_1:82

proof end;

theorem Th83: :: SQUARE_1:83

proof end;

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

sqrt x < sqrt y

proof end;

theorem :: SQUARE_1:84

Lm4: 2 ^2 = 2 * 2

;

theorem Th85: :: SQUARE_1:85

theorem :: SQUARE_1:86

theorem :: SQUARE_1:87

canceled;

theorem :: SQUARE_1:88

canceled;

theorem :: SQUARE_1:89

theorem :: SQUARE_1:90

proof end;

theorem :: SQUARE_1:91

canceled;

theorem Th92: :: SQUARE_1:92

proof end;

theorem Th93: :: SQUARE_1:93

proof end;

theorem Th94: :: SQUARE_1:94

proof end;

theorem :: SQUARE_1:95

theorem Th96: :: SQUARE_1:96

proof end;

theorem Th97: :: SQUARE_1:97

proof end;

theorem :: SQUARE_1:98

canceled;

theorem Th99: :: SQUARE_1:99

proof end;

theorem :: SQUARE_1:100

for a, b being real number st 0 <= a & 0 <= b holds

( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) ) by Th82, Th92;

( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) ) by Th82, Th92;

theorem :: SQUARE_1:101

theorem :: SQUARE_1:102

proof end;

theorem :: SQUARE_1:103

proof end;

theorem :: SQUARE_1:104

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

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

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

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

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

proof end;

theorem :: SQUARE_1:110

proof end;

theorem :: SQUARE_1:111

proof end;

theorem :: SQUARE_1:112

proof end;

theorem :: SQUARE_1:113

canceled;

begin

theorem Th114: :: SQUARE_1:114

proof end;

theorem :: SQUARE_1:115

proof end;

theorem :: SQUARE_1:116

proof end;

theorem :: SQUARE_1:117

proof end;

theorem :: SQUARE_1:118

proof end;

theorem Th119: :: SQUARE_1:119

proof end;

theorem :: SQUARE_1:120

proof end;

theorem :: SQUARE_1:121

proof end;

theorem :: SQUARE_1:122

proof end;

theorem Th123: :: SQUARE_1:123

proof end;

theorem Th124: :: SQUARE_1:124

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 Th125: :: SQUARE_1:125

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

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;

theorem :: SQUARE_1:127

proof end;