:: by Li Yan , Xiquan Liang and Junjie Zhao

::

:: Received October 9, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

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 ;

ex b_{1} 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_{1} . x = Sum fr )

for b_{1}, b_{2} 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_{1} . 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_{2} . x = Sum fr ) ) holds

b_{1} = b_{2}

end;
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 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 );

ex b

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

proof end;

uniqueness for b

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & b

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & b

b

proof end;

:: deftheorem Def1 defines Poly-INT INT_5:def 1 :

for fp being FinSequence of INT

for b_{2} being Function of INT,INT holds

( b_{2} = 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_{2} . x = Sum fr ) );

for fp being FinSequence of INT

for b

( b

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = (fp . d) * (x |^ (d -' 1)) ) & b

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

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) )

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) )

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 )

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

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 ;

end;
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 ;

ex x being Integer st ((x ^2) - a) mod m = 0 ;

:: 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 );

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 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

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 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

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

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 )

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 ) )

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

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

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

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

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

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

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

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

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;

( ( 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_{1} 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} = 1 iff b_{1} = 0 )
;

end;
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 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;

( ( 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

( b

:: 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 ) );

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 )

for p being Prime holds

( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,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

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)

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))

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 )

( 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

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

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 )

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)

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 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 )

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

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

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 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)

(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)

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

end;
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;

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)

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

;

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))

(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))

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)

Lege (p,q) = Lege (q,p)

proof end;