let n, k, q, p, n1, p, a be Element of NAT ; :: thesis: ( n - 1 = k * (q |^ n1) & k > 0 & n1 > 0 & q is prime & (a |^ (n -' 1)) mod n = 1 & p is prime & p divides n & not p divides (a |^ ((n -' 1) div q)) -' 1 implies p mod (q |^ n1) = 1 )
assume that
A1: n - 1 = k * (q |^ n1) and
A2: k > 0 and
A3: n1 > 0 and
A4: q is prime ; :: thesis: ( not (a |^ (n -' 1)) mod n = 1 or not p is prime or not p divides n or p divides (a |^ ((n -' 1) div q)) -' 1 or p mod (q |^ n1) = 1 )
A5: (n - 1) + 1 > 0 + 1 by A1, A2, A4, XREAL_1:6;
assume A6: (a |^ (n -' 1)) mod n = 1 ; :: thesis: ( not p is prime or not p divides n or p divides (a |^ ((n -' 1) div q)) -' 1 or p mod (q |^ n1) = 1 )
a |^ ((n -' 1) div q) >= 1

proof

assume a |^ ((n -' 1) div q) < 1 ; :: thesis: contradiction
then A7: a = 0 by NAT_1:14;
(n -' 1) + 1 > 1 by A5, XREAL_1:233;
then n -' 1 >= 1 by NAT_1:13;
then (a |^ (n -' 1)) mod n = (0 * n) mod n by A7, NEWTON:11
.= 0 by NAT_D:13 ;
hence contradiction by A6; :: thesis: verum

end;

then A8: (a |^ ((n -' 1) div q)) -' 1 = (a |^ ((n -' 1) div q)) - 1 by XREAL_1:233;
n1 + 1 > 0 + 1 by A3, XREAL_1:6;
then n1 >= 1 by NAT_1:13;
then A9: n1 -' 1 = n1 - 1 by XREAL_1:233;
then A10: (n -' 1) div q = ((q |^ ((n1 -' 1) + 1)) * k) div q by A1, A5, XREAL_1:233
.= ((q * (q |^ (n1 -' 1))) * k) div q by NEWTON:6
.= (q * ((q |^ (n1 -' 1)) * k)) div q
.= k * (q |^ (n1 -' 1)) by A4, NAT_D:18 ;
assume that
A11: p is prime and
A12: p divides n ; :: thesis: ( p divides (a |^ ((n -' 1) div q)) -' 1 or p mod (q |^ n1) = 1 )
consider i being Nat such that
A13: n = p * i by A12, NAT_D:def 3;
assume not p divides (a |^ ((n -' 1) div q)) -' 1 ; :: thesis: p mod (q |^ n1) = 1
then A14: not (a |^ ((n -' 1) div q)) mod p = 1 by A11, A8, PEPIN:8;
set nn = n -' 1;
n1 + 1 > 0 + 1 by A3, XREAL_1:6;
then n1 >= 1 by NAT_1:13;
then A15: n1 -' 1 = n1 - 1 by XREAL_1:233;
A16: p > 1 by A11, INT_2:def 4;
then p -' 1 = p - 1 by XREAL_1:233;
then A17: (p -' 1) + 1 = p ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i * p <> 0 by A1, A13;
then A18: (a |^ (n -' 1)) mod p = 1 by A6, A16, A13, PEPIN:9;
0 + 1 < (n -' 1) + 1 by A5, XREAL_1:233;
then A19: 1 <= n -' 1 by NAT_1:13;
then A20: a,p are_coprime by A11, A18, Th15;
A21: order (a,p) divides p -' 1 by A11, A18, A19, Th15, PEPIN:49;
n -' 1 = n - 1 by A5, XREAL_1:233;
then order (a,p) divides k * (q |^ ((n1 -' 1) + 1)) by A1, A16, A15, A18, A20, PEPIN:47;
then q |^ n1 divides order (a,p) by A4, A16, A20, A14, A9, A10, Th17, PEPIN:48;
then q |^ n1 divides p -' 1 by A21, NAT_D:4;
then A22: (p -' 1) mod (q |^ n1) = 0 by A4, PEPIN:6;
q > 1 by A4, INT_2:def 4;
hence p mod (q |^ n1) = 1 by A3, A17, A22, NAT_D:16, PEPIN:25; :: thesis: verum