B.13 REAL_2

Equalities and Inequalities in Real Numbers. Continuation of Real_1 by Andrzej Kondracki

reserve a,b,d,e for real number;

1 b-a=b implies a=0;
2 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;
5 -a-b=-b-a;
6 -(a+b)=-a+-b & -(a+b)=-b-a;
8 -(a-b)=-a+b;
9 -(-a+b)=a-b & -(-a+b)=a+-b;
10 a+b=-(-a-b) & a+b=-(-a+-b) & a+b=a--b;
ll a=a+b+-b;
12 b=a-(a-b);
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=-b-(-a-b);
18 a-(b-e)=a+(e-b);
20 a+(-b-e)=a-b-e & a-(-b-e)=a+b+e;
22 a+b-e=a-e+b & a+b-e=-e+a+b;
23 a-b+e=e-b+a & a-b+e=-b+e+a;
24 a-b-e=a-e-b & 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=(a+b)-(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 a*b"=1 implies a=b);
31 e<>0 & a/e=b/e implies a=b;
33 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 a*b=l implies a=l/b & a=b"
36 b<>0 implies (a=l/b or a=b" implies a*b=l & a"=b & b=l/a);
37 b<>0 & a*b=b implies a=1;
38 b<>0 & a*b=-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 a*b"<>0 & a/b<>0 & a"*b"<>0 & 1/(a*b)<>0;
45 (-a)"=-a" & (a<>0 implies (-a)/a=-1 & a/(-a)=-1);
46 a<>0 implies (a=a" or a=1/a implies a=1 or a=-1);
47 (a*b")"=a"*b & (a"*b")"=a*b;
48 1/(a/b)=b/a & (a/b)"=b/a;
49 (-a)*(-b)=a*b & -a*(-b)=a*b & -(-a)*b=a*b;
50 b<>0 implies (a/b=0 iff a=0);
51 (1/a)*(1/b)=1/(a*b);
53 (a/e)*(b/d)=(a/d)*(b/e);
55 e<>0 implies a/b=(a/e)/(b/e)
      & a/b=a/(b*e)*e & a/b=e*(a/e/b) & a/b=a/e*(e/b);
56 a*(1/b)=a/b;
57 a/(1/b)=a*b;
58 -a/(-b)=a/b & -(-a)/b =a/b & (-a)/(-b)=a/b & (-a)/b=a/(-b);
61 a/(b/e)=a*(e/b) & a/(b/e)=e/b*a & a/(b/e)=e*(a/b) & a/(b/e)=a/b*e;
62 b<>0 implies a=a*(b/b) & a=a*b/b & a=a*b*(1/b)
      & a=a/(b/b) & a=a/(b*(1/b)) & a=a*(1/b*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<>O implies a/b+e=(a+b*e)/b;
66 b<>0 implies a/b-e=(a-e*b)/b & e-a/b=(e*b-a)/b;
67 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/(b*e);
70 (a*b)/(e*d)=(a/e*b)/d;
71 (-1)*a=-a & (-a)*(-l)=a & -a=a/(-l) & a=(-a)/(-l);
74 a<>0 & e<>0 & a=b/e implies e=b/a;
75 e<>0 & d<>0 & a*e=b*d implies a/d=b/e;
76 e<>0 & d<>0 & a/d=b/e implies a*e=b*d;
77 e<>0 & d<>0 & a*e=b/d implies a*d=b/e;
78 b<>0 implies a*e=a*b (e/b);
79 b<>0 & e<>0 implies a*e=a*b/(b/e);
80 a/b*e=e/b*a & a/b*e=1/b*a*e & a/b*e=1/b*e*a;
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 (a-b)*e=(b-a)*(-e) & (a-b)*e=-(b-a)*e;
88 3*a=a+a+a & 4*a=a+a+a+a;
89 (a+a+a)/3=a & (a+a+a+a)/4=a & (a+a)/4=a/2;
90 a/4+a/4+a/4+a/4=a;
91 a/(2*b)+a/(2*b)=a/b & a/(3*b)+a/(3*b)+a/(3*b)=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=(a*e+b*e)/e;
95 e<>0 implies a-b=(a*e-b*e)/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=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;
100 (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)=a*e+a*d+b*e+b*d & (a+b)*(e-d)=a*e-a*d+b*e-b*d
      & (a-b)*(e+d)=a*e+a*d-b*e-b*d & (a-b)*(e-d)=a*e-a*d-b*e+b*d;
105 (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) implies a<=b;
106 (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) implies a<b;
109 a<=-b implies a+b<=0 & -a>=b;
110 a<-b implies a+b<0 & -a>b;
111 -a<=b implies a+b>=0;
112 -b<a implies a+b>0;
117 b>0 implies (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);
118 b>0 implies (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);
119 b<0 implies (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);
120 b<0 implies (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);
121 a>=0 & b>=0 or a<=0 & b<=0 implies a*b>=0;
122 a<0 & b<0 or a>0 & b>0 implies a*b>0;
123 a>=0 & b<=0 or a<=0 & b>=0 implies a*b<=0;
125 a<=0 & b<0 or a>=0 & b>0 implies a/b>=0;
126 a>=0 & b<0 or a<=0 & b>0 implies a/b<=0;
127 a>0 & b>0 or a<0 & b<0 implies a/b>0;
128 a<0 & b>0 implies a/b<0 & b/a<0;
129 a*b<=0 implies a>=0 & b<=0 or a<=0 & b>=0;
132 a*b<0 implies a>0 & b<0 or a<0 & b>0;
133 b<>0 & a/b<=0 implies b>0 & a<=0 or b<0 & a>=0;
134 b<>0 & a/b>=0 implies b>0 & a>=0 or b<0 & a<=0;
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 a<=-1 & b<=-1 implies a*b>=1;
138 a>=1 & b>=1 or a<=-1 & b<=-1 implies a*b>=1;
139 0<=a & a<1 & 0<=b & b<=1 or 0>=a & a>-1 & 0>=b & b>=-1
      implies a*b<1;
140 0<=a & a<=1 & 0<=b & b<=1 or 0>=a & a>=-1 & 0>=b & b>=-1
     implies a*b<=1;
142 0<a & a<b or b<a & a<0 implies a/b<1 & b/a>1;
143 0<a & a<=b or b<=a & a<0 implies a/b<=1 & b/a>=1;
144 a>0 & b>1 or a<0 & b<1 implies a*b>a;
145 a>0 & b<1 or a<0 & b>1 implies a*b<a;
146 a>=0 & b>=1 or a<=0 & b<=1 implies a*b>=a;
147 a>=0 & b<=1 or a<=0 & b>=1 implies a*b<=a;
149 a<0 implies 1/a<0 & a"<0;
150 (1/a<0 implies a<0) & (1/a>0 implies a>0);
151 (0<a or b<0) & a<b implies 1/a>1/b;
152 (0<a or b<0) & a<=b implies 1/a>=1/b;
153 a<0 & b>0 implies 1/a<1/b;
154 (1/b>0 or 1/a<0) & 1/a>1/b implies a<b;
155 (1/b>0 or 1/a<0) & 1/a>=1/b implies a<=b;
156 1/a<0 & 1/b>0 implies a<b;
157 a<-1 implies 1/a>-1;
158 a<=-1 implies 1/a>=-1;
164 1<=a implies 1/a<=1;
165 (b<=e-a implies a<=e-b) & (b>=e-a implies a>=e-b);
167 a+b<e+d implies a-e<d-b;
168 a+b<e+d implies a-e<d-b;
169 a-b<e-d implies a+d<e+b & a-e<b-d & e-a<d-b & b-a<d-e;
170 a-b<e-d implies a+d<e+b & a-e<b-d & e-a<d-b & b-a<d-e;
171 (a+b<e-d implies a+d<e-b) & (a+b<e-d implies a+d<e-b);
173 (a<0 implies a+b<b & b-a<b) & (a+b<b or b-a<b implies a<0);
174 (a<=0 implies a+b<=b & b-a>=b) & (a+b<=b or b-a>=b implies a<=0);
177 (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);
178 (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);
181 (for a st a>0 holds b+a>=e)
        or (for a st a<0 holds b-a>=e) implies b>=e;
182 (for a st a>0 holds b-a<=e)
        or (for a st a<0 holds b+a<=e) implies b<=e;
183 (for a st a>1 holds b*a>=e)
        or (for a st 0<a & a<1 holds b/a>=e) implies b>=e;
184 (for a st 0<a & a<1 holds b*a<=e)
        or (for a st a>1 holds b/a<=e) implies b<=e;
185 (b>0 & d>0 or b<0 & d<0) & a*d<e*b implies a/b<e/d;
186 (b>0 & d<0 or b<0 & d>0) & a*d<e*b implies a/b>e/d;
187 (b>0 & d>0 or b<0 & d<0) & a*d<=e*b implies a/b<=e/d;
188 (b>0 & d<0 or b<0 & d>0) & a*d<=e*b implies a/b>=e/d;
193 b<0 & d<0 or b>0 & d>0 implies
      (a*b<e/d implies a*d<e/b) & (a*b>e/d implies a*d>e/b);
194 b<0 & d>0 or b>0 & d<0 implies
      (a*b<e/d implies a*d>e/b) & (a*b>e/d implies a*d<e/b);
197 (0<a or 0<=a) & (a<b or a<=b) & (0<e or 0<=e) & e<=d
       implies a*e<=b*d;
198 0>=a & a>=b & 0>=e & e>=d implies a*e<=b*d;
199 0<a & a<=b & 0<e & e<d or 0>a & a>=b & 0>e & e>d implies a*e<b*d;
200 (e>0 & a>0 & a<b implies e/a>e/b) &
     (e>0 & b<0 & a<b implies e/a>e/b);
201 e>=0 & (a>0 or b<0) & a<=b implies e/a>=e/b;
202 e<0 & (a>0 or b<0) & a<b implies e/a<e/b;
203 e<=0 & (a>0 or b<0) & a<=b implies e/a<=e/b;
204 for X,Y being Subset of REAL st
      X<>{} & Y<>{} & for a,b st a in X & b in Y holds a<=b
      holds ex d st (for a st a in X holds a<=d) & for b st b in Y
      holds d<=b;