B.6 REAL_1
Basic Properties of Real Numbers by Krzysztof Hryniewiecki
mode Real is Element of REAL;
reserve r for set;
reserve x,y,z,t for real number;
9 z<>0 & x*z=y*z implies x=y;
10 x + z = y + z implies x=y;
def 1 func -x -> real number means x + it = 0;
def 2 func x" -> real number means x * it = 1 if x <> 0
otherwise it = 0;
def 3 func x-y equals x+(-y);
def 4 func x/y equals x * y";
cluster x-y -> real;
cluster x/y -> real;
redefine func -x -> Real;
redefine func x" -> Real;
redefine func x-y -> Real;
redefine func x/y -> Real;
17 x+y-z=x+(y-z);
19 0-x=-x;
21 (-x)*y = -(x*y) & (-x)*y=x*(-y);
22 x<>0 iff -x<>0;
23 x*y=0 iff x=0 or y=0;
24 x"*y"=(x*y)";
25 x-0=x;
26 -0=0;
27 x-(y+z)=x-y-z;
28 x-(y-z)=x-y+z;
29 x*(y-z)=x*y - x*z;
30 x=x+z-z;
31 x<>0 implies x"<>0;
33 1/x=x" & 1/x"=x;
34 x<>0 implies x*(1/x)=1;
35 (x/y) * (z/t) =(x*z)/(y*t);
36 x-x=0;
37 x<>0 implies x/x = 1;
38 z<>0 implies x/y=(x*z)/(y*z);
39 (-x/y=(-x)/y & x/(-y)=-x/y);
40 x/z + y/z = (x+y)/z & x/z - y/z = (x-y)/z;
41 y<>0 & t<>0 implies x/y + z/t =(x*t + z*y)/(y*t)
& x/y - z/t =(x*t - z*y)/(y*t);
42 x/(y/z)=(x*z)/y;
43 y<>0 implies x/y*y=x;
44 for x,y ex z st x=y+z;
45 for x,y st y<>0 ex z st x=y*z;
49 x <= y implies x - z <= y - z;
50 x<=y iff -y<=-x;
52 x<=y & z<=0 implies y*z<=x*z;
53 x+z<=y+z implies x <= y;
54 x-z<=y-z implies x <= y;
55 x<=y & z<=t implies x+z<=y+t;
def 5 redefine pred x<y means x<=y & x<>y;
66 x < 0 iff 0 < -x;
67 x<y & z<=t implies x+z<y+t;
69 0<x implies y<y+x;
70 0<z & x<y implies x*z<y*z;
71 z<0 & x<y implies y*z<x*z;
72 0<z implies 0<z";
73 0<z implies (x<y iff x/z<y/z);
74 z<0 implies (x<y iff y/z<x/z);
75 x<y implies ex z st x<z & z<y;
76 for x ex y st x<y;
77 for x ex y st y<x;
scheme SepReal { P[Real]}:
ex X being Subset of REAL st
for x being Real holds x in X iff P[x];
81 (x/y)"=y/x;
82 (x/y)/(z/t)=(x*t)/(y*z);
83 -(x-y)=y-x;
84 x+y <= z iff x <= z-y;
86 x <= y+z iff x-y <= z;
92 (x <= y & z <= t implies x - t <= y - z) &
(x < y & z <= t or x <= y & z < t implies
x-t < y-z);
93 0 <= x*x;