let i be Nat; for p being Prime st p > 2 & i,p are_coprime & i is_primitive_root_of p holds
for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p
let p be Prime; ( p > 2 & i,p are_coprime & i is_primitive_root_of p implies for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p )
assume A1:
( p > 2 & i,p are_coprime & i is_primitive_root_of p )
; for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p
A2: order (i,p) =
Euler p
by A1
.=
p - 1
by EULER_1:20
;
A3:
p > 1
by INT_2:def 4;
then A4: (p -' 1) + 1 =
(p + 1) -' 1
by NAT_D:38
.=
(p + 1) - 1
by NAT_D:37
.=
(p - 1) + 1
;
now for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod passume
ex
k being
Nat st
i |^ ((2 * k) + 1) is_quadratic_residue_mod p
;
contradictionthen consider k being
Nat such that A5:
i |^ ((2 * k) + 1) is_quadratic_residue_mod p
;
set L =
(2 * k) + 1;
set Q =
p -' 1;
i |^ ((2 * k) + 1),
p are_coprime
by A1, WSIERP_1:10;
then
(i |^ ((2 * k) + 1)) gcd p = 1
by INT_2:def 3;
then 1 =
((i |^ ((2 * k) + 1)) |^ ((p -' 1) div 2)) mod p
by A1, A5, INT_5:17
.=
(i |^ (((2 * k) + 1) * ((p -' 1) div 2))) mod p
by NEWTON:9
.=
(i |^ (((2 * k) * ((p -' 1) div 2)) + (1 * ((p -' 1) div 2)))) mod p
.=
((i |^ ((2 * k) * ((p -' 1) div 2))) * (i |^ ((p -' 1) div 2))) mod p
by NEWTON:8
;
then A6:
(i |^ ((2 * k) * ((p -' 1) div 2))) * (i |^ ((p -' 1) div 2)),1
are_congruent_mod p
by A3, PEPIN:39;
p is
odd
by A1, PEPIN:17;
then
2
divides p -' 1
by PEPIN:22, A4;
then A7:
p -' 1
= 2
* ((p -' 1) div 2)
by NAT_D:3;
(i |^ (p -' 1)) mod p = 1
by A1, PEPIN:37;
then
((i |^ (p -' 1)) |^ k) mod p = 1
by A3, PEPIN:35;
then
(i |^ (p -' 1)) |^ k,1
are_congruent_mod p
by A3, PEPIN:39;
then
i |^ (k * (p -' 1)),1
are_congruent_mod p
by NEWTON:9;
then
(i |^ (k * (p -' 1))) * (i |^ ((p -' 1) div 2)),1
* (i |^ ((p -' 1) div 2)) are_congruent_mod p
by INT_4:11;
then
i |^ ((p -' 1) div 2),1
are_congruent_mod p
by A6, A7, PEPIN:40;
then A8:
(i |^ ((p -' 1) div 2)) mod p = 1
by A3, PEPIN:39;
p - 1
>= 2
by A1, INT_1:52;
then A9:
(p -' 1) div 2
>= 2
div 2
by A4, NAT_2:24;
A10:
p -' 1
divides (p -' 1) div 2
by A8, A3, A1, A2, A4, PEPIN:47;
(p -' 1) div 2
divides p -' 1
by A7, NAT_D:def 3;
then
2
* ((p -' 1) div 2) = 1
* ((p -' 1) div 2)
by A7, A10, NAT_D:5;
hence
contradiction
by A9, PEPIN:44;
verum end;
hence
for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p
; verum