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 2a = 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);

• Contents

• Back

• Next