let m, n be Nat; :: thesis: (Partial_Sums (m GeoSeq)) . n,m |^ (n + 1) are_coprime
set P = (Partial_Sums (m GeoSeq)) . n;
assume not (Partial_Sums (m GeoSeq)) . n,m |^ (n + 1) are_coprime ; :: thesis: contradiction
then consider p being Prime such that
A1: p divides (Partial_Sums (m GeoSeq)) . n and
A2: p divides m |^ (n + 1) by PYTHTRIP:def 2;
p divides ((Partial_Sums (m GeoSeq)) . n) - 1 by A2, Th21, NAT_3:5;
then p divides ((Partial_Sums (m GeoSeq)) . n) - (((Partial_Sums (m GeoSeq)) . n) - 1) by A1, INT_5:1;
then p = 1 by WSIERP_1:15;
hence contradiction by INT_2:def 4; :: thesis: verum