:: REAL_2 semantic presentation

Lm1: ( 1 / 1 = 1 & 1 " = 1 & 1 / (- 1) = - 1 & (- 1) " = - 1 & (- 1) * (- 1) = 1 )
;

theorem :: REAL_2:1

canceled;

theorem :: REAL_2:2

canceled;

theorem :: REAL_2:3

canceled;

theorem :: REAL_2:4

canceled;

theorem :: REAL_2:5

canceled;

theorem :: REAL_2:6

canceled;

theorem :: REAL_2:7

canceled;

theorem :: REAL_2:8

canceled;

theorem :: REAL_2:9

canceled;

theorem :: REAL_2:10

canceled;

theorem :: REAL_2:11

canceled;

theorem :: REAL_2:12

canceled;

theorem :: REAL_2:13

canceled;

theorem :: REAL_2:14

canceled;

theorem :: REAL_2:15

canceled;

theorem :: REAL_2:16

canceled;

theorem :: REAL_2:17

canceled;

theorem :: REAL_2:18

canceled;

theorem :: REAL_2:19

canceled;

theorem :: REAL_2:20

canceled;

theorem :: REAL_2:21

canceled;

theorem :: REAL_2:22

canceled;

theorem :: REAL_2:23

canceled;

theorem :: REAL_2:24

canceled;

theorem :: REAL_2:25

canceled;

theorem :: REAL_2:26

canceled;

theorem :: REAL_2:27

canceled;

theorem :: REAL_2:28

canceled;

theorem :: REAL_2:29

canceled;

theorem :: REAL_2:30

canceled;

theorem :: REAL_2:31

canceled;

theorem :: REAL_2:32

canceled;

theorem :: REAL_2:33

canceled;

theorem :: REAL_2:34

canceled;

theorem :: REAL_2:35

canceled;

theorem :: REAL_2:36

canceled;

theorem :: REAL_2:37

canceled;

theorem :: REAL_2:38

canceled;

theorem :: REAL_2:39

canceled;

theorem :: REAL_2:40

canceled;

theorem :: REAL_2:41

canceled;

theorem :: REAL_2:42

canceled;

theorem :: REAL_2:43

canceled;

theorem :: REAL_2:44

canceled;

theorem :: REAL_2:45

canceled;

theorem :: REAL_2:46

canceled;

theorem :: REAL_2:47

canceled;

theorem :: REAL_2:48

canceled;

theorem :: REAL_2:49

canceled;

theorem :: REAL_2:50

canceled;

theorem :: REAL_2:51

canceled;

theorem :: REAL_2:52

canceled;

theorem :: REAL_2:53

canceled;

theorem :: REAL_2:54

canceled;

theorem :: REAL_2:55

canceled;

theorem :: REAL_2:56

canceled;

theorem :: REAL_2:57

canceled;

theorem :: REAL_2:58

canceled;

theorem :: REAL_2:59

canceled;

theorem :: REAL_2:60

canceled;

theorem :: REAL_2:61

canceled;

theorem :: REAL_2:62

canceled;

theorem :: REAL_2:63

for a, b being real number ex e being real number st a = b - e

proof end;

theorem :: REAL_2:64

canceled;

theorem :: REAL_2:65

canceled;

theorem :: REAL_2:66

canceled;

theorem :: REAL_2:67

canceled;

theorem :: REAL_2:68

canceled;

theorem :: REAL_2:69

canceled;

theorem :: REAL_2:70

canceled;

theorem :: REAL_2:71

canceled;

theorem :: REAL_2:72

canceled;

theorem :: REAL_2:73

canceled;

theorem :: REAL_2:74

canceled;

theorem :: REAL_2:75

canceled;

theorem :: REAL_2:76

canceled;

theorem :: REAL_2:77

canceled;

theorem :: REAL_2:78

canceled;

theorem :: REAL_2:79

canceled;

theorem :: REAL_2:80

canceled;

theorem :: REAL_2:81

canceled;

theorem :: REAL_2:82

canceled;

theorem :: REAL_2:83

canceled;

theorem :: REAL_2:84

canceled;

theorem :: REAL_2:85

canceled;

theorem :: REAL_2:86

canceled;

theorem :: REAL_2:87

canceled;

theorem :: REAL_2:88

canceled;

theorem :: REAL_2:89

canceled;

theorem :: REAL_2:90

canceled;

theorem :: REAL_2:91

canceled;

theorem :: REAL_2:92

canceled;

theorem :: REAL_2:93

canceled;

theorem :: REAL_2:94

canceled;

theorem :: REAL_2:95

canceled;

theorem :: REAL_2:96

canceled;

theorem :: REAL_2:97

canceled;

theorem :: REAL_2:98

canceled;

theorem :: REAL_2:99

canceled;

theorem :: REAL_2:100

canceled;

theorem :: REAL_2:101

canceled;

theorem :: REAL_2:102

canceled;

theorem :: REAL_2:103

canceled;

theorem :: REAL_2:104

canceled;

theorem :: REAL_2:105

for a, b, e being real number st ( a + (- b) <= 0 or b - a >= 0 or b + (- a) >= 0 or a - e <= b + (- e) or a + (- e) <= b - e or e - a >= e - b ) holds
a <= b

proof end;

theorem :: REAL_2:106

for a, b, e being real number st ( a + (- b) < 0 or b - a > 0 or (- a) + b > 0 or a - e e - b ) holds
a < b

proof end;

theorem :: REAL_2:107

canceled;

theorem :: REAL_2:108

canceled;

theorem :: REAL_2:109

for a, b being real number st a <= - b holds
( a + b <= 0 & - a >= b ) by XREAL_1:27, XREAL_1:61;

theorem :: REAL_2:110

for a, b being real number st a < - b holds
( a + b < 0 & - a > b ) by XREAL_1:28, XREAL_1:63;

theorem :: REAL_2:111

canceled;

theorem :: REAL_2:112

canceled;

theorem :: REAL_2:113

canceled;

theorem :: REAL_2:114

canceled;

theorem :: REAL_2:115

canceled;

theorem :: REAL_2:116

canceled;

theorem :: REAL_2:117

for b, a being real number st b > 0 holds
( ( a / b > 1 implies a > b ) & ( a / b < 1 implies a - 1 implies ( a > - b & b > - a ) ) & ( a / b < - 1 implies ( a < - b & b < - a ) ) ) by XREAL_1:183, XREAL_1:187, XREAL_1:195, XREAL_1:196, XREAL_1:203, XREAL_1:204;

theorem :: REAL_2:118

for b, a being real number st b > 0 holds
( ( a / b >= 1 implies a >= b ) & ( a / b <= 1 implies a <= b ) & ( a / b >= - 1 implies ( a >= - b & b >= - a ) ) & ( a / b <= - 1 implies ( a <= - b & b <= - a ) ) ) by XREAL_1:189, XREAL_1:193, XREAL_1:200, XREAL_1:199, XREAL_1:207, XREAL_1:208;

theorem :: REAL_2:119

for b, a being real number st b < 0 holds
( ( a / b > 1 implies a b ) & ( a / b > - 1 implies ( a < - b & b < - a ) ) & ( a / b < - 1 implies ( a > - b & b > - a ) ) ) by XREAL_1:184, XREAL_1:188, XREAL_1:197, XREAL_1:198, XREAL_1:205, XREAL_1:206;

theorem :: REAL_2:120

for b, a being real number st b < 0 holds
( ( a / b >= 1 implies a <= b ) & ( a / b <= 1 implies a >= b ) & ( a / b >= - 1 implies ( a <= - b & b <= - a ) ) & ( a / b <= - 1 implies ( a >= - b & b >= - a ) ) ) by XREAL_1:190, XREAL_1:194, XREAL_1:202, XREAL_1:201, XREAL_1:210, XREAL_1:209;

theorem :: REAL_2:121

for a, b being real number st ( ( a >= 0 & b >= 0 ) or ( a <= 0 & b <= 0 ) ) holds
a * b >= 0 by XREAL_1:129, XREAL_1:130;

theorem :: REAL_2:122

for a, b being real number st ( ( a < 0 & b < 0 ) or ( a > 0 & b > 0 ) ) holds
a * b > 0 by XREAL_1:131, XREAL_1:132;

theorem :: REAL_2:123

canceled;

theorem :: REAL_2:124

canceled;

theorem :: REAL_2:125

for a, b being real number st ( ( a <= 0 & b <= 0 ) or ( a >= 0 & b >= 0 ) ) holds
a / b >= 0 by XREAL_1:137, XREAL_1:138;

theorem :: REAL_2:126

for a, b being real number st ( ( a >= 0 & b < 0 ) or ( a <= 0 & b > 0 ) ) holds
a / b <= 0 by XREAL_1:139, XREAL_1:140;

theorem Th127: :: REAL_2:127

for a, b being real number st ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) holds
a / b > 0 by XREAL_1:141, XREAL_1:142;

theorem Th128: :: REAL_2:128

for a, b being real number st a < 0 & b > 0 holds
( a / b < 0 & b / a < 0 ) by XREAL_1:143, XREAL_1:144;

theorem :: REAL_2:129

for a, b being real number holds
( not a * b <= 0 or ( a >= 0 & b <= 0 ) or ( a <= 0 & b >= 0 ) ) by XREAL_1:131, XREAL_1:132;

theorem :: REAL_2:130

canceled;

theorem :: REAL_2:131

canceled;

theorem :: REAL_2:132

canceled;

theorem :: REAL_2:133

for b, a being real number st b <> 0 & a / b <= 0 & not ( b > 0 & a <= 0 ) holds
( b < 0 & a >= 0 ) by XREAL_1:141, XREAL_1:142;

theorem :: REAL_2:134

for b, a being real number st b <> 0 & a / b >= 0 & not ( b > 0 & a >= 0 ) holds
( b < 0 & a <= 0 ) by XREAL_1:143, XREAL_1:144;

theorem :: REAL_2:135

canceled;

theorem :: REAL_2:136

canceled;

theorem :: REAL_2:137

for a, b being real number st ( ( a > 1 & ( b > 1 or b >= 1 ) ) or ( a < - 1 & ( b < - 1 or b <= - 1 ) ) ) holds
a * b > 1 by XREAL_1:163, XREAL_1:166;

theorem :: REAL_2:138

for a, b being real number st ( ( a >= 1 & b >= 1 ) or ( a <= - 1 & b <= - 1 ) ) holds
a * b >= 1 by XREAL_1:161, XREAL_1:165;

theorem :: REAL_2:139

for a, b being real number st ( ( 0 <= a & a < 1 & 0 <= b & b <= 1 ) or ( 0 >= a & a > - 1 & 0 >= b & b >= - 1 ) ) holds
a * b < 1 by XREAL_1:164, XREAL_1:168;

theorem :: REAL_2:140

for a, b being real number st ( ( 0 <= a & a <= 1 & 0 <= b & b <= 1 ) or ( 0 >= a & a >= - 1 & 0 >= b & b >= - 1 ) ) holds
a * b <= 1 by XREAL_1:162, XREAL_1:167;

theorem :: REAL_2:141

canceled;

theorem :: REAL_2:142

for a, b being real number st ( ( 0 < a & a 1 ) by XREAL_1:190, XREAL_1:191, XREAL_1:192, XREAL_1:189;

theorem :: REAL_2:143

for a, b being real number st ( ( 0 < a & a <= b ) or ( b <= a & a < 0 ) ) holds
( a / b <= 1 & b / a >= 1 ) by XREAL_1:184, XREAL_1:185, XREAL_1:186, XREAL_1:183;

theorem :: REAL_2:144

for a, b being real number st ( ( a > 0 & b > 1 ) or ( a < 0 & b < 1 ) ) holds
a * b > a by XREAL_1:157, XREAL_1:158;

theorem :: REAL_2:145

for a, b being real number st ( ( a > 0 & b < 1 ) or ( a < 0 & b > 1 ) ) holds
a * b < a by XREAL_1:159, XREAL_1:160;

theorem :: REAL_2:146

for a, b being real number st ( ( a >= 0 & b >= 1 ) or ( a <= 0 & b <= 1 ) ) holds
a * b >= a by XREAL_1:153, XREAL_1:154;

theorem :: REAL_2:147

for a, b being real number st ( ( a >= 0 & b <= 1 ) or ( a <= 0 & b >= 1 ) ) holds
a * b <= a by XREAL_1:155, XREAL_1:156;

theorem :: REAL_2:148

canceled;

theorem Th149: :: REAL_2:149

for a being real number st a < 0 holds
( 1 / a < 0 & a " < 0 )

proof end;

theorem :: REAL_2:150

for a being real number holds
( ( 1 / a < 0 implies a < 0 ) & ( 1 / a > 0 implies a > 0 ) )

proof end;

theorem Th151: :: REAL_2:151

for a, b being real number st ( 0 < a or b < 0 ) & a 1 / b

proof end;

theorem Th152: :: REAL_2:152

for a, b being real number st ( 0 < a or b < 0 ) & a <= b holds
1 / a >= 1 / b

proof end;

theorem Th153: :: REAL_2:153

for a, b being real number st a < 0 & b > 0 holds
1 / a < 1 / b

proof end;

theorem :: REAL_2:154

for b, a being real number st ( 1 / b > 0 or 1 / a < 0 ) & 1 / a > 1 / b holds
a < b

proof end;

theorem :: REAL_2:155

for b, a being real number st ( 1 / b > 0 or 1 / a < 0 ) & 1 / a >= 1 / b holds
a <= b

proof end;

theorem :: REAL_2:156

for a, b being real number st 1 / a < 0 & 1 / b > 0 holds
a < b

proof end;

theorem :: REAL_2:157

for a being real number st a < - 1 holds
1 / a > - 1 by Lm1, Th151;

theorem :: REAL_2:158

for a being real number st a <= - 1 holds
1 / a >= - 1 by Lm1, Th152;

theorem :: REAL_2:159

canceled;

theorem :: REAL_2:160

canceled;

theorem :: REAL_2:161

canceled;

theorem :: REAL_2:162

canceled;

theorem :: REAL_2:163

canceled;

theorem :: REAL_2:164

for a being real number st 1 <= a holds
1 / a <= 1 by Lm1, Th152;

theorem :: REAL_2:165

for b, e, a being real number holds
( ( b <= e - a implies a <= e - b ) & ( b >= e - a implies a >= e - b ) ) by XREAL_1:13, XREAL_1:14;

theorem :: REAL_2:166

canceled;

theorem :: REAL_2:167

canceled;

theorem :: REAL_2:168

canceled;

theorem :: REAL_2:169

for a, b, e, d being real number st a - b <= e - d holds
( a + d <= e + b & a - e <= b - d & e - a >= d - b & b - a >= d - e ) by XREAL_1:18, XREAL_1:19, XREAL_1:20, XREAL_1:23;

theorem :: REAL_2:170

for a, b, e, d being real number st a - b < e - d holds
( a + d < e + b & a - e d - b & b - a > d - e ) by XREAL_1:18, XREAL_1:19, XREAL_1:20, XREAL_1:23;

theorem :: REAL_2:171

for a, b, e, d being real number holds
( ( a + b <= e - d implies a + d <= e - b ) & ( a + b >= e - d implies a + d >= e - b ) ) by XREAL_1:24, XREAL_1:25;

theorem :: REAL_2:172

canceled;

theorem :: REAL_2:173

for a, b being real number holds
( ( a < 0 implies ( a + b b ) ) & ( ( a + b b ) implies a < 0 ) ) by XREAL_1:32, XREAL_1:33, XREAL_1:45, XREAL_1:48;

theorem :: REAL_2:174

for a, b being real number holds
( ( a <= 0 implies ( a + b <= b & b - a >= b ) ) & ( ( a + b <= b or b - a >= b ) implies a <= 0 ) ) by XREAL_1:31, XREAL_1:34, XREAL_1:46, XREAL_1:47;

theorem :: REAL_2:175

canceled;

theorem :: REAL_2:176

canceled;

theorem :: REAL_2:177

for b, a, e being real number holds
( ( b > 0 & a * b <= e implies a <= e / b ) & ( b < 0 & a * b <= e implies a >= e / b ) & ( b > 0 & a * b >= e implies a >= e / b ) & ( b < 0 & a * b >= e implies a <= e / b ) ) by XREAL_1:79, XREAL_1:80, XREAL_1:81, XREAL_1:82;

theorem :: REAL_2:178

for b, a, e being real number holds
( ( b > 0 & a * b < e implies a < e / b ) & ( b < 0 & a * b < e implies a > e / b ) & ( b > 0 & a * b > e implies a > e / b ) & ( b < 0 & a * b > e implies a < e / b ) ) by XREAL_1:83, XREAL_1:84, XREAL_1:85, XREAL_1:86;

theorem :: REAL_2:179

canceled;

theorem :: REAL_2:180

canceled;

theorem :: REAL_2:181

for b, e being real number st ( for a being real number st a > 0 holds
b + a >= e or for a being real number st a < 0 holds
b - a >= e ) holds
b >= e by XREAL_1:43, XREAL_1:58;

theorem :: REAL_2:182

for b, e being real number st ( for a being real number st a > 0 holds
b - a <= e or for a being real number st a < 0 holds
b + a <= e ) holds
b <= e by XREAL_1:44, XREAL_1:59;

theorem :: REAL_2:183

for b, e being real number st ( for a being real number st a > 1 holds
b * a >= e or for a being real number st 0 < a & a < 1 holds
b / a >= e ) holds
b >= e by XREAL_1:169, XREAL_1:211;

theorem :: REAL_2:184

for b, e being real number st ( for a being real number st 0 < a & a < 1 holds
b * a <= e or for a being real number st a > 1 holds
b / a <= e ) holds
b <= e by XREAL_1:170, XREAL_1:212;

theorem :: REAL_2:185

for b, d, a, e being real number st ( ( b > 0 & d > 0 ) or ( b < 0 & d < 0 ) ) & a * d < e * b holds
a / b < e / d by XREAL_1:108, XREAL_1:109;

theorem :: REAL_2:186

for b, d, a, e being real number st ( ( b > 0 & d < 0 ) or ( b < 0 & d > 0 ) ) & a * d < e * b holds
a / b > e / d by XREAL_1:110, XREAL_1:111;

theorem :: REAL_2:187

for b, d, a, e being real number st ( ( b > 0 & d > 0 ) or ( b < 0 & d < 0 ) ) & a * d <= e * b holds
a / b <= e / d by XREAL_1:104, XREAL_1:105;

theorem :: REAL_2:188

for b, d, a, e being real number st ( ( b > 0 & d < 0 ) or ( b < 0 & d > 0 ) ) & a * d <= e * b holds
a / b >= e / d by XREAL_1:106, XREAL_1:107;

theorem :: REAL_2:189

canceled;

theorem :: REAL_2:190

canceled;

theorem :: REAL_2:191

canceled;

theorem :: REAL_2:192

canceled;

theorem :: REAL_2:193

for b, d, a, e being real number st ( ( b < 0 & d < 0 ) or ( b > 0 & d > 0 ) ) holds
( ( a * b < e / d implies a * d < e / b ) & ( a * b > e / d implies a * d > e / b ) ) by XREAL_1:112, XREAL_1:113, XREAL_1:114, XREAL_1:115;

theorem :: REAL_2:194

for b, d, a, e being real number st ( ( b < 0 & d > 0 ) or ( b > 0 & d < 0 ) ) holds
( ( a * b < e / d implies a * d > e / b ) & ( a * b > e / d implies a * d < e / b ) ) by XREAL_1:116, XREAL_1:117, XREAL_1:119, XREAL_1:118;

theorem :: REAL_2:195

canceled;

theorem :: REAL_2:196

canceled;

theorem :: REAL_2:197

canceled;

theorem :: REAL_2:198

canceled;

theorem :: REAL_2:199

for a, b, e, d being real number st ( ( 0 < a & a <= b & 0 < e & e < d ) or ( 0 > a & a >= b & 0 > e & e > d ) ) holds
a * e < b * d by XREAL_1:72, XREAL_1:100;

theorem :: REAL_2:200

for e, a, b being real number holds
( ( e > 0 & a > 0 & a e / b ) & ( e > 0 & b < 0 & a e / b ) ) by XREAL_1:78, XREAL_1:101;

theorem :: REAL_2:201

for e, a, b being real number st e >= 0 & ( a > 0 or b < 0 ) & a <= b holds
e / a >= e / b by XREAL_1:120, XREAL_1:121;

theorem :: REAL_2:202

for e, a, b being real number st e < 0 & ( a > 0 or b < 0 ) & a < b holds
e / a < e / b by XREAL_1:102, XREAL_1:103;

theorem :: REAL_2:203

for e, a, b being real number st e <= 0 & ( a > 0 or b < 0 ) & a <= b holds
e / a <= e / b by XREAL_1:122, XREAL_1:123;

theorem :: REAL_2:204

for X, Y being Subset of REAL st X <> {} & Y <> {} & ( for a, b being real number st a in X & b in Y holds
a <= b ) holds
ex d being real number st
( ( for a being real number st a in X holds
a <= d ) & ( for b being real number st b in Y holds
d <= b ) )

proof end;