let i, k be Nat; for p being Prime st p > 2 & k >= 2 & i,p are_coprime & i is_primitive_root_of p & (i |^ (p -' 1)) mod (p ^2) <> 1 holds
(i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1
let p be Prime; ( p > 2 & k >= 2 & i,p are_coprime & i is_primitive_root_of p & (i |^ (p -' 1)) mod (p ^2) <> 1 implies (i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1 )
assume A1:
( p > 2 & k >= 2 & i,p are_coprime & i is_primitive_root_of p & (i |^ (p -' 1)) mod (p ^2) <> 1 )
; (i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1
A2:
p > 1
by INT_2:def 4;
defpred S1[ Nat] means (i |^ (Euler (p |^ ($1 -' 1)))) mod (p |^ $1) <> 1;
A3:
S1[2]
A5:
for k being Nat st k >= 2 & S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( k >= 2 & S1[k] implies S1[k + 1] )
assume A6:
(
k >= 2 &
S1[
k] )
;
S1[k + 1]
A7:
i <> 0
by A1, A2, Th5;
A8:
i,
p |^ (k -' 1) are_coprime
by A1, WSIERP_1:10;
A9:
(
k > 1 &
k > 0 )
by A6, XXREAL_0:2;
then
k - 1
> 0
by XREAL_1:50;
then A10:
k -' 1
> 0
by A6, XXREAL_0:2, XREAL_1:233;
then A11:
p |^ (k -' 1) > 1
by A2, PEPIN:25;
(i |^ (Euler (p |^ (k -' 1)))) mod (p |^ (k -' 1)) = 1
by A7, A8, A10, A2, PEPIN:25, EULER_2:18;
then
i |^ (Euler (p |^ (k -' 1))),1
are_congruent_mod p |^ (k -' 1)
by A11, PEPIN:39;
then
p |^ (k -' 1) divides (i |^ (Euler (p |^ (k -' 1)))) - 1
by INT_2:15;
then consider s being
Integer such that A12:
(i |^ (Euler (p |^ (k -' 1)))) - 1
= (p |^ (k -' 1)) * s
by INT_1:def 3;
A13:
p |^ k > 1
by A2, A6, PEPIN:25;
A14:
(p |^ (k -' 1)) * s >= 0
by A12, XREAL_1:48, NAT_1:14, A7;
s >= 0
by A14;
then reconsider s =
s as
Element of
NAT by INT_1:3;
reconsider M =
s ^3 as
Element of
NAT by ORDINAL1:def 12;
A18:
k -' 1
>= 1
by A10, NAT_1:14;
A19:
Euler (p |^ k) =
(p |^ k) - (p |^ (k -' 1))
by A6, XXREAL_0:2, Th8
.=
(p |^ ((k + 1) -' 1)) - (p |^ (k -' 1))
by NAT_D:34
.=
(p |^ ((k -' 1) + 1)) - (p |^ (k -' 1))
by A6, XXREAL_0:2, NAT_D:38
.=
((p |^ (k -' 1)) * p) - (p |^ (k -' 1))
by NEWTON:6
.=
((p |^ (k -' 1)) * p) - (p |^ (((k -' 1) + 1) -' 1))
by NAT_D:34
.=
((p |^ (k -' 1)) * p) - (p |^ (((k -' 1) -' 1) + 1))
by NAT_D:38, A10, NAT_1:14
.=
((p |^ (k -' 1)) * p) - ((p |^ ((k -' 1) -' 1)) * p)
by NEWTON:6
.=
((p |^ (k -' 1)) - (p |^ ((k -' 1) -' 1))) * p
.=
(Euler (p |^ (k -' 1))) * p
by A10, NAT_1:14, Th8
;
consider t being
Nat such that A20:
(1 + ((p |^ (k -' 1)) * s)) |^ p = ((1 + (p * ((p |^ (k -' 1)) * s))) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by Th4;
A21:
p is
odd
by A1, PEPIN:17;
A22:
p -' 1
= p - 1
by A2, XREAL_1:233;
then
2
divides p -' 1
by A21, PEPIN:22;
then
(p -' 1) mod 2
= 0
by PEPIN:6;
then A23:
(p -' 1) div 2
= (p - 1) / 2
by A22, PEPIN:63;
A24:
(1 + ((p |^ (k -' 1)) * s)) |^ p =
((1 + ((p * (p |^ (k -' 1))) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by A20
.=
((1 + ((p |^ ((k -' 1) + 1)) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NEWTON:6
.=
((1 + ((p |^ ((k + 1) -' 1)) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by A9, NAT_D:38
.=
((1 + ((p |^ k) * s)) + ((p choose 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NAT_D:34
.=
((1 + ((p |^ k) * s)) + (((p * (p - 1)) / 2) * (((p |^ (k -' 1)) * s) ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by STIRL2_1:51
.=
((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * ((p |^ (k -' 1)) * p)) * (p |^ (k -' 1))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by A23
.=
((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ ((k -' 1) + 1))) * (p |^ (k -' 1))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NEWTON:6
.=
((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ ((k + 1) -' 1))) * (p |^ (k -' 1))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NAT_D:38, A9
.=
((1 + ((p |^ k) * s)) + (((((p -' 1) div 2) * (p |^ k)) * (p |^ (k -' 1))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NAT_D:34
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * ((p |^ (k -' 1)) * (p |^ k))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((k -' 1) + k))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by NEWTON:8
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((k + k) -' 1))) * (s ^2))) + (t * (((p |^ (k -' 1)) * s) ^3))
by A9, NAT_D:38
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2))) + (((t * ((p |^ (k -' 1)) * (p |^ (k -' 1)))) * (p |^ (k -' 1))) * (s ^3))
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2))) + (((t * (p |^ ((k -' 1) + (k -' 1)))) * (p |^ (k -' 1))) * M)
by NEWTON:8
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2))) + ((t * ((p |^ ((k -' 1) + (k -' 1))) * (p |^ (k -' 1)))) * M)
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2))) + ((t * (p |^ (((k -' 1) + (k -' 1)) + (k -' 1)))) * M)
by NEWTON:8
.=
((1 + ((p |^ k) * s)) + ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2))) + ((t * M) * (p |^ (3 * (k -' 1))))
;
(k -' 1) + k >= 1
+ k
by A18, XREAL_1:6;
then A25:
(k + k) -' 1
>= k + 1
by A6, XXREAL_0:2, NAT_D:38;
then A26:
p |^ (k + 1) divides (((p -' 1) div 2) * (s ^2)) * (p |^ ((2 * k) -' 1))
by Lm2, NAT_D:9;
k + (2 * k) >= 2
+ (2 * k)
by A6, XREAL_1:6;
then A27:
(3 * k) - 3
>= ((2 * k) + 2) - 3
by XREAL_1:9;
2
* k > 2
* 1
by A9, XREAL_1:68;
then
(2 * k) -' 1
= (2 * k) - 1
by XXREAL_0:2, XREAL_1:233;
then
3
* (k - 1) >= k + 1
by A25, A27, XXREAL_0:2;
then
3
* (k -' 1) >= k + 1
by A6, XXREAL_0:2, XREAL_1:233;
then
p |^ (k + 1) divides (t * M) * (p |^ (3 * (k -' 1)))
by Lm2, NAT_D:9;
then A28:
p |^ (k + 1) divides ((((p -' 1) div 2) * (p |^ ((2 * k) -' 1))) * (s ^2)) + ((t * M) * (p |^ (3 * (k -' 1))))
by A26, NAT_D:8;
i |^ (Euler (p |^ k)) = (1 + ((p |^ (k -' 1)) * s)) |^ p
by A12, A19, NEWTON:9;
then A29:
p |^ (k + 1) divides ((i |^ (Euler (p |^ k))) - 1) - ((p |^ k) * s)
by A24, A28;
hence
S1[
k + 1]
;
verum
end;
for k being Nat st k >= 2 holds
S1[k]
from NAT_1:sch 8(A3, A5);
hence
(i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1
by A1; verum