assume ex k being Nat st i |^ ((2 * k) + 1) is_quadratic_residue_mod p ; :: thesis: contradiction
then 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; :: thesis: verum