Irrationality of Root 2

Introduction

------------

Prove: ~EXIST(a):[a e qpos & a*a=2/1]

where qpos is the set of postive rational numbers and 2/1 = 2

Axioms, Definitions and Previous Results

----------------------------------------

Fundamental properties of the set of natural numbers n (from Peano's Axioms)

1 Set(n)

Axiom

2 1 e n

Axiom

Define: + for n

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

Axiom

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

Axiom

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

Axiom

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

Axiom

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

Axiom

Define: 2

8 2 e n

Axiom

9 1+1=2

Axiom

Define: * for n

10 ALL(a):ALL(b):[a e n & b e n => a*b e n]

& ALL(a):[a e n => a*1=a]

& ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]

Definition

11 ALL(a):ALL(b):[a e n & b e n => a*b e n]

Split, 10

12 ALL(a):[a e n => a*1=a]

Split, 10

13 ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]

Split, 10

Associativity of * on n

14 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]

Axiom

Commutativity of * on n

15 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]

Axiom

Right cancellability of * on n

16 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & a*b=c*b => a=c]

Axiom

Left cancellability of * on n

17 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & a*b=a*c => b=c]

Axiom

Define: < on n

18 ALL(a):ALL(b):[a e n & b e n => [a<b <=> EXIST(c):[c e n & a+c=b]]]

Definition

Previous result x<=y iff ~y<x

19 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> ~b<a]]

Axiom

Define: Div

Div(x,y) means x divides y, or y is divisible by x

20 ALL(a):ALL(b):[a e n & b e n => [Div(a,b) <=> EXIST(c):[c e n & b=a*c]]]

Axiom

Odd x Odd = Odd

Previous result: OddxOdd2.proof

21 ALL(a):ALL(b):[a e n & b e n & ~Div(2,a) & ~Div(2,b) => ~Div(2,a*b)]

Axiom

Define: gcd

gcd(x,y) is the greatest common divisor of x and y

22 ALL(a):ALL(b):[a e n & b e n

=> gcd(a,b) e n & Div(gcd(a,b),a) & Div(gcd(a,b),b)

& ALL(d):[d e n & Div(d,a) & Div(d,b) => d<=gcd(a,b)]]

Axiom

Define: qpos The set of positive rational numbers

23 Set(qpos)

Axiom

24 ALL(a):[a e qpos

=> EXIST(b):EXIST(c):[b e n & c e n & a=b/c]]

Axiom

Define: / operator

25 ALL(a):ALL(b):[a e n & b e n

=> a/b e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e a/b <=> a*e=d*b]]]

Axiom

Equality on qpos

26 ALL(a):ALL(b):ALL(c):ALL(d):[a e n & b e n & c e n & d e n & a/b e qpos & c/d e qpos

=> [a/b=c/d <=> a*d=c*b]]

Axiom

Define: * on qpos qMult3.proof

27 ALL(a):ALL(b):ALL(c):ALL(d):[a e n & b e n & c e n & d e n & a/b e qpos & c/d e qpos

=> a/b*(c/d)=a*c/(b*d)]

Axiom

Previous result: Existence of lowest terms LowestTerms2.proof

28 ALL(a):ALL(b):[a e n & b e n

=> EXIST(c):EXIST(d):[c e n & d e n & [a/b=c/d & gcd(c,d)=1]]]

Axiom

Proof

-----

Prove: ALL(a):~[a e qpos & a*a=2/1]

Suppose to the contrary...

29 x e qpos & x*x=2/1

Premise

30 x e qpos

Split, 29

31 x*x=2/1

Split, 29

Apply definition of qpos

32 x e qpos

=> EXIST(b):EXIST(c):[b e n & c e n & x=b/c]

U Spec, 24

33 EXIST(b):EXIST(c):[b e n & c e n & x=b/c]

Detach, 32, 30

34 EXIST(c):[x1 e n & c e n & x=x1/c]

E Spec, 33

Define: x1, x2

35 x1 e n & x2 e n & x=x1/x2

E Spec, 34

36 x1 e n

Split, 35

37 x2 e n

Split, 35

38 x=x1/x2

Split, 35

Apply previous result (existence of lowest terms)

39 ALL(b):[x1 e n & b e n

=> EXIST(c):EXIST(d):[c e n & d e n & [x1/b=c/d & gcd(c,d)=1]]]

U Spec, 28

40 x1 e n & x2 e n

=> EXIST(c):EXIST(d):[c e n & d e n & [x1/x2=c/d & gcd(c,d)=1]]

U Spec, 39

41 x1 e n & x2 e n

Join, 36, 37

42 EXIST(c):EXIST(d):[c e n & d e n & [x1/x2=c/d & gcd(c,d)=1]]

Detach, 40, 41

43 EXIST(d):[x1' e n & d e n & [x1/x2=x1'/d & gcd(x1',d)=1]]

E Spec, 42

44 x1' e n & x2' e n & [x1/x2=x1'/x2' & gcd(x1',x2')=1]

E Spec, 43

Define: x1', x2' (lowest terms)

45 x1' e n

Split, 44

46 x2' e n

Split, 44

47 x1/x2=x1'/x2' & gcd(x1',x2')=1

Split, 44

48 x1/x2=x1'/x2'

Split, 47

49 gcd(x1',x2')=1

Split, 47

Apply definition of gcd

50 ALL(b):[x1' e n & b e n

=> gcd(x1',b) e n & Div(gcd(x1',b),x1') & Div(gcd(x1',b),b)

& ALL(d):[d e n & Div(d,x1') & Div(d,b) => d<=gcd(x1',b)]]

U Spec, 22

51 x1' e n & x2' e n

=> gcd(x1',x2') e n & Div(gcd(x1',x2'),x1') & Div(gcd(x1',x2'),x2')

& ALL(d):[d e n & Div(d,x1') & Div(d,x2') => d<=gcd(x1',x2')]

U Spec, 50

52 x1' e n & x2' e n

Join, 45, 46

53 gcd(x1',x2') e n & Div(gcd(x1',x2'),x1') & Div(gcd(x1',x2'),x2')

& ALL(d):[d e n & Div(d,x1') & Div(d,x2') => d<=gcd(x1',x2')]

Detach, 51, 52

54 gcd(x1',x2') e n

Split, 53

55 Div(gcd(x1',x2'),x1')

Split, 53

56 Div(gcd(x1',x2'),x2')

Split, 53

57 ALL(d):[d e n & Div(d,x1') & Div(d,x2') => d<=gcd(x1',x2')]

Split, 53

58 x=x1'/x2'

Substitute, 48, 38

59 x1'/x2'*(x1'/x2')=2/1

Substitute, 58, 31

Apply definition of * on qpos

60 ALL(b):ALL(c):ALL(d):[x1' e n & b e n & c e n & d e n & x1'/b e qpos & c/d e qpos

=> x1'/b*(c/d)=x1'*c/(b*d)]

U Spec, 27

61 ALL(c):ALL(d):[x1' e n & x2' e n & c e n & d e n & x1'/x2' e qpos & c/d e qpos

=> x1'/x2'*(c/d)=x1'*c/(x2'*d)]

U Spec, 60

62 ALL(d):[x1' e n & x2' e n & x1' e n & d e n & x1'/x2' e qpos & x1'/d e qpos

=> x1'/x2'*(x1'/d)=x1'*x1'/(x2'*d)]

U Spec, 61

63 x1' e n & x2' e n & x1' e n & x2' e n & x1'/x2' e qpos & x1'/x2' e qpos

=> x1'/x2'*(x1'/x2')=x1'*x1'/(x2'*x2')

U Spec, 62

64 x1'/x2' e qpos

Substitute, 58, 30

65 x1' e n & x2' e n

Join, 45, 46

66 x1' e n & x2' e n & x1' e n

Join, 65, 45

67 x1' e n & x2' e n & x1' e n & x2' e n

Join, 66, 46

68 x1' e n & x2' e n & x1' e n & x2' e n

& x1'/x2' e qpos

Join, 67, 64

69 x1' e n & x2' e n & x1' e n & x2' e n

& x1'/x2' e qpos

Join, 68, 64

70 x1'/x2'*(x1'/x2')=x1'*x1'/(x2'*x2')

Detach, 63, 69

71 x1'*x1'/(x2'*x2')=2/1

Substitute, 70, 59

Apply equality on qpos

72 ALL(b):ALL(c):ALL(d):[x1'*x1' e n & b e n & c e n & d e n & x1'*x1'/b e qpos & c/d e qpos

=> [x1'*x1'/b=c/d <=> x1'*x1'*d=c*b]]

U Spec, 26

73 ALL(c):ALL(d):[x1'*x1' e n & x2'*x2' e n & c e n & d e n & x1'*x1'/(x2'*x2') e qpos & c/d e qpos

=> [x1'*x1'/(x2'*x2')=c/d <=> x1'*x1'*d=c*(x2'*x2')]]

U Spec, 72

74 ALL(d):[x1'*x1' e n & x2'*x2' e n & 2 e n & d e n & x1'*x1'/(x2'*x2') e qpos & 2/d e qpos

=> [x1'*x1'/(x2'*x2')=2/d <=> x1'*x1'*d=2*(x2'*x2')]]

U Spec, 73

75 x1'*x1' e n & x2'*x2' e n & 2 e n & 1 e n & x1'*x1'/(x2'*x2') e qpos & 2/1 e qpos

=> [x1'*x1'/(x2'*x2')=2/1 <=> x1'*x1'*1=2*(x2'*x2')]

U Spec, 74

76 ALL(b):[x1' e n & b e n => x1'*b e n]

U Spec, 11

77 x1' e n & x1' e n => x1'*x1' e n

U Spec, 76

78 x1' e n & x1' e n

Join, 45, 45

79 x1'*x1' e n

Detach, 77, 78

80 ALL(b):[x2' e n & b e n => x2'*b e n]

U Spec, 11

81 x2' e n & x2' e n => x2'*x2' e n

U Spec, 80

82 x2' e n & x2' e n

Join, 46, 46

83 x2'*x2' e n

Detach, 81, 82

84 ALL(b):[x1'*x1' e n & b e n

=> x1'*x1'/b e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e x1'*x1'/b <=> x1'*x1'*e=d*b]]]

U Spec, 25

85 x1'*x1' e n & x2'*x2' e n

=> x1'*x1'/(x2'*x2') e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e x1'*x1'/(x2'*x2') <=> x1'*x1'*e=d*(x2'*x2')]]

U Spec, 84

86 x1'*x1' e n & x2'*x2' e n

Join, 79, 83

87 x1'*x1'/(x2'*x2') e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e x1'*x1'/(x2'*x2') <=> x1'*x1'*e=d*(x2'*x2')]]

Detach, 85, 86

88 x1'*x1'/(x2'*x2') e qpos

Split, 87

89 ALL(d):ALL(e):[d e n & e e n => [(d,e) e x1'*x1'/(x2'*x2') <=> x1'*x1'*e=d*(x2'*x2')]]

Split, 87

90 ALL(b):[2 e n & b e n

=> 2/b e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e 2/b <=> 2*e=d*b]]]

U Spec, 25

91 2 e n & 1 e n

=> 2/1 e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e 2/1 <=> 2*e=d*1]]

U Spec, 90

92 2 e n & 1 e n

Join, 8, 2

93 2/1 e qpos

& ALL(d):ALL(e):[d e n & e e n => [(d,e) e 2/1 <=> 2*e=d*1]]

Detach, 91, 92

94 2/1 e qpos

Split, 93

95 ALL(d):ALL(e):[d e n & e e n => [(d,e) e 2/1 <=> 2*e=d*1]]

Split, 93

96 x1'*x1' e n & x2'*x2' e n

Join, 79, 83

97 x1'*x1' e n & x2'*x2' e n & 2 e n

Join, 96, 8

98 x1'*x1' e n & x2'*x2' e n & 2 e n & 1 e n

Join, 97, 2

99 x1'*x1' e n & x2'*x2' e n & 2 e n & 1 e n

& x1'*x1'/(x2'*x2') e qpos

Join, 98, 88

100 x1'*x1' e n & x2'*x2' e n & 2 e n & 1 e n

& x1'*x1'/(x2'*x2') e qpos

& 2/1 e qpos

Join, 99, 94

101 x1'*x1'/(x2'*x2')=2/1 <=> x1'*x1'*1=2*(x2'*x2')

Detach, 75, 100

102 [x1'*x1'/(x2'*x2')=2/1 => x1'*x1'*1=2*(x2'*x2')]

& [x1'*x1'*1=2*(x2'*x2') => x1'*x1'/(x2'*x2')=2/1]

Iff-And, 101

103 x1'*x1'/(x2'*x2')=2/1 => x1'*x1'*1=2*(x2'*x2')

Split, 102

104 x1'*x1'*1=2*(x2'*x2') => x1'*x1'/(x2'*x2')=2/1

Split, 102

105 x1'*x1'*1=2*(x2'*x2')

Detach, 103, 71

106 x1'*x1' e n => x1'*x1'*1=x1'*x1'

U Spec, 12

107 x1'*x1'*1=x1'*x1'

Detach, 106, 79

108 x1'*x1'=2*(x2'*x2')

Substitute, 107, 105

109 ALL(b):[2 e n & b e n => [Div(2,b) <=> EXIST(c):[c e n & b=2*c]]]

U Spec, 20

110 2 e n & x1'*x1' e n => [Div(2,x1'*x1') <=> EXIST(c):[c e n & x1'*x1'=2*c]]

U Spec, 109

111 2 e n & x1'*x1' e n

Join, 8, 79

112 Div(2,x1'*x1') <=> EXIST(c):[c e n & x1'*x1'=2*c]

Detach, 110, 111

113 [Div(2,x1'*x1') => EXIST(c):[c e n & x1'*x1'=2*c]]

& [EXIST(c):[c e n & x1'*x1'=2*c] => Div(2,x1'*x1')]

Iff-And, 112

114 Div(2,x1'*x1') => EXIST(c):[c e n & x1'*x1'=2*c]

Split, 113

115 EXIST(c):[c e n & x1'*x1'=2*c] => Div(2,x1'*x1')

Split, 113

116 x2'*x2' e n & x1'*x1'=2*(x2'*x2')

Join, 83, 108

117 EXIST(c):[c e n & x1'*x1'=2*c]

E Gen, 116

x1'*x1' is even

118 Div(2,x1'*x1')

Detach, 115, 117

Prove: Div(2,x1') x1' is even

Suppose to the contrary...

119 ~Div(2,x1')

Premise

120 ALL(b):[x1' e n & b e n & ~Div(2,x1') & ~Div(2,b) => ~Div(2,x1'*b)]

U Spec, 21

121 x1' e n & x1' e n & ~Div(2,x1') & ~Div(2,x1') => ~Div(2,x1'*x1')

U Spec, 120

122 x1' e n & x1' e n

Join, 45, 45

123 x1' e n & x1' e n & ~Div(2,x1')

Join, 122, 119

124 x1' e n & x1' e n & ~Div(2,x1') & ~Div(2,x1')

Join, 123, 119

125 ~Div(2,x1'*x1')

Detach, 121, 124

126 Div(2,x1'*x1') & ~Div(2,x1'*x1')

Join, 118, 125

As Required:

127 ~~Div(2,x1')

4 Conclusion, 119

x1' is even

128 Div(2,x1')

Rem DNeg, 127

129 ALL(b):[2 e n & b e n => [Div(2,b) <=> EXIST(c):[c e n & b=2*c]]]

U Spec, 20

130 2 e n & x1' e n => [Div(2,x1') <=> EXIST(c):[c e n & x1'=2*c]]

U Spec, 129

131 2 e n & x1' e n

Join, 8, 45

132 Div(2,x1') <=> EXIST(c):[c e n & x1'=2*c]

Detach, 130, 131

133 [Div(2,x1') => EXIST(c):[c e n & x1'=2*c]]

& [EXIST(c):[c e n & x1'=2*c] => Div(2,x1')]

Iff-And, 132

134 Div(2,x1') => EXIST(c):[c e n & x1'=2*c]

Split, 133

135 EXIST(c):[c e n & x1'=2*c] => Div(2,x1')

Split, 133

136 EXIST(c):[c e n & x1'=2*c]

Detach, 134, 128

Define: p

137 p e n & x1'=2*p

E Spec, 136

138 p e n

Split, 137

139 x1'=2*p

Split, 137

140 2*p*(2*p)=2*(x2'*x2')

Substitute, 139, 108

Prove: 2*(p*p)=x2'*x2'

Apply assciativity of *

141 ALL(b):ALL(c):[2 e n & b e n & c e n => 2*b*c=2*(b*c)]

U Spec, 14

142 ALL(c):[2 e n & p e n & c e n => 2*p*c=2*(p*c)]

U Spec, 141

143 2 e n & p e n & 2*p e n => 2*p*(2*p)=2*(p*(2*p))

U Spec, 142

144 ALL(b):[2 e n & b e n => 2*b e n]

U Spec, 11

145 2 e n & p e n => 2*p e n

U Spec, 144

146 2 e n & p e n

Join, 8, 138

147 2*p e n

Detach, 145, 146

148 2 e n & p e n

Join, 8, 138

149 2 e n & p e n & 2*p e n

Join, 148, 147

150 2*p*(2*p)=2*(p*(2*p))

Detach, 143, 149

151 2*(p*(2*p))=2*(x2'*x2')

Substitute, 150, 140

Apply left cancellability of *

152 ALL(b):ALL(c):[2 e n & b e n & c e n & 2*b=2*c => b=c]

U Spec, 17

153 ALL(c):[2 e n & p*(2*p) e n & c e n & 2*(p*(2*p))=2*c => p*(2*p)=c]

U Spec, 152

154 2 e n & p*(2*p) e n & x2'*x2' e n & 2*(p*(2*p))=2*(x2'*x2') => p*(2*p)=x2'*x2'

U Spec, 153

155 ALL(b):[p e n & b e n => p*b e n]

U Spec, 11

156 p e n & 2*p e n => p*(2*p) e n

U Spec, 155

157 p e n & 2*p e n

Join, 138, 147

158 p*(2*p) e n

Detach, 156, 157

159 2 e n & p*(2*p) e n

Join, 8, 158

160 2 e n & p*(2*p) e n & x2'*x2' e n

Join, 159, 83

161 2 e n & p*(2*p) e n & x2'*x2' e n

& 2*(p*(2*p))=2*(x2'*x2')

Join, 160, 151

162 p*(2*p)=x2'*x2'

Detach, 154, 161

Apply associativity of *

163 ALL(b):ALL(c):[p e n & b e n & c e n => p*b*c=p*(b*c)]

U Spec, 14

164 ALL(c):[p e n & 2 e n & c e n => p*2*c=p*(2*c)]

U Spec, 163

165 p e n & 2 e n & p e n => p*2*p=p*(2*p)

U Spec, 164

166 p e n & 2 e n

Join, 138, 8

167 p e n & 2 e n & p e n

Join, 166, 138

168 p*2*p=p*(2*p)

Detach, 165, 167

169 p*2*p=x2'*x2'

Substitute, 168, 162

Apply commutativity of *

170 ALL(b):[p e n & b e n => p*b=b*p]

U Spec, 15

171 p e n & 2 e n => p*2=2*p

U Spec, 170

172 p e n & 2 e n

Join, 138, 8

173 p*2=2*p

Detach, 171, 172

174 2*p*p=x2'*x2'

Substitute, 173, 169

175 ALL(b):ALL(c):[2 e n & b e n & c e n => 2*b*c=2*(b*c)]

U Spec, 14

176 ALL(c):[2 e n & p e n & c e n => 2*p*c=2*(p*c)]

U Spec, 175

177 2 e n & p e n & p e n => 2*p*p=2*(p*p)

U Spec, 176

178 2 e n & p e n

Join, 8, 138

179 2 e n & p e n & p e n

Join, 178, 138

180 2*p*p=2*(p*p)

Detach, 177, 179

As Required:

181 2*(p*p)=x2'*x2'

Substitute, 180, 174

Apply definiton of Div

182 ALL(b):[2 e n & b e n => [Div(2,b) <=> EXIST(c):[c e n & b=2*c]]]

U Spec, 20

183 2 e n & x2'*x2' e n => [Div(2,x2'*x2') <=> EXIST(c):[c e n & x2'*x2'=2*c]]

U Spec, 182

184 2 e n & x2'*x2' e n

Join, 8, 83

185 Div(2,x2'*x2') <=> EXIST(c):[c e n & x2'*x2'=2*c]

Detach, 183, 184

186 [Div(2,x2'*x2') => EXIST(c):[c e n & x2'*x2'=2*c]]

& [EXIST(c):[c e n & x2'*x2'=2*c] => Div(2,x2'*x2')]

Iff-And, 185

187 Div(2,x2'*x2') => EXIST(c):[c e n & x2'*x2'=2*c]

Split, 186

188 EXIST(c):[c e n & x2'*x2'=2*c] => Div(2,x2'*x2')

Split, 186

189 ALL(b):[p e n & b e n => p*b e n]

U Spec, 11

190 p e n & p e n => p*p e n

U Spec, 189

191 p e n & p e n

Join, 138, 138

192 p*p e n

Detach, 190, 191

193 x2'*x2'=2*(p*p)

Sym, 181

194 p*p e n & x2'*x2'=2*(p*p)

Join, 192, 193

195 EXIST(c):[c e n & x2'*x2'=2*c]

E Gen, 194

x2'*x2' is even

196 Div(2,x2'*x2')

Detach, 188, 195

Prove: Div(2,x2') x2' is even

Suppose to the contrary...

197 ~Div(2,x2')

Premise

198 ALL(b):[x2' e n & b e n & ~Div(2,x2') & ~Div(2,b) => ~Div(2,x2'*b)]

U Spec, 21

199 x2' e n & x2' e n & ~Div(2,x2') & ~Div(2,x2') => ~Div(2,x2'*x2')

U Spec, 198

200 x2' e n & x2' e n

Join, 46, 46

201 x2' e n & x2' e n & ~Div(2,x2')

Join, 200, 197

202 x2' e n & x2' e n & ~Div(2,x2') & ~Div(2,x2')

Join, 201, 197

203 ~Div(2,x2'*x2')

Detach, 199, 202

Obtain the contradiction...

204 Div(2,x2'*x2') & ~Div(2,x2'*x2')

Join, 196, 203

As Required:

205 ~~Div(2,x2')

4 Conclusion, 197

x2' is even

206 Div(2,x2')

Rem DNeg, 205

Apply previous result

207 2 e n & Div(2,x1') & Div(2,x2') => 2<=gcd(x1',x2')

U Spec, 57

208 2 e n & Div(2,x1')

Join, 8, 128

209 2 e n & Div(2,x1') & Div(2,x2')

Join, 208, 206

210 2<=gcd(x1',x2')

Detach, 207, 209

211 2<=1

Substitute, 49, 210

Apply previous result

212 ALL(b):[2 e n & b e n => [2<=b <=> ~b<2]]

U Spec, 19

213 2 e n & 1 e n => [2<=1 <=> ~1<2]

U Spec, 212

214 2 e n & 1 e n

Join, 8, 2

215 2<=1 <=> ~1<2

Detach, 213, 214

216 [2<=1 => ~1<2] & [~1<2 => 2<=1]

Iff-And, 215

217 2<=1 => ~1<2

Split, 216

218 ~1<2 => 2<=1

Split, 216

219 ~1<2

Detach, 217, 211

Apply definiton of <

220 ALL(b):[1 e n & b e n => [1<b <=> EXIST(c):[c e n & 1+c=b]]]

U Spec, 18

221 1 e n & 2 e n => [1<2 <=> EXIST(c):[c e n & 1+c=2]]

U Spec, 220

222 1 e n & 2 e n

Join, 2, 8

223 1<2 <=> EXIST(c):[c e n & 1+c=2]

Detach, 221, 222

224 [1<2 => EXIST(c):[c e n & 1+c=2]]

& [EXIST(c):[c e n & 1+c=2] => 1<2]

Iff-And, 223

225 1<2 => EXIST(c):[c e n & 1+c=2]

Split, 224

226 EXIST(c):[c e n & 1+c=2] => 1<2

Split, 224

227 1 e n & 1+1=2

Join, 2, 9

228 EXIST(c):[c e n & 1+c=2]

E Gen, 227

229 1<2

Detach, 226, 228

Obtain the contradiction...

230 1<2 & ~1<2

Join, 229, 219

231 ~EXIST(a):[a e qpos & a*a=2/1]

4 Conclusion, 29