:: Elementary Number Theory Problems. {P}art {XVIII}
:: by Adam Grabowski
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 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 4.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/4.0/.
environ
vocabularies NUMBERS, NAT_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_3, XCMPLX_0,
CARD_1, INT_1, NEWTON, INT_2, ARYTM_1, SUBSET_1, XBOOLE_0, TARSKI,
FINSET_1, PBOOLE, ABIAN, SQUARE_1, MEMBERED, ZFMISC_1, ORDINAL1, POWER,
REAL_1, PARTFUN3, VALUED_0, REALSET1, NUMPOLY1, EUCLID_3, FUNCT_7,
ORDINAL2, MOEBIUS1, FINSEQ_1, CARD_3, NUMBER06, PRE_POLY, NAT_3,
PARTFUN1, PEPIN, ORDINAL4, FUNCOP_1, NUMBER18, GR_CY_3, NUMBER12, NAT_5,
PROB_1, RFUNCT_3, FINSEQ_2, MSSUBFAM, NEWTON04, UPROOTS, ROBBINS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, CARD_1,
XTUPLE_0, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PBOOLE, FINSET_1,
MEMBERED, FUNCOP_1, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, XXREAL_0,
RFINSEQ, CARD_3, FUNCT_2, PARTFUN1, FINSEQ_1, SQUARE_1, FINSEQ_2,
FINSEQ_4, RVSUM_1, SGRAPH1, VALUED_0, PARTFUN3, VALUED_1, POWER, NEWTON,
ABIAN, SERIES_1, AFINSQ_1, PRE_POLY, NAT_3, PEPIN, INT_5, WSIERP_1,
GR_CY_3, UPROOTS, RFUNCT_3, NEWTON04, EULER_2, PYTHTRIP, NAT_5, MOEBIUS1,
NUMPOLY1, NUMBER06, NUMBER12;
constructors NAT_D, RELSET_1, NEWTON, ABIAN, NAT_6, ENUMSET1, EULER_1, PEPIN,
PYTHTRIP, PREPOWER, QUIN_1, SERIES_1, PARTFUN3, NUMPOLY1, MOEBIUS1,
FUNCOP_1, FINSOP_1, NAT_5, GR_CY_3, SGRAPH1, PRE_POLY, SQUARE_1, NAT_3,
LATSTONE, FINSEQ_4, INT_5, RVSUM_1, EULER_2, NUMBER04, RFINSEQ, FINSEQ_1,
SEQ_1, AFINSQ_1, PRE_FF, FIB_NUM2, NEWTON03, DOMAIN_1, CARD_3, NUMBER02,
NUMBER06, INT_7, WSIERP_1, RECDEF_1, NUMBER12, UPROOTS, CLASSES1,
RFUNCT_3, RVSUM_2, NEWTON04;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, CARD_1, SQUARE_1, NEWTON,
NEWTON02, NEWTON03, FOMODEL0, ABIAN, NAT_6, JORDAN1D, POWER, SERIES_1,
LIOUVIL1, WSIERP_1, QUIN_1, AFINSQ_2, FUNCT_2, RELAT_1, XBOOLE_0,
FUNCT_1, NUMPOLY1, RVSUM_1, SEQ_1, NUMBER02, NUMBER06, NAT_3, LATSTONE,
NEWTON04, FINSEQ_1, NUMBER15, MOEBIUS1, NAT_5, PRE_POLY, MOEBIUS2,
NEWTON01, INT_6, NIVEN, VALUED_1, NUMBER10, HILB10_4, FUNCOP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RELAT_1, MEMBERED, TARSKI, XBOOLE_0, NAT_D, INT_2, SEQM_3,
NUMBER02;
equalities SQUARE_1, NAT_6, QUIN_1, ORDINAL1, SUBSET_1, XCMPLX_0, NUMBER12,
FINSEQ_1, FINSEQ_2;
expansions ORDINAL1, INT_1, INT_2, ZFMISC_1, NUMBER12;
theorems NEWTON, WSIERP_1, INT_1, INT_2, NAT_D, NEWTON03, PEPIN, EULER_2,
ORDINAL1, XREAL_1, XXREAL_0, NAT_1, XCMPLX_1, NAT_3, XBOOLE_0, PYTHTRIP,
FUNCT_1, PARTFUN1, NAT_6, TARSKI, NAT_5, ENUMSET1, CARD_1, POWER,
PREPOWER, PARTFUN3, NUMPOLY1, MOEBIUS2, XREAL_0, FUNCT_2, NUMBERS, ABIAN,
VALUED_0, FINSEQ_1, RELAT_1, MOEBIUS1, LATSTONE, CARD_2, XBOOLE_1, NAT_2,
XPRIMES1, RVSUM_1, FUNCOP_1, PRE_POLY, NUMBER04, NUMBER05, NUMBER06,
FINSEQ_3, NUMBER12, GR_CY_3, SGRAPH1, NUMBER15, PBOOLE, RFUNCT_3,
NEWTON01, GROUP_22, NEWTON06, GROUPP_1, FINSEQ_2, NEWTON04, LAGRA4SQ,
NUMBER14, RFINSEQ, UPROOTS, AFINSQ_2, MEMBERED, NUMBER07, XCMPLX_0,
VALUED_1;
schemes NAT_1, FUNCT_2, CLASSES1, BINOP_2;
begin :: Preliminaries
Lm1:
for x being Nat holds x |^ 3 = x * x * x
proof
let x be Nat;
x |^ (2+1) = x |^ 2 * x by NEWTON:6
.= x * x * x by NEWTON:81;
hence thesis;
end;
begin :: Problem 53
:: Prove that for every positive integer k the set of all positive integers
:: n whose number of positive integer divisors is divisible by k contains an
:: infinite arithmetic progression.
:: NatDivisors Revisited
definition let n be Nat;
func Bnumber_of_divisors n -> ManySortedSet of SetPrimes means :BDef:
support it = support pfexp n &
for p being Nat st p in support pfexp n holds
it.p = (p |-count n) + 1;
existence
proof
defpred P[object,object] means
for p being Prime st $1 = p holds
(p in support pfexp n implies $2 = (p |-count n) + 1) &
(not p in support pfexp n implies $2 = 0);
A1: for x being object st x in SetPrimes ex y being object st P[x,y]
proof
let x be object;
assume x in SetPrimes;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
per cases;
suppose
A2: i in support pfexp n;
take (i |-count n) + 1;
let p be Prime;
assume p = x;
hence thesis by A2;
end;
suppose
A3: not i in support pfexp n;
take 0;
let p be Prime;
assume p = x;
hence thesis by A3;
end;
end;
consider f being Function such that
A4: dom f = SetPrimes and
A5: for x being object st x in SetPrimes holds P[x,f.x]
from CLASSES1:sch 1(A1);
A6: support f c= SetPrimes by A4,PRE_POLY:37;
A7: now
let x be object;
hereby
assume
A8: x in support f;
then x in SetPrimes by A6;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
assume not x in support pfexp n;
then f.i = 0 by A5,A6,A8;
hence contradiction by A8,PRE_POLY:def 7;
end;
ZX: support pfexp n c= SetPrimes by MOEBIUS2:2;
assume
A9: x in support pfexp n; then
AA: x in SetPrimes by ZX;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
f.i = (i |-count n) + 1 by A9,AA,A5;
hence x in support f by PRE_POLY:def 7;
end;
reconsider f as ManySortedSet of SetPrimes
by A4,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus support f = support pfexp n by A7,TARSKI:2;
let p be Nat;
assume
A10: p in support pfexp n; then
p is Prime by NAT_3:34; then
reconsider p1 = p as Prime;
p1 in SetPrimes by NEWTON:def 6;
hence thesis by A5,A10;
end;
uniqueness
proof
let it1, it2 be ManySortedSet of SetPrimes such that
A11: support it1 = support pfexp n and
A12: for p being Nat st p in support pfexp n holds it1.p = (p |-count n) + 1
and
A13: support it2 = support pfexp n and
A14: for p being Nat st p in support pfexp n holds it2.p = (p |-count n) + 1;
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
per cases;
suppose
A15: p in support pfexp n;
hence it1.i = (p |-count n) + 1 by A12
.= it2.i by A14,A15;
end;
suppose
A16: not p in support pfexp n;
hence it1.i = 0 by A11,PRE_POLY:def 7
.= it2.i by A13,A16,PRE_POLY:def 7;
end;
end;
hence it1 = it2 by PBOOLE:3;
end;
end;
registration
let n be non zero Nat;
cluster Bnumber_of_divisors n -> natural-valued finite-support;
coherence
proof
A1: rng Bnumber_of_divisors n c= NAT
proof
let x be object;
assume x in rng Bnumber_of_divisors n;
then consider y being object such that
A2: y in dom Bnumber_of_divisors n and
A3: (Bnumber_of_divisors n).y = x by FUNCT_1:def 3;
A4: y in SetPrimes by A2,PARTFUN1:def 2;
per cases;
suppose
S1: y in support pfexp n;
reconsider p = y as Prime by A4,NEWTON:def 6;
x = (p |-count n) + 1 by S1,A3,BDef;
hence thesis;
end;
suppose
not y in support pfexp n;
then not y in support Bnumber_of_divisors n by BDef;
then x = 0 by A3,PRE_POLY:def 7;
hence thesis;
end;
end;
T1: support Bnumber_of_divisors n = support pfexp n by BDef;
thus Bnumber_of_divisors n is natural-valued by A1,VALUED_0:def 6;
thus thesis by T1,PRE_POLY:def 8;
end;
end;
definition let n be non zero Nat;
func number_of_divisors n -> Nat equals
Product Bnumber_of_divisors n;
coherence;
end;
theorem
for p being Prime holds (Bnumber_of_divisors p) * <*p*> = <*2*>
proof
let p be Prime;
set f = <*p*>, g = Bnumber_of_divisors p;
set z = <*2*>;
A1: dom (g * f) = {1}
proof
thus dom (g * f) c= {1}
proof
let x be object;
assume x in dom (g * f);
then x in dom f by FUNCT_1:11;
hence thesis by FINSEQ_1:2,38;
end;
let x be object;
assume
A2: x in {1};
then x = 1 by TARSKI:def 1;
then f.x in SetPrimes by NEWTON:def 6;
then
A3: f.x in dom g by PARTFUN1:def 2;
x in dom f by A2,FINSEQ_1:2,38;
hence thesis by A3,FUNCT_1:11;
end;
A4: for x being object st x in dom (g * f) holds (g * f).x = z.x
proof
let x be object;
(pfexp p).p <> 0 by NAT_3:38; then
A5: p in support pfexp p by PRE_POLY:def 7;
SX: p > 1 by INT_2:def 4;
assume
A6: x in dom (g * f); then
A7: x = 1 by A1,TARSKI:def 1;
then (g * f).1 = g.(f.1) by A6,FUNCT_1:12
.= p |-count p + 1 by A5,BDef
.= 1 + 1 by SX,NAT_3:22
.= z.1;
hence thesis by A7;
end;
dom z = {1} by FINSEQ_1:2,38;
hence thesis by A1,A4,FUNCT_1:2;
end;
theorem
Bnumber_of_divisors 1 = EmptyBag SetPrimes
proof
set f = Bnumber_of_divisors 1;
for z being object st z in dom f holds f.z = 0
proof
let z be object;
assume z in dom f;
then z in SetPrimes by PARTFUN1:def 2;
then reconsider z as Element of NAT;
support pfexp 1 = {};
then not z in support f by BDef;
hence thesis by PRE_POLY:def 7;
end; then
A1: f = (dom f) --> 0 by FUNCOP_1:11;
dom f = SetPrimes by PARTFUN1:def 2;
hence thesis by A1,PBOOLE:def 3;
end;
theorem Th48:
for p being Prime, n being non zero Nat holds
p |-count n = 0 implies (Bnumber_of_divisors n).p = 0
proof
let p be Prime, n be non zero Nat;
assume p |-count n = 0;
then (pfexp n).p = 0 by NAT_3:def 8;
then not p in support pfexp n by PRE_POLY:def 7;
then not p in support Bnumber_of_divisors n by BDef;
hence thesis by PRE_POLY:def 7;
end;
theorem Th49:
for n being non zero Nat, p being Prime st
p |-count n <> 0 holds
(Bnumber_of_divisors n).p = (p |-count n) + 1
proof
let n be non zero Nat, p be Prime;
assume p |-count n <> 0;
then (pfexp n).p <> 0 by NAT_3:def 8;
then p in support pfexp n by PRE_POLY:def 7;
hence thesis by BDef;
end;
theorem Th50:
for m, n being non zero Nat st m, n are_coprime holds
Bnumber_of_divisors (m * n) =
Bnumber_of_divisors m + Bnumber_of_divisors n
proof
let a, b be non zero Nat;
reconsider an = a, bn = b as non zero Nat;
assume
A1: a, b are_coprime;
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A2: p |-count (an*bn) = (p |-count a) + (p |-count b) by NAT_3:28;
A4: p > 1 by INT_2:def 4;
per cases;
suppose
A5: p |-count (a*b) = 0; then
A6: (p |-count b) = 0 by A2;
A7: (p |-count a) = 0 by A2,A5;
thus (Bnumber_of_divisors (a*b)).i = 0 by A5,Th48
.= 0 + (Bnumber_of_divisors b).i by A6,Th48
.= (Bnumber_of_divisors a).i + (Bnumber_of_divisors b).i by A7,Th48
.= (Bnumber_of_divisors a + Bnumber_of_divisors b).i
by PRE_POLY:def 5;
end;
suppose
A8: p |-count (a*b) <> 0;
thus (Bnumber_of_divisors (a*b)).i =
(Bnumber_of_divisors a + Bnumber_of_divisors b).i
proof
per cases by A2,A8;
suppose
A9: (p |-count a) <> 0;
A10: now
consider ka being Nat such that
A11: (p |-count a) = ka+1 by A9,NAT_1:6;
reconsider ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4,NAT_3:def 7;
then p*(p|^ka) divides a by A11,NEWTON:6;
then consider la being Nat such that
A12: a = p*(p|^ka)*la by NAT_D:def 3;
a = p*((p|^ka)*la) by A12; then
A13: p divides a;
assume (p |-count b) <> 0;
then consider kb being Nat such that
A14: (p |-count b) = kb+1 by NAT_1:6;
reconsider kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4,NAT_3:def 7;
then p*(p|^kb) divides b by A14,NEWTON:6;
then consider lb being Nat such that
A15: b = p*(p|^kb)*lb by NAT_D:def 3;
b = p*((p|^kb)*lb) by A15;
then p divides b;
then p divides 1 by A1,A13,NAT_D:def 5;
hence contradiction by A4,NAT_D:7;
end;
thus (Bnumber_of_divisors (a*b)).i = (p |-count (a*b)) + 1
by A8,Th49
.= (p |-count a) + (p |-count b) + 1 by NAT_3:28
.= (p |-count a) + 1 + (p |-count b)
.= (Bnumber_of_divisors a).p + (p |-count b) by A9,Th49
.= (Bnumber_of_divisors a).p + (Bnumber_of_divisors b).p
by A10,Th48
.= (Bnumber_of_divisors a + Bnumber_of_divisors b).i
by PRE_POLY:def 5;
end;
suppose
A16: (p |-count b) <> 0;
A17: now
assume (p |-count a) <> 0;
then consider ka being Nat such that
A18: (p |-count a) = ka+1 by NAT_1:6;
reconsider ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4,NAT_3:def 7;
then p*(p|^ka) divides a by A18,NEWTON:6;
then consider la being Nat such that
A19: a = p*(p|^ka)*la by NAT_D:def 3;
a = p*((p|^ka)*la) by A19; then
A20: p divides a;
consider kb being Nat such that
A21: (p |-count b) = kb+1 by A16,NAT_1:6;
reconsider kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4,NAT_3:def 7;
then p*(p|^kb) divides b by A21,NEWTON:6;
then consider lb being Nat such that
A22: b = p*(p|^kb)*lb by NAT_D:def 3;
b = p*((p|^kb)*lb) by A22;
then p divides b;
then p divides 1 by A1,A20,NAT_D:def 5;
hence contradiction by A4,NAT_D:7;
end;
thus (Bnumber_of_divisors (a*b)).i = (p |-count (a*b)) + 1
by A8,Th49
.= (p |-count a) + (p |-count b) + 1 by NAT_3:28
.= (p |-count a) + ((p |-count b) + 1)
.= (p |-count a) + (Bnumber_of_divisors b).p by A16,Th49
.= (Bnumber_of_divisors a).p + (Bnumber_of_divisors b).p
by A17,Th48
.= (Bnumber_of_divisors a + Bnumber_of_divisors b).i
by PRE_POLY:def 5;
end;
end;
end;
end;
hence thesis by PBOOLE:3;
end;
::: sigma (k,n) from NAT_5:def 2 is sigma_k (n)
::: sigma (1,n) is the sum of divisors
::: sigma (0,n) is the number of divisors
definition let n be Nat;
func #divs n -> Nat equals
sigma (0,n);
coherence;
end;
theorem ThEXP0:
EXP 0 = NAT --> 1
proof
set f = EXP 0;
set g = NAT --> 1;
for n being Element of NAT holds f.n = g.n
proof
let n be Element of NAT;
f.n = n |^ 0 by NAT_5:def 1
.= g.n by NEWTON:4;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
EXP 1 = id NAT
proof
set f = EXP 1;
set g = id NAT;
for n being Element of NAT holds f.n = g.n
proof
let n be Element of NAT;
f.n = n |^ 1 by NAT_5:def 1
.= g.n;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for n being Nat st n = 0 holds
#divs n = 0 by NAT_5:def 2;
ETRANS:
for i be Nat, r be Real holds
Sum(i |-> r) = i * r by RVSUM_1:80;
theorem LemmaCard:
for X being finite Subset of NAT holds
Sum ((NAT --> 1) | X) = card X
proof
let X be finite Subset of NAT;
per cases;
suppose
AA: X = {}; then
(NAT --> 1) | X = {}
.= X --> {} by AA; then
(NAT --> 1) | X = EmptyMS X by PBOOLE:def 3; then
(NAT --> 1) | X = EmptyBag X; then
A3: Sum ((NAT --> 1) | X) = 0 by UPROOTS:11;
card X = 0 by AA;
hence thesis by A3;
end;
suppose
F1: X <> {};
set f = NAT --> 1;
NAT c= REAL by NUMBERS:19; then
reconsider F = f as PartFunc of NAT, REAL by FUNCT_2:7;
A1: Sum (f|X) = Sum (F,X) by NAT_5:25;
A2: Sum (F,X) = Sum FinS (F,X) by RFUNCT_3:def 14;
reconsider Z = dom (F|X) as finite set;
f3: dom F = NAT;
F|X = (X /\ NAT) --> 1 by FUNCOP_1:12
.= X --> 1 by XBOOLE_1:28; then
rng (F|X) = {1} by F1,FUNCOP_1:8; then
F2: Sum FinS (F, X) = Sum (card Z |-> 1) by RFUNCT_3:75;
Sum (card Z |-> 1) = 1 * card Z by ETRANS;
hence thesis by A1,A2,F2,f3;
end;
end;
theorem
for p being Prime holds
#divs p = 2
proof
let p be Prime;
set X = NatDivisors p;
D2: EXP 0 = NAT --> 1 by ThEXP0;
D1: NatDivisors p = {1,p} by LATSTONE:26;
D3: #divs p = Sum ((EXP 0) | X) by NAT_5:def 2;
1 <> p by INT_2:def 4; then
card X = 2 by D1,CARD_2:57;
hence thesis by D3,D2,LemmaCard;
end;
theorem
for m,n being non zero Nat st
m,n are_coprime holds
number_of_divisors (m * n) =
(number_of_divisors m) * (number_of_divisors n)
proof
let m, n be non zero Nat;
assume
W1: m, n are_coprime; then
AA: Bnumber_of_divisors (m * n) =
Bnumber_of_divisors m + Bnumber_of_divisors n by Th50;
support Bnumber_of_divisors m = support pfexp m &
support Bnumber_of_divisors n = support pfexp n by BDef; then
KK: support Bnumber_of_divisors m misses support Bnumber_of_divisors n
by W1,NAT_3:44;
hence thesis by AA,NAT_3:19;
end;
theorem ThDivs:
for n being non zero Nat holds
#divs n = card NatDivisors n
proof
let n be non zero Nat;
reconsider z = 0 as Nat;
set f = EXP z;
set X = NatDivisors n;
D1: #divs n = Sum (f | X) by NAT_5:def 2;
f = NAT --> 1 by ThEXP0;
hence thesis by D1,LemmaCard;
end;
theorem CardSucc: :: trivial as k \/ {k} = succ k
for k being Nat holds
card (k \/ {k}) = k + 1
proof
let k be Nat;
not k in k; then
card (k \/ {k}) = card k + 1 by CARD_2:41
.= k + 1;
hence thesis;
end;
theorem CardNatDiv:
for p being Prime,
k being Nat holds
card NatDivisors (p |^ k) = k + 1
proof
let p be Prime,
k be Nat;
B1: {l where l is Element of NAT : l <= k} = k \/ {k}
proof
thus {l where l is Element of NAT : l <= k} c= k \/ {k}
proof
let x be object;
assume x in {l where l is Element of NAT : l <= k}; then
consider ll being Element of NAT such that
A1: ll = x & ll <= k;
ll < k or ll = k by A1,XXREAL_0:1; then
ll in Segm k or ll in {k} by NAT_1:44,TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 3;
end;
let x be object;
assume x in k \/ {k}; then
x in k or x in {k} by XBOOLE_0:def 3; then
A2: x in Segm k or x = k by TARSKI:def 1; then
reconsider ll = x as Element of NAT by ORDINAL1:def 12;
ll <= k by A2,NAT_1:44;
hence thesis;
end;
B2: card NatDivisors (p|^k) =
card {p|^l where l is Element of NAT : l <= k} by NAT_5:19;
deffunc F(Element of NAT) = p |^ $1;
set X = { l where l is Element of NAT : l <= k };
set YY = { F(w) where w is Element of NAT : w in X };
ZZ: YY = { p |^ l where l is Element of NAT : l <= k }
proof
thus YY c= { p |^ l where l is Element of NAT : l <= k }
proof
let a be object;
assume a in YY; then
consider w being Element of NAT such that
E1: a = F(w) & w in X;
consider ll being Element of NAT such that
E2: ll = w & ll <= k by E1;
thus thesis by E1,E2;
end;
let a be object;
assume a in { p |^ l where l is Element of NAT : l <= k }; then
consider ll being Element of NAT such that
E3: a = p |^ ll & ll <= k;
a = F(ll) & ll in X by E3;
hence thesis;
end;
YY c= Seg (p |^ k) \/ {p |^ k}
proof
let u be object;
assume u in YY; then
consider ll being Element of NAT such that
W1: u = p |^ ll & ll <= k by ZZ;
W0: p > 1 by INT_2:def 4; then
p |^ ll >= p |^ 0 by PREPOWER:93; then
W2: 1 <= p |^ ll by NEWTON:4;
p |^ ll <= p |^ k by W1,W0,PREPOWER:93; then
p |^ ll in Seg (p |^ k) by W2;
hence thesis by W1,XBOOLE_0:def 3;
end; then
reconsider YY as finite set;
set FF = {l where l is Element of NAT : l <= k};
deffunc F(Element of NAT) = In (p |^ $1,NAT);
ex f being Function of NAT,NAT st
for x being Element of NAT holds
f.x = F(x) from FUNCT_2:sch 4; then
consider ff being Function of NAT, NAT such that
C0: for x being Element of NAT holds ff.x = F(x);
set f = ff | FF;
FF c= NAT
proof
let x be object;
assume x in FF; then
consider ll being Element of NAT such that
G1: x = ll & ll <= k;
thus thesis by G1;
end; then
FF c= dom ff by FUNCT_2:def 1; then
Z1: dom f = FF by RELAT_1:62;
Z2: rng f = YY
proof
thus rng f c= YY
proof
let y be object;
assume
y in rng f; then
consider yy being object such that
C1: yy in dom f & y = f.yy by FUNCT_1:def 3;
consider ll being Element of NAT such that
C2: ll = yy & ll <= k by C1,Z1;
C3: y = f.ll by C1,C2;
ll in FF by C2; then
y = ff.ll by C3,FUNCT_1:49; then
y = In (p |^ ll, NAT) by C0;
hence thesis by ZZ,C2;
end;
let y be object;
assume y in YY; then
consider ll being Element of NAT such that
D1: y = p |^ ll & ll <= k by ZZ;
D5: ll in FF by D1; then
D6: ll in dom f by Z1;
D7: f.ll = ff.ll by D5,FUNCT_1:49;
ff.ll = In (p |^ ll,NAT) by C0
.= p |^ ll;
hence thesis by D1,D7,D6,FUNCT_1:def 3;
end;
for x1,x2 being object st x1 in dom ff & x2 in dom ff & ff.x1 = ff.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
DD: x1 in dom ff & x2 in dom ff & ff.x1 = ff.x2; then
reconsider n1 = x1, n2 = x2 as Element of NAT by FUNCT_2:def 1;
DA: p > 0 & p <> 1 by INT_2:def 4;
D9: ff.x1 = In (p |^ n1, NAT) by C0
.= p |^ n1;
ff.x2 = In (p |^ n2, NAT) by C0
.= p |^ n2; then
p to_power n1 = p to_power n2 by DD,D9;
hence thesis by DA,POWER:50;
end; then
ff is one-to-one by FUNCT_1:def 4; then
card dom f = card rng f by CARD_1:70; then
card {p|^l where l is Element of NAT : l <= k} =
card {l where l is Element of NAT : l <= k} by ZZ,Z1,Z2;
hence thesis by B1,B2,CardSucc;
end;
definition
func Divs -> sequence of NAT means :DivsDef:
for n being Element of NAT holds it.n = #divs n;
existence
proof
deffunc Mer(Element of NAT) = In ( #divs $1, NAT);
ex f being sequence of NAT st
for x being Element of NAT holds f.x = Mer(x)
from FUNCT_2:sch 4; then
consider f being sequence of NAT such that
A1: for x being Element of NAT holds f.x = Mer(x);
take f;
let x be Element of NAT;
f.x = Mer(x) by A1
.= #divs x;
hence thesis;
end;
uniqueness
proof
A1: for f1, f2 be sequence of NAT st
(for x being Element of NAT holds f1.x = #divs x) &
(for x being Element of NAT holds f2.x = #divs x) holds
f1 = f2 from BINOP_2:sch 1;
let f1, f2 be sequence of NAT;
assume
(for k being Element of NAT holds f1.k = #divs k)&
for k being Element of NAT holds f2.k = #divs k;
hence thesis by A1;
end;
end;
theorem DivsMulti:
for m,n being non zero Nat st m,n are_coprime holds
#divs (m*n) = ( #divs m ) * #divs n
proof
let m,n be non zero Nat;
assume
AA: m,n are_coprime;
set f = EXP 0;
set X = NatDivisors m;
D4: f is multiplicative by NAT_5:35;
XX: n in NAT & m in NAT & m * n in NAT by ORDINAL1:def 12;
for n0 being non zero Nat holds Divs.n0 = Sum (f|NatDivisors n0)
proof
let n0 be non zero Nat;
n0 in NAT by ORDINAL1:def 12; then
Divs.n0 = #divs n0 by DivsDef
.= Sum (f|NatDivisors n0) by NAT_5:def 2;
hence thesis;
end; then
Divs is multiplicative by D4,NAT_5:34; then
F1: Divs.(n * m) = Divs.n * Divs.m by AA,NAT_5:def 5;
Divs.(n * m) = #divs (m*n) & Divs.n = #divs n &
Divs.m = #divs m by XX,DivsDef;
hence thesis by F1;
end;
theorem ::: see DivsMulti
for m,n being non zero Nat st m,n are_coprime holds
card NatDivisors (m * n) =
(card NatDivisors m) * (card NatDivisors n)
proof
let m,n be non zero Nat;
assume m,n are_coprime; then
A1: #divs (m*n) = ( #divs m ) * #divs n by DivsMulti;
#divs (m*n) = card NatDivisors (m * n) &
#divs m = card NatDivisors m &
#divs n = card NatDivisors n by ThDivs;
hence thesis by A1;
end;
:::theorem ::: reg by JORDAN1D:1, move wherever
::: for k being non zero Nat holds 2 |^ k is even;
theorem Cosik1:
for k being Nat holds
#divs (2 |^ k) = k + 1
proof
let k be Nat;
2 is Prime by INT_2:28; then
card NatDivisors (2 |^ k) = k + 1 by CardNatDiv;
hence thesis by ThDivs;
end;
::: ChatGPT says that
::: n = p ^ {k - 1} * m, m = 1, 2, 3... will do the work , which is false as if m = 2, then we obtain
::: n = 2 ^ (k - 1) * 2 = 2 ^ k, which has k+1 divisors
::: n = 2 ^ {k - 1} * m, m = 1, 2, 3... will do the work
:: 53. Prove that for every positive integer k the set of all positive integers
:: n whose number of positive integer divisors is divisible by k contains an
:: infinite arithmetic progression.
theorem PreProb53: :::: Problem 53
for n being non zero Nat, k, t being Nat st
k >= 1 & n = (2 |^ k) * t + 2 |^ (k -' 1) holds
k divides card NatDivisors n
proof
let n be non zero Nat, k,t be Nat;
assume k >= 1; then
per cases by XXREAL_0:1;
suppose k = 1; then
k divides card NatDivisors n by NAT_D:6;
hence thesis;
end;
suppose
SY: k > 1; then
A0: k -' 1 + 1 = k by XREAL_1:235;
assume
n = (2 |^ k) * t + 2 |^ (k -' 1); then
A3: n = (((2 |^ (k-'1)) * 2) * t + 2 |^ (k -' 1)) by A0,NEWTON:6
.= (2 |^ (k -' 1)) * (2 * t + 1);
A2: 2 |^ (k -' 1), 2 * t + 1 are_coprime by NAT_5:3;
PP: #divs n = card NatDivisors n by ThDivs;
P0: #divs (2 |^ (k -' 1)) = k by A0,Cosik1;
#divs n = ( #divs (2 * t + 1)) * #divs (2 |^ (k -' 1))
by A2,A3,DivsMulti;
hence thesis by PP,P0;
end;
end;
definition let k be Nat;
func Sierp53Seq k -> sequence of REAL equals
ArProg (2 |^ (k -' 1), 2 |^ k);
:: it.t = (2 |^ k) * t + 2 |^ (k -' 1);
coherence;
end;
::: Maybe we get the set X of all n's such that
::: k divides card NatDivisors n
::: and then intersect X with rng Sierp53Seq, which is a subset of X
registration let k be positive Nat, t be Nat;
cluster (Sierp53Seq k).t -> non zero natural;
coherence
proof
T1: (Sierp53Seq k).t <> 0
proof
assume (Sierp53Seq k).t = 0; then
(2 |^ k) * t + 2 |^ (k -' 1) = 0 by NUMBER06:7;
hence thesis;
end;
(2 |^ k) * t + 2 |^ (k -' 1) in NAT; then
ArProg (2 |^ (k -' 1), 2 |^ k).t in NAT by NUMBER06:7;
hence thesis by T1;
end;
end;
theorem
for k being positive Nat,
t being Nat holds
k divides card NatDivisors ((Sierp53Seq k).t)
proof
let k be positive Nat, t be Nat;
A2: (ArProg (2 |^ (k -' 1), 2 |^ k)).t =
2 |^ (k -' 1) + (2 |^ k) * t by NUMBER06:7;
A1: k >= 0 + 1 by NAT_1:13;
reconsider n = (2 |^ k) * t + 2 |^ (k -' 1) as non zero Nat;
k divides card NatDivisors n by A1,PreProb53;
hence thesis by A2;
end;
begin :: Problem 61
theorem
for s being Nat
ex f being fAP-like increasing positive-yielding FinSequence of NAT
st len f = s & for i being Nat st 1 <= i <= len f holds f.i is non prime
proof
let s be Nat;
consider f being fAP-like increasing positive-yielding FinSequence of NAT
such that
A1: len f = s & for i being Nat st 1 <= i <= len f holds f.i is perfect_power
by NUMBER15:51;
take f;
thus len f = s by A1;
let i be Nat;
assume 1 <= i <= len f;
hence thesis by A1;
end;
begin :: Problem 81
:: Find three triangular numbers with prime indices, which form
:: an increasing arithmetic progression
theorem
ex p, q, r being Prime st
Triangle p, Triangle q, Triangle r form_an_AP
proof
reconsider p = 127 as Prime by XPRIMES1:127;
reconsider q = 3697 as Prime by XPRIMES1:3697;
reconsider r = 5227 as Prime by XPRIMES1:5227;
take p, q, r;
T1: Triangle 127 = 127 * (127+1) / 2 by NUMPOLY1:19
.= 8128;
T2: Triangle 3697 = 3697 * (3697+1) / 2 by NUMPOLY1:19
.= 6835753;
Triangle 5227 = 5227 * (5227+1) / 2 by NUMPOLY1:19
.= 13663378; then
Triangle 5227 - Triangle 3697 = Triangle 3697 - Triangle 127
by T1,T2;
hence thesis by NUMBER06:def 9;
end;
theorem
for p, q, r being Prime st p = 127 & q = 3697 & r = 5227 holds
:: q * (q + 1) - p * (p + 1) = r * (r + 1) - q * (q + 1)
p * (p+1), q * (q+1), r * (r+1) form_an_AP
proof
let p, q, r be Prime;
assume
A1: p = 127 & q = 3697 & r = 5227; then
A3: q * (q + 1) = 13671506;
T1: Triangle 127 = 127 * (127+1) / 2 by NUMPOLY1:19
.= 8128;
T2: Triangle 3697 = 3697 * (3697+1) / 2 by NUMPOLY1:19
.= 6835753;
q * (q + 1) - p * (p + 1) = r * (r + 1) - q * (q + 1) by A1;
hence thesis by NUMBER06:def 9;
end;
begin :: Problem 90
theorem
for m being Nat st m >= 1 holds
Mersenne m is Prime implies
card PrimeDivisors Mersenne m = 1 &
card PrimeDivisors (Mersenne m + 1) = 1
proof
let m be Nat;
A0: 2 is Prime by INT_2:28;
assume
A1: m >= 1;
assume
ZZ: Mersenne m is Prime;
Mersenne m + 1 = 2 |^ m - 1 + 1 by GR_CY_3:def 3
.= 2 |^ m; then
PrimeDivisors (Mersenne m + 1) = {2} by A0,A1,NUMBER12:50; then
T1: card PrimeDivisors (Mersenne m + 1) = 1 by CARD_2:42;
PrimeDivisors (Mersenne m) =
PrimeDivisors ((Mersenne m) |^ 1)
.= {Mersenne m} by ZZ,NUMBER12:50;
hence thesis by T1,CARD_2:42;
end;
theorem
for m being Nat st m >= 1 holds
Fermat m is Prime implies
card PrimeDivisors Fermat m = 1 &
card PrimeDivisors (Fermat m - 1) = 1
proof
let m be Nat;
A0: 2 is Prime by INT_2:28;
assume m >= 1; then
2 |^ m >= 2 |^ 1 by PREPOWER:93; then
A2: 2 |^ m >= 1 by XXREAL_0:2;
assume
ZZ: Fermat m is Prime;
Fermat m = 2 |^ (2 |^ m) + 1 by PEPIN:def 3; then
PrimeDivisors (Fermat m - 1) = {2} by A0,A2,NUMBER12:50; then
T1: card PrimeDivisors (Fermat m - 1) = 1 by CARD_2:42;
PrimeDivisors Fermat m =
PrimeDivisors ((Fermat m) |^ 1)
.= {Fermat m} by ZZ,NUMBER12:50;
hence thesis by T1,CARD_2:42;
end;
begin :: Problem 90
:: 90. Prove that the theorem asserting that there exist only finitely many
:: positive integers n such that both n and n + 1 have only one prime divisor
:: is equivalent to the theorem asserting that there exist only finitely many
:: prime Mersenne numbers and finitely many prime Fermat numbers.
definition
func Mersenne_Primes -> Subset of NAT equals
{ n where n is Prime : n is mersenne };
coherence
proof
{ n where n is Prime : n is mersenne } c= NAT
proof
let x be object;
assume x in { n where n is Prime : n is mersenne }; then
consider n being Prime such that
A1: n = x & n is mersenne;
thus thesis by A1,ORDINAL1:def 12;
end;
hence thesis;
end;
end;
definition let n be Nat;
attr n is fermat means :FerDef:
ex k being Nat st n = Fermat k;
end;
definition
func Fermat_Primes -> Subset of NAT equals
{ n where n is Prime : n is fermat };
coherence
proof
{ n where n is Prime : n is fermat } c= NAT
proof
let x be object;
assume x in { n where n is Prime : n is fermat }; then
consider n being Prime such that
A1: n = x & n is fermat;
thus thesis by A1;
end;
hence thesis;
end;
end;
theorem MersenneDivisors:
for n being mersenne Prime holds
card PrimeDivisors n = 1 &
card PrimeDivisors (n+1) = 1
proof
let n be mersenne Prime;
consider k being Nat such that
A1: n = Mersenne k by NUMPOLY1:def 12;
A3: k >= 1
proof
assume k < 1; then
k = 0 by NAT_1:14;
hence thesis by A1,GR_CY_3:16;
end;
A2: Mersenne k = 2 |^ k - 1 by GR_CY_3:def 3;
A4: n + 1 = 2 |^ k by A1,A2;
2 is Prime by INT_2:28; then
PrimeDivisors (2 |^ k) = { 2 } by A3,NUMBER12:50; then
T1: card PrimeDivisors (n+1) = 1 by A4,CARD_2:42;
PrimeDivisors (n) = PrimeDivisors (n |^ 1)
.= { n } by NUMBER12:50;
hence thesis by T1,CARD_2:42;
end;
registration
cluster fermat for Prime;
existence
proof
Fermat 0 = 3 by PEPIN:50; then
3 is fermat & 3 is Prime by XPRIMES1:3;
hence thesis;
end;
end;
theorem FermatDivisors:
for n being fermat Prime holds
card PrimeDivisors n = 1 &
card PrimeDivisors (n-1) = 1
proof
let n be fermat Prime;
consider k being Nat such that
A1: n = Fermat k by FerDef;
A2: Fermat k = 2 |^ (2 |^ k) + 1 by PEPIN:def 3;
2 |^ k >= 2 |^ 0 by PREPOWER:93; then
A5: 2 |^ k >= 1 by NEWTON:4;
A4: n - 1 = 2 |^ (2 |^ k) by A1,A2;
2 is Prime by INT_2:28; then
PrimeDivisors (2 |^ (2 |^ k)) = { 2 } by A5,NUMBER12:50; then
T1: card PrimeDivisors (n-1) = 1 by A4,CARD_2:42;
PrimeDivisors (n) = PrimeDivisors (n |^ 1)
.= { n } by NUMBER12:50;
hence thesis by T1,CARD_2:42;
end;
theorem
Mersenne_Primes c= SetPrimes
proof
{ n where n is Prime : n is mersenne } c= SetPrimes
proof
let x be object;
assume x in { n where n is Prime : n is mersenne }; then
consider n being Prime such that
A1: n = x & n is mersenne;
thus thesis by A1,NEWTON:def 6;
end;
hence thesis;
end;
theorem
Fermat_Primes c= SetPrimes
proof
{ n where n is Prime : n is fermat } c= SetPrimes
proof
let x be object;
assume x in { n where n is Prime : n is fermat }; then
consider n being Prime such that
A1: n = x & n is fermat;
thus thesis by A1,NEWTON:def 6;
end;
hence thesis;
end;
registration
cluster mersenne -> natural for set;
coherence
proof
let x be set;
assume x is mersenne; then
consider n being Nat such that
A1: x = Mersenne n by NUMPOLY1:def 12;
thus thesis by A1;
end;
end;
::: Sierpinski Theorem 2 about Mersenne numbers, p. 335
theorem OddEven:
for m be odd Nat, k be Nat
st m divides 2 |^ k holds
m = 1
proof
let m be odd Nat, k be Nat;
assume
A1: m divides 2 |^ k;
A2: 2 is Prime by INT_2:28;
assume m <> 1; then
m is non trivial by NAT_2:28; then
2 divides m by A1,A2,NEWTON03:47;
hence thesis;
end;
registration
cluster INT-valued for FinSequence of REAL;
existence
proof
set f = <*>INT;
rng f c= REAL; then
f is FinSequence of REAL by FINSEQ_1:def 4;
hence thesis;
end;
end;
theorem OddSum:
for F being INT-valued FinSequence of REAL st
len F is odd &
for i being Nat st i in dom F holds
F.i is odd holds
Sum F is odd
proof
let F be INT-valued FinSequence of REAL;
assume
A1: len F is odd &
for i being Nat st i in dom F holds F.i is odd;
A2: Sum F, Sum (F mod 2) are_congruent_mod 2
by NUMBER04:10;
F mod 2 = (len F) |-> 1
proof
C1: dom (F mod 2) = dom F by EULER_2:def 1
.= dom ((len F) |-> 1) by FINSEQ_1:def 3;
for i being Nat st i in dom (F mod 2) holds
(F mod 2).i = ((len F) |-> 1).i
proof
let i be Nat;
assume i in dom (F mod 2); then
D2: i in dom F by EULER_2:def 1; then
D3: F.i is odd by A1;
(F mod 2).i = (F.i) mod 2 by D2,EULER_2:def 1
.= 1 by D3,NAT_2:22
.= ((dom F) --> 1).i by D2,FUNCOP_1:7
.= ((len F) |-> 1).i by FINSEQ_1:def 3;
hence thesis;
end;
hence thesis by C1,FINSEQ_1:13;
end; then
Sum (F mod 2) = (len F) * 1 by RVSUM_1:80
.= len F;
hence thesis by A2,A1;
end;
theorem MersenneTh:
for n, k, m being Nat st
n > 1 & m > 1 holds Mersenne n <> k |^ m
proof
let n, k, m be Nat;
set M = Mersenne n;
assume
Z0: n > 1 & m > 1;
assume
ZA: M = k |^ m;
WW: M = 2 |^ n - 1 by GR_CY_3:def 3; then
A2: k |^ m = 2 |^ n - 1 by ZA;
FO: k |^ m + 1 = 2 |^ n by ZA,WW;
2 |^ n >= 2 |^ 1 by PREPOWER:93,Z0; then
2 |^ n - 1 >= 2 |^ 1 - 1 by XREAL_1:9; then
OO: M >= 1 by WW;
O1: k <> 0
proof
assume k = 0; then
2 |^ n - 1 = 0 by A2,Z0,NEWTON:11;
hence thesis by WW,OO;
end;
F1: n > 1 by Z0; then
F2: n >= 1 + 1 by NAT_1:13;
2 |^ n >= 2 |^ 2 by F2,PREPOWER:93; then
2 |^ n >= 4 by POWER:60; then
2 |^ n - 1 >= 4 - 1 by XREAL_1:9; then
WA: M >= 3 by WW;
R1: k is odd
proof
assume k is even;
hence thesis by A2,Z0;
end;
VV: m is odd
proof
assume
G0: m is even;
k |^ m is odd by R1; then
k |^ m mod 8 = 1 by G0,NEWTON06:74; then
ex t being Nat st k |^ m = 8 * t + 1 & 1 < 8 by NAT_D:def 2;
then consider t being Nat such that
B1: k |^ m = 8 * t + 1;
BB: k |^ m + 1 = 2 * (4 * t + 1) by B1;
A3: k |^ m + 1 = 2 |^ n by A2;
n >= 1 + 1 by F1,NAT_1:13; then
n - 1 >= 1 + 1 - 1 by XREAL_1:9; then
A5: n -' 1 = n - 1 by NAT_D:39;
n >= 3
proof
assume n < 3; then
n < 2 + 1; then
n <= 2 by NAT_1:13; then
n = 0 or ... or n = 2; then
per cases;
suppose n = 0; then
M = 0 by GR_CY_3:16;
hence thesis by WA;
end;
suppose n = 1; then
M = 1 by GR_CY_3:17;
hence thesis by WA;
end;
suppose n = 2; then
Y1: M = 3 by GR_CY_3:18;
Y2: M = k |^ m by ZA; then
Y9: 3 = k |^ m by Y1;
Y8: m > 1 by Z0;
Y3: m >= 1 + 1 by Z0,NAT_1:13;
per cases;
suppose k <= 1; then
k < 1 + 1 by NAT_1:13; then
k = 0 or k = 1 by NAT_1:23;
hence thesis by Y9,Y8,NEWTON:11;
end;
suppose Y5: k > 1; then
Y7: k >= 1 + 1 by NAT_1:13;
Y6: k |^ m >= k |^ 2 by Y3,Y5,PREPOWER:93;
k to_power 2 >= 2 to_power 2 by Y7,PREPOWER:9; then
k |^ 2 >= 4 by POWER:60;
hence thesis by Y1,Y2,Y6,XXREAL_0:2;
end;
end;
end; then
n - 1 >= 3 - 1 by XREAL_1:9; then
a4: n -' 1 - 1 >= 2 - 1 by A5,XREAL_1:9;
n -' 2 + 1 = (n -' 1) -' 1 + 1 by NAT_D:45
.= n -' 1 by a4,NAT_D:43; then
U1: n -' 1 = n -' 2 + 1;
n = n -' 1 + 1 by F1,XREAL_1:235; then
2 |^ n = 2 |^ (n -' 1) * 2 by NEWTON:6
.= (2 |^ (n -' 2)) * 2 * 2 by NEWTON:6,U1
.= 4 * 2 |^ (n -' 2); then
2 * 2 divides 2 * (4 * t + 1) by A3,BB; then
T2: 2 divides 4 * t + 1 by GROUP_22:1;
2 * 2 * t is even;
hence thesis by T2;
end;
ZE: k <> 1
proof
assume k = 1;
hence thesis by WW,WA,A2;
end;
U1: k > 0 & k <> 1 by O1,ZE;
consider i being Nat such that
J1: m = 2 * i + 1 by VV,ABIAN:9;
k + 1 divides k|^(2*i+1) + 1|^(2*i+1) by NEWTON01:35; then
C1: k + 1 divides k |^ m + 1 by J1;
set R = (k |^ m + 1) div (k + 1);
FG: k |^ m + 1 = (k + 1) * R by C1; then
FZ: R divides 2 |^ n by FO;
set m1 = m -' 1;
m >= 1 + 1 by Z0,NAT_1:13; then
m - 1 >= 2 - 1 by XREAL_1:9; then
GT: m - 1 >= 1; then
CI: m = m1 + 1 by NAT_D:43;
CP: m -' 1 = m - 1 by GT,XREAL_0:def 2;
m is odd by VV; then
CL: (-1) |^ (m1+1) = -1 by CP;
k|^(m1+1) - (-1) |^(m1+1) = (k-(-1))* Sum ((k,-1) Subnomial m1)
by NEWTON04:51; then
k|^(m1+1) - (-1) |^(m1+1) = (k+1) * Sum ((k,-1) Subnomial m1); then
k|^m + 1 = (k+1) * Sum ((k,-1) Subnomial m1) by CL,CI; then
FD: (k + 1) * R = (k+1) * Sum ((k,-1) Subnomial m1);
HU: R = Sum ((k,-1) Subnomial m1) by FD,XCMPLX_1:5;
HJ: len ((k,-1) Subnomial m1) = m by CI,NEWTON04:def 2; then
D2: len ((k,-1) Subnomial m1) is odd by VV;
set SS = (k,-1) Subnomial m1;
SE: for i,l,j being Nat st i in dom SS & j = i - 1 & l = m1-j holds
SS.i = k|^l * (-1) |^j by NEWTON04:def 2;
D1: for i being Nat st i in dom SS holds SS.i is odd
proof
let i be Nat;
assume
UU: i in dom SS; then
1 <= i <= len SS by FINSEQ_3:25; then
UY: 1 <= i <= m by HJ; then
reconsider j = i - 1 as Nat;
i - 1 <= m - 1 by UY,XREAL_1:9; then
m1 - j >= j - j by CP,XREAL_1:9; then
reconsider l = m1 - j as Nat by INT_1:3;
DS: SS.i = k |^ l * (-1) |^ j by UU,SE;
0 is even; then
0 - 1 is odd;
hence thesis by DS,R1;
end;
R is odd by D1,D2,HU,OddSum; then
R = 1 by FZ,OddEven; then
2 |^ n = k + 1 by FG,FO; then
k to_power m = k to_power 1 by A2;
hence thesis by Z0,U1,POWER:50;
end;
MerLemma:
for n being Nat st Mersenne n = 1 holds
n = 1
proof
let n be Nat;
assume
A1: Mersenne n = 1;
Mersenne n = 2|^n - 1 by GR_CY_3:def 3; then
2 to_power n = 2 to_power 1 by A1;
hence thesis by POWER:50;
end;
Lemma3Prime:
for p being Prime, l being Nat st
p |^ l = 3 holds p = 3
proof
let p be Prime, l be Nat;
AB: 3 is Prime by XPRIMES1:3;
AA: 3 is non trivial by NAT_2:28;
assume
p |^ l = 3; then
p divides 3 by AA,NEWTON03:47; then
p = 3 or p = 1 by AB,INT_2:def 4;
hence thesis by INT_2:def 4;
end;
theorem ZeroDiv1:
card PrimeDivisors 1 = 0
proof
PrimeDivisors 1 = {} by NUMBER12:51;
hence thesis;
end;
theorem Diff2A:
for k,l being Nat st 2 |^ k - 2 |^ l = 2 & k >= 2 & l >= 1 holds
k = 2 & l = 1
proof
let k,l be Nat;
assume
A0: 2 |^ k - 2 |^ l = 2;
assume
k >= 2; then
k - 1 >= 2 - 1 by XREAL_1:9; then
a1: k - 1 >= 1; then
k -' 1 + 1 = k by NAT_D:43; then
A1: 2 |^ (k -' 1) * 2 = 2 |^ k by NEWTON:6;
A5: k - 1 >= 0 by a1;
assume l >= 1; then
A3: l - 1 >= 0; then
l -' 1 = l - 1 by XREAL_0:def 2; then
l -' 1 + 1 = l; then
2 |^ (l -' 1) * 2 = 2 |^ l by NEWTON:6; then
2 |^ (k -' 1) = 2 |^ (l -' 1) + 1 by A0,A1; then
per cases;
suppose
2 |^ (k -' 1) is even & 2 |^ (l -' 1) is odd; then
k -' 1 is non empty & l -' 1 is zero; then
l - 1 = 0 by A3,XREAL_0:def 2; then
A4: l = 1;
2 |^ k = 2 + 2 |^ l by A0
.= 4 by A4; then
2 to_power k = 2 to_power 2 by POWER:60;
hence thesis by A4,POWER:50;
end;
suppose
2 |^ (k -' 1) is odd & 2 |^ (l -' 1) is even; then
k -' 1 is zero & l -' 1 is non empty; then
k - 1 = 0 by A5,XREAL_0:def 2; then
A4: k = 1;
2 |^ l = 2 |^ k - 2 by A0
.= 0 by A4;
hence thesis;
end;
end;
theorem Fermat3:
3 is fermat Prime
proof
3 is fermat by PEPIN:50;
hence thesis by XPRIMES1:3;
end;
theorem Mersenne3:
3 is mersenne Prime
proof
Mersenne 2 = 3 by GR_CY_3:18; then
3 is mersenne by NUMPOLY1:def 12;
hence thesis by XPRIMES1:3;
end;
registration
cluster odd natural for Integer;
existence
proof
take 1;
2 * 0 + 1 is odd;
hence thesis;
end;
end;
theorem PrimeSet0:
PrimeDivisors 0 = SetPrimes
proof
thus PrimeDivisors 0 c= SetPrimes
proof
let x be object;
assume x in PrimeDivisors 0; then
consider k being Prime such that
A1: x = k & k divides 0;
thus thesis by A1,NEWTON:def 6;
end;
let p be object;
assume p in SetPrimes; then
reconsider pp = p as Prime by NEWTON:def 6;
pp divides 0 by NAT_D:6;
hence thesis;
end;
registration
cluster card SetPrimes -> non zero;
coherence;
end;
theorem DivEqualOne:
for n being odd natural Integer, k being Nat st
n divides 2 |^ k holds n = 1
proof
let n be odd natural Integer, k be Nat;
assume
A0: n divides 2 |^ k;
assume
AA: n <> 1;
per cases;
suppose n >= 0;
A3: n in NAT by INT_1:3;
2 is Prime by XPRIMES1:2; then
consider r be Nat such that
A4: n = 2 |^ r & r <= k by A0,A3,GROUPP_1:2;
r = 0 by A4;
hence thesis by AA,A4,NEWTON:4;
end;
suppose
n < 0;
hence thesis;
end;
end;
theorem
for a, b being Nat st a divides b holds
PrimeDivisors a c= PrimeDivisors b
proof
let a, b be Nat;
assume
A1: a divides b;
let x be object;
assume x in PrimeDivisors a; then
consider q being Prime such that
A3: x = q & q divides a;
q divides b by A1,A3,NAT_D:4;
hence thesis by A3;
end;
theorem OnlyOddPrimeX:
for m,n being Nat st PrimeDivisors n = {m} holds
m |-count n >= 1 & n = m |^ (m |-count n)
proof
let m, n be Nat such that
a1: PrimeDivisors n = {m};
a2: m in {m} by TARSKI:def 1;
then consider P being Prime such that
a3: P = m & P divides n by a1;
set k = m |-count n;
k >= 0+1 by a1,a3,PrimeSet0,MOEBIUS1:6,NAT_1:13;
hence k >= 1;
reconsider n as non zero Nat by a1,PrimeSet0;
a4: support pfexp n = PrimeDivisors n by NUMBER14:48;
consider f being FinSequence of COMPLEX such that
a5: Product ppf n = Product f and
a6: f = (ppf n)*canFS(support ppf n) by NAT_3:def 5;
a7: support ppf n c= dom ppf n by PRE_POLY:37;
a8: support ppf n = support pfexp n by NAT_3:def 9; then
f = (ppf n)*canFS{m} by a1,a6,NUMBER14:48
.= (ppf n)*<*m*> by FINSEQ_1:94
.= <*(ppf n).m*> by a1,a2,a4,a7,a8,FINSEQ_2:34
.= <*m|^k*> by a1,a2,a4,NAT_3:def 9;
hence thesis by a5,NAT_3:61;
end;
theorem
for n being even Nat st
card PrimeDivisors n = 1 holds
ex k being Nat st k >= 1 & n = 2 |^ k
proof
let n be even Nat;
assume card PrimeDivisors n = 1; then
consider x being object such that
A2: PrimeDivisors n = {x} by CARD_2:42;
x in PrimeDivisors n by A2,TARSKI:def 1; then
consider p being Prime such that
A3: x = p & p divides n;
Z1: PrimeDivisors n = {p} by A2,A3;
set k = p |-count n;
set a = p |^ k;
n <> 0
proof
assume n = 0;
hence thesis by Z1,PrimeSet0;
end; then
reconsider nn = n as non zero Nat;
consider s,t being Nat such that
C1: t is odd & s > 0 & nn = 2 |^ s * t by NAT_5:2;
II: 2 is Prime by XPRIMES1:2;
C2: 2 divides 2 |^ s by C1,NAT_3:3;
2 |^ s divides nn by C1; then
2 divides nn by C2,NAT_D:4; then
2 in PrimeDivisors n by II; then
G1: x = 2 by A2,TARSKI:def 1;
D4: t divides nn by C1;
per cases;
suppose
E1: t = 1;
IK: s >= 0 + 1 by C1,NAT_1:13;
t = 1 implies thesis
proof
assume t = 1;
hence thesis by IK,C1;
end;
hence thesis by E1;
end;
suppose t <> 1; then
consider q being Prime such that
D2: q divides t by MOEBIUS1:5;
consider m being Nat such that
D3: t = q * m by D2,NAT_D:def 3;
q divides nn by D2,D4,NAT_D:4; then
q in {2} by A2,G1; then
q = 2 * 1 by TARSKI:def 1;
hence thesis by C1,D3;
end;
end;
theorem OnlyPrimeDiv2:
for n being odd Nat st
card PrimeDivisors n = 1 holds
ex k being Nat,
p be Prime st n = p |^ k
proof
let n be odd Nat;
assume
card PrimeDivisors n = 1; then
consider x being object such that
A2: PrimeDivisors n = {x} by CARD_2:42;
x in PrimeDivisors n by A2,TARSKI:def 1; then
consider p being Prime such that
A3: x = p & p divides n;
set k = p |-count n;
k >= 1 & n = p |^ k by A2,A3,OnlyOddPrimeX;
hence thesis;
end;
theorem OnlyPrimeDiv:
for n being even Nat st
card PrimeDivisors n = 1 holds
ex k being Nat st n = 2 |^ k
proof
let n be even Nat;
assume
A0: card PrimeDivisors n = 1;
n <> 0
proof
assume n = 0;
hence thesis by A0,PrimeSet0;
end; then
consider j,i being Nat such that
c1: i is odd & j > 0 & n = 2 |^ j * i by NAT_5:2;
A9: 2 is Prime by XPRIMES1:2;
2 divides n by ABIAN:def 1; then
A8: 2 in PrimeDivisors n by A9;
consider x being object such that
A2: PrimeDivisors n = {x} by A0,CARD_2:42;
x in PrimeDivisors n by A2,TARSKI:def 1; then
consider k being Prime such that
A3: x = k & k divides n;
per cases by c1,A3,NAT_6:7;
suppose k divides 2 |^ j; then
k = 2 by A9,NAT_3:6; then
S1: PrimeDivisors n = {2} by A2,A3;
S2: i divides n by c1;
EE: i = 1 implies thesis
proof
assume i = 1;
hence thesis by c1;
end;
per cases;
suppose i is Prime; then
i in PrimeDivisors n by S2; then
i = 2 * 1 by S1,TARSKI:def 1;
hence thesis by c1;
end;
suppose not i is Prime & i <> 1; then
consider p being Prime such that
D2: p divides i & p <> i by MOEBIUS1:4;
p divides n by D2,S2,NAT_D:4; then
p in { k where k is Prime : k divides n }; then
2 divides i by S1,D2,TARSKI:def 1;
hence thesis by c1;
end;
suppose not i is Prime & i = 1;
hence thesis by EE;
end;
end;
suppose
S1: k divides i;
E3: i divides n by c1;
E4: i is odd & k is Prime by c1;
E2: i <> 1
proof
assume i = 1; then
k = 1 by S1,WSIERP_1:15;
hence thesis by INT_2:def 4;
end;
not i is Prime
proof
assume i is Prime; then
i in PrimeDivisors n by E3; then
i = k by A2,A3,TARSKI:def 1; then
E5: k is odd by E4;
set l = k |-count n;
l >= 1 & n = k |^ l by A3,A2,OnlyOddPrimeX;
hence thesis by E5;
end; then
consider p being Prime such that
D2: p divides i & p <> i by E2,MOEBIUS1:4;
d4: p is odd by D2,E4;
d3: k = 2 * 1 by A2,A8,A3,TARSKI:def 1;
p divides n by D2,E3,NAT_D:4; then
p in { k where k is Prime : k divides n };
hence thesis by A2,A3,d3,d4,TARSKI:def 1;
end;
end;
theorem :: see JORDAN1D and PEPIN
for a, n being Nat st n > 1 holds
a |^ n + 1 is odd iff a is even
proof
let a, n be Nat;
assume
A1: n > 1;
thus a |^ n + 1 is odd implies a is even;
assume a is even;
hence thesis by A1;
end;
theorem FunnyLemma:
for a, n being Nat st
a > 1 & n > 1 & a |^ n + 1 is Prime holds
n is even
proof
let a, n be Nat;
assume
A0: a > 1 & n > 1 & a |^ n + 1 is Prime;
assume
A2: n is odd;
set n1 = n -' 1;
set aa = - a;
set bb = 1;
n >= 1 + 1 by A0,NAT_1:13; then
n - 1 >= 2 - 1 by XREAL_1:9; then
A1: n = n1 + 1 by NAT_D:43;
B2: aa |^ n = - a |^ n by A2,POWER:2;
aa |^ n - bb |^ n =
(aa - bb) * Sum ((aa,bb) Subnomial n1) by A1,NEWTON04:51; then
(a |^ n + 1) =
(a + 1) * Sum ((aa,bb) Subnomial n1) by B2; then
V1: a + 1 divides a |^ n + 1; ::: see NUMBER04:13
V3: a > 0 by A0; then
V2: a + 1 <> 1;
V4: a <> 1 by A0;
a + 1 <> a |^ n + 1
proof
assume a + 1 = a |^ n + 1; then
a to_power 1 = a to_power n; then
1 = n by V3,V4,POWER:50;
hence thesis by A0;
end; then
a |^ n + 1 is not Prime by V1,V2,INT_2:def 4;
hence thesis by A0;
end;
theorem Curious:
for a, n being Nat st
a > 1 & n > 1 & a |^ n + 1 is Prime holds
a is even & ex k being non zero Nat st
n = 2 |^ k
proof
let a, n be Nat;
assume
A0: a > 1 & n > 1 & a |^ n + 1 is Prime;
FinalLemma:
n is even implies ex s being Nat st n = 2 |^ s
proof
assume n is even; then
consider s,t being Nat such that
C1: t is odd & s > 0 & n = 2 |^ s * t by A0,NAT_5:2;
P1: t >= 1
proof
assume t < 1;
hence thesis by C1,NAT_1:14;
end;
VV: (a |^ (2 |^ s)) |^ t + 1 is Prime by A0,C1,NEWTON:9;
reconsider aaa = a |^ (2 |^ s) as Nat;
a to_power (2 |^ s) > a to_power 0 by A0,POWER:39; then
VB: aaa > 1 by NEWTON:4;
v2: t is odd by C1;
t < 1 + 1
proof
assume t >= 1 + 1; then
t > 1 by NAT_1:13; then
t is even by VV,VB,FunnyLemma;
hence thesis by v2;
end; then
t <= 1 by NAT_1:13; then
t = 1 by P1,XXREAL_0:1;
hence thesis by C1;
end;
V4: a <> 1 by A0;
n is even
proof
assume
A2: n is odd;
set n1 = n -' 1;
set aa = - a;
set bb = 1;
n >= 1 + 1 by A0,NAT_1:13; then
n - 1 >= 2 - 1 by XREAL_1:9; then
A1: n -' 1 + 1 = n by NAT_D:43;
B2: aa |^ n = - a |^ n by A2,POWER:2;
aa |^ n - bb |^ n =
(aa - bb) * Sum ((aa,bb) Subnomial n1) by A1,NEWTON04:51; then
- (a |^ n + 1) =
- ((a + 1) * Sum ((aa,bb) Subnomial n1)) by B2; then
V1: a + 1 divides a |^ n + 1; ::: see NUMBER04:13
V3: a > 0 by A0; then
V2: a + 1 <> 1;
a + 1 <> a |^ n + 1
proof
assume a + 1 = a |^ n + 1; then
a to_power 1 = a to_power n; then
1 = n by V3,V4,POWER:50;
hence thesis by A0;
end; then
a |^ n + 1 is not Prime by V1,V2,INT_2:def 4;
hence thesis by A0;
end; then
consider s being Nat such that
D1: n = 2 |^ s by FinalLemma;
D2: s <> 0
proof
assume s = 0; then
n = 1 by D1,NEWTON:4;
hence thesis by A0;
end;
a is even
proof
assume
a is odd; then
a |^ n + 1 = 2 by A0,NUMBER06:2; then
a to_power n = a to_power 0 by NEWTON:4;
hence thesis by A0,POWER:50;
end;
hence thesis by D1,D2;
end;
registration let n be Nat;
cluster Mersenne n -> mersenne;
coherence by NUMPOLY1:def 12;
end;
registration let n be Nat;
cluster Fermat n -> fermat;
coherence;
end;
theorem Fer0:
card PrimeDivisors 0 = 1 & card PrimeDivisors (0 + 1) = 1
implies
0 is mersenne Prime or 0 + 1 is fermat Prime
proof
assume card PrimeDivisors 0 = 1 & card PrimeDivisors (0 + 1) = 1;
hence thesis by ZeroDiv1;
end;
theorem Fer1:
card PrimeDivisors 1 = 1 & card PrimeDivisors (1 + 1) = 1
implies
1 is mersenne Prime or 1 + 1 is fermat Prime
proof
assume
A1: card PrimeDivisors 1 = 1 & card PrimeDivisors (1 + 1) = 1;
card PrimeDivisors 1 = 0 by ZeroDiv1;
hence thesis by A1;
end;
theorem Fer2:
card PrimeDivisors 2 = 1 & card PrimeDivisors (2 + 1) = 1
implies
2 is mersenne Prime or 2 + 1 is fermat Prime
proof
3 is fermat Prime by XPRIMES1:3,PEPIN:50;
hence thesis;
end;
theorem Fer3:
card PrimeDivisors 3 = 1 & card PrimeDivisors (3 + 1) = 1
implies
3 is mersenne Prime or 3 + 1 is fermat Prime
proof
3 = Mersenne 2 by GR_CY_3:18;
hence thesis by XPRIMES1:3;
end;
theorem Fer4:
card PrimeDivisors 4 = 1 & card PrimeDivisors (4 + 1) = 1
implies
4 is mersenne Prime or 4 + 1 is fermat Prime
proof
5 = Fermat 1 by PEPIN:51;
hence thesis by XPRIMES1:5;
end;
Moshe1:
for p,q being Prime st p <> q holds
card PrimeDivisors (p * q) = 2
proof
let p,q be Prime;
assume
A1: p <> q;
PrimeDivisors (p * q) = PrimeDivisors (p |^ 1) \/ PrimeDivisors (q |^ 1)
by NUMBER12:48
.= PrimeDivisors (p |^ 1) \/ {q} by NUMBER12:50
.= {p} \/ {q} by NUMBER12:50
.= {p,q} by ENUMSET1:1;
hence thesis by A1,CARD_2:57;
end;
theorem Fer5:
card PrimeDivisors 5 = 1 & card PrimeDivisors (5 + 1) = 1
implies
5 is mersenne Prime or 5 + 1 is fermat Prime
proof
assume
A1: card PrimeDivisors 5 = 1 & card PrimeDivisors (5 + 1) = 1;
card PrimeDivisors (2 * 3) = 2 by XPRIMES1:2,3,Moshe1;
hence thesis by A1;
end;
theorem Fer6:
card PrimeDivisors 6 = 1 & card PrimeDivisors (6 + 1) = 1
implies
6 is mersenne Prime or 6 + 1 is fermat Prime
proof
assume
A1: card PrimeDivisors 6 = 1 & card PrimeDivisors (6 + 1) = 1;
card PrimeDivisors (2 * 3) = 2 by XPRIMES1:2,3,Moshe1;
hence thesis by A1;
end;
theorem Fer7:
card PrimeDivisors 7 = 1 & card PrimeDivisors (7 + 1) = 1
implies
7 is mersenne Prime or 7 + 1 is fermat Prime
proof
7 = Mersenne 3 by GR_CY_3:19;
hence thesis by XPRIMES1:7;
end;
::: by GR_CY_3:20
::: by PEPIN:52
theorem :::
not (card PrimeDivisors 8 = 1 & card PrimeDivisors (8 + 1) = 1
implies
8 is mersenne Prime or 8 + 1 is fermat Prime)
proof
A0: 2 is Prime by XPRIMES1:2;
A3: 3 is Prime by XPRIMES1:3;
A1: card PrimeDivisors 8 = card {2} by A0,NUMBER12:50,POWER:61
.= 1 by CARD_2:42;
A2: card PrimeDivisors (8 + 1) = card PrimeDivisors (3 * 3)
.= card PrimeDivisors (3 |^ 2) by NEWTON:81
.= card {3} by A3,NUMBER12:50
.= 1 by CARD_2:42;
2 divides 2 * 4; then
A4: not 8 is mersenne Prime by INT_2:def 4;
3 * 3 is not Prime;
hence thesis by A1,A2,A4;
end;
theorem
for n being Nat st n < 8 &
card PrimeDivisors n = 1 & card PrimeDivisors (n + 1) = 1
holds
n is mersenne Prime or n + 1 is fermat Prime
proof
let n be Nat;
assume n < 8; then
n < 7 + 1; then
n <= 7 by NAT_1:13; then
n = 0 or ... or n = 7; then
per cases;
suppose n = 0;
hence thesis by Fer0;
end;
suppose n = 1;
hence thesis by Fer1;
end;
suppose n = 2;
hence thesis by Fer2;
end;
suppose n = 3;
hence thesis by Fer3;
end;
suppose n = 4;
hence thesis by Fer4;
end;
suppose n = 5;
hence thesis by Fer5;
end;
suppose n = 6;
hence thesis by Fer6;
end;
suppose n = 7;
hence thesis by Fer7;
end;
end;
theorem InfiniteMersenne:
for n being Nat st n > 8 &
card PrimeDivisors n = 1 & card PrimeDivisors (n + 1) = 1
holds
n is mersenne Prime or n + 1 is fermat Prime
proof
let n be Nat;
assume
FF: n > 8;
assume
AA: card PrimeDivisors n = 1 & card PrimeDivisors (n + 1) = 1;
assume
CC: not n is mersenne Prime & not n + 1 is fermat Prime;
per cases;
suppose
E1: n is odd & n + 1 is even; then
consider m being Nat such that
R1: n + 1 = 2 |^ m by AA,OnlyPrimeDiv;
consider k being Nat, p being Prime such that
R2: n = p |^ k by E1,AA,OnlyPrimeDiv2;
ST: p |^ k = 2 |^ m - 1 by R1,R2;
RG: p > 0 & p <> 1 by INT_2:def 4;
HG: m > 1
proof
assume m <= 1; then
m < 1 + 1 by NAT_1:13; then
m = 0 or m = 1 by NAT_1:23; then
p |^ k = 1 - 1 or p |^ k = 2 |^ 1 - 1 by ST,NEWTON:4; then
p to_power k = p to_power 0 by NEWTON:4; then
k = 0 by RG,POWER:50;
hence thesis by AA,ZeroDiv1,R2,NEWTON:4;
end;
HH: p |^ k = Mersenne m by ST,GR_CY_3:def 3;
k <= 1 by HH,HG,MersenneTh; then
k < 1 + 1 by NAT_1:13; then
HA: k = 0 or k = 1 by NAT_1:23;
k <> 0
proof
assume k = 0; then
Mersenne m = 1 by HH,NEWTON:4;
hence thesis by HG,MerLemma;
end; then
S9: n is Prime by R2,HA;
n = 2 |^ m - 1 by R1; then
n = Mersenne m by GR_CY_3:def 3;
hence thesis by CC,S9;
end;
suppose
E1: n + 1 is odd & n is even; then
consider m being Nat such that
R1: n = 2 |^ m by AA,OnlyPrimeDiv;
R3: n + 1 is odd by E1; then
consider k being Nat, p being Prime such that
R2: n + 1 = p |^ k by AA,OnlyPrimeDiv2;
R4: k >= 1
proof
assume k < 1; then
k = 0 by NAT_1:14; then
n + 1 = 1 by R2,NEWTON:4; then
n = 0;
hence thesis by FF;
end;
XX: p is odd
proof
assume p is even; then
p = 2 by LAGRA4SQ:13;
hence thesis by R2,R3,R4;
end;
m <= 1 implies thesis
proof
assume m <= 1; then
m < 1 + 1 by NAT_1:13; then
m = 0 or m = 1 by NAT_1:23; then
n = 1 or n = 2 |^ 1 by R1,NEWTON:4;
hence thesis by FF;
end; then
UJ: m > 1;
SH: p |^ k = 2 |^ m + 1 by R2,R1;
SY: 2 |^ m = p |^ k - 1 by R2,R1;
k = 1 implies thesis
proof
assume
k = 1; then
E0: n + 1 = p by R2;
E1: not n + 1 is fermat Prime by CC;
E2: n = 2 |^ m by R1; then
e2: p = 2 |^ m + 1 by E0;
per cases by UJ;
suppose m < 1; then
n = 2 |^ 0 by E2,NAT_1:14
.= 1 by NEWTON:4;
hence thesis by FF;
end;
suppose m = 1; then
e3: p = 3 by e2;
3 is fermat Prime by Fermat3;
hence thesis by CC,e3,E0;
end;
suppose
fg: m > 1;
ff: p = 2 |^ m + 1 by e2;
consider k being non zero Nat such that
fz: m = 2 |^ k by ff,fg,Curious;
p = 2 |^ (2 |^ k) + 1 by fz,ff; then
p = Fermat k by PEPIN:def 3;
hence thesis by E0,E1;
end;
end; then
hc: k > 1 by R4,XXREAL_0:1; then
k >= 1 + 1 by NAT_1:13; then
k - 1 >= 2 - 1 by XREAL_1:9; then
X4: k -' 1 + 1 = k by NAT_D:43; then
p |^ k - 1 |^ k = (p - 1) * Sum ((p,1) Subnomial (k -' 1))
by NEWTON04:51;
then
KK: p |^ k - 1 = (p - 1) * Sum ((p,1) Subnomial (k -' 1)); then
X9: Sum ((p,1) Subnomial (k -' 1)) divides 2 |^ m by SY;
set SS = (p,1) Subnomial (k -' 1);
O1: p > 0 & p <> 1 by INT_2:def 4;
k is even
proof
assume
X1: k is odd;
X8: len SS = k by X4,NEWTON04:def 2; then
X2: len SS is odd by X1;
for i being Nat st i in dom SS holds SS.i is odd
proof
let i be Nat;
assume
X6: i in dom SS; then
X0: 1 <= i <= len SS by FINSEQ_3:25; then
reconsider m = i - 1 as Nat;
k - 1 >= 1 - 1 by hc,XREAL_1:9; then
S1: k -' 1 = k - 1 by XREAL_0:def 2;
i - 1 <= k - 1 by X0,X8,XREAL_1:9; then
(k -' 1) - m in NAT by S1,INT_1:5; then
reconsider l = (k -' 1) - m as Nat;
SS.i = p |^ l * 1 |^ m by X6,NEWTON04:def 2
.= p |^ l;
hence thesis by XX;
end; then
Sum SS is odd by X2,OddSum; then
Sum SS = 1 by X9,DivEqualOne; then
p to_power k = p to_power 1 by KK;
hence thesis by hc,O1,POWER:50;
end; then
consider l being Nat such that
h1: k = 2 * l by ABIAN:def 2;
(p |^ l - 1) * (p |^ l + 1) = (p |^ l) ^2 - 1 ^2
.= (p |^ l) |^ 2 - 1 by NEWTON:81
.= p |^ k - 1 by h1,NEWTON:9; then
h3: 2 |^ m = (p |^ l - 1) * (p |^ l + 1) by SH;
hh: 2 is Prime by INT_2:28;
hb: p > 1 & p > 0 by INT_2:def 4;
p |^ l <> 2
proof
assume
UK: p |^ l = 2;
UL: p <> 2
proof
assume p = 2;
hence thesis by UJ,hc,SH;
end;
UH: 2 divides p |^ l by UK;
2 is non trivial by NAT_2:28; then
p divides 2 by UH,NEWTON03:47; then
p = 1 or p = 2 by hh,INT_2:def 4;
hence thesis by UL,INT_2:def 4;
end; then
tt: p |^ l - 1 <> 1;
ts: l >= 1
proof
assume l < 1; then
l = 0 by NAT_1:14;
hence thesis by h1,R4;
end;
p >= 1 + 1 by hb,NAT_1:13; then
P9: p |^ l >= l + 1 by NEWTON:85;
1 <= 1 + l by NAT_1:12; then
1 <= p |^ l by XXREAL_0:2,P9; then
AA: p |^ l - 1 in NAT & 2 is Prime by INT_2:28,INT_1:5;
p |^ l - 1 divides 2 |^ m by h3; then
consider m1 be Nat such that
SY: p |^ l - 1 = 2 |^ m1 & m1 <= m by AA,GROUPP_1:2;
p |^ l + 1 divides 2 |^ m by h3; then
consider m2 be Nat such that
SZ: p |^ l + 1 = 2 |^ m2 & m2 <= m by AA,GROUPP_1:2;
y4: m1 >= 1
proof
assume m1 < 1; then
m1 = 0 by NAT_1:14; then
p |^ l - 1 = 1 by SY,NEWTON:4;
hence thesis by tt;
end;
cc: p > 0 & p <> 1 by INT_2:def 4;
y1: m2 >= 2
proof
assume m2 < 2; then
per cases by NAT_1:23;
suppose m2 = 0; then
p |^ l + 1 = 1 by SZ,NEWTON:4; then
p |^ l = 0;
hence thesis;
end;
suppose m2 = 1; then
p |^ l + 1 = 2 by SZ; then
p to_power l = p to_power 0 by NEWTON:4;
hence thesis by ts,cc,POWER:50;
end;
end;
2 |^ m2 - 2 |^ m1 = 2 by SY,SZ; then
m2 = 2 & m1 = 1 by y1,y4,Diff2A; then
p |^ l - 1 = 2 |^ 1 & p |^ l + 1 = 2 |^ 2 by SY,SZ; then
h4: p |^ l - 1 = 2 & p |^ l + 1 = 4; then
h5: p = 3 by Lemma3Prime;
2 |^ m = 2 |^ 3 by h3,h4,POWER:61; then
jj: 3 |^ k = 2 |^ 3 + 1 by SH,h5;
n + 1 = 3 |^ k by R2,h5; then
n = 8 by jj,POWER:61;
hence thesis by FF;
end;
end;
theorem
for p being Prime, k being Nat st k >= 1 holds
card PrimeDivisors (p |^ k) = 1
proof
let p be Prime,
k be Nat;
assume k >= 1; then
PrimeDivisors (p |^ k) = {p} by NUMBER12:50;
hence thesis by CARD_2:42;
end;
registration
cluster Mersenne_Primes -> non empty natural-membered;
coherence
proof
3 in Mersenne_Primes by Mersenne3;
hence thesis;
end;
end;
LemmaA: for a be mersenne Prime holds
a in Mersenne_Primes \/ Fermat_Primes
proof
let a be mersenne Prime;
a in Mersenne_Primes;
hence thesis by XBOOLE_0:def 3;
end;
LemmaB: for a be fermat Prime holds
a in Mersenne_Primes \/ Fermat_Primes
proof
let a be fermat Prime;
a in Fermat_Primes;
hence thesis by XBOOLE_0:def 3;
end;
theorem Problem90: ::: Problem 90
{ n where n is Nat :
n > 8 & card PrimeDivisors n = 1 & card PrimeDivisors (n+1) = 1 }
is infinite implies
Mersenne_Primes \/ Fermat_Primes is infinite
proof
set X =
{ n where n is Nat : n > 8 & card PrimeDivisors n = 1 &
card PrimeDivisors (n+1) = 1 };
assume
Z1: X is infinite;
set MFFP = Mersenne_Primes \/ Fermat_Primes;
assume
G1: MFFP is finite;
for m being Nat ex n being Nat st n >= m & n in MFFP
proof
let m be Nat;
ex c being Nat st c > m & c > 8 & c in X
proof
assume not ex c being Nat st c > m & c > 8 & c in X; then
Z3: for c being Nat holds c in X implies (c <= m or c <= 8);
X c= Seg m
proof
let x be object;
assume
Z4: x in X; then
consider nn being Nat such that
Z2: x = nn & nn > 8 & card PrimeDivisors nn = 1 &
card PrimeDivisors (nn+1) = 1;
nn <> 0
proof
assume nn = 0;
hence thesis by Z2;
end; then
Z5: 1 <= nn by NAT_1:14;
nn <= m by Z2,Z3,Z4;
hence thesis by Z2,Z5;
end;
hence thesis by Z1;
end; then
consider c being Nat such that
B1a: c > m & c > 8 & c in X;
B1: c > m & c > 8 & c in X by B1a;
consider mm being Nat such that
B3: mm = c &
mm > 8 & card PrimeDivisors mm = 1 &
card PrimeDivisors (mm + 1) = 1 by B1;
c is mersenne Prime or c + 1 is fermat Prime by B3,InfiniteMersenne; then
D2: c in MFFP or c + 1 in MFFP by LemmaA,LemmaB;
c + 1 > c by NAT_1:16; then
c > m & c + 1 > m by B1,XXREAL_0:2;
hence thesis by D2;
end;
hence thesis by G1,PYTHTRIP:9;
end;
theorem
Mersenne_Primes \/ Fermat_Primes is finite implies
{ n where n is Nat :
n > 8 & card PrimeDivisors n = 1 & card PrimeDivisors (n+1) = 1 }
is finite by Problem90;
LemmaMer:
for x being object st x in Mersenne_Primes holds
x is mersenne Prime
proof
let x be object;
assume x in Mersenne_Primes; then
consider n being Prime such that
A1: n = x & n is mersenne;
thus thesis by A1;
end;
LemmaFer:
for x being object st x in Fermat_Primes holds
x is fermat Prime
proof
let x be object;
assume x in Fermat_Primes; then
consider n being Prime such that
A1: n = x & n is fermat;
thus thesis by A1;
end;
theorem Infinite:
for X being infinite Subset of NAT holds
for a being Nat ex b being Nat st b > a & b in X
proof
let X be infinite Subset of NAT;
let a be Nat;
assume not ex b being Nat st b > a & b in X; then
P1: for b being Nat holds b in X implies b <= a;
X c= Seg a \/ {0}
proof
let x be object;
assume A1: x in X; then
reconsider xx = x as Nat;
P2: xx <= a by P1,A1;
0 = xx or 0 + 1 <= xx by NAT_1:14; then
xx in {0} or xx in Seg a by P2,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem :: Problem 90
{ n where n is Nat :
card PrimeDivisors n = 1 & card PrimeDivisors (n+1) = 1 }
is finite implies
Mersenne_Primes \/ Fermat_Primes is finite
proof
set X = { n where n is Nat :
card PrimeDivisors n = 1 & card PrimeDivisors (n+1) = 1 };
for x being object st x in X holds x is natural
proof
let x be object;
assume x in X; then
consider xx being Nat such that
B1: xx = x &
card PrimeDivisors xx = 1 & card PrimeDivisors (xx+1) = 1;
thus thesis by B1;
end; then
AA: X is natural-membered by MEMBERED:def 6;
assume X is finite; then
consider nn being Nat such that
AB: X c= Segm nn by AA,AFINSQ_2:2;
set Y = Mersenne_Primes \/ Fermat_Primes;
assume Y is infinite; then
consider c being Nat such that
F1: c > nn & c in Mersenne_Primes \/ Fermat_Primes by Infinite;
0 + 1 <= c by F1,NAT_1:13; then
GG: c - 1 in NAT by INT_1:5;
c in Mersenne_Primes or c in Fermat_Primes by XBOOLE_0:def 3,F1; then
per cases by LemmaMer,LemmaFer;
suppose c is mersenne Prime; then
card PrimeDivisors c = 1 &
card PrimeDivisors (c + 1) = 1 by MersenneDivisors; then
c in X; then
c in Segm nn by AB;
hence thesis by F1,NAT_1:44;
end;
suppose c is fermat Prime; then
G1: card PrimeDivisors c = 1 &
card PrimeDivisors (c - 1) = 1 by FermatDivisors;
c - 1 + 1 = c; then
c - 1 in X by GG,G1; then
c - 1 < nn by AB,NAT_1:44; then
c - 1 + 1 <= nn by NAT_1:13;
hence thesis by F1;
end;
end;
begin :: Problem 100
:: Subsequent composite numbers in Mersenne sequence
:: 100.
:: Prove that the infinite sequence 2^n-1 (n = 1, 2, ... )
:: contains arbitrarily long subsequences of consecutive terms
:: consisting of composite numbers.
:: maybe there exists a segment between two numbers that f | Seg (a,a+n) is
:: composite-membered / subsequence?
definition
func Mersenne_sequence -> sequence of NAT means :MerDef:
for n being Element of NAT holds
it.n = Mersenne n;
existence
proof
deffunc Mer(Element of NAT) = In (Mersenne $1, NAT);
ex f being sequence of NAT st
for x being Element of NAT holds f.x = Mer(x)
from FUNCT_2:sch 4; then
consider f being sequence of NAT such that
A1: for x being Element of NAT holds f.x = Mer(x);
take f;
let x be Element of NAT;
f.x = Mer(x) by A1
.= Mersenne x;
hence thesis;
end;
uniqueness
proof
A1: for f1, f2 be sequence of NAT st
(for x being Element of NAT holds f1.x = Mersenne(x)) &
(for x being Element of NAT holds f2.x = Mersenne(x)) holds
f1 = f2 from BINOP_2:sch 1;
let f1, f2 be sequence of NAT;
assume
(for k being Element of NAT holds f1.k = Mersenne(k))&
for k being Element of NAT holds f2.k = Mersenne(k);
hence thesis by A1;
end;
end;
theorem LemmaMersenne:
for m,k being Nat st m >= k >= 2 holds
2 |^ (m! + k) - 1 is not Prime
proof
let m,k be Nat;
assume
A0: m >= k >= 2;
2 |^ k > k by NEWTON:86; then
A1: 2 |^ k - 1 <> 1 by A0;
a2: 0 + k < m! + k by XREAL_1:8; then
2 |^ k divides 2 |^ (m! + k) by NEWTON:89; then
C1: 2 |^ k <= 2 |^ (m! + k) by NAT_D:7;
2 |^ k <> 2 |^ (m! + k)
proof
assume 2 |^ k = 2 |^ (m! + k);
hence thesis by a2,PEPIN:30;
end; then
2 |^ k < 2 |^ (m! + k) by C1,XXREAL_0:1; then
A2: 2 |^ k - 1 < 2 |^ (m!+k) - 1 by XREAL_1:14;
k divides m! by A0,NEWTON:41; then
k divides (m! + k) by NAT_D:8; then
2 |^ k - 1 divides (2 |^ (m!+k) - 1) by NUMBER05:19; then
2 |^ (m!+k) - 1 is not prime by A1,A2;
hence thesis;
end;
theorem
for m being Nat holds
rng (Mersenne_sequence | Seg (m! + 2, m! + m)) misses SetPrimes
proof
let m be Nat;
set f = Mersenne_sequence | Seg (m!+2,m!+m);
assume rng f meets SetPrimes; then
consider x being object such that
A2: x in rng f & x in SetPrimes by XBOOLE_0:3;
consider n being object such that
A3: n in dom f & x = f.n by A2,FUNCT_1:def 3;
A4: n in Seg (m!+2,m!+m) by A3,RELAT_1:57; then
n in {i where i is Nat: m!+2 <= i & i <= m!+m} by SGRAPH1:def 1;
then
consider nn being Nat such that
A5: n = nn & m!+2 <= nn & nn <= m! + m;
consider k being Nat such that
C1: m! + 2 + k = nn by A5,NAT_1:10;
E1: m! + (2 + k) <= m! + m by C1,A5;
set l = k + 2;
A6: nn = m! + l by C1;
2 <= l by NAT_1:11; then
A7: 2 <= l <= m by E1,XREAL_1:6;
AA: n in NAT by A5,ORDINAL1:def 12;
BA: Mersenne nn = 2 |^ nn - 1 by GR_CY_3:def 3;
x = Mersenne_sequence.n by A3,A4,FUNCT_1:49
.= Mersenne nn by AA,A5,MerDef; then
x is not Prime by BA,A7,A6,LemmaMersenne;
hence thesis by A2,NEWTON:def 6;
end;
begin :: Problem 156
theorem ::: Problem 156, m = 1
not ex x,y,z being positive Nat st
x |^ 3 + y |^ 3 + z |^ 3 = x * y * z
proof
assume ex x,y,z being positive Nat st
x |^ 3 + y |^ 3 + z |^ 3 = x * y * z; then
consider x,y,z being positive Nat such that
A1: x |^ 3 + y |^ 3 + z |^ 3 = x * y * z;
set X = x ^2 * y;
set Y = y ^2 * z;
set Z = z ^2 * x;
A2: X / Y = (x * x * y) / (y * z * y)
.= (x * x) / (y * z) by XCMPLX_1:91
.= (x * x * x) / (y * z * x) by XCMPLX_1:91
.= (x |^ 3) / (x * y * z) by Lm1;
A3: Y / Z = (y * y * z) / (z * x * z)
.= (y * y) / (z * x) by XCMPLX_1:91
.= (y * y * y) / (z * x * y) by XCMPLX_1:91
.= (y |^ 3) / (x * y * z) by Lm1;
A4: Z / X = (z * z * x) / (x * y * x)
.= (z * z) / (x * y) by XCMPLX_1:91
.= (z * z * z) / (x * y * z) by XCMPLX_1:91
.= (z |^ 3) / (x * y * z) by Lm1;
(x |^ 3) / (x * y * z) + (y |^ 3) / (x * y * z) + (z |^ 3) / (x * y * z)
= (x |^ 3 + y |^ 3 + z |^ 3) / (x * y * z)
.= 1 by A1,XCMPLX_1:60;
hence thesis by A2,A3,A4,NUMBER12:59;
end;
theorem ::: Problem 156, m = 2
not ex x,y,z being positive Nat st
x |^ 3 + y |^ 3 + z |^ 3 = 2 * x * y * z
proof
assume ex x,y,z being positive Nat st
x |^ 3 + y |^ 3 + z |^ 3 = 2 * x * y * z; then
consider x,y,z being positive Nat such that
A1: x |^ 3 + y |^ 3 + z |^ 3 = 2 * x * y * z;
set X = x ^2 * y;
set Y = y ^2 * z;
set Z = z ^2 * x;
A2: X / Y = (x * x * y) / (y * z * y)
.= (x * x) / (y * z) by XCMPLX_1:91
.= (x * x * x) / (y * z * x) by XCMPLX_1:91
.= (x |^ 3) / (x * y * z) by Lm1;
A3: Y / Z = (y * y * z) / (z * x * z)
.= (y * y) / (z * x) by XCMPLX_1:91
.= (y * y * y) / (z * x * y) by XCMPLX_1:91
.= (y |^ 3) / (x * y * z) by Lm1;
A4: Z / X = (z * z * x) / (x * y * x)
.= (z * z) / (x * y) by XCMPLX_1:91
.= (z * z * z) / (x * y * z) by XCMPLX_1:91
.= (z |^ 3) / (x * y * z) by Lm1;
(x |^ 3) / (x * y * z) + (y |^ 3) / (x * y * z) + (z |^ 3) / (x * y * z)
= (x |^ 3 + y |^ 3 + z |^ 3) / (x * y * z)
.= (2 * x * y * z) / (x * y * z) by A1
.= 2 * ((x * y * z) / (x * y * z))
.= 2 * 1 by XCMPLX_1:60
.= 2;
hence thesis by A2,A3,A4,NUMBER12:62;
end;
theorem ::: Problem 156, m = 3
for x,y,z being positive Nat st
x |^ 3 + y |^ 3 + z |^ 3 = 3 * x * y * z holds
x = y & y = z
proof
let x,y,z be positive Nat;
assume
A1: x |^ 3 + y |^ 3 + z |^ 3 = 3 * x * y * z;
set X = x ^2 * y;
set Y = y ^2 * z;
set Z = z ^2 * x;
A2: X / Y = (x * x * y) / (y * z * y)
.= (x * x) / (y * z) by XCMPLX_1:91
.= (x * x * x) / (y * z * x) by XCMPLX_1:91
.= (x |^ 3) / (x * y * z) by Lm1;
A3: Y / Z = (y * y * z) / (z * x * z)
.= (y * y) / (z * x) by XCMPLX_1:91
.= (y * y * y) / (z * x * y) by XCMPLX_1:91
.= (y |^ 3) / (x * y * z) by Lm1;
A4: Z / X = (z * z * x) / (x * y * x)
.= (z * z) / (x * y) by XCMPLX_1:91
.= (z * z * z) / (x * y * z) by XCMPLX_1:91
.= (z |^ 3) / (x * y * z) by Lm1;
(x |^ 3) / (x * y * z) + (y |^ 3) / (x * y * z) + (z |^ 3) / (x * y * z)
= (x |^ 3 + y |^ 3 + z |^ 3) / (x * y * z)
.= (3 * x * y * z) / (x * y * z) by A1
.= 3 * ((x * y * z) / (x * y * z))
.= 3 * 1 by XCMPLX_1:60
.= 3; then
X / Y + Y / Z + Z / X = 3 by A2,A3,A4; then
C0: X = Y & Y = Z by NUMBER12:63;
set n = x ^2 * y;
X * Y * Z = n * n * n by C0; then
(x * y * z) * (x * y * z) * (x * y * z) = n * n * n; then
(x * y * z) |^ 3 = n * n * n by Lm1; then
(x * y * z) |^ 3 = n |^ 3 by Lm1; then
D1: x * y * z = n by NEWTON03:12;
z / x = (z * (x * y)) / (x * (x * y)) by XCMPLX_1:91
.= 1 by D1,XCMPLX_1:60; then
T1: z = x by XCMPLX_1:58;
x / y = (x * (y * z)) / (y * (y * z)) by XCMPLX_1:91
.= 1 by C0,D1,XCMPLX_1:60;
hence thesis by T1,XCMPLX_1:58;
end;
begin :: Needed for Problem 167
theorem SierpTh16: :: Sierpinski Th. 16, p. 28
for a,b being non zero Nat st a, b are_coprime holds
ex u,v being Nat st a * u - b * v = 1
proof
let a,b be non zero Nat;
assume a, b are_coprime; then
A1: a gcd b = 1;
ex c,d be Nat st a gcd b = a * c - b * d by WSIERP_1:31;
hence thesis by A1;
end;
theorem Cosik1:
for a,b being Real st a - b > 1 holds
ex t being Integer st a > t > b
proof
let a,b be Real;
reconsider t = [\ a /] as Integer;
assume
A1: a - b > 1; then
a - b + b > 1 + b by XREAL_1:6; then
A2: a > 1 + b;
A3: t <= a by INT_1:def 6;
per cases;
suppose
t <> a; then
S1: t < a by A3,XXREAL_0:1;
take t;
S3: a - 1 < t by INT_1:def 6;
a - b + b > 1 + b by A1,XREAL_1:6; then
a - 1 > 1 + b - 1 by XREAL_1:6; then
b < t by S3,XXREAL_0:2;
hence thesis by S1;
end;
suppose
S0: t = a;
take t - 1;
a - 1 < a - 0 by XREAL_1:15; then
S1: t - 1 < a by S0;
a - 1 > 1 + b - 1 by A2,XREAL_1:8;
hence thesis by S1,S0;
end;
end;
theorem SierpCorr2: :: Sierpinski, Corollary 2, p. 29
for a, b being non zero Nat st a, b are_coprime holds
for n being Nat st n > a * b holds
ex x,y being non zero Nat st n = a * x + b * y
proof
let a, b be non zero Nat;
assume
A1: a, b are_coprime;
let n be Nat;
assume
A3: n > a * b;
consider u, v being Nat such that
A2: a * u - b * v = 1 by A1,SierpTh16;
A5: n = n * (a * u - b * v) by A2
.= a * n * u - b * n * v; then
(a * b) / (a * b) < (a * n * u - b * n * v) / (a * b)
by A3,XREAL_1:74; then
1 < (a * n * u) / (a * b) - (b * n * v) / (a * b) by XCMPLX_1:60; then
1 < ((n * u) * a) / a / b - (b * n * v) / (a * b) by XCMPLX_1:78; then
1 < (n * u) / b - (b * n * v) / (a * b) by XCMPLX_1:89; then
1 < (n * u) / b - ((n * v) * b) / b / a by XCMPLX_1:78; then
1 < (n * u) / b - (n * v) / a by XCMPLX_1:89; then
consider t being Integer such that
B1: (n * u) / b > t > (n * v) / a by Cosik1;
set x = n * u - b * t;
set y = a * t - n * v;
(n * u) / b * b > t * b by B1,XREAL_1:68; then
n * u > t * b + 0 by XCMPLX_1:87; then
T1: x > 0 by XREAL_1:20;
t * a > (n * v) / a * a by B1,XREAL_1:68; then
t * a > n * v + 0 by XCMPLX_1:87; then
T2: y > 0 by XREAL_1:20;
a * x + b * y = n by A5;
hence thesis by T1,T2;
end;
:: Sierpinski, Corollary 3, p. 29
:: for a being non zero Nat,
:: m, n being non zero Nat holds
:: (a |^ m - 1) gcd (a |^ n - 1) = a |^ (m gcd n) - 1
:: by NUMBER03:26;
theorem CoprimeProof:
for m being non zero Nat holds
2 |^ m - 1, (2 |^ m - 1) |^ m - 1 are_coprime
proof
let m be non zero Nat;
1 <= m by NAT_1:14; then
(2 |^ m - 1) |^ 1 divides (2 |^ m - 1) |^ m by NEWTON03:16;
hence thesis by NUMBER07:6;
end;
::: for all sufficiently large
theorem Lemma167A:
for m, n being non zero Nat st
n > (2 |^ m - 1) * ((2 |^ m - 1) |^ m - 1) holds
:::: improve the limit?
ex k,l being non zero Nat st
n = :::2 |^ m +
(2 |^ m - 1) * k + ((2 |^ m - 1) |^ m - 1) * l
proof
let m, n be non zero Nat;
assume
A1: n > (2 |^ m - 1) * ((2 |^ m - 1) |^ m - 1);
reconsider a = 2 |^ m - 1 as non zero Nat;
0 + 1 <= m by NAT_1:13; then
per cases by XXREAL_0:1;
suppose
O1: m = 1;
set k = n, l = 1;
(2 |^ m - 1) * k + ((2 |^ m - 1) |^ m - 1) * l =
k by O1;
hence thesis;
end;
suppose m > 1; then
2 to_power m > 2 to_power 1 by POWER:39; then
2 to_power m - 1 > 2 - 1 by XREAL_1:6; then
A0: 2 |^ m - 1 > 1;
(2 |^ m - 1) to_power 0 < (2 |^ m - 1) to_power m by A0,POWER:39; then
reconsider b = (2 |^ m - 1) |^ m - 1 as non zero Nat by NEWTON:4;
a, b are_coprime by CoprimeProof; then
consider x,y being non zero Nat such that
A2: n = a * x + b * y by A1,SierpCorr2;
:: n = (2 |^ m - 1) * x + ((2 |^ m - 1) |^ m - 1) * y by A2
:: .= (2 |^ m) * x - (1 * x) + ((2 |^ m - 1) |^ m - 1) * y by XCMPLX_1:8
:: .= (2 |^ m) * x - x + ((2 |^ m - 1) |^ m - 1) * y by XCMPLX_1:8
:: .= (2 |^ m) * x - x + ((2 |^ m - 1) |^ m) * y - 1 * y by XCMPLX_1:8
:: .= (2 |^ m) * x - x + ((2 |^ m - 1) |^ m) * y - y by XCMPLX_1:8
:: .= (2 |^ m) + (2 |^ m) * (x - 1) - x + ((2 |^ m - 1) |^ m) * y - y by XCMPLX_1:8;
thus thesis by A2;
end;
end;
begin :: Problem 167
registration
let s be Nat;
cluster s-element positive-yielding natural-valued for FinSequence;
existence
proof
set f = s |-> 1;
len f = s; then
f is s-element by CARD_1:def 7;
hence thesis;
end;
end;
registration
let s be Nat;
let f be s-element natural-valued FinSequence;
cluster f | s -> s-element;
coherence
proof
s <= len f by CARD_1:def 7; then
len (f | s) = s by FINSEQ_1:59;
hence thesis by CARD_1:def 7;
end;
end;
registration
let s be Nat;
let f be s-element positive-yielding natural-valued FinSequence;
cluster (f | s)" -> s-element;
coherence
proof
dom ((f | s)") = dom (f | s) by VALUED_1:def 7; then
A1: len ((f | s)") = len (f | s) by FINSEQ_3:29;
s <= len f by CARD_1:def 7; then
len ((f | s)") = s by A1,FINSEQ_1:59;
hence thesis by CARD_1:def 7;
end;
end;
definition
let s,m be Nat;
let f be s-element positive-yielding natural-valued FinSequence;
attr f is m-solution_of_Sierp167 means
Sum (f" |^ m) = 1;
end;
theorem Expand0:
for s, m being Nat
for f being s-element positive-yielding natural-valued FinSequence st
s = 2 |^ m & f = s |-> 2 holds
f is m-solution_of_Sierp167
proof
let s, m be Nat;
let f be s-element positive-yielding natural-valued FinSequence;
assume
A1: s = 2 |^ m & f = s |-> 2;
set r = (2 |^ m)";
W3: dom f = Seg s by FINSEQ_1:89;
W2: dom ((f | s)") = Seg s by W3,VALUED_1:def 7;
len f = s by CARD_1:def 7; then
ST: f | s = f;
f0: len ((f | s)" |^ m) = len ((f | s)") by NAT_3:def 1; then
f1: dom ((f | s)" |^ m) = Seg s by W2,FINSEQ_3:29; then
F1: dom ((f | s)" |^ m) = dom (s |-> ((2 |^ m)"));
for x being object st x in dom ((f | s)" |^ m) holds
((f | s)" |^ m).x = (s |-> ((2 |^ m)")).x
proof
let x be object;
assume
H1: x in dom ((f | s)" |^ m); then
f2: x in dom ((f | s)") by f0,FINSEQ_3:29; then
reconsider i = x as Nat;
H2: i in Seg s by H1,f1;
CC: ((f | s)").i = ((f | s).i)" by f2,VALUED_1:def 7
.= 2" by A1,H2,FUNCOP_1:7;
((f | s)" |^ m).x = (1 / 2) to_power m by CC,H1,NAT_3:def 1
.= (1 to_power m) / (2 to_power m) by POWER:31
.= (s |-> ((2 |^ m)")).x by H2,FUNCOP_1:7;
hence thesis;
end; then
Z2: (f | s)" |^ m = s |-> ((2 |^ m)") by F1,FUNCT_1:2;
Sum(s |-> r) = s * r by RVSUM_1:80
.= 1 by A1,XCMPLX_0:def 7;
hence thesis by Z2,ST;
end;
definition let s,m,a be non zero Nat;
let f be s-element positive-yielding natural-valued FinSequence;
func Expand (f,m,a) -> (s + a |^ m - 1)-element natural-valued FinSequence
equals
(f | (s-'1)) ^ ((a |^ m) |-> (a * f.s));
coherence
proof
set g = (f | (s -'1)) ^ ((a |^ m) |-> (a * f.s));
0 + 1 <= s by NAT_1:13; then
AA: s -' 1 = s - 1 by XREAL_1:233;
A2: len f = s by CARD_1:def 7; then
s -' 1 <= len f by NAT_D:35; then
A4: len (f | (s -' 1)) = len f - 1 by AA,A2,FINSEQ_1:17;
len g =
len (f | (s -' 1)) + len ((a |^ m) |-> (a * f.s)) by FINSEQ_1:22
.= s + a |^ m - 1 by A2,A4;
hence thesis by CARD_1:def 7;
end;
end;
registration let n be non zero Nat;
let a be positive Real;
cluster n |-> a -> positive-yielding;
coherence
proof
set f = n |-> a;
for x being Real st x in rng f holds x > 0
proof
let x be Real;
assume
A1: x in rng f;
rng f c= {a} by FUNCOP_1:13;
hence thesis by A1,TARSKI:def 1;
end;
hence thesis by PARTFUN3:def 1;
end;
end;
registration let s, a be non zero Nat;
cluster s |-> a -> positive-yielding;
coherence;
end;
registration let s,m,a be non zero Nat;
let f be s-element positive-yielding natural-valued FinSequence;
cluster Expand (f,m,a) -> positive-yielding;
coherence
proof
A1: 1 <= s by NAT_1:14;
s <= len f by CARD_1:def 7; then
s in dom f by A1,FINSEQ_3:25; then
f.s in rng f by FUNCT_1:3; then
f.s is positive by PARTFUN3:def 1;
hence thesis;
end;
end;
theorem ConcatPower:
for f,g being real-valued FinSequence,
m being non zero Nat holds
(f ^ g) |^ m = f |^ m ^ g |^ m
proof
let f,g be real-valued FinSequence,
m be non zero Nat;
set ff = (f ^ g) |^ m;
set gg = f |^ m ^ g |^ m;
X1: len ff = len (f ^ g) by NAT_3:def 1; then
a1: dom ff = dom (f ^ g) by FINSEQ_3:29
.= Seg (len f + len g) by FINSEQ_1:def 7;
a2: len (f |^ m) = len f & len (g |^ m) = len g by NAT_3:def 1;
dom gg = Seg (len f + len g) by a2,FINSEQ_1:def 7; then
A1: dom ff = dom gg by a1;
for k being Nat st k in dom ff holds ff.k = gg.k
proof
let k be Nat;
len f = len (f |^ m) by NAT_3:def 1; then
X3: dom f = dom (f |^ m) by FINSEQ_3:29;
len g = len (g |^ m) by NAT_3:def 1; then
X4: dom g = dom (g |^ m) by FINSEQ_3:29;
assume
B1: k in dom ff; then
k in dom (f ^ g) by X1,FINSEQ_3:29; then
per cases by FINSEQ_1:25;
suppose X2: k in dom f;
ff.k = ((f ^ g).k) |^ m by B1,NAT_3:def 1
.= (f.k) |^ m by X2,FINSEQ_1:def 7
.= (f |^ m).k by X2,X3,NAT_3:def 1
.= gg.k by X3,X2,FINSEQ_1:def 7;
hence thesis;
end;
suppose ex n being Nat st n in dom g & k = len f + n; then
consider n being Nat such that
O2: n in dom g & k = len f + n;
X6: k = len (f |^ m) + n by O2,a2;
ff.k = ((f ^ g).k) |^ m by B1,NAT_3:def 1
.= (g.n) |^ m by O2,FINSEQ_1:def 7
.= (g |^ m).n by X4,O2,NAT_3:def 1
.= gg.k by X6,X4,O2,FINSEQ_1:def 7;
hence thesis;
end;
end;
hence thesis by A1,FINSEQ_1:13;
end;
theorem SinglePower:
for a being Real,
m being non zero Nat holds
<* a *> |^ m = <* a |^ m *>
proof
let a be Real,
m be non zero Nat;
set f = <* a *> |^ m, g = <* a |^ m *>;
len f = len <*a*> by NAT_3:def 1; then
A0: dom f = dom <*a*> by FINSEQ_3:29
.= Seg 1 by FINSEQ_1:38; then
A1: dom f = dom g by FINSEQ_1:38;
for k being Nat st k in dom f holds f.k = g.k
proof
let k be Nat;
assume
B1: k in dom f; then
B2: k = 1 by TARSKI:def 1,A0,FINSEQ_1:2;
f.k = (<*a*>.k) |^ m by B1,NAT_3:def 1
.= g.k by B2;
hence thesis;
end;
hence thesis by A1,FINSEQ_1:13;
end;
theorem
for s, m, a being non zero Nat,
f being positive-yielding s-element natural-valued FinSequence,
g being positive-yielding (s + a |^ m - 1)-element
natural-valued FinSequence
st g = Expand (f,m,a) holds
Sum (f" |^ m) = Sum (g" |^ m)
proof
let s, m, a be non zero Nat,
f be positive-yielding s-element natural-valued FinSequence,
g be positive-yielding (s + a |^ m - 1)-element
natural-valued FinSequence;
assume
CC: g = Expand (f,m,a);
p0: len f = s by CARD_1:def 7; then
AA: f | s = f;
set t = s -' 1;
set S = Sum ((f|s)" |^ m);
s -' 1 + 1 = s by NAT_1:14,XREAL_1:235; then
f = (f | t) ^ <*f.s*> by p0,RFINSEQ:7; then
f" = (f | t)" ^ <*f.s*>" by NUMBER15:60; then
f" |^ m = (((f | t)") |^ m) ^ ((<*f.s*>") |^ m) by ConcatPower; then
Sum (f" |^ m) = Sum (((f | t)") |^ m) + Sum ((<*f.s*>") |^ m)
by RVSUM_1:75; then
K1: Sum (((f | t)") |^ m) = S - Sum ((<*f.s*>") |^ m) by AA;
set h = (a |^ m) |-> (a * f.s);
HH: Sum ((h | (a |^ m))" |^ m) = (1 / (f.s)) |^ m
proof
len f = s by CARD_1:def 7; then
1 <= s <= len f by NAT_1:14; then
s in dom f by FINSEQ_3:25; then
f.s in rng f by FUNCT_1:3; then
f.s > 0 by PARTFUN3:def 1; then
S1: 1 / (a * (f.s)) > 0;
len ((h | (a |^ m))" |^ m) = len ((h | (a |^ m))") by NAT_3:def 1; then
P1: dom ((h | (a |^ m))" |^ m) = dom ((h | (a |^ m))") by FINSEQ_3:29
.= dom (h | (a |^ m)) by VALUED_1:def 7
.= Seg (a |^ m); then
J1: dom ((h | (a |^ m))" |^ m) = dom ((a |^ m) |-> ((1 / (a * (f.s))) |^ m));
for k being Nat st k in dom ((h | (a |^ m))" |^ m) holds
((h | (a |^ m))" |^ m).k = ((a |^ m) |-> ((1 / (a * (f.s))) |^ m)).k
proof
let k be Nat;
assume
P4: k in dom ((h | (a |^ m))" |^ m); then
P3: k in Seg (a |^ m) by P1;
len ((h | (a |^ m))" |^ m) = len ((h | (a |^ m))") by NAT_3:def 1; then
dom ((h | (a |^ m))" |^ m) = dom ((h | (a |^ m))") by FINSEQ_3:29; then
P5: k in dom ((h | (a |^ m))") by P4;
PP: (h.k)" = 1 / (a * (f.s)) by P3,FUNCOP_1:7;
((h | (a |^ m))" |^ m).k = ((h | (a |^ m))".k) |^ m by P4,NAT_3:def 1
.= (((h | (a |^ m)).k)" ) |^ m by P5,VALUED_1:def 7
.= ((a |^ m) |-> ((1 / (a * (f.s))) |^ m)).k by PP,P3,FUNCOP_1:7;
hence thesis;
end; then
(h | (a |^ m))" |^ m = (a |^ m) |-> ((1 / (a * (f.s))) |^ m)
by J1,FINSEQ_1:13; then
Sum ((h | (a |^ m))" |^ m)
= (a to_power m) * ((1 / (a * (f.s))) to_power m) by RVSUM_1:80
.= (a / (a * (f.s))) to_power m by S1,POWER:30
.= (a / a / (f.s)) to_power m by XCMPLX_1:78
.= (1 / (f.s)) to_power m by XCMPLX_1:60;
hence thesis;
end;
set ff = f | t;
set gg = (a |^ m) |-> (a * f.s);
((ff ^ gg)") |^ m = ((ff") ^ (gg")) |^ m by NUMBER15:60; then
SX: ((ff ^ gg)") |^ m = ((ff") |^ m) ^ ((gg") |^ m) by ConcatPower;
HJ: Sum (gg" |^ m) = (1 / (f.s)) |^ m by HH;
<*(f.s)"*> = <*(f.s)*>" by NUMBER15:63; then
<*(f.s)" |^ m*> = <*(f.s)*>" |^ m by SinglePower; then
HI: Sum (<*(f.s)*>" |^ m) = (1 / (f.s)) |^ m;
Sum (g" |^ m) = Sum ((ff") |^ m) + Sum (gg" |^ m)
by CC,SX,RVSUM_1:75
.= S by K1,HI,HJ;
hence thesis by AA;
end;
theorem Ble1:
for s, m, a being non zero Nat,
f being positive-yielding s-element natural-valued FinSequence st
f is m-solution_of_Sierp167 holds
Expand (f,m,a) is m-solution_of_Sierp167
proof
let s, m, a be non zero Nat,
f be positive-yielding s-element natural-valued FinSequence;
p0: len f = s by CARD_1:def 7;
set t = s -' 1;
assume
aa: f is m-solution_of_Sierp167;
s -' 1 + 1 = s by NAT_1:14,XREAL_1:235; then
f = (f | t) ^ <*f.s*> by p0,RFINSEQ:7; then
f" = (f | t)" ^ <*f.s*>" by NUMBER15:60; then
f" |^ m = (((f | t)") |^ m) ^ ((<*f.s*>") |^ m) by ConcatPower; then
Sum (f" |^ m) = Sum (((f | t)") |^ m) + Sum ((<*f.s*>") |^ m)
by RVSUM_1:75; then
K1: Sum (((f | t)") |^ m) = 1 - Sum ((<*f.s*>") |^ m) by aa;
set g = Expand (f,m,a);
set h = (a |^ m) |-> (a * f.s);
HH: Sum ((h | (a |^ m))" |^ m) = (1 / (f.s)) |^ m
proof
len f = s by CARD_1:def 7; then
1 <= s <= len f by NAT_1:14; then
s in dom f by FINSEQ_3:25; then
f.s in rng f by FUNCT_1:3; then
f.s > 0 by PARTFUN3:def 1; then
S1: 1 / (a * (f.s)) > 0;
len ((h | (a |^ m))" |^ m) = len ((h | (a |^ m))") by NAT_3:def 1; then
P1: dom ((h | (a |^ m))" |^ m) = dom ((h | (a |^ m))") by FINSEQ_3:29
.= dom (h | (a |^ m)) by VALUED_1:def 7
.= Seg (a |^ m); then
J1: dom ((h | (a |^ m))" |^ m) = dom ((a |^ m) |-> ((1 / (a * (f.s))) |^ m));
for k being Nat st k in dom ((h | (a |^ m))" |^ m) holds
((h | (a |^ m))" |^ m).k = ((a |^ m) |-> ((1 / (a * (f.s))) |^ m)).k
proof
let k be Nat;
assume
P4: k in dom ((h | (a |^ m))" |^ m); then
P3: k in Seg (a |^ m) by P1;
len ((h | (a |^ m))" |^ m) = len ((h | (a |^ m))") by NAT_3:def 1; then
dom ((h | (a |^ m))" |^ m) = dom ((h | (a |^ m))") by FINSEQ_3:29; then
P5: k in dom ((h | (a |^ m))") by P4;
PP: (h.k)" = 1 / (a * (f.s)) by P3,FUNCOP_1:7;
((h | (a |^ m))" |^ m).k = ((h | (a |^ m))".k) |^ m by P4,NAT_3:def 1
.= (((h | (a |^ m)).k)" ) |^ m by P5,VALUED_1:def 7
.= ((a |^ m) |-> ((1 / (a * (f.s))) |^ m)).k by PP,P3,FUNCOP_1:7;
hence thesis;
end; then
(h | (a |^ m))" |^ m = (a |^ m) |-> ((1 / (a * (f.s))) |^ m)
by J1,FINSEQ_1:13; then
Sum ((h | (a |^ m))" |^ m)
= (a to_power m) * ((1 / (a * (f.s))) to_power m) by RVSUM_1:80
.= (a / (a * (f.s))) to_power m by S1,POWER:30
.= (a / a / (f.s)) to_power m by XCMPLX_1:78
.= (1 / (f.s)) to_power m by XCMPLX_1:60;
hence thesis;
end;
set ff = f | t;
set gg = (a |^ m) |-> (a * f.s);
(ff ^ gg)" = (ff") ^ (gg") by NUMBER15:60; then
SX: ((ff ^ gg)") |^ m = ((ff") |^ m) ^ ((gg") |^ m) by ConcatPower;
HJ: Sum (gg" |^ m) = (1 / (f.s)) |^ m by HH;
<*(f.s)"*> = <*(f.s)*>" by NUMBER15:63; then
<*(f.s)" |^ m*> = <*(f.s)*>" |^ m by SinglePower; then
HI: Sum (<*(f.s)*>" |^ m) = (1 / (f.s)) |^ m;
Sum (g" |^ m) = Sum ((ff") |^ m) + Sum (gg" |^ m) by SX,RVSUM_1:75
.= 1 by K1,HI,HJ;
hence thesis;
end;
theorem Important167:
for m, s, k, l, a, b being non zero Nat st
(ex f being positive-yielding s-element natural-valued FinSequence st
f is m-solution_of_Sierp167) holds
(ex f being positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * l)-element
natural-valued FinSequence st
f is m-solution_of_Sierp167)
proof
let m, s, k, l, a, b be non zero Nat;
assume ex f being positive-yielding s-element natural-valued FinSequence st
f is m-solution_of_Sierp167; then
consider f being positive-yielding s-element natural-valued FinSequence
such that
B1: f is m-solution_of_Sierp167;
defpred P[non zero Nat] means
ex f being positive-yielding
(s + (a |^ m - 1) * $1)-element natural-valued FinSequence st
f is m-solution_of_Sierp167;
A1: P[1]
proof
reconsider g = Expand (f,m,a) as positive-yielding
(s + (a |^ m - 1) * 1)-element natural-valued FinSequence;
take g;
thus thesis by B1,Ble1;
end;
A2: for l being non zero Nat st P[l] holds P[l + 1]
proof
let l be non zero Nat;
assume P[l]; then
consider f being positive-yielding (s + (a |^ m - 1) * l)-element
natural-valued FinSequence such that
C1: f is m-solution_of_Sierp167;
reconsider g = Expand (f,m,a) as
positive-yielding (s + (a |^ m - 1) * (l + 1))-element
natural-valued FinSequence;
take g;
thus thesis by C1,Ble1;
end;
for n being non zero Nat holds P[n] from NAT_1:sch 10(A1,A2); then
consider f being positive-yielding
(s + (a |^ m - 1) * k)-element natural-valued FinSequence
such that
S1: f is m-solution_of_Sierp167;
defpred Q[non zero Nat] means
ex f being positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * $1)-element
natural-valued FinSequence st
f is m-solution_of_Sierp167;
A1: Q[1]
proof
reconsider g = Expand (f,m,b) as positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * 1)-element
natural-valued FinSequence;
take g;
g is m-solution_of_Sierp167 by S1,Ble1;
hence thesis;
end;
A2: for l being non zero Nat st Q[l] holds Q[l + 1]
proof
let l be non zero Nat;
assume Q[l]; then
consider f being positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * l)-element
natural-valued FinSequence such that
C1: f is m-solution_of_Sierp167;
reconsider g = Expand (f,m,b) as positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * (l + 1))-element
natural-valued FinSequence;
take g;
thus thesis by C1,Ble1;
end;
for n being non zero Nat holds Q[n] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
theorem
for m being non zero Nat
ex N being Nat st
for n being non zero Nat st n > N holds
ex f being positive-yielding n-element natural-valued FinSequence st
f is m-solution_of_Sierp167
proof
let m be non zero Nat;
reconsider s = 2 |^ m as non zero Nat;
set f = s |-> 2;
len f = s; then
reconsider f as s-element positive-yielding natural-valued
FinSequence by CARD_1:def 7;
A1: f is m-solution_of_Sierp167 by Expand0;
reconsider a = 2 as non zero Nat;
reconsider b = 2 |^ m - 1 as non zero Nat;
take N = (2 |^ m - 1) * ((2 |^ m - 1) |^ m - 1) + s;
let n be non zero Nat;
assume n > N; then
k1: n - s > (2 |^ m - 1) * ((2 |^ m - 1) |^ m - 1) + s - s by XREAL_1:8;
consider k,l being non zero Nat such that
A2: n - s = (2 |^ m - 1) * k + ((2 |^ m - 1) |^ m - 1) * l by k1,Lemma167A;
A4: n = (2 |^ m - 1) * k + ((2 |^ m - 1) |^ m - 1) * l + s by A2;
consider f being positive-yielding
(s + (a |^ m - 1) * k + (b |^ m - 1) * l)-element
natural-valued FinSequence
such that
A3: f is m-solution_of_Sierp167 by Important167,A1;
reconsider f as positive-yielding
n-element natural-valued FinSequence by A4;
f is m-solution_of_Sierp167 by A3;
hence thesis;
end;