:: Fundamental {T}heorem of {A}rithmetic
::  by Artur Korni{\l}owicz and Piotr Rudnicki
::
:: Received February 13, 2004
:: Copyright (c) 2004-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, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
      RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
      TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
      UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
      TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
 constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
      BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
      XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
      XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
      XREAL_0, RVSUM_1;
 requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;


begin :: Preliminaries

reserve a, b, n for Nat,
  r for Real,
  f for FinSequence of REAL;

registration
  cluster natural-valued for FinSequence;
end;

registration
  let a be non zero Nat;
  let b be Nat;
  cluster a |^ b -> non zero;
end;

registration
  cluster -> non zero for Prime;
end;

reserve p for Prime;

theorem :: NAT_3:1
  for a, b, c, d being Nat st a divides c & b divides d holds a*b divides c*d;

theorem :: NAT_3:2
  1 < a implies b < a |^ b;

theorem :: NAT_3:3
  a <> 0 implies n divides n |^ a;

theorem :: NAT_3:4
  for i, j, m, n being Nat st i < j & m |^ j divides n
  holds m |^ (i+1) divides n;

theorem :: NAT_3:5
  p divides a |^ b implies p divides a;

theorem :: NAT_3:6
  for a being Prime st a divides p |^ b holds a = p;

theorem :: NAT_3:7
  for f being FinSequence of NAT st a in rng f holds a divides Product f;

theorem :: NAT_3:8
  for f being FinSequence of SetPrimes st p divides Product f holds p in rng f;

:: Power

definition
  let f be real-valued FinSequence;
  let a be Nat;
  func f |^ a -> FinSequence means
:: NAT_3:def 1

  len it = len f & for i being set st i in dom it holds it.i = f.i |^ a;
end;

registration
  let f be real-valued FinSequence;
  let a be Nat;
  cluster f |^ a -> real-valued;
end;

registration
  let f be natural-valued FinSequence;
  let a be Nat;
  cluster f |^ a -> natural-valued;
end;

definition
  let f be FinSequence of REAL;
  let a be Nat;
  redefine func f |^ a -> FinSequence of REAL;
end;

definition
  let f be FinSequence of NAT;
  let a be Nat;
  redefine func f |^ a -> FinSequence of NAT;
end;

theorem :: NAT_3:9
  f |^ 0 = (len f) |-> 1;

theorem :: NAT_3:10
  f |^ 1 = f;

theorem :: NAT_3:11
  <*>REAL |^ a = <*>REAL;

theorem :: NAT_3:12
  <*r*>|^a = <*r|^a*>;

theorem :: NAT_3:13
  (f^<*r*>) |^ a = (f|^a)^(<*r*>|^a);

theorem :: NAT_3:14
  Product (f|^(b+1)) = Product (f|^b) * Product f;

theorem :: NAT_3:15
  Product (f|^a) = (Product f) |^ a;

begin :: More about bags

registration
  let X be set;
  cluster natural-valued finite-support for ManySortedSet of X;
end;

definition
  let X be set, b be real-valued ManySortedSet of X, a be Nat;
  func a * b -> ManySortedSet of X means
:: NAT_3:def 2

  for i being object holds it.i = a * b.i;
end;

registration
  let X be set, b be real-valued ManySortedSet of X, a be Nat;
  cluster a * b -> real-valued;
end;

registration
  let X be set, b be natural-valued ManySortedSet of X, a be Nat;
  cluster a * b -> natural-valued;
end;

registration
  let X be set, b be real-valued ManySortedSet of X;
  cluster support (0*b) -> empty;
end;

theorem :: NAT_3:16
  for X being set, b being real-valued ManySortedSet of X st a <>
  0 holds support b = support (a*b);

registration
  let X be set, b be real-valued finite-support ManySortedSet of X, a be
  Nat;
  cluster a * b -> finite-support;
end;

definition
  let X be set;
  let b1, b2 be real-valued ManySortedSet of X;
  func min(b1,b2) -> ManySortedSet of X means
:: NAT_3:def 3

  for i being object holds (b1
  .i <= b2.i implies it.i = b1.i) & (b1.i > b2.i implies it.i = b2.i);
end;

registration
  let X be set;
  let b1, b2 be real-valued ManySortedSet of X;
  cluster min(b1,b2) -> real-valued;
end;

registration
  let X be set;
  let b1, b2 be natural-valued ManySortedSet of X;
  cluster min(b1,b2) -> natural-valued;
end;

theorem :: NAT_3:17
  for X being set, b1, b2 being real-valued finite-support
  ManySortedSet of X holds support min(b1,b2) c= support b1 \/ support b2;

registration
  let X be set;
  let b1, b2 be real-valued finite-support ManySortedSet of X;
  cluster min(b1,b2) -> finite-support;
end;

definition
  let X be set;
  let b1, b2 be real-valued ManySortedSet of X;
  func max(b1,b2) -> ManySortedSet of X means
:: NAT_3:def 4

  for i being object holds (b1
  .i <= b2.i implies it.i = b2.i) & (b1.i > b2.i implies it.i = b1.i);
end;

registration
  let X be set;
  let b1, b2 be real-valued ManySortedSet of X;
  cluster max(b1,b2) -> real-valued;
end;

registration
  let X be set;
  let b1, b2 be natural-valued ManySortedSet of X;
  cluster max(b1,b2) -> natural-valued;
end;

theorem :: NAT_3:18
  for X being set, b1, b2 being real-valued finite-support
  ManySortedSet of X holds support max(b1,b2) c= support b1 \/ support b2;

registration
  let X be set;
  let b1, b2 be real-valued finite-support ManySortedSet of X;
  cluster max(b1,b2) -> finite-support;
end;

registration
  let A be set;
  cluster finite-support complex-valued for ManySortedSet of A;
end;

definition
  let A be set, b be finite-support complex-valued ManySortedSet of A;
  func Product b -> Complex means
:: NAT_3:def 5

  ex f being FinSequence of COMPLEX st it = Product f & f = b*canFS(support b);
end;

definition
  let A be set, b be bag of A;
  redefine func Product b -> Element of NAT;
end;

theorem :: NAT_3:19
  for X being set, a, b being bag of X st support a misses support
  b holds Product (a+b) = (Product a) * Product b;

definition
  let X be set, b be real-valued ManySortedSet of X, n be non zero Nat;
  func b |^ n -> ManySortedSet of X means
:: NAT_3:def 6

  support it = support b & for i being object holds it.i = b.i |^ n;
end;

registration
  let X be set, b be natural-valued ManySortedSet of X, n be non zero Nat;
  cluster b |^ n -> natural-valued;
end;

registration
  let X be set, b be real-valued finite-support ManySortedSet of X,
  n be non zero Nat;
  cluster b |^ n -> finite-support;
end;

theorem :: NAT_3:20
  for A being set holds Product EmptyBag A = 1;

begin :: Multiplicity of a divisor

definition
  let n, d be Nat such that
 d <> 1 and
 n <> 0;
  func d |-count n -> Nat means
:: NAT_3:def 7

  d |^ it divides n & not d |^ (it+1) divides n;
end;

definition
  let n, d be Nat;
  redefine func d |-count n -> Element of NAT;
end;

theorem :: NAT_3:21
  n <> 1 implies n |-count 1 = 0;

theorem :: NAT_3:22
  1 < n implies n |-count n = 1;

theorem :: NAT_3:23
  b <> 0 & b < a & a <> 1 implies a |-count b = 0;

theorem :: NAT_3:24
  a <> 1 & a <> p implies a |-count p = 0;

theorem :: NAT_3:25
  1 < b implies b |-count (b|^a) = a;

theorem :: NAT_3:26
  b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a;

theorem :: NAT_3:27
  b <> 1 implies (a <> 0 & b |-count a = 0 iff not b divides a);

theorem :: NAT_3:28
  for a, b being non zero Nat holds p |-count (a*b) =
  (p |-count a) + (p |-count b);

theorem :: NAT_3:29
  for a, b being non zero Nat holds p |^ (p |-count (a
  *b)) = (p |^ (p |-count a)) * (p |^ (p |-count b));

theorem :: NAT_3:30
  for a, b being non zero Nat st b divides a holds p
  |-count b <= p |-count a;

theorem :: NAT_3:31
  for a, b being non zero Nat st b divides a holds p
  |-count (a div b) = (p |-count a) -' (p |-count b);

theorem :: NAT_3:32
  for a being non zero Nat holds p |-count (a|^b) = b
  * (p |-count a);

begin :: Exponents in prime-power factorization

definition
  let n be Nat;
  func prime_exponents n -> ManySortedSet of SetPrimes means
:: NAT_3:def 8

  for p being Prime holds it.p = p |-count n;
end;

notation
  let n be Nat;
  synonym pfexp n for prime_exponents n;
end;

theorem :: NAT_3:33
  for x being set st x in dom pfexp n holds x is Prime;

theorem :: NAT_3:34
  for x being set st x in support pfexp n holds x is Prime;

theorem :: NAT_3:35
  a > n & n <> 0 implies (pfexp n).a = 0;

registration
  let n be Nat;
  cluster pfexp n -> natural-valued;
end;

theorem :: NAT_3:36
  a in support pfexp b implies a divides b;

theorem :: NAT_3:37
  b is non empty & a is Prime & a divides b implies a in support pfexp b;

registration
  let n be non zero Nat;
  cluster pfexp n -> finite-support;
end;

theorem :: NAT_3:38
  for a being non zero Nat st p divides a holds (pfexp a).p <> 0;

theorem :: NAT_3:39
  pfexp 1 = EmptyBag SetPrimes;

registration
  cluster support pfexp 1 -> empty;
end;

theorem :: NAT_3:40
  (pfexp (p|^a)).p = a;

theorem :: NAT_3:41
  (pfexp p).p = 1;

theorem :: NAT_3:42
  a <> 0 implies support pfexp (p|^a) = {p};

theorem :: NAT_3:43
  support pfexp p = {p};

registration
  let p be Prime;
  let a be non zero Nat;
  cluster support pfexp (p|^a) -> 1-element;
end;

registration
  let p be Prime;
  cluster support pfexp p -> 1-element;
end;

theorem :: NAT_3:44
  for a, b being non zero Nat st a,b are_coprime holds
  support pfexp a misses support pfexp b;

theorem :: NAT_3:45
  for a,b being non zero Nat holds support pfexp a c=
  support pfexp (a*b);

theorem :: NAT_3:46
  for a, b being non zero Nat holds support pfexp (a*b) = support
  pfexp a \/ support pfexp b;

theorem :: NAT_3:47
  for a, b being non zero Nat st a,b are_coprime holds card
  support pfexp (a*b) = card support pfexp a + card support pfexp b;

theorem :: NAT_3:48
  for a, b being non zero Nat holds support pfexp a =
  support pfexp (a|^b);

reserve n, m for non zero Nat;

theorem :: NAT_3:49
  pfexp (n*m) = pfexp n + pfexp m;

theorem :: NAT_3:50
  m divides n implies pfexp (n div m) = pfexp n -' pfexp m;

theorem :: NAT_3:51
  pfexp (n|^a) = a * pfexp n;

theorem :: NAT_3:52
  support pfexp n = {} implies n = 1;

theorem :: NAT_3:53
  for m, n being non zero Nat holds pfexp (n gcd m) = min(pfexp n, pfexp m);

theorem :: NAT_3:54
  for m, n being non zero Nat holds pfexp (n lcm m) = max(pfexp n, pfexp m);

begin :: Prime-power factorization

definition
  let n be non zero Nat;
  func prime_factorization n -> ManySortedSet of SetPrimes means
:: NAT_3:def 9

support it = support pfexp n & for p being Nat st p in support pfexp
  n holds it.p = p |^ (p |-count n);
end;

notation
  let n be non zero Nat;
  synonym ppf n for prime_factorization n;
end;

:: for prime-power factorization

registration
  let n be non zero Nat;
  cluster ppf n -> natural-valued finite-support;
end;

theorem :: NAT_3:55
  p |-count n = 0 implies (ppf n).p = 0;

theorem :: NAT_3:56
  p |-count n <> 0 implies (ppf n).p = p |^ (p |-count n);

theorem :: NAT_3:57
  support ppf n = {} implies n = 1;

theorem :: NAT_3:58
  for a, b being non zero Nat st a, b are_coprime holds
  ppf (a*b) = ppf a + ppf b;

theorem :: NAT_3:59
  (ppf (p |^ n)).p = p |^ n;

theorem :: NAT_3:60
  ppf (n|^m) = (ppf n) |^ m;

::$N Fundamental Theorem of Arithmetic
theorem :: NAT_3:61
  Product ppf n = n;