:: REAL_2 semantic presentation

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

theorem Th1: :: REAL_2:1

canceled;

theorem Th2: :: REAL_2:2

canceled;

theorem Th3: :: REAL_2:3

canceled;

theorem Th4: :: REAL_2:4

canceled;

theorem Th5: :: REAL_2:5

canceled;

theorem Th6: :: REAL_2:6

canceled;

theorem Th7: :: REAL_2:7

canceled;

theorem Th8: :: REAL_2:8

canceled;

theorem Th9: :: REAL_2:9

canceled;

theorem Th10: :: REAL_2:10

canceled;

theorem Th11: :: REAL_2:11

canceled;

theorem Th12: :: REAL_2:12

canceled;

theorem Th13: :: REAL_2:13

canceled;

theorem Th14: :: REAL_2:14

canceled;

theorem Th15: :: REAL_2:15

canceled;

theorem Th16: :: REAL_2:16

canceled;

theorem Th17: :: REAL_2:17

canceled;

theorem Th18: :: REAL_2:18

canceled;

theorem Th19: :: REAL_2:19

canceled;

theorem Th20: :: REAL_2:20

canceled;

theorem Th21: :: REAL_2:21

canceled;

theorem Th22: :: REAL_2:22

canceled;

theorem Th23: :: REAL_2:23

canceled;

theorem Th24: :: REAL_2:24

canceled;

theorem Th25: :: REAL_2:25

canceled;

theorem Th26: :: REAL_2:26

canceled;

theorem Th27: :: REAL_2:27

canceled;

theorem Th28: :: REAL_2:28

canceled;

theorem Th29: :: REAL_2:29

canceled;

theorem Th30: :: REAL_2:30

canceled;

theorem Th31: :: REAL_2:31

canceled;

theorem Th32: :: REAL_2:32

canceled;

theorem Th33: :: REAL_2:33

canceled;

theorem Th34: :: REAL_2:34

canceled;

theorem Th35: :: REAL_2:35

canceled;

theorem Th36: :: REAL_2:36

canceled;

theorem Th37: :: REAL_2:37

canceled;

theorem Th38: :: REAL_2:38

canceled;

theorem Th39: :: REAL_2:39

canceled;

theorem Th40: :: REAL_2:40

canceled;

theorem Th41: :: REAL_2:41

canceled;

theorem Th42: :: REAL_2:42

canceled;

theorem Th43: :: REAL_2:43

canceled;

theorem Th44: :: REAL_2:44

canceled;

theorem Th45: :: REAL_2:45

canceled;

theorem Th46: :: REAL_2:46

canceled;

theorem Th47: :: REAL_2:47

canceled;

theorem Th48: :: REAL_2:48

canceled;

theorem Th49: :: REAL_2:49

canceled;

theorem Th50: :: REAL_2:50

canceled;

theorem Th51: :: REAL_2:51

canceled;

theorem Th52: :: REAL_2:52

canceled;

theorem Th53: :: REAL_2:53

canceled;

theorem Th54: :: REAL_2:54

canceled;

theorem Th55: :: REAL_2:55

canceled;

theorem Th56: :: REAL_2:56

canceled;

theorem Th57: :: REAL_2:57

canceled;

theorem Th58: :: REAL_2:58

canceled;

theorem Th59: :: REAL_2:59

canceled;

theorem Th60: :: REAL_2:60

canceled;

theorem Th61: :: REAL_2:61

canceled;

theorem Th62: :: REAL_2:62

canceled;

theorem Th63: :: REAL_2:63

for b₁, b₂ being real number ex b₃ being real number st b₁ = b₂ - b₃

proof end;

theorem Th64: :: REAL_2:64

canceled;

theorem Th65: :: REAL_2:65

canceled;

theorem Th66: :: REAL_2:66

canceled;

theorem Th67: :: REAL_2:67

canceled;

theorem Th68: :: REAL_2:68

canceled;

theorem Th69: :: REAL_2:69

canceled;

theorem Th70: :: REAL_2:70

canceled;

theorem Th71: :: REAL_2:71

canceled;

theorem Th72: :: REAL_2:72

canceled;

theorem Th73: :: REAL_2:73

canceled;

theorem Th74: :: REAL_2:74

canceled;

theorem Th75: :: REAL_2:75

canceled;

theorem Th76: :: REAL_2:76

canceled;

theorem Th77: :: REAL_2:77

canceled;

theorem Th78: :: REAL_2:78

canceled;

theorem Th79: :: REAL_2:79

canceled;

theorem Th80: :: REAL_2:80

canceled;

theorem Th81: :: REAL_2:81

canceled;

theorem Th82: :: REAL_2:82

canceled;

theorem Th83: :: REAL_2:83

canceled;

theorem Th84: :: REAL_2:84

canceled;

theorem Th85: :: REAL_2:85

canceled;

theorem Th86: :: REAL_2:86

canceled;

theorem Th87: :: REAL_2:87

canceled;

theorem Th88: :: REAL_2:88

canceled;

theorem Th89: :: REAL_2:89

canceled;

theorem Th90: :: REAL_2:90

canceled;

theorem Th91: :: REAL_2:91

canceled;

theorem Th92: :: REAL_2:92

canceled;

theorem Th93: :: REAL_2:93

canceled;

theorem Th94: :: REAL_2:94

canceled;

theorem Th95: :: REAL_2:95

canceled;

theorem Th96: :: REAL_2:96

canceled;

theorem Th97: :: REAL_2:97

canceled;

theorem Th98: :: REAL_2:98

canceled;

theorem Th99: :: REAL_2:99

canceled;

theorem Th100: :: REAL_2:100

canceled;

theorem Th101: :: REAL_2:101

canceled;

theorem Th102: :: REAL_2:102

canceled;

theorem Th103: :: REAL_2:103

canceled;

theorem Th104: :: REAL_2:104

canceled;

theorem Th105: :: REAL_2:105

for b₁, b₂, b₃ being real number st ( b₁ + (- b₂) <= 0 or b₂ - b₁ >= 0 or b₂ + (- b₁) >= 0 or b₁ - b₃ <= b₂ + (- b₃) or b₁ + (- b₃) <= b₂ - b₃ or b₃ - b₁ >= b₃ - b₂ ) holds
b₁ <= b₂

proof end;

theorem Th106: :: REAL_2:106

for b₁, b₂, b₃ being real number st ( b₁ + (- b₂) < 0 or b₂ - b₁ > 0 or (- b₁) + b₂ > 0 or b₁ - b₃ < b₂ + (- b₃) or b₁ + (- b₃) < b₂ - b₃ or b₃ - b₁ > b₃ - b₂ ) holds
b₁ < b₂

proof end;

theorem Th107: :: REAL_2:107

canceled;

theorem Th108: :: REAL_2:108

canceled;

theorem Th109: :: REAL_2:109

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

theorem Th110: :: REAL_2:110

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

theorem Th111: :: REAL_2:111

canceled;

theorem Th112: :: REAL_2:112

canceled;

theorem Th113: :: REAL_2:113

canceled;

theorem Th114: :: REAL_2:114

canceled;

theorem Th115: :: REAL_2:115

canceled;

theorem Th116: :: REAL_2:116

canceled;

theorem Th117: :: REAL_2:117

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

theorem Th118: :: REAL_2:118

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

theorem Th119: :: REAL_2:119

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

theorem Th120: :: REAL_2:120

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

theorem Th121: :: REAL_2:121

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

theorem Th122: :: REAL_2:122

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

theorem Th123: :: REAL_2:123

canceled;

theorem Th124: :: REAL_2:124

canceled;

theorem Th125: :: REAL_2:125

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

theorem Th126: :: REAL_2:126

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

theorem Th127: :: REAL_2:127

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

theorem Th128: :: REAL_2:128

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

theorem Th129: :: REAL_2:129

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

theorem Th130: :: REAL_2:130

canceled;

theorem Th131: :: REAL_2:131

canceled;

theorem Th132: :: REAL_2:132

canceled;

theorem Th133: :: REAL_2:133

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

theorem Th134: :: REAL_2:134

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

theorem Th135: :: REAL_2:135

canceled;

theorem Th136: :: REAL_2:136

canceled;

theorem Th137: :: REAL_2:137

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

theorem Th138: :: REAL_2:138

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

theorem Th139: :: REAL_2:139

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

theorem Th140: :: REAL_2:140

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

theorem Th141: :: REAL_2:141

canceled;

theorem Th142: :: REAL_2:142

for b₁, b₂ being real number st ( ( 0 < b₁ & b₁ < b₂ ) or ( b₂ < b₁ & b₁ < 0 ) ) holds
( b₁ / b₂ < 1 & b₂ / b₁ > 1 ) by XREAL_1:190, XREAL_1:191, XREAL_1:192, XREAL_1:189;

theorem Th143: :: REAL_2:143

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

theorem Th144: :: REAL_2:144

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

theorem Th145: :: REAL_2:145

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

theorem Th146: :: REAL_2:146

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

theorem Th147: :: REAL_2:147

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

theorem Th148: :: REAL_2:148

canceled;

theorem Th149: :: REAL_2:149

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

proof end;

theorem Th150: :: REAL_2:150

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

proof end;

theorem Th151: :: REAL_2:151

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

proof end;

theorem Th152: :: REAL_2:152

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

proof end;

theorem Th153: :: REAL_2:153

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

proof end;

theorem Th154: :: REAL_2:154

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

proof end;

theorem Th155: :: REAL_2:155

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

proof end;

theorem Th156: :: REAL_2:156

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

proof end;

theorem Th157: :: REAL_2:157

for b₁ being real number st b₁ < - 1 holds
1 / b₁ > - 1 by Lemma1, Th151;

theorem Th158: :: REAL_2:158

for b₁ being real number st b₁ <= - 1 holds
1 / b₁ >= - 1 by Lemma1, Th152;

theorem Th159: :: REAL_2:159

canceled;

theorem Th160: :: REAL_2:160

canceled;

theorem Th161: :: REAL_2:161

canceled;

theorem Th162: :: REAL_2:162

canceled;

theorem Th163: :: REAL_2:163

canceled;

theorem Th164: :: REAL_2:164

for b₁ being real number st 1 <= b₁ holds
1 / b₁ <= 1 by Lemma1, Th152;

theorem Th165: :: REAL_2:165

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

theorem Th166: :: REAL_2:166

canceled;

theorem Th167: :: REAL_2:167

canceled;

theorem Th168: :: REAL_2:168

canceled;

theorem Th169: :: REAL_2:169

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ <= b₃ - b₄ holds
( b₁ + b₄ <= b₃ + b₂ & b₁ - b₃ <= b₂ - b₄ & b₃ - b₁ >= b₄ - b₂ & b₂ - b₁ >= b₄ - b₃ ) by XREAL_1:18, XREAL_1:19, XREAL_1:20, XREAL_1:23;

theorem Th170: :: REAL_2:170

for b₁, b₂, b₃, b₄ being real number st b₁ - b₂ < b₃ - b₄ holds
( b₁ + b₄ < b₃ + b₂ & b₁ - b₃ < b₂ - b₄ & b₃ - b₁ > b₄ - b₂ & b₂ - b₁ > b₄ - b₃ ) by XREAL_1:18, XREAL_1:19, XREAL_1:20, XREAL_1:23;

theorem Th171: :: REAL_2:171

for b₁, b₂, b₃, b₄ being real number holds
( ( b₁ + b₂ <= b₃ - b₄ implies b₁ + b₄ <= b₃ - b₂ ) & ( b₁ + b₂ >= b₃ - b₄ implies b₁ + b₄ >= b₃ - b₂ ) ) by XREAL_1:24, XREAL_1:25;

theorem Th172: :: REAL_2:172

canceled;

theorem Th173: :: REAL_2:173

for b₁, b₂ being real number holds
( ( b₁ < 0 implies ( b₁ + b₂ < b₂ & b₂ - b₁ > b₂ ) ) & ( ( b₁ + b₂ < b₂ or b₂ - b₁ > b₂ ) implies b₁ < 0 ) ) by XREAL_1:32, XREAL_1:33, XREAL_1:45, XREAL_1:48;

theorem Th174: :: REAL_2:174

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

theorem Th175: :: REAL_2:175

canceled;

theorem Th176: :: REAL_2:176

canceled;

theorem Th177: :: REAL_2:177

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

theorem Th178: :: REAL_2:178

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

theorem Th179: :: REAL_2:179

canceled;

theorem Th180: :: REAL_2:180

canceled;

theorem Th181: :: REAL_2:181

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

theorem Th182: :: REAL_2:182

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

theorem Th183: :: REAL_2:183

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

theorem Th184: :: REAL_2:184

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

theorem Th185: :: REAL_2:185

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ > 0 & b₂ > 0 ) or ( b₁ < 0 & b₂ < 0 ) ) & b₃ * b₂ < b₄ * b₁ holds
b₃ / b₁ < b₄ / b₂ by XREAL_1:108, XREAL_1:109;

theorem Th186: :: REAL_2:186

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ > 0 & b₂ < 0 ) or ( b₁ < 0 & b₂ > 0 ) ) & b₃ * b₂ < b₄ * b₁ holds
b₃ / b₁ > b₄ / b₂ by XREAL_1:110, XREAL_1:111;

theorem Th187: :: REAL_2:187

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ > 0 & b₂ > 0 ) or ( b₁ < 0 & b₂ < 0 ) ) & b₃ * b₂ <= b₄ * b₁ holds
b₃ / b₁ <= b₄ / b₂ by XREAL_1:104, XREAL_1:105;

theorem Th188: :: REAL_2:188

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ > 0 & b₂ < 0 ) or ( b₁ < 0 & b₂ > 0 ) ) & b₃ * b₂ <= b₄ * b₁ holds
b₃ / b₁ >= b₄ / b₂ by XREAL_1:106, XREAL_1:107;

theorem Th189: :: REAL_2:189

canceled;

theorem Th190: :: REAL_2:190

canceled;

theorem Th191: :: REAL_2:191

canceled;

theorem Th192: :: REAL_2:192

canceled;

theorem Th193: :: REAL_2:193

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ < 0 & b₂ < 0 ) or ( b₁ > 0 & b₂ > 0 ) ) holds
( ( b₃ * b₁ < b₄ / b₂ implies b₃ * b₂ < b₄ / b₁ ) & ( b₃ * b₁ > b₄ / b₂ implies b₃ * b₂ > b₄ / b₁ ) ) by XREAL_1:112, XREAL_1:113, XREAL_1:114, XREAL_1:115;

theorem Th194: :: REAL_2:194

for b₁, b₂, b₃, b₄ being real number st ( ( b₁ < 0 & b₂ > 0 ) or ( b₁ > 0 & b₂ < 0 ) ) holds
( ( b₃ * b₁ < b₄ / b₂ implies b₃ * b₂ > b₄ / b₁ ) & ( b₃ * b₁ > b₄ / b₂ implies b₃ * b₂ < b₄ / b₁ ) ) by XREAL_1:116, XREAL_1:117, XREAL_1:119, XREAL_1:118;

theorem Th195: :: REAL_2:195

canceled;

theorem Th196: :: REAL_2:196

canceled;

theorem Th197: :: REAL_2:197

canceled;

theorem Th198: :: REAL_2:198

canceled;

theorem Th199: :: REAL_2:199

for b₁, b₂, b₃, b₄ being real number st ( ( 0 < b₁ & b₁ <= b₂ & 0 < b₃ & b₃ < b₄ ) or ( 0 > b₁ & b₁ >= b₂ & 0 > b₃ & b₃ > b₄ ) ) holds
b₁ * b₃ < b₂ * b₄ by XREAL_1:72, XREAL_1:100;

theorem Th200: :: REAL_2:200

for b₁, b₂, b₃ being real number holds
( ( b₁ > 0 & b₂ > 0 & b₂ < b₃ implies b₁ / b₂ > b₁ / b₃ ) & ( b₁ > 0 & b₃ < 0 & b₂ < b₃ implies b₁ / b₂ > b₁ / b₃ ) ) by XREAL_1:78, XREAL_1:101;

theorem Th201: :: REAL_2:201

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

theorem Th202: :: REAL_2:202

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

theorem Th203: :: REAL_2:203

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

theorem Th204: :: REAL_2:204

for b₁, b₂ being Subset of REAL st b₁ <> {} & b₂ <> {} & ( for b₃, b₄ being real number st b₃ in b₁ & b₄ in b₂ holds
b₃ <= b₄ ) holds
ex b₃ being real number st
( ( for b₄ being real number st b₄ in b₁ holds
b₄ <= b₃ ) & ( for b₄ being real number st b₄ in b₂ holds
b₃ <= b₄ ) )

proof end;