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 A1: ( n - 1 = k * (q |^ n1) & k > 0 & n1 > 0 & 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 )
assume A2: (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 )
assume A3: ( p is prime & p divides n ) ; :: thesis: ( p divides (a |^ ((n -' 1) div q)) -' 1 or p mod (q |^ n1) = 1 )
assume A4: not p divides (a |^ ((n -' 1) div q)) -' 1 ; :: thesis: p mod (q |^ n1) = 1
A5: ( p > 1 & q > 1 ) by A1, A3, INT_2:def 5;
A8: (n - 1) + 1 > 0 + 1 by A1, XREAL_1:8;
then A9: n -' 1 = n - 1 by XREAL_1:235;
n1 + 1 > 0 + 1 by A1, XREAL_1:8;
then n1 >= 1 by NAT_1:13;
then A10: n1 -' 1 = n1 - 1 by XREAL_1:235;
consider i being Nat such that
A11: n = p * i by A3, NAT_D:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
i * p <> 0 by A1, A11;
then A12: (a |^ (n -' 1)) mod p = 1 by A2, A3, A5, A11, PEPIN:9;
set nn = n -' 1;
0 + 1 < (n -' 1) + 1 by A8, XREAL_1:235;
then A13: 1 <= n -' 1 by NAT_1:13;
then A14: a,p are_relative_prime by A3, A12, Th15;
then A15: order a,p divides k * (q |^ ((n1 -' 1) + 1)) by A1, A5, A9, A10, A12, PEPIN:52;
a |^ ((n -' 1) div q) >= 1

proof

assume a |^ ((n -' 1) div q) < 1 ; :: thesis: contradiction
then A16: a = 0 by NAT_1:14;
(n -' 1) + 1 > 1 by A8, XREAL_1:235;
then n -' 1 >= 1 by NAT_1:13;
then (a |^ (n -' 1)) mod n = (0 * n) mod n by A16, NEWTON:16
.= 0 by NAT_D:13 ;
hence contradiction by A2; :: thesis: verum

end;

then (a |^ ((n -' 1) div q)) -' 1 = (a |^ ((n -' 1) div q)) - 1 by XREAL_1:235;
then A17: not (a |^ ((n -' 1) div q)) mod p = 1 by A4, A3, PEPIN:8;
n1 + 1 > 0 + 1 by A1, XREAL_1:8;
then n1 >= 1 by NAT_1:13;
then A18: n1 -' 1 = n1 - 1 by XREAL_1:235;
then (n -' 1) div q = ((q |^ ((n1 -' 1) + 1)) * k) div q by A1, A8, XREAL_1:235
.= ((q * (q |^ (n1 -' 1))) * k) div q by NEWTON:11
.= (q * ((q |^ (n1 -' 1)) * k)) div q
.= k * (q |^ (n1 -' 1)) by A1, NAT_D:18 ;
then A19: q |^ n1 divides order a,p by A1, A5, A14, A15, A17, A18, Th17, PEPIN:53;
p -' 1 = p - 1 by A5, XREAL_1:235;
then A20: (p -' 1) + 1 = p ;
order a,p divides p -' 1 by A3, A12, A13, Th15, PEPIN:54;
then q |^ n1 divides p -' 1 by A19, NAT_D:4;
then (p -' 1) mod (q |^ n1) = 0 by A1, PEPIN:6;
hence p mod (q |^ n1) = 1 by A20, A1, A5, PEPIN:26, NAT_D:16; :: thesis: verum