let r be Real; :: thesis: for n1, n2 being Nat st (scf r) . 0 > 0 holds
for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1
let n1, n2 be Nat; :: thesis: ( (scf r) . 0 > 0 implies for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1 )
set s1 = c_n r;
set s = scf r;
defpred S2[ Nat] means for n1, n2 being Nat st n1 = (c_n r) . ($1 + 1) & n2 = (c_n r) . $1 holds
n1 gcd n2 = 1;
assume A1: (scf r) . 0 > 0 ; :: thesis: for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1
A2: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
reconsider n3 = (c_n r) . (k + 2) as Element of NAT by A1, Th44;
reconsider n2 = (c_n r) . k as Element of NAT by A1, Th44;
k + 2 >= 0 + 1 by XREAL_1:7;
then reconsider n4 = (scf r) . (k + 2) as Element of NAT by Th38, INT_1:3;
reconsider n1 = (c_n r) . (k + 1) as Element of NAT by A1, Th44;
assume for n1, n2 being Nat st n1 = (c_n r) . (k + 1) & n2 = (c_n r) . k holds
n1 gcd n2 = 1 ; :: thesis: S2[k + 1]
then A3: n1 gcd n2 = 1 ;
n3 = (n4 * n1) + n2 by Def5;
hence S2[k + 1] by A3, EULER_1:8; :: thesis: verum
end;
A4: S2[ 0 ]
proof
reconsider u = (scf r) . 1 as Element of NAT by Th38, INT_1:3;
let n1, n2 be Nat; :: thesis: ( n1 = (c_n r) . (0 + 1) & n2 = (c_n r) . 0 implies n1 gcd n2 = 1 )
assume that
A5: n1 = (c_n r) . (0 + 1) and
A6: n2 = (c_n r) . 0 ; :: thesis: n1 gcd n2 = 1
n1 = (u * ((scf r) . 0)) + 1 by A5, Def5;
then A7: n1 = (u * n2) + 1 by A6, Def5;
1 gcd n2 = 1 by NEWTON:51;
hence n1 gcd n2 = 1 by A7, EULER_1:8; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A4, A2);
 hence for n being Nat st n1 = (c_n r) . (n + 1) & n2 = (c_n r) . n holds
n1 gcd n2 = 1 ; :: thesis: verum