let n be Nat; :: thesis: for r being Real
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; :: 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 S2[ 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 S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[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: S2[k + 1]
then A2: n1 gcd n2 = 1 ;
n3 = (n4 * n1) + n2 by Def6;
hence S2[k + 1] by A2, EULER_1:8; :: thesis: verum
end;
A3: S2[ 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, Def6; :: thesis: verum
end;
for n being Nat holds S2[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