B.12 REAL_2

REAL_2.ABS (Digest)
Equalities and Inequalities in Real Numbers. Continuation of Real_1,
by Andrzej Kondracki.

reserve a,b,d,e for Real;

1 a+b=b or b-a=b implies a=0;
2 a-b=0 or a+-b=0 or -a=-b or a-e=b-e or a-e=b+-e

or e-a=e-b or e-a=e+-b implies a=b;
3 a=-b implies a+b=0 & -a=b;
4 a+b=0 implies a=-b;
5 -a-b=b-a;
6 -(a+b)=-a+-b & -(a+b)=-b-a & -(a+b)=-a-b;
8 -(a-b)=-a+b & -(a-b)=b-a;
9 -(-a+b)=a-b & -(-a+b)=a+-b;
10 a+b=-(-a-b) &a+b=-(-b-a) & a+b=-(-a+-b)
& a+b=a--b & a+b=b--a;
11 a+b=e implies a=e-b & a=e+-b;
12 a=e-b or a=e+-b implies a+b=e & b=e-a;
13 a+b=e+d implies a-e=d-b;
14 a-e=d-b implies a+b=e+d;
15 a-b=e-d implies a-e=b-d;
16 a+b=e-d implies a+d=e-b;
17 a=a+(b-b) & a=a+b-b & a=a+(b+-b) & a=a+b+-b
& a=a-(b-b) & a=a-b+b & a=a-(b+-b) & a=a+-b+b
& a=b-(b-a) & a=-b-(-a-b) & a=-b-(-b-a);
18 a-(b-e)=a+(e-b) & a+(b-e)=a+b-e;
20 a+(-b-e)=a-b-e & a-(-b-e)=a+b+e;
22 a+b-e=a-e+b & a+b-e=b-e+a & a+b-e=-e+a+b;
23 a-b+e=e-b+a & a-b+e=-b+a+e & a-b+e=-b+e+a;
24 a-b-e=a-e-b & a-b-e=-b+a-e & a-b-e=-b-e+a
& a-b-e=-e+a-b & a-b-e=-e-b+a;
25 -a+b-e=-e+b-a & -a+b-e=-e-a+b;
26 -a-b-e=-a-e-b & -a-b-e=-b-e-a & -a-b-e=-e-a-b & -a-b-e=-e-b-a;
27 -(a+b+e)=-a-b-e & -(a+b-e)=-a-b+e & -(a-b+e)=-a+b-e & -(-a+b+e)=a-b-e
& -(a-b-e)=-a+b+e & -(-a+b-e)=a-b+e & -(-a-b+e)=a+b-e & -(-a-b-e)=a+b+e;
28 a+e=(a+b)+(e-b) & a+e=(b+a)+(e-b) & a+e=(a-b)+(e+b) & a+e=(a-b)+(b+e)
& a+e=(a+b)-(b-e) & a+e=(b+a)-(b-e);
29 a-e=(a-b)-(e-b) & a-e=(a-b)+(b-e) & a-e=(a+b)-(e+b);
30 b< >0 implies (a/b=1 or ab"=1 implies a=b);
31 e< >0 & a/e=b/e implies a=b;
33 a< >0 & b< >0 implies (a"=b" or 1/a=1/b or 1/a=b" implies a=b);
34 b< >0 & a/b=-1 implies a=-b & b=-a;
35 ab=1 implies a=1/b & a=b";
36 b< >0 implies (a=1/b or a=b" implies ab=1 & a"=b & b=1/a);
37 b< >0 & ab=b implies a=1;
38 b< >0 & ab=-b implies a=-1;
39 a< >0 & b< >0 & b/a=b implies a=1;
40 a< >0 & b< >0 & b/a=-b implies a=-1;
41 a< >0 implies 1/a< >0;
42 a< >0 & b< >0 implies ab"< > & a/b< >0 & a"b"< >0 & 1/(ab)< >0;
43 1/1=1 & 1"=1 & 1/(-1)=-1 & (-1)"=-1 & (-1)(-1)=1;
44 a/1=a & a1"=a;
45 a< >0 implies (-a)/a=-1 & a/(-a)=-1 & (-a)"=-a";
46 a< >0 implies (a=a" or a=1/a implies a=1 or a=-1);
47 a< >0 & b< >0 implies (ab")"=a"b & (a"b")"=ab;
48 a< >0 & b< >0 implies 1/(a/b)=b/a & (a/b)"=b/a;
49 (-a)b=-ba & (-a)b=(-b)a & (-a)(-b)=ab & -a(-b)=ab& -(-a)b=ab;
50 b< >0 implies (a/b=0 iff a=0); 51 a< >0 & b< >0 implies (1/a)(1/b)=1/(ab);
53 e< >0 & d< >0 implies (a/e)(b/d)=(ba)/(ed) & (a/e)(b/d)=a/d)(b/e);
55 b< >0 & e< >0 implies a/b=(ae)/(eb) & a/b=(a/e)/(b/e)
&a/b=a/(be)e & a/b=e(a/e/b)
& a/b=a/e(e/b);
56 b< >0 implies a(1/b)=a/b;
57 b< >0 implies a/(1/b)=-ab;
58 b< >0 implies -a/(-b)=a/b & -(-a)/b=a/b & (-a)/(-b)=a/b & (-a)/b=a/(-b);
61 b< >0 & e< >0 implies a/(b/e)=ea)/b & a/(b/e)=a(e/b) & a/(b/e)=e/ba
& a/(b/e)=e(a/b) & a/(b/e)=a/be;
62 b< >0 implies a=a(b/b) & a=ab/b & a=ab(1/b)
& a=a/(b/b) & a=a/bb & a=a/(b(1/b)) & a=a(1/b)b;
63 for a,b ex e st a=-b-e;
64 for a,b st a< >0 & b< >0 ex e st a=b/e;
65 b< >0 implies a/b+e=(a+be)/b;
66 b< >0 implies a/b-e=(a-eb)/b & e-a/b=(eb-a)/b;
67 b< >0 & e< >0 implies a/b/e=a/(be) & a/b/e=a/e/b & a/b/e=1/b(a/e)
& a/b/e=1/e(a/b) & 1/e(a/b)=a/(be);
70 e< >0 & d< >0 implies (ab)/(ed)=(a/eb)/d;
71 (-1)a=-a & (-a)(-1)=a & -a=a/(-1) & a=(-a)/(-1);
72 e< >0 & ea=b implies a=b/e;
73 e< >0 & a=b/e implies ae=b;
74 a< >0 & e< >0 & a=b/e implies e=b/a;
75 e< >0 & d< >0 & ae=bd implies a/d=b/e;
76 e< >0 & d< >0 & a/d=b/e implies ae=bd;
77 e< >0 & d< >0 & ae=b/d implies ad=b/e;
78 b< >0 implies ae=ab(e/b);
79 b< >0 & e< >0 implies ae=ab/(b/e);
80 b< >0 implies a/be=e/ba & a/be=1/bae & a/be=1/bea;
81 (-a)(-b)=ab & (-a)(-b)=ba;
82 b< >0 & d< >0 & b< >d & a/b=e/d implies a/b=(a-e)/(b-d);
83 b< >0 & d< >0 & b< >-d & a/b=e/d implies a/b=(a+e)/(b+d);
85 e(a-b)=ae-eb & (a-b)e=(b-a)(-e) & (a-b)e=-(b-a)e;
86 a< >0 implies (1/a=1 or a"=1 implies a=1);
87 a< >0 implies (1/a=-1 or a"=-1 implies a=-1);
88 2a=a+a & 3a=a+a+a & 4a=a+a+a+a;
89 (a+a)/2=a & (a+a+a)/3=a & (a+a+a+a)/4=a & (a+a)/4=a/2;
90 a/2+a/2=a & a/3+a/3+a/3=a & a/4+a/4+a/4+a/4=a & a/4+a/4=a/2;
91 b< >0 implies a/(2b)+a/(2b)=a/b & a/(3b)+a/(3b)=a/b; 92 e< >0 implies a+b=e(a/e+b/e);
93 e< >0 implies a-b=e(a/e-b/e);
94 e< >0 implies a+b=(ae+be)/e;
95 e< >0 implies a-b=(ae-be)/e;
96 a< >0 implies a+b=a(1+b/a);
97 a< >0 implies a-b=a(1-b/a);
98 (a-b)(e-d)=(b-a)(d-e);
99 (a+b+e)d=ad+bd+ed & (a+b-e)d=ad+bd-ed
& (a-b+e)d=ad-bd+ed & (a-b-e)d=ad-bd-ed;
100 d< >0 implies (a+b+e)/d=a/d+b/d+e/d & (a+b-e)/d=a/d+b/d-e/d
& (a-b+e)/d=a/d-b/d+e/d & (a-b-e)/d=a/d-b/d-e/d;
101 (a+b)(e+d)=ae+ad+be+bd & (a+b)(e-d)=ae-ad+be-bd
& (a-b)(e+d)=ae+ad-be-bd & (a-b)(e-d)=ae-ad-be+bd;
105 (a-b0 or a+-b0 or -a-b or b-a0 or b+-a0
or a-eb+-e or a+-eb-e or e-ae-b) implies ab;
106 (a-b<0 or a+-b<0 or -a>-b or b-a>0 or -a+b>0
or a-ee-b) implies a 107 ab implies a-b0 & a+-b0 & -b+a0
& -a-b & e-ae-b;
108 a < b implies a-b<0 & a+-b<0 & -b+a<0
& b-a>0 & b+-a>0 & -a+b>0
& -a>-b & e-a>e-b;
109 a-b implies a+b0 & -ab;
110 a<-b implies a+b<0 & -a>b;
111 -ab implies a+b0 & a-b;
112 -b0 & b>-a;
113 (a+b0 or b+a0) implies a-b;
114 (a+b<0 or b+a<0) implies a<-b;
115 (a+b0 or b+a0) implies a-b;
116 (a+b>0 or b+a>0) implies a>-b;
117 b>0 implies (a/b>1 implies a>b) & (a/b<1 implies a
& (a/b>-1 implies a>-b & b>-a) & (a/b<-1 implies a<-b & b<-a);
118 b>0 implies (a/b1 implies ab) & (a/b1 implies ab)
& (a/b-1 implies a-b & b-a) & (a/b-1 implies a-b & b-a);
119 b< >0 implies (a/b>1 implies ab)
& (a/b>-1 implies a<-b & b<-a) & (a/b<-1 implies a>-b & b>-a);
120 b< >0 implies (a/b1 implies ab) & (a/b1 implies ab)
& (a/b-1 implies a-b & b-a) & (a/b-1 implies a-b & b-a);
121 (a0 or a>0) & (b0 or b>0) or (a0 or a<0) & (b0 or b<0)
implies ab0;
122 a<0 & b<0 or a>0 & b>0 implies ab>0;
123 (a0 or a>0) & (b0 or b<0) or (a0 or a<0) & (b0 or b>0)
implies ab0;
125 a0 & b<0 or a0 & b>0 implies a/b0;
126 a0 & b<0 or a0 & b>0 implies a/b0;
127 a>0 & b>0 or a<0 & b<0 implies a/b>0;
128 a<0 & b>9 implies a/b<0 & b/a<0;
129 ab0 implies a0 & b0 or a0 & b0;
132 ab<0 implies a>0 & b<0 or a<0 & b>0;
133 b< >0 & a/b0 implies b>0 & a0 or b<0 & a0;
134 b< >0 & a/b0 implies b>0 & a0 or b<0 & a0;
135 b< >0 & a/b<0 implies b<0 & a>0 or b>0 & a<0;
136 b< >0 & a/b>0 implies b>0 & a>0 or b<0 & a<0;
137 a>1 & (b>1 or b1) or a<-1 & (b<-1 or b-1)
implies ab>1 & ba>1;
138 a1 & b1 or a-1 & b-1 implies ab1;
139 (0a) & a<1 & (0 < b or 0b) & (b<1 or b1)
or (0>a or 0a) & a>-1 & (0>b or 0b) & (b>-1 or b-1)
implies ab<1;
140 0a & a1 & 0b & b1 or 0a & a-1 & 0b & b-1
implies ab1;
141 e<0 & ab or e>0 & ab implies a/eb/e;
142 (01;
143 (0b or ba & a<0) implies a/b1 & b/a1;
144 a>0 & b>1 or a<0 & b<1 implies ab>a;
145 a>0 & b<1 or a<0 & b>1 implies ab 146 (a>0 or a0) & (b>1 or b1) or (a<0 or a0) & (b<1 or b1)
implies aba;
147 (a>0 or a0) & (b<1 or b1) or (a<0 or a0) & (b>1 or b1)
implies aba;
148 (a>0 iff -a<0) & (a0 iff -a0) & (a0 iff -a0);
149 (a<0 implies 1/a<0 & a"<0) & (a>0 implies 1/a>0);
150 a< >0 implies (1/a<0 implies a<0) & (1/a>0 implies a>0);
151 (01/b;
152 (0b implies 1/a1/b;
153 a<0 & b>0 implies 1/a<1/b;
154 a< >0 & b< >0 & (1/b>0 or 1/a<0) & 1/a>1/b implies a 155 a< >0 & b< >0 & (1/b>0 or 1/a<0) & 1/a1/b implies ab;
156 a< >0 & b< >0 & 1/a<0 & 1/b>0 implies a 157 a<-1 implies 0>1/a & 1/a>-1;
158 a-1 implies 0>1/a & 1/a-1;
159 -1 160 -1a & a<0 implies 1/a -1;
161 01;
162 01 implies 1/a1;
163 1 164 1a implies 0<1/a & 1/a1;
165 (be-a implies ae-b) & (be-a implies ae-b);
167 a+be+d implies a-ed-b;
168 a+b 169 a-be-d implies a+de+b & a-eb-d & e-ad-b & b-ad-e;
170 a-bd-b & b-a>d-e;
171 (a+be-d implies a+de-b) & (a+be-d implies a+de-b);
173 (a<0 implies a+b < b & b-a b implies a<0);
174 (a0 implies a+bb & b-ab) & (a+bb or b-ab implies a0);
177 (b>0 & abe implies ae/b)
& (b<0 & abe implies ae/b)
& (b>0 & abe implies ae/b)
& (b<0 & abe implies ae/b);
178 (b>0 & ab
& (b<0 & abe/b)
& (b>0 & ab>e implies a>e/b)
& (b<0 & ab>e implies a 181 (for a st a>0 holds b+ae)
or (for a st a<0 holds b+ae) implies be;
182 (for a st a>0 holds b-ae)
or (for a st a<0 holds b+ae) implies be;
183 (for a st a>1 holds bae)
or (for a st 0e) implies be;
184 (for a st 0ae)
or (for a st a>1 holds b/ae) implies be;
185 (b>0 & d>0 or b<0 & d<0) & adb implies a/b 186 (b>0 & d<0 or b<0 & d>0) & adb implies a/b>e/d;
187 (b>0 & d>0 or b<0 & d<0) & adeb implies a/be/d;
188 (b>0 & d<0 or b<0 & d>0) & adeb implies a/be/d;
193 b<0 & d<0 or b>0 & d>0
implies (abdb>e/d implies ad>e/b);
194 b<0 & d>0 or b>0 & d<0
implies (ab< e/d implies a d >e/b) & (a b > e/d implies ad < e/b);
197 (0a) & (a < b or ab) & (0e) & ed implies aebd;
198 (0>a or 0a) & (a>b or ab) & (0>e or 0e) & ed implies aebd;
199 0b or aa & (ab or a>b) & 0>e & e>d
implies aed;
200 e>0 & (a>0 or b<0) & a < b implies e/a>e/b;
201 (e>0 or e0) & (a>0 or b<0) & ab implies e/ae/b;
202 e<0 & (a>0 or b<0) & a < b implies e/a 203 (e<0 or e0) & (a>0 or b<0) & ab implies e/ae/b;

reserve x,y for Any;


204 for X,Y being Subset of REAL st X< > & Y< >

     & for a,b st aCX & bCY holds ab

     holds ex d st

       (for a st aCX holds ad)

        & for b st bCY holds db;