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

registration

let f be real-valued positive-yielding FinSequence;

cluster Rev f -> positive-yielding ;

coherence
Rev f is positive-yielding

proof end;

let n be Nat;

cluster f /^ n -> positive-yielding ;

coherence
f /^ n is positive-yielding

proof end;

cluster f | n -> positive-yielding ;

coherence
f | n is positive-yielding ;

end;

registration

let f be real-valued positive-yielding FinSequence;
let n, m be Nat;

cluster mid (f,n,m) -> positive-yielding ;

coherence
mid (f,n,m) is positive-yielding

proof end;

end;

theorem Th1: :: NUMBER19:1

for n, m being Nat st n divides m holds
NatDivisors n c= NatDivisors m

proof end;

theorem :: NUMBER19:2

for n being Nat
for p being Prime
for m being non zero Nat st p |^ n divides m holds
n + 1 <= card (NatDivisors m)

proof end;

registration

let p be Prime;

cluster p -' 1 -> non zero ;

coherence
not p -' 1 is zero

proof end;

end;

theorem Th3: :: NUMBER19:3

for k, m, n being Nat
for p being Prime st 1 <= k & k <= m & m <= n holds
( p divides Product (mid ((primesFinS n),k,m)) iff ( k <= 1 + (primeindex p) & 1 + (primeindex p) <= m ) )

proof end;

theorem :: NUMBER19:4

for k, m, n, a, b being Nat st 1 <= k & k <= m & m < n & n <= a & a <= b holds
Product (mid ((primesFinS b),k,m)), Product (mid ((primesFinS b),n,a)) are_coprime

proof end;

theorem Th5: :: NUMBER19:5

for u being integer-valued FinSequence
for m being CR_Sequence
for z being Integer st z solves_CRT u,m holds
for i being Nat st i in dom u & u . i,m . i are_coprime holds
z,m . i are_coprime by NUMBER14:def 3, WSIERP_1:43;

theorem :: NUMBER19:6

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for z being Nat st z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) holds
z, Product m are_coprime

proof end;

registration

let f be one-to-one FinSequence;
let n, m be Nat;

cluster mid (f,n,m) -> one-to-one ;

coherence
mid (f,n,m) is one-to-one

proof end;

end;

theorem Th7: :: NUMBER19:7

for k, m, n being Nat st 1 <= k & k <= m & m <= n holds
PrimeDivisors (Product (mid ((primesFinS n),k,m))) = rng (mid ((primesFinS n),k,m))

proof end;

theorem :: NUMBER19:8

for k, m, n being Nat st 1 <= k & k <= m & m <= n holds
card (PrimeDivisors (Product (mid ((primesFinS n),k,m)))) = (m - k) + 1

proof end;

theorem :: NUMBER19:9

for n, k being Nat st k divides n holds
PrimeDivisors k c= PrimeDivisors n

proof end;

theorem Th10: :: NUMBER19:10

for n being Nat holds n < primenumber n

proof end;

theorem :: NUMBER19:11

for p being Prime holds primeindex p < p

proof end;

theorem Th12: :: NUMBER19:12

for n, b being Nat holds value ((n --> 0),b) = 0

proof end;

theorem Th13: :: NUMBER19:13

for n, k, b being Nat st b > 1 & k > 0 & n > 0 holds
value (((<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))),b) = (k * (b |^ n)) + 1

proof end;

theorem :: NUMBER19:14

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

proof end;

theorem :: NUMBER19:15

for f, g being XFinSequence
for X being set holds card ((f ^ g) " X) = (card (f " X)) + (card (g " X))

proof end;

theorem Th16: :: NUMBER19:16

for n, k, b being Nat st b > 1 & k > 0 holds
value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) = (k * (b |^ n)) - 1

proof end;

theorem :: NUMBER19:17

for n, k, b being Nat st b > 1 & k > 0 & n > 0 holds
Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1)

proof end;

:: For each odd number n > 1, the numbers n and n + 2 are prime
:: if and only if (n - 1)! is not divisible by n or n + 2.

theorem Th18: :: NUMBER19:18

for n being natural odd number st n > 1 holds
( n is prime iff not n divides (n -' 1) ! )

proof end;

theorem Th19: :: NUMBER19:19

for n being natural odd number st n > 1 holds
( n + 2 is prime iff not n + 2 divides (n -' 1) ! )

proof end;

:: Problem 108

theorem :: NUMBER19:20

for n being natural odd number st n > 1 holds
( n is prime & n + 2 is prime iff ( not n divides (n -' 1) ! & not n + 2 divides (n -' 1) ! ) ) by Th18, Th19;

:: For each integer s between 2 and 10 inclusive, find all prime numbers
:: p such that the sum of all positive integer divisors of p is equal to
:: the s^(th) power of an integer.

theorem Th21: :: NUMBER19:21

for n, s being Nat
for p being Prime st Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s holds
n = 2

proof end;

::Problem 112

theorem :: NUMBER19:22

for p being Prime
for n, s being Nat st Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s & s <= 10 & not ( s = 2 & p = 3 ) & not ( s = 3 & p = 7 ) & not ( s = 5 & p = 31 ) holds
( s = 7 & p = 127 )

proof end;

:: Prove that no prime greater than 5 and positive integer m exists such
:: that (p-1)!+1 = p^m.

theorem Th23: :: NUMBER19:23

for m being Nat
for p being Prime st p > 5 holds
((p -' 1) !) + 1 <> p |^ m

proof end;

:: Prove that there are infinitely many prime numbers q for which there
:: is a positive integer n < q such that q divides (n-1)!+1.

theorem Th24: :: NUMBER19:24

for p being Prime st p > 5 holds
ex q being Prime st
( p < q & q divides ((p -' 1) !) + 1 )

proof end;

theorem Th25: :: NUMBER19:25

for n, k being Nat st 0 < n & n < k holds
n ! < k !

proof end;

theorem Th26: :: NUMBER19:26

{ q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } is infinite

proof end;

:: Problem 114

theorem :: NUMBER19:27

{ q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) } is infinite

proof end;

:: There are an infinite number of positive integers k such that
:: all numbers of the form k * 2^n+1 (where n = 1, 2, ...) are composite.

theorem Th28: :: NUMBER19:28

( Fermat 5 = (2 |^ 32) + 1 & (2 |^ 32) + 1 = 641 * 6700417 & 6700417 > Fermat 4 )

proof end;

Lm1: for n, t being Nat holds Fermat n divides (2 |^ ((2 |^ n) * ((2 * t) + 1))) + 1

proof end;

theorem Th29: :: NUMBER19:29

((2 |^ 32) - 1) * 641,6700417 are_coprime

proof end;

Lm2: for m being Nat st m <= 4 holds
Fermat m divides (2 |^ 32) - 1

proof end;

theorem Th30: :: NUMBER19:30

for k being Nat st k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k > 6700417 holds
for n being positive Nat holds
( (k * (2 |^ n)) + 1 is composite & ( not not Fermat 0 divides (k * (2 |^ n)) + 1 & ... & not Fermat 4 divides (k * (2 |^ n)) + 1 or 641 divides (k * (2 |^ n)) + 1 or 6700417 divides (k * (2 |^ n)) + 1 ) )

proof end;

theorem Th31: :: NUMBER19:31

ex crt being Nat st
( 6700417 < crt & crt < 2 * ((2 |^ 64) - 1) & ( for n being Nat holds
( crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod ((2 |^ 32) - 1) * 641 & crt + ((n * 2) * ((2 |^ 64) - 1)), - 1 are_congruent_mod 6700417 & crt + ((n * 2) * ((2 |^ 64) - 1)),1 are_congruent_mod 2 ) ) )

proof end;

::Problem 118

theorem :: NUMBER19:32

{ k where k is Nat : for n being positive Nat holds (k * (2 |^ n)) + 1 is composite } is infinite

proof end;

:: There are infinitely many odd numbers k such that every number
:: of the form 2^n + k (where n = 1, 2, ...) is composite.

theorem :: NUMBER19:33

for k being Nat st k = (((15 * 1000000000) * 1000000000) + (511380746 * 1000000000)) + 462593381 holds
( k > 6700417 & k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k,1 are_congruent_mod 2 & not Fermat 0 divides (k * (2 |^ (2 |^ 5))) + 1 & ... & not Fermat 4 divides (k * (2 |^ (2 |^ 5))) + 1 & not 6700417 divides (k * (2 |^ (2 |^ 5))) + 1 & 641 divides (k * (2 |^ (2 |^ 5))) + 1 )

proof end;

registration

let n be Nat;

cluster Fermat n -> odd ;

coherence
not Fermat n is even

proof end;

end;

theorem Th34: :: NUMBER19:34

for n, m being non zero Nat
for p being Prime st p |^ n divides m holds
Euler (p |^ n) <= Euler m

proof end;

theorem Th35: :: NUMBER19:35

for k being Nat st k,1 are_congruent_mod ((2 |^ 32) - 1) * 641 & k, - 1 are_congruent_mod 6700417 & k > 6700417 holds
for n being positive Nat holds
( k + (2 |^ n) is composite & ( not not Fermat 0 divides k + (2 |^ n) & ... & not Fermat 4 divides k + (2 |^ n) or 641 divides k + (2 |^ n) or 6700417 divides k + (2 |^ n) ) )

proof end;

::Problem 119

theorem :: NUMBER19:36

{ k where k is Nat : for n being positive Nat holds (2 |^ n) + k is composite } is infinite

proof end;

theorem :: NUMBER19:37

for L being non empty ZeroStr
for p being Polynomial of L st len p = 1 holds
p = <%(p . 0)%>

proof end;

theorem Th38: :: NUMBER19:38

for L being non empty ZeroStr
for p being Polynomial of L st len p = 2 holds
p = <%(p . 0),(p . 1)%>

proof end;

theorem Th39: :: NUMBER19:39

for R being Ring
for x being Element of R
for p being Polynomial of R holds Ext_eval (p,x) = eval (p,x)

proof end;

theorem Th40: :: NUMBER19:40

for R, S being Ring st S is Subring of R holds
for p being Polynomial of R
for x being Element of R
for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)

proof end;

theorem Th41: :: NUMBER19:41

for R being Field
for p being Polynomial of R
for a being Element of R st a is_a_root_of p holds
p = (p div (rpoly (1,a))) *' (rpoly (1,a))

proof end;

theorem Th42: :: NUMBER19:42

for R being comRing
for S being Ring st S is Subring of R holds
for p, q being Polynomial of R st p is Polynomial of S holds
for a being Element of R
for b being Element of S st a = b & b is left_invertible & p = q *' (rpoly (1,a)) holds
q is Polynomial of S

proof end;

definition

let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ;
let z be FinSequence of the carrier of L;
let f be NAT -valued FinSequence;

func rpoly (f,z) -> FinSequence of the carrier of (Polynom-Ring L) means :Def1: :: NUMBER19:def 1
( len it = len f & ( for i being Nat st 1 <= i & i <= len f holds
it . i = rpoly ((f /. i),(z /. i)) ) );

existence
ex b₁ being FinSequence of the carrier of (Polynom-Ring L) st
( len b₁ = len f & ( for i being Nat st 1 <= i & i <= len f holds
b₁ . i = rpoly ((f /. i),(z /. i)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of (Polynom-Ring L) st len b₁ = len f & ( for i being Nat st 1 <= i & i <= len f holds
b₁ . i = rpoly ((f /. i),(z /. i)) ) & len b₂ = len f & ( for i being Nat st 1 <= i & i <= len f holds
b₂ . i = rpoly ((f /. i),(z /. i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines rpoly NUMBER19:def 1 :
for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for b₄ being FinSequence of the carrier of (Polynom-Ring L) holds
( b₄ = rpoly (f,z) iff ( len b₄ = len f & ( for i being Nat st 1 <= i & i <= len f holds
b₄ . i = rpoly ((f /. i),(z /. i)) ) ) );

theorem Th43: :: NUMBER19:43

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z1, z2 being FinSequence of the carrier of L
for f1, f2 being NAT -valued FinSequence st len f1 = len z1 & len f2 <= len z2 holds
rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2))

proof end;

theorem Th44: :: NUMBER19:44

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being Element of the carrier of L
for k being Element of NAT holds rpoly (<*k*>,<*z*>) = <*(rpoly (k,z))*>

proof end;

theorem :: NUMBER19:45

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z1, z2 being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f <= len z1 & len f <= len z2 & z1 | (len f) = z2 | (len f) holds
rpoly (f,z1) = rpoly (f,z2)

proof end;

theorem Th46: :: NUMBER19:46

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for n being Nat st n < len f holds
rpoly ((f | (n + 1)),z) = (rpoly ((f | n),z)) ^ <*(rpoly ((f /. (n + 1)),(z /. (n + 1))))*>

proof end;

theorem Th47: :: NUMBER19:47

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f = len z holds
for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
rpoly ((f * p),zp) = (rpoly (f,z)) * p

proof end;

theorem Th48: :: NUMBER19:48

for L being comRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence st len f = len z holds
for p being Permutation of (dom f)
for zp being FinSequence of the carrier of L st zp = z * p holds
Product (rpoly (f,z)) = Product (rpoly ((f * p),zp))

proof end;

theorem Th49: :: NUMBER19:49

for L being non degenerated domRing-like Ring
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence holds deg (~ (Product (rpoly (f,z)))) = Sum f

proof end;

theorem Th50: :: NUMBER19:50

for L being non degenerated comRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for x being Element of the carrier of L ex e being FinSequence of the carrier of L st
( eval ((~ (Product (rpoly (f,z)))),x) = Product e & len e = len f & ( for i being Nat st 1 <= i & i <= len e holds
e . i = eval ((rpoly ((f /. i),(z /. i))),x) ) )

proof end;

theorem Th51: :: NUMBER19:51

for L being non degenerated comRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for i being Nat st i in dom f & f . i <> 0 holds
z /. i is_a_root_of ~ (Product (rpoly (f,z)))

proof end;

theorem Th52: :: NUMBER19:52

for L being domRing
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for x being Element of the carrier of L holds
( x is_a_root_of ~ (Product (rpoly (f,z))) iff ex i being Nat st
( i in dom f & x is_a_root_of rpoly ((f /. i),(z /. i)) ) )

proof end;

theorem Th53: :: NUMBER19:53

for L being domRing
for z being FinSequence of the carrier of L holds Roots (~ (Product (rpoly (((len z) |-> 1),z)))) = rng z

proof end;

definition

let F be Field;
let X be finite Subset of F;
let x be Element of F;

func LagBPoly (X,x) -> Polynomial of F means :Def2: :: NUMBER19:def 2
for z being one-to-one FinSequence of the carrier of F st rng z = X holds
it = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z))));

existence
ex b₁ being Polynomial of F st
for z being one-to-one FinSequence of the carrier of F st rng z = X holds
b₁ = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z))))

proof end;

uniqueness
for b₁, b₂ being Polynomial of F st ( for z being one-to-one FinSequence of the carrier of F st rng z = X holds
b₁ = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z)))) ) & ( for z being one-to-one FinSequence of the carrier of F st rng z = X holds
b₂ = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z)))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines LagBPoly NUMBER19:def 2 :
for F being Field
for X being finite Subset of F
for x being Element of F
for b₄ being Polynomial of F holds
( b₄ = LagBPoly (X,x) iff for z being one-to-one FinSequence of the carrier of F st rng z = X holds
b₄ = ((eval ((~ (Product (rpoly (((len z) |-> 1),z)))),x)) ") * (~ (Product (rpoly (((len z) |-> 1),z)))) );

theorem Th54: :: NUMBER19:54

for F being Field
for X being finite Subset of F
for x being Element of F st not x in X holds
( Roots (LagBPoly (X,x)) = X & eval ((LagBPoly (X,x)),x) = 1. F & deg (LagBPoly (X,x)) = card X )

proof end;

theorem :: NUMBER19:55

for F being Field
for x, y being Element of F holds LagBPoly ({y},x) = ((x - y) ") * (rpoly (1,y))

proof end;

theorem :: NUMBER19:56

for F being Field
for X1, X2 being finite Subset of F
for x being Element of F st not x in X1 & not x in X2 & X1 misses X2 holds
(LagBPoly (X1,x)) *' (LagBPoly (X2,x)) = LagBPoly ((X1 \/ X2),x)

proof end;

definition

let F be Field;
let x, y be FinSequence of the carrier of F;

func LagPoly (x,y) -> Polynomial of F means :Def3: :: NUMBER19:def 3
ex L being FinSequence of the carrier of (Polynom-Ring F) st
( it = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) );

existence
ex b₁ being Polynomial of F ex L being FinSequence of the carrier of (Polynom-Ring F) st
( b₁ = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) )

proof end;

uniqueness
for b₁, b₂ being Polynomial of F st ex L being FinSequence of the carrier of (Polynom-Ring F) st
( b₁ = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) ) & ex L being FinSequence of the carrier of (Polynom-Ring F) st
( b₂ = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines LagPoly NUMBER19:def 3 :
for F being Field
for x, y being FinSequence of the carrier of F
for b₄ being Polynomial of F holds
( b₄ = LagPoly (x,y) iff ex L being FinSequence of the carrier of (Polynom-Ring F) st
( b₄ = Sum L & len L = len x & ( for i being Nat st 1 <= i & i <= len x holds
L . i = (y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i))) ) ) );

theorem Th57: :: NUMBER19:57

for F being Field
for x, y being FinSequence of the carrier of F
for i being Nat holds
( ( y /. i <> 0. F implies Roots ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (rng x) \ {(x /. i)} ) & eval (((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))),(x /. i)) = y /. i & ( i in dom x & y /. i <> 0. F implies deg ((y /. i) * (LagBPoly (((rng x) \ {(x /. i)}),(x /. i)))) = (card (rng x)) - 1 ) )

proof end;

theorem :: NUMBER19:58

for F being Field
for x, y being FinSequence of the carrier of F holds degree (LagPoly (x,y)) <= (len x) - 1

proof end;

theorem Th59: :: NUMBER19:59

for F being Field
for x, y being FinSequence of the carrier of F st x is one-to-one holds
for i being Nat st i in dom x holds
eval ((LagPoly (x,y)),(x /. i)) = y /. i

proof end;

definition

let F be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ;
let z be FinSequence of the carrier of F;
let i be Nat;

func LagIPoly (z,i) -> Polynomial of F equals :: NUMBER19:def 4
Product (rpoly (((len (Del (z,i))) |-> 1),(Del (z,i))));

coherence
Product (rpoly (((len (Del (z,i))) |-> 1),(Del (z,i)))) is Polynomial of F

proof end;

end;

:: deftheorem defines LagIPoly NUMBER19:def 4 :
for F being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of F
for i being Nat holds LagIPoly (z,i) = Product (rpoly (((len (Del (z,i))) |-> 1),(Del (z,i))));

theorem :: NUMBER19:60

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for i being Nat st not i in dom z holds
LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z))

proof end;

theorem Th61: :: NUMBER19:61

for z being FinSequence
for i being Nat st z is_one-to-one_at i holds
rng (Del (z,i)) = (rng z) \ {(z . i)}

proof end;

theorem :: NUMBER19:62

for F being Field
for z being FinSequence of the carrier of F
for i being Nat st i in dom z & z is one-to-one holds
LagBPoly (((rng z) \ {(z . i)}),(z /. i)) = ((eval ((LagIPoly (z,i)),(z /. i))) ") * (LagIPoly (z,i))

proof end;

theorem Th63: :: NUMBER19:63

for n, k being Nat st 1 <= k & k <= n holds
for z being FinSequence of INT.Ring st z = idseq n holds
( eval ((LagIPoly (z,k)),(In (k,INT.Ring))) = (((- 1) |^ (n -' k)) * ((n -' k) !)) * ((k -' 1) !) & ( for i being Nat st 1 <= i & i <= n & i <> k holds
In (i,INT.Ring) is_a_root_of LagIPoly (z,k) ) )

proof end;

theorem :: NUMBER19:64

for n being Nat
for y being b₁ -element FinSequence of INT ex p being Polynomial of INT.Ring st
for k being Nat st 1 <= k & k <= n holds
eval (p,(In (k,INT.Ring))) = 1 + ((((k -' 1) !) * ((n -' k) !)) * (y . k))

proof end;

registration

let i be Rational;

reduce In (i,F_Rat) to i;

reducibility
In (i,F_Rat) = i by SUBSET_1:def 8, RAT_1:def 2, GAUSSINT:def 14;

end;

:: Prove that there is no polynomial f(x) with integer coefficients
:: such that f(1) = 2, f(2) = 3 and f(3) = 5.
:: However, for every integer m > 1, there exists a polynomial f(x)
:: with rational coefficients such that f(k) = P.k for k = 1, 2, ...,
:: where P.k denotes the k^(th) prime number.
:: Problem 127 part 1

theorem :: NUMBER19:65

for p being Polynomial of INT.Ring holds
( not eval (p,(In (1,INT.Ring))) = 2 or not eval (p,(In (3,INT.Ring))) = 5 )

proof end;

:: Problem 127 part 2

theorem :: NUMBER19:66

for n being Nat
for i, z being FinSequence of the carrier of F_Rat st i = idseq n & z = primesFinS n holds
for k being Nat st k < n holds
eval ((LagPoly (i,z)),(In ((k + 1),F_Rat))) = primenumber k

proof end;

:: Provide an example of a reducible polynomial, f(x), with integer
:: coefficients, for which the values of f(x) for m distinct positive
:: integers are all prime numbers.

theorem :: NUMBER19:67

for n being Nat ex p, q being Polynomial of INT.Ring st
( degree p > 0 & degree q > 0 & ( for i being Nat st i <= n holds
eval ((p *' q),(In ((primenumber i),INT.Ring))) = primenumber i ) )

proof end;

:: Show that if f(x) is a non-constant polynomial with integer coefficients,
:: then the congruence f(x)==0(mod p) has a solution for an infinite number
:: of primes p.

theorem Th68: :: NUMBER19:68

for L being non empty non degenerated well-unital unital multLoopStr_0 st L is domRing-like holds
for x being Element of L
for i being Nat st (power L) . (x,i) = 0. L holds
x = 0. L

proof end;

theorem Th69: :: NUMBER19:69

for L being non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive unital associative commutative domRing-like doubleLoopStr
for p being Polynomial of L st p . 0 <> 0. L holds
ex q being Polynomial of L st
( len p = len q & q . 0 = 1. L & ( for i being Element of NAT st 0 < i holds
q . i = (p . i) * ((power L) . ((p . 0),(i -' 1))) ) & ( for x being Element of L holds eval (p,((p . 0) * x)) = (p . 0) * (eval (q,x)) ) )

proof end;

theorem Th70: :: NUMBER19:70

for L being non empty right_complementable Abelian add-associative right_zeroed left-distributive well-unital unital associative doubleLoopStr
for p being Polynomial of L
for x being Element of L ex d being Element of L st eval (p,x) = (d * x) + (p . 0)

proof end;

Lm3: for p being Polynomial of F_Complex st len p > 2 holds
for r being Real ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r

proof end;

theorem Th71: :: NUMBER19:71

for p being Polynomial of F_Complex st len p >= 2 holds
for r being Real ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r

proof end;

:: Problem 130

theorem :: NUMBER19:72

for f being Polynomial of INT.Ring st degree f > 0 holds
{ p where p is Prime : ex x being Element of INT.Ring st eval (f,x), 0 are_congruent_mod p } is infinite

proof end;

theorem Th73: :: NUMBER19:73

for n, m, k being Nat holds
( k in seq (n,m) iff ( n < k & k <= n + m ) )

proof end;

theorem Th74: :: NUMBER19:74

for n, m, k being Nat holds
( k in primeNumbers (n,m) iff ( n < k & k <= n + m & k is prime ) )

proof end;

theorem Th75: :: NUMBER19:75

for n1, m1, n2, m2 being Nat st n1 + m1 <= n2 holds
seq (n1,m1) misses seq (n2,m2)

proof end;

theorem Th76: :: NUMBER19:76

for n1, m1, n2, m2 being Nat st n1 + m1 <= n2 holds
primeNumbers (n1,m1) misses primeNumbers (n2,m2)

proof end;

theorem Th77: :: NUMBER19:77

for n, m, k being Nat holds (seq (n,m)) \/ (seq ((n + m),k)) = seq (n,(m + k))

proof end;

theorem Th78: :: NUMBER19:78

for n, m, k being Nat holds (primeNumbers (n,m)) \/ (primeNumbers ((n + m),k)) = primeNumbers (n,(m + k))

proof end;

theorem Th79: :: NUMBER19:79

for n, m, k being Nat holds card (primeNumbers (n,(m + k))) = (card (primeNumbers (n,m))) + (card (primeNumbers ((n + m),k)))

proof end;

theorem Th80: :: NUMBER19:80

for n being Nat holds
( ( n + 1 is prime implies primeNumbers (n,1) = {(n + 1)} ) & ( not n + 1 is prime implies primeNumbers (n,1) = {} ) )

proof end;

theorem Th81: :: NUMBER19:81

for n being Nat holds
( ( n + 1 is prime implies card (primeNumbers (n,1)) = 1 ) & ( not n + 1 is prime implies card (primeNumbers (n,1)) = 0 ) )

proof end;

Lm4: for n being Nat holds card (primeNumbers (n,4)) = (((card (primeNumbers (n,1))) + (card (primeNumbers ((n + 1),1)))) + (card (primeNumbers ((n + 2),1)))) + (card (primeNumbers ((n + 3),1)))

proof end;

theorem Th82: :: NUMBER19:82

for n, k being Nat st k > 0 & ( ( n + 1 is prime & (n + k) + 1 is prime ) or ( not n + 1 is prime & not (n + k) + 1 is prime ) ) holds
card (primeNumbers ((n + 1),k)) = card (primeNumbers (n,k))

proof end;

theorem Th83: :: NUMBER19:83

for n, k being Nat st k > 0 & not n + 1 is prime & (n + k) + 1 is prime holds
card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) + 1

proof end;

theorem Th84: :: NUMBER19:84

for n, k being Nat st k > 0 & n + 1 is prime & not (n + k) + 1 is prime holds
card (primeNumbers ((n + 1),k)) = (card (primeNumbers (n,k))) - 1

proof end;

Lm5: ( card (primeNumbers (0,21)) = 8 & card (primeNumbers (0,100)) = 25 )

proof end;

theorem Th85: :: NUMBER19:85

( card (primeNumbers (1,100)) = 26 & ( for k being Nat st ( k = 0 or k = 2 or k = 3 or k = 4 or k = 9 or k = 10 ) holds
card (primeNumbers (k,100)) = 25 ) & ( for k being Nat st ( k = 5 or k = 6 or k = 7 or k = 8 ) holds
card (primeNumbers (k,100)) < 25 ) )

proof end;

theorem Th86: :: NUMBER19:86

for n, k, p being Integer st p divides k holds
( n in multiples p iff n + k in multiples p )

proof end;

theorem Th87: :: NUMBER19:87

for n, k, d, s being Nat holds
( s in seq (n,k) iff s + d in seq ((n + d),k) )

proof end;

theorem Th88: :: NUMBER19:88

for n, k, d being Nat
for p, q, r, s, t being Integer st p divides d & q divides d & r divides d & s divides d & t divides d holds
card ((seq (n,k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + d),k)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

proof end;

theorem Th89: :: NUMBER19:89

for n, k, d being Nat
for p, q, r, s, t being Integer st p divides d & q divides d & r divides d & s divides d & t divides d holds
card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

proof end;

theorem Th90: :: NUMBER19:90

for n, k, d being Nat
for p, q, r, s, t being Integer st p divides d & q divides d & r divides d & s divides d & t divides d holds
card ((seq (n,(k * d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = k * (card ((seq (0,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))))

proof end;

theorem Th91: :: NUMBER19:91

for n being Nat holds
( 4 = card ((seq ((6 * n),6)) /\ ((multiples 2) \/ (multiples 3))) & {((6 * n) + 1),((6 * n) + 5)} = (seq ((6 * n),6)) \ ((multiples 2) \/ (multiples 3)) )

proof end;

theorem Th92: :: NUMBER19:92

22 = card ((seq (0,30)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))

proof end;

Lm6: for i being Nat holds
( not i in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) iff ( not 2 divides i & not 3 divides i & not 5 divides i ) )

proof end;

Lm7: for n, c being Nat st 0 <= n & n < 30 & c = card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) holds
( c >= 72 & ( not c = 72 or n = 9 or n = 10 ) )

proof end;

theorem Th93: :: NUMBER19:93

for n, c being Nat st c = card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) holds
( c >= 72 & ( not c = 72 or n mod 30 = 9 or n mod 30 = 10 ) )

proof end;

Lm8: for n, c being Nat st 0 <= n & n < 210 & c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) holds
( c >= 75 & ( not c = 75 or n = 9 or n = 10 or n = 99 or n = 100 ) )

proof end;

theorem Th94: :: NUMBER19:94

for n, c being Nat st c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) holds
( c >= 75 & ( not c = 75 or n mod 210 = 9 or n mod 210 = 10 or n mod 210 = 99 or n mod 210 = 100 ) )

proof end;

Lm9: for i being Nat holds
( not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) iff ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i ) )

proof end;

theorem Th95: :: NUMBER19:95

for n being Nat st 0 <= n & n < (((2 * 3) * 5) * 7) * 11 holds
76 <= card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)))

proof end;

theorem Th96: :: NUMBER19:96

for n being Nat st 11 <= n holds
card (primeNumbers (n,100)) <= 24

proof end;

Lm10: for n being Nat st 0 <= n & n < 6 holds
card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13

proof end;

theorem Th97: :: NUMBER19:97

for n being Nat st 0 <= n & n < (2 * 3) * 5 holds
14 <= card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))

proof end;

theorem Th98: :: NUMBER19:98

for n being Nat st 5 <= n holds
card (primeNumbers (n,21)) <= 7

proof end;

:: The only case' where the sequences k+l, k+2, ..., k+100
:: contain maximal numbers of primes (26) is when n = 1.

theorem :: NUMBER19:99

( card (primeNumbers (1,100)) = 26 & ( for n being Nat st n <> 1 holds
card (primeNumbers (n,100)) < 26 ) )

proof end;

:: The sequences k+l, k+2, ..., k+100 contain exactly 25 prime numbers
:: in only six cases: k = 0, 2, 3, 4, 9 and 10.

theorem :: NUMBER19:100

{ n where n is Nat : card (primeNumbers (n,100)) = 25 } = {0,2,3,4,9,10}

proof end;

:: The sequences k+l, k+2, ..., k+21 contain exactly 8 prime numbers
:: in only three cases: when k = 0, 1 or 2.

theorem :: NUMBER19:101

{ n where n is Nat : card (primeNumbers (n,21)) = 8 } = {0,1,2}

proof end;