:: 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 Association of Mizar Users
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
:: deftheorem SQUARE_1:def 1 :
canceled;
:: deftheorem SQUARE_1:def 2 :
canceled;
:: deftheorem defines ^2 SQUARE_1:def 3 :
theorem :: SQUARE_1:54
canceled;
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
theorem Th71: :: SQUARE_1:71
theorem :: SQUARE_1:72
canceled;
theorem :: SQUARE_1:73
canceled;
theorem :: SQUARE_1:74
theorem Th75: :: SQUARE_1:75
theorem Th76: :: SQUARE_1:76
Lm1:
for a being real number st 0 < a holds
ex x being real number st
( 0 < x & x ^2 < a )
theorem Th77: :: SQUARE_1:77
theorem Th78: :: SQUARE_1:78
Lm2:
for x, y being real number st 0 <= x & 0 <= y & x ^2 = y ^2 holds
x = y
:: deftheorem Def4 defines sqrt SQUARE_1:def 4 :
theorem :: SQUARE_1:79
canceled;
theorem :: SQUARE_1:80
canceled;
theorem :: SQUARE_1:81
canceled;
theorem :: SQUARE_1:82
theorem Th83: :: SQUARE_1:83
Lm3:
for a being real number st 0 <= a holds
sqrt (a ^2 ) = a
by Def4;
Lm4:
for x, y being real number st 0 <= x & x < y holds
sqrt x < sqrt y
theorem :: SQUARE_1:84
Lm5:
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
theorem :: SQUARE_1:91
canceled;
theorem :: SQUARE_1:92
theorem Th93: :: SQUARE_1:93
theorem Th94: :: SQUARE_1:94
theorem :: SQUARE_1:95
theorem Th96: :: SQUARE_1:96
theorem Th97: :: SQUARE_1:97
theorem :: SQUARE_1:98
canceled;
theorem Th99: :: SQUARE_1:99
theorem :: SQUARE_1:100
canceled;
theorem :: SQUARE_1:101
theorem :: SQUARE_1:102
theorem :: SQUARE_1:103
theorem :: SQUARE_1:104
Lm6:
for a, b being real number st 0 <= a & 0 <= b & a <> b holds
((sqrt a) ^2 ) - ((sqrt b) ^2 ) <> 0
theorem :: SQUARE_1:105
theorem :: SQUARE_1:106
theorem :: SQUARE_1:107
theorem :: SQUARE_1:108
theorem :: SQUARE_1:109
theorem :: SQUARE_1:110
theorem :: SQUARE_1:111
theorem :: SQUARE_1:112
theorem :: SQUARE_1:113
canceled;
theorem Th114: :: SQUARE_1:114
theorem :: SQUARE_1:115
theorem :: SQUARE_1:116
theorem :: SQUARE_1:117
theorem :: SQUARE_1:118
theorem Th119: :: SQUARE_1:119
theorem :: SQUARE_1:120
theorem :: SQUARE_1:121
theorem :: SQUARE_1:122
theorem Th123: :: SQUARE_1:123
theorem Th124: :: SQUARE_1:124
Lm7:
for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 )
theorem Th125: :: SQUARE_1:125
theorem :: SQUARE_1:126
Lm8:
for b, a being real number st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))
Lm9:
for a, b being real number st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))
Lm10:
for a, b being real number st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2 ))) >= b * (sqrt (1 + (a ^2 )))
theorem :: SQUARE_1:127