:: by Hiroyuki Okazaki and Yasunari Shidama

::

:: Received January 31, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

Lm1: for x, X, y, z being set st z <> x holds

((X --> 0) +* (x,y)) . z = 0

proof end;

theorem Th1: :: INT_7:1

for X, x being set

for p being ManySortedSet of X st support p = {x} holds

p = (X --> 0) +* (x,(p . x))

for p being ManySortedSet of X st support p = {x} holds

p = (X --> 0) +* (x,(p . x))

proof end;

theorem Th2: :: INT_7:2

for X being set

for p, q, r being real-valued ManySortedSet of X st (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) holds

p + q = r

for p, q, r being real-valued ManySortedSet of X st (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) holds

p + q = r

proof end;

Lm2: for p, q being bag of SetPrimes st support p c= support q & p | (support p) = q | (support p) holds

ex r being bag of SetPrimes st

( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )

proof end;

Lm3: for p being bag of SetPrimes

for X being set st X c= support p holds

ex q, r being bag of SetPrimes st

( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )

proof end;

:: deftheorem Def1 defines prime-factorization-like INT_7:def 1 :

for p being bag of SetPrimes holds

( p is prime-factorization-like iff for x being Prime st x in support p holds

ex n being Nat st

( 0 < n & p . x = x |^ n ) );

for p being bag of SetPrimes holds

( p is prime-factorization-like iff for x being Prime st x in support p holds

ex n being Nat st

( 0 < n & p . x = x |^ n ) );

Lm4: for a being Prime

for b being bag of SetPrimes st b is prime-factorization-like & a in support b holds

( a divides Product b & ex n being Nat st a |^ n divides Product b )

proof end;

Lm5: for p being FinSequence of NAT

for x being Element of NAT

for b being bag of SetPrimes st b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) holds

ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st

( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )

proof end;

Lm6: for i being Element of NAT

for f being FinSequence of NAT

for b being bag of SetPrimes

for a being Prime st len f = i & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds

a in support b

proof end;

theorem Th6: :: INT_7:6

for f being FinSequence of NAT

for b being bag of SetPrimes

for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds

a in support b

for b being bag of SetPrimes

for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds

a in support b

proof end;

Lm7: for a being Prime

for b being bag of SetPrimes st b is prime-factorization-like & a divides Product b holds

a in support b

proof end;

theorem Th7: :: INT_7:7

for p, q being bag of SetPrimes st support p c= support q & p | (support p) = q | (support p) holds

Product p divides Product q

Product p divides Product q

proof end;

theorem :: INT_7:8

theorem Th9: :: INT_7:9

for n, m, k being non empty Nat st k = n lcm m holds

support (ppf k) = (support (ppf n)) \/ (support (ppf m))

support (ppf k) = (support (ppf n)) \/ (support (ppf m))

proof end;

theorem Th10: :: INT_7:10

for X being set

for b1, b2 being bag of X holds support (min (b1,b2)) = (support b1) /\ (support b2)

for b1, b2 being bag of X holds support (min (b1,b2)) = (support b1) /\ (support b2)

proof end;

theorem :: INT_7:11

for n, m, k being non empty Nat st k = n gcd m holds

support (ppf k) = (support (ppf n)) /\ (support (ppf m))

support (ppf k) = (support (ppf n)) /\ (support (ppf m))

proof end;

theorem Th12: :: INT_7:12

for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & support p misses support q holds

Product p, Product q are_relative_prime

Product p, Product q are_relative_prime

proof end;

Lm8: for q being Prime

for g being Element of NAT st g <> 0 holds

ex p1 being bag of SetPrimes st

( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )

proof end;

Lm9: for p being bag of SetPrimes

for x being Prime st p is prime-factorization-like & x in support p & p . x = x holds

ex p1, r1 being bag of SetPrimes st

( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x )

proof end;

Lm10: for p being bag of SetPrimes

for x being Prime st p is prime-factorization-like & x in support p & p . x <> x holds

ex p1, r1 being bag of SetPrimes st

( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )

proof end;

theorem Th14: :: INT_7:14

for p being bag of SetPrimes st p is prime-factorization-like holds

( Product p = 1 iff support p = {} )

( Product p = 1 iff support p = {} )

proof end;

Lm11: for n being Element of NAT

for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds

p = q

proof end;

:: Fundamental Theorem of Arithmetic (uniqueness)

theorem Th15: :: INT_7:15

for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p = Product q holds

p = q

p = q

proof end;

theorem :: INT_7:16

for p being bag of SetPrimes

for n being non empty Nat st p is prime-factorization-like & n = Product p holds

ppf n = p

for n being non empty Nat st p is prime-factorization-like & n = Product p holds

ppf n = p

proof end;

theorem Th17: :: INT_7:17

for n, m being Element of NAT st 1 <= n & 1 <= m holds

ex m0, n0 being Element of NAT st

( n lcm m = n0 * m0 & n0 gcd m0 = 1 & n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0 )

ex m0, n0 being Element of NAT st

( n lcm m = n0 * m0 & n0 gcd m0 = 1 & n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0 )

proof end;

begin

definition

let n be Nat;

assume A1: 1 < n ;

correctness

coherence

(Segm n) \ {0} is non empty finite Subset of NAT;

end;
assume A1: 1 < n ;

correctness

coherence

(Segm n) \ {0} is non empty finite Subset of NAT;

proof end;

:: deftheorem Def2 defines Segm0 INT_7:def 2 :

for n being Nat st 1 < n holds

Segm0 n = (Segm n) \ {0};

for n being Nat st 1 < n holds

Segm0 n = (Segm n) \ {0};

:: deftheorem defines multint0 INT_7:def 3 :

for n being Prime holds multint0 n = (multint n) || (Segm0 n);

for n being Prime holds multint0 n = (multint n) || (Segm0 n);

Lm12: for p being Prime

for a, b being Element of multMagma(# (Segm0 p),(multint0 p) #)

for x, y being Element of (INT.Ring p) st a = x & y = b holds

x * y = a * b

proof end;

theorem Th19: :: INT_7:19

for p being Prime holds

( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )

( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )

proof end;

definition

let p be Prime;

correctness

coherence

multMagma(# (Segm0 p),(multint0 p) #) is commutative Group;

by Th19;

end;
correctness

coherence

multMagma(# (Segm0 p),(multint0 p) #) is commutative Group;

by Th19;

:: deftheorem defines Z/Z* INT_7:def 4 :

for p being Prime holds Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #);

for p being Prime holds Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #);

theorem :: INT_7:20

theorem :: INT_7:22

for p being Prime

for x being Element of (Z/Z* p)

for x1 being Element of (INT.Ring p) st x = x1 holds

x " = x1 "

for x being Element of (Z/Z* p)

for x1 being Element of (INT.Ring p) st x = x1 holds

x " = x1 "

proof end;

registration
end;

theorem :: INT_7:24

for G being Group

for a being Element of G

for i being Integer st not a is being_of_order_0 holds

ex n, k being Element of NAT st

( a |^ i = a |^ n & n = (k * (ord a)) + i )

for a being Element of G

for i being Integer st not a is being_of_order_0 holds

ex n, k being Element of NAT st

( a |^ i = a |^ n & n = (k * (ord a)) + i )

proof end;

theorem Th25: :: INT_7:25

for G being commutative Group

for a, b being Element of G

for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds

ord (a * b) = n * m

for a, b being Element of G

for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds

ord (a * b) = n * m

proof end;

Lm13: for L being Field

for n being Element of NAT

for f being non-zero Polynomial of L st deg f = n holds

ex m being Element of NAT st

( m = card (Roots f) & m <= n )

proof end;

theorem Th27: :: INT_7:27

for L being Field

for f being Polynomial of L st 0 <= deg f holds

( Roots f is finite set & ex m, n being Element of NAT st

( n = deg f & m = card (Roots f) & m <= n ) )

for f being Polynomial of L st 0 <= deg f holds

( Roots f is finite set & ex m, n being Element of NAT st

( n = deg f & m = card (Roots f) & m <= n ) )

proof end;

theorem Th28: :: INT_7:28

for p being Prime

for z being Element of (Z/Z* p)

for y being Element of (INT.Ring p) st z = y holds

for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)

for z being Element of (Z/Z* p)

for y being Element of (INT.Ring p) st z = y holds

for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)

proof end;

Lm14: for p being Prime

for L being Field

for n being Nat st 0 < n & L = INT.Ring p holds

ex f being Polynomial of L st

( deg f = n & ( for x being Element of L

for xz being Element of (Z/Z* p)

for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1_ (INT.Ring p)) ) )

proof end;

theorem Th29: :: INT_7:29

for p being Prime

for a, b being Element of (Z/Z* p)

for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds

b is Element of (gr {a})

for a, b being Element of (Z/Z* p)

for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds

b is Element of (gr {a})

proof end;

theorem Th30: :: INT_7:30

for G being Group

for z being Element of G

for d, l being Element of NAT st G is finite & ord z = d * l holds

ord (z |^ d) = l

for z being Element of G

for d, l being Element of NAT st G is finite & ord z = d * l holds

ord (z |^ d) = l

proof end;