let r be real number ; :: thesis: ( r is rational iff ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0 )
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 number ;
frac r >= 0 by INT_1:69;
then consider m, n being Nat such that
A1: n <> 0 and
A2: frac r = m / n by Th7;
A3: n > 0 by A1;
frac r < 1 by INT_1:69;
then A4: m < n by A2, A3, XREAL_1:183;
set fd = divSeq n,m;
set fm = modSeq n,m;

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

suppose m = 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
(scf r) . m = 0

then A5: r is integer by A2;
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 A5, Th30; :: thesis: verum

end;

suppose A6: 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
A7: (divSeq n,m) . k = 0 and
(modSeq n,m) . k = 0 by Th25;
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 A8: a >= k + 1 ; :: thesis: (scf r) . a = 0
k + 0 < k + 1 by XREAL_1:8;
then A9: k < a by A8, XXREAL_0:2;
1 <= k + 1 by NAT_1:11;
then reconsider a1 = a - 1 as Element of NAT by A8, INT_1:18, XXREAL_0:2;
A10: a = a1 + 1 ;

A11: now

assume A12: k = 0 ; :: thesis: contradiction
( m <= 0 or n div m <> 0 ) by A4, NAT_2:14;
hence contradiction by A6, A7, A12, Def3; :: thesis: verum

end;

A13: k <= a1 by A9, A10, NAT_1:13;
(scf r) . a = (scf (1 / (frac r))) . a1 by A10, Th37
.= (scf (n / m)) . a1 by A2, XCMPLX_1:57
.= (divSeq n,m) . a1 by Th41
.= 0 by A7, A11, A13, Th17 ;
hence (scf r) . a = 0 ; :: thesis: verum

end;

end;

end;

given n being Nat such that A14: for m being Nat st m >= n holds
(scf r) . m = 0 ; :: thesis: r is rational
defpred S₂[ Nat] means for s being real number st ( for m being Nat st m >= $1 holds
(scf s) . m = 0 ) holds
s is rational ;
A15: S₂[ 0 ]

proof

let s be real number ; :: thesis: ( ( for m being Nat st m >= 0 holds
(scf s) . m = 0 ) implies s is rational )
assume A16: for m being Nat st m >= 0 holds
(scf s) . m = 0 ; :: thesis: s is rational
for m being Nat holds (scf s) . m = 0 by A16;
hence s is rational by Th34; :: thesis: verum

end;

A17: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A18: S₂[m] ; :: thesis: S₂[m + 1]
let s be real number ; :: thesis: ( ( for m being Nat st m >= m + 1 holds
(scf s) . m = 0 ) implies s is rational )
assume A19: 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 A21: n + 1 >= m + 1 by XREAL_1:8;
thus (scf (1 / (s - ((scf s) . 0 )))) . n = (scf s) . (n + 1) by Lm8
.= 0 by A19, A21 ; :: thesis: verum

end;

then reconsider B = 1 / (s - ((scf s) . 0 )) as rational number by A18;
((scf s) . 0 ) + (1 / B) is rational ;
hence s is rational ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A15, A17);
hence r is rational by A14; :: thesis: verum