Czes{
1}aw Byli'nski
reserve a,b,c,x,x',x1,x2,y,y',z for Real;
2 1 < x implies 1/x < 1;
3 1/2 < 1;
4 2" <1;
5 2
a = a + a;
6 a = (a-x)+x;
8 x - y = 0 implies x = y;
10 a 
a + 1;
11 x < y implies 0 < y - x;
12 x y implies 0 y - x;
13 1" = 1;
14 x/1 = x;
15 (x + x)/2 = x;
16 x< >0 implies 1/(1/x) = x;
17 y< >0 & z < > 0 implies x/(yz)=x/y/z;
18 z< >0 implies x (y/z) = (xy)/z;
19 0 x & 0 y implies 0 x y;
20 x 0 & y 0 implies 0 xy;
21 0 < x & 0 < y implies 0 < x y;
22 x < 0 & y < 0 implies 0 < x y;
23 0 x & y 0 implies xy 0 & yx 0;
24 0 < x & y < 0 implies x y < 0 & y x < 0;
25 0 xy implies 0x & 0 y or x 0 & y 0;
26 0 < xy 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[Any], Q[Any] } :
ex z st
for x,y st P[x] & Q[y] holds x z & z y
provided
ex x st P[x] and
for x,y st P[x] & Q[y] holds xy;
def 1 func min(x,y) -> Real means it = x if x y otherwise it = y;
def 2 func max(x,y) -> Real means it = x if y x otherwise it = y;
32 y x implies min(x,y) = y;
33 not y x implies min(x,y) = x;
34 min(x,y) = (x + y - |.x - y.|)/2;
35 min(x,y) x & min(y,x) x;
36 min(x,x) = x;
37 min(x,y) = min(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);
43 x y implies max(x,y) = y;
44 not x y implies max(x,y) = x;
45 max(x,y) = (x + y + |.x - y.|)/2;
46 x max(x,y) & x max(y,x);
47 max(x,x) = x;
48 max(x,y) = max(y,x);
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 & max(min(x,y),x) = x
& max(min(y,x),x) = x & max(x,min(y,x)) = x;
55 min(x,max(x,y)) = x & min(max(x,y),x) = x
& min(max(y,x),x) = x & min(x,max(y,x)) = x;
56 min(x,max(y,z)) = max(min(x,y),min(x,z))
& min(max(y,z),x) = max(min(y,x),min(z,x));
57 max(x,min(y,z)) = min(max(x,y),max(x,z))
& max(min(y,z),x) = min(max(y,x),max(z,x));
def 3 func x^2-> Element of REAL means it = x x;
58 x^2 = xx;
59 1^2 = 1;
60 0^2 = 0;
61 a^2 = (-a)^2;
62 |.a.|^2 = a^2;
63 (a + b)^2 = a^2 + 2ab + b^2;
64 (a - b)^2 = a^2 - 2ab + b^2;
65 (a + 1)^2 = a^2 + 2a + 1;
66 (a - 1)^2 = a^2 - 2a + 1;
67 (a - b)(a + b) = a^2 - b^2 & (a + b)(a - b) = a^2 - b^2;
68 (ab)^2 = a^2b^2;
69 0 < > b implies (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 0a^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 
a -> Real means 0 it & it^2 = a;
82 0 = 0;
83 1 = 1;
84 1 < 2;
85 4 = 2;
86 2 < 2;
87 0 a implies 0 a;
88 0 a implies (a)^2 = a;
89 0 a implies a^2 = a;
90 a 0 implies a^2 = -a;
91 a^2 = |.a.|;
92 0 a & a = 0 implies a = 0;
93 0< a implies 0 < a;
94 0 x & x y implies x y;
95 0 x & x < y implies x < y;
96 0 x & 0 y & x = y implies x = y;
97 0 a & 0 b implies (ab) = ab;
98 0 ab implies (ab) = |.a.||.b.|;
99 0 a & 0 < b implies (a/b) = a/b;
100 0 < a/b & b < > 0 implies (a/b) = |.a.|/|.b.|;
101 0 < a implies (1/a) = 1/a;
102 0 < a implies a/a = 1/a;
103 0 < a implies a /a = a;
104 0 a & 0 b implies (a - b)(a + b) = a - b;
105 0 a & 0 b & a < > b implies 1/(a+b) = (a - b)/(a-b);
106 0 b & b < a implies 1/(a+b) = (a - b)/(a-b);
107 0 a & 0 b & a < > b implies 1/(a-b) = (a + b)/(a-b);
108 0 b & b < a implies 1/(a-b) = (a + b)/(a-b);