let m, n, x be Nat; :: thesis: ( n + 1,m + 1 are_coprime & n < m implies (Partial_Sums (x GeoSeq)) . n,(Partial_Sums (x GeoSeq)) . m are_coprime )
assume that
A1: n + 1,m + 1 are_coprime and
A2: n < m ; :: thesis: (Partial_Sums (x GeoSeq)) . n,(Partial_Sums (x GeoSeq)) . m are_coprime
set P = Partial_Sums (x GeoSeq);
A3: (Partial_Sums (x GeoSeq)) . 0 = (x GeoSeq) . 0 by SERIES_1:def 1
.= 1 by PREPOWER:3 ;
defpred S₁[ Nat] means for z being Nat st $1 + 1,($1 + z) + 1 are_coprime holds
(Partial_Sums (x GeoSeq)) . $1,(Partial_Sums (x GeoSeq)) . ($1 + z) are_coprime ;
A4: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A5: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
defpred S₂[ Nat] means ( k + 1,(k + $1) + 1 are_coprime implies (Partial_Sums (x GeoSeq)) . k,(Partial_Sums (x GeoSeq)) . (k + $1) are_coprime );
A6: for i being Nat st ( for n being Nat st n < i holds
S₂[n] ) holds
S₂[i]

proof

let i be Nat; :: thesis: ( ( for n being Nat st n < i holds
S₂[n] ) implies S₂[i] )
assume that
A7: for n being Nat st n < i holds
S₂[n] and
A8: k + 1,(k + i) + 1 are_coprime ; :: thesis: (Partial_Sums (x GeoSeq)) . k,(Partial_Sums (x GeoSeq)) . (k + i) are_coprime
( (k + 1) + 0 <> (k + 1) + i or ( k + 1 = (k + i) + 1 & (k + i) + 1 = 0 + 1 ) ) by A8, Th14;

per cases then ( ( k = i & i = 0 ) or i <> 0 ) ;

suppose ( k = i & i = 0 ) ; :: thesis: (Partial_Sums (x GeoSeq)) . k,(Partial_Sums (x GeoSeq)) . (k + i) are_coprime

hence ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . (k + i)) = 1 by A3, NAT_D:32; :: according to INT_2:def 3 :: thesis: verum

end;

suppose i <> 0 ; :: thesis: (Partial_Sums (x GeoSeq)) . k,(Partial_Sums (x GeoSeq)) . (k + i) are_coprime

then reconsider i1 = i - 1 as Element of NAT by INT_1:5, NAT_1:14;
A9: (k + i) + 1 = (k + 1) + i ;
then A10: (k + 1) gcd i = 1 by A8, FIB_NUM:1;
A11: (Partial_Sums (x GeoSeq)) . k,x |^ (k + 1) are_coprime by Th22;
A12: ((Partial_Sums (x GeoSeq)) . ((k + i1) + 1)) - ((Partial_Sums (x GeoSeq)) . k) = (x |^ (k + 1)) * ((Partial_Sums (x GeoSeq)) . i1) by Th24;
A13: ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . (k + i)) = ((Partial_Sums (x GeoSeq)) . k) gcd (((Partial_Sums (x GeoSeq)) . (k + i)) - ((Partial_Sums (x GeoSeq)) . k)) by Th23
.= ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) by A11, A12, FIB_NUM:2 ;

now :: thesis: ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1

per cases ( i1 < k or i1 > k or i1 = k ) by XXREAL_0:1;

suppose A14: i1 < k ; :: thesis: ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1

then reconsider z = k - i1 as Element of NAT by INT_1:5;
( i1 + 1,(i1 + z) + 1 are_coprime implies (Partial_Sums (x GeoSeq)) . i1,(Partial_Sums (x GeoSeq)) . (i1 + z) are_coprime ) by A14, A5;
hence ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1 by A8, A9, FIB_NUM:1; :: thesis: verum

end;

suppose i1 > k ; :: thesis: ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1

then consider j being Nat such that
A15: i1 = k + j by NAT_1:10;
A16: j = i - (1 + k) by A15;
k + 1,(k + j) + 1 are_coprime by A8, A9, A15, FIB_NUM:1;
then (Partial_Sums (x GeoSeq)) . k,(Partial_Sums (x GeoSeq)) . (k + j) are_coprime by A16, A7, XREAL_1:44;
hence ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1 by A15; :: thesis: verum

end;

suppose A17: i1 = k ; :: thesis: ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1

then (k + 1) gcd i = i by NAT_D:32;
hence ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . i1) = 1 by A10, A17, A3; :: thesis: verum

end;

end;

end;

hence ((Partial_Sums (x GeoSeq)) . k) gcd ((Partial_Sums (x GeoSeq)) . (k + i)) = 1 by A13; :: according to INT_2:def 3 :: thesis: verum

end;

end;

end;

for k being Nat holds S₂[k] from NAT_1:sch 4(A6);
hence S₁[k] ; :: thesis: verum

end;

A18: for k being Nat holds S₁[k] from NAT_1:sch 4(A4);
reconsider z = m - n as Element of NAT by A2, INT_1:5;
m = z + n ;
hence (Partial_Sums (x GeoSeq)) . n,(Partial_Sums (x GeoSeq)) . m are_coprime by A1, A18; :: thesis: verum