Uniqueness of even number function

From email:
From: "Thomas Heye" <1910-131εonlinehome.de> 
To: <dcproofεyahoogroups.com> 
Sent: Saturday, September 16, 2006 3:41 AM 
Subject: [DC Proof] Ideas for uniqueness of even number function 

> Hi folks,
> I'd like to prove for all natural numbers a,b that a +a=b+b implies
> a=b.
> 
> My ideas so far: Having shown that a<b, a=b, b<a are mutually
> exclusive, it should be possible to deduce from a+a=b+b that a<b, b<a
> resp. is impossible, so equality must hold.
> 
> Or is there an easier way?
> 
> Thanks,
> 
> Thomas

Peano's Axioms

1	Set(n)
	& 1 ε n
	& ALL(a):[a ε n => next(a) ε n]
	& ALL(a):[a ε n => ~next(a)=1]
	& ALL(a):ALL(b):[a ε n & b ε n & next(a)=next(b) => a=b]
	& ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => next(b) ε a]
	=> ALL(b):[b ε n => b ε a]]
	Premise

Define +

2	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	& ALL(a):[a ε n => a+1=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => a+next(b)=next(a+b)]
	Definition

3	Set(n)
	Split, 1

4	1 ε n
	Split, 1

5	ALL(a):[a ε n => next(a) ε n]
	Split, 1

6	ALL(a):[a ε n => ~next(a)=1]
	Split, 1

7	ALL(a):ALL(b):[a ε n & b ε n & next(a)=next(b) => a=b]
	Split, 1

8	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => next(b) ε a]
	=> ALL(b):[b ε n => b ε a]]
	Split, 1

9	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	Split, 2

10	ALL(a):[a ε n => a+1=next(a)]
	Split, 2

11	ALL(a):ALL(b):[a ε n & b ε n => a+next(b)=next(a+b)]
	Split, 2

Define <

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

Assumed: a<b & b<c => a<c

13	ALL(a):ALL(b):ALL(c):[a ε n & b ε n & c ε n & a<b & b<c => a<c]
	Premise

Assumed: a+b=b+a

14	ALL(a):ALL(b):[a ε n & b ε n => a+b=b+a]
	Premise

Assumed: Exclusivity of a<b, a=b, and b<a

15	ALL(a):ALL(b):[a ε n & b ε n => [a<b | a=b | b<a]
	& ~[a<b & a=b] & ~[a=b & b<a] & ~[a<b & b<a]]
	Premise

Assumed: a<b => a+c<b+c

16	ALL(a):ALL(b):ALL(c):[a ε n & b ε n & c ε n & a<b => a+c<b+c]
	Premise

	17	x ε n & y ε n & x+x=y+y
		Premise

	18	x ε n
		Split, 17

	19	y ε n
		Split, 17

	20	x+x=y+y
		Split, 17

	21	x ε n & y ε n
		Join, 18, 19

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

	23	x ε n & y ε n => x+y ε n
		U Spec, 22

	24	x+y ε n
		Detach, 23, 21

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

	26	x ε n & y ε n => x+y=y+x
		U Spec, 25

	27	x+y=y+x
		Detach, 26, 21

		28	z ε n
			Premise

		29	z ε n & z ε n
			Join, 28, 28

		30	ALL(b):[z ε n & b ε n => z+b ε n]
			U Spec, 9

		31	z ε n & z ε n => z+z ε n
			U Spec, 30

		32	z+z ε n
			Detach, 31, 29

	33	z ε n => z+z ε n
		Conclusion, 28

	34	ALL(c):[c ε n => c+c ε n]
		U Gen, 33

	35	x ε n => x+x ε n
		U Spec, 34

	36	y ε n => y+y ε n
		U Spec, 34

	37	x+x ε n
		Detach, 35, 18

	38	y+y ε n
		Detach, 36, 19

	39	ALL(b):[x+x ε n & b ε n => [x+x<b | x+x=b | b<x+x]
		& ~[x+x<b & x+x=b] & ~[x+x=b & b<x+x] & ~[x+x<b & b<x+x]]
		U Spec, 15

	40	x+x ε n & y+y ε n => [x+x<y+y | x+x=y+y | y+y<x+x]
		& ~[x+x<y+y & x+x=y+y] & ~[x+x=y+y & y+y<x+x] & ~[x+x<y+y & y+y<x+x]
		U Spec, 39

	41	x+x ε n & y+y ε n
		Join, 37, 38

	42	[x+x<y+y | x+x=y+y | y+y<x+x]
		& ~[x+x<y+y & x+x=y+y] & ~[x+x=y+y & y+y<x+x] & ~[x+x<y+y & y+y<x+x]
		Detach, 40, 41

	43	x+x<y+y | x+x=y+y | y+y<x+x
		Split, 42

	44	~[x+x<y+y & x+x=y+y]
		Split, 42

		45	x<y
			Premise

		46	ALL(b):ALL(c):[x ε n & b ε n & c ε n & x<b => x+c<b+c]
			U Spec, 16

		47	ALL(c):[x ε n & y ε n & c ε n & x<y => x+c<y+c]
			U Spec, 46

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

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

		50	x ε n & y ε n & x ε n
			Join, 21, 18

		51	x ε n & y ε n & y ε n
			Join, 21, 19

		52	x ε n & y ε n & x ε n & x<y
			Join, 50, 45

		53	x ε n & y ε n & y ε n & x<y
			Join, 51, 45

		54	x+x<y+x
			Detach, 48, 52

		55	x+y<y+y
			Detach, 49, 53

		56	x+x<x+y
			Substitute, 27, 54

		57	ALL(b):ALL(c):[x+x ε n & b ε n & c ε n & x+x<b & b<c => x+x<c]
			U Spec, 13

		58	ALL(c):[x+x ε n & x+y ε n & c ε n & x+x<x+y & x+y<c => x+x<c]
			U Spec, 57

		59	x+x ε n & x+y ε n & y+y ε n & x+x<x+y & x+y<y+y => x+x<y+y
			U Spec, 58

		60	x+x ε n & x+y ε n
			Join, 37, 24

		61	x+x ε n & x+y ε n & y+y ε n
			Join, 60, 38

		62	x+x ε n & x+y ε n & y+y ε n & x+x<x+y
			Join, 61, 56

		63	x+x ε n & x+y ε n & y+y ε n & x+x<x+y & x+y<y+y
			Join, 62, 55

		64	x+x<y+y
			Detach, 59, 63

		65	x+x<y+y & x+x=y+y
			Join, 64, 20

		66	~[x+x<y+y & x+x=y+y] & [x+x<y+y & x+x=y+y]
			Join, 44, 65

	67	~x<y
		Conclusion, 45

68	x ε n & y ε n & x+x=y+y => ~x<y
	Conclusion, 17

69	ALL(b):[x ε n & b ε n & x+x=b+b => ~x<b]
	U Gen, 68

70	ALL(a):ALL(b):[a ε n & b ε n & a+a=b+b => ~a<b]
	U Gen, 69

	71	x ε n & y ε n & x+x=y+y
		Premise

	72	~x<y
		Detach, 68, 71

	73	x ε n
		Split, 71

	74	y ε n
		Split, 71

	75	x+x=y+y
		Split, 71

	76	y+y=x+x
		Sym, 75

	77	y ε n & x ε n
		Join, 74, 73

	78	y ε n & x ε n & y+y=x+x
		Join, 77, 76

	79	ALL(b):[y ε n & b ε n & y+y=b+b => ~y<b]
		U Spec, 70

	80	y ε n & x ε n & y+y=x+x => ~y<x
		U Spec, 79

	81	~y<x
		Detach, 80, 78

	82	ALL(b):[x ε n & b ε n => [x<b | x=b | b<x]
		& ~[x<b & x=b] & ~[x=b & b<x] & ~[x<b & b<x]]
		U Spec, 15

	83	x ε n & y ε n => [x<y | x=y | y<x]
		& ~[x<y & x=y] & ~[x=y & y<x] & ~[x<y & y<x]
		U Spec, 82

	84	x ε n & y ε n
		Join, 73, 74

	85	[x<y | x=y | y<x]
		& ~[x<y & x=y] & ~[x=y & y<x] & ~[x<y & y<x]
		Detach, 83, 84

	86	x<y | x=y | y<x
		Split, 85

	87	[~x<y => x=y] | y<x
		Imply-Or, 86

	88	~[~x<y => x=y] => y<x
		Imply-Or, 87

	89	~y<x => ~~[~x<y => x=y]
		Contra, 88

	90	~y<x => [~x<y => x=y]
		Rem DNeg, 89

	91	~x<y => x=y
		Detach, 90, 81

	92	x=y
		Detach, 91, 72

93	x ε n & y ε n & x+x=y+y => x=y
	Conclusion, 71

94	ALL(b):[x ε n & b ε n & x+x=b+b => x=b]
	U Gen, 93

95	ALL(a):ALL(b):[a ε n & b ε n & a+a=b+b => a=b]
	U Gen, 94