:: Elementary Number Theory Problems. Part {XIII}
:: by Artur Korni{\l}owicz and Rafa{\l} Ziobro
::
:: Received June 18, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

Lm1: 2 |^ 0 = 1
by NEWTON:4;

Lm2: 2 |^ 2 = 2 * 2
by NEWTON:81;

Lm3: 2 |^ 3 = (2 * 2) * 2
by POLYEQ_5:2;

Lm4: 2 |^ 4 = ((2 * 2) * 2) * 2
by POLYEQ_5:3;

Lm5: 2 |^ 5 = (((2 * 2) * 2) * 2) * 2
by NUMBER02:1;

Lm6: 2 |^ 8 = ((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER02:4;

Lm7: 2 |^ (8 + 8) = (2 |^ 8) * (2 |^ 8) by NEWTON:8
.= 65536 by Lm6 ;

Lm8: 1 mod 3 = 1
by NAT_D:24;

Lm9: 2 mod 3 = 2
by NAT_D:24;

4 = 1 + (3 * 1)
;

then Lm10: 4 mod 3 = 1 mod 3
by NAT_D:61;

theorem Th1: :: NUMBER13:1

for n being Nat holds
( not n < 3 or n = 0 or n = 1 or n = 2 )

proof end;

theorem :: NUMBER13:2

for n being Nat holds
( not n < 4 or n = 0 or n = 1 or n = 2 or n = 3 )

proof end;

theorem Th3: :: NUMBER13:3

for n being Nat holds
( not n < 5 or n = 0 or n = 1 or n = 2 or n = 3 or n = 4 )

proof end;

registration

cluster 1 / 2 -> non integer ;

coherence
not 1 / 2 is integer

proof end;

end;

registration

cluster non natural complex real ext-real rational for object ;

existence
not for b₁ being Rational holds b₁ is natural

proof end;

end;

registration

cluster complex real non integer ext-real rational for object ;

existence
not for b₁ being Rational holds b₁ is integer

proof end;

end;

theorem Th4: :: NUMBER13:4

for i, j being Integer st j <> 0 & i / j is integer holds
j divides i

proof end;

registration

let q be non integer Rational;

cluster q ^2 -> non integer ;

coherence
not q ^2 is integer

proof end;

end;

theorem Th5: :: NUMBER13:5

for a, b, c being Nat st (a / b) * c is natural & b <> 0 & a,b are_coprime holds
ex d being Nat st c = b * d

proof end;

:: Problem 41 a

theorem :: NUMBER13:6

for k being Integer holds (2 * k) + 1,(9 * k) + 4 are_coprime

proof end;

:: Problem 41 b

theorem :: NUMBER13:7

for k being Integer holds ((2 * k) - 1) gcd ((9 * k) + 4) = (k + 8) gcd 17

proof end;

theorem Th8: :: NUMBER13:8

for m, n being Nat st m > 1 & n > 1 & m,n are_coprime holds
ex p, q being Prime st
( p divides m & not p divides n & q divides n & not q divides m & p <> q )

proof end;

definition

let k be Nat;

func primesFinS k -> FinSequence of NAT means :Def1: :: NUMBER13:def 1
( len it = k & ( for i being Nat st i < k holds
it . (i + 1) = primenumber i ) );

existence
ex b₁ being FinSequence of NAT st
( len b₁ = k & ( for i being Nat st i < k holds
b₁ . (i + 1) = primenumber i ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = k & ( for i being Nat st i < k holds
b₁ . (i + 1) = primenumber i ) & len b₂ = k & ( for i being Nat st i < k holds
b₂ . (i + 1) = primenumber i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines primesFinS NUMBER13:def 1 :
for k being Nat
for b₂ being FinSequence of NAT holds
( b₂ = primesFinS k iff ( len b₂ = k & ( for i being Nat st i < k holds
b₂ . (i + 1) = primenumber i ) ) );

registration

cluster primesFinS 0 -> empty ;

coherence
primesFinS 0 is empty

proof end;

end;

theorem :: NUMBER13:9

primesFinS 1 = <*2*>

proof end;

theorem :: NUMBER13:10

primesFinS 2 = <*2,3*>

proof end;

theorem Th11: :: NUMBER13:11

primesFinS 3 = <*2,3,5*>

proof end;

theorem Th12: :: NUMBER13:12

for k being Nat
for p being Prime holds
( p < primenumber k iff primeindex p < k )

proof end;

theorem Th13: :: NUMBER13:13

for k being Nat
for p being Prime st primeindex p < k holds
1 + (primeindex p) in dom (primesFinS k)

proof end;

theorem Th14: :: NUMBER13:14

for k being Nat
for p being Prime st primeindex p < k holds
(primesFinS k) . (1 + (primeindex p)) = p

proof end;

theorem Th15: :: NUMBER13:15

for k being Nat
for p being Prime st p < primenumber k holds
p in rng (primesFinS k)

proof end;

theorem Th16: :: NUMBER13:16

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

proof end;

registration

let k be Nat;

cluster primesFinS k -> positive-yielding ;

coherence
primesFinS k is positive-yielding

proof end;

end;

registration

let k be Nat;

cluster primesFinS k -> increasing ;

coherence
primesFinS k is increasing

proof end;

end;

definition

let R be ext-real-valued Relation;

attr R is with_values_greater_or_equal_one means :: NUMBER13:def 2
for r being ExtReal st r in rng R holds
r >= 1;

end;

:: deftheorem defines with_values_greater_or_equal_one NUMBER13:def 2 :
for R being ext-real-valued Relation holds
( R is with_values_greater_or_equal_one iff for r being ExtReal st r in rng R holds
r >= 1 );

registration

cluster <*1*> -> with_values_greater_or_equal_one ;

coherence
<*1*> is with_values_greater_or_equal_one

proof end;

end;

registration

cluster Relation-like omega -defined omega -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued with_values_greater_or_equal_one for set ;

existence
ex b₁ being natural-valued FinSequence st b₁ is with_values_greater_or_equal_one

proof end;

end;

definition

let f be ext-real-valued Function;

redefine attr f is with_values_greater_or_equal_one means :: NUMBER13:def 3
for x being object st x in dom f holds
f . x >= 1;

compatibility
( f is with_values_greater_or_equal_one iff for x being object st x in dom f holds
f . x >= 1 )

proof end;

end;

:: deftheorem defines with_values_greater_or_equal_one NUMBER13:def 3 :
for f being ext-real-valued Function holds
( f is with_values_greater_or_equal_one iff for x being object st x in dom f holds
f . x >= 1 );

definition

let f be ext-real-valued FinSequence;

redefine attr f is with_values_greater_or_equal_one means :: NUMBER13:def 4
for n being Nat st 1 <= n & n <= len f holds
f . n >= 1;

compatibility
( f is with_values_greater_or_equal_one iff for n being Nat st 1 <= n & n <= len f holds
f . n >= 1 )

proof end;

end;

:: deftheorem defines with_values_greater_or_equal_one NUMBER13:def 4 :
for f being ext-real-valued FinSequence holds
( f is with_values_greater_or_equal_one iff for n being Nat st 1 <= n & n <= len f holds
f . n >= 1 );

registration

cluster Relation-like empty ext-real-valued -> ext-real-valued with_values_greater_or_equal_one for set ;

coherence
for b₁ being ext-real-valued Relation st b₁ is empty holds
b₁ is with_values_greater_or_equal_one ;

end;

registration

cluster Relation-like ext-real-valued with_values_greater_or_equal_one -> ext-real-valued positive-yielding for set ;

coherence
for b₁ being ext-real-valued Relation st b₁ is with_values_greater_or_equal_one holds
b₁ is positive-yielding

proof end;

end;

theorem Th17: :: NUMBER13:17

for m, n being Nat st m <= n holds
(primesFinS n) | m = primesFinS m

proof end;

theorem :: NUMBER13:18

for P, R being ext-real-valued Relation st rng P c= rng R & R is with_values_greater_or_equal_one holds
P is with_values_greater_or_equal_one ;

theorem Th19: :: NUMBER13:19

for f, g being ext-real-valued FinSequence st f ^ g is with_values_greater_or_equal_one holds
( f is with_values_greater_or_equal_one & g is with_values_greater_or_equal_one )

proof end;

theorem Th20: :: NUMBER13:20

for r being ExtReal st <*r*> is with_values_greater_or_equal_one holds
r >= 1

proof end;

theorem :: NUMBER13:21

for f being real-valued with_values_greater_or_equal_one FinSequence holds Product f >= 1

proof end;

theorem Th22: :: NUMBER13:22

for n being Nat
for f being real-valued with_values_greater_or_equal_one FinSequence holds Product (f | n) <= Product f

proof end;

registration

let k be Nat;

cluster primesFinS k -> with_values_greater_or_equal_one ;

coherence
primesFinS k is with_values_greater_or_equal_one

proof end;

end;

Lm12: now :: thesis: for k being Nat st 3 <= k holds
Product (primesFinS k) >= ((primenumber 0) * (primenumber 1)) * (primenumber 2)

let k be Nat; :: thesis: ( 3 <= k implies Product (primesFinS k) >= ((primenumber 0) * (primenumber 1)) * (primenumber 2) )
set f = primesFinS k;
set g = primesFinS 3;
set x = ((primenumber 0) * (primenumber 1)) * (primenumber 2);
assume 3 <= k ; :: thesis: Product (primesFinS k) >= ((primenumber 0) * (primenumber 1)) * (primenumber 2)
then A1: primesFinS 3 = (primesFinS k) | 3 by Th17;
((primenumber 0) * (primenumber 1)) * (primenumber 2) = Product (primesFinS 3) by Th11, RVSUM_1:100, MOEBIUS2:8, MOEBIUS2:10, MOEBIUS2:12;
hence Product (primesFinS k) >= ((primenumber 0) * (primenumber 1)) * (primenumber 2) by A1, Th22; :: thesis: verum

end;

:: Problem 92

theorem :: NUMBER13:23

for k being Nat st 3 <= k holds
(primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

proof end;

definition

let k, n be Nat;

pred n satisfies_Sierpinski_problem_121_for k means :: NUMBER13:def 5
( (k * (2 |^ (2 |^ n))) + 1 is composite & ( for m being positive Nat st m < n holds
not (k * (2 |^ (2 |^ m))) + 1 is composite ) );

end;

:: deftheorem defines satisfies_Sierpinski_problem_121_for NUMBER13:def 5 :
for k, n being Nat holds
( n satisfies_Sierpinski_problem_121_for k iff ( (k * (2 |^ (2 |^ n))) + 1 is composite & ( for m being positive Nat st m < n holds
not (k * (2 |^ (2 |^ m))) + 1 is composite ) ) );

:: Problem 121 a

theorem Th24: :: NUMBER13:24

5 satisfies_Sierpinski_problem_121_for 1

proof end;

:: Problem 121 b

theorem :: NUMBER13:25

1 satisfies_Sierpinski_problem_121_for 2

proof end;

:: Problem 121 c

theorem Th26: :: NUMBER13:26

2 satisfies_Sierpinski_problem_121_for 3

proof end;

:: Problem 121 d

theorem Th27: :: NUMBER13:27

2 satisfies_Sierpinski_problem_121_for 4

proof end;

:: Problem 121 e

theorem :: NUMBER13:28

1 satisfies_Sierpinski_problem_121_for 5

proof end;

:: Problem 121 f

theorem :: NUMBER13:29

1 satisfies_Sierpinski_problem_121_for 6

proof end;

:: Problem 121 g

theorem Th30: :: NUMBER13:30

3 satisfies_Sierpinski_problem_121_for 7

proof end;

:: Problem 121 h

theorem :: NUMBER13:31

1 satisfies_Sierpinski_problem_121_for 8

proof end;

:: Problem 121 i

theorem Th32: :: NUMBER13:32

2 satisfies_Sierpinski_problem_121_for 9

proof end;

:: Problem 121 j

theorem Th33: :: NUMBER13:33

2 satisfies_Sierpinski_problem_121_for 10

proof end;

Lm13: for n being positive Nat holds 3 divides (2 * (2 |^ (2 |^ n))) + 1

proof end;

theorem Th34: :: NUMBER13:34

for a being Nat
for n being positive Nat holds 3 divides (((3 * a) + 2) * (2 |^ (2 |^ n))) + 1

proof end;

deffunc H₁( Nat, Nat) -> set = ($1 * (2 |^ (2 |^ $2))) + 1;

Lm14: now :: thesis: for n being Nat holds 2 |^ (2 |^ n) >= 2 |^ (2 |^ 0)

let n be Nat; :: thesis: 2 |^ (2 |^ n) >= 2 |^ (2 |^ 0)
2 |^ n >= 2 |^ 0 by PREPOWER:93;
hence 2 |^ (2 |^ n) >= 2 |^ (2 |^ 0) by PREPOWER:93; :: thesis: verum

end;

Lm15: now :: thesis: for n being Nat holds (2 * (2 |^ (2 |^ n))) + 1 >= (2 * 2) + 1

let n be Nat; :: thesis: (2 * (2 |^ (2 |^ n))) + 1 >= (2 * 2) + 1
2 * (2 |^ (2 |^ n)) >= 2 * 2 by Lm1, Lm14, XREAL_1:64;
hence (2 * (2 |^ (2 |^ n))) + 1 >= (2 * 2) + 1 by XREAL_1:6; :: thesis: verum

end;

Lm16: now :: thesis: for n being Nat holds (5 * (2 |^ (2 |^ n))) + 1 >= (5 * 2) + 1

let n be Nat; :: thesis: (5 * (2 |^ (2 |^ n))) + 1 >= (5 * 2) + 1
5 * (2 |^ (2 |^ n)) >= 5 * 2 by Lm1, Lm14, XREAL_1:64;
hence (5 * (2 |^ (2 |^ n))) + 1 >= (5 * 2) + 1 by XREAL_1:6; :: thesis: verum

end;

Lm17: now :: thesis: for n being Nat holds (8 * (2 |^ (2 |^ n))) + 1 >= (8 * 2) + 1

let n be Nat; :: thesis: (8 * (2 |^ (2 |^ n))) + 1 >= (8 * 2) + 1
8 * (2 |^ (2 |^ n)) >= 8 * 2 by Lm1, Lm14, XREAL_1:64;
hence (8 * (2 |^ (2 |^ n))) + 1 >= (8 * 2) + 1 by XREAL_1:6; :: thesis: verum

end;

theorem Th35: :: NUMBER13:35

for n being positive Nat holds (2 * (2 |^ (2 |^ n))) + 1 is composite

proof end;

theorem Th36: :: NUMBER13:36

for n being positive Nat holds (5 * (2 |^ (2 |^ n))) + 1 is composite

proof end;

theorem Th37: :: NUMBER13:37

for n being positive Nat holds (8 * (2 |^ (2 |^ n))) + 1 is composite

proof end;

:: Problem 122

theorem :: NUMBER13:38

for k being positive Nat holds
( ( k <= 10 & ( for n being positive Nat holds (k * (2 |^ (2 |^ n))) + 1 is composite ) ) iff k in {2,5,8} )

proof end;

theorem Th39: :: NUMBER13:39

for n being Nat holds ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 7

proof end;

theorem :: NUMBER13:40

for n being Nat st n > 0 holds
((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 21

proof end;

theorem Th41: :: NUMBER13:41

for n being Nat st n > 1 holds
((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 >= 273

proof end;

theorem Th42: :: NUMBER13:42

for m, n being Nat st ( m is even or m = 2 * n ) holds
(2 |^ m) mod 3 = 1

proof end;

theorem Th43: :: NUMBER13:43

for m, n being Nat st ( m is odd or m = (2 * n) + 1 ) holds
(2 |^ m) mod 3 = 2

proof end;

theorem Th44: :: NUMBER13:44

for n being non zero Nat holds 3 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1

proof end;

theorem Th45: :: NUMBER13:45

for n being Nat holds 7 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1

proof end;

registration

let n be non zero Nat;

cluster (1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) -> natural ;

coherence
(1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is natural

proof end;

end;

:: Problem 123

theorem :: NUMBER13:46

for n being non zero Nat st n > 1 holds
(1 / 3) * (((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) is composite

proof end;

Lm18: for n, x, y, z being positive Nat st x <= y & (n |^ x) + (n |^ y) = n |^ z holds
( n = 2 & y = x & z = x + 1 )

proof end;

:: Problem 172

theorem :: NUMBER13:47

for n, x, y, z being positive Nat holds
( (n |^ x) + (n |^ y) = n |^ z iff ( n = 2 & y = x & z = x + 1 ) )

proof end;

theorem Th48: :: NUMBER13:48

for a, b, c being Real st c > 1 & c to_power a = c to_power b holds
a = b

proof end;

theorem Th49: :: NUMBER13:49

for n, x, y, z, t being positive Nat st x <= y & y <= z holds
( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) )

proof end;

:: Problem 182

theorem Th50: :: NUMBER13:50

for n, x, y, z, t being positive Nat holds
( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) )

proof end;

:: Problem 183

theorem :: NUMBER13:51

for x, y, z, t being positive Nat holds ((4 |^ x) + (4 |^ y)) + (4 |^ z) <> 4 |^ t by Th50;

Lm19: for x, y, z, t being positive Nat st (x ^2) + (5 * (y ^2)) = z ^2 & (5 * (x ^2)) + (y ^2) = t ^2 holds
ex x1, y1, z1, t1 being Nat st
( (x1 ^2) + (5 * (y1 ^2)) = z1 ^2 & (5 * (x1 ^2)) + (y1 ^2) = t1 ^2 & x1,y1 are_coprime )

proof end;

Lm20: for x, y, z, t being Nat holds
( not x,y are_coprime or (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

Lm21: for x, y, z, t being positive Nat holds
( (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

:: Problem 191

theorem :: NUMBER13:52

for x, y, z, t being non zero Integer holds
( (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

Lm22: for x, y, z, t being positive Nat st (x ^2) + (6 * (y ^2)) = z ^2 & (6 * (x ^2)) + (y ^2) = t ^2 holds
ex x1, y1, z1, t1 being Nat st
( (x1 ^2) + (6 * (y1 ^2)) = z1 ^2 & (6 * (x1 ^2)) + (y1 ^2) = t1 ^2 & x1,y1 are_coprime )

proof end;

Lm23: for x, y, z, t being Nat holds
( not x,y are_coprime or (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

Lm24: for x, y, z, t being positive Nat holds
( (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

:: Problem 192

theorem :: NUMBER13:53

for x, y, z, t being non zero Integer holds
( (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )

proof end;

:: Problem 192 a

theorem :: NUMBER13:54

( (3 ^2) + (7 * (1 ^2)) = 4 ^2 & (7 * (3 ^2)) + (1 ^2) = 8 ^2 ) ;