:: Elementary Number Theory Problems. {P}art {V}
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users


theorem Th1: :: NUMBER05:1
for n, k being Nat st n |^|^ k = 0 holds
n = 0
proof end;

registration
let x be odd Nat;
let i be Nat;
cluster x |^|^ i -> odd ;
coherence
not x |^|^ i is even
proof end;
end;

registration
let x be non zero even Nat;
let i be non zero Nat;
cluster x |^|^ i -> even ;
coherence
x |^|^ i is even
proof end;
end;

:: Problem 12
theorem :: NUMBER05:2
for n being non zero Nat ex x being non zero Nat st
for i being Nat holds n divides (x |^|^ (i + 1)) + 1
proof end;

theorem Th3: :: NUMBER05:3
for i being Integer
for n being Nat st n = (4 * i) + 3 holds
ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides n )
proof end;

definition
defpred S1[ set ] means ex k being Nat st
( $1 = (4 * k) + 3 & (4 * k) + 3 is prime );
func 4k+3_Primes -> Subset of NAT means :Def1: :: NUMBER05:def 1
 for n being Nat holds
( n in it iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) );
existence
ex b1 being Subset of NAT st
for n being Nat holds
( n in b1 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) )
proof end;
uniqueness
for b1, b2 being Subset of NAT st ( for n being Nat holds
( n in b1 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) ) & ( for n being Nat holds
( n in b2 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines 4k+3_Primes NUMBER05:def 1 :
for b1 being Subset of NAT holds
( b1 = 4k+3_Primes iff for n being Nat holds
( n in b1 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) );

theorem Th4: :: NUMBER05:4
for n being Nat st n in 4k+3_Primes holds
n >= 3
proof end;

registration
cluster 4k+3_Primes -> infinite ;
coherence
not 4k+3_Primes is finite
proof end;
end;

:: Problem 13
theorem :: NUMBER05:5
for n being Nat st n in 4k+3_Primes holds
for x being even Nat
for i being Nat holds not n divides (x |^|^ (i + 2)) + 1
proof end;

theorem Th6: :: NUMBER05:6
for a being Integer holds
( 3 divides a or (a |^ 3) mod 9 = 1 or (a |^ 3) mod 9 = 8 )
proof end;

:: Problem 31
theorem :: NUMBER05:7
for a, b, c being Integer holds
( not 9 divides ((a |^ 3) + (b |^ 3)) + (c |^ 3) or 3 divides a or 3 divides b or 3 divides c )
proof end;

theorem Th8: :: NUMBER05:8
for a, b, c, n being Integer holds ((a + b) + c) mod n = (((a mod n) + (b mod n)) + (c mod n)) mod n
proof end;

theorem Th9: :: NUMBER05:9
for a, b, c, d, n being Integer holds (((a + b) + c) + d) mod n = ((((a mod n) + (b mod n)) + (c mod n)) + (d mod n)) mod n
proof end;

theorem Th10: :: NUMBER05:10
for a, b, c, d, e, n being Integer holds ((((a + b) + c) + d) + e) mod n = (((((a mod n) + (b mod n)) + (c mod n)) + (d mod n)) + (e mod n)) mod n
proof end;

:: Problem 32
theorem :: NUMBER05:11
for a1, a2, a3, a4, a5 being Integer st 9 divides ((((a1 |^ 3) + (a2 |^ 3)) + (a3 |^ 3)) + (a4 |^ 3)) + (a5 |^ 3) holds
3 divides (((a1 * a2) * a3) * a4) * a5
proof end;

theorem :: NUMBER05:12
canceled;

Lm1: for x, y, z being Nat st x,y are_coprime & (x |^ 2) + (y |^ 2) = z |^ 4 & x is odd holds
7 divides x * y
proof end;

:: Problem 33 a
theorem :: NUMBER05:13
for x, y, z being Nat st x,y are_coprime & (x |^ 2) + (y |^ 2) = z |^ 4 holds
7 divides x * y
proof end;

:: Problem 33 b
theorem :: NUMBER05:14
( not 15,20 are_coprime & (15 |^ 2) + (20 |^ 2) = 5 |^ 4 & not 7 divides 15 * 20 )
proof end;

definition
let x, y be Nat;
pred x,y satisfy_Sierpinski_problem_35 means :: NUMBER05:def 2
( x * (x + 1) divides y * (y + 1) & not x divides y & not x + 1 divides y & not x divides y + 1 & not x + 1 divides y + 1 );
end;

:: deftheorem defines satisfy_Sierpinski_problem_35 NUMBER05:def 2 :
for x, y being Nat holds
( x,y satisfy_Sierpinski_problem_35 iff ( x * (x + 1) divides y * (y + 1) & not x divides y & not x + 1 divides y & not x divides y + 1 & not x + 1 divides y + 1 ) );

theorem Th15: :: NUMBER05:15
for k, x, y being Nat st x = (36 * k) + 14 & y = ((12 * k) + 5) * ((18 * k) + 7) holds
x,y satisfy_Sierpinski_problem_35
proof end;

:: Problem 35 a
theorem :: NUMBER05:16
{ [x,y] where x, y is Nat : x,y satisfy_Sierpinski_problem_35 } is infinite
proof end;

:: Problem 35 b
theorem :: NUMBER05:17
14,35 satisfy_Sierpinski_problem_35
proof end;

:: Problem 35 c
theorem :: NUMBER05:18
for x, y being Nat holds
( not x < 14 or not y < 35 or not x,y satisfy_Sierpinski_problem_35 )
proof end;

theorem Th19: :: NUMBER05:19
for a, b, n being Nat st a divides b holds
(n |^ a) - 1 divides (n |^ b) - 1
proof end;

:: Problem 40
theorem :: NUMBER05:20
for n being Nat holds (2 |^ (2 |^ n)) + 1 divides (2 |^ ((2 |^ (2 |^ n)) + 1)) - 2
proof end;

theorem Th21: :: NUMBER05:21
for n being Nat holds
( not n divides 4 or n = 1 or n = 2 or n = 4 )
proof end;

:: Problem 47
theorem :: NUMBER05:22
for n being Nat st n > 6 holds
ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )
proof end;

definition
let n be Nat;
pred n satisfies_Sierpinski_problem_76a means :: NUMBER05:def 3
 for x being Nat st n < x & x < n + 10 holds
not x is prime ;
end;

:: deftheorem defines satisfies_Sierpinski_problem_76a NUMBER05:def 3 :
for n being Nat holds
( n satisfies_Sierpinski_problem_76a iff for x being Nat st n < x & x < n + 10 holds
not x is prime );

definition
let m be Nat;
pred m satisfies_Sierpinski_problem_76b means :: NUMBER05:def 4
 for x being Nat st 10 * m < x & x < 10 * (m + 1) holds
not x is prime ;
end;

:: deftheorem defines satisfies_Sierpinski_problem_76b NUMBER05:def 4 :
for m being Nat holds
( m satisfies_Sierpinski_problem_76b iff for x being Nat st 10 * m < x & x < 10 * (m + 1) holds
not x is prime );

theorem :: NUMBER05:23
113 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:24
114 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:25
115 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:26
116 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:27
117 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:28
139 satisfies_Sierpinski_problem_76a
proof end;

theorem :: NUMBER05:29
181 satisfies_Sierpinski_problem_76a
proof end;

:: Problem 76 a
theorem :: NUMBER05:30
for n being Nat st n satisfies_Sierpinski_problem_76a & n <= 181 holds
n in {113,114,115,116,117,139,181}
proof end;

theorem :: NUMBER05:31
20 satisfies_Sierpinski_problem_76b
proof end;

theorem :: NUMBER05:32
32 satisfies_Sierpinski_problem_76b
proof end;

theorem :: NUMBER05:33
51 satisfies_Sierpinski_problem_76b
proof end;

theorem :: NUMBER05:34
53 satisfies_Sierpinski_problem_76b
proof end;

theorem :: NUMBER05:35
62 satisfies_Sierpinski_problem_76b
proof end;

:: Problem 76 b
theorem :: NUMBER05:36
for m being Nat st m satisfies_Sierpinski_problem_76b & m <= 62 holds
m in {20,32,51,53,62}
proof end;

theorem Th33: :: NUMBER05:37
for a, b, c being Nat st c <> 0 & c < b holds
not ((a * b) + c) / b is integer
proof end;

Lm2: not 5 / 4 is integer
proof end;

theorem Th34: :: NUMBER05:38
for m, n being positive Nat holds not (m ^2) - (n ^2) = 1
proof end;

theorem Th35: :: NUMBER05:39
for m, n being positive Nat holds not (m ^2) - (n ^2) = 4
proof end;

theorem Th36: :: NUMBER05:40
for n being Nat holds (((2 * n) + 1) ^2) mod 8 = 1
proof end;

theorem Th37: :: NUMBER05:41
for n being Nat st n is odd holds
(n ^2) mod 8 = 1
proof end;

Lm3: for p being Prime st p is odd holds
3 <= p
proof end;

Lm4: for p being Prime st p is odd holds
9 <= p ^2
proof end;

theorem Th38: :: NUMBER05:42
for q, s, t being Prime holds
( not q ^2 = (s ^2) + (t ^2) or ( s is even & t is odd ) or ( s is odd & t is even ) )
proof end;

theorem Th39: :: NUMBER05:43
for q, s, t being Prime holds not q ^2 = (s ^2) + (t ^2)
proof end;

theorem :: NUMBER05:44
for p, q, r, s, t being Prime holds
( not (p ^2) + (q ^2) = ((r ^2) + (s ^2)) + (t ^2) or p is even or q is even or r is even or s is even or t is even ) ;

:: Problem 79
theorem :: NUMBER05:45
for p, q, r, s, t being Prime holds not (p ^2) + (q ^2) = ((r ^2) + (s ^2)) + (t ^2)
proof end;