let n be Nat; :: thesis: for r being real number
for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds
n1 gcd n2 = 1
let r be real number ; :: thesis: for n1, n2 being Nat st n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n holds
n1 gcd n2 = 1
let n1, n2 be Nat; :: thesis: ( n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n implies n1 gcd n2 = 1 )
set s = scf r;
set s2 = c_d r;
defpred S₂[ Nat] means for n1, n2 being Nat st n1 = (c_d r) . ($1 + 1) & n2 = (c_d r) . $1 holds
n1 gcd n2 = 1;
A1: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
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 n3 = (c_d r) . (k + 2) as Element of NAT by Th50;
reconsider n2 = (c_d r) . k as Element of NAT by Th50;
reconsider n1 = (c_d r) . (k + 1) as Element of NAT by Th50;
assume for n1, n2 being Nat st n1 = (c_d r) . (k + 1) & n2 = (c_d r) . k holds
n1 gcd n2 = 1 ; :: thesis: S₂[k + 1]
then A2: n1 gcd n2 = 1 ;
n3 = (n4 * n1) + n2 by Def7;
hence S₂[k + 1] by A2, EULER_1:8; :: thesis: verum

end;

A3: S₂[ 0 ]

proof

let n1, n2 be Nat; :: thesis: ( n1 = (c_d r) . (0 + 1) & n2 = (c_d r) . 0 implies n1 gcd n2 = 1 )
assume that
n1 = (c_d r) . (0 + 1) and
A4: n2 = (c_d r) . 0 ; :: thesis: n1 gcd n2 = 1
n1 gcd 1 = 1 by NEWTON:51;
hence n1 gcd n2 = 1 by A4, Def7; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A3, A1);
hence ( n1 = (c_d r) . (n + 1) & n2 = (c_d r) . n implies n1 gcd n2 = 1 ) ; :: thesis: verum