:: Gauss Lemma and Law of Quadratic Reciprocity :: by Li Yan , Xiquan Liang and Junjie Zhao :: :: Received October 9, 2007 :: Copyright (c) 2007-2012 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 proofend; theorem Th2: :: INT_5:2 for i, a, b being Integer st i divides a & i divides a - b holds i divides b proofend; 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 ) ) proofend; 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 ) proofend; 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 proofend; 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) proofend; 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 proofend; 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) ) proofend; 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) ) proofend; 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 ) proofend; 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 proofend; definition let a be Integer; let m be Nat; preda 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 proofend; theorem :: INT_5:10 1 is_quadratic_residue_mod 2 proofend; 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 proofend; Lm2: for i being Integer for p being Prime holds ( i,p are_relative_prime or p divides i ) proofend; theorem Th12: :: INT_5:12 for i, j being Integer st i divides j holds i gcd j = abs i proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) ) proofend; ::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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; theorem Th26: :: INT_5:26 for a being Integer for p being Prime st a mod p <> 0 holds Lege ((a ^2),p) = 1 proofend; theorem :: INT_5:27 for p being Prime holds Lege (1,p) = 1 proofend; Lm3: for a being Integer for p being Prime st a gcd p = 1 holds not p divides a proofend; 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 proofend; 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) proofend; 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)) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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) proofend; theorem Th36: :: INT_5:36 for p being Prime st p > 2 holds Lege ((- 1),p) = (- 1) |^ ((p -' 1) div 2) proofend; theorem :: INT_5:37 for p being Prime st p > 2 & p mod 4 = 1 holds - 1 is_quadratic_residue_mod p proofend; theorem :: INT_5:38 for p being Prime st p > 2 & p mod 4 = 3 holds not - 1 is_quadratic_residue_mod p proofend; 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 ) proofend; 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 proofend; 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 proofend; theorem Th42: :: INT_5:42 for p being Prime st p > 2 holds Lege (2,p) = (- 1) |^ (((p ^2) -' 1) div 8) proofend; 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 proofend; 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 proofend; theorem Th45: :: INT_5:45 for a, b being Nat st a mod 2 = b mod 2 holds (- 1) |^ a = (- 1) |^ b proofend; 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) proofend; 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) proofend; 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 proofend; 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) proofend; Lm4: for fp being FinSequence of NAT holds Sum fp is Element of NAT ; :: [WP: ] 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)) proofend; 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)) proofend; 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) proofend;