Irreflexivity of Less Than

Introduction
------------

Required to prove: ALL(a):[a ε n => ~a<a]


Axioms for n, 1, +
------------------

1	Set(n)
	Axiom

2	1 ε n
	Axiom

Define: +

3	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	Axiom

4	ALL(a):[a ε n => ~a+1=1]
	Axiom

5	ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
	Axiom

6	ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
	Axiom

7	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a] => ALL(b):[b ε n => b ε a]]
	Axiom


Definitions
-----------

Define: <

8	ALL(a):ALL(b):[a ε n & b ε n => [a<b <=> EXIST(c):[c ε n & a+c=b]]]
	Definition


Previous Results
----------------

Associativity of +

9	ALL(a):ALL(b):ALL(c):[a ε n & b ε n & c ε n => a+b+c=a+(b+c)]
	Axiom

Commutativity of +

10	ALL(a):ALL(b):[a ε n & b ε n => a+b=b+a]
	Axiom


Proof
-----

Apply Induction shortcut

11	ALL(b):[b ε n => ~1+b=1]
	& ALL(k):[k ε n & ALL(b):[b ε n => ~k+b=k] => ALL(b):[b ε n => ~k+1+b=k+1]]
	=> ALL(k):[k ε n => ALL(b):[b ε n => ~k+b=k]]
	Induction

	
	Base Step
	---------
	
	Prove: ALL(b):[b ε n => ~1+b=1]
	
	Suppose...

	12	x ε n
		Premise

	Apply axiom

	13	x ε n => ~x+1=1
		U Spec, 4

	14	~x+1=1
		Detach, 13, 12

	Apply commutativity of +

	15	ALL(b):[x ε n & b ε n => x+b=b+x]
		U Spec, 10

	16	x ε n & 1 ε n => x+1=1+x
		U Spec, 15

	17	x ε n & 1 ε n
		Join, 12, 2

	18	x+1=1+x
		Detach, 16, 17

	19	~1+x=1
		Substitute, 18, 14

Base Step
---------

As Required:

20	ALL(b):[b ε n => ~1+b=1]
	Conclusion, 12
	
	Inductive Step
	--------------
	
	Prove: ALL(k):[k ε n & ALL(b):[b ε n => ~k+b=k]
	       => ALL(b):[b ε n => ~k+1+b=k+1]]
	
	
	Suppose...

	21	x ε n & ALL(b):[b ε n => ~x+b=x]
		Premise

	22	x ε n
		Split, 21

	23	ALL(b):[b ε n => ~x+b=x]
		Split, 21

		
		Prove: ALL(b):[b ε n => ~x+1+b=x+1]
		
		Suppose...

		24	y ε n
			Premise

			
			Prove: ~x+1+y=x+1
			
			Suppose to the contrary...

			25	x+1+y=x+1
				Premise

			Apply premise

			26	y ε n => ~x+y=x
				U Spec, 23

			27	~x+y=x
				Detach, 26, 24

			Apply associativity

			28	ALL(b):ALL(c):[x ε n & b ε n & c ε n => x+b+c=x+(b+c)]
				U Spec, 9

			29	ALL(c):[x ε n & 1 ε n & c ε n => x+1+c=x+(1+c)]
				U Spec, 28

			30	x ε n & 1 ε n & y ε n => x+1+y=x+(1+y)
				U Spec, 29

			31	x ε n & 1 ε n
				Join, 22, 2

			32	x ε n & 1 ε n & y ε n
				Join, 31, 24

			33	x+1+y=x+(1+y)
				Detach, 30, 32

			34	x+(1+y)=x+1
				Substitute, 33, 25

			Apply commutativity

			35	ALL(b):[1 ε n & b ε n => 1+b=b+1]
				U Spec, 10

			36	1 ε n & y ε n => 1+y=y+1
				U Spec, 35

			37	1 ε n & y ε n
				Join, 2, 24

			38	1+y=y+1
				Detach, 36, 37

			39	x+(y+1)=x+1
				Substitute, 38, 34

			Apply associativity

			40	ALL(b):ALL(c):[x ε n & b ε n & c ε n => x+b+c=x+(b+c)]
				U Spec, 9

			41	ALL(c):[x ε n & y ε n & c ε n => x+y+c=x+(y+c)]
				U Spec, 40

			42	x ε n & y ε n & 1 ε n => x+y+1=x+(y+1)
				U Spec, 41

			43	x ε n & y ε n
				Join, 22, 24

			44	x ε n & y ε n & 1 ε n
				Join, 43, 2

			45	x+y+1=x+(y+1)
				Detach, 42, 44

			46	x+y+1=x+1
				Substitute, 45, 39

			Apply axiom

			47	ALL(b):[x+y ε n & b ε n & x+y+1=b+1 => x+y=b]
				U Spec, 5

			48	x+y ε n & x ε n & x+y+1=x+1 => x+y=x
				U Spec, 47

			49	ALL(b):[x ε n & b ε n => x+b ε n]
				U Spec, 3

			50	x ε n & y ε n => x+y ε n
				U Spec, 49

			51	x ε n & y ε n
				Join, 22, 24

			52	x+y ε n
				Detach, 50, 51

			53	x+y ε n & x ε n
				Join, 52, 22

			54	x+y ε n & x ε n & x+y+1=x+1
				Join, 53, 46

			55	x+y=x
				Detach, 48, 54

			Obtain contradiction...

			56	x+y=x & ~x+y=x
				Join, 55, 27

		As Required:

		57	~x+1+y=x+1
			Conclusion, 25
	As Required:

	58	ALL(b):[b ε n => ~x+1+b=x+1]
		Conclusion, 24
Inductive Step
--------------

As Required:

59	ALL(k):[k ε n & ALL(b):[b ε n => ~k+b=k]
	=> ALL(b):[b ε n => ~k+1+b=k+1]]
	Conclusion, 21
Joining results...

60	ALL(b):[b ε n => ~1+b=1]
	& ALL(k):[k ε n & ALL(b):[b ε n => ~k+b=k]
	=> ALL(b):[b ε n => ~k+1+b=k+1]]
	Join, 20, 59

By induction...

61	ALL(k):[k ε n => ALL(b):[b ε n => ~k+b=k]]
	Detach, 11, 60

	
	Prove: ALL(a):ALL(b):[a ε n & b ε n => ~a+b=a]
	
	Suppose...

	62	x ε n & y ε n
		Premise

	63	x ε n
		Split, 62

	64	y ε n
		Split, 62

	Apply previous result...

	65	x ε n => ALL(b):[b ε n => ~x+b=x]
		U Spec, 61

	66	ALL(b):[b ε n => ~x+b=x]
		Detach, 65, 63

	67	y ε n => ~x+y=x
		U Spec, 66

	68	~x+y=x
		Detach, 67, 64

As Required:

69	ALL(a):ALL(b):[a ε n & b ε n => ~a+b=a]
	Conclusion, 62
	
	Prove: ALL(a):[a ε n => ~a<a]
	
	Suppose...

	70	x ε n
		Premise

	Apply definition of <

	71	ALL(b):[x ε n & b ε n => [x<b <=> EXIST(c):[c ε n & x+c=b]]]
		U Spec, 8

	72	x ε n & x ε n => [x<x <=> EXIST(c):[c ε n & x+c=x]]
		U Spec, 71

	73	x ε n & x ε n
		Join, 70, 70

	74	x<x <=> EXIST(c):[c ε n & x+c=x]
		Detach, 72, 73

	75	[x<x => EXIST(c):[c ε n & x+c=x]]
		& [EXIST(c):[c ε n & x+c=x] => x<x]
		Iff-And, 74

	76	x<x => EXIST(c):[c ε n & x+c=x]
		Split, 75

	77	EXIST(c):[c ε n & x+c=x] => x<x
		Split, 75

	78	~EXIST(c):[c ε n & x+c=x] => ~x<x
		Contra, 76

	79	~~ALL(c):~[c ε n & x+c=x] => ~x<x
		Quant, 78

	80	ALL(c):~[c ε n & x+c=x] => ~x<x
		Rem DNeg, 79

	81	ALL(c):~~[c ε n => ~x+c=x] => ~x<x
		Imply-And, 80

	Sufficient for: ~x<x

	82	ALL(c):[c ε n => ~x+c=x] => ~x<x
		Rem DNeg, 81

		
		Prove: ALL(c):[c ε n => ~x+c=x]
		
		Suppose...

		83	y ε n
			Premise

		84	ALL(b):[x ε n & b ε n => ~x+b=x]
			U Spec, 69

		85	x ε n & y ε n => ~x+y=x
			U Spec, 84

		86	x ε n & y ε n
			Join, 70, 83

		87	~x+y=x
			Detach, 85, 86

	88	ALL(c):[c ε n => ~x+c=x]
		Conclusion, 83
	89	~x<x
		Detach, 82, 88

As Required:

90	ALL(a):[a ε n => ~a<a]
	Conclusion, 70