:: Elementary Number Theory Problems. {P}art {XVI}
:: by Karol P\kak
::
:: Received December 14, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

theorem Th1: :: NUMBER16:1

for b being Nat
for f, g being XFinSequence of NAT holds value ((f ^ g),b) = (value (f,b)) + ((value (g,b)) * (b |^ (len f)))

proof end;

theorem Th2: :: NUMBER16:2

for b, n, k, x being Nat st b > 1 & n > 0 & n * (b |^ k) <= x & x < (n + 1) * (b |^ k) holds
digits (n,b) = (digits (x,b)) /^ k

proof end;

theorem Th3: :: NUMBER16:3

for a, b, d, s being Nat st b > 0 & d > 1 & s > 0 holds
ex m, i being Nat st (digits (((ArProg (a,b)) . m),d)) /^ i = digits (s,d)

proof end;

theorem :: NUMBER16:4

for a, b, s being Nat st b > 0 & s > 0 holds
ex m, i being Nat st (digits (((ArProg (a,b)) . m),10)) /^ i = digits (s,10) by Th3;

:: Construct an infinite set of relatively prime numbers
:: in a given arithmetic progression

theorem :: NUMBER16:5

for a, b being Nat st a > 0 & a,b are_coprime holds
ex N being infinite Subset of NAT st
for n, m being Nat st n in N & m in N & n <> m holds
(ArProg (b,a)) . n,(ArProg (b,a)) . m are_coprime

proof end;

:: Construction of an infinite set of numbers with exactly
:: the same prime divisors in a given arithmetic progression.

theorem :: NUMBER16:6

for a, b being Nat st a > 0 & b > 0 holds
ex N being infinite Subset of NAT st
for n, m being Nat
for p being Prime st n in N & m in N holds
( p divides (ArProg (b,a)) . n iff p divides (ArProg (b,a)) . m )

proof end;

:: Construct an arithmetic progression with the least difference
:: without fibonacci numbers.

theorem Th7: :: NUMBER16:7

( Fib 6 = 8 & Fib 7 = 13 & Fib 8 = 21 & Fib 9 = 34 & Fib 10 = 55 & Fib 11 = 89 & Fib 12 = 144 & Fib 13 = 233 & Fib 14 = 377 & Fib 15 = 610 & Fib 16 = 987 & Fib 17 = 1597 & Fib 18 = 2584 & Fib 19 = 4181 & Fib 20 = 6765 & Fib 21 = 10946 & Fib 22 = 17711 & Fib 23 = 28657 & Fib 24 = 46368 & Fib 25 = 75025 )

proof end;

theorem Th8: :: NUMBER16:8

for n being Nat holds Fib (n + 2) >= n

proof end;

theorem Th9: :: NUMBER16:9

for n, k being Nat st k < n & n <= 7 holds
ex i being Nat st (Fib i) mod n = k

proof end;

theorem Th10: :: NUMBER16:10

for j being Nat st 0 < j & j <= 7 holds
ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

proof end;

theorem Th11: :: NUMBER16:11

for n, i, j being Nat st Fib n, Fib (n + i) are_congruent_mod j & Fib (n + 1), Fib ((n + i) + 1) are_congruent_mod j holds
for x, y being Nat st x,y are_congruent_mod i holds
Fib x, Fib y are_congruent_mod j

proof end;

theorem Th12: :: NUMBER16:12

for i, j, k being Nat st 0 < j & k < i & ( for x, y being Nat st x,y are_congruent_mod j holds
Fib x, Fib y are_congruent_mod i ) & ( for x being Nat st x < j holds
(Fib x) mod i <> k ) holds
for m being Nat holds not (ArProg (k,i)) . m is Fibonacci

proof end;

theorem Th13: :: NUMBER16:13

( Fib 0, Fib 12 are_congruent_mod 8 & Fib 1, Fib (12 + 1) are_congruent_mod 8 & ( for x being Nat st x < 12 holds
( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 ) ) )

proof end;

theorem :: NUMBER16:14

( ( for i, j being Nat st 0 < i & i <= 7 holds
ex k being Nat st (ArProg (j,i)) . k is Fibonacci ) & ( for k being Nat holds not (ArProg (4,8)) . k is Fibonacci ) )

proof end;

:: Construct an arithmetic progression ak+b (k=0,1,2,...)
:: without Fibonacci numbers where a,b are coprime.

theorem :: NUMBER16:15

( 4,11 are_coprime & ( for m being Nat holds not (ArProg (4,11)) . m is Fibonacci ) )

proof end;

:: Find the largest prime number in the sequence 1, 31, 331, 3331, ...

theorem Th16: :: NUMBER16:16

for n being Nat holds value ((<%1%> ^ (n --> 3)),10) = ((10 |^ (n + 1)) - 7) / 3

proof end;

theorem Th17: :: NUMBER16:17

for n being Nat ex k being Nat st
( 17 divides k & k = ((10 |^ ((16 * n) + 9)) - 7) / 3 )

proof end;

theorem Th18: :: NUMBER16:18

33331 is prime

proof end;

theorem Th19: :: NUMBER16:19

333331 is prime

proof end;

Lm1: for n being Nat holds 17 <> ((10 |^ (n + 1)) - 7) / 3

proof end;

theorem :: NUMBER16:20

( ( for n being non zero Nat st n < 6 holds
value ((<%1%> ^ (n --> 3)),10) is prime ) & not value ((<%1%> ^ (8 --> 3)),10) is prime & { (value ((<%1%> ^ (n --> 3)),10)) where n is Nat : not value ((<%1%> ^ (n --> 3)),10) is prime } is infinite )

proof end;

theorem Th21: :: NUMBER16:21

for n being non zero Nat
for p being Prime st support (pfexp n) = {p} holds
n = p |^ ((pfexp n) . p)

proof end;

theorem Th22: :: NUMBER16:22

for n being non zero Nat holds
( ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 ) iff n is prime )

proof end;

theorem Th23: :: NUMBER16:23

for n being non zero Nat holds 0 in rng (pfexp n)

proof end;

theorem Th24: :: NUMBER16:24

for n, m being non zero Nat st n,m are_coprime holds
rng (pfexp (n * m)) = (rng (pfexp n)) \/ (rng (pfexp m))

proof end;

theorem Th25: :: NUMBER16:25

for n being Nat holds Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n)

proof end;

theorem Th26: :: NUMBER16:26

for k being Nat holds 2 |^ k <= Product (primesFinS k)

proof end;

theorem Th27: :: NUMBER16:27

for n being Nat st 2 <= n holds
ex k being non zero Nat st
( Product (primesFinS k) <= n & n < Product (primesFinS (k + 1)) )

proof end;

theorem Th28: :: NUMBER16:28

for p being Prime
for k being Nat holds
( ( p |-count (Product (primesFinS k)) = 1 implies primeindex p < k ) & ( primeindex p < k implies p |-count (Product (primesFinS k)) = 1 ) & ( p |-count (Product (primesFinS k)) = 0 implies primeindex p >= k ) & ( primeindex p >= k implies p |-count (Product (primesFinS k)) = 0 ) )

proof end;

theorem :: NUMBER16:29

for p being Prime
for k being Nat holds
( p divides Product (primesFinS k) iff primeindex p < k )

proof end;

theorem Th30: :: NUMBER16:30

for p being Prime
for k being Nat st k <= primeindex p holds
p, Product (primesFinS k) are_coprime

proof end;

theorem Th31: :: NUMBER16:31

for n being Nat holds
( rng (prime_exponents (Product (primesFinS n))) c= {0,1} & card (support (prime_exponents (Product (primesFinS n)))) = n )

proof end;

theorem Th32: :: NUMBER16:32

for n, m being Nat st ( for k being Nat st k < m holds
primenumber k divides n ) holds
Product (primesFinS m) divides n

proof end;

Lm2: for n, m being Nat st n <= m holds
Product (primesFinS n) <= Product (primesFinS m)

proof end;

theorem Th33: :: NUMBER16:33

for n, m being Nat holds
( n < m iff Product (primesFinS n) < Product (primesFinS m) )

proof end;

:: Prove that the ratio of the smallest prime number that does not
:: divide n to n tends to zero as n increases to infinity

theorem :: NUMBER16:34

for r being Real_Sequence st ( for n being non zero Nat ex q being Prime st
( r . n = q / n & not q divides n & ( for p being Prime st not p divides n holds
q <= p ) ) ) holds
( r is convergent & lim r = 0 )

proof end;

:: Prove that for all sufficiently large n, between n and 2n
:: there exists at least one number which is a product of s
:: different primes for a given s

theorem :: NUMBER16:35

for s being non zero Nat
for n being Nat st n > Product (primesFinS s) holds
ex p being Nat st
( n < p & p < 2 * n & rng (prime_exponents p) c= {0,1} & card (support (prime_exponents p)) = s )

proof end;

:: Prove that the Chebyshev theorem is equivalent to the theorem
:: that for integers n > 1 the expansion of n! into prime factors
:: contains at least one prime with exponent 1.

theorem Th36: :: NUMBER16:36

for n being Nat
for p being Prime st p <= n & p |^ 2 divides n ! holds
2 * p <= n

proof end;

theorem Th37: :: NUMBER16:37

for a, b, n being Nat st 0 < a & a < b & b <= n holds
a * b divides n !

proof end;

theorem Th38: :: NUMBER16:38

for n being Nat
for p being Prime st 2 < n & n div 2 < p & p <= 2 * (n div 2) holds
p |-count (n !) = 1

proof end;

theorem :: NUMBER16:39

( ( for n being Nat st n > 1 holds
ex p being Prime st
( n < p & p < 2 * n ) ) iff for n being Nat st n > 1 holds
ex p being Prime st p |-count (n !) = 1 )

proof end;

:: Prove equivalence, there are two primes between n and 2n where 5 < n,
:: and the expansion of n! into prime factors contains at least two primes
:: with exponent 1 where n > 11.

theorem :: NUMBER16:40

( ( for n being Nat st n > 5 holds
ex p, q being Prime st
( n < p & p < q & q < 2 * n ) ) implies for n being Nat st n > 10 holds
ex p, q being Prime st
( p < q & p |-count (n !) = 1 & q |-count (n !) = 1 ) )

proof end;