let n be Nat; :: thesis: for a being non trivial Nat holds Py (a,n),n are_congruent_mod a - 1
let a be non trivial Nat; :: thesis: Py (a,n),n are_congruent_mod a - 1
set A = a - 1;
A1: (a ^2) -' 1 = (a ^2) - 1 by NAT_1:14, XREAL_1:233;
consider Fy, Fx being FinSequence of NAT such that
A2: ( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] ) and
A3: for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) and
( (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) ) by Th12;

per cases ( n = 0 or n <> 0 ) ;

suppose A4: n = 0 ; :: thesis: Py (a,n),n are_congruent_mod a - 1

then Py (a,n) = 0 by Th6;
hence Py (a,n),n are_congruent_mod a - 1 by A4, INT_1:11; :: thesis: verum

end;

suppose A5: n <> 0 ; :: thesis: Py (a,n),n are_congruent_mod a - 1

for i being Nat st 1 < i & i <= len Fy holds
(Fy . i) mod (a - 1) = 0

proof

let i be Nat; :: thesis: ( 1 < i & i <= len Fy implies (Fy . i) mod (a - 1) = 0 )
assume A6: ( 1 < i & i <= len Fy ) ; :: thesis: (Fy . i) mod (a - 1) = 0
i -' 1 = i - 1 by A6, XREAL_1:233;
then i -' 1 <> 0 by A6;
then reconsider ii = (i -' 1) - 1 as Element of NAT by NAT_1:20;
i -' 1 = ii + 1 ;
then A7: ((a ^2) -' 1) |^ (i -' 1) = ((a - 1) * (a + 1)) * (((a ^2) -' 1) |^ ii) by A1, NEWTON:6;
[\((n + 1) / 2)/] <= (n + 1) / 2 by INT_1:def 6;
then i <= (n + 1) / 2 by A2, A6, XXREAL_0:2;
then Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) by A6, A3
.= ((((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (a + 1)) * (((a ^2) -' 1) |^ ii)) * (a - 1) by A7 ;
then a - 1 divides Fy . i by INT_1:def 3;
hence (Fy . i) mod (a - 1) = 0 by INT_1:62; :: thesis: verum

end;

then (Py (a,n)) mod (a - 1) = (Fy . 1) mod (a - 1) by Th1, A2;
then ((Py (a,n)) - (Fy . 1)) mod (a - 1) = 0 by INT_4:22;
then a - 1 divides (Py (a,n)) - (Fy . 1) by INT_1:62;
then A8: Py (a,n),Fy . 1 are_congruent_mod a - 1 by INT_1:def 4;
n >= 1 by A5, NAT_1:14;
then ( n + 1 >= 1 + 1 & 1 + 1 = 2 * 1 ) by XREAL_1:7;
then A9: (n + 1) / 2 >= 1 by XREAL_1:77;
1 -' 1 = 1 - 1 by XREAL_1:233;
then A10: ((a ^2) -' 1) |^ (1 -' 1) = 1 by NEWTON:4;
(2 * 1) -' 1 = 2 - 1 by XREAL_1:233;
then A11: n choose ((2 * 1) -' 1) = n by A5, NAT_1:14, NEWTON:23;
A12: Fy . 1 = (n * (a |^ ((n + 1) -' (2 * 1)))) * 1 by A9, A10, A11, A3;
A13: a - 1 >= 2 - 1 by NAT_2:29, XREAL_1:9;

per cases ( a - 1 = 1 or a - 1 > 1 ) by A13, XXREAL_0:1;

suppose a - 1 = 1 ; :: thesis: Py (a,n),n are_congruent_mod a - 1

then (a - 1) * ((Py (a,n)) - n) = (Py (a,n)) - n ;
hence Py (a,n),n are_congruent_mod a - 1 by INT_1:def 5; :: thesis: verum

end;

suppose A14: a - 1 > 1 ; :: thesis: Py (a,n),n are_congruent_mod a - 1

a = ((a - 1) * 1) + 1 ;
then a mod (a - 1) = 1 mod (a - 1) by PEPIN:10
.= 1 by A14, PEPIN:5 ;
then (a |^ ((n + 1) -' (2 * 1))) mod (a - 1) = 1 by A14, PEPIN:35;
then a |^ ((n + 1) -' (2 * 1)),1 are_congruent_mod a - 1 by A14, PEPIN:39;
then Fy . 1,1 * n are_congruent_mod a - 1 by A12, INT_4:11;
hence Py (a,n),n are_congruent_mod a - 1 by A8, INT_1:15; :: thesis: verum

end;

end;

end;

end;