:: Elementary Number Theory Problems. {P}art {I}
:: by Adam Naumowicz
::
:: Received February 26, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, ORDINAL1, CARD_1, XBOOLE_0, ARYTM_1, TARSKI,
ARYTM_3, XXREAL_0, NAT_1, RELAT_1, INT_1, INT_2, SQUARE_1, NEWTON,
COMPLEX1, FINSET_1, PBOOLE, FUNCT_1, ABIAN, EULER_1, AFINSQ_1, FINSEQ_1,
CARD_3, ORDINAL4, SEQ_1, SERIES_1, FINSEQ_5, RFINSEQ;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, XXREAL_0, INT_1, INT_2, FINSEQ_1, FINSEQ_5, SEQ_1,
SERIES_1, SQUARE_1, NEWTON, FINSET_1, RVSUM_1, RFINSEQ, PBOOLE, ABIAN,
EULER_1, AFINSQ_1, AFINSQ_2;
constructors SQUARE_1, NEWTON, NAT_D, RELSET_1, ABIAN, EULER_1, AFINSQ_2,
RVSUM_1, SERIES_1, FINSEQ_5, RFINSEQ;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, INT_1,
PYTHTRIP, WSIERP_1, FOMODEL0, ABIAN, AFINSQ_1, AFINSQ_2, VALUED_0,
FUNCT_1, RELSET_1, NEWTON02, GR_CY_1, NEWTON04, INT_6, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Problem 1
registration
cluster positive for Integer;
end;
theorem :: NUMBER01:1
for n being positive Integer holds n+1 divides n^2 + 1 iff n = 1;
theorem :: NUMBER01:2
for i,n being Integer st |.i.|=n holds i=n or i=-n;
theorem :: NUMBER01:3
for n being natural number st n divides 24 holds
n=1 or n=2 or n=3 or n=4 or n=6 or n=8 or n=12 or n=24;
theorem :: NUMBER01:4
for t being Integer st t divides 24 holds
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;
begin :: Problem 2
::x<>3 not necessary
theorem :: NUMBER01:5
for x being Integer st x-3 divides x|^3 - 3 holds
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;
begin :: Problem 3
theorem :: NUMBER01:6
{n where n is positive Integer:
5 divides 4*(n|^2) + 1 & 13 divides 4*(n|^2) + 1} is infinite;
begin :: Problem 4
theorem :: NUMBER01:7
for n being positive Integer holds 169 divides 3|^(3*n+3)-26*n-27;
begin :: Problem 5
theorem :: NUMBER01:8
for k being Nat holds 19 divides 2|^(2|^(6*k+2))+3;
begin :: Problem 6 (due to Kraitchik)
theorem :: NUMBER01:9
13 divides 2|^70 + 3|^70;
begin :: Problem 7
theorem :: NUMBER01:10
11*31*61 divides 20|^15-1;
theorem :: NUMBER01:11
for a being Integer, m being Nat holds a-1 divides a|^m - 1;
theorem :: NUMBER01:12
for a being Nat, m being positive Integer, 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;
begin :: Problem 8
theorem :: NUMBER01:13
for m being positive Integer, a being Nat st a > 1
holds ((a|^m - 1) div (a-1)) gcd (a-1) = (a-1) gcd m;
begin :: Problem 9
theorem :: NUMBER01:14
for s1,s2 being XFinSequence of NAT, 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;
theorem :: NUMBER01:15 :: NEWTON02:146 generalized for integers
for a,b be Integer, m be positive Nat holds
Sum (a,b) In_Power m = a|^m + b|^m + Sum ((((a,b) In_Power m)|m)/^1);
theorem :: NUMBER01:16
for n,k being Nat st n is odd holds n divides k|^n + (n-k)|^n;
begin :: Problem 10
theorem :: NUMBER01:17
for s being FinSequence of NAT, n being Nat st
n>1 & len s=n-1 & for i being Nat st i in dom s holds s.i=i|^n
holds n is odd implies n divides Sum s;