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


begin

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 b1 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)) ) & b1 . x = Sum fr )
proof end;
uniqueness
for b1, b2 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)) ) & b1 . 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)) ) & b2 . x = Sum fr ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Poly-INT INT_5:def 1 :
for fp being FinSequence of INT
for b2 being Function of INT,INT holds
( b2 = 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)) ) & b2 . 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 Nat;
pred a is_quadratic_residue_mod m means :Def2: :: INT_5:def 2
ex x being Integer st ((x ^2) - a) mod m = 0 ;
end;

:: deftheorem Def2 defines is_quadratic_residue_mod INT_5:def 2 :
for a being Integer
for m being Nat 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_relative_prime or p divides i )
proof end;

theorem Th12: :: INT_5:12
for i, j being Integer st i divides j holds
i gcd j = abs 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_relative_prime
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;

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;
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 b1 being Integer st a is_quadratic_residue_mod p & a mod p <> 0 & a is_quadratic_residue_mod p & a mod p = 0 holds
( b1 = 1 iff b1 = 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;

begin

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, h, g, 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 n being Nat
for X being finite set
for f being FinSequence of bool X st len f = n & ( 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
;

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;