:: by Adam Naumowicz

::

:: Received February 26, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

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 )

( 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 )

( 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 )

( 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 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

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

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)

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))

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 :: 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

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;