let m be positive Integer; :: thesis: for a being Nat st a > 1 holds
(((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m
let a be Nat; :: thesis: ( a > 1 implies (((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m )
assume a: a > 1 ; :: thesis: (((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m
set d = (((a |^ m) - 1) div (a - 1)) gcd (a - 1);
set d1 = (a - 1) gcd m;
m >= 0 + 1 by INT_1:7;
then reconsider m0 = m as Nat by POLYFORM:3;
reconsider m1 = m0 - 1 as Nat by INT_1:74;
deffunc H₁( Nat) -> set = (a |^ ($1 + 1)) - 1;
consider f being XFinSequence such that
f: ( len f = m1 & ( for i being Nat st i in m1 holds
f . i = H₁(i) ) ) from AFINSQ_1:sch 2();
rng f c= INT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng f or o in INT )
assume o in rng f ; :: thesis: o in INT
then consider x being object such that
x: ( x in dom f & o = f . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by x;
o = (a |^ (x + 1)) - 1 by f, x;
hence o in INT by INT_1:def 2; :: thesis: verum

end;

then reconsider f = f as XFinSequence of INT by RELAT_1:def 19;
d2: ( (((a |^ m) - 1) div (a - 1)) gcd (a - 1) divides a - 1 & (((a |^ m) - 1) div (a - 1)) gcd (a - 1) divides ((a |^ m) - 1) div (a - 1) ) by INT_2:def 2;

now :: thesis: for i being Nat st i in dom f holds
a - 1 divides f . i

let i be Nat; :: thesis: ( i in dom f implies a - 1 divides f . i )
assume i in dom f ; :: thesis: a - 1 divides f . i
then f . i = (a |^ (i + 1)) - 1 by f;
hence a - 1 divides f . i by lemdiv; :: thesis: verum

end;

then ad: a - 1 divides Sum f by NUMERAL2:16;
then ds: (((a |^ m) - 1) div (a - 1)) gcd (a - 1) divides Sum f by d2, INT_2:9;
ss: ((a |^ m) - 1) div (a - 1) = (Sum f) + m by a, f, lempowers;
then (((a |^ m) - 1) div (a - 1)) gcd (a - 1) divides (Sum f) + m by d2;
then d1: (((a |^ m) - 1) div (a - 1)) gcd (a - 1) divides m by ds, INT_2:1;

now :: thesis: for q being Integer st q divides a - 1 & q divides m holds
q divides (((a |^ m) - 1) div (a - 1)) gcd (a - 1)

let q be Integer; :: thesis: ( q divides a - 1 & q divides m implies q divides (((a |^ m) - 1) div (a - 1)) gcd (a - 1) )
assume q: ( q divides a - 1 & q divides m ) ; :: thesis: q divides (((a |^ m) - 1) div (a - 1)) gcd (a - 1)
then q divides Sum f by ad, INT_2:9;
then q divides ((a |^ m) - 1) div (a - 1) by ss, q, WSIERP_1:4;
hence q divides (((a |^ m) - 1) div (a - 1)) gcd (a - 1) by q, INT_2:def 2; :: thesis: verum

end;

hence (((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m by d1, d2, INT_2:def 2; :: thesis: verum