let i, k be Nat; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: (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]
proof
2 -' 1 = 2 - 1 by XREAL_1:233
.= 1 ;
then A4: (i |^ (Euler (p |^ (2 -' 1)))) mod (p |^ 2) = (i |^ (Euler p)) mod (p |^ 2) ;
Euler p = p - 1 by EULER_1:20
.= p -' 1 by A2, XREAL_1:233 ;
hence S1[2] by A1, A4, NEWTON:81; :: thesis: verum
end;
A5: for k being Nat st k >= 2 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 2 & S1[k] implies S1[k + 1] )
assume A6: ( k >= 2 & S1[k] ) ; :: thesis: 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;
A15: ( p |^ (k -' 1) is Element of NAT & p is Element of NAT ) by ORDINAL1:def 12;
A16: now :: thesis: not p divides s
assume p divides s ; :: thesis: contradiction
then (p |^ (k -' 1)) * p divides (p |^ (k -' 1)) * s by A15, PYTHTRIP:7;
then A17: p |^ ((k -' 1) + 1) divides (p |^ (k -' 1)) * s by NEWTON:6;
p |^ ((k -' 1) + 1) = p |^ ((k + 1) -' 1) by A9, NAT_D:38
.= p |^ k by NAT_D:34 ;
then i |^ (Euler (p |^ (k -' 1))),1 are_congruent_mod p |^ k by INT_2:15, A17, A12;
hence contradiction by A6, A13, PEPIN:39; :: thesis: verum
end;
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;
now :: thesis: not (i |^ (Euler (p |^ ((k + 1) -' 1)))) mod (p |^ (k + 1)) = 1
assume A30: (i |^ (Euler (p |^ ((k + 1) -' 1)))) mod (p |^ (k + 1)) = 1 ; :: thesis: contradiction
p |^ (k + 1) > 1 by A2, PEPIN:25;
then i |^ (Euler (p |^ ((k + 1) -' 1))),1 are_congruent_mod p |^ (k + 1) by A30, PEPIN:39;
then p |^ (k + 1) divides (i |^ (Euler (p |^ ((k + 1) -' 1)))) - 1 by INT_2:15;
then p |^ (k + 1) divides (i |^ (Euler (p |^ k))) - 1 by NAT_D:34;
then p |^ (k + 1) divides (p |^ k) * s by A29, INT_5:2;
then A31: (p |^ k) * p divides (p |^ k) * s by NEWTON:6;
p |^ k is Element of NAT by ORDINAL1:def 12;
hence contradiction by A16, A15, A31, PYTHTRIP:7; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: 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; :: thesis: verum