:: REAL_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

theorem :: REAL_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number ex e being real number st a = b - e
proof end;

theorem :: REAL_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, e being real number st ( a + (- b) < 0 or b - a > 0 or (- a) + b > 0 or a - e < b + (- e) or a + (- e) < b - e or e - a > e - b ) holds
a < b
proof end;

theorem :: REAL_2:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:183, XREAL_1:187, XREAL_1:195, XREAL_1:196, XREAL_1:203, XREAL_1:204;

theorem :: REAL_2:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:184, XREAL_1:188, XREAL_1:197, XREAL_1:198, XREAL_1:205, XREAL_1:206;

theorem :: REAL_2:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:142  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:190, XREAL_1:191, XREAL_1:192, XREAL_1:189;

theorem :: REAL_2:143  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th149: :: REAL_2:149  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a < 0 holds
( 1 / a < 0 & a " < 0 )
proof end;

theorem :: REAL_2:150  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st ( 0 < a or b < 0 ) & a < b holds
1 / a > 1 / b
proof end;

theorem Th152: :: REAL_2:152  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a < 0 & b > 0 holds
1 / a < 1 / b
proof end;

theorem :: REAL_2:154  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st 1 / a < 0 & 1 / b > 0 holds
a < b
proof end;

theorem :: REAL_2:157  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a < - 1 holds
1 / a > - 1 by Lm1, Th151;

theorem :: REAL_2:158  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a <= - 1 holds
1 / a >= - 1 by Lm1, Th152;

theorem :: REAL_2:159  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:160  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:161  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:162  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:163  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:164  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st 1 <= a holds
1 / a <= 1 by Lm1, Th152;

theorem :: REAL_2:165  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:167  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:168  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:169  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:171  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:173  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:32, XREAL_1:33, XREAL_1:45, XREAL_1:48;

theorem :: REAL_2:174  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:176  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:177  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:180  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:181  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:190  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:191  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:192  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:193  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:196  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:197  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:198  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: REAL_2:199  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e, a, b being real number holds
( ( e > 0 & a > 0 & a < b implies e / a > e / b ) & ( e > 0 & b < 0 & a < b implies e / a > e / b ) ) by XREAL_1:78, XREAL_1:101;

theorem :: REAL_2:201  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;