Properties of the Real Numbers Prove: ALL(a):[a ε real & 1<a & a<2 => ~a ε n] That is, prove that there are no natural numbers between 1 and 2. Essential properties of the real numbers From the field axioms... 1 Set(real) & ALL(a):ALL(b):[a ε real & b ε real => a+b ε real] & ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)] & ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a] & 0 ε real & ALL(a):[a ε real => a+0=a] & ALL(a):[a ε real => _a ε real] & ALL(a):[a ε real => a+_a=0] & ALL(a):ALL(b):[a ε real & b ε real => a*b ε real] & ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)] & ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a] & ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c] & 1 ε real & ~0=1 & ALL(a):[a ε real => a*1=a] & ALL(a):[a ε real & ~a=0 => 1/a ε real] & ALL(a):[a ε real & ~a=0 => a*(1/a)=1] & ALL(a):ALL(b):[a ε real & b ε real => a-b=a+_b] & ALL(a):ALL(b):[a ε real & b ε real & ~b=0 => a/b=a*(1/b)] Premise Define: real 2 Set(real) Split, 1 Define: + function (addition) 3 ALL(a):ALL(b):[a ε real & b ε real => a+b ε real] Split, 1 + is associative 4 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)] Split, 1 + is commutative 5 ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a] Split, 1 Define: 0 6 0 ε real Split, 1 7 ALL(a):[a ε real => a+0=a] Split, 1 Define: _ function (negation) 8 ALL(a):[a ε real => _a ε real] Split, 1 9 ALL(a):[a ε real => a+_a=0] Split, 1 Define: * function (multiplication) 10 ALL(a):ALL(b):[a ε real & b ε real => a*b ε real] Split, 1 * is associative 11 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)] Split, 1 * is commutative 12 ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a] Split, 1 * is distributive over + 13 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c] Split, 1 Define: 1 14 1 ε real Split, 1 15 ~0=1 Split, 1 16 ALL(a):[a ε real => a*1=a] Split, 1 Define: 1/x function (reciprocal) 17 ALL(a):[a ε real & ~a=0 => 1/a ε real] Split, 1 18 ALL(a):[a ε real & ~a=0 => a*(1/a)=1] Split, 1 Define: - function (subtraction) 19 ALL(a):ALL(b):[a ε real & b ε real => a-b=a+_b] Split, 1 Define: / function (division) 20 ALL(a):ALL(b):[a ε real & b ε real & ~b=0 => a/b=a*(1/b)] Split, 1 Define: <= 21 ALL(a):ALL(b):[a ε real & b ε real => [a<=b <=> a<b | a=b]] Premise Define: n, the set of natural numbers 22 Set(n) & ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => a ε b]] Premise 23 Set(n) Split, 22 24 ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => a ε b]] Split, 22 Essential properties of the natural numbers(equivalent of Peano's Axioms with next(a)=a+1) 25 1 ε n & ALL(a):[a ε n => a+1 ε n] & ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b] & ALL(a):[a ε n => ~a+1=1] & ALL(s):[Set(s) & 1 ε s & ALL(a):[a ε s => a+1 ε s] => ALL(a):[a ε n => a ε s]] Premise 26 1 ε n Split, 25 27 ALL(a):[a ε n => a+1 ε n] Split, 25 28 ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b] Split, 25 29 ALL(a):[a ε n => ~a+1=1] Split, 25 30 ALL(s):[Set(s) & 1 ε s & ALL(a):[a ε s => a+1 ε s] => ALL(a):[a ε n => a ε s]] Split, 25 Prove: 1+1εn 31 1 ε n => 1+1 ε n U Spec, 27 As Required: 32 1+1 ε n Detach, 31, 26 33 1+1=1+1 Reflex 34 1+1 ε n & 1+1=1+1 Join, 32, 33 35 EXIST(a):[a ε n & 1+1=a] E Gen, 34 Previous results... Lemma 1 n is as subset of real 36 ALL(a):[a ε n => a ε real] Premise Lemma 2 a<a+1 37 ALL(a):[a ε real => a<a+1] Premise Lemma 3 a<a+b 38 ALL(a):ALL(b):[a ε n & b ε n => a<a+b] Premise Lemma 4 Transitivity of < 39 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real & a<b & b<c => a<c] Premise Lemma 5 Generalized Trichotomy Rule 40 ALL(a):ALL(b):[a ε real & b ε real => [a=b | a<b | b<a] & ~[a=b & a<b] & ~[a=b & b<a] & ~[a<b & b<a]] Premise Lemma 6 a<=b <=> ~b<a 41 ALL(a):ALL(b):[a ε real & b ε real => [a<=b <=> ~b<a]] Premise Define: 2 42 2 ε n & 1+1=2 E Spec, 35 43 2 ε n Split, 42 44 1+1=2 Split, 42 45 2 ε n => 2 ε real U Spec, 36 46 2 ε real Detach, 45, 43 Prove: x ε real & 1<x & x<2 => ~xεn Suppose... 47 x ε real & 1<x & x<2 Premise 48 x ε real Split, 47 49 1<x Split, 47 50 x<2 Split, 47 Apply definition of n for x 51 x ε n <=> x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] U Spec, 24 52 [x ε n => x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b]] & [x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] => x ε n] Iff-And, 51 53 x ε n => x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] Split, 52 54 x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] => x ε n Split, 52 55 EXIST(p):[Set(p) & ALL(a):[a ε p <=> a ε real & [a=1 | a ε n & 2<=a]]] Subset, 2 56 x ε n <=> x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] U Spec, 24 57 [x ε n => x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b]] & [x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] => x ε n] Iff-And, 56 58 x ε n => x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] Split, 57 59 x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b] => x ε n Split, 57 Define: p Prove: p is "inductive" and ~xεp 60 Set(p) & ALL(a):[a ε p <=> a ε real & [a=1 | a ε n & 2<=a]] E Spec, 55 61 Set(p) Split, 60 62 ALL(a):[a ε p <=> a ε real & [a=1 | a ε n & 2<=a]] Split, 60 63 ~[x ε real & ALL(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] => x ε b]] => ~x ε n Contra, 58 64 ~[x ε real & ALL(b):~[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b]] => ~x ε n Imply-And, 63 65 ~[x ε real & ~EXIST(b):~~[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b]] => ~x ε n Quant, 64 66 ~[x ε real & ~EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b]] => ~x ε n Rem DNeg, 65 67 ~~[~x ε real | ~~EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b]] => ~x ε n DeMorgan, 66 68 ~x ε real | ~~EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b] => ~x ε n Rem DNeg, 67 Sufficient: For ~xεn Show that p has the required properties. 69 ~x ε real | EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b] => ~x ε n Rem DNeg, 68 Prove: k ε p => k ε real Suppose... 70 k ε p Premise Apply definition of p 71 k ε p <=> k ε real & [k=1 | k ε n & 2<=k] U Spec, 62 72 [k ε p => k ε real & [k=1 | k ε n & 2<=k]] & [k ε real & [k=1 | k ε n & 2<=k] => k ε p] Iff-And, 71 73 k ε p => k ε real & [k=1 | k ε n & 2<=k] Split, 72 74 k ε real & [k=1 | k ε n & 2<=k] => k ε p Split, 72 75 k ε real & [k=1 | k ε n & 2<=k] Detach, 73, 70 76 k ε real Split, 75 As Required: 77 k ε p => k ε real Conclusion, 70 As Required: Generalizing... 78 ALL(c):[c ε p => c ε real] U Gen, 77 Prove: 1 ε p Apply definition of p for 1 79 1 ε p <=> 1 ε real & [1=1 | 1 ε n & 2<=1] U Spec, 62 80 [1 ε p => 1 ε real & [1=1 | 1 ε n & 2<=1]] & [1 ε real & [1=1 | 1 ε n & 2<=1] => 1 ε p] Iff-And, 79 81 1 ε p => 1 ε real & [1=1 | 1 ε n & 2<=1] Split, 80 Sufficient: For 1 ε p 82 1 ε real & [1=1 | 1 ε n & 2<=1] => 1 ε p Split, 80 83 1=1 Reflex 84 1=1 | 1 ε n & 2<=1 Arb Or, 83 85 1 ε real & [1=1 | 1 ε n & 2<=1] Join, 14, 84 As Required: 86 1 ε p Detach, 82, 85 Prove: k ε p => k+1 ε p Suppose... 87 k ε p Premise Apply definition of p for k 88 k ε p <=> k ε real & [k=1 | k ε n & 2<=k] U Spec, 62 89 [k ε p => k ε real & [k=1 | k ε n & 2<=k]] & [k ε real & [k=1 | k ε n & 2<=k] => k ε p] Iff-And, 88 90 k ε p => k ε real & [k=1 | k ε n & 2<=k] Split, 89 91 k ε real & [k=1 | k ε n & 2<=k] => k ε p Split, 89 92 k ε real & [k=1 | k ε n & 2<=k] Detach, 90, 87 93 k ε real Split, 92 Two cases to consider... 94 k=1 | k ε n & 2<=k Split, 92 Apply definition of p for k+1 95 k+1 ε p <=> k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1] U Spec, 62 96 [k+1 ε p => k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1]] & [k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1] => k+1 ε p] Iff-And, 95 97 k+1 ε p => k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1] Split, 96 Sufficient: k+1 ε p 98 k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1] => k+1 ε p Split, 96 99 ALL(b):[k ε real & b ε real => k+b ε real] U Spec, 3 100 k ε real & 1 ε real => k+1 ε real U Spec, 99 101 k ε real & 1 ε real Join, 93, 14 102 k+1 ε real Detach, 100, 101 Case 1 Prove: k=1 => k+1=1 | k+1 ε n & 2<=k+1 Suppose... 103 k=1 Premise 104 1 ε n => 1+1 ε n U Spec, 27 105 1+1 ε n Detach, 104, 26 As Required: 106 k+1 ε n Substitute, 103, 105 107 ALL(b):[2 ε real & b ε real => [2<=b <=> 2<b | 2=b]] U Spec, 21 108 2 ε real & 1+1 ε real => [2<=1+1 <=> 2<1+1 | 2=1+1] U Spec, 107 109 2 ε n => 2 ε real U Spec, 36 110 2 ε real Detach, 109, 43 111 ALL(b):[1 ε real & b ε real => 1+b ε real] U Spec, 3 112 1 ε real & 1 ε real => 1+1 ε real U Spec, 111 113 1 ε real & 1 ε real Join, 14, 14 114 1+1 ε real Detach, 112, 113 115 2 ε real & 1+1 ε real Join, 110, 114 116 2<=1+1 <=> 2<1+1 | 2=1+1 Detach, 108, 115 117 [2<=1+1 => 2<1+1 | 2=1+1] & [2<1+1 | 2=1+1 => 2<=1+1] Iff-And, 116 118 2<=1+1 => 2<1+1 | 2=1+1 Split, 117 119 2<1+1 | 2=1+1 => 2<=1+1 Split, 117 120 2=1+1 Sym, 44 121 2<1+1 | 2=1+1 Arb Or, 120 122 2<=1+1 Detach, 119, 121 123 2<=k+1 Substitute, 103, 122 124 k+1 ε n & 2<=k+1 Join, 106, 123 125 k+1=1 | k+1 ε n & 2<=k+1 Arb Or, 124 Case 1 As Required: 126 k=1 => k+1=1 | k+1 ε n & 2<=k+1 Conclusion, 103 Case 2 Prove: k ε n & 2<=k => k+1=1 | k+1 ε n & 2<=k+1 Suppose... 127 k ε n & 2<=k Premise 128 k ε n Split, 127 129 2<=k Split, 127 130 k ε n => k+1 ε n U Spec, 27 131 k+1 ε n Detach, 130, 128 Apply generalized trichotomy rule 132 ALL(b):[2 ε real & b ε real => [2<=b <=> 2<b | 2=b]] U Spec, 21 133 2 ε real & k ε real => [2<=k <=> 2<k | 2=k] U Spec, 132 134 2 ε real & k ε real Join, 46, 93 135 2<=k <=> 2<k | 2=k Detach, 133, 134 136 [2<=k => 2<k | 2=k] & [2<k | 2=k => 2<=k] Iff-And, 135 137 2<=k => 2<k | 2=k Split, 136 138 2<k | 2=k => 2<=k Split, 136 Two subcases to consider... 139 2<k | 2=k Detach, 137, 129 Subcase 1 Prove: 2<k => 2<=k+1 Suppose... 140 2<k Premise 141 k ε real => k<k+1 U Spec, 37 142 k<k+1 Detach, 141, 93 Apply transitivity of < 143 ALL(b):ALL(c):[2 ε real & b ε real & c ε real & 2<b & b<c => 2<c] U Spec, 39 144 ALL(c):[2 ε real & k ε real & c ε real & 2<k & k<c => 2<c] U Spec, 143 145 2 ε real & k ε real & k+1 ε real & 2<k & k<k+1 => 2<k+1 U Spec, 144 146 2 ε real & k ε real Join, 46, 93 147 2 ε real & k ε real & k+1 ε real Join, 146, 102 148 2 ε real & k ε real & k+1 ε real & 2<k Join, 147, 140 149 2 ε real & k ε real & k+1 ε real & 2<k & k<k+1 Join, 148, 142 150 2<k+1 Detach, 145, 149 151 2<k+1 | 2=k+1 Arb Or, 150 Apply definition of <= 152 ALL(b):[2 ε real & b ε real => [2<=b <=> 2<b | 2=b]] U Spec, 21 153 2 ε real & k+1 ε real => [2<=k+1 <=> 2<k+1 | 2=k+1] U Spec, 152 154 2 ε real & k+1 ε real Join, 46, 102 155 2<=k+1 <=> 2<k+1 | 2=k+1 Detach, 153, 154 156 [2<=k+1 => 2<k+1 | 2=k+1] & [2<k+1 | 2=k+1 => 2<=k+1] Iff-And, 155 157 2<=k+1 => 2<k+1 | 2=k+1 Split, 156 158 2<k+1 | 2=k+1 => 2<=k+1 Split, 156 159 2<=k+1 Detach, 158, 151 Subcase 1 As Required: 160 2<k => 2<=k+1 Conclusion, 140 Subcase 2 Prove: 2=k => 2<=k+1 Suppose... 161 2=k Premise 162 k ε real => k<k+1 U Spec, 37 163 k<k+1 Detach, 162, 93 164 2<k+1 Substitute, 161, 163 Apply definition of <= 165 ALL(b):[2 ε real & b ε real => [2<=b <=> 2<b | 2=b]] U Spec, 21 166 2 ε real & k+1 ε real => [2<=k+1 <=> 2<k+1 | 2=k+1] U Spec, 165 167 2 ε real & k+1 ε real Join, 46, 102 168 2<=k+1 <=> 2<k+1 | 2=k+1 Detach, 166, 167 169 [2<=k+1 => 2<k+1 | 2=k+1] & [2<k+1 | 2=k+1 => 2<=k+1] Iff-And, 168 170 2<=k+1 => 2<k+1 | 2=k+1 Split, 169 171 2<k+1 | 2=k+1 => 2<=k+1 Split, 169 172 2<k+1 | 2=k+1 Arb Or, 164 173 2<=k+1 Detach, 171, 172 Subcase 2 As Required: 174 2=k => 2<=k+1 Conclusion, 161 175 [2<k => 2<=k+1] & [2=k => 2<=k+1] Join, 160, 174 176 2<=k+1 Cases, 139, 175 177 k+1 ε n & 2<=k+1 Join, 131, 176 178 k+1=1 | k+1 ε n & 2<=k+1 Arb Or, 177 Case 2 As Required: 179 k ε n & 2<=k => k+1=1 | k+1 ε n & 2<=k+1 Conclusion, 127 180 [k=1 => k+1=1 | k+1 ε n & 2<=k+1] & [k ε n & 2<=k => k+1=1 | k+1 ε n & 2<=k+1] Join, 126, 179 181 k+1=1 | k+1 ε n & 2<=k+1 Cases, 94, 180 182 k+1 ε real & [k+1=1 | k+1 ε n & 2<=k+1] Join, 102, 181 183 k+1 ε p Detach, 98, 182 As Required: 184 k ε p => k+1 ε p Conclusion, 87 As Required: Generalizing... 185 ALL(c):[c ε p => c+1 ε p] U Gen, 184 Apply definition of p for x 186 x ε p <=> x ε real & [x=1 | x ε n & 2<=x] U Spec, 62 187 [x ε p => x ε real & [x=1 | x ε n & 2<=x]] & [x ε real & [x=1 | x ε n & 2<=x] => x ε p] Iff-And, 186 188 x ε p => x ε real & [x=1 | x ε n & 2<=x] Split, 187 189 x ε real & [x=1 | x ε n & 2<=x] => x ε p Split, 187 190 ~[x ε real & [x=1 | x ε n & 2<=x]] => ~x ε p Contra, 188 191 ~~[~x ε real | ~[x=1 | x ε n & 2<=x]] => ~x ε p DeMorgan, 190 192 ~x ε real | ~[x=1 | x ε n & 2<=x] => ~x ε p Rem DNeg, 191 193 ~x ε real | ~~[~x=1 & ~[x ε n & 2<=x]] => ~x ε p DeMorgan, 192 194 ~x ε real | ~x=1 & ~[x ε n & 2<=x] => ~x ε p Rem DNeg, 193 195 ~x ε real | ~x=1 & ~~[~x ε n | ~2<=x] => ~x ε p DeMorgan, 194 Sufficient: For ~x ε p 196 ~x ε real | ~x=1 & [~x ε n | ~2<=x] => ~x ε p Rem DNeg, 195 Prove: ~x=1 Apply generalized trichotomy rule 197 ALL(b):[1 ε real & b ε real => [1=b | 1<b | b<1] & ~[1=b & 1<b] & ~[1=b & b<1] & ~[1<b & b<1]] U Spec, 40 198 1 ε real & x ε real => [1=x | 1<x | x<1] & ~[1=x & 1<x] & ~[1=x & x<1] & ~[1<x & x<1] U Spec, 197 199 1 ε real & x ε real Join, 14, 48 200 [1=x | 1<x | x<1] & ~[1=x & 1<x] & ~[1=x & x<1] & ~[1<x & x<1] Detach, 198, 199 201 1=x | 1<x | x<1 Split, 200 202 ~[1=x & 1<x] Split, 200 203 ~[1=x & x<1] Split, 200 204 ~[1<x & x<1] Split, 200 205 ~~[1=x => ~1<x] Imply-And, 202 206 1=x => ~1<x Rem DNeg, 205 207 ~~1<x => ~1=x Contra, 206 208 1<x => ~1=x Rem DNeg, 207 209 ~1=x Detach, 208, 49 As Required: 210 ~x=1 Sym, 209 Prove: ~xεp Apply lemma 211 ALL(b):[2 ε real & b ε real => [2<=b <=> ~b<2]] U Spec, 41 212 2 ε real & x ε real => [2<=x <=> ~x<2] U Spec, 211 213 2 ε real & x ε real Join, 46, 48 214 2<=x <=> ~x<2 Detach, 212, 213 215 [2<=x => ~x<2] & [~x<2 => 2<=x] Iff-And, 214 216 2<=x => ~x<2 Split, 215 217 ~x<2 => 2<=x Split, 215 218 ~~x<2 => ~2<=x Contra, 216 219 x<2 => ~2<=x Rem DNeg, 218 220 ~2<=x Detach, 219, 50 221 ~x ε n | ~2<=x Arb Or, 220 222 ~x=1 & [~x ε n | ~2<=x] Join, 210, 221 223 ~x ε real | ~x=1 & [~x ε n | ~2<=x] Arb Or, 222 As Required: 224 ~x ε p Detach, 196, 223 225 Set(p) & ALL(c):[c ε p => c ε real] Join, 61, 78 226 Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p Join, 225, 86 227 Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p & ALL(c):[c ε p => c+1 ε p] Join, 226, 185 228 Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p & ALL(c):[c ε p => c+1 ε p] & ~x ε p Join, 227, 224 229 EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b] E Gen, 228 230 ~x ε real | EXIST(b):[Set(b) & ALL(c):[c ε b => c ε real] & 1 ε b & ALL(c):[c ε b => c+1 ε b] & ~x ε b] Arb Or, 229 231 ~x ε n Detach, 69, 230 As Required: 232 x ε real & 1<x & x<2 => ~x ε n Conclusion, 47 As Required: Generalizing... 233 ALL(a):[a ε real & 1<a & a<2 => ~a ε n] U Gen, 232