:: Elementary Number Theory Problems. {P}art {I}
:: by Adam Naumowicz
::
:: Received February 26, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

registration
existence
ex b1 being Integer st b1 is positive
proof end;
end;

theorem :: NUMBER01:1
for n being positive Integer holds
( n + 1 divides (n ^2) + 1 iff n = 1 )
proof end;

theorem lemmod: :: NUMBER01:2
for i, n being Integer holds
( not |.i.| = n or i = n or i = - n )
proof end;

theorem lem24nat: :: NUMBER01:3
for n being natural number holds
( not n divides 24 or n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 8 or n = 12 or n = 24 )
proof end;

theorem lem24: :: NUMBER01:4
for t being Integer holds
( not t divides 24 or t = - 1 or t = 1 or t = - 2 or t = 2 or t = - 3 or t = 3 or t = - 4 or t = 4 or t = - 6 or t = 6 or t = - 8 or t = 8 or t = - 12 or t = 12 or t = - 24 or t = 24 )
proof end;

::x<>3 not necessary
theorem :: NUMBER01:5
for x being Integer holds
( not x - 3 divides (x |^ 3) - 3 or x = - 21 or x = - 9 or x = - 5 or x = - 3 or x = - 1 or x = 0 or x = 1 or x = 2 or x = 4 or x = 5 or x = 6 or x = 7 or x = 9 or x = 11 or x = 15 or x = 27 )
proof end;

theorem :: NUMBER01:6
{ n where n is positive Integer : ( 5 divides (4 * (n |^ 2)) + 1 & 13 divides (4 * (n |^ 2)) + 1 ) } is infinite
proof end;

theorem :: NUMBER01:7
for n being positive Integer holds 169 divides ((3 |^ ((3 * n) + 3)) - (26 * n)) - 27
proof end;

theorem :: NUMBER01:8
for k being Nat holds 19 divides (2 |^ (2 |^ ((6 * k) + 2))) + 3
proof end;

theorem :: NUMBER01:9
13 divides (2 |^ 70) + (3 |^ 70)
proof end;

theorem :: NUMBER01:10
(11 * 31) * 61 divides (20 |^ 15) - 1
proof end;

theorem lemdiv: :: NUMBER01:11
for a being Integer
for m being Nat holds a - 1 divides (a |^ m) - 1
proof end;

theorem lempowers: :: NUMBER01:12
for a being Nat
for m being positive Integer
for f being XFinSequence of INT st a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) holds
((a |^ m) - 1) div (a - 1) = (Sum f) + m
proof end;

theorem :: NUMBER01:13
for m being positive Integer
for a being Nat st a > 1 holds
(((a |^ m) - 1) div (a - 1)) gcd (a - 1) = (a - 1) gcd m
proof end;

theorem :: NUMBER01:14
for s1, s2 being XFinSequence of NAT
for n being Nat st len s1 = n + 1 & ( for i being Nat st i in dom s1 holds
s1 . i = i |^ 5 ) & len s2 = n + 1 & ( for i being Nat st i in dom s2 holds
s2 . i = i |^ 3 ) holds
Sum s2 divides 3 * (Sum s1)
proof end;

theorem lemman02: :: NUMBER01:15
for a, b being Integer
for m being positive Nat holds Sum ((a,b) In_Power m) = ((a |^ m) + (b |^ m)) + (Sum ((((a,b) In_Power m) | m) /^ 1))
proof end;

theorem lemmandiv: :: NUMBER01:16
for n, k being Nat st n is odd holds
n divides (k |^ n) + ((n - k) |^ n)
proof end;

theorem :: NUMBER01:17
for s being FinSequence of NAT
for n being Nat st n > 1 & len s = n - 1 & ( for i being Nat st i in dom s holds
s . i = i |^ n ) & n is odd holds
n divides Sum s
proof end;