:: 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
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, INT_1, NAT_1, FINSEQ_1, NEWTON, ARYTM_3,
      ARYTM_1, RELAT_1, CARD_1, FUNCT_1, CARD_3, FUNCOP_1, ORDINAL4, XBOOLE_0,
      TARSKI, XXREAL_0, FINSEQ_5, SQUARE_1, INT_2, COMPLEX1, ABIAN, FINSEQ_2,
      FUNCT_7, PARTFUN1, FINSET_1, RFINSEQ, CALCUL_2, REAL_1, ZFMISC_1, INT_5,
      ORDINAL1;
 notations XREAL_0, GROUP_4, INT_1, RVSUM_1, FINSET_1, ORDINAL1, CARD_1, NAT_D,
      INT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_3, ABIAN, GR_CY_1,
      FINSEQ_5, FINSEQ_2, EULER_2, NEWTON, FINSEQ_7, REAL_1, PEPIN, TARSKI,
      XBOOLE_0, SUBSET_1, XCMPLX_0, NUMBERS, XXREAL_0, NAT_1, DOMAIN_1,
      FINSEQ_1, RFINSEQ, FUNCOP_1, CALCUL_2, ZFMISC_1, CARD_3, WSIERP_1,
      BINOP_1, RECDEF_1;
 constructors ABIAN, WSIERP_1, PEPIN, NAT_3, NAT_D, REALSET1, GR_CY_1,
      FINSEQ_5, EULER_2, RFINSEQ, GROUP_4, FINSEQ_7, REAL_1, WELLORD2,
      CALCUL_2, PROB_3, RECDEF_1, BINOP_1, BINOP_2, CLASSES1, NUMBERS;
 registrations XXREAL_0, MEMBERED, RELAT_1, FINSEQ_1, ORDINAL1, WSIERP_1,
      NUMBERS, XBOOLE_0, XREAL_0, NAT_1, INT_1, FINSET_1, NAT_3, RVSUM_1,
      FUNCT_1, CARD_1, NEWTON, SUBSET_1, VALUED_0, VALUED_1, FINSEQ_2,
      PRE_POLY, RELSET_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve i,i1,i2,i3,i4,i5,j,r,a,b,x,y for Integer,
  d,e,k,n for Nat,
  fp,fk for FinSequence of INT,
  f,f1,f2 for FinSequence of REAL,
  p for Prime;

theorem :: INT_5:1
  i1 divides i2 & i1 divides i3 implies i1 divides i2-i3;

theorem :: INT_5:2
  i divides a & i divides (a-b) implies i divides b;

definition
  let fp;
  func Poly-INT fp -> Function of INT,INT means
:: INT_5:def 1

  for x being Element of
  INT holds ex fr being FinSequence of INT st len fr = len fp & (for d st d in
  dom fr holds fr.d = (fp.d) * x|^(d-'1)) & it.x = Sum fr;
end;

theorem :: INT_5:3
  len fp = 1 implies (Poly-INT fp) = INT --> fp.1;

theorem :: INT_5:4
  len fp = 1 implies for x being Element of INT holds (Poly-INT fp).x = fp.1;

reserve fr for FinSequence of REAL;

theorem :: INT_5:5
  for f,f1,f2 st len f = n+1 & len f1 = len f & len f2 = len f & (
for d st d in dom f holds f.d = f1.d - f2.d) holds ex fr st len fr = len f - 1
& (for d st d in dom fr holds fr.d = f1.d - f2.(d + 1)) & Sum f = Sum fr + f1.(
  n+1) - f2.1;

theorem :: INT_5:6
  len fp = n+2 implies for a being Integer holds ex fr being
  FinSequence of INT, 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);

theorem :: INT_5:7
  p divides i*j implies p divides i or p divides j;

reserve fr,f for FinSequence of INT;

theorem :: INT_5:8
  for fp st len fp = n+1 & p>2 & not p divides fp.(n+1) holds for
fr st (for d st d in dom fr holds (Poly-INT fp).(fr.d) mod p=0) & (for d,e 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;

definition
  let a be Integer, 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;

reserve b,m for Nat;

theorem :: INT_5:9
  a^2 is_quadratic_residue_mod m;

theorem :: INT_5:10
  1 is_quadratic_residue_mod 2;

theorem :: INT_5:11
  i is_quadratic_residue_mod m & i,j are_congruent_mod m implies
  j is_quadratic_residue_mod m;

theorem :: INT_5:12
  i divides j implies i gcd j = |.i.|;

theorem :: INT_5:13
  for i,j,m being Integer st i mod m = j mod m holds i|^n mod m = j|^n mod m;

theorem :: INT_5:14
  a gcd p = 1 & (x^2 - a) mod p = 0 implies x,p are_coprime;

theorem :: INT_5:15
  p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies 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;

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

::Euler Criterion

theorem :: INT_5:17
  p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies
  a|^((p-'1) div 2) mod p = 1;

theorem :: INT_5:18
  p>2 & b gcd p = 1 & not b is_quadratic_residue_mod p implies
  b|^((p-'1) div 2) mod p = p - 1;

theorem :: INT_5:19
  p>2 & a gcd p = 1 & not a is_quadratic_residue_mod p implies
  a|^((p-'1) div 2) mod p = p - 1;

theorem :: INT_5:20
  p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies (a|^(
  (p-'1) div 2) - 1) mod p = 0;

theorem :: INT_5:21
  p > 2 & a gcd p = 1 & not a is_quadratic_residue_mod p implies
  (a|^((p-'1) div 2) + 1) mod p = 0;

reserve b for Integer;

theorem :: INT_5:22
  a is_quadratic_residue_mod p & b is_quadratic_residue_mod p implies
  a*b is_quadratic_residue_mod p;

theorem :: INT_5:23
  p>2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b
  is_quadratic_residue_mod p implies not a*b is_quadratic_residue_mod p;

theorem :: INT_5:24
  p>2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p &
  not b is_quadratic_residue_mod p implies a*b is_quadratic_residue_mod p;

definition
::$N Legendre symbol
  let a be Integer, p be Prime;
  func Lege (a,p) -> Integer equals
:: 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;
end;

theorem :: INT_5:25
  Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = -1;

theorem :: INT_5:26
  a mod p <> 0 implies Lege (a^2,p) = 1;

theorem :: INT_5:27
  Lege (1,p) = 1;

theorem :: INT_5:28
  p>2 & a gcd p = 1 implies Lege (a,p),a|^((p-'1) div 2) are_congruent_mod p;

theorem :: INT_5:29
  p>2 & a gcd p =1 & a,b are_congruent_mod p implies Lege (a,p) = Lege (b,p);

theorem :: INT_5:30
  p>2 & a gcd p=1 & b gcd p=1 implies Lege(a*b,p)=Lege(a,p)*Lege(b,p);

theorem :: INT_5:31
  (for d st d in dom fr holds fr.d = 1 or fr.d = 0 or fr.d = -1) implies
  Product fr = 1 or Product fr = 0 or Product fr = -1;

reserve m for Integer;

theorem :: INT_5:32
  for f,fr st len f = len fr & (for d st d in dom f holds f.d,fr.d
  are_congruent_mod m) holds Product f,Product fr are_congruent_mod m;

theorem :: INT_5:33
  for f,fr st len f = len fr & (for d 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;

reserve fp for FinSequence of NAT;

theorem :: INT_5:34
  p>2 & (for d st d in dom fp holds fp.d gcd p = 1) implies ex fr
being FinSequence of INT st len fr = len fp & (for d st d in dom fr holds fr.d
  = Lege (fp.d,p)) & Lege (Product fp,p) = Product fr;

theorem :: INT_5:35
  p > 2 & d gcd p = 1 & e gcd p = 1 implies Lege((d^2)*e,p) = Lege(e,p);

theorem :: INT_5:36
  p>2 implies Lege (-1,p) = (-1)|^((p-'1) div 2);

theorem :: INT_5:37
  p>2 & p mod 4 = 1 implies (-1) is_quadratic_residue_mod p;

theorem :: INT_5:38
  p>2 & p mod 4 = 3 implies not (-1) is_quadratic_residue_mod p;

begin :: Gauss Lemma and Law of Quadratic Reciprocity

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

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

reserve a,m for Nat;

theorem :: INT_5:41
  for f be 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;

theorem :: INT_5:42
  p>2 implies Lege(2,p) = (-1)|^((p^2 -'1) div 8);

theorem :: INT_5:43
  p>2 & (p mod 8 = 1 or p mod 8 = 7) implies 2 is_quadratic_residue_mod p;

theorem :: INT_5:44
  p>2 & (p mod 8 = 3 or p mod 8 = 5) implies not 2 is_quadratic_residue_mod p;

theorem :: INT_5:45
  for a,b be Nat st a mod 2 = b mod 2 holds (-1)|^a = (-1)|^b;

reserve f,g,h,k for FinSequence of REAL;

theorem :: INT_5:46
  len f = len h & len g = len k implies f^g-h^k = (f-h)^(g-k);

theorem :: INT_5:47
  for f be FinSequence of REAL,m be Real holds Sum(((len f) |-> m)
  - f) = (len f)*m - Sum f;

reserve X for finite set,
  F for FinSequence of bool X;

definition
  let X, F;
  redefine func Card F -> Cardinal-yielding FinSequence of NAT;
end;

theorem :: INT_5:48
  for f be FinSequence of bool X st (for d,e 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;

reserve q for Prime;

::$N The law of quadratic reciprocity
theorem :: INT_5:49
  p>2 & q>2 & p<>q implies
  Lege(p,q)*Lege(q,p)=(-1)|^(((p-'1) div 2)*((q-'1) div 2));

theorem :: INT_5:50
  p>2 & q>2 & p<>q & p mod 4 = 3 & q mod 4 = 3 implies Lege(p,q) = -Lege (q,p);

theorem :: INT_5:51
  p>2 & q>2 & p<>q & (p mod 4 = 1 or q mod 4 = 1) implies Lege(p,q) = Lege(q,p)
;