:: Gauss Lemma and Law of Quadratic Reciprocity
:: by Li Yan , Xiquan Liang and Junjie Zhao
::
:: Received October 9, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: INT_5:1

for i1, i2, i3 being Integer st i1 divides i2 & i1 divides i3 holds
i1 divides i2 - i3

proof end;

theorem Th2: :: INT_5:2

for i, a, b being Integer st i divides a & i divides a - b holds
i divides b

proof end;

Lm1: for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )

proof end;

definition

let fp be FinSequence of INT ;

func Poly-INT fp -> Function of INT,INT means :Def1: :: INT_5:def 1
for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & it . x = Sum fr );

existence
ex b₁ being Function of INT,INT st
for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & b₁ . x = Sum fr )

proof end;

uniqueness
for b₁, b₂ being Function of INT,INT st ( for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & b₁ . x = Sum fr ) ) & ( for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & b₂ . x = Sum fr ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Poly-INT INT_5:def 1 :
for fp being FinSequence of INT
for b₂ being Function of INT,INT holds
( b₂ = Poly-INT fp iff for x being Element of INT ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = (fp . d) * (x |^ (d -' 1)) ) & b₂ . x = Sum fr ) );

theorem Th3: :: INT_5:3

for fp being FinSequence of INT st len fp = 1 holds
Poly-INT fp = INT --> (fp . 1)

proof end;

theorem :: INT_5:4

for fp being FinSequence of INT st len fp = 1 holds
for x being Element of INT holds (Poly-INT fp) . x = fp . 1

proof end;

theorem Th5: :: INT_5:5

for n being Nat
for f, f1, f2 being FinSequence of REAL st len f = n + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds
f . d = (f1 . d) - (f2 . d) ) holds
ex fr being FinSequence of REAL st
( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds
fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) )

proof end;

theorem Th6: :: INT_5:6

for n being Nat
for fp being FinSequence of INT st len fp = n + 2 holds
for a being Integer ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )

proof end;

theorem Th7: :: INT_5:7

for i, j being Integer
for p being Prime holds
( not p divides i * j or p divides i or p divides j )

proof end;

theorem Th8: :: INT_5:8

for n being Nat
for p being Prime
for fp being FinSequence of INT st len fp = n + 1 & p > 2 & not p divides fp . (n + 1) holds
for fr being FinSequence of INT st ( for d being Nat st d in dom fr holds
((Poly-INT fp) . (fr . d)) mod p = 0 ) & ( for d, e being Nat st d in dom fr & e in dom fr & d <> e holds
not fr . d,fr . e are_congruent_mod p ) holds
len fr <= n

proof end;

definition

let a be Integer;
let m be natural Number ;

pred a is_quadratic_residue_mod m means :: INT_5:def 2
ex x being Integer st ((x ^2) - a) mod m = 0 ;

end;

:: deftheorem defines is_quadratic_residue_mod INT_5:def 2 :
for a being Integer
for m being natural Number holds
( a is_quadratic_residue_mod m iff ex x being Integer st ((x ^2) - a) mod m = 0 );

theorem Th9: :: INT_5:9

for a being Integer
for m being Nat holds a ^2 is_quadratic_residue_mod m

proof end;

theorem :: INT_5:10

1 is_quadratic_residue_mod 2

proof end;

theorem Th11: :: INT_5:11

for i, j being Integer
for m being Nat st i is_quadratic_residue_mod m & i,j are_congruent_mod m holds
j is_quadratic_residue_mod m

proof end;

Lm2: for i being Integer
for p being Prime holds
( i,p are_coprime or p divides i )

proof end;

theorem Th12: :: INT_5:12

for i, j being Integer st i divides j holds
i gcd j = |.i.|

proof end;

theorem Th13: :: INT_5:13

for n being Nat
for i, j, m being Integer st i mod m = j mod m holds
(i |^ n) mod m = (j |^ n) mod m

proof end;

theorem Th14: :: INT_5:14

for a, x being Integer
for p being Prime st a gcd p = 1 & ((x ^2) - a) mod p = 0 holds
x,p are_coprime

proof end;

theorem :: INT_5:15

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
ex x, y being Integer st
( ((x ^2) - a) mod p = 0 & ((y ^2) - a) mod p = 0 & not x,y are_congruent_mod p )

proof end;

theorem Th16: :: INT_5:16

for p being Prime st p > 2 holds
ex fp being FinSequence of NAT st
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) )

proof end;

::Euler Criterion

theorem Th17: :: INT_5:17

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
(a |^ ((p -' 1) div 2)) mod p = 1

proof end;

theorem Th18: :: INT_5:18

for p being Prime
for b being Nat st p > 2 & b gcd p = 1 & not b is_quadratic_residue_mod p holds
(b |^ ((p -' 1) div 2)) mod p = p - 1

proof end;

theorem Th19: :: INT_5:19

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p holds
(a |^ ((p -' 1) div 2)) mod p = p - 1

proof end;

theorem Th20: :: INT_5:20

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
((a |^ ((p -' 1) div 2)) - 1) mod p = 0

proof end;

theorem Th21: :: INT_5:21

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p holds
((a |^ ((p -' 1) div 2)) + 1) mod p = 0

proof end;

theorem :: INT_5:22

for a being Integer
for p being Prime
for b being Integer st a is_quadratic_residue_mod p & b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p

proof end;

theorem :: INT_5:23

for a being Integer
for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
not a * b is_quadratic_residue_mod p

proof end;

theorem :: INT_5:24

for a being Integer
for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p

proof end;

definition

let a be Integer;
let p be Prime;

:: Legendre symbol

func Lege (a,p) -> Integer equals :Def3: :: INT_5:def 3
1 if ( a is_quadratic_residue_mod p & a mod p <> 0 )
0 if ( a is_quadratic_residue_mod p & a mod p = 0 )
otherwise - 1;

coherence
( ( a is_quadratic_residue_mod p & a mod p <> 0 implies 1 is Integer ) & ( a is_quadratic_residue_mod p & a mod p = 0 implies 0 is Integer ) & ( ( not a is_quadratic_residue_mod p or not a mod p <> 0 ) & ( not a is_quadratic_residue_mod p or not a mod p = 0 ) implies - 1 is Integer ) ) ;
consistency
for b₁ being Integer st a is_quadratic_residue_mod p & a mod p <> 0 & a is_quadratic_residue_mod p & a mod p = 0 holds
( b₁ = 1 iff b₁ = 0 ) ;

end;

:: deftheorem Def3 defines Lege INT_5:def 3 :
for a being Integer
for p being Prime holds
( ( a is_quadratic_residue_mod p & a mod p <> 0 implies Lege (a,p) = 1 ) & ( a is_quadratic_residue_mod p & a mod p = 0 implies Lege (a,p) = 0 ) & ( ( not a is_quadratic_residue_mod p or not a mod p <> 0 ) & ( not a is_quadratic_residue_mod p or not a mod p = 0 ) implies Lege (a,p) = - 1 ) );

theorem Th25: :: INT_5:25

for a being Integer
for p being Prime holds
( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 )

proof end;

theorem Th26: :: INT_5:26

for a being Integer
for p being Prime st a mod p <> 0 holds
Lege ((a ^2),p) = 1

proof end;

theorem :: INT_5:27

for p being Prime holds Lege (1,p) = 1

proof end;

Lm3: for a being Integer
for p being Prime st a gcd p = 1 holds
not p divides a

proof end;

theorem Th28: :: INT_5:28

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 holds
Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p

proof end;

theorem :: INT_5:29

for a being Integer
for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & a,b are_congruent_mod p holds
Lege (a,p) = Lege (b,p)

proof end;

theorem :: INT_5:30

for a being Integer
for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 holds
Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))

proof end;

theorem Th31: :: INT_5:31

for fr being FinSequence of INT holds
( ex d being Nat st
( d in dom fr & not fr . d = 1 & not fr . d = 0 & not fr . d = - 1 ) or Product fr = 1 or Product fr = 0 or Product fr = - 1 )

proof end;

theorem Th32: :: INT_5:32

for m being Integer
for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) holds
Product f, Product fr are_congruent_mod m

proof end;

theorem Th33: :: INT_5:33

for m being Integer
for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) holds
Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m

proof end;

theorem Th34: :: INT_5:34

for p being Prime
for fp being FinSequence of NAT st p > 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) holds
ex fr being FinSequence of INT st
( len fr = len fp & ( for d being Nat st d in dom fr holds
fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

proof end;

theorem :: INT_5:35

for d, e being Nat
for p being Prime st p > 2 & d gcd p = 1 & e gcd p = 1 holds
Lege (((d ^2) * e),p) = Lege (e,p)

proof end;

theorem Th36: :: INT_5:36

for p being Prime st p > 2 holds
Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2)

proof end;

theorem :: INT_5:37

for p being Prime st p > 2 & p mod 4 = 1 holds
- 1 is_quadratic_residue_mod p

proof end;

theorem :: INT_5:38

for p being Prime st p > 2 & p mod 4 = 3 holds
not - 1 is_quadratic_residue_mod p

proof end;

theorem Th39: :: INT_5:39

for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( f is one-to-one iff Swap (f,i,j) is one-to-one )

proof end;

theorem Th40: :: INT_5:40

for n being Nat
for f being FinSequence of NAT st len f = n & ( for d being Nat st d in dom f holds
( f . d > 0 & f . d <= n ) ) & f is one-to-one holds
rng f = Seg n

proof end;

theorem Th41: :: INT_5:41

for p being Prime
for a, m being Nat
for f being FinSequence of NAT st p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds
Lege (a,p) = (- 1) |^ m

proof end;

theorem Th42: :: INT_5:42

for p being Prime st p > 2 holds
Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8)

proof end;

theorem :: INT_5:43

for p being Prime st p > 2 & ( p mod 8 = 1 or p mod 8 = 7 ) holds
2 is_quadratic_residue_mod p

proof end;

theorem :: INT_5:44

for p being Prime st p > 2 & ( p mod 8 = 3 or p mod 8 = 5 ) holds
not 2 is_quadratic_residue_mod p

proof end;

theorem Th45: :: INT_5:45

for a, b being Nat st a mod 2 = b mod 2 holds
(- 1) |^ a = (- 1) |^ b

proof end;

theorem Th46: :: INT_5:46

for f, g, h, k being FinSequence of REAL st len f = len h & len g = len k holds
(f ^ g) - (h ^ k) = (f - h) ^ (g - k)

proof end;

theorem Th47: :: INT_5:47

for f being FinSequence of REAL
for m being Real holds Sum (((len f) |-> m) - f) = ((len f) * m) - (Sum f)

proof end;

definition

let X be finite set ;
let F be FinSequence of bool X;
:: original: Card
redefine func Card F -> Cardinal-yielding FinSequence of NAT ;
coherence
Card F is Cardinal-yielding FinSequence of NAT

proof end;

end;

theorem Th48: :: INT_5:48

for X being finite set
for f being FinSequence of bool X st ( for d, e being Nat st d in dom f & e in dom f & d <> e holds
f . d misses f . e ) holds
card (union (rng f)) = Sum (Card f)

proof end;

Lm4: for fp being FinSequence of NAT holds Sum fp is Element of NAT
;

:: The law of quadratic reciprocity

theorem Th49: :: INT_5:49

for p, q being Prime st p > 2 & q > 2 & p <> q holds
(Lege (p,q)) * (Lege (q,p)) = (- 1) |^ (((p -' 1) div 2) * ((q -' 1) div 2))

proof end;

theorem :: INT_5:50

for p, q being Prime st p > 2 & q > 2 & p <> q & p mod 4 = 3 & q mod 4 = 3 holds
Lege (p,q) = - (Lege (q,p))

proof end;

theorem :: INT_5:51

for p, q being Prime st p > 2 & q > 2 & p <> q & ( p mod 4 = 1 or q mod 4 = 1 ) holds
Lege (p,q) = Lege (q,p)

proof end;