let p be Prime; :: thesis: for a being Element of (GF p) st 2 < p holds
card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)
let a be Element of (GF p); :: thesis: ( 2 < p implies card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) )
assume AS: 2 < p ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

per cases ( a is quadratic_residue or not a is quadratic_residue ) ;

suppose A1: a is quadratic_residue ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

then consider x being Element of (GF p) such that
P1: x |^ 2 = a by QRDef1;
P2: x in { b where b is Element of (GF p) : b |^ 2 = a } by P1;
(- x) |^ 2 = (- x) * (- x) by EXLm4
.= x * x by VECTSP_1:10
.= a by P1, EXLm4 ;
then - x in { b where b is Element of (GF p) : b |^ 2 = a } ;
then P4: {x,(- x)} c= { b where b is Element of (GF p) : b |^ 2 = a } by P2, ZFMISC_1:32;
P5: x <> - x

proof

assume x = - x ; :: thesis: contradiction
then x + x = 0. (GF p) by VECTSP_1:16;
then F2: x = 0. (GF p) by AS, EX8;
x |^ 2 = (0. (GF p)) * (0. (GF p)) by F2, EXLm4
.= 0. (GF p) by VECTSP_1:12
.= 0 by XLm2 ;
hence contradiction by P1, A1, QRDef1; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in { b where b is Element of (GF p) : b |^ 2 = a } implies y in {x,(- x)} )
assume y in { b where b is Element of (GF p) : b |^ 2 = a } ; :: thesis: y in {x,(- x)}
then consider z being Element of (GF p) such that
P52: ( y = z & z |^ 2 = a ) ;
z * z = z |^ 2 by EXLm4
.= x * x by P1, P52, EXLm4 ;
then ( z = x or z = - x ) by EX7;
hence y in {x,(- x)} by P52, TARSKI:def 2; :: thesis: verum

end;

then { b where b is Element of (GF p) : b |^ 2 = a } c= {x,(- x)} by TARSKI:def 3;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = card {x,(- x)} by P4, XBOOLE_0:def 10
.= 1 + 1 by P5, CARD_2:57
.= 1 + (Lege_p a) by A1, QRDef3 ;
:: thesis: verum

end;

suppose A1: not a is quadratic_residue ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

now

per cases ( a = 0 or a <> 0 ) ;

suppose A10: a = 0 ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) :: thesis: verum

proof

now

let x be set ; :: thesis: ( x in { b where b is Element of (GF p) : b |^ 2 = a } implies x in {(0. (GF p))} )
assume x in { b where b is Element of (GF p) : b |^ 2 = a } ; :: thesis: x in {(0. (GF p))}
then consider b being Element of (GF p) such that
A101: ( x = b & b |^ 2 = 0 ) by A10;
b = 0 by EX6, A101
.= 0. (GF p) by XLm2 ;
hence x in {(0. (GF p))} by A101, TARSKI:def 1; :: thesis: verum

end;

then A11: { b where b is Element of (GF p) : b |^ 2 = a } c= {(0. (GF p))} by TARSKI:def 3;
(0. (GF p)) |^ 2 = (0. (GF p)) * (0. (GF p)) by EXLm4
.= 0. (GF p) by VECTSP_1:12
.= 0 by XLm2 ;
then 0. (GF p) in { b where b is Element of (GF p) : b |^ 2 = a } by A10;
then {(0. (GF p))} c= { b where b is Element of (GF p) : b |^ 2 = a } by ZFMISC_1:31;
then { b where b is Element of (GF p) : b |^ 2 = a } = {(0. (GF p))} by A11, XBOOLE_0:def 10;
hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + 0 by CARD_2:42
.= 1 + (Lege_p a) by A10, QRDef3 ;
:: thesis: verum

end;

end;

suppose A11: a <> 0 ; :: thesis: card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a)

A13: { b where b is Element of (GF p) : b |^ 2 = a } = {}

proof

assume { b where b is Element of (GF p) : b |^ 2 = a } <> {} ; :: thesis: contradiction
then consider x being set such that
A131: x in { b where b is Element of (GF p) : b |^ 2 = a } by XBOOLE_0:def 1;
ex b being Element of (GF p) st
( x = b & b |^ 2 = a ) by A131;
hence contradiction by A1, QRDef1, A11; :: thesis: verum

end;

thus card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (- 1) by A13
.= 1 + (Lege_p a) by A1, A11, QRDef3 ; :: thesis: verum

end;

end;

end;

hence card { b where b is Element of (GF p) : b |^ 2 = a } = 1 + (Lege_p a) ; :: thesis: verum

end;

end;