:: On Square-free Numbers
::  by Adam Grabowski
::
:: Received July 12, 2013
:: Copyright (c) 2013-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 ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2,
      INT_1, SQUARE_1, SEQ_1, REALSET1, SERIES_1, SEQ_2, NAT_LAT, FINSET_1,
      CARD_1, MOEBIUS1, LATTICES, PRE_POLY, XXREAL_2, MSAFREE, MOEBIUS2,
      NEWTON, XXREAL_0, XBOOLE_0, INT_2, TARSKI, PARTFUN3, NAT_1, BINOP_1,
      EQREL_1, PBOOLE, NAT_3, CARD_3, FUNCT_2, VALUED_0, UPROOTS, QUOFIELD,
      MEMBERED, INT_7, STRUCT_0, XCMPLX_0, COMPLEX1, ORDINAL1, SUBSET_1,
      ZFMISC_1, NUMBERS, REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XXREAL_0,
      XCMPLX_0, MEMBERED, ENUMSET1, ZFMISC_1, FINSET_1, MCART_1, SQUARE_1,
      COMPLEX1, ABSVALUE, INT_1, INT_2, NAT_1, XREAL_0, REAL_1, RELAT_1,
      FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, FINSEQ_1, REALSET1, FUNCOP_1,
      CARD_2, PARTFUN3, PRE_POLY, PBOOLE, NAT_D, SEQ_1, SEQ_2, FINSEQ_2,
      FINSEQ_4, RVSUM_1, STRUCT_0, BINOP_1, LATTICES, NAT_LAT, BINARITH,
      NEWTON, SERIES_1, SEQM_3, COMSEQ_2, INT_7, WSIERP_1, NAT_3, POLYNOM1,
      PEPIN, MOEBIUS1, PARTFUN1;
 constructors PARTFUN1, WELLORD2, SQUARE_1, NAT_1, BINOP_2, FINSEQOP, SEQ_1,
      VALUED_1, SIN_COS, POLYNOM2, UPROOTS, INT_7, SERIES_3, COMSEQ_2,
      ZFMISC_1, CARD_1, CARD_2, MCART_1, MOEBIUS1, ABSVALUE, COMPLEX1,
      FINSEQ_4, FINSOP_1, SETWOP_2, RVSUM_1, INT_2, NEWTON, BINARITH, BAGORDER,
      ENUMSET1, LATTICES, NAT_LAT, STRUCT_0, BINOP_1, REALSET1, SERIES_1,
      ORDINAL1, XXREAL_0, POWER, SEQ_2, REAL_1, PARTFUN3, PEPIN, PBOOLE, NAT_3,
      POLYNOM1, POLYEQ_3, RELSET_1, WSIERP_1, RSSPACE, ASYMPT_1, FUNCOP_1,
      SEQM_3, FUNCT_7, NAT_D, RECDEF_1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_2;
 registrations RELSET_1, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSET_1,
      RVSUM_1, XXREAL_0, FUNCT_1, REALSET1, FUNCOP_1, NEWTON, XCMPLX_0,
      NUMBERS, MOEBIUS1, SQUARE_1, ORDINAL1, PARTFUN3, FRAENKEL, CARD_1,
      STRUCT_0, PRE_POLY, NAT_3, LATTICES, NAT_LAT, CAYLDICK, LATTICE2,
      XBOOLE_0, VALUED_0, FUNCT_2, SUBSET_1, VALUED_1, SEQ_4;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

registration let a, b be non zero Nat;
  cluster a gcd b -> non zero;
  cluster a lcm b -> non zero;
end;

registration
  let n be Nat;
  reduce 0 -' n to 0;
end;

theorem :: MOEBIUS2:1
  for n, i being Nat st n >= 2 |^ (2 * i + 2) holds
    n / 2 >= (2 |^ i) * sqrt n;

theorem :: MOEBIUS2:2
  for n being Nat holds support pfexp n c= SetPrimes;

theorem :: MOEBIUS2:3
  for n being non zero Nat holds
    n - (n div 2) * 2 <= 1;

theorem :: MOEBIUS2:4
  for a,n being non zero Nat holds
    (n div a) * a <= n;

theorem :: MOEBIUS2:5
  for a, b being non zero Nat st
    not a, b are_coprime holds
      ex k being non zero Nat st k <> 1 & k divides a & k divides b;

theorem :: MOEBIUS2:6
  for n,a being non zero Nat st a divides n holds
    n div a <> 0;

theorem :: MOEBIUS2:7
  for i,j being Nat st i,j are_coprime holds i lcm j = i * j;

registration let f be natural-valued FinSequence;
  cluster Product f -> natural;
end;

begin :: Prime Numbers

theorem :: MOEBIUS2:8
  primenumber 0 = 2;

theorem :: MOEBIUS2:9
  SetPrimenumber 3 = {2};

theorem :: MOEBIUS2:10
  primenumber 1 = 3;

theorem :: MOEBIUS2:11
  SetPrimenumber 5 = {2, 3};

theorem :: MOEBIUS2:12
  primenumber 2 = 5;

theorem :: MOEBIUS2:13
  SetPrimenumber 6 = {2, 3, 5};

theorem :: MOEBIUS2:14
  SetPrimenumber 7 = {2, 3, 5};

theorem :: MOEBIUS2:15
  primenumber 3 = 7;

theorem :: MOEBIUS2:16
  SetPrimenumber 11 = {2, 3, 5, 7};

theorem :: MOEBIUS2:17
  primenumber 4 = 11;

theorem :: MOEBIUS2:18
  SetPrimenumber 13 = {2, 3, 5, 7, 11};

theorem :: MOEBIUS2:19
  primenumber 5 = 13;

theorem :: MOEBIUS2:20
  for m, n being Nat holds
     SetPrimenumber m c= SetPrimenumber n
    or SetPrimenumber n c= SetPrimenumber m;

theorem :: MOEBIUS2:21
  for n, m being Nat holds n < m iff primenumber n < primenumber m;

begin :: Prime Reciprocals

 reserve n,i for Nat;

definition
  func ReciPrime -> Real_Sequence means
:: MOEBIUS2:def 1
    for i being Nat holds
      it.i = 1 / primenumber i;
end;

notation let f be Real_Sequence;
  antonym f is divergent for f is convergent;
end;

registration
  cluster ReciPrime -> decreasing bounded_below;
end;

registration
  cluster ReciPrime -> convergent;
end;

definition
  func invNAT -> Real_Sequence means
:: MOEBIUS2:def 2
    for i being Nat holds it.i = 1 / i;
end;

registration
  cluster invNAT -> nonnegative-yielding;
end;

registration
  cluster invNAT -> convergent;
end;

theorem :: MOEBIUS2:22
  lim invNAT = 0;

theorem :: MOEBIUS2:23
  ReciPrime is subsequence of invNAT;

registration let f be nonnegative-yielding Real_Sequence;
  cluster -> nonnegative-yielding for subsequence of f;
end;

registration
  cluster ReciPrime -> nonnegative-yielding;
end;

theorem :: MOEBIUS2:24
  lim ReciPrime = 0;

registration
  cluster Partial_Sums ReciPrime -> non-decreasing for Real_Sequence;
end;

theorem :: MOEBIUS2:25
  for f being nonnegative-yielding Real_Sequence st f is summable holds
    for p being Real st p > 0 holds
    ex i being Element of NAT st Sum (f ^\ i) < p;

begin :: Square Factors

definition let n be non zero Nat;
  func SqFactors n -> ManySortedSet of SetPrimes means
:: MOEBIUS2:def 3
  support it = support pfexp n &
  for p being Nat st p in support pfexp n holds
    it.p = p |^ ((p |-count n) div 2);
end;

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

registration let n be non zero Nat;
  cluster -> natural for Element of support SqFactors n;
end;

definition let n be non zero Nat;
  func SqF n -> Nat equals
:: MOEBIUS2:def 4
    Product SqFactors n;
end;

theorem :: MOEBIUS2:26
  for f being bag of SetPrimes holds Product f <> 0;

registration let n be non zero Nat;
  cluster SqF n -> non zero;
end;

definition let p be Prime;
  func FreeGen p -> Subset of NAT means
:: MOEBIUS2:def 5
    for n being Nat holds n in it iff
      n is square-free & for i being Prime st i divides n holds i <= p;
end;

 reserve p for Prime;

theorem :: MOEBIUS2:27
  1 in FreeGen p;

theorem :: MOEBIUS2:28
  not 0 in FreeGen p;

registration
  cluster square-free non zero for Nat;
end;

registration let p;
  cluster positive-yielding for bag of Seg p;
end;

theorem :: MOEBIUS2:29
  for f being positive-yielding bag of Seg p holds
    dom f = support f;

theorem :: MOEBIUS2:30
  dom canFS Seg p = Seg p;

theorem :: MOEBIUS2:31
  for A being finite set holds
    dom canFS A = Seg card A;

theorem :: MOEBIUS2:32
  for g being positive-yielding bag of Seg p st g = p |-> p holds
    g = g * canFS support g;

theorem :: MOEBIUS2:33
  for f being positive-yielding bag of Seg p st f = p |-> p holds
    Product f = p |^ p;

theorem :: MOEBIUS2:34
  for n being non zero Nat st n in FreeGen p holds
    support pfexp n c= Seg p;

theorem :: MOEBIUS2:35
  for n being non zero Nat st n in FreeGen p holds
    card support pfexp n <= p;

theorem :: MOEBIUS2:36
  for n being square-free non zero Nat holds
    rng pfexp n c= 2;

theorem :: MOEBIUS2:37
  for m, n being non zero Nat st pfexp m = pfexp n holds
    m = n;

registration let p be Prime;
  cluster FreeGen p -> non empty;
end;

registration let p be Prime;
  cluster -> non empty for Element of FreeGen p;
end;

definition let p be Prime;
  func BoolePrime p -> set equals
:: MOEBIUS2:def 6
    Funcs ((Seg p) /\ SetPrimes, 2);
end;

registration let p be Prime;
  cluster BoolePrime p -> finite;
end;

definition let p be Prime;
  func canHom p -> Function of FreeGen p, BoolePrime p means
:: MOEBIUS2:def 7
    for x being Element of FreeGen p holds
      it.x = (pfexp x) | (Seg p /\ SetPrimes);
end;

registration let p be Prime;
  cluster canHom p -> one-to-one;
end;

theorem :: MOEBIUS2:38
  card FreeGen p c= card BoolePrime p;

registration let p be Prime;
  cluster FreeGen p -> finite;
end;

theorem :: MOEBIUS2:39
  card FreeGen p <= 2 |^ p;

theorem :: MOEBIUS2:40  :: MOEBIUS1:9 inverted
  n <> 0 & (p |^ i) divides n implies i <= p |-count n;

theorem :: MOEBIUS2:41  :: MOEBIUS1:24 inverted
  n <> 0 & (for p being Prime holds p |-count n <= 1) implies
    n is square-free;

theorem :: MOEBIUS2:42
  for p being Prime, n being non zero Nat st
    p |-count n = 0 holds (SqFactors n).p = 0;

theorem :: MOEBIUS2:43
  for n being non zero Nat, p being Prime st
    p |-count n <> 0 holds
      (SqFactors n).p = p |^ ((p |-count n) div 2);

theorem :: MOEBIUS2:44
  for m, n being non zero Nat st
    m, n are_coprime holds
      SqFactors (m * n) = SqFactors m + SqFactors n;

theorem :: MOEBIUS2:45
  for n being non zero Nat holds SqF n divides n;

registration let n be non zero Nat;
  cluster PFactors n -> prime-factorization-like;
end;

theorem :: MOEBIUS2:46
  for f being bag of SetPrimes
    ex g being FinSequence of NAT st
    Product f = Product g & g = f*canFS(support f);

theorem :: MOEBIUS2:47
  for f being bag of SetPrimes st f.p = p |^ n holds
    p |^ n divides Product f;

theorem :: MOEBIUS2:48
  for f being bag of SetPrimes st f.p = p |^ n holds
    p |-count Product f >= n;

begin :: Extracting Square-Containing and Square-Free Part of a Number

definition let n be non zero Nat;
  func TSqFactors n -> ManySortedSet of SetPrimes means
:: MOEBIUS2:def 8
  support it = support pfexp n &
  for p being Nat st p in support pfexp n holds
    it.p = p |^ (2 * ((p |-count n) div 2));
end;

theorem :: MOEBIUS2:49
  for n being non zero Nat holds
    TSqFactors n = (SqFactors n) |^ 2;

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

definition let n be non zero Nat;
  func TSqF n -> Nat equals
:: MOEBIUS2:def 9
    Product TSqFactors n;
end;

registration let n be non zero Nat;
  cluster TSqF n -> non zero;
end;

theorem :: MOEBIUS2:50
  for p being Prime, n being non zero Nat holds
    p |-count n = 0 implies (TSqFactors n).p = 0;

theorem :: MOEBIUS2:51
  for n being non zero Nat, p being Prime st
    p |-count n <> 0 holds
      (TSqFactors n).p = p |^ (2 * ((p |-count n) div 2));

theorem :: MOEBIUS2:52
  for m, n being non zero Nat st
    m, n are_coprime holds
      TSqFactors (m * n) = TSqFactors m + TSqFactors n;

registration let n be non zero Nat;
  cluster support TSqFactors n -> natural-membered;
end;

theorem :: MOEBIUS2:53
  for n being non zero Nat holds TSqF n divides n;

registration
  let n be non zero Nat;
  cluster n div TSqF n -> square-free for Nat;
end;

theorem :: MOEBIUS2:54
  for n,k being non zero Nat st
    k <> 1 & k ^2 divides n holds
   n is square-containing;

theorem :: MOEBIUS2:55
  for n being square-free non zero Nat,
      a being non zero Nat st a divides n holds
    a, n div a are_coprime;

begin :: Binary Operations

theorem :: MOEBIUS2:56
  for A, C being non empty set,
      L being commutative BinOp of A,
      LC being BinOp of C st
    C c= A & LC = L || C holds
     LC is commutative;

theorem :: MOEBIUS2:57
  for A, C being non empty set,
      L being associative BinOp of A,
      LC being BinOp of C st
    C c= A & LC = L || C holds
     LC is associative;

registration let C be non empty set;
  let L be commutative BinOp of C,
      M be BinOp of C;
  cluster LattStr (# C, L, M #) -> join-commutative;
end;

registration let C be non empty set;
  let L be BinOp of C,
      M be commutative BinOp of C;
  cluster LattStr (# C, L, M #) -> meet-commutative;
end;

registration let C be non empty set;
  let L be associative BinOp of C,
      M be BinOp of C;
  cluster LattStr (# C, L, M #) -> join-associative;
end;

registration let C be non empty set;
  let L be BinOp of C,
      M be associative BinOp of C;
  cluster LattStr (# C, L, M #) -> meet-associative;
end;

begin :: On the Natural Divisors

theorem :: MOEBIUS2:58
  for n being non zero Nat holds NatDivisors n c= NATPLUS;

theorem :: MOEBIUS2:59
  for n being non zero Nat,
      x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
    x lcm y in NatDivisors n;

theorem :: MOEBIUS2:60
  for n being non zero Nat,
      x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
    x gcd y in NatDivisors n;

registration let n be non zero Nat;
  cluster NatDivisors n -> non empty;
end;

registration
  cluster hcflat -> commutative associative;
  cluster lcmlat -> commutative associative;
end;

theorem :: MOEBIUS2:61
  hcflatplus = hcflat || NATPLUS;

theorem :: MOEBIUS2:62
  lcmlatplus = lcmlat || NATPLUS;

registration
  cluster hcflatplus -> commutative;
  cluster lcmlatplus -> commutative;
  cluster hcflatplus -> associative;
  cluster lcmlatplus -> associative;
end;

begin :: The Lattice of Natural Divisors

::$N The lattice of natural divisors

definition let n be non zero Nat;
  func Divisors_Lattice n -> strict SubLattice of NatPlus_Lattice means
:: MOEBIUS2:def 10

    the carrier of it = NatDivisors n;
end;

registration let n be non zero Nat;
  cluster the carrier of Divisors_Lattice n -> natural-membered;
end;

theorem :: MOEBIUS2:63
  for n being non zero Nat,
      a, b being Element of Divisors_Lattice n holds
    a "\/" b = a lcm b &
    a "/\" b = a gcd b;

registration
  let n be non zero Nat;
  let p,q be Element of Divisors_Lattice n;
  identify p "\/" q with p lcm q;
  identify p "/\" q with p gcd q;
end;

registration let n be non zero Nat;
  cluster Divisors_Lattice n -> non empty;
end;

registration let n be non zero Nat;
  cluster Divisors_Lattice n -> distributive bounded;
end;

theorem :: MOEBIUS2:64
  for n being non zero Nat holds
    Top Divisors_Lattice n = n &
    Bottom Divisors_Lattice n = 1;

registration let n be square-free non zero Nat;
  cluster Divisors_Lattice n -> Boolean;
end;

registration let n be non zero Nat;
  cluster -> non zero for Element of Divisors_Lattice n;
end;

theorem :: MOEBIUS2:65
  for n being non zero Nat holds
    Divisors_Lattice n is Boolean iff n is square-free;