:: On Square-free Numbers
:: by Adam Grabowski
::
:: Received July 12, 2013
:: Copyright (c) 2013-2016 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, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, ORDINAL2,
FINSEQ_1, FINSET_1, RVSUM_1, XXREAL_0, FUNCT_1, REALSET1, NAT_2,
FUNCOP_1, NEWTON, SEQ_1, SEQM_3, XCMPLX_0, NUMBERS, MATRIX13, MOEBIUS1,
SQUARE_1, ORDINAL1, PARTFUN3, FRAENKEL, CARD_1, STRUCT_0, PRE_POLY,
NAT_3, UPROOTS, LATTICES, NAT_LAT, BINOP_1, CAYLDICK, LATTICE2, XBOOLE_0,
VALUED_0, XXREAL_2, FUNCT_2, REAL_1, 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;