B.4 REAL_1


REAL_1. ABS (Digest)
Basic Properties of Real Numbers, by Krzysztof Hryniewiecki.


reserve x,y,z,t for Real; reserve a,b,c,d for Element of REAL; reserve r for Any;

9 (z< >0 & x< >y) implies xz< >yz;
10 x + z = y + z implies x=y;
11 x< >y iff x + z< >y + z;
12 (z< >0 & xz=yz) implies x=y;

def 1 func -x -> Real means x+it = 0;
def 2 func x" -> Real means xit = 1;
def 3 func x-y -> Real means it=x+(-y);
def 4 func x/y -> Real means it=xy";

13 x + -x = 0 & -x + x = 0;
14 x-y=x+ -y;
15 x< >0 implies xx" =1 & x"x=1;
16 x/y=xy" & x/y=y"x;
17 x+y-z=x+(y-z);
18 -(-x)=x;
19 0-x=-x;
21 (-x)y = -(xy) & x(-y)=-(xy) & (-x)y=x(-y);
22 x< >0 iff -x< >0;
23 xy=0 iff (x=0 or y=0);
24 x< >0 & y< >0 implies x"y"=(xy)";
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)=xy - xz & (y-z)x=yx - zx;
30 x+z=y implies (x=y-z & z=y-x);
31 x< >0 implies x"< >0;
32 x< >0 implies x""=x;
33 x< >0 implies (1/x=x" & 1/x"=x);
34 x< >0 implies x(1/x)=1 & (1/x)x=1;
35 (y< >0 & t< >0) implies (x/y)(z/t)=(xz)/(yt);
36 x-x=0;
37 x< >0 implies x/x = 1;
38 y< >0 & z< >0 implies x/y=(xz)/(yz);
39 y< >0 implies (-x/y=(-x)/y & x/(-y)=-x/y);
40 z< >0 implies (x/z + y/z = (x+y)/z ) & (x/z - y/z = (x-y)/z );
41 y< >0 & t< >0 implies (x/y +z/t =(xt + zy)/(yt)) & (x/y - z/t = (xt - zy)/(yt));
42 y< >0 & z< >0 implies x/(y/z)=(xz)/y;
43 y< >0 implies x/yy=x;
44 for x,y ex z st (x=y+z & x=z+y);
45 for x,y st y< >0 ex z st (x=yz & x=zy);
49 x <= y implies (x + z <= y + z & x - z <= y - z);
50 x<=y iff -y<=-x;
52 x<=y & z<=0 implies (yz<=xz & zy<=zx & yz<=zx & zy<=xz);
53 x <= y iff x+z<=y+z;
54 x <= y iff x-z<=y-z;
55 (x<=y & z<=t) implies x+z<=y+t;

def 5 redefine pred xy;

59 x 60 x+z 61 x< >y implies x 66 x<0 iff 0<-x;
67 ((x 69 for x,y st 0 70 0 71 z<0 & x 72 0 73 0 74 z< >0 implies (x 75 x 76 for x ex y st x 77 for x ex y st y


scheme SepReal { P[Real]}: ex X being Subset of REAL st for x holds x C X iff P[x];

81 for x,y st x< >0 & y < > 0 holds (x/y)"=y/x;
82 for x,y,z,t st y< >0 & z< >0 & t< >0 holds (x/y)/(z/t)=(xt)/(yz);
83 -(x-y)=y-x;
84 (x+y <= z iff x <= z-y);
85 (x+y <= z iff y <= z-x);
86 (x <= y+z iff x-y <= z);
87 (x <= y+z iff x-z <= y);
92 ((x<=y & z<=t) implies x-t<=y-z) & (((x 93 0 <= xx;