let r be real number ; :: 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 S₂[ 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 S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[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: S₂[k + 1]
then A3: n1 gcd n2 = 1 ;
n3 = (n4 * n1) + n2 by Def6;
hence S₂[k + 1] by A3, EULER_1:8; :: thesis: verum

end;

A4: S₂[ 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, Def6;
then A7: n1 = (u * n2) + 1 by A6, Def6;
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 S₂[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