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