:: REAL_2 semantic presentation :: 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 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:42 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:47 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:48 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:49 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:50 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:51 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:52 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:53 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:54 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:55 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:56 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:57 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:58 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:59 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:60 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:61 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:62 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:63 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:64 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:65 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:66 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:67 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:68 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:69 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:70 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:71 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:72 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:73 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:74 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:75 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:76 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:77 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:78 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:79 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:80 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:81 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:82 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:83 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:84 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:85 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:86 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:87 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:88 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:89 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:90 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:91 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:92 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:93 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:94 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:95 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:96 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:97 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:98 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:99 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:100 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:101 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:102 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:103 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:104 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:105 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:106 :: Showing IDV graph ... (Click the Palm Tree again to close it)
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
theorem :: REAL_2:107 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:108 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:109 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:110 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:111 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:112 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:113 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:114 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:115 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:116 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:117 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:118 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:119 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:120 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:121 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:122 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:123 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:124 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:125 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:126 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th127: :: REAL_2:127 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th128: :: REAL_2:128 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:129 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:130 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:131 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:132 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:133 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:134 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:135 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:136 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:137 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:138 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:139 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:140 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:141 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:142 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:143 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:144 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:145 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:146 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:147 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:148 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem Th149: :: REAL_2:149 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:150 :: Showing IDV graph ... (Click the Palm Tree again to close it)
for
a being
real number holds
( ( 1
/ a < 0 implies
a < 0 ) & ( 1
/ a > 0 implies
a > 0 ) )
theorem Th151: :: REAL_2:151 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th152: :: REAL_2:152 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th153: :: REAL_2:153 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:154 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:155 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:156 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:157 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:158 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:159 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:160 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:161 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:162 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:163 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:164 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:165 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:166 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:167 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:168 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:169 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:170 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:171 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:172 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:173 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:174 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:175 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:176 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:177 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:178 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:179 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:180 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:181 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:182 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:183 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:184 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:185 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:186 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:187 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:188 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:189 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:190 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:191 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:192 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:193 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:194 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:195 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:196 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:197 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:198 :: Showing IDV graph ... (Click the Palm Tree again to close it)
canceled;
theorem :: REAL_2:199 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:200 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:201 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:202 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:203 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: REAL_2:204 :: Showing IDV graph ... (Click the Palm Tree again to close it)