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