defpred S1[ Element of RAT+ ] means $1 *' $1 < two;
set X = { s where s is Element of RAT+ : S1[s] } ;
reconsider X = { s where s is Element of RAT+ : S1[s] } as Subset of RAT+ from DOMAIN_1:sch 7();
 A1: ( 2 *^ 2 = two *' two & 1 *^ 2 = 2 ) by ARYTM_3:65, ORDINAL2:56;
2 = succ 1
.= 1 \/ {1} by ORDINAL1:def 1 ;
then A2: a9 <=' two by Lm10, XBOOLE_1:7;
then A3: a9 < two by ARYTM_3:75;
A4: a9 *' a9 = a9 by ARYTM_3:59;
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
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:90;
then t *' t <=' r *' r by ARYTM_3:74;
then t *' t < two by A7, ARYTM_3:76;
hence t in X ; :: thesis: verum
end;
then A8: 0 in X by A5, ARYTM_3:71;
now
assume X = [0,0] ; :: thesis: contradiction
then X = {{0},{0}} by ENUMSET1:69
.= {{0}} by ENUMSET1:69 ;
hence contradiction by A8, TARSKI:def 1; :: thesis: verum
end;
then A9: not X in {[0,0]} by TARSKI:def 1;
reconsider 09 = 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:61;
A11: one <=' two by Lm13, ARYTM_3:def 13;
then A12: one < two by ARYTM_3:75;
A13: now
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;
now
assume A16: t0 *' t0 <> two ; :: thesis: contradiction
per cases ( t0 *' t0 < two or two < t0 *' t0 ) by A16, ARYTM_3:73;
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;
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:100;
A19: now
assume 09 = es ; :: thesis: contradiction
then two + es = two by ARYTM_3:56;
hence contradiction by A17, A18, ARYTM_3:def 13; :: thesis: verum
end;
09 <=' es by ARYTM_3:71;
then 09 < es by A19, ARYTM_3:75;
then consider s being Element of RAT+ such that
A20: 09 < s and
A21: s < es by ARYTM_3:101;
now
per cases ( s < one or one <=' s ) ;
suppose A22: s < one ; :: thesis: contradiction
A23: s <> 0 by A20;
then s *' s < s *' one by A22, ARYTM_3:88;
then A24: s *' s < s by ARYTM_3:59;
then A27: one *' one < one *' t0 by ARYTM_3:88;
one *' t0 < two *' t0 by A12, A15, ARYTM_3:88;
then A28: one *' one < two *' t0 by A27, ARYTM_3:77;
consider t02s2 being Element of RAT+ such that
A29: ( (s *' s) + t02s2 = t0 *' t0 or (t0 *' t0) + t02s2 = s *' s ) by ARYTM_3:100;
s < t0 by A22, A25, ARYTM_3:77;
then A30: s *' s < t0 by A24, ARYTM_3:77;
consider 2t9 being Element of RAT+ such that
A31: (two *' t0) *' 2t9 = one by A15, ARYTM_3:61, ARYTM_3:86;
set x = (s *' s) *' 2t9;
consider t0x being Element of RAT+ such that
A32: ( ((s *' s) *' 2t9) + t0x = t0 or t0 + t0x = (s *' s) *' 2t9 ) by ARYTM_3:100;
((s *' s) *' 2t9) *' (two *' t0) = (s *' s) *' one by A31, ARYTM_3:58;
then ( (s *' s) *' 2t9 <=' s *' s or two *' t0 <=' one ) by ARYTM_3:91;
then A33: (s *' s) *' 2t9 < t0 by A28, A30, ARYTM_3:59, ARYTM_3:76;
then A34: t0x <=' t0 by A32, ARYTM_3:def 13;
A35: ((((s *' s) *' 2t9) *' t0x) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) = ((((s *' s) *' 2t9) *' t0x) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) + (((s *' s) *' 2t9) *' t0) by ARYTM_3:57
.= (((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' t0) by A32, A33, ARYTM_3:63, ARYTM_3:def 13
.= ((((s *' s) *' 2t9) *' t0) *' one) + (((s *' s) *' 2t9) *' t0) by ARYTM_3:59
.= ((((s *' s) *' 2t9) *' t0) *' one) + ((((s *' s) *' 2t9) *' t0) *' one) by ARYTM_3:59
.= (t0 *' ((s *' s) *' 2t9)) *' two by Lm13, ARYTM_3:63
.= ((s *' s) *' 2t9) *' (t0 *' two) by ARYTM_3:58
.= (s *' s) *' one by A31, ARYTM_3:58
.= s *' s by ARYTM_3:59 ;
es <=' t0 *' t0 by A17, A18, ARYTM_3:def 13;
then s < t0 *' t0 by A21, ARYTM_3:76;
then A36: s *' s < t0 *' t0 by A24, ARYTM_3:77;
then (t02s2 + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) + (s *' s) = ((t0x + ((s *' s) *' 2t9)) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by A29, A32, A33, ARYTM_3:57, ARYTM_3:def 13
.= ((t0x *' (t0x + ((s *' s) *' 2t9))) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by A32, A33, ARYTM_3:63, ARYTM_3:def 13
.= (((t0x *' t0x) + (((s *' s) *' 2t9) *' t0x)) + (((s *' s) *' 2t9) *' t0)) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by ARYTM_3:63
.= ((t0x *' t0x) + (((s *' s) *' 2t9) *' t0x)) + ((((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9))) by ARYTM_3:57
.= (t0x *' t0x) + ((((s *' s) *' 2t9) *' t0x) + ((((s *' s) *' 2t9) *' t0) + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)))) by ARYTM_3:57
.= (t0x *' t0x) + (s *' s) by A35, ARYTM_3:57 ;
then t0x *' t0x = t02s2 + (((s *' s) *' 2t9) *' ((s *' s) *' 2t9)) by ARYTM_3:69;
then A37: t02s2 <=' t0x *' t0x by ARYTM_3:def 13;
now
assume A38: (s *' s) *' 2t9 = 0 ; :: thesis: contradiction
end;
then t0x <> t0 by A32, A33, ARYTM_3:92, ARYTM_3:def 13;
then t0x < t0 by A34, ARYTM_3:75;
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:77;
then two + (s *' s) < two + es by ARYTM_3:83;
then two < t02s2 by A17, A18, A29, A36, ARYTM_3:83, ARYTM_3:def 13;
hence contradiction by A37, A39, ARYTM_3:76; :: thesis: verum
end;
suppose A40: one <=' s ; :: thesis: contradiction
half *' two = one *' one by A10, ARYTM_3:59;
then A41: half <=' one by A12, ARYTM_3:91;
half <> one by A10, ARYTM_3:59;
then A42: half < one by A41, ARYTM_3:75;
then half < s by A40, ARYTM_3:76;
then A43: half < es by A21, ARYTM_3:77;
one <=' two by Lm13, ARYTM_3:def 13;
then one < two by ARYTM_3:75;
then A44: one *' t0 < two *' t0 by A15, ARYTM_3:88;
then one *' one < one *' t0 by ARYTM_3:88;
then A47: one *' one < two *' t0 by A44, ARYTM_3:77;
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:100;
A49: half <> 0 by A10, ARYTM_3:54;
then half *' half < half *' one by A42, ARYTM_3:88;
then A50: half *' half < half by ARYTM_3:59;
half < t0 by A42, A45, ARYTM_3:77;
then A51: half *' half < t0 by A50, ARYTM_3:77;
consider 2t9 being Element of RAT+ such that
A52: (two *' t0) *' 2t9 = one by A15, ARYTM_3:61, ARYTM_3:86;
set x = (half *' half) *' 2t9;
consider t0x being Element of RAT+ such that
A53: ( ((half *' half) *' 2t9) + t0x = t0 or t0 + t0x = (half *' half) *' 2t9 ) by ARYTM_3:100;
((half *' half) *' 2t9) *' (two *' t0) = (half *' half) *' one by A52, ARYTM_3:58;
then ( (half *' half) *' 2t9 <=' half *' half or two *' t0 <=' one ) by ARYTM_3:91;
then A54: (half *' half) *' 2t9 < t0 by A47, A51, ARYTM_3:59, ARYTM_3:76;
then A55: t0x <=' t0 by A53, ARYTM_3:def 13;
A56: ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) = ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' t0) by ARYTM_3:57
.= (((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' t0) by A53, A54, ARYTM_3:63, ARYTM_3:def 13
.= ((((half *' half) *' 2t9) *' t0) *' one) + (((half *' half) *' 2t9) *' t0) by ARYTM_3:59
.= ((((half *' half) *' 2t9) *' t0) *' one) + ((((half *' half) *' 2t9) *' t0) *' one) by ARYTM_3:59
.= (t0 *' ((half *' half) *' 2t9)) *' two by Lm13, ARYTM_3:63
.= ((half *' half) *' 2t9) *' (t0 *' two) by ARYTM_3:58
.= (half *' half) *' one by A52, ARYTM_3:58
.= half *' half by ARYTM_3:59 ;
es <=' t0 *' t0 by A17, A18, ARYTM_3:def 13;
then half < t0 *' t0 by A43, ARYTM_3:76;
then A57: half *' half < t0 *' t0 by A50, ARYTM_3:77;
then (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (half *' half) = (t0 *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by A48, ARYTM_3:57, ARYTM_3:def 13
.= ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by A53, A54, ARYTM_3:63, ARYTM_3:def 13
.= (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' t0)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by ARYTM_3:63
.= ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + ((((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) by ARYTM_3:57
.= (t0x *' t0x) + ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' t0) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) by ARYTM_3:57
.= (t0x *' t0x) + (half *' half) by A56, ARYTM_3:57 ;
then t0x *' t0x = t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) by ARYTM_3:69;
then A58: t02s2 <=' t0x *' t0x by ARYTM_3:def 13;
now
assume A59: (half *' half) *' 2t9 = 0 ; :: thesis: contradiction
end;
then t0x <> t0 by A53, A54, ARYTM_3:92, ARYTM_3:def 13;
then t0x < t0 by A55, ARYTM_3:75;
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:77;
then two + (half *' half) < two + es by ARYTM_3:83;
then two < t02s2 by A17, A18, A48, A57, ARYTM_3:83, ARYTM_3:def 13;
hence contradiction by A58, A60, ARYTM_3:76; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
then A61: two / 1 = ((numerator t0) *^ (numerator t0)) / ((denominator t0) *^ (denominator t0)) by ARYTM_3:46;
denominator t0 <> 0 by ARYTM_3:41;
then (denominator t0) *^ (denominator t0) <> {} by ORDINAL3:34;
then A62: two *^ ((denominator t0) *^ (denominator t0)) = 1 *^ ((numerator t0) *^ (numerator t0)) by A61, ARYTM_3:51
.= (numerator t0) *^ (numerator t0) by ORDINAL2:56 ;
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:58;
then (denominator t0) *^ (denominator t0) = k *^ (2 *^ k) by ORDINAL3:36
.= 2 *^ (k *^ k) by ORDINAL3:58 ;
then A64: ex p being natural Ordinal st denominator t0 = 2 *^ p by Lm12;
numerator t0, denominator t0 are_relative_prime by ARYTM_3:40;
hence contradiction by A63, A64, ARYTM_3:def 2; :: thesis: verum
end;
2 = succ 1 ;
then 1 in 2 by ORDINAL1:10;
then A65: 1 *^ 2 in 2 *^ 2 by ORDINAL3:22;
A66: 09 <=' a9 by ARYTM_3:71;
now
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
( b2 in X & a9 < b2 ) ) )
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
( b2 in X & a9 < b2 ) )
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
( b2 in X & a9 < b2 )
per cases ( r = 0 or r <> 0 ) ;
suppose A69: r = 0 ; :: thesis: ex a9 being Element of RAT+ st
( b2 in X & a9 < b2 )
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:75; :: thesis: verum
end;
suppose A70: r <> 0 ; :: thesis: ex t being Element of RAT+ st
( b2 in X & t < b2 )
then consider 3r9 being Element of RAT+ such that
A71: ((r + r) + r) *' 3r9 = one by ARYTM_3:60, ARYTM_3:70;
consider rr being Element of RAT+ such that
A72: ( (r *' r) + rr = two or two + rr = r *' r ) by ARYTM_3:100;
set eps = rr *' 3r9;
A73: now
assume A74: rr *' 3r9 = 0 ; :: thesis: contradiction
end;
now
per cases ( rr *' 3r9 < r or r <=' rr *' 3r9 ) ;
suppose rr *' 3r9 < r ; :: thesis: ex t being Element of RAT+ st
( t in X & r < t )
then (rr *' 3r9) *' (rr *' 3r9) < r *' (rr *' 3r9) by A73, ARYTM_3:88;
then A75: ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)) < ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + (r *' (rr *' 3r9)) by ARYTM_3:83;
take t = r + (rr *' 3r9); :: thesis: ( t in X & r < t )
A76: t *' t = (r *' t) + ((rr *' 3r9) *' t) by ARYTM_3:63
.= ((r *' r) + (r *' (rr *' 3r9))) + ((rr *' 3r9) *' t) by ARYTM_3:63
.= ((r *' r) + (r *' (rr *' 3r9))) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) by ARYTM_3:63
.= (r *' r) + ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) by ARYTM_3:57
.= (r *' r) + (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))) by ARYTM_3:57 ;
((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + (r *' (rr *' 3r9)) = ((rr *' 3r9) *' (r + r)) + (r *' (rr *' 3r9)) by ARYTM_3:63
.= (rr *' 3r9) *' ((r + r) + r) by ARYTM_3:63
.= rr *' one by A71, ARYTM_3:58
.= rr by ARYTM_3:59 ;
then t *' t < two by A68, A72, A75, A76, ARYTM_3:83, ARYTM_3:def 13;
hence t in X ; :: thesis: r < t
09 <=' rr *' 3r9 by ARYTM_3:71;
then 09 < rr *' 3r9 by A73, ARYTM_3:75;
then r + 09 < r + (rr *' 3r9) by ARYTM_3:83;
hence r < t by ARYTM_3:56; :: thesis: verum
end;
suppose A77: r <=' rr *' 3r9 ; :: thesis: ex t being Element of RAT+ st
( t in X & r < t )
(rr *' 3r9) *' ((r + r) + r) = rr *' one by A71, ARYTM_3:58
.= rr by ARYTM_3:59 ;
then A78: r *' ((r + r) + r) <=' rr by A77, ARYTM_3:90;
take t = (a9 + half) *' r; :: thesis: ( t in X & r < t )
a9 < two *' one by A3, ARYTM_3:59;
then half < one by A10, ARYTM_3:90;
then one + half < two by Lm13, ARYTM_3:83;
then A79: t < two *' r by A70, ARYTM_3:88;
then A80: (two *' r) *' t < (two *' r) *' (two *' r) by A70, ARYTM_3:86, ARYTM_3:88;
a9 + half <> 0 by ARYTM_3:70;
then t *' t < (two *' r) *' t by A70, A79, ARYTM_3:86, ARYTM_3:88;
then A81: t *' t < (two *' r) *' (two *' r) by A80, ARYTM_3:77;
(r *' ((r + r) + r)) + (r *' r) = ((r *' (r + r)) + (r *' r)) + (r *' r) by ARYTM_3:63
.= (r *' (r + r)) + ((r *' r) + (r *' r)) by ARYTM_3:57
.= (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:58
.= two *' (two *' (r *' r)) by Lm14
.= two *' ((two *' r) *' r) by ARYTM_3:58
.= (two *' r) *' (two *' r) by ARYTM_3:58 ;
then (two *' r) *' (two *' r) <=' two by A68, A72, A78, ARYTM_3:83, ARYTM_3:def 13;
then t *' t < two by A81, ARYTM_3:76;
hence t in X ; :: thesis: r < t
( 09 <> half & 09 <=' half ) by A10, ARYTM_3:54, ARYTM_3:71;
then 09 < half by ARYTM_3:75;
then one + 09 < one + half by ARYTM_3:83;
then one < one + half by ARYTM_3:56;
then one *' r < t by A70, ARYTM_3:88;
hence r < t by ARYTM_3:59; :: thesis: verum
end;
end;
end;
hence ex t being Element of RAT+ st
( t in X & r < t ) ; :: thesis: verum
end;
end;
end;
then A82: X in { 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 ) ) } ;
a9 *' half = half by ARYTM_3:59;
then A83: half in X by A10, A6, A2, A5, ARYTM_3:90;
A84: now
assume A85: X in RAT ; :: thesis: contradiction
per cases ( X in RAT+ or X in [:{0},RAT+:] ) by A85, XBOOLE_0:def 3;
suppose A86: X in RAT+ ; :: thesis: contradiction
now
per cases ( X in { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & j <> {} ) } \ { [k,one] where k is Element of omega : verum } or X in omega ) by A86, XBOOLE_0:def 3;
suppose X in { [i,j] where i, j is Element of omega : ( i,j are_relative_prime & 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_relative_prime & j <> {} ) } ;
then ex i, j being Element of omega st
( X = [i,j] & i,j are_relative_prime & j <> {} ) ;
hence contradiction by A8, TARSKI:def 2; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
now
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 X <> RAT+ ;
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, XBOOLE_0:def 8; :: thesis: verum