:: Elementary Number Theory Problems. {P}art {XVIII}
:: by Adam Grabowski
::
:: Received December 21, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users

Lm1: for x being Nat holds x |^ 3 = (x * x) * x

proof end;

:: 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;

:: 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

func Bnumber_of_divisors n -> ManySortedSet of SetPrimes means :BDef: :: NUMBER18:def 1
( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
it . p = (p |-count n) + 1 ) );

existence
ex b₁ being ManySortedSet of SetPrimes st
( support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = (p |-count n) + 1 ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of SetPrimes st support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = (p |-count n) + 1 ) & support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = (p |-count n) + 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem BDef defines Bnumber_of_divisors NUMBER18:def 1 :
for n being Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = Bnumber_of_divisors n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = (p |-count n) + 1 ) ) );

registration

let n be non zero Nat;

cluster Bnumber_of_divisors n -> natural-valued finite-support ;

coherence
( Bnumber_of_divisors n is natural-valued & Bnumber_of_divisors n is finite-support )

proof end;

end;

definition

let n be non zero Nat;

func number_of_divisors n -> Nat equals :: NUMBER18:def 2
Product (Bnumber_of_divisors n);

coherence
Product (Bnumber_of_divisors n) is Nat ;

end;

:: deftheorem defines number_of_divisors NUMBER18:def 2 :
for n being non zero Nat holds number_of_divisors n = Product (Bnumber_of_divisors n);

theorem :: NUMBER18:1

for p being Prime holds (Bnumber_of_divisors p) * <*p*> = <*2*>

proof end;

theorem :: NUMBER18:2

Bnumber_of_divisors 1 = EmptyBag SetPrimes

proof end;

theorem Th48: :: NUMBER18:3

for p being Prime
for n being non zero Nat st p |-count n = 0 holds
(Bnumber_of_divisors n) . p = 0

proof end;

theorem Th49: :: NUMBER18:4

for n being non zero Nat
for p being Prime st p |-count n <> 0 holds
(Bnumber_of_divisors n) . p = (p |-count n) + 1

proof end;

theorem Th50: :: NUMBER18:5

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 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 :: NUMBER18:def 3
sigma (0,n);

coherence
sigma (0,n) is Nat ;

end;

:: deftheorem defines #divs NUMBER18:def 3 :
for n being Nat holds #divs n = sigma (0,n);

theorem ThEXP0: :: NUMBER18:6

EXP 0 = NAT --> 1

proof end;

theorem :: NUMBER18:7

EXP 1 = id NAT

proof end;

theorem :: NUMBER18:8

for n being Nat st n = 0 holds
#divs n = 0 by NAT_5:def 2;

ETRANS: for i being Nat
for r being Real holds Sum (i |-> r) = i * r
by RVSUM_1:80;

theorem LemmaCard: :: NUMBER18:9

for X being finite Subset of NAT holds Sum ((NAT --> 1) | X) = card X

proof end;

theorem :: NUMBER18:10

for p being Prime holds #divs p = 2

proof end;

theorem :: NUMBER18:11

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 end;

theorem ThDivs: :: NUMBER18:12

for n being non zero Nat holds #divs n = card (NatDivisors n)

proof end;

theorem CardSucc: :: NUMBER18:13

for k being Nat holds card (k \/ {k}) = k + 1

proof end;

theorem CardNatDiv: :: NUMBER18:14

for p being Prime
for k being Nat holds card (NatDivisors (p |^ k)) = k + 1

proof end;

definition

func Divs -> sequence of NAT means :DivsDef: :: NUMBER18:def 4
for n being Element of NAT holds it . n = #divs n;

existence
ex b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = #divs n

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = #divs n ) & ( for n being Element of NAT holds b₂ . n = #divs n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DivsDef defines Divs NUMBER18:def 4 :
for b₁ being sequence of NAT holds
( b₁ = Divs iff for n being Element of NAT holds b₁ . n = #divs n );

theorem DivsMulti: :: NUMBER18:15

for m, n being non zero Nat st m,n are_coprime holds
#divs (m * n) = (#divs m) * (#divs n)

proof end;

theorem :: NUMBER18:16

for m, n being non zero Nat st m,n are_coprime holds
card (NatDivisors (m * n)) = (card (NatDivisors m)) * (card (NatDivisors n))

proof end;

:::theorem ::: reg by JORDAN1D:1, move wherever
::: for k being non zero Nat holds 2 |^ k is even;

theorem Cosik1: :: NUMBER18:17

for k being Nat holds #divs (2 |^ k) = k + 1

proof 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: :: NUMBER18:18

for n being non zero Nat
for k, t being Nat st k >= 1 & n = ((2 |^ k) * t) + (2 |^ (k -' 1)) holds
k divides card (NatDivisors n)

proof end;

definition

let k be Nat;

func Sierp53Seq k -> sequence of REAL equals :: NUMBER18:def 5
ArProg ((2 |^ (k -' 1)),(2 |^ k));

coherence
ArProg ((2 |^ (k -' 1)),(2 |^ k)) is sequence of REAL ;

end;

:: deftheorem defines Sierp53Seq NUMBER18:def 5 :
for k being Nat holds Sierp53Seq k = ArProg ((2 |^ (k -' 1)),(2 |^ k));

::: 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;
let t be Nat;

cluster (Sierp53Seq k) . t -> natural non zero ;

coherence
( not (Sierp53Seq k) . t is zero & (Sierp53Seq k) . t is natural )

proof end;

end;

theorem :: NUMBER18:19

for k being positive Nat
for t being Nat holds k divides card (NatDivisors ((Sierp53Seq k) . t))

proof end;

theorem :: NUMBER18:20

for s being Nat ex f being increasing positive-yielding fAP-like FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
not f . i is prime ) )

proof end;

:: Find three triangular numbers with prime indices, which form
:: an increasing arithmetic progression

theorem :: NUMBER18:21

ex p, q, r being Prime st Triangle p, Triangle q, Triangle r form_an_AP

proof end;

theorem :: NUMBER18:22

for p, q, r being Prime st p = 127 & q = 3697 & r = 5227 holds
p * (p + 1),q * (q + 1),r * (r + 1) form_an_AP

proof end;

theorem :: NUMBER18:23

for m being Nat st m >= 1 & Mersenne m is Prime holds
( card (PrimeDivisors (Mersenne m)) = 1 & card (PrimeDivisors ((Mersenne m) + 1)) = 1 )

proof end;

theorem :: NUMBER18:24

for m being Nat st m >= 1 & Fermat m is Prime holds
( card (PrimeDivisors (Fermat m)) = 1 & card (PrimeDivisors ((Fermat m) - 1)) = 1 )

proof end;

:: 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 :: NUMBER18:def 6
{ n where n is Prime : n is mersenne } ;

coherence
{ n where n is Prime : n is mersenne } is Subset of NAT

proof end;

end;

:: deftheorem defines Mersenne_Primes NUMBER18:def 6 :
Mersenne_Primes = { n where n is Prime : n is mersenne } ;

definition

let n be Nat;

attr n is fermat means :FerDef: :: NUMBER18:def 7
ex k being Nat st n = Fermat k;

end;

:: deftheorem FerDef defines fermat NUMBER18:def 7 :
for n being Nat holds
( n is fermat iff ex k being Nat st n = Fermat k );

definition

func Fermat_Primes -> Subset of NAT equals :: NUMBER18:def 8
{ n where n is Prime : n is fermat } ;

coherence
{ n where n is Prime : n is fermat } is Subset of NAT

proof end;

end;

:: deftheorem defines Fermat_Primes NUMBER18:def 8 :
Fermat_Primes = { n where n is Prime : n is fermat } ;

theorem MersenneDivisors: :: NUMBER18:25

for n being mersenne Prime holds
( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 )

proof end;

registration

cluster non empty non trivial epsilon-transitive epsilon-connected ordinal natural non zero complex real integer dim-like prime finite cardinal square ext-real positive non negative non square-containing composite non perfect_power fermat for set ;

existence
ex b₁ being Prime st b₁ is fermat

proof end;

end;

theorem FermatDivisors: :: NUMBER18:26

for n being fermat Prime holds
( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n - 1)) = 1 )

proof end;

theorem :: NUMBER18:27

Mersenne_Primes c= SetPrimes

proof end;

theorem :: NUMBER18:28

Fermat_Primes c= SetPrimes

proof end;

registration

cluster mersenne -> natural for set ;

coherence
for b₁ being set st b₁ is mersenne holds
b₁ is natural

proof end;

end;

::: Sierpinski Theorem 2 about Mersenne numbers, p. 335

theorem OddEven: :: NUMBER18:29

for m being odd Nat
for k being Nat st m divides 2 |^ k holds
m = 1

proof end;

registration

cluster Relation-like omega -defined REAL -valued INT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support for FinSequence of REAL ;

existence
ex b₁ being FinSequence of REAL st b₁ is INT -valued

proof end;

end;

theorem OddSum: :: NUMBER18:30

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 end;

theorem MersenneTh: :: NUMBER18:31

for n, k, m being Nat st n > 1 & m > 1 holds
Mersenne n <> k |^ m

proof end;

MerLemma: for n being Nat st Mersenne n = 1 holds
n = 1

proof end;

Lemma3Prime: for p being Prime
for l being Nat st p |^ l = 3 holds
p = 3

proof end;

theorem ZeroDiv1: :: NUMBER18:32

card (PrimeDivisors 1) = 0

proof end;

theorem Diff2A: :: NUMBER18:33

for k, l being Nat st (2 |^ k) - (2 |^ l) = 2 & k >= 2 & l >= 1 holds
( k = 2 & l = 1 )

proof end;

theorem Fermat3: :: NUMBER18:34

3 is fermat Prime

proof end;

theorem Mersenne3: :: NUMBER18:35

3 is mersenne Prime

proof end;

registration

cluster natural complex real integer odd ext-real for object ;

existence
ex b₁ being Integer st
( b₁ is odd & b₁ is natural )

proof end;

end;

theorem PrimeSet0: :: NUMBER18:36

PrimeDivisors 0 = SetPrimes

proof end;

registration

cluster card SetPrimes -> non zero ;

coherence
not card SetPrimes is zero ;

end;

theorem DivEqualOne: :: NUMBER18:37

for n being natural odd Integer
for k being Nat st n divides 2 |^ k holds
n = 1

proof end;

theorem :: NUMBER18:38

for a, b being Nat st a divides b holds
PrimeDivisors a c= PrimeDivisors b

proof end;

theorem OnlyOddPrimeX: :: NUMBER18:39

for m, n being Nat st PrimeDivisors n = {m} holds
( m |-count n >= 1 & n = m |^ (m |-count n) )

proof end;

theorem :: NUMBER18:40

for n being even Nat st card (PrimeDivisors n) = 1 holds
ex k being Nat st
( k >= 1 & n = 2 |^ k )

proof end;

theorem OnlyPrimeDiv2: :: NUMBER18:41

for n being odd Nat st card (PrimeDivisors n) = 1 holds
ex k being Nat ex p being Prime st n = p |^ k

proof end;

theorem OnlyPrimeDiv: :: NUMBER18:42

for n being even Nat st card (PrimeDivisors n) = 1 holds
ex k being Nat st n = 2 |^ k

proof end;

theorem :: NUMBER18:43

for a, n being Nat st n > 1 holds
( (a |^ n) + 1 is odd iff a is even )

proof end;

theorem FunnyLemma: :: NUMBER18:44

for a, n being Nat st a > 1 & n > 1 & (a |^ n) + 1 is Prime holds
n is even

proof end;

theorem Curious: :: NUMBER18:45

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 end;

registration

let n be Nat;

cluster Mersenne n -> mersenne ;

coherence
Mersenne n is mersenne by NUMPOLY1:def 12;

end;

registration

let n be Nat;

cluster Fermat n -> fermat ;

coherence
Fermat n is fermat ;

end;

theorem Fer0: :: NUMBER18:46

( card (PrimeDivisors 0) = 1 & card (PrimeDivisors (0 + 1)) = 1 & 0 is not mersenne Prime implies 0 + 1 is fermat Prime )

proof end;

theorem Fer1: :: NUMBER18:47

( card (PrimeDivisors 1) = 1 & card (PrimeDivisors (1 + 1)) = 1 & 1 is not mersenne Prime implies 1 + 1 is fermat Prime )

proof end;

theorem Fer2: :: NUMBER18:48

( card (PrimeDivisors 2) = 1 & card (PrimeDivisors (2 + 1)) = 1 & 2 is not mersenne Prime implies 2 + 1 is fermat Prime )

proof end;

theorem Fer3: :: NUMBER18:49

( card (PrimeDivisors 3) = 1 & card (PrimeDivisors (3 + 1)) = 1 & 3 is not mersenne Prime implies 3 + 1 is fermat Prime )

proof end;

theorem Fer4: :: NUMBER18:50

( card (PrimeDivisors 4) = 1 & card (PrimeDivisors (4 + 1)) = 1 & 4 is not mersenne Prime implies 4 + 1 is fermat Prime )

proof end;

Moshe1: for p, q being Prime st p <> q holds
card (PrimeDivisors (p * q)) = 2

proof end;

theorem Fer5: :: NUMBER18:51

( card (PrimeDivisors 5) = 1 & card (PrimeDivisors (5 + 1)) = 1 & 5 is not mersenne Prime implies 5 + 1 is fermat Prime )

proof end;

theorem Fer6: :: NUMBER18:52

( card (PrimeDivisors 6) = 1 & card (PrimeDivisors (6 + 1)) = 1 & 6 is not mersenne Prime implies 6 + 1 is fermat Prime )

proof end;

theorem Fer7: :: NUMBER18:53

( card (PrimeDivisors 7) = 1 & card (PrimeDivisors (7 + 1)) = 1 & 7 is not mersenne Prime implies 7 + 1 is fermat Prime )

proof end;

::: by GR_CY_3:20
::: by PEPIN:52

theorem :: NUMBER18:54

( card (PrimeDivisors 8) = 1 & card (PrimeDivisors (8 + 1)) = 1 & 8 is not mersenne Prime & 8 + 1 is not fermat Prime )

proof end;

theorem :: NUMBER18:55

for n being Nat st n < 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 & n is not mersenne Prime holds
n + 1 is fermat Prime

proof end;

theorem InfiniteMersenne: :: NUMBER18:56

for n being Nat st n > 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 & n is not mersenne Prime holds
n + 1 is fermat Prime

proof end;

theorem :: NUMBER18:57

for p being Prime
for k being Nat st k >= 1 holds
card (PrimeDivisors (p |^ k)) = 1

proof end;

registration

cluster Mersenne_Primes -> non empty natural-membered ;

coherence
( not Mersenne_Primes is empty & Mersenne_Primes is natural-membered )

proof end;

end;

LemmaA: for a being mersenne Prime holds a in Mersenne_Primes \/ Fermat_Primes

proof end;

LemmaB: for a being fermat Prime holds a in Mersenne_Primes \/ Fermat_Primes

proof end;

theorem Problem90: :: NUMBER18:58

( { 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 end;

theorem :: NUMBER18:59

( 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 end;

LemmaFer: for x being object st x in Fermat_Primes holds
x is fermat Prime

proof end;

theorem Infinite: :: NUMBER18:60

for X being infinite Subset of NAT
for a being Nat ex b being Nat st
( b > a & b in X )

proof end;

theorem :: NUMBER18:61

( { n where n is Nat : ( card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 ) } is finite implies Mersenne_Primes \/ Fermat_Primes is finite )

proof end;

:: 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

:: 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?

func Mersenne_sequence -> sequence of NAT means :MerDef: :: NUMBER18:def 9
for n being Element of NAT holds it . n = Mersenne n;

existence
ex b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = Mersenne n

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Element of NAT holds b₁ . n = Mersenne n ) & ( for n being Element of NAT holds b₂ . n = Mersenne n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem MerDef defines Mersenne_sequence NUMBER18:def 9 :
for b₁ being sequence of NAT holds
( b₁ = Mersenne_sequence iff for n being Element of NAT holds b₁ . n = Mersenne n );

theorem LemmaMersenne: :: NUMBER18:62

for m, k being Nat st m >= k & k >= 2 holds
not (2 |^ ((m !) + k)) - 1 is Prime

proof end;

theorem :: NUMBER18:63

for m being Nat holds rng (Mersenne_sequence | (Seg (((m !) + 2),((m !) + m)))) misses SetPrimes

proof end;

theorem :: NUMBER18:64

for x, y, z being positive Nat holds not ((x |^ 3) + (y |^ 3)) + (z |^ 3) = (x * y) * z

proof end;

theorem :: NUMBER18:65

for x, y, z being positive Nat holds not ((x |^ 3) + (y |^ 3)) + (z |^ 3) = ((2 * x) * y) * z

proof end;

theorem :: NUMBER18:66

for x, y, z being positive Nat st ((x |^ 3) + (y |^ 3)) + (z |^ 3) = ((3 * x) * y) * z holds
( x = y & y = z )

proof end;

theorem SierpTh16: :: NUMBER18:67

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 end;

theorem Cosik1: :: NUMBER18:68

for a, b being Real st a - b > 1 holds
ex t being Integer st
( a > t & t > b )

proof end;

theorem SierpCorr2: :: NUMBER18:69

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 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: :: NUMBER18:70

for m being non zero Nat holds (2 |^ m) - 1,(((2 |^ m) - 1) |^ m) - 1 are_coprime

proof end;

::: for all sufficiently large

theorem Lemma167A: :: NUMBER18:71

for m, n being non zero Nat st n > ((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1) holds
ex k, l being non zero Nat st n = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)

proof end;

registration

let s be Nat;

cluster Relation-like omega -defined Function-like finite s -element FinSequence-like FinSubsequence-like natural-valued positive-yielding finite-support for set ;

existence
ex b₁ being FinSequence st
( b₁ is s -element & b₁ is positive-yielding & b₁ is natural-valued )

proof end;

end;

registration

let s be Nat;
let f be s -element natural-valued FinSequence;

cluster f | s -> s -element ;

coherence
f | s is s -element

proof end;

end;

registration

let s be Nat;
let f be s -element natural-valued positive-yielding FinSequence;

cluster (f | s) " -> s -element ;

coherence
(f | s) " is s -element

proof end;

end;

definition

let s, m be Nat;
let f be s -element natural-valued positive-yielding FinSequence;

attr f is m -solution_of_Sierp167 means :: NUMBER18:def 10
Sum ((f ") |^ m) = 1;

end;

:: deftheorem defines -solution_of_Sierp167 NUMBER18:def 10 :
for s, m being Nat
for f being b₁ -element natural-valued positive-yielding FinSequence holds
( f is m -solution_of_Sierp167 iff Sum ((f ") |^ m) = 1 );

theorem Expand0: :: NUMBER18:72

for s, m being Nat
for f being b₁ -element natural-valued positive-yielding FinSequence st s = 2 |^ m & f = s |-> 2 holds
f is m -solution_of_Sierp167

proof end;

definition

let s, m, a be non zero Nat;
let f be s -element natural-valued positive-yielding FinSequence;

func Expand (f,m,a) -> (s + (a |^ m)) - 1 -element natural-valued FinSequence equals :: NUMBER18:def 11
(f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s)));

coherence
(f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s))) is (s + (a |^ m)) - 1 -element natural-valued FinSequence

proof end;

end;

:: deftheorem defines Expand NUMBER18:def 11 :
for s, m, a being non zero Nat
for f being b₁ -element natural-valued positive-yielding FinSequence holds Expand (f,m,a) = (f | (s -' 1)) ^ ((a |^ m) |-> (a * (f . s)));

registration

let n be non zero Nat;
let a be positive Real;

cluster n |-> a -> positive-yielding ;

coherence
n |-> a is positive-yielding

proof end;

end;

registration

let s, a be non zero Nat;

cluster s |-> a -> positive-yielding ;

coherence
s |-> a is positive-yielding ;

end;

registration

let s, m, a be non zero Nat;
let f be s -element natural-valued positive-yielding FinSequence;

cluster Expand (f,m,a) -> (s + (a |^ m)) - 1 -element natural-valued positive-yielding ;

coherence
Expand (f,m,a) is positive-yielding

proof end;

end;

theorem ConcatPower: :: NUMBER18:73

for f, g being real-valued FinSequence
for m being non zero Nat holds (f ^ g) |^ m = (f |^ m) ^ (g |^ m)

proof end;

theorem SinglePower: :: NUMBER18:74

for a being Real
for m being non zero Nat holds <*a*> |^ m = <*(a |^ m)*>

proof end;

theorem :: NUMBER18:75

for s, m, a being non zero Nat
for f being b₁ -element natural-valued positive-yielding FinSequence
for g being (b₁ + (b₃ |^ b₂)) - 1 -element natural-valued positive-yielding FinSequence st g = Expand (f,m,a) holds
Sum ((f ") |^ m) = Sum ((g ") |^ m)

proof end;

theorem Ble1: :: NUMBER18:76

for s, m, a being non zero Nat
for f being b₁ -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 holds
Expand (f,m,a) is m -solution_of_Sierp167

proof end;

theorem Important167: :: NUMBER18:77

for m, s, k, l, a, b being non zero Nat st ex f being b₂ -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 holds
ex f being (b₂ + (((b₅ |^ b₁) - 1) * b₃)) + (((b₆ |^ b₁) - 1) * b₄) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167

proof end;

theorem :: NUMBER18:78

for m being non zero Nat ex N being Nat st
for n being non zero Nat st n > N holds
ex f being b₃ -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167

proof end;