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

registration

cluster V19() V20() integer ext-real positive for object ;

existence
ex b₁ being Integer st b₁ 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;