reconsider two = 2 as ordinal Element of RAT+ by Lm1;

reconsider a9 = 1 as Element of RAT+ by Lm1;

defpred S_{1}[ Element of RAT+ ] means $1 *' $1 < two;

set X = { s where s is Element of RAT+ : S_{1}[s] } ;

reconsider X = { s where s is Element of RAT+ : S_{1}[s] } as Subset of RAT+ from DOMAIN_1:sch 7();

A1: ( 2 *^ 2 = two *' two & 1 *^ 2 = 2 ) by ARYTM_3:59, ORDINAL2:39;

2 = succ 1

.= 1 \/ {1} ;

then A2: a9 <=' two by Lm10, XBOOLE_1:7;

then A3: a9 < two by ARYTM_3:68;

A4: a9 *' a9 = a9 by ARYTM_3:53;

then A5: 1 in X by A3;

A6: for r, t being Element of RAT+ st r in X & t <=' r holds

t in X

reconsider O9 = 0 as Element of RAT+ by Lm1;

set DD = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } ;

consider half being Element of RAT+ such that

A10: a9 = two *' half by ARYTM_3:55, Lm11;

A11: one <=' two by Lm13;

then A12: one < two by ARYTM_3:68;

then 1 in 2 by ORDINAL1:6;

then A65: 1 *^ 2 in 2 *^ 2 by ORDINAL3:19;

A66: O9 <=' a9 by ARYTM_3:64;

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } ;

a9 *' half = half by ARYTM_3:53;

then A83: half in X by A10, A6, A2, A5, ARYTM_3:82;

then not X in {RAT+} by TARSKI:def 1;

then X in DEDEKIND_CUTS by A82, ARYTM_2:def 1, XBOOLE_0:def 5;

then X in RAT+ \/ DEDEKIND_CUTS by XBOOLE_0:def 3;

then X in REAL+ by A13, ARYTM_2:def 2, XBOOLE_0:def 5;

then X in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;

then X in REAL by A9, XBOOLE_0:def 5;

hence RAT c< REAL by A84, Lm8; :: thesis: verum

reconsider a9 = 1 as Element of RAT+ by Lm1;

defpred S

set X = { s where s is Element of RAT+ : S

reconsider X = { s where s is Element of RAT+ : S

A1: ( 2 *^ 2 = two *' two & 1 *^ 2 = 2 ) by ARYTM_3:59, ORDINAL2:39;

2 = succ 1

.= 1 \/ {1} ;

then A2: a9 <=' two by Lm10, XBOOLE_1:7;

then A3: a9 < two by ARYTM_3:68;

A4: a9 *' a9 = a9 by ARYTM_3:53;

then A5: 1 in X by A3;

A6: for r, t being Element of RAT+ st r in X & t <=' r holds

t in X

proof

then A8:
0 in X
by A5, ARYTM_3:64;
let r, t be Element of RAT+ ; :: thesis: ( r in X & t <=' r implies t in X )

assume r in X ; :: thesis: ( not t <=' r or t in X )

then A7: ex s being Element of RAT+ st

( r = s & s *' s < two ) ;

assume t <=' r ; :: thesis: t in X

then ( t *' t <=' t *' r & t *' r <=' r *' r ) by ARYTM_3:82;

then t *' t <=' r *' r by ARYTM_3:67;

then t *' t < two by A7, ARYTM_3:69;

hence t in X ; :: thesis: verum

end;assume r in X ; :: thesis: ( not t <=' r or t in X )

then A7: ex s being Element of RAT+ st

( r = s & s *' s < two ) ;

assume t <=' r ; :: thesis: t in X

then ( t *' t <=' t *' r & t *' r <=' r *' r ) by ARYTM_3:82;

then t *' t <=' r *' r by ARYTM_3:67;

then t *' t < two by A7, ARYTM_3:69;

hence t in X ; :: thesis: verum

now :: thesis: not X = [0,0]

then A9:
not X in {[0,0]}
by TARSKI:def 1;assume
X = [0,0]
; :: thesis: contradiction

then X = {{0},{0}} by ENUMSET1:29

.= {{0}} by ENUMSET1:29 ;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

end;then X = {{0},{0}} by ENUMSET1:29

.= {{0}} by ENUMSET1:29 ;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

reconsider O9 = 0 as Element of RAT+ by Lm1;

set DD = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } ;

consider half being Element of RAT+ such that

A10: a9 = two *' half by ARYTM_3:55, Lm11;

A11: one <=' two by Lm13;

then A12: one < two by ARYTM_3:68;

A13: now :: thesis: not X in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> 0 }

2 = succ 1
;assume
X in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> 0 }
; :: thesis: contradiction

then consider t0 being Element of RAT+ such that

A14: X = { s where s is Element of RAT+ : s < t0 } and

A15: t0 <> 0 ;

set n = numerator t0;

set d = denominator t0;

denominator t0 <> 0 by ARYTM_3:35;

then (denominator t0) *^ (denominator t0) <> {} by ORDINAL3:31;

then A62: two *^ ((denominator t0) *^ (denominator t0)) = 1 *^ ((numerator t0) *^ (numerator t0)) by A61, ARYTM_3:45, Lm11

.= (numerator t0) *^ (numerator t0) by ORDINAL2:39 ;

then consider k being natural Ordinal such that

A63: numerator t0 = 2 *^ k by Lm12;

two *^ ((denominator t0) *^ (denominator t0)) = 2 *^ (k *^ (2 *^ k)) by A62, A63, ORDINAL3:50;

then (denominator t0) *^ (denominator t0) = k *^ (2 *^ k) by ORDINAL3:33, Lm11

.= 2 *^ (k *^ k) by ORDINAL3:50 ;

then A64: ex p being natural Ordinal st denominator t0 = 2 *^ p by Lm12;

numerator t0, denominator t0 are_coprime by ARYTM_3:34;

hence contradiction by A63, A64; :: thesis: verum

end;then consider t0 being Element of RAT+ such that

A14: X = { s where s is Element of RAT+ : s < t0 } and

A15: t0 <> 0 ;

set n = numerator t0;

set d = denominator t0;

now :: thesis: not t0 *' t0 <> two

then A61:
two / 1 = ((numerator t0) *^ (numerator t0)) / ((denominator t0) *^ (denominator t0))
by ARYTM_3:40;assume A16:
t0 *' t0 <> two
; :: thesis: contradiction

end;per cases
( t0 *' t0 < two or two < t0 *' t0 )
by A16, ARYTM_3:66;

end;

suppose
t0 *' t0 < two
; :: thesis: contradiction

then
t0 in X
;

then ex s being Element of RAT+ st

( s = t0 & s < t0 ) by A14;

hence contradiction ; :: thesis: verum

end;then ex s being Element of RAT+ st

( s = t0 & s < t0 ) by A14;

hence contradiction ; :: thesis: verum

suppose A17:
two < t0 *' t0
; :: thesis: contradiction

consider es being Element of RAT+ such that

A18: ( two + es = t0 *' t0 or (t0 *' t0) + es = two ) by ARYTM_3:92;

then O9 < es by A19, ARYTM_3:68;

then consider s being Element of RAT+ such that

A20: O9 < s and

A21: s < es by ARYTM_3:93;

end;A18: ( two + es = t0 *' t0 or (t0 *' t0) + es = two ) by ARYTM_3:92;

A19: now :: thesis: not O9 = es

O9 <=' es
by ARYTM_3:64;assume
O9 = es
; :: thesis: contradiction

then two + es = two by ARYTM_3:50;

hence contradiction by A17, A18; :: thesis: verum

end;then two + es = two by ARYTM_3:50;

hence contradiction by A17, A18; :: thesis: verum

then O9 < es by A19, ARYTM_3:68;

then consider s being Element of RAT+ such that

A20: O9 < s and

A21: s < es by ARYTM_3:93;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( s < one or one <=' s )
;

end;

suppose A22:
s < one
; :: thesis: contradiction

A23:
s <> 0
by A20;

then s *' s < s *' one by A22, ARYTM_3:80;

then A24: s *' s < s by ARYTM_3:53;

one *' t0 < two *' t0 by A12, A15, ARYTM_3:80;

then A28: one *' one < two *' t0 by A27, ARYTM_3:70;

consider t02s2 being Element of RAT+ such that

A29: ( (s *' s) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = s *' s ) by ARYTM_3:92;

s < t0 by A22, A25, ARYTM_3:70;

then A30: s *' s < t0 by A24, ARYTM_3:70;

consider T2t9 being Element of RAT+ such that

A31: (two *' t0) *' T2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;

set x = (s *' s) *' T2t9;

consider t0x being Element of RAT+ such that

A32: ( ((s *' s) *' T2t9) + t0x = t0 or t0 + t0x = (s *' s) *' T2t9 ) by ARYTM_3:92;

((s *' s) *' T2t9) *' (two *' t0) = (s *' s) *' one by A31, ARYTM_3:52;

then ( (s *' s) *' T2t9 <=' s *' s or two *' t0 <=' one ) by ARYTM_3:83;

then A33: (s *' s) *' T2t9 < t0 by A28, A30, ARYTM_3:53, ARYTM_3:69;

then A34: t0x <=' t0 by A32;

A35: ((((s *' s) *' T2t9) *' t0x) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) = ((((s *' s) *' T2t9) *' t0x) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) + (((s *' s) *' T2t9) *' t0) by ARYTM_3:51

.= (((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' t0) by A32, A33, ARYTM_3:57

.= ((((s *' s) *' T2t9) *' t0) *' one) + (((s *' s) *' T2t9) *' t0) by ARYTM_3:53

.= ((((s *' s) *' T2t9) *' t0) *' one) + ((((s *' s) *' T2t9) *' t0) *' one) by ARYTM_3:53

.= (t0 *' ((s *' s) *' T2t9)) *' two by Lm13, ARYTM_3:57

.= ((s *' s) *' T2t9) *' (t0 *' two) by ARYTM_3:52

.= (s *' s) *' one by A31, ARYTM_3:52

.= s *' s by ARYTM_3:53 ;

es <=' t0 *' t0 by A17, A18;

then s < t0 *' t0 by A21, ARYTM_3:69;

then A36: s *' s < t0 *' t0 by A24, ARYTM_3:70;

then (t02s2 + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) + (s *' s) = ((t0x + ((s *' s) *' T2t9)) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by A29, A32, A33, ARYTM_3:51

.= ((t0x *' (t0x + ((s *' s) *' T2t9))) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by A32, A33, ARYTM_3:57

.= (((t0x *' t0x) + (((s *' s) *' T2t9) *' t0x)) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by ARYTM_3:57

.= ((t0x *' t0x) + (((s *' s) *' T2t9) *' t0x)) + ((((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) by ARYTM_3:51

.= (t0x *' t0x) + ((((s *' s) *' T2t9) *' t0x) + ((((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)))) by ARYTM_3:51

.= (t0x *' t0x) + (s *' s) by A35, ARYTM_3:51 ;

then t0x *' t0x = t02s2 + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by ARYTM_3:62;

then A37: t02s2 <=' t0x *' t0x ;

then t0x < t0 by A34, ARYTM_3:68;

then t0x in X by A14;

then A39: ex s being Element of RAT+ st

( s = t0x & s *' s < two ) ;

s *' s < es by A21, A24, ARYTM_3:70;

then two + (s *' s) < two + es by ARYTM_3:76;

then two < t02s2 by A17, A18, A29, A36, ARYTM_3:76;

hence contradiction by A37, A39, ARYTM_3:69; :: thesis: verum

end;then s *' s < s *' one by A22, ARYTM_3:80;

then A24: s *' s < s by ARYTM_3:53;

A25: now :: thesis: not t0 <=' one

then A27:
one *' one < one *' t0
by ARYTM_3:80;assume A26:
t0 <=' one
; :: thesis: contradiction

then t0 *' t0 <=' t0 *' one by ARYTM_3:82;

then t0 *' t0 <=' t0 by ARYTM_3:53;

then t0 *' t0 <=' one by A26, ARYTM_3:67;

hence contradiction by A11, A17, ARYTM_3:69; :: thesis: verum

end;then t0 *' t0 <=' t0 *' one by ARYTM_3:82;

then t0 *' t0 <=' t0 by ARYTM_3:53;

then t0 *' t0 <=' one by A26, ARYTM_3:67;

hence contradiction by A11, A17, ARYTM_3:69; :: thesis: verum

one *' t0 < two *' t0 by A12, A15, ARYTM_3:80;

then A28: one *' one < two *' t0 by A27, ARYTM_3:70;

consider t02s2 being Element of RAT+ such that

A29: ( (s *' s) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = s *' s ) by ARYTM_3:92;

s < t0 by A22, A25, ARYTM_3:70;

then A30: s *' s < t0 by A24, ARYTM_3:70;

consider T2t9 being Element of RAT+ such that

A31: (two *' t0) *' T2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;

set x = (s *' s) *' T2t9;

consider t0x being Element of RAT+ such that

A32: ( ((s *' s) *' T2t9) + t0x = t0 or t0 + t0x = (s *' s) *' T2t9 ) by ARYTM_3:92;

((s *' s) *' T2t9) *' (two *' t0) = (s *' s) *' one by A31, ARYTM_3:52;

then ( (s *' s) *' T2t9 <=' s *' s or two *' t0 <=' one ) by ARYTM_3:83;

then A33: (s *' s) *' T2t9 < t0 by A28, A30, ARYTM_3:53, ARYTM_3:69;

then A34: t0x <=' t0 by A32;

A35: ((((s *' s) *' T2t9) *' t0x) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) = ((((s *' s) *' T2t9) *' t0x) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) + (((s *' s) *' T2t9) *' t0) by ARYTM_3:51

.= (((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' t0) by A32, A33, ARYTM_3:57

.= ((((s *' s) *' T2t9) *' t0) *' one) + (((s *' s) *' T2t9) *' t0) by ARYTM_3:53

.= ((((s *' s) *' T2t9) *' t0) *' one) + ((((s *' s) *' T2t9) *' t0) *' one) by ARYTM_3:53

.= (t0 *' ((s *' s) *' T2t9)) *' two by Lm13, ARYTM_3:57

.= ((s *' s) *' T2t9) *' (t0 *' two) by ARYTM_3:52

.= (s *' s) *' one by A31, ARYTM_3:52

.= s *' s by ARYTM_3:53 ;

es <=' t0 *' t0 by A17, A18;

then s < t0 *' t0 by A21, ARYTM_3:69;

then A36: s *' s < t0 *' t0 by A24, ARYTM_3:70;

then (t02s2 + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) + (s *' s) = ((t0x + ((s *' s) *' T2t9)) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by A29, A32, A33, ARYTM_3:51

.= ((t0x *' (t0x + ((s *' s) *' T2t9))) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by A32, A33, ARYTM_3:57

.= (((t0x *' t0x) + (((s *' s) *' T2t9) *' t0x)) + (((s *' s) *' T2t9) *' t0)) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by ARYTM_3:57

.= ((t0x *' t0x) + (((s *' s) *' T2t9) *' t0x)) + ((((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9))) by ARYTM_3:51

.= (t0x *' t0x) + ((((s *' s) *' T2t9) *' t0x) + ((((s *' s) *' T2t9) *' t0) + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)))) by ARYTM_3:51

.= (t0x *' t0x) + (s *' s) by A35, ARYTM_3:51 ;

then t0x *' t0x = t02s2 + (((s *' s) *' T2t9) *' ((s *' s) *' T2t9)) by ARYTM_3:62;

then A37: t02s2 <=' t0x *' t0x ;

now :: thesis: not (s *' s) *' T2t9 = 0

then
t0x <> t0
by A32, A33, ARYTM_3:84;assume A38:
(s *' s) *' T2t9 = 0
; :: thesis: contradiction

end;then t0x < t0 by A34, ARYTM_3:68;

then t0x in X by A14;

then A39: ex s being Element of RAT+ st

( s = t0x & s *' s < two ) ;

s *' s < es by A21, A24, ARYTM_3:70;

then two + (s *' s) < two + es by ARYTM_3:76;

then two < t02s2 by A17, A18, A29, A36, ARYTM_3:76;

hence contradiction by A37, A39, ARYTM_3:69; :: thesis: verum

suppose A40:
one <=' s
; :: thesis: contradiction

half *' two = one *' one
by A10, ARYTM_3:53;

then A41: half <=' one by A12, ARYTM_3:83;

half <> one by A10, ARYTM_3:53;

then A42: half < one by A41, ARYTM_3:68;

then half < s by A40, ARYTM_3:69;

then A43: half < es by A21, ARYTM_3:70;

one <=' two by Lm13;

then one < two by ARYTM_3:68;

then A44: one *' t0 < two *' t0 by A15, ARYTM_3:80;

then A47: one *' one < two *' t0 by A44, ARYTM_3:70;

set s = half;

consider t02s2 being Element of RAT+ such that

A48: ( (half *' half) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = half *' half ) by ARYTM_3:92;

A49: half <> 0 by A10, ARYTM_3:48;

then half *' half < half *' one by A42, ARYTM_3:80;

then A50: half *' half < half by ARYTM_3:53;

half < t0 by A42, A45, ARYTM_3:70;

then A51: half *' half < t0 by A50, ARYTM_3:70;

consider T2t9 being Element of RAT+ such that

A52: (two *' t0) *' T2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;

set x = (half *' half) *' T2t9;

consider t0x being Element of RAT+ such that

A53: ( ((half *' half) *' T2t9) + t0x = t0 or t0 + t0x = (half *' half) *' T2t9 ) by ARYTM_3:92;

((half *' half) *' T2t9) *' (two *' t0) = (half *' half) *' one by A52, ARYTM_3:52;

then ( (half *' half) *' T2t9 <=' half *' half or two *' t0 <=' one ) by ARYTM_3:83;

then A54: (half *' half) *' T2t9 < t0 by A47, A51, ARYTM_3:53, ARYTM_3:69;

then A55: t0x <=' t0 by A53;

A56: ((((half *' half) *' T2t9) *' t0x) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) = ((((half *' half) *' T2t9) *' t0x) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) + (((half *' half) *' T2t9) *' t0) by ARYTM_3:51

.= (((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' t0) by A53, A54, ARYTM_3:57

.= ((((half *' half) *' T2t9) *' t0) *' one) + (((half *' half) *' T2t9) *' t0) by ARYTM_3:53

.= ((((half *' half) *' T2t9) *' t0) *' one) + ((((half *' half) *' T2t9) *' t0) *' one) by ARYTM_3:53

.= (t0 *' ((half *' half) *' T2t9)) *' two by Lm13, ARYTM_3:57

.= ((half *' half) *' T2t9) *' (t0 *' two) by ARYTM_3:52

.= (half *' half) *' one by A52, ARYTM_3:52

.= half *' half by ARYTM_3:53 ;

es <=' t0 *' t0 by A17, A18;

then half < t0 *' t0 by A43, ARYTM_3:69;

then A57: half *' half < t0 *' t0 by A50, ARYTM_3:70;

then (t02s2 + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) + (half *' half) = (t0 *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by A48, ARYTM_3:51

.= ((t0x *' (t0x + ((half *' half) *' T2t9))) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by A53, A54, ARYTM_3:57

.= (((t0x *' t0x) + (((half *' half) *' T2t9) *' t0x)) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by ARYTM_3:57

.= ((t0x *' t0x) + (((half *' half) *' T2t9) *' t0x)) + ((((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) by ARYTM_3:51

.= (t0x *' t0x) + ((((half *' half) *' T2t9) *' t0x) + ((((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)))) by ARYTM_3:51

.= (t0x *' t0x) + (half *' half) by A56, ARYTM_3:51 ;

then t0x *' t0x = t02s2 + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by ARYTM_3:62;

then A58: t02s2 <=' t0x *' t0x ;

then t0x < t0 by A55, ARYTM_3:68;

then t0x in X by A14;

then A60: ex s being Element of RAT+ st

( s = t0x & s *' s < two ) ;

half *' half < es by A50, A43, ARYTM_3:70;

then two + (half *' half) < two + es by ARYTM_3:76;

then two < t02s2 by A17, A18, A48, A57, ARYTM_3:76;

hence contradiction by A58, A60, ARYTM_3:69; :: thesis: verum

end;then A41: half <=' one by A12, ARYTM_3:83;

half <> one by A10, ARYTM_3:53;

then A42: half < one by A41, ARYTM_3:68;

then half < s by A40, ARYTM_3:69;

then A43: half < es by A21, ARYTM_3:70;

one <=' two by Lm13;

then one < two by ARYTM_3:68;

then A44: one *' t0 < two *' t0 by A15, ARYTM_3:80;

A45: now :: thesis: not t0 <=' one

then
one *' one < one *' t0
by ARYTM_3:80;assume A46:
t0 <=' one
; :: thesis: contradiction

then t0 *' t0 <=' t0 *' one by ARYTM_3:82;

then t0 *' t0 <=' t0 by ARYTM_3:53;

then t0 *' t0 <=' one by A46, ARYTM_3:67;

hence contradiction by A11, A17, ARYTM_3:69; :: thesis: verum

end;then t0 *' t0 <=' t0 *' one by ARYTM_3:82;

then t0 *' t0 <=' t0 by ARYTM_3:53;

then t0 *' t0 <=' one by A46, ARYTM_3:67;

hence contradiction by A11, A17, ARYTM_3:69; :: thesis: verum

then A47: one *' one < two *' t0 by A44, ARYTM_3:70;

set s = half;

consider t02s2 being Element of RAT+ such that

A48: ( (half *' half) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = half *' half ) by ARYTM_3:92;

A49: half <> 0 by A10, ARYTM_3:48;

then half *' half < half *' one by A42, ARYTM_3:80;

then A50: half *' half < half by ARYTM_3:53;

half < t0 by A42, A45, ARYTM_3:70;

then A51: half *' half < t0 by A50, ARYTM_3:70;

consider T2t9 being Element of RAT+ such that

A52: (two *' t0) *' T2t9 = one by A15, ARYTM_3:55, ARYTM_3:78;

set x = (half *' half) *' T2t9;

consider t0x being Element of RAT+ such that

A53: ( ((half *' half) *' T2t9) + t0x = t0 or t0 + t0x = (half *' half) *' T2t9 ) by ARYTM_3:92;

((half *' half) *' T2t9) *' (two *' t0) = (half *' half) *' one by A52, ARYTM_3:52;

then ( (half *' half) *' T2t9 <=' half *' half or two *' t0 <=' one ) by ARYTM_3:83;

then A54: (half *' half) *' T2t9 < t0 by A47, A51, ARYTM_3:53, ARYTM_3:69;

then A55: t0x <=' t0 by A53;

A56: ((((half *' half) *' T2t9) *' t0x) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) = ((((half *' half) *' T2t9) *' t0x) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) + (((half *' half) *' T2t9) *' t0) by ARYTM_3:51

.= (((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' t0) by A53, A54, ARYTM_3:57

.= ((((half *' half) *' T2t9) *' t0) *' one) + (((half *' half) *' T2t9) *' t0) by ARYTM_3:53

.= ((((half *' half) *' T2t9) *' t0) *' one) + ((((half *' half) *' T2t9) *' t0) *' one) by ARYTM_3:53

.= (t0 *' ((half *' half) *' T2t9)) *' two by Lm13, ARYTM_3:57

.= ((half *' half) *' T2t9) *' (t0 *' two) by ARYTM_3:52

.= (half *' half) *' one by A52, ARYTM_3:52

.= half *' half by ARYTM_3:53 ;

es <=' t0 *' t0 by A17, A18;

then half < t0 *' t0 by A43, ARYTM_3:69;

then A57: half *' half < t0 *' t0 by A50, ARYTM_3:70;

then (t02s2 + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) + (half *' half) = (t0 *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by A48, ARYTM_3:51

.= ((t0x *' (t0x + ((half *' half) *' T2t9))) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by A53, A54, ARYTM_3:57

.= (((t0x *' t0x) + (((half *' half) *' T2t9) *' t0x)) + (((half *' half) *' T2t9) *' t0)) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by ARYTM_3:57

.= ((t0x *' t0x) + (((half *' half) *' T2t9) *' t0x)) + ((((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9))) by ARYTM_3:51

.= (t0x *' t0x) + ((((half *' half) *' T2t9) *' t0x) + ((((half *' half) *' T2t9) *' t0) + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)))) by ARYTM_3:51

.= (t0x *' t0x) + (half *' half) by A56, ARYTM_3:51 ;

then t0x *' t0x = t02s2 + (((half *' half) *' T2t9) *' ((half *' half) *' T2t9)) by ARYTM_3:62;

then A58: t02s2 <=' t0x *' t0x ;

now :: thesis: not (half *' half) *' T2t9 = 0

then
t0x <> t0
by A53, A54, ARYTM_3:84;assume A59:
(half *' half) *' T2t9 = 0
; :: thesis: contradiction

end;then t0x < t0 by A55, ARYTM_3:68;

then t0x in X by A14;

then A60: ex s being Element of RAT+ st

( s = t0x & s *' s < two ) ;

half *' half < es by A50, A43, ARYTM_3:70;

then two + (half *' half) < two + es by ARYTM_3:76;

then two < t02s2 by A17, A18, A48, A57, ARYTM_3:76;

hence contradiction by A58, A60, ARYTM_3:69; :: thesis: verum

denominator t0 <> 0 by ARYTM_3:35;

then (denominator t0) *^ (denominator t0) <> {} by ORDINAL3:31;

then A62: two *^ ((denominator t0) *^ (denominator t0)) = 1 *^ ((numerator t0) *^ (numerator t0)) by A61, ARYTM_3:45, Lm11

.= (numerator t0) *^ (numerator t0) by ORDINAL2:39 ;

then consider k being natural Ordinal such that

A63: numerator t0 = 2 *^ k by Lm12;

two *^ ((denominator t0) *^ (denominator t0)) = 2 *^ (k *^ (2 *^ k)) by A62, A63, ORDINAL3:50;

then (denominator t0) *^ (denominator t0) = k *^ (2 *^ k) by ORDINAL3:33, Lm11

.= 2 *^ (k *^ k) by ORDINAL3:50 ;

then A64: ex p being natural Ordinal st denominator t0 = 2 *^ p by Lm12;

numerator t0, denominator t0 are_coprime by ARYTM_3:34;

hence contradiction by A63, A64; :: thesis: verum

then 1 in 2 by ORDINAL1:6;

then A65: 1 *^ 2 in 2 *^ 2 by ORDINAL3:19;

A66: O9 <=' a9 by ARYTM_3:64;

now :: thesis: for r being Element of RAT+ st r in X holds

( ( for t being Element of RAT+ st t <=' r holds

t in X ) & ex a9 being Element of RAT+ st

( a9 in X & r < a9 ) )

then A82:
X in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds ( ( for t being Element of RAT+ st t <=' r holds

t in X ) & ex a9 being Element of RAT+ st

( a9 in X & r < a9 ) )

let r be Element of RAT+ ; :: thesis: ( r in X implies ( ( for t being Element of RAT+ st t <=' r holds

t in X ) & ex a9 being Element of RAT+ st

( b_{2} in X & a9 < b_{2} ) ) )

assume A67: r in X ; :: thesis: ( ( for t being Element of RAT+ st t <=' r holds

t in X ) & ex a9 being Element of RAT+ st

( b_{2} in X & a9 < b_{2} ) )

then A68: ex s being Element of RAT+ st

( r = s & s *' s < two ) ;

thus for t being Element of RAT+ st t <=' r holds

t in X by A6, A67; :: thesis: ex a9 being Element of RAT+ st

( b_{2} in X & a9 < b_{2} )

end;t in X ) & ex a9 being Element of RAT+ st

( b

assume A67: r in X ; :: thesis: ( ( for t being Element of RAT+ st t <=' r holds

t in X ) & ex a9 being Element of RAT+ st

( b

then A68: ex s being Element of RAT+ st

( r = s & s *' s < two ) ;

thus for t being Element of RAT+ st t <=' r holds

t in X by A6, A67; :: thesis: ex a9 being Element of RAT+ st

( b

per cases
( r = 0 or r <> 0 )
;

end;

suppose A69:
r = 0
; :: thesis: ex a9 being Element of RAT+ st

( b_{2} in X & a9 < b_{2} )

( b

take a9 = a9; :: thesis: ( a9 in X & r < a9 )

thus a9 in X by A4, A3; :: thesis: r < a9

thus r < a9 by A66, A69, ARYTM_3:68; :: thesis: verum

end;thus a9 in X by A4, A3; :: thesis: r < a9

thus r < a9 by A66, A69, ARYTM_3:68; :: thesis: verum

suppose A70:
r <> 0
; :: thesis: ex t being Element of RAT+ st

( b_{2} in X & t < b_{2} )

( b

then consider T3r9 being Element of RAT+ such that

A71: ((r + r) + r) *' T3r9 = one by ARYTM_3:54, ARYTM_3:63;

consider rr being Element of RAT+ such that

A72: ( (r *' r) + rr = two or two + rr = r *' r ) by ARYTM_3:92;

set eps = rr *' T3r9;

( t in X & r < t ) ; :: thesis: verum

end;A71: ((r + r) + r) *' T3r9 = one by ARYTM_3:54, ARYTM_3:63;

consider rr being Element of RAT+ such that

A72: ( (r *' r) + rr = two or two + rr = r *' r ) by ARYTM_3:92;

set eps = rr *' T3r9;

A73: now :: thesis: not rr *' T3r9 = 0

assume A74:
rr *' T3r9 = 0
; :: thesis: contradiction

end;per cases
( rr = O9 or T3r9 = O9 )
by A74, ARYTM_3:78;

end;

now :: thesis: ex t being Element of RAT+ st

( t in X & r < t )end;

hence
ex t being Element of RAT+ st ( t in X & r < t )

per cases
( rr *' T3r9 < r or r <=' rr *' T3r9 )
;

end;

suppose
rr *' T3r9 < r
; :: thesis: ex t being Element of RAT+ st

( t in X & r < t )

( t in X & r < t )

then
(rr *' T3r9) *' (rr *' T3r9) < r *' (rr *' T3r9)
by A73, ARYTM_3:80;

then A75: ((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + ((rr *' T3r9) *' (rr *' T3r9)) < ((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + (r *' (rr *' T3r9)) by ARYTM_3:76;

take t = r + (rr *' T3r9); :: thesis: ( t in X & r < t )

A76: t *' t = (r *' t) + ((rr *' T3r9) *' t) by ARYTM_3:57

.= ((r *' r) + (r *' (rr *' T3r9))) + ((rr *' T3r9) *' t) by ARYTM_3:57

.= ((r *' r) + (r *' (rr *' T3r9))) + (((rr *' T3r9) *' r) + ((rr *' T3r9) *' (rr *' T3r9))) by ARYTM_3:57

.= (r *' r) + ((r *' (rr *' T3r9)) + (((rr *' T3r9) *' r) + ((rr *' T3r9) *' (rr *' T3r9)))) by ARYTM_3:51

.= (r *' r) + (((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + ((rr *' T3r9) *' (rr *' T3r9))) by ARYTM_3:51 ;

((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + (r *' (rr *' T3r9)) = ((rr *' T3r9) *' (r + r)) + (r *' (rr *' T3r9)) by ARYTM_3:57

.= (rr *' T3r9) *' ((r + r) + r) by ARYTM_3:57

.= rr *' one by A71, ARYTM_3:52

.= rr by ARYTM_3:53 ;

then t *' t < two by A68, A72, A75, A76, ARYTM_3:76;

hence t in X ; :: thesis: r < t

O9 <=' rr *' T3r9 by ARYTM_3:64;

then O9 < rr *' T3r9 by A73, ARYTM_3:68;

then r + O9 < r + (rr *' T3r9) by ARYTM_3:76;

hence r < t by ARYTM_3:50; :: thesis: verum

end;then A75: ((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + ((rr *' T3r9) *' (rr *' T3r9)) < ((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + (r *' (rr *' T3r9)) by ARYTM_3:76;

take t = r + (rr *' T3r9); :: thesis: ( t in X & r < t )

A76: t *' t = (r *' t) + ((rr *' T3r9) *' t) by ARYTM_3:57

.= ((r *' r) + (r *' (rr *' T3r9))) + ((rr *' T3r9) *' t) by ARYTM_3:57

.= ((r *' r) + (r *' (rr *' T3r9))) + (((rr *' T3r9) *' r) + ((rr *' T3r9) *' (rr *' T3r9))) by ARYTM_3:57

.= (r *' r) + ((r *' (rr *' T3r9)) + (((rr *' T3r9) *' r) + ((rr *' T3r9) *' (rr *' T3r9)))) by ARYTM_3:51

.= (r *' r) + (((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + ((rr *' T3r9) *' (rr *' T3r9))) by ARYTM_3:51 ;

((r *' (rr *' T3r9)) + ((rr *' T3r9) *' r)) + (r *' (rr *' T3r9)) = ((rr *' T3r9) *' (r + r)) + (r *' (rr *' T3r9)) by ARYTM_3:57

.= (rr *' T3r9) *' ((r + r) + r) by ARYTM_3:57

.= rr *' one by A71, ARYTM_3:52

.= rr by ARYTM_3:53 ;

then t *' t < two by A68, A72, A75, A76, ARYTM_3:76;

hence t in X ; :: thesis: r < t

O9 <=' rr *' T3r9 by ARYTM_3:64;

then O9 < rr *' T3r9 by A73, ARYTM_3:68;

then r + O9 < r + (rr *' T3r9) by ARYTM_3:76;

hence r < t by ARYTM_3:50; :: thesis: verum

suppose A77:
r <=' rr *' T3r9
; :: thesis: ex t being Element of RAT+ st

( t in X & r < t )

( t in X & r < t )

(rr *' T3r9) *' ((r + r) + r) =
rr *' one
by A71, ARYTM_3:52

.= rr by ARYTM_3:53 ;

then A78: r *' ((r + r) + r) <=' rr by A77, ARYTM_3:82;

take t = (a9 + half) *' r; :: thesis: ( t in X & r < t )

a9 < two *' one by A3, ARYTM_3:53;

then half < one by A10, ARYTM_3:82;

then one + half < two by Lm13, ARYTM_3:76;

then A79: t < two *' r by A70, ARYTM_3:80;

then A80: (two *' r) *' t < (two *' r) *' (two *' r) by A70, ARYTM_3:78, ARYTM_3:80;

a9 + half <> 0 by ARYTM_3:63;

then t *' t < (two *' r) *' t by A70, A79, ARYTM_3:78, ARYTM_3:80;

then A81: t *' t < (two *' r) *' (two *' r) by A80, ARYTM_3:70;

(r *' ((r + r) + r)) + (r *' r) = ((r *' (r + r)) + (r *' r)) + (r *' r) by ARYTM_3:57

.= (r *' (r + r)) + ((r *' r) + (r *' r)) by ARYTM_3:51

.= (r *' (two *' r)) + ((r *' r) + (r *' r)) by Lm14

.= (r *' (two *' r)) + (two *' (r *' r)) by Lm14

.= (two *' (r *' r)) + (two *' (r *' r)) by ARYTM_3:52

.= two *' (two *' (r *' r)) by Lm14

.= two *' ((two *' r) *' r) by ARYTM_3:52

.= (two *' r) *' (two *' r) by ARYTM_3:52 ;

then (two *' r) *' (two *' r) <=' two by A68, A72, A78, ARYTM_3:76;

then t *' t < two by A81, ARYTM_3:69;

hence t in X ; :: thesis: r < t

( O9 <> half & O9 <=' half ) by A10, ARYTM_3:48, ARYTM_3:64;

then O9 < half by ARYTM_3:68;

then one + O9 < one + half by ARYTM_3:76;

then one < one + half by ARYTM_3:50;

then one *' r < t by A70, ARYTM_3:80;

hence r < t by ARYTM_3:53; :: thesis: verum

end;.= rr by ARYTM_3:53 ;

then A78: r *' ((r + r) + r) <=' rr by A77, ARYTM_3:82;

take t = (a9 + half) *' r; :: thesis: ( t in X & r < t )

a9 < two *' one by A3, ARYTM_3:53;

then half < one by A10, ARYTM_3:82;

then one + half < two by Lm13, ARYTM_3:76;

then A79: t < two *' r by A70, ARYTM_3:80;

then A80: (two *' r) *' t < (two *' r) *' (two *' r) by A70, ARYTM_3:78, ARYTM_3:80;

a9 + half <> 0 by ARYTM_3:63;

then t *' t < (two *' r) *' t by A70, A79, ARYTM_3:78, ARYTM_3:80;

then A81: t *' t < (two *' r) *' (two *' r) by A80, ARYTM_3:70;

(r *' ((r + r) + r)) + (r *' r) = ((r *' (r + r)) + (r *' r)) + (r *' r) by ARYTM_3:57

.= (r *' (r + r)) + ((r *' r) + (r *' r)) by ARYTM_3:51

.= (r *' (two *' r)) + ((r *' r) + (r *' r)) by Lm14

.= (r *' (two *' r)) + (two *' (r *' r)) by Lm14

.= (two *' (r *' r)) + (two *' (r *' r)) by ARYTM_3:52

.= two *' (two *' (r *' r)) by Lm14

.= two *' ((two *' r) *' r) by ARYTM_3:52

.= (two *' r) *' (two *' r) by ARYTM_3:52 ;

then (two *' r) *' (two *' r) <=' two by A68, A72, A78, ARYTM_3:76;

then t *' t < two by A81, ARYTM_3:69;

hence t in X ; :: thesis: r < t

( O9 <> half & O9 <=' half ) by A10, ARYTM_3:48, ARYTM_3:64;

then O9 < half by ARYTM_3:68;

then one + O9 < one + half by ARYTM_3:76;

then one < one + half by ARYTM_3:50;

then one *' r < t by A70, ARYTM_3:80;

hence r < t by ARYTM_3:53; :: thesis: verum

( t in X & r < t ) ; :: thesis: verum

( ( for s being Element of RAT+ st s <=' r holds

s in A ) & ex s being Element of RAT+ st

( s in A & r < s ) ) } ;

a9 *' half = half by ARYTM_3:53;

then A83: half in X by A10, A6, A2, A5, ARYTM_3:82;

A84: now :: thesis: not X in RAT

assume A85:
X in RAT
; :: thesis: contradiction

end;per cases
( X in RAT+ or X in [:{0},RAT+:] )
by A85, XBOOLE_0:def 3;

end;

suppose A86:
X in RAT+
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( X in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,one] where k is Element of omega : verum } or X in omega )
by A86, XBOOLE_0:def 3;

end;

suppose
X in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,one] where k is Element of omega : verum }
; :: thesis: contradiction

then
X in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) }
;

then ex i, j being Element of omega st

( X = [i,j] & i,j are_coprime & j <> {} ) ;

hence contradiction by A8, TARSKI:def 2; :: thesis: verum

end;then ex i, j being Element of omega st

( X = [i,j] & i,j are_coprime & j <> {} ) ;

hence contradiction by A8, TARSKI:def 2; :: thesis: verum

suppose A87:
X in omega
; :: thesis: contradiction

2 c= X
by A5, A8, Lm11, ZFMISC_1:32;

then A88: not X in 2 by ORDINAL1:5;

end;then A88: not X in 2 by ORDINAL1:5;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( X = two or two in X )
by A87, A88, ORDINAL1:14;

end;

suppose
X = two
; :: thesis: contradiction

then
( half = 0 or half = 1 )
by A83, Lm11, TARSKI:def 2;

hence contradiction by A10, ARYTM_3:48, ARYTM_3:53; :: thesis: verum

end;hence contradiction by A10, ARYTM_3:48, ARYTM_3:53; :: thesis: verum

suppose
two in X
; :: thesis: contradiction

then
ex s being Element of RAT+ st

( s = two & s *' s < two ) ;

hence contradiction by A1, A65, Lm9; :: thesis: verum

end;( s = two & s *' s < two ) ;

hence contradiction by A1, A65, Lm9; :: thesis: verum

suppose
X in [:{0},RAT+:]
; :: thesis: contradiction

then
ex x, y being object st X = [x,y]
by RELAT_1:def 1;

hence contradiction by A8, TARSKI:def 2; :: thesis: verum

end;hence contradiction by A8, TARSKI:def 2; :: thesis: verum

now :: thesis: not two in X

then
X <> RAT+
;assume
two in X
; :: thesis: contradiction

then ex s being Element of RAT+ st

( two = s & s *' s < two ) ;

hence contradiction by A1, A65, Lm9; :: thesis: verum

end;then ex s being Element of RAT+ st

( two = s & s *' s < two ) ;

hence contradiction by A1, A65, Lm9; :: thesis: verum

then not X in {RAT+} by TARSKI:def 1;

then X in DEDEKIND_CUTS by A82, ARYTM_2:def 1, XBOOLE_0:def 5;

then X in RAT+ \/ DEDEKIND_CUTS by XBOOLE_0:def 3;

then X in REAL+ by A13, ARYTM_2:def 2, XBOOLE_0:def 5;

then X in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;

then X in REAL by A9, XBOOLE_0:def 5;

hence RAT c< REAL by A84, Lm8; :: thesis: verum