let r be Real; :: thesis: ( r is rational iff ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 )
defpred S2[ Nat] means for s being Real st ( for m being Nat st m >= $1 holds
(scf s) . m = 0 ) holds
s is rational ;
A1: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A2: S2[m] ; :: thesis: S2[m + 1]
let s be Real; :: thesis: ( ( for m being Nat st m >= m + 1 holds
(scf s) . m = 0 ) implies s is rational )
assume A3: for n being Nat st n >= m + 1 holds
(scf s) . n = 0 ; :: thesis: s is rational
set B = 1 / (s - ((scf s) . 0));
for n being Nat st n >= m holds
(scf (1 / (s - ((scf s) . 0)))) . n = 0
proof
let n be Nat; :: thesis: ( n >= m implies (scf (1 / (s - ((scf s) . 0)))) . n = 0 )
assume n >= m ; :: thesis: (scf (1 / (s - ((scf s) . 0)))) . n = 0
then A4: n + 1 >= m + 1 by XREAL_1:6;
thus (scf (1 / (s - ((scf s) . 0)))) . n = (scf s) . (n + 1) by Lm6
.= 0 by A3, A4 ; :: thesis: verum
end;
then reconsider B = 1 / (s - ((scf s) . 0)) as Rational by A2;
((scf s) . 0) + (1 / B) is rational ;
hence s is rational ; :: thesis: verum
end;
thus ( r is rational implies ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 ) :: thesis: ( ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 implies r is rational )
proof
assume r is rational ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0
then reconsider r = r as Rational ;
consider m, n being Nat such that
A5: n <> 0 and
A6: frac r = m / n by Th7, INT_1:43;
frac r < 1 by INT_1:43;
then A7: m < n by A5, A6, XREAL_1:181;
set fm = modSeq (n,m);
set fd = divSeq (n,m);
per cases ( m = 0 or m <> 0 ) ;
suppose A8: m = 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0
take 1 ; :: thesis: for m being Nat st m >= 1 holds
(scf r) . m = 0
let a be Nat; :: thesis: ( a >= 1 implies (scf r) . a = 0 )
assume a >= 1 ; :: thesis: (scf r) . a = 0
then ex x being Nat st a = x + 1 by NAT_1:6;
hence (scf r) . a = 0 by A6, A8, Th30; :: thesis: verum
end;
suppose A9: m <> 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0
consider k being Nat such that
A10: (divSeq (n,m)) . k = 0 and
(modSeq (n,m)) . k = 0 by Th25;
A11: now :: thesis: not k = 0
assume A12: k = 0 ; :: thesis: contradiction
( m <= 0 or n div m <> 0 ) by A7, NAT_2:12;
hence contradiction by A9, A10, A12, Def2; :: thesis: verum
end;
take k + 1 ; :: thesis: for m being Nat st m >= k + 1 holds
(scf r) . m = 0
let a be Nat; :: thesis: ( a >= k + 1 implies (scf r) . a = 0 )
assume A13: a >= k + 1 ; :: thesis: (scf r) . a = 0
1 <= k + 1 by NAT_1:11;
then reconsider a1 = a - 1 as Element of NAT by A13, INT_1:5, XXREAL_0:2;
A14: a = a1 + 1 ;
k + 0 < k + 1 by XREAL_1:6;
then k < a by A13, XXREAL_0:2;
then A15: k <= a1 by A14, NAT_1:13;
(scf r) . a = (scf (1 / (frac r))) . a1 by A14, Th37
.= (scf (n / m)) . a1 by A6, XCMPLX_1:57
.= (divSeq (n,m)) . a1 by Th41
.= 0 by A10, A11, A15, Th17 ;
hence (scf r) . a = 0 ; :: thesis: verum
end;
end;
end;
given n being Nat such that A16: for m being Nat st m >= n holds
(scf r) . m = 0 ; :: thesis: r is rational
A17: S2[ 0 ]
proof
let s be Real; :: thesis: ( ( for m being Nat st m >= 0 holds
(scf s) . m = 0 ) implies s is rational )
assume for m being Nat st m >= 0 holds
(scf s) . m = 0 ; :: thesis: s is rational
then for m being Nat holds (scf s) . m = 0 ;
hence s is rational by Th34; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A17, A1);
 hence r is rational by A16; :: thesis: verum