:: Elementary Number Theory Problems. {P}art {I}
:: by Adam Naumowicz
::
:: Received February 26, 2020
:: Copyright (c) 2020-2026 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, NAT_3, FIB_NUM2,
AFINSQ_2, VALUED_0, FUNCOP_1, MEMBERED, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS,
VALUED_0, FUNCOP_1, XCMPLX_0,
XREAL_0, NAT_1, XXREAL_0, ABSVALUE, INT_1, INT_2, NAT_D,
FINSEQ_1, SEQ_1, CARD_1, MEMBERED, SERIES_1, SQUARE_1, NEWTON, FINSET_1,
RVSUM_1, RFINSEQ, PBOOLE, ABIAN, EULER_1, AFINSQ_1, AFINSQ_2, NAT_3,
FIB_NUM2, VALUED_1;
constructors SQUARE_1, NAT_D, RELSET_1, ABIAN, EULER_1, AFINSQ_2, RVSUM_1,
SERIES_1, RFINSEQ, NAT_3, FIB_NUM2, RECDEF_1;
registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, CARD_1, INT_1,
PYTHTRIP, WSIERP_1, FOMODEL0, ABIAN, AFINSQ_1, AFINSQ_2, VALUED_0,
HILB10_2, FINSET_1, MEMBERED, FUNCT_1, RELSET_1, NEWTON02, NEWTON04,
INT_6, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities ORDINAL1, SQUARE_1, FINSEQ_1, AFINSQ_2;
theorems INT_1, INT_2, INT_5, XREAL_1, XXREAL_0, NEWTON03, ABSVALUE, TARSKI,
NEWTON, WSIERP_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, FINSEQ_1, VALUED_1, ORDINAL1, NEWTON04, NEWTON02, POWER, NAT_3,
RFINSEQ, ABIAN, NUMERAL1, CARD_1, FUNCOP_1, ZFMISC_1, XBOOLE_1, XBOOLE_0,
CARD_2, INT_8, NAT_D;
schemes PBOOLE, NAT_1, AFINSQ_1, SEQ_1, AFINSQ_2;
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;
thus thesis;
end;
theorem lemmod:
for i,n being Real st |.i.|=n holds i=n or i=-n
proof
let i,n be Real;
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 Nat ex n being Nat st n >= m & n in R
proof
let m be Nat;
take n=F(m);
65*m >= 1*m by XREAL_1:66;
hence n >= m by XREAL_1:38;
aa: m in NAT by ORDINAL1:def 12;
then m in dom f by d;
then f.m in rng f by FUNCT_1:3;
hence n in R by f,aa;
end;
then R is infinite by PYTHTRIP:9;
hence thesis by rs;
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 PARTFUN1:def 2;
then dom (S2|Segm(n+1)) = Segm(n+1);
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;
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 PARTFUN1:def 2;
then dom (S1|Segm(n+1)) = Segm(n+1);
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;
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<p+1 by NAT_1:13,op;
then i in Seg len ((p,-k) In_Power p) by x,elen;
then i: i in dom ((p,-k) In_Power p) by FINSEQ_1:def 3;
reconsider m=i-1 as Nat;
po: p-o >= 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;
theorem lemmacardeven:
for n being Nat st n is odd holds card (n /\ EvenNAT) = (n div 2) + 1
proof
0 is even; then
ze: 0 in EvenNAT by NUMERAL2:def 1;
let n be Nat;
assume n: n is odd;
defpred P[Nat] means $1 is odd implies card ($1 /\ EvenNAT) = ($1 div 2)+1;
i: for n being Nat st for k being Nat st k<n holds P[k] holds P[n]
proof
let n be Nat;
assume k: for k being Nat st k<n holds P[k];
assume nod: n is odd;
then reconsider no=n as odd Nat;
per cases;
suppose nd: n >= 2;
then n >= 1 by XXREAL_0:2;
then reconsider nj=no-1 as even Nat by NAT_1:21;
n - 1 < n-0 by XREAL_1:15;
then njz: nj < n;
nj >= 2-1 by nd,XREAL_1:9;
then reconsider nd=nj-1 as odd Nat by NAT_1:21;
n - 2 < n-0 by XREAL_1:15;
then ndz: nd < n;
then tc: card (nd /\ EvenNAT) = (nd div 2)+1 by k;
n-2 < n-1 by XREAL_1:15;
then njd: nd < nj;
reconsider X=nd/\EvenNAT as finite set;
reconsider Y=n/\EvenNAT as finite set;
reconsider Z={nd,nj}/\EvenNAT as finite set;
sen: Segm nd c= Segm n by ndz,NAT_1:39;
n=nd\/{nj,nd}
proof
thus n c= nd\/{nj,nd}
proof
let o be object;
assume o in n;
then os: o in Segm n;
then reconsider on=o as Nat;
per cases;
suppose on < nd;
then card Segm on in card Segm nd by NAT_1:41;
then on in nd;
hence o in nd\/{nj,nd} by XBOOLE_0:def 3;
end;
suppose on: on >= nd;
card Segm on in card Segm n by os;
then on < nj+1 by NAT_1:41;
then on <= nd+1 by NAT_1:13;
then on = nd or on=nj by on,NAT_1:9;
then on in {nd,nj} by TARSKI:def 2;
hence o in nd\/{nj,nd} by XBOOLE_0:def 3;
end;
end;
thus nd\/{nj,nd} c= n
proof
let o be object;
assume o in nd\/{nj,nd};
then o in nd or o in {nj,nd} by XBOOLE_0:def 3;
then per cases by TARSKI:def 2;
suppose o in nd;
hence o in n by sen;
end;
suppose on: o=nj;
card Segm nj in card Segm n by NAT_1:41,njz;
hence o in n by on;
end;
suppose on: o=nd;
card Segm nd in card Segm n by NAT_1:41,ndz;
hence o in n by on;
end;
end;
end;
then xyz: Y = X \/ Z by XBOOLE_1:23;
X /\ Z = {}
proof
thus X /\ Z c= {}
proof
let o be object;
assume o in X /\ Z;
then ox: o in X & o in Z by XBOOLE_0:def 4;
then o in {nd,nj} by XBOOLE_0:def 4;
then per cases by TARSKI:def 2;
suppose o=nd;
then nd in nd by ox,XBOOLE_0:def 4;
hence thesis;
end;
suppose o=nj;
then card Segm nj in card Segm nd by ox,XBOOLE_0:def 4;
hence thesis by njd,NAT_1:41;
end;
end;
thus {} c= X /\ Z by XBOOLE_1:2;
end;
then xmz: X misses Z by XBOOLE_0:def 7;
Z = {nj}
proof
thus Z c= {nj}
proof
let o be object;
assume o in Z;
then o in {nd,nj} & o in EvenNAT by XBOOLE_0:def 4;
then oj: (o=nd or o=nj) & o in EvenNAT by TARSKI:def 2;
then consider oj being Nat such that
ojoj: oj=o & oj is even by NUMERAL2:def 1;
o=nj by oj,ojoj;
hence o in {nj} by TARSKI:def 1;
end;
thus {nj} c= Z
proof
let o be object;
assume o in {nj};
then o=nj by TARSKI:def 1;
then o in {nd,nj} & o in EvenNAT by TARSKI:def 2,NUMERAL2:def 1;
hence o in Z by XBOOLE_0:def 4;
end;
end;
then card Z = 1 by CARD_2:42;
hence card (n /\ EvenNAT) = (nd div 2)+1 + 1 by tc,xyz,xmz,CARD_2:40
.= (nd-1)/2 +1 + 1 by NAT_6:5
.= ((no-1)/2)+1
.= (n div 2)+1 by NAT_6:5;
end;
suppose n < 2;
then j: n=1 by nod,NAT_1:23;
then n={0} by CARD_1:49;
then n /\ EvenNAT = {0} by ze,ZFMISC_1:46;
hence card (n /\ EvenNAT) = ((no-1)/2)+1 by j,CARD_1:30
.= (n div 2)+1 by NAT_6:5;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 4(i);
hence card (n /\ EvenNAT) = (n div 2)+1 by n;
end;
begin :: Problem 10
theorem
for s being XFinSequence 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+1)|^n
holds n is odd iff n divides Sum s
proof
let s be XFinSequence 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+1)|^n;
reconsider n1=n-1 as Nat by n;
d: dom s = dom Rev s by AFINSQ_2:5;
d2: dom (s+Rev s) = (dom s) /\ (dom Rev s) by VALUED_1:def 1
.= dom s by d;
reconsider ss=s as (n1)-element complex-valued XFinSequence
by n,CARD_1:def 7;
reconsider rs=Rev s as (n1)-element complex-valued XFinSequence
by n,CARD_1:def 7,d;
ss: Sum (ss+rs) = Sum s + Sum Rev s by RVSUM_4:49
.= Sum s + Sum s by AFINSQ_2:69
.= 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 XFinSequence of NAT by RELAT_1:def 19;
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+1)|^n + (Rev s).k by d2,k,s
.= (k+1)|^n + s.(len s - (k + 1)) by k,d,d2,AFINSQ_2:def 1
.= (k+1)|^n + s.(n-k-2) by n;
k < n-1 by n,AFINSQ_1:66,k,d2;
then k+2 < n-1+2 by XREAL_1:6;
then k+2 < n+1;
then k+2<=n by NAT_1:13;
then reconsider nik=n-(k+2) as Nat by NAT_1:21;
1 < k+2 by XREAL_1:40; then
nik < n-1 by XREAL_1:10;
then nik in dom s by n,AFINSQ_1:66;
then
sr.k = (k+1)|^n + (nik+1)|^n by serek,s
.= (k+1)|^n + (n-(k+1))|^n;
hence n divides sr.k by no,lemmandiv;
end;
then n divides Sum (sr) by NUMERAL1:2;
then n divides 2*Sum s by ss;
then n divides Sum s by 2c,EULER_1:13;
hence n divides Sum s;
end;
thus n divides Sum s implies n is odd
proof
assume that nd: n divides Sum s and e: n is even;
reconsider ne=n as even Nat by e;
consider n2 being Nat such that n2: n=2*n2 by ABIAN:def 2,e;
set h=2 |-count n;
2 divides n by n2,INT_1:def 3; then
h <> 0 by n,NAT_3:27; then
hen: h > 0;
then reconsider hj=h-1 as Nat by NAT_1:20;
dwah: 2 |^ h divides n by n,NAT_3:def 7; then
2n: 2 |^ h <= n by n,INT_2:27;
2|^h >= h by NAT_3:2;
then h <= n by 2n,XXREAL_0:2;
then hn2: 2|^h divides 2|^n by NEWTON:89;
deffunc F(Nat) = s.$1 mod 2|^h;
consider sm being XFinSequence of NAT such that
sm: len sm = len s &
for j being Nat st j in len s holds sm.j = F(j)
from AFINSQ_2:sch 1;
ss: Sum s mod 2|^h = Sum sm mod 2|^h by sm,NUMERAL2:17;
set B1=OddNAT, B2=EvenNAT;
now
let o be object;
assume o: o in dom SubXFinS(sm,B1);
then reconsider k=o as Nat;
reconsider ds=dom sm as natural-membered finite set;
reconsider BB=B1 /\ ds as finite natural-membered set;
kid: k in dom Sgm0(BB) by o,NUMERAL2:6;
SX: SubXFinS(sm,B1).o = sm.((Sgm0(BB)).k) by o,FUNCT_1:12
.= sm.(2*k+1) by kid,NUMERAL2:13;
thus SubXFinS(sm,B1).o = 0
proof
per cases;
suppose
dk: 2*k+1 in dom s;
then sf: SubXFinS(sm,B1).o = s.(2*k+1) mod 2|^h by SX,sm
.= ((2*k+1)+1)|^n mod 2|^h by s,dk
.= (2*(k+1))|^n mod 2|^h
.= ((2|^n) * ((k+1)|^n)) mod 2|^h by NEWTON:7;
2|^h divides (2|^n)*((k+1)|^n) by hn2,INT_2:2;
hence SubXFinS(sm,B1).o = 0 by sf,PEPIN:6;
end;
suppose
not 2*k+1 in dom s;
then not 2*k+1 in dom sm by sm;
hence SubXFinS(sm,B1).o = 0 by SX,FUNCT_1:def 2;
end;
end;
end; then
SubXFinS(sm,B1) = (dom SubXFinS(sm,B1)) --> 0 by FUNCOP_1:11; then
sz: Sum(SubXFinS(sm,B1))=(len SubXFinS(sm,B1))*0 by AFINSQ_2:58;
ll: len sm = ne-1 by n,sm;
then reconsider Slm=Segm(len sm) as odd Nat;
card (Slm /\ B2) = (Slm div 2) + 1 by lemmacardeven
.= (Slm-1)/2 + 1 by NAT_6:5
.= n2 by n2,ll; then
dn2: len SubXFinS(sm,B2) = n2 by AFINSQ_2:36;
now
let o be object;
assume o: o in dom SubXFinS(sm,B2);
then reconsider k=o as Nat;
reconsider ds=dom sm as natural-membered finite set;
reconsider BB=B2 /\ ds as finite natural-membered set;
kid: k in dom Sgm0(BB) by o,NUMERAL2:6;
reconsider dk=2*k as even Nat;
reconsider dkj=dk+1 as odd Nat;
k < len SubXFinS(sm,B2) by o,AFINSQ_1:86;
then k < n2 by dn2;
then 2*k < 2*n2 by XREAL_1:68;
then dk < len s + 1 by n,n2;
then dk <= len s by NAT_1:13;
then dk < len s or dk=ne-1 by n,XXREAL_0:1;
then dks: dk in dom s by AFINSQ_1:86;
SX: SubXFinS(sm,B2).o = sm.((Sgm0(BB)).k) by o,FUNCT_1:12
.= sm.(2*k) by kid,NUMERAL2:12
.= s.(dk) mod 2|^h by sm,dks
.= dkj|^n mod 2|^h by s,dks;
reconsider d=2 as Prime by INT_2:28;
hen1: h >= 1 by hen,NAT_1:14;
then eu: Euler (2|^h)= d|^h - d|^(h-'1) by INT_8:8
.= d|^(hj+1) - d|^hj by XREAL_1:233,hen1
.= (d|^hj)*d - d|^hj by NEWTON:6
.= d|^hj;
2|^h >= 1+1 by hen1,PREPOWER:12;
then ddh: 2|^h > 1 by NAT_1:13;
hj<=h-0 by XREAL_1:10; then
2|^hj divides 2|^h by PEPIN:31;
then 2|^hj divides n by dwah,INT_2:9;
then consider a being Nat such that
a: n=2|^hj*a by NAT_D:def 3;
dkj,2|^1 are_coprime by NAT_5:3;
then dkj,2 are_coprime by NEWTON:5;
then dkj,2|^h are_coprime by EULER_2:17;
then dkj|^(Euler (2|^h)) mod (2|^h) = 1 by ddh,EULER_2:18;
:: by Euler's theorem
then dkj|^(d|^hj) mod (2|^h) = 1 by eu;
then (dkj|^(d|^hj))|^a mod (2|^h) = 1 by ddh,PEPIN:35;
then (dkj|^((d|^hj)*a)) mod (2|^h) = 1 by NEWTON:9;
hence SubXFinS(sm,B2).o = 1 by SX,a;
end; then
SubXFinS(sm,B2) = (dom SubXFinS(sm,B2)) --> 1 by FUNCOP_1:11; then
sn: Sum SubXFinS(sm,B2) = n2*1 by dn2,AFINSQ_2:58;
B1 misses B2 by NUMERAL2:7;
then Sum(SubXFinS(sm,B1\/B2))=0+Sum(SubXFinS(sm,B2)) by NUMERAL2:10,sz;
then Sum sm = Sum(SubXFinS(sm,B2)) by NUMERAL2:8,11;
then Sum s mod 2|^h = n2 mod 2|^h by sn,ss; then
fs: n2, Sum s are_congruent_mod 2|^h by NAT_D:64;
2|^h divides n by n,NAT_3:def 7;
then 2|^h divides Sum s - 0 by INT_2:9,nd;
then Sum s, 0 are_congruent_mod 2|^h by INT_1:def 4;
then n2,0 are_congruent_mod 2|^h by fs,INT_1:15;
then 2|^h divides n2-0 by INT_1:def 4;
then 2*(2|^h) divides n by INT_6:8,n2;
then 2|^(h+1) divides n by NEWTON:6;
hence contradiction by n,NAT_3:def 7;
end;
end;