:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$ :: 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 proofend; 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)) proofend; 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 proofend; theorem Th3: :: INT_7:3 for X being set for p, q being ManySortedSet of X st p | (support p) = q | (support q) holds p = q proofend; theorem Th4: :: INT_7:4 for X being set for p, q being bag of X st support p = {} & support q = {} holds p = q proofend; 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 ) proofend; 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 ) proofend; definition let p be bag of SetPrimes ; attrp is prime-factorization-like means :Def1: :: INT_7:def 1 for x being Prime st x in support p holds ex n being Nat st ( 0 < n & p . x = x |^ n ); 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 ) ); registration let n be non empty Nat; cluster prime_factorization n -> prime-factorization-like ; coherence ppf n is prime-factorization-like proofend; end; theorem Th5: :: INT_7:5 for p, q being Prime for n, m being Nat st p divides m * (q |^ n) & p <> q holds p divides m proofend; 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 ) proofend; 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)) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: INT_7:8 for p being bag of SetPrimes for x being Prime st p is prime-factorization-like holds ( x divides Product p iff x in support p ) by Lm4, Lm7; 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)) proofend; 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) proofend; 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)) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem Th13: :: INT_7:13 for p being bag of SetPrimes st p is prime-factorization-like holds Product p <> 0 proofend; theorem Th14: :: INT_7:14 for p being bag of SetPrimes st p is prime-factorization-like holds ( Product p = 1 iff support p = {} ) proofend; 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 proofend; :: [WP: ] 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 proofend; 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 proofend; 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 ) proofend; begin definition let n be Nat; assume A1: 1 < n ; func Segm0 n -> non empty finite Subset of NAT equals :Def2: :: INT_7:def 2 (Segm n) \ {0}; correctness coherence (Segm n) \ {0} is non empty finite Subset of NAT; proofend; end; :: deftheorem Def2 defines Segm0 INT_7:def_2_:_ for n being Nat st 1 < n holds Segm0 n = (Segm n) \ {0}; theorem Th18: :: INT_7:18 for n being Nat st 1 < n holds card (Segm0 n) = n - 1 proofend; definition let n be Prime; func multint0 n -> BinOp of (Segm0 n) equals :: INT_7:def 3 (multint n) || (Segm0 n); coherence (multint n) || (Segm0 n) is BinOp of (Segm0 n) proofend; end; :: deftheorem defines multint0 INT_7:def_3_:_ 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 proofend; 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 ) proofend; definition let p be Prime; func Z/Z* p -> commutative Group equals :: INT_7:def 4 multMagma(# (Segm0 p),(multint0 p) #); correctness coherence multMagma(# (Segm0 p),(multint0 p) #) is commutative Group; by Th19; end; :: deftheorem defines Z/Z* INT_7:def_4_:_ for p being Prime holds Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #); theorem :: INT_7:20 for p being Prime for x, y being Element of (Z/Z* p) for x1, y1 being Element of (INT.Ring p) st x = x1 & y = y1 holds x * y = x1 * y1 by Lm12; theorem Th21: :: INT_7:21 for p being Prime holds ( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) ) proofend; 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 " proofend; registration let p be Prime; cluster Z/Z* p -> finite commutative ; coherence Z/Z* p is finite ; end; theorem :: INT_7:23 for p being Prime holds card (Z/Z* p) = p - 1 proofend; 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 ) proofend; 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 proofend; 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 ) proofend; theorem Th26: :: INT_7:26 for L being non empty ZeroStr for p being Polynomial of L st 0 <= deg p holds p is non-zero proofend; 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 ) ) proofend; 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) proofend; 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)) ) ) proofend; 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}) proofend; 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 proofend; theorem :: INT_7:31 for p being Prime holds Z/Z* p is cyclic Group proofend;