let n, k, q, p, n1, p, a be Element of NAT ; ( 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
; ( 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
; ( 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
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
; ( 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
; 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; verum