B.12 SQUARE_1

Some Properties of Real Numbers Operations, by Andrzej Trybulec and
Czeslaw Bylinski
reserve a,b,c,x,y,z for real number;
2 1 < x implies 1/x < 1;
5 2*a = a+ a;
6 a= (a-x)+x;
8 x - y=0 implies x = y;
ll x <  y implies 0 < y - x;
12 x <  y implies 0 <=y - x;
15 (x + x) /2 = x;
16 l/(l/x) =x;
17 x/(y*z) =x/y/z;
18 x*(y/z) = (x*y)/z;
19 0 <= x & 0 <= y implies 0 <= x*y;
20 x <= 0 & y <= 0 implies 0 <= x*y;
21 0 < x & 0 < y implies 0 < x*y;
22 x < 0 & y < 0 implies 0 < x*y;
23 0 <= x & y <= 0 implies x*y <= 0;
24 0 < x & y < 0 implies x*y < 0;
25 0 <= x*y implies 0 <= x & 0 <= y or x <= 0 & y <= 0;
26 0 < x*y implies 0 < x & 0 < y or x < 0 & y < 0;
27 0 <= a & 0 <= b implies 0 <= a/b;
29 0 < x implies y - x < y;

scheme RealContinuity { P[set], Q[set] } :
 ex z st
  for x,y st P[x] & Q[y] holds x <= z & z <= y
provided
 for x,y st P[x] & Q[y] holds x <= y;

def 1 func min(x,y) -> real number equals x if x <= y otherwise y;
def 2 func max(x,y) -> real number equals x if y <= x otherwise y;

34 min(x,y) = (x + y - abs(x - y)) / 2;
35 min(x,y) <= x;
38 min(x,y) = x or min(x,y) = y;
39 x <= y & x <= z iff x <= min(y,z);
40 min(x,min(y,z)) = min(min(x,y),z);
45 max(x,y) = (x + y + abs(x-y)) / 2;
46 x <= max(x,y);
49 max(x,y) = x or max(x,y) = y;
50 y <= x & z <= x iff max(y,z) <= x;
51 max(x,max(y,z)) = max(max(x,y),z);
53 min(x,y) + max(x,y) =x + y;
54 max(x,min(x,y)) = x;
55 min(x,max(x,y)) = x;
56 min(x,max(y,z)) = max(min(x,y),min(x,z));
57 max(x,min(y,z)) = min(max(x,y),max(x,z));

def 3 func x^2 equals x*x;

59 1^2 = 1;
60 0^2 = 0;
61 a^2 = (-a)^2;
62 (abs(a))^2 = a^2;
63 (a + b)^2 = a^2 + 2*a*b + b^2;
64 (a - b)^2 = a^2 - 2*a*b + b^2;
65 (a + 1)^2 = a^2 + 2*a + 1;
66 (a - 1)^2 = a^2 - 2*a + 1;
67 (a - b)*(a + b) = a^2 - b^2 & (a + b)*(a - b) = a^2 - b^2;
68 (a*b)^2 = a^2*b^2;
69 (a/b)^2 = a^2/b^2;
70 a^2-b^2 <> 0 implies 1/(a+b) = (a-b)/(a^2-b^2);
71 a^2-b^2 <> 0 implies 1/(a-b) = (a+b)/(a^2-b^2);
72 0 <= a^2;
73 a^2 = 0 implies a = 0;
74 0 <> a implies 0 < a^2;
75 0 < a & a < 1 implies a^2 < a;
76 1 < a implies a < a^2;
77 0 <= x & x <= y implies x^2 <= y^2;
78 0 <= x & x < y implies x^2 < y^2;

def 4 func sqrt a -> real number means 0 <= it & it^2 = a;

82 sqrt 0 = 0;
83 sqrt 1 = 1;
84 1 < sqrt 2;
85 sqrt 4 = 2;
86 sqrt 2 < 2;
89 0 <= a implies sqrt a^2 = a;
90 a <= 0 implies sqrt a^2 = -a;
91 sqrt a^2 = abs(a);
92 0 <= a & sqrt a = 0 implies a = 0;
93 0 < a implies 0 < sqrt a;
94 0 <= x & x <= y implies sqrt x <= sqrt y;
95 0 <= x & x < y implies sqrt x < sqrt y;
96 0 <= x & 0 <= y & sqrt x = sqrt y implies x = y;
97 0 <= a & 0 <= b implies sqrt (a*b) = sqrt a * sqrt b;
98 0 <= a*b implies sqrt (a*b) = sqrt abs(a)*sqrt abs(b);
99 0 <= a & 0 <= b implies sqrt (a/b) = sqrt a/sqrt b;
100 0 < a/b implies sqrt (a/b) = sqrt abs(a) / sqrt abs(b);
101 0 < a implies sqrt (1/a) = 1/sqrt a;
102 0 < a implies sqrt a/a = 1/sqrt a;
103 0 < a implies a /sqrt a = sqrt a;
104 0 <= a & 0 <= b
       implies (sqrt a - sqrt b)*(sqrt a + sqrt b) = a - b;
105 0 <= a & 0 <= b & a <>b
       implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b);
106 0 <= b & b < a
       implies 1/(sqrt a+sqrt b) = (sqrt a - sqrt b)/(a-b);
107 0 <= a & 0 <= b & a <> b
       implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b);
lO8 0 <= b & b < a
       implies 1/(sqrt a-sqrt b) = (sqrt a + sqrt b)/(a-b);