:: 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; definitions TARSKI; equalities ORDINAL1, SQUARE_1, FINSEQ_1; theorems INT_1, INT_2, INT_5, XREAL_1, XXREAL_0, NEWTON03, ABSVALUE, TARSKI, NEWTON, WSIERP_1, FINSET_1, FUNCT_1, PARTFUN1, PYTHTRIP, NAT_1, NEWTON01, GR_CY_3, POLYFORM, NAT_5, INT_6, EULER_2, NAT_4, EULER_1, NAT_6, NUMERAL2, PEPIN, PREPOWER, RELAT_1, AFINSQ_1, AFINSQ_2, RING_3, XCMPLX_1, RVSUM_4, SERIES_2, MEMBERED, POLYNOM3, FINSEQ_5, ENTROPY1, FINSEQ_1, VALUED_1, ORDINAL1, NEWTON04, NEWTON02, POWER, NAT_3, RFINSEQ; schemes PBOOLE, NAT_1, AFINSQ_1, SEQ_1; begin :: Problem 1 registration cluster positive for Integer; existence proof take 1; thus thesis; end; end; theorem for n being positive Integer holds n+1 divides n^2 + 1 iff n = 1 proof let n be positive Integer; thus n+1 divides n^2 + 1 implies n = 1 proof assume n+1 divides n^2 + 1; then n: n+1 divides n*(n+1)-(n-1); n+1 divides n*(n+1) by INT_1:def 3; then n1: n+1 divides n-1 by n,INT_5:2; assume o: n<>1; n >= 0+1 by INT_1:7; then n > 1 by o,XXREAL_0:1; then n-1 > 1-1 by XREAL_1:9; then n+1 <= n-1 by n1,INT_2:27; then n+1-n <= n-1-n by XREAL_1:9; hence contradiction; end; assume n=1; hence n+1 divides n^2 + 1; end; theorem lemmod: for i,n being Integer st |.i.|=n holds i=n or i=-n proof let i,n be Integer; assume |.i.| = n & i<>n; then n=-i by ABSVALUE:def 1; hence i=-n; end; theorem lem24nat: 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 proof let n be natural number; assume n: n divides 24; then n <= 24 by INT_2:27; then el: n=0 or...or n=24; n0: not 0 divides 24 by INT_2:3; 5*4 < 24 < 5*(4+1); then n5: not 5 divides 24 by NEWTON03:40; 7*3 < 24 < 7*(3+1); then n7: not 7 divides 24 by NEWTON03:40; 9*2 < 24 < 9*(2+1); then n9: not 9 divides 24 by NEWTON03:40; 10*2 < 24 < 10*(2+1); then n10: not 10 divides 24 by NEWTON03:40; 11*2 < 24 < 11*(2+1); then n11: not 11 divides 24 by NEWTON03:40; 13*1 < 24 < 13*(1+1); then n13: not 13 divides 24 by NEWTON03:40; 14*1 < 24 < 14*(1+1); then n14: not 14 divides 24 by NEWTON03:40; 15*1 < 24 < 15*(1+1); then n15: not 15 divides 24 by NEWTON03:40; 16*1 < 24 < 16*(1+1); then n16: not 16 divides 24 by NEWTON03:40; 17*1 < 24 < 17*(1+1); then n17: not 17 divides 24 by NEWTON03:40; 18*1 < 24 < 18*(1+1); then n18: not 18 divides 24 by NEWTON03:40; 19*1 < 24 < 19*(1+1); then n19: not 19 divides 24 by NEWTON03:40; 20*1 < 24 < 20*(1+1); then n20: not 20 divides 24 by NEWTON03:40; 21*1 < 24 < 21*(1+1); then n21: not 21 divides 24 by NEWTON03:40; 22*1 < 24 < 22*(1+1); then n22: not 22 divides 24 by NEWTON03:40; 23*1 < 24 < 23*(1+1); then not 23 divides 24 by NEWTON03:40; hence n=1 or n=2 or n=3 or n=4 or n=6 or n=8 or n=12 or n=24 by n,el,n0,n5,n7,n9,n10,n11,n13,n14,n15,n16,n17,n18,n19,n20,n21,n22; end; theorem lem24: 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 proof let t be Integer; reconsider n=|.t.| as Nat; assume t divides 24; then n divides |.24.| by INT_2:16; then n divides 24; then n=1 or n=2 or n=3 or n=4 or n=6 or n=8 or n=12 or n=24 by lem24nat; hence 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 by lemmod; end; begin :: Problem 2 ::x<>3 not necessary theorem 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 proof let x be Integer; assume x: x-3 divides x|^3 - 3; set t=x-3; e: (t+3)|^(2+1) - 3 = ((t+3)|^(1+1))*(t+3) - 3 by NEWTON:6 .= (((t+3)|^1)*(t+3))*(t+3) - 3 by NEWTON:6 .= (t+3)*(t+3)*(t+3) - 3 by NEWTON:5 .= ((t*t*t)+(27*t)+(9*t*t))+24; t: t divides t*t*t & t divides 27*t & t divides 9*t*t by INT_1:def 3; then t divides (t*t*t)+(27*t) by WSIERP_1:4; then t divides ((t*t*t)+(27*t)+(9*t*t)) by t,WSIERP_1:4; then t divides 24 by x,e,INT_2:1; then 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 by lem24; hence 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; end; begin :: Problem 3 theorem {n where n is positive Integer: 5 divides 4*(n|^2) + 1 & 13 divides 4*(n|^2) + 1} is infinite proof set S={n where n is positive Integer: 5 divides 4*n|^2 + 1 & 13 divides 4*n|^2 + 1}; deffunc F(Nat) = 65*$1+56; consider f being ManySortedSet of NAT such that f: for n being Element of NAT holds f.n=F(n) from PBOOLE:sch 5; set R = rng f; d: dom f = NAT by PARTFUN1:def 2; rs: R c= S proof let a be object; assume a in R; then consider k being object such that k: k in dom f & a=f.k by FUNCT_1:def 3; reconsider k as Element of NAT by d,k; a: a=65*k+56 by f,k; then reconsider n=a as positive Integer; c: 4*(n|^(1+1)) + 1 = 4*((n|^(1))*n)+1 by NEWTON:6 .= 4*(n*n) + 1 by NEWTON:5; 65=5*13; then p: 13 divides 65-0 by INT_1:def 3; 65*k+56-1 = 5*(13*k+11); then 5 divides 65*k+56-1 by INT_1:def 3; then n,1 are_congruent_mod 5 by a,INT_1:def 4; then n*n,1*1 are_congruent_mod 5 & 4,4 are_congruent_mod 5 by INT_1:18,11; then 4*(n*n),1*4 are_congruent_mod 5 & 1,1 are_congruent_mod 5 by INT_1:18,11; then 4*(n*n)+1,4+1 are_congruent_mod 5 & 5,0 are_congruent_mod 5 by INT_1:16,12; then 4*(n*n)+1,0 are_congruent_mod 5 by INT_1:15; then 4*n|^2 + 1,0 are_congruent_mod 5 by c; then d1: 5 divides (4*n|^2 + 1) - 0 by INT_1:def 4; 65*k+56-4 = 13*(5*k+4); then 13 divides 65*k+56-4 by INT_1:def 3; then n,4 are_congruent_mod 13 by a,INT_1:def 4; then n*n,4*4 are_congruent_mod 13 & 4,4 are_congruent_mod 13 by INT_1:18,11; then 4*(n*n),4*4*4 are_congruent_mod 13 & 1,1 are_congruent_mod 13 by INT_1:18,11; then 4*(n*n)+1,64+1 are_congruent_mod 13 & 65,0 are_congruent_mod 13 by INT_1:16,def 4,p; then 4*(n*n)+1,0 are_congruent_mod 13 by INT_1:15; then 4*n|^2 + 1,0 are_congruent_mod 13 by c; then 13 divides (4*n|^2 + 1) - 0 by INT_1:def 4; hence a in S by d1; end; for m being Element of NAT ex n being Element of NAT st n >= m & n in R proof let m be Element of NAT; take n=F(m); 65*m >= 1*m by XREAL_1:66; hence n >= m by XREAL_1:38; m in dom f by d; then f.m in rng f by FUNCT_1:3; hence n in R by f; end; then R is infinite by PYTHTRIP:9; hence thesis by rs,FINSET_1:1; end; begin :: Problem 4 theorem for n being positive Integer holds 169 divides 3|^(3*n+3)-26*n-27 proof let n be positive Integer; reconsider k=n as Nat by TARSKI:1; defpred P[Nat] means 169 divides 3|^(3*$1+3)-26*$1-27; tt: 3|^(2+1) = 3|^(1+1)*3 by NEWTON:6 .= 3|^(0+1)*3*3 by NEWTON:6 .= 3*3*3 by NEWTON:5; 3|^(3*1+3)-26*1-27 = 3|^(5+1)-53 .= 3|^(4+1)*3 - 53 by NEWTON:6 .= 3|^(3+1)*3*3 - 53 by NEWTON:6 .= 3|^(2+1)*3*3*3 - 53 by NEWTON:6 .= 169*4 by tt; then o: P[1] by INT_1:def 3; i: now let n be Nat; assume n: 1 <= n & P[n]; d: 13 divides 13*2 by INT_1:def 3; e: 3|^(3*(n+1)+3)-26*(n+1)-27 - (3|^(3*n+3)-26*n-27) = (3|^3)*3|^(3*n+3)-26*(n+1)-27 - (3|^(3*n+3)-26*n-27) by NEWTON:8 .= 26*(3|^(3*n+3)-1) by tt; 3|^(2+1) - 1 = 3|^(1+1)*3 - 1 by NEWTON:6 .= 3|^(0+1)*3*3 - 1 by NEWTON:6 .= 3*3*3 - 1 by NEWTON:5; then 3|^3-1 = 13*2; then t: 13 divides 3|^3-1 by INT_1:def 3; 3|^(3*(n+1)) - 1 = (3|^3)|^(n+1) - 1 by NEWTON:9 .= (3|^3)|^(n+1) - 1|^(n+1) by NEWTON:10; then 3|^3 - 1 divides 3|^(3*n+3) - 1 by NEWTON01:33; then 13 divides 3|^(3*n+3) - 1 by t,INT_2:9; then 13*13 divides 3|^(3*(n+1)+3)-26*(n+1)-27 - (3|^(3*(n+1))-26*n-27) by d,e,NEWTON03:5; then 169 divides -(3|^(3*(n+1)+3)-26*(n+1)-27 - (3|^(3*n+3)-26*n-27)) by INT_2:10; then 169 divides (3|^(3*n+3)-26*n-27) - (3|^(3*(n+1)+3)-26*(n+1)-27); then 169 divides 3|^(3*(n+1)+3)-26*(n+1)-27 by n,INT_5:2; hence P[n+1]; end; for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(o,i); then P[k] by NAT_1:14; hence thesis; end; begin :: Problem 5 theorem for k being Nat holds 19 divides 2|^(2|^(6*k+2))+3 proof let k be Nat; 2|^1 = 2 by NEWTON:5; then d2: 2|^(1+1) = 2*2 by NEWTON:6; then 2|^(2+1) = 2*4 by NEWTON:6; then d4: 2|^(3+1) = 2*8 by NEWTON:6; then 2|^(4+1) = 2*16 by NEWTON:6; then d6: 2|^(5+1) = 2*32 by NEWTON:6; 64-1=9*7; then 9 divides 2|^6 - 1 by d6,INT_1:def 3; then 2|^6,1 are_congruent_mod 9 by INT_1:def 4; then (2|^6)|^k,1|^k are_congruent_mod 9 by GR_CY_3:34; then 2|^(6*k),1|^k are_congruent_mod 9 by NEWTON:9; then a: 2|^(6*k),1 are_congruent_mod 9 by NEWTON:10; 2|^2,2|^2 are_congruent_mod 9 by INT_1:11; then (2|^(6*k))*(2|^2),1*(2|^2) are_congruent_mod 9 by a,INT_1:18; then c9: 2|^(6*k+2),2|^2 are_congruent_mod 9 by NEWTON:8; 2|^(6*k+1+1) = 2*2|^(6*k+1) & 2|^(1+1) = 2*2|^1 by NEWTON:6; then 2|^(6*k+2),0 are_congruent_mod 2 & 2|^2,0 are_congruent_mod 2 by INT_1:60; then 2|^(6*k+2),0 are_congruent_mod 2 & 0,2|^2 are_congruent_mod 2 by INT_1:14; then c2: 2|^(6*k+2),2|^2 are_congruent_mod 2 by INT_1:15; 3 is odd by POLYFORM:6; then 3*3 is odd; then 2|^1,9 are_coprime by NAT_5:3; then 2,9 are_coprime by NEWTON:5; then 2|^(6*k+2),2|^2 are_congruent_mod 2*9 by c2,c9,INT_6:21; then consider t being Integer such that t: 2|^(6*k+2) - 2|^2 = 18*t by INT_1:def 5; t1: 2|^(6*k+2) = 18*t + 2|^2 by t .= 18*t + 4 by d2; 6*k+2 >= 0+2 by XREAL_1:7; then 2|^(6*k+2) >= 2|^2 by NAT_6:1; then 18*t >= 0 & 18>0 by t,XREAL_1:48; then t >= 0 by XREAL_1:132; then t in NAT by INT_1:3; then reconsider t as Nat; dz: 19 is prime by NAT_4:29; 2 is prime by INT_2:28; then 2,19 are_coprime by dz,INT_2:30; then (2 |^ Euler 19) mod 19 = 1 & 18=19-1 by EULER_2:18; :: by Fermat's little theorem then (2 |^ 18) mod 19 = 1 by EULER_1:20,dz; then 2|^18,1 are_congruent_mod 19 by NAT_6:10; then (2|^18)|^t,1|^t are_congruent_mod 19 by GR_CY_3:34; then 2|^(18*t),1|^t are_congruent_mod 19 by NEWTON:9; then 2|^(18*t),1 are_congruent_mod 19 & 2|^4,2|^4 are_congruent_mod 19 by NEWTON:10,INT_1:11; then 2|^(18*t)*(2|^4),1*(2|^4) are_congruent_mod 19 by INT_1:18; then 2|^(18*t+4),2|^4 are_congruent_mod 19 by NEWTON:8; then 2|^(2|^(6*k+2)),2|^4 are_congruent_mod 19 & 3,3 are_congruent_mod 19 by t1,INT_1:11; then 2|^(2|^(6*k+2))+3,2|^4+3 are_congruent_mod 19 by INT_1:16; then 2|^(2|^(6*k+2))+3,19 are_congruent_mod 19 & 19,0 are_congruent_mod 19 by d4,INT_1:12; then 2|^(2|^(6*k+2))+3,0 are_congruent_mod 19 by INT_1:15; then 19 divides 2|^(2|^(6*k+2))+3-0 by INT_1:def 4; hence thesis; end; begin :: Problem 6 (due to Kraitchik) theorem 13 divides 2|^70 + 3|^70 proof dp: 2 is prime by INT_2:28; tp: 13 is prime by NAT_4:28; then 2,13 are_coprime by dp,INT_2:30; then 2 |^ Euler 13 mod 13 = 1 & 12=13-1 by EULER_2:18; :: by Fermat's little theorem then (2 |^ 12) mod 13 = 1 by EULER_1:20,tp; then 2|^12,1 are_congruent_mod 13 by NAT_6:10; then (2|^12)|^5,1|^5 are_congruent_mod 13 by GR_CY_3:34; then 2|^(12*5),1|^5 are_congruent_mod 13 by NEWTON:9; then ds: 2|^60,1 are_congruent_mod 13 by NEWTON:10; 2|^1 = 2 by NEWTON:5; then 2|^(1+1) = 2*2 by NEWTON:6; then 2|^(2+1) = 2*4 by NEWTON:6; then 2|^(3+1) = 2*8 by NEWTON:6; then 2|^(4+1) = 2*16 by NEWTON:6; then 2|^5-6=13*2; then 2|^5,6 are_congruent_mod 13 by INT_1:def 5; then (2|^5)|^2,6|^2 are_congruent_mod 13 by GR_CY_3:34; then 2|^(5*2),6|^2 are_congruent_mod 13 by NEWTON:9; then ts: 2|^(5*2),6*6 are_congruent_mod 13 by WSIERP_1:1; 36 - -3 = 13*3; then 36,-3 are_congruent_mod 13 by INT_1:def 5; then 2|^10,-3 are_congruent_mod 13 by ts,INT_1:15; then (2|^60)*(2|^10),1*(-3) are_congruent_mod 13 by ds,INT_1:18; then dsi: 2|^(60+10),-3 are_congruent_mod 13 by NEWTON:8; 3|^(2+1)=3|^2*3 by NEWTON:6 .= 3*3*3 by WSIERP_1:1 .= 2*13+1; then 3|^3-1 = 2*13; then 3|^3,1 are_congruent_mod 13 by INT_1:def 5; then (3|^3)|^23,1|^23 are_congruent_mod 13 by GR_CY_3:34; then 3|^(3*23),1|^23 are_congruent_mod 13 by NEWTON:9; then 3|^69,1 are_congruent_mod 13 & 3,3 are_congruent_mod 13 by NEWTON:10,INT_1:11; then (3|^69)*3,1*3 are_congruent_mod 13 by INT_1:18; then 3|^(69+1),1*3 are_congruent_mod 13 by NEWTON:6; then 2|^70 + 3|^70,-3+3 are_congruent_mod 13 by dsi,INT_1:16; then 13 divides 2|^70 + 3|^70 - 0 by INT_1:def 4; hence thesis; end; begin :: Problem 7 theorem 11*31*61 divides 20|^15-1 proof 20|^15 >= 1|^15 by PREPOWER:9; then 20|^15 >= 1 by NEWTON:10; then 20|^15-1 >= 1-1 by XREAL_1:9; then 20|^15-1 in NAT by INT_1:3; then reconsider D=20|^15-1 as Nat; jp: 11 is prime by NAT_4:27; tp: 31 is prime by NUMERAL2:24; sp: 61 is prime by NUMERAL2:29; jtc: 11,31 are_coprime by jp,tp,INT_2:30; cp1: 11,61 are_coprime by jp,sp,INT_2:30; cp2: 31,61 are_coprime by tp,sp,INT_2:30; jsc: 11*31,61 are_coprime by cp1,cp2,EULER_1:14; 2|^1 = 2 by NEWTON:5; then 2|^(1+1) = 2*2 by NEWTON:6; then 2|^(2+1) = 2*4 by NEWTON:6; then 2|^(3+1) = 2*8 by NEWTON:6; then dc: 2|^(4+1) = 2*16 & 3*11 = 32 - -1 by NEWTON:6; then dp: 2|^5,-1 are_congruent_mod 11 by INT_1:def 5; 5=2*2+1; then po: 5 is odd; reconsider J=-1 as Integer; 11*1=10 - -1; then 10,-1 are_congruent_mod 11 by INT_1:def 5; then 10|^5,(-1)|^5 are_congruent_mod 11 by GR_CY_3:34; then 10|^5,-1 are_congruent_mod 11 by po,POLYFORM:9; then (2|^5)*(10|^5),J*J are_congruent_mod 11 by dp,INT_1:18; then (2*10)|^5,1 are_congruent_mod 11 by NEWTON:7; then (20|^5)|^3,1|^3 are_congruent_mod 11 by GR_CY_3:34; then 20|^(5*3),1|^3 are_congruent_mod 11 by NEWTON:9; then 20|^15,1 are_congruent_mod 11 by NEWTON:10; then jd: 11 divides D by INT_1:def 4; 31*4=121 - -3; then sd: 121,-3 are_congruent_mod 31 by INT_1:def 5; 31*1 = 33 - 2; then tt: 33,2 are_congruent_mod 31 by INT_1:def 5; 31*1=20 - -11; then dw: 20,-11 are_congruent_mod 31 by INT_1:def 5; then 20|^2,(-11)|^2 are_congruent_mod 31 by GR_CY_3:34; then 20|^2,(-11)*(-11) are_congruent_mod 31 by WSIERP_1:1; then 20|^2,-3 are_congruent_mod 31 by sd,INT_1:15; then 20*(20|^2),(-11)*(-3) are_congruent_mod 31 by dw,INT_1:18; then 20|^(2+1),33 are_congruent_mod 31 by NEWTON:6; then 20|^3,2 are_congruent_mod 31 by tt,INT_1:15; then (20|^3)|^5,2|^5 are_congruent_mod 31 by GR_CY_3:34; then dwp: 20|^(3*5),2|^5 are_congruent_mod 31 by NEWTON:9; 31*1=(2|^5) - 1 by dc; then 2|^5,1 are_congruent_mod 31 by INT_1:def 5; then 20|^15,1 are_congruent_mod 31 by dwp,INT_1:15; then 31 divides D by INT_1:def 4; then jtd: 11*31 divides D by jd,jtc,PEPIN:4; 3|^(2+2) = (3|^2)*(3|^2) by NEWTON:8 .= (3*3)*(3|^2) by WSIERP_1:1 .= (3*3)*(3*3) by WSIERP_1:1; then 61*1=(3|^4) - 20; then 3|^4,20 are_congruent_mod 61 by INT_1:def 5; then (3|^4)|^15,20|^15 are_congruent_mod 61 by GR_CY_3:34; then 3|^(4*15),20|^15 are_congruent_mod 61 by NEWTON:9; then f: 20|^15,3|^60 are_congruent_mod 61 by INT_1:14; 3,61 are_coprime by sp,PEPIN:41,INT_2:30; then 3|^(Euler 61) mod 61 = 1 & 60=61-1 by EULER_2:18; :: by Fermat's little theorem then (3 |^ 60) mod 61 = 1 by EULER_1:20,sp; then 3|^60,1 are_congruent_mod 61 by NAT_6:10; then 20|^15,1 are_congruent_mod 61 by f,INT_1:15; then 61 divides D by INT_1:def 4; then 11*31*61 divides D by jsc,jtd,PEPIN:4; hence thesis; end; theorem lemdiv: for a being Integer, m being Nat holds a-1 divides a|^m - 1 proof let a be Integer, m be Nat; defpred P[Nat] means a-1 divides a|^$1 - 1; a|^0 - 1 = 1-1 by NEWTON:4; then z: P[0] by INT_2:12; i: now let k be Nat; assume P[k]; then consider l being Integer such that l: a|^k-1=(a-1)*l by INT_1:def 3; a|^(k+1)-1 = a|^k*a-1 by NEWTON:6 .= (a-1)*(a|^k+l) by l; hence P[k+1] by INT_1:def 3; end; for k being Nat holds P[k] from NAT_1:sch 2(z,i); hence thesis; end; theorem lempowers: 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 proof let a be Nat, m be positive Integer, f be XFinSequence of INT such that f: a>1 & len f = m-1 & for i being Nat st i in dom f holds f.i=a|^(i+1)-1; a: a-1<>0 by f; reconsider a1=a-1 as Nat by f,INT_1:74; m>=0+1 by INT_1:7; then reconsider m0=m as Nat by POLYFORM:3; reconsider m1=m0-1 as Nat by INT_1:74; defpred P[Nat] means for f being XFinSequence of INT st len f = $1 & for i being Nat st i in dom f holds f.i=a|^(i+1)-1 holds (a|^($1+1) - 1) div (a-1) = Sum f + ($1+1); z: P[0] proof let f0 be XFinSequence of INT such that f0: len f0 = 0 & for i being Nat st i in dom f0 holds f0.i=a|^(i+1)-1; f0={} by f0; then sz: Sum f0=0; thus (a|^(0+1) - 1) div (a-1) = (a-1) div (a-1) by NEWTON:5 .= Sum f0 + (0+1) by sz,a,INT_1:49; end; k: now let k be Nat; assume pk: P[k]; thus P[k+1] proof let f1 be XFinSequence of INT such that f1: len f1 = k+1 & for i being Nat st i in dom f1 holds f1.i=a|^(i+1)-1; set fk=f1|k; km: k < k+1 by NAT_1:13; then df: dom fk=k by f1,AFINSQ_1:11; k in Segm (k+1) & dom f1 = k+1 by f1,km,NAT_1:44; then kd: k in dom f1; lek: len fk=k by km,f1,AFINSQ_1:54; now let i be Nat; assume idk: i in dom fk; dom fk c= dom f1 by RELAT_1:60; then idf: i in dom f1 by idk; thus fk.i=f1.i by df,km,idk,f1,AFINSQ_1:53 .= a|^(i+1)-1 by f1,idf; end; then pek: (a|^(k+1) - 1) div (a-1) = Sum fk + (k+1) by pk,lek; sf: Sum <% f1.k %>=f1.k by AFINSQ_2:53; f1=fk^<% f1.k %> by f1,AFINSQ_1:56; then ss: Sum f1 = Sum fk + f1.k by sf,AFINSQ_2:55; ld: a-1 divides a|^((k+1)+1) - 1 & a-1 divides a|^(k+1) - 1 by lemdiv; hence (a|^((k+1)+1) - 1) div (a-1) = (a|^((k+1)+1) - 1) / a1 by RING_3:6 .= (a|^((k+1))*a + a|^(k+1) - a|^(k+1) - 1) / a1 by NEWTON:6 .= (a|^((k+1))*(a-1) + (a|^(k+1) - 1)) / a1 .= (a|^((k+1))*(a-1))/a1 + (a|^(k+1) - 1) / a1 by XCMPLX_1:62 .= a|^(k+1) + ((a|^(k+1) - 1) / a1) by a,XCMPLX_1:89 .= a|^(k+1) + ((a|^(k+1) - 1) div a1) by ld,RING_3:6 .= (a|^(k+1) - 1) + Sum fk + ((k+1)+1) by pek .= f1.k + Sum fk + ((k+1)+1) by f1,kd .= Sum f1 + ((k+1)+1) by ss; end; end; for k being Nat holds P[k] from NAT_1:sch 2(z,k); then (a|^(m1+1) - 1) div (a-1) = Sum f + (m1+1) by f; hence (a|^m - 1) div (a-1) = Sum f + m; end; begin :: Problem 8 theorem 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 proof let m be positive Integer, a be Nat such that a: a > 1; set d=((a|^m - 1) div (a-1)) gcd (a-1); set d1=(a-1) gcd m; m>=0+1 by INT_1:7; then reconsider m0=m as Nat by POLYFORM:3; reconsider m1=m0-1 as Nat by INT_1:74; deffunc F(Nat) = a|^($1+1)-1; consider f being XFinSequence such that f: len f = m1 & for i being Nat st i in m1 holds f.i=F(i) from AFINSQ_1:sch 2; rng f c= INT proof let o be object; assume o in rng f; then consider x being object such that x: x in dom f & o=f.x by FUNCT_1:def 3; reconsider x as Nat by x; o=a|^(x+1)-1 by f,x; hence o in INT by INT_1:def 2; end; then reconsider f as XFinSequence of INT by RELAT_1:def 19; d2: d divides a-1 & d divides (a|^m - 1) div (a-1) by INT_2:def 2; now let i be Nat; assume i in dom f; then f.i=a|^(i+1)-1 by f; hence a-1 divides f.i by lemdiv; end; then ad: a-1 divides Sum f by NUMERAL2:16; then ds: d divides Sum f by d2,INT_2:9; ss: (a|^m - 1) div (a-1) = Sum f + m by a,f,lempowers; then d divides Sum f + m by d2; then d1: d divides m by ds,INT_2:1; now let q be Integer; assume q: q divides a-1 & q divides m; then q divides Sum f by ad,INT_2:9; then q divides (a|^m - 1) div (a-1) by ss,q,WSIERP_1:4; hence q divides d by q,INT_2:def 2; end; hence d = d1 by d1,d2,INT_2:def 2; end; begin :: Problem 9 theorem 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 proof let s1,s2 be XFinSequence of NAT, n be Nat; assume that s1: len s1=n+1 & for i being Nat st i in dom s1 holds s1.i=i|^5 and s2: len s2=n+1 & for i being Nat st i in dom s2 holds s2.i=i|^3; deffunc F(Nat) = $1|^3; consider S2 being Real_Sequence such that S2: for i being Nat holds S2.i=F(i) from SEQ_1:sch 1; Segm(n+1) c= NAT & dom S2=NAT by MEMBERED:6,PARTFUN1:def 2; then dom (S2|Segm(n+1)) = Segm(n+1) by RELAT_1:62; then dr: dom (S2|Segm(n+1)) = dom s2 by s2; now let o be object; assume o: o in dom s2; then o in Segm(n+1) by s2; then o is natural by MEMBERED:def 6; then reconsider on=o as Nat by TARSKI:1; thus s2.o=on|^3 by s2,o .= S2.on by S2 .= (S2|Segm(n+1)).o by o,dr,FUNCT_1:47; end; then s2=S2|Segm(n+1) by dr,FUNCT_1:2; then Sum s2=Partial_Sums(S2).n by RVSUM_4:4; then ss: Sum s2 = n|^2*(n+1)|^2/4 by S2,SERIES_2:15; deffunc G(Nat) = $1|^5; consider S1 being Real_Sequence such that S1: for i being Nat holds S1.i=G(i) from SEQ_1:sch 1; Segm(n+1) c= NAT & dom S1=NAT by MEMBERED:6,PARTFUN1:def 2; then dom (S1|Segm(n+1)) = Segm(n+1) by RELAT_1:62; then ds: dom (S1|Segm(n+1)) = dom s1 by s1; now let o be object; assume o: o in dom s1; then o in Segm(n+1) by s1; then o is natural by MEMBERED:def 6; then reconsider on=o as Nat by TARSKI:1; thus s1.o=on|^5 by s1,o .= S1.on by S1 .= (S1|Segm(n+1)).o by o,ds,FUNCT_1:47; end; then s1=S1|Segm(n+1) by ds,FUNCT_1:2; then Sum s1=Partial_Sums(S1).n by RVSUM_4:4; then Sum s1 = n|^2*(n+1)|^2*(2*n|^2+2*n-1)/12 by S1,SERIES_2:19; then 3*Sum s1 = (2*n|^2+2*n-1)*Sum s2 by ss; hence Sum s2 divides 3*Sum s1 by INT_1:def 3; end; theorem lemman02: :: 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) proof let a,b be Integer; let m be positive Nat; len ((a,b) In_Power m) = m + 1 by NEWTON:def 4; then Sum ((a,b) In_Power m) = Sum(((a,b) In_Power m)|m/^1) + ((a,b) In_Power m).1 + ((a,b) In_Power m).(m+1) by NEWTON02:115 .= Sum(((a,b) In_Power m)|m/^1) + a|^m + ((a,b) In_Power m).(m+1) by NEWTON:28 .= Sum(((a,b) In_Power m)|m/^1) + a|^m + b|^m by NEWTON:29; hence thesis; end; theorem lemmandiv: for n,k being Nat st n is odd holds n divides k|^n + (n-k)|^n proof let n,k be Nat; assume no: n is odd; then reconsider p=n as positive Nat; kk: k|^p + (p+(-k))|^p = k|^p + Sum((p,-k) In_Power p) by NEWTON:30 .= k|^p + (p|^p + (-k)|^p + Sum((((p,-k) In_Power p)|p)/^1)) by lemman02 .= k|^p + (p|^p + - k|^p + Sum((((p,-k) In_Power p)|p)/^1)) by no,POWER:2 .= p|^p + Sum((((p,-k) In_Power p)|p)/^1); pp: p divides p|^p by NAT_3:3; reconsider S=Sum((((p,-k) In_Power p)|p)/^1) as Integer; reconsider f=(((p,-k) In_Power p)|p)/^1 as INT-valued FinSequence; now let o be Nat; assume o: o in dom f; then f <> {}; then 1<=len (((p,-k) In_Power p)|p) by RFINSEQ:def 1; then rf: len f = len (((p,-k) In_Power p)|p)-1 & for l be Nat st l in dom f holds f.l = (((p,-k) In_Power p)|p).(l+1) by RFINSEQ:def 1; elen: len ((p,-k) In_Power p) = n+1 & for i,l,m being Nat st i in dom ((p,-k) In_Power p) & m = i - 1 & l = n-m holds ((p,-k) In_Power p).i = (n choose m) * p|^l * (-k)|^m by NEWTON:def 4; x: 0+1<=o+1 by XREAL_1:6; pz: p+0<=n+1 by XREAL_1:6; len (((p,-k) In_Power p)|p) = p by elen,pz,FINSEQ_1:17; then lp: len f = p-1 by rf; o in Seg len f by o,FINSEQ_1:def 3; then o <= p-1 by lp,FINSEQ_1:1; then op: o+1 <= p-1+1 by XREAL_1:6; then el: o+1 in Seg p by x; set i=o+1; i
= o+1-o by op,XREAL_1:9; then reconsider l=n-m as Nat; fo: f.o = (((p,-k) In_Power p)|p).(o+1) by o,rf .= ((p,-k) In_Power p).(o+1) by el,FUNCT_1:49 .= (n choose m) * p|^l * (-k)|^m by elen,i .= p|^l * ((n choose m) * (-k)|^m); p divides p|^l by po,NAT_3:3; hence n divides f.o by fo,INT_2:2; end; then n divides Sum f by NEWTON04:80; then n divides k|^n + (n+(-k))|^n by kk,pp,WSIERP_1:4; hence n divides k|^n + (n-k)|^n; end; begin :: Problem 10 theorem 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 proof let s be FinSequence of NAT, n be Nat such that n: n>1 & len s=n-1 and s: for i being Nat st i in dom s holds s.i=i|^n; rng s c= REAL; then reconsider s0=s as FinSequence of REAL by FINSEQ_1:def 4; reconsider ser=Sum s as Nat by TARSKI:1; d: dom s = dom Rev s by FINSEQ_5:57; d2: dom (s+Rev s) = (dom s) /\ (dom Rev s) by VALUED_1:def 1 .= dom s by d; then Seg len (s+Rev s) = dom s by FINSEQ_1:def 3 .= Seg len s by FINSEQ_1:def 3; then l1: len s0=len (s0+Rev s0) by FINSEQ_1:6; Seg len s = dom Rev s by d,FINSEQ_1:def 3; then l2: len s0=len Rev s0 by FINSEQ_1:def 3; for k being Nat st k in dom s0 holds (s0+Rev s0).k = s0.k + (Rev s0).k by d2,VALUED_1:def 1; then ss: Sum (s0+Rev s0) = Sum s0 + Sum Rev s0 by l1,l2,ENTROPY1:7 .= Sum s + Sum s by POLYNOM3:3 .= 2*Sum s; rng (s+Rev s) c= NAT proof let o be object; assume o in rng (s+Rev s); then consider a being object such that a: a in dom (s+Rev s) & o=(s+Rev s).a by FUNCT_1:def 3; reconsider a as Nat by a; o=s.a+(Rev s).a by a,VALUED_1:def 1; hence o in NAT by ORDINAL1:def 12; end; then reconsider sr=s+Rev s as FinSequence of NAT by FINSEQ_1:def 4; thus n is odd implies n divides Sum s proof assume no: n is odd; 2|^1=2 by NEWTON:5; then 2c: 2,n are_coprime by NAT_5:3,no; now let k be Nat; assume k: k in dom sr; then serek: sr.k = s.k + (Rev s).k by VALUED_1:def 1 .= k|^n + (Rev s).k by d2,k,s .= k|^n + s.(len s - k + 1) by FINSEQ_5:58,k,d2 .= k|^n + s.(n-k) by n; k in Seg len s by k,d2,FINSEQ_1:def 3; then kk: 1 <= k & k <= n-1 by FINSEQ_1:1,n; then nk: n-k <= n-1 by XREAL_1:10; k+(1-k) <= (n-1)+(1-k) by kk,XREAL_1:6; then jk: 1 <= n-k; then reconsider nik=n-k as Nat; nik in Seg len s by n,jk,nk; then n-k in dom s by FINSEQ_1:def 3; then sr.k = k|^n + (n-k)|^n by serek,s; hence n divides sr.k by no,lemmandiv; end; then n divides Sum (sr) by NEWTON04:80; then n divides 2*Sum s by ss; then n divides ser by 2c,EULER_1:13; hence n divides Sum s; end; end;