:: More on Divisibility Criteria for Selected Primes
:: by Adam Naumowicz and Rados{\l}aw Piliszek
::
:: Received May 19, 2013
:: Copyright (c) 2013-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 TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, CARD_1, CARD_3, ARYTM_3, ARYTM_1, NUMBERS, XXREAL_0, NAT_1,
INT_1, MEMBERED, VALUED_0, INT_2, BINOP_2, ORDINAL4, FINSEQ_1, VALUED_1,
FINSOP_1, NEWTON, RFINSEQ, ABIAN, AFINSQ_1, AFINSQ_2, FIB_NUM2, JORDAN3,
NUMERAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FINSET_1, CARD_1, SETWISEO,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, RAT_1, MEMBERED,
VALUED_0, INT_2, NAT_D, BINOP_2, FINSEQ_1, RECDEF_1, VALUED_1, FINSOP_1,
NEWTON, ABIAN, SERIES_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STIRL2_1,
FIB_NUM2, NUMERAL1;
constructors XTUPLE_0, FUNCT_1, RELSET_1, PARTFUN1, WELLORD2, FUNCT_2,
BINOP_1, FUNCOP_1, CARD_1, SETWISEO, XXREAL_0, REAL_1, SQUARE_1, NAT_1,
VALUED_0, ABSVALUE, NAT_D, BINOP_2, ORDINAL4, RECDEF_1, VALUED_1, SEQ_1,
FINSOP_1, NEWTON, PREPOWER, ABIAN, SERIES_1, AFINSQ_1, PARTFUN3,
AFINSQ_2, STIRL2_1, FIB_NUM2, ORDINAL6, BINOM, CARD_FIN, NUMERAL1,
ALGSTR_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
FINSET_1, CARD_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0,
BINOP_2, VALUED_1, NEWTON, ABIAN, AFINSQ_1, AFINSQ_2, ORDINAL6;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, AFINSQ_2;
equalities ORDINAL1, AFINSQ_2, XCMPLX_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
XXREAL_0, XREAL_0, XREAL_1, NAT_1, INT_1, VALUED_0, INT_2, NAT_D,
BINOP_2, CARD_2, VALUED_1, NEWTON, ABIAN, WSIERP_1, EULER_1, AFINSQ_1,
PEPIN, AFINSQ_2, FINSEQ_4, NAT_4, FIB_NUM2, NUMERAL1, CARD_FIN, XCMPLX_1;
schemes NAT_1, AFINSQ_2, STIRL2_1;
begin :: Preliminaries on finite sequences
reserve n,k,b for Nat, i for Integer;
theorem Th1:
for f being non empty XFinSequence holds f|1 = <% f.0 %>
proof
let f be non empty XFinSequence;
A1: 0 in Segm(0+1) by NAT_1:45;
len f >= 1 by NAT_1:14; then
len (f|1) = 1 & (f|1).0=f.0 by AFINSQ_1:54,FUNCT_1:49,A1;
hence thesis by AFINSQ_1:34;
end;
theorem Th2:
for f being non empty XFinSequence holds f=<%f.0%> ^ (f/^1)
proof
let f be non empty XFinSequence;
thus f=(f|1)^(f/^1) .= <%f.0%>^(f/^1) by Th1;
end;
theorem Th3:
for f being XFinSequence holds mid(f,2,len f)=f/^1
proof
let f be XFinSequence;
A1: 2-1>=0;
thus mid(f,2,len f) = f/^1 by A1,XREAL_0:def 2;
end;
theorem Th4:
for X,Y being finite natural-membered set st X misses Y
holds dom (Sgm0(X)^Sgm0(Y)) = dom Sgm0(X\/Y)
proof
let X,Y be finite natural-membered set such that A1: X misses Y;
thus dom (Sgm0(X)^Sgm0(Y)) = len (Sgm0(X)) + len (Sgm0(Y))
by AFINSQ_1:def 3
.= card (X) + len (Sgm0(Y)) by AFINSQ_2:20
.= card (X) + card (Y) by AFINSQ_2:20
.= card (X\/Y) by A1,CARD_2:40
.= len Sgm0(X\/Y) by AFINSQ_2:20
.= dom Sgm0(X\/Y);
end;
theorem Th5:
for X,Y being finite natural-membered set
holds rng (Sgm0(X)^Sgm0(Y)) = rng Sgm0(X\/Y)
proof
let X,Y be finite natural-membered set;
thus rng (Sgm0(X)^Sgm0(Y)) = rng Sgm0(X) \/ rng Sgm0(Y) by AFINSQ_1:26
.= X \/ rng Sgm0(Y) by AFINSQ_2:def 4
.= X \/ Y by AFINSQ_2:def 4
.= rng Sgm0(X\/Y) by AFINSQ_2:def 4;
end;
theorem Th6:
for F being XFinSequence
for X being set
holds dom SubXFinS(F, X) = dom Sgm0(X /\ dom F)
proof
let F be XFinSequence;
let X be set;
len SubXFinS(F, X) = card (X /\ Segm(len F)) by AFINSQ_2:36
.= card Sgm0(X /\ dom F) by AFINSQ_2:20;
hence thesis;
end;
definition
redefine func EvenNAT equals {n where n is Nat: n is even}; :: redefines EvenNAT (FIB_NUM2, definition)
compatibility
proof
EvenNAT ={n where n is Nat: n is even}
proof
thus EvenNAT c= {n where n is Nat: n is even}
proof
let m be object;
assume m in EvenNAT;
then consider k being Nat such that
A1: m=2 * k by FIB_NUM2:def 3;
thus m in {n where n is Nat: n is even} by A1;
end;
thus {n where n is Nat: n is even} c= EvenNAT
proof
let m be object;
assume m in {n where n is Nat: n is even};
then consider n being Nat such that
A2: n=m & n is even;
consider k being Nat such that
A3: n=2 * k by A2,ABIAN:def 2;
thus m in EvenNAT by A2,A3,FIB_NUM2:def 3;
end;
end;
hence thesis;
end;
end;
definition
redefine func OddNAT equals {n where n is Nat: n is odd}; :: redefines OddNAT (FIB_NUM2, definition)
compatibility
proof
OddNAT = {n where n is Nat: n is odd}
proof
thus OddNAT c= {n where n is Nat: n is odd}
proof
let m be object;
assume m in OddNAT;
then consider k being Element of NAT such that
A1: m=2 * k + 1 by FIB_NUM2:def 4;
thus m in {n where n is Nat: n is odd} by A1;
end;
let m be object;
assume m in {n where n is Nat: n is odd};
then consider n being Nat such that
A2: n=m & n is odd;
consider k being Nat such that
A3: n=2 * k + 1 by A2,ABIAN:9;
k is Element of NAT by ORDINAL1:def 12;
hence m in OddNAT by A2,A3,FIB_NUM2:def 4;
end;
hence thesis;
end;
end;
theorem Th7:
EvenNAT misses OddNAT
proof
thus EvenNAT /\ OddNAT c= {}
proof
let n be object;
assume n in EvenNAT /\ OddNAT;
then A1: n in EvenNAT & n in OddNAT by XBOOLE_0:def 4;
consider e being Nat such that
A2: e=n & e is even by A1;
consider o being Nat such that
A3: o=n & o is odd by A1;
thus thesis by A2,A3;
end;
thus {} c= EvenNAT /\ OddNAT by XBOOLE_1:2;
end;
theorem Th8:
EvenNAT \/ OddNAT = NAT
proof
thus EvenNAT \/ OddNAT c= NAT;
let n be object;
assume A1: n in NAT & not n in (EvenNAT \/ OddNAT);
then reconsider n as Nat;
n in NAT & not n in EvenNAT & not n in OddNAT by A1, XBOOLE_0:def 3;
then not n is even & not n is odd;
hence contradiction;
end;
registration
let F be Sequence;
let P be Permutation of dom F;
cluster F*P -> Sequence-like;
correctness
proof
per cases;
suppose rng F is empty;
then F = {};
hence thesis;
end;
suppose A1: rng F is non empty;
A2: dom P = dom F by FUNCT_2:52;
F is Function of dom F, rng F by FUNCT_2:1;
then dom (F*P) = dom F by A1,FUNCT_2:123,A2;
hence thesis by ORDINAL1:def 7;
end;
end;
end;
theorem Th9:
for F being XFinSequence
for X,Y being set st X misses Y
ex P being Permutation of dom SubXFinS(F,X\/Y) st
SubXFinS(F,X\/Y) * P = SubXFinS(F,X) ^ SubXFinS(F,Y)
proof
let F be XFinSequence;
let X,Y be set such that A1: X misses Y;
set A=Sgm0(X/\Segm len F)^Sgm0(Y/\Segm len F);
set B=Sgm0((X\/Y)/\Segm len F);
A2: rng Sgm0(X/\Segm len F) = X/\len F &
rng Sgm0(Y/\Segm len F) = Y/\len F by AFINSQ_2:def 4;
then reconsider A as one-to-one Function by A1,XBOOLE_1:76,CARD_FIN:52;
reconsider B as one-to-one Function;
A3: (X\/Y) /\ len F = (X/\len F) \/ (Y/\len F) by XBOOLE_1:23;
then A4: rng A = rng B by Th5;
then A5: rng A = dom (B") by FUNCT_1:33;
set P=(B")*A;
A6: dom P = dom A by A5,RELAT_1:27
.= dom B by A3,A1,XBOOLE_1:76,Th4
.= dom SubXFinS(F,X\/Y) by Th6;
A7: rng P = rng (B") by A5,RELAT_1:28
.= dom B by FUNCT_1:33
.= dom SubXFinS(F,X\/Y) by Th6;
reconsider P as Function of dom SubXFinS(F,X\/Y),dom SubXFinS(F,X\/Y)
by A6,A7,FUNCT_2:2;
card dom SubXFinS(F,X\/Y) = card dom SubXFinS(F,X\/Y);
then P is onto by FINSEQ_4:63;
then reconsider P as Permutation of dom SubXFinS(F,X\/Y);
take P;
A8: rng Sgm0(X/\Segm len F) c= len F & rng Sgm0(Y/\Segm len F) c= len F
by A2,XBOOLE_1:17;
thus SubXFinS(F,X\/Y) * P = F * (Sgm0((X\/Y)/\Segm len F) * (B"*A))
by RELAT_1:36
.= F * ((Sgm0((X\/Y)/\Segm len F) * B") * A) by RELAT_1:36
.= F * (id (rng A) * A) by FUNCT_1:39,A4
.= F * A by RELAT_1:54
.= SubXFinS(F,X) ^ SubXFinS(F,Y) by A8,AFINSQ_2:70;
end;
theorem Th10:
for cF being complex-valued XFinSequence
for B1,B2 being set st
B1 misses B2 holds
Sum(SubXFinS(cF,B1\/B2))=Sum(SubXFinS(cF,B1))+Sum(SubXFinS(cF,B2))
proof
let cF be complex-valued XFinSequence;
let B1,B2 be set such that A1: B1 misses B2;
set O=SubXFinS(cF,B1\/B2);
reconsider O=SubXFinS(cF,B1\/B2) as XFinSequence of COMPLEX;
consider P be Permutation of dom O such that
A2: O * P = SubXFinS (cF,B1) ^ SubXFinS (cF,B2) by A1,Th9;
Sum(O * P) = Sum(SubXFinS(cF,B1)) + Sum(SubXFinS(cF,B2)) by A2,AFINSQ_2:55;
hence thesis by AFINSQ_2:45;
end;
theorem Th11:
for F being XFinSequence
holds F = SubXFinS(F,NAT)
proof
let F be XFinSequence;
set SFN=Sgm0(len F /\ NAT);
dom F c= NAT;
then A1: len F /\ NAT = len F by XBOOLE_1:28;
A2: F is Function of dom F,rng F by FUNCT_2:1;
reconsider idF= id dom F as XFinSequence of NAT;
A3: rng idF = len F;
now
let l,m,k1,k2 be Nat;
assume A4: l < m & m < len idF & k1=idF.l & k2=idF.m;
then l < len idF by XXREAL_0:2;
then k1=l & k2=m by A4,FUNCT_1:18,AFINSQ_1:66;
hence k1 < k2 by A4;
end;
then id dom F = Sgm0(Segm len F) by AFINSQ_2:def 4,A3;
hence thesis by A1,FUNCT_2:17,A2;
end;
theorem Th12:
for N,i being Nat
st i in dom Sgm0(N /\ EvenNAT)
holds (Sgm0(N /\ EvenNAT)).i = 2*i
proof
defpred P[Nat] means for i being Nat st i in dom Sgm0($1 /\ EvenNAT)
holds (Sgm0($1 /\ EvenNAT)).i = 2*i;
A1: P[0]
proof
let i be Nat;
assume i in dom Sgm0(0 /\ EvenNAT);
then i in len Sgm0({});
then i in card {} by AFINSQ_2:20;
hence thesis;
end;
A2:
now
let n be Nat;
assume A3: P[n];
thus P[n+1]
proof
let i be Nat;
assume A4: i in dom Sgm0((n+1) /\ EvenNAT);
per cases;
suppose A5: n is even;
A6: (n+1)/\EvenNAT = (n /\ EvenNAT) \/ {n}
proof
thus (n+1)/\EvenNAT c= (n /\ EvenNAT) \/ {n}
proof
let x be object;
assume A7: x in (n+1)/\EvenNAT;
then x in (n+1) & x in EvenNAT by XBOOLE_0:def 4;
then consider y being Nat such that
A8: y=x & y is even;
y in Segm(n+1) & y in EvenNAT by A7,XBOOLE_0:def 4,A8;
then (y < n or y = n) & y in EvenNAT by NAT_1:44,NAT_1:22;
then (y in Segm n & y in EvenNAT) or y = n by NAT_1:44;
then y in (n /\ EvenNAT) or y in {n}
by XBOOLE_0:def 4,TARSKI:def 1;
hence x in (n /\ EvenNAT) \/ {n} by A8,XBOOLE_0:def 3;
end;
let x be object;
assume x in (n/\EvenNAT) \/ {n};
then per cases by XBOOLE_0:def 3;
suppose A9: x in (n/\EvenNAT);
Segm n c= Segm(n+1) by NAT_1:11,NAT_1:39;
then n /\ EvenNAT c= (n+1) /\ EvenNAT by XBOOLE_1:26;
hence x in (n+1) /\ EvenNAT by A9;
end;
suppose x in {n};
then x=n by TARSKI:def 1;
then x in Segm(n+1) & x in EvenNAT by NAT_1:45,A5;
hence x in (n+1) /\ EvenNAT by XBOOLE_0:def 4;
end;
end;
reconsider X = n /\ EvenNAT as finite natural-membered set;
reconsider Y = {n} as finite natural-membered set;
A10: X <N< Y
proof
let a,b be Nat;
assume a in X & b in Y;
then a in Segm n & b=n by XBOOLE_0:def 4,TARSKI:def 1;
hence a < b by NAT_1:44;
end;
not n in n; then
not n in (n /\ EvenNAT) by XBOOLE_0:def 4;
then A11: card ((n+1)/\EvenNAT) = card (n /\ EvenNAT) + 1
by A6,CARD_2:41;
A12: i in Segm dom Sgm0((n+1) /\ EvenNAT) by A4;
then i < len Sgm0((n+1) /\ EvenNAT) by NAT_1:44;
then i < card (n /\ EvenNAT) + 1 by A11,AFINSQ_2:20;
then i < len (Sgm0 X) + 1 by AFINSQ_2:20;
then per cases by NAT_1:22;
suppose A13: i < len (Sgm0 X);
then A14: i < Segm card (Sgm0(n /\ EvenNAT));
thus (Sgm0((n+1) /\ EvenNAT)).i = (Sgm0(n /\ EvenNAT)).i
by A10,A13,AFINSQ_2:29,A6
.= 2*i by A14,NAT_1:44,A3;
end;
suppose A15: i=len (Sgm0 X);
then A16: (Sgm0((n+1) /\ EvenNAT)).i = (Sgm0 Y).0
by AFINSQ_2:32,A10,A6
.= n by AFINSQ_2:22;
(Sgm0((n+1) /\ EvenNAT)).i in rng (Sgm0((n+1) /\ EvenNAT))
by FUNCT_1:3,A4;
then (Sgm0((n+1) /\ EvenNAT)).i in (n+1) /\ EvenNAT
by AFINSQ_2:def 4;
then (Sgm0((n+1) /\ EvenNAT)).i in EvenNAT by XBOOLE_0:def 4;
then consider r being Nat such that
A17: r=(Sgm0((n+1) /\ EvenNAT)).i & r is even;
consider j being Nat such that
A18: r=2*j by A17,ABIAN:def 2;
per cases by XXREAL_0:1;
suppose A19: j<i;
then A20: j < Segm card (Sgm0(n /\ EvenNAT)) by A15;
j < card Sgm0((n+1) /\ EvenNAT) by A19,A12,NAT_1:44,XXREAL_0:2;
then A21: j in Segm dom Sgm0((n+1) /\ EvenNAT) by NAT_1:44;
(Sgm0((n+1) /\ EvenNAT)).j = (Sgm0(n /\ EvenNAT)).j
by A10,A19,A15,AFINSQ_2:29,A6
.= (Sgm0((n+1) /\ EvenNAT)).i by A20,NAT_1:44,A3,A17,A18;
hence (Sgm0((n+1) /\ EvenNAT)).i = 2*i
by A21,A4,FUNCT_1:def 4,A19;
end;
suppose j=i;
hence (Sgm0((n+1) /\ EvenNAT)).i = 2*i by A17,A18;
end;
suppose A22: j>i;
A23: 2*i in EvenNAT;
2*i < n & n < n+1 by A22,XREAL_1:68,A17,A18,A16,NAT_1:16;
then 2*i < n+1 by XXREAL_0:2;
then 2*i in Segm (n+1) by NAT_1:44;
then 2*i in ((n+1) /\ EvenNAT) by A23,XBOOLE_0:def 4;
then 2*i in rng (Sgm0((n+1) /\ EvenNAT)) by AFINSQ_2:def 4;
then consider l being object such that
A24: l in dom (Sgm0((n+1) /\ EvenNAT)) &
(Sgm0((n+1) /\ EvenNAT)).l=2*i by FUNCT_1:def 3;
reconsider l as Element of NAT by A24;
l in Segm dom Sgm0((n+1) /\ EvenNAT) by A24;
then l < len Sgm0((n+1) /\ EvenNAT) by NAT_1:44;
then l < card (n /\ EvenNAT) + 1 by A11,AFINSQ_2:20;
then l < len (Sgm0 X) + 1 by AFINSQ_2:20;
then per cases by NAT_1:22;
suppose A25: l < len (Sgm0 X);
then A26: l < Segm card (Sgm0(n /\ EvenNAT));
(Sgm0((n+1) /\ EvenNAT)).l = (Sgm0(n /\ EvenNAT)).l
by A10,A25,AFINSQ_2:29,A6
.= 2*l by A26,NAT_1:44,A3;
then 2*i=2*l by A24;
hence (Sgm0((n+1) /\ EvenNAT)).i = 2*i by A25,A15;
end;
suppose l=len (Sgm0 X);
hence (Sgm0((n+1) /\ EvenNAT)).i = 2*i by A15,A24;
end;
end;
end;
end;
suppose A27: n is odd;
(n+1)/\EvenNAT = n /\ EvenNAT
proof
thus (n+1)/\EvenNAT c= n /\ EvenNAT
proof
let x be object;
assume x in (n+1)/\EvenNAT;
then A28: x in Segm (n+1) & x in EvenNAT by XBOOLE_0:def 4;
then consider y being Nat such that
A29: y=x & y is even;
y<n by A28,A29,NAT_1:44,A27,NAT_1:22;
then y in Segm n & y in EvenNAT by A29,NAT_1:44;
hence x in n /\ EvenNAT by A29,XBOOLE_0:def 4;
end;
Segm n c= Segm(n+1) by NAT_1:11,NAT_1:39;
hence n /\ EvenNAT c= (n+1) /\ EvenNAT by XBOOLE_1:26;
end;
hence (Sgm0((n+1) /\ EvenNAT)).i = 2*i by A4,A3;
end;
end;
end;
for N being Nat holds P[N] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th13:
for N,i being Nat
st i in dom Sgm0(N /\ OddNAT)
holds (Sgm0(N /\ OddNAT)).i = 2*i+1
proof
defpred P[Nat] means for i being Nat st i in dom Sgm0($1 /\ OddNAT)
holds (Sgm0($1 /\ OddNAT)).i = 2*i+1;
A1: P[0]
proof
let i be Nat;
assume i in dom Sgm0(0 /\ OddNAT);
then i in len Sgm0({});
then i in card {} by AFINSQ_2:20;
hence thesis;
end;
A2:
now
let n be Nat;
assume A3: P[n];
thus P[n+1]
proof
let i be Nat;
assume A4: i in dom Sgm0((n+1) /\ OddNAT);
per cases;
suppose A5: n is odd;
A6: (n+1)/\OddNAT = (n /\ OddNAT) \/ {n}
proof
thus (n+1)/\OddNAT c= (n /\ OddNAT) \/ {n}
proof
let x be object;
assume A7: x in (n+1)/\OddNAT;
then x in (n+1) & x in OddNAT by XBOOLE_0:def 4;
then consider y being Nat such that
A8: y=x & y is odd;
y in Segm(n+1) & y in OddNAT by A7,XBOOLE_0:def 4,A8;
then (y < n or y = n) & y in OddNAT by NAT_1:44,NAT_1:22;
then (y in Segm n & y in OddNAT) or y = n by NAT_1:44;
then y in (n /\ OddNAT) or y in {n}
by XBOOLE_0:def 4,TARSKI:def 1;
hence x in (n /\ OddNAT) \/ {n} by A8,XBOOLE_0:def 3;
end;
let x be object;
assume x in (n/\OddNAT) \/ {n};
then per cases by XBOOLE_0:def 3;
suppose A9: x in (n/\OddNAT);
Segm n c= Segm(n+1) by NAT_1:11,NAT_1:39;
then n /\ OddNAT c= (n+1) /\ OddNAT by XBOOLE_1:26;
hence x in (n+1) /\ OddNAT by A9;
end;
suppose x in {n};
then x=n by TARSKI:def 1;
then x in Segm(n+1) & x in OddNAT by NAT_1:45,A5;
hence x in (n+1) /\ OddNAT by XBOOLE_0:def 4;
end;
end;
reconsider X = n /\ OddNAT as finite natural-membered set;
reconsider Y = {n} as finite natural-membered set;
A10: X <N< Y
proof
let a,b be Nat;
assume a in X & b in Y;
then a in Segm n & b=n by XBOOLE_0:def 4,TARSKI:def 1;
hence a < b by NAT_1:44;
end;
not n in n; then
not n in (n /\ OddNAT) by XBOOLE_0:def 4;
then A11: card ((n+1)/\OddNAT) = card (n /\ OddNAT) + 1
by A6,CARD_2:41;
A12: i in Segm dom Sgm0((n+1) /\ OddNAT) by A4;
then i < len Sgm0((n+1) /\ OddNAT) by NAT_1:44;
then i < card (n /\ OddNAT) + 1 by A11,AFINSQ_2:20;
then i < len (Sgm0 X) + 1 by AFINSQ_2:20;
then per cases by NAT_1:22;
suppose A13: i < len (Sgm0 X);
then A14: i < Segm card (Sgm0(n /\ OddNAT));
thus (Sgm0((n+1) /\ OddNAT)).i = (Sgm0(n /\ OddNAT)).i
by A10,A13,AFINSQ_2:29,A6
.= 2*i+1 by A14,NAT_1:44,A3;
end;
suppose A15: i=len (Sgm0 X);
then A16: (Sgm0((n+1) /\ OddNAT)).i = (Sgm0 Y).0
by AFINSQ_2:32,A10,A6
.= n by AFINSQ_2:22;
(Sgm0((n+1) /\ OddNAT)).i in rng (Sgm0((n+1) /\ OddNAT))
by FUNCT_1:3,A4;
then (Sgm0((n+1) /\ OddNAT)).i in (n+1) /\ OddNAT
by AFINSQ_2:def 4;
then (Sgm0((n+1) /\ OddNAT)).i in OddNAT by XBOOLE_0:def 4;
then consider r being Nat such that
A17: r=(Sgm0((n+1) /\ OddNAT)).i & r is odd;
consider j being Nat such that
A18: r=2*j+1 by A17,ABIAN:9;
per cases by XXREAL_0:1;
suppose A19: j<i;
then A20: j < Segm card (Sgm0(n /\ OddNAT)) by A15;
j < card Sgm0((n+1) /\ OddNAT) by A19,A12,NAT_1:44,XXREAL_0:2;
then A21: j in Segm dom Sgm0((n+1) /\ OddNAT) by NAT_1:44;
(Sgm0((n+1) /\ OddNAT)).j = (Sgm0(n /\ OddNAT)).j
by A10,A19,A15,AFINSQ_2:29,A6
.= (Sgm0((n+1) /\ OddNAT)).i by A20,NAT_1:44,A3,A17,A18;
hence (Sgm0((n+1) /\ OddNAT)).i = 2*i+1
by A21,A4,FUNCT_1:def 4,A19;
end;
suppose j=i;
hence (Sgm0((n+1) /\ OddNAT)).i = 2*i+1 by A17,A18;
end;
suppose j>i;
then A22: 2*i< 2*j by XREAL_1:68;
A23: 2*i+1 in OddNAT;
2*i+1 < n & n < n+1 by A22,XREAL_1:8,A17,A18,A16,NAT_1:16;
then 2*i+1 < n+1 by XXREAL_0:2;
then 2*i+1 in Segm (n+1) by NAT_1:44;
then 2*i+1 in ((n+1) /\ OddNAT) by A23,XBOOLE_0:def 4;
then 2*i+1 in rng (Sgm0((n+1) /\ OddNAT)) by AFINSQ_2:def 4;
then consider l being object such that
A24: l in dom (Sgm0((n+1) /\ OddNAT)) &
(Sgm0((n+1) /\ OddNAT)).l=2*i+1 by FUNCT_1:def 3;
reconsider l as Element of NAT by A24;
l in Segm dom Sgm0((n+1) /\ OddNAT) by A24;
then l < len Sgm0((n+1) /\ OddNAT) by NAT_1:44;
then l < card (n /\ OddNAT) + 1 by A11,AFINSQ_2:20;
then l < len (Sgm0 X) + 1 by AFINSQ_2:20;
then per cases by NAT_1:22;
suppose A25: l < len (Sgm0 X);
then A26: l < Segm card (Sgm0(n /\ OddNAT));
(Sgm0((n+1) /\ OddNAT)).l = (Sgm0(n /\ OddNAT)).l
by A10,A25,AFINSQ_2:29,A6
.= 2*l+1 by A26,NAT_1:44,A3;
then 2*i+1=2*l+1 by A24;
hence (Sgm0((n+1) /\ OddNAT)).i = 2*i+1 by A25,A15;
end;
suppose l=len (Sgm0 X);
hence (Sgm0((n+1) /\ OddNAT)).i = 2*i+1 by A15,A24;
end;
end;
end;
end;
suppose A27: n is even;
(n+1)/\OddNAT = n /\ OddNAT
proof
thus (n+1)/\OddNAT c= n /\ OddNAT
proof
let x be object;
assume x in (n+1)/\OddNAT;
then A28: x in Segm (n+1) & x in OddNAT by XBOOLE_0:def 4;
then consider y being Nat such that
A29: y=x & y is odd;
y<n by A28,A29,NAT_1:44,A27,NAT_1:22;
then y in Segm n & y in OddNAT by A29,NAT_1:44;
hence x in n /\ OddNAT by A29,XBOOLE_0:def 4;
end;
Segm n c= Segm(n+1) by NAT_1:11,NAT_1:39;
hence n /\ OddNAT c= (n+1) /\ OddNAT by XBOOLE_1:26;
end;
hence (Sgm0((n+1) /\ OddNAT)).i = 2*i+1 by A4,A3;
end;
end;
end;
for N being Nat holds P[N] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
begin :: Lemmas on some divisibility properties
theorem Th14:
for i,j being Integer holds (i mod j) mod j = i mod j
proof
let i,j be Integer;
per cases;
suppose j<>0;
hence (i mod j) mod j = (i - (i div j) * j) mod j by INT_1:def 10
.= (i + j * (-(i div j) qua Integer)) mod j
.= i mod j by NAT_D:61;
end;
suppose A1: j=0;
hence (i mod j) mod j = 0 .= i mod j by A1;
end;
end;
theorem
for i,j,k,l being Integer st i mod l = j mod l holds
(k + i) mod l = (k + j) mod l
proof
let i,j,k,l be Integer;
assume A1: i mod l = j mod l;
thus (k + i) mod l = ((k mod l)+(i mod l)) mod l by NAT_D:66
.= (k + j) mod l by A1,NAT_D:66;
end;
theorem Th16:
for d being XFinSequence of INT, n being Integer st for i being Nat
st i in dom d holds n divides d.i holds n divides Sum d
proof
let d be XFinSequence of INT, n be Integer such that
A1: for i being Nat st i in dom d holds n divides d.i;
per cases;
suppose
len d=0;
then d={};
then Sum d = 0;
hence thesis by INT_2:12;
end;
suppose
A2: len d > 0;
then consider f being Function of NAT,INT such that
A3: f.0 = d.0 and
A4: for n being Nat st n+1 < len d holds
f.(n + 1) = addint.(f.n,d.(n + 1)) and
A5: addint "**" d = f.(len d-1) by AFINSQ_2:def 8;
defpred P[Nat] means $1 < len d implies n divides f.$1;
A6:
now
let k be Nat;
assume A7: P[k];
thus P[k+1]
proof
assume
A8: k+1 < len d;
then k+1 in Segm(len d) by NAT_1:44;
then
A9: n divides d.(k+1) by A1;
f.(k+1) = addint.(f.k,d.(k+1)) by A4,A8
.= f.k + d.(k+1) by BINOP_2:def 20;
hence thesis by A7,A8,A9,XREAL_1:145,WSIERP_1:4;
end;
end;
reconsider ld=len d-1 as Element of NAT by A2,NAT_1:20;
A10: ld < len d by XREAL_1:147;
0 in Segm dom d by NAT_1:44,A2; then
A11: P[0] by A1,A3;
A12: addint "**" d = Sum d by AFINSQ_2:50;
for k being Nat holds P[k] from NAT_1:sch 2(A11,A6);
hence thesis by A5,A10,A12;
end;
end;
theorem
for d,e being XFinSequence of INT, n being Integer st
dom d = dom e & for i being Nat st i in dom d holds e.i = d.i mod n
holds Sum d mod n = Sum e mod n
proof
let d,e be XFinSequence of INT, n be Integer such that
A1: dom d = dom e & for i being Nat st i in dom d holds e.i = d.i mod n;
defpred P[XFinSequence of INT] means for e being XFinSequence of INT st dom
$1=dom e & for i being Nat st i in dom $1 holds
e.i = $1.i mod n holds (Sum $1)
mod n = (Sum e) mod n;
A2: for p being XFinSequence of INT, l being Element of INT st P[p]
holds P[p^<%l%>]
proof
let p be XFinSequence of INT, l be Element of INT;
assume
A3: P[p];
thus P[p^<%l%>]
proof
reconsider dop=dom p as Element of NAT by ORDINAL1:def 12;
defpred Q[set,Integer] means $2=p.$1 mod n;
let e be XFinSequence of INT;
assume that
A4: dom (p^<%l%>)=dom e and
A5: for i being Nat st i in dom (p^<%l%>) holds
e.i = (p^<%l%>).i mod n;
A6: for k being Nat st k in Segm dop
ex x being Element of INT st Q[k,x]
proof
let k be Nat;
assume k in Segm dop;
reconsider x=p.k mod n as Element of INT by INT_1:def 2;
take x;
thus thesis;
end;
consider p9 being XFinSequence of INT such that
A7: dom p9 = Segm dop & for k be Nat st k in Segm dop holds Q[k,p9.k]
from STIRL2_1:sch 5(A6);
A8:
now
let k be Nat;
assume
A9: k in dom p9;
then k < Segm dom p9 by NAT_1:44;
then k < len p + 1 by A7,NAT_1:13;
then k < len p + len <%l%> by AFINSQ_1:33;
then k in Segm (len p + len <%l%>) by NAT_1:44;
then k in dom (p^<%l%>) by AFINSQ_1:def 3;
hence e.k = (p^<%l%>).k mod n by A5
.= p.k mod n by A7,A9,AFINSQ_1:def 3
.= p9.k by A7,A9;
end;
A10:
now
let k be Nat;
assume k in dom <%l mod n%>; then
A11: k in Segm 1 by AFINSQ_1:33; then
A12: k = 0 by NAT_1:44,NAT_1:14;
k in dom <%l%> by A11,AFINSQ_1:33;
hence e.(len p9 + k) = (p^<%l%>).len p mod n by A5,A7,A12,AFINSQ_1:23
.= <%l mod n%>.k by A12,AFINSQ_1:36;
end;
dom e=len p + len <%l%> by A4,AFINSQ_1:def 3
.= dom p + 1 by AFINSQ_1:33
.= len p9 + len <%l mod n%> by A7,AFINSQ_1:33;
then
A13: e=p9^<%l mod n%> by A8,A10,AFINSQ_1:def 3;
reconsider lmn=l mod n as Element of INT by INT_1:def 2;
thus Sum (p^<%l%>) mod n = (Sum p + Sum <%l%>) mod n by AFINSQ_2:55
.= (Sum p + l) mod n by AFINSQ_2:53
.= ((Sum p) mod n + (l mod n)) mod n by NAT_D:66
.= ((Sum p9) mod n + (l mod n)) mod n by A3,A7
.= ((Sum p9) mod n + ((l mod n) mod n)) mod n by Th14
.= (Sum p9 + (l mod n)) mod n by NAT_D:66
.= (Sum p9 + Sum <%lmn%>) mod n by AFINSQ_2:53
.= (Sum e) mod n by A13,AFINSQ_2:55;
end;
end;
A14: P[<%>INT] by AFINSQ_1:15;
for p being XFinSequence of INT holds P[p] from AFINSQ_2:sch 2(A14,A2);
hence thesis by A1;
end;
theorem Th18:
for f,g being XFinSequence of NAT, i being Integer st dom f = dom g &
for n being object st n in dom f holds f.n=i*g.n holds Sum f = i * Sum g
proof
let f,g be XFinSequence of NAT, i be Integer;
assume dom f = dom g &
for n being object st n in dom f holds f.n=i*g.n;
then f=i(#)g by VALUED_1:def 5;
hence Sum f = i * Sum g by AFINSQ_2:64;
end;
theorem Th19:
b>1 implies
n = b*value(mid(digits(n,b),2,len(digits(n,b))),b) + digits(n,b).0
proof
assume A1: b>1;
set d=digits(n,b);
A2: len d >= 1 by A1,NUMERAL1:4; then
A3: 0 in Segm(dom d) by NAT_1:44;
n=value(d,b) by A1,NUMERAL1:5; then
consider d1 being XFinSequence of NAT such that
A4: (dom d1 = dom d & for i being Nat st i in dom d1 holds
d1.i = (d.i)*(b|^i)) & n = Sum d1 by NUMERAL1:def 1;
d1<>{} by A4,A2; then
d1=<%d1.0%>^(d1/^1) by Th2; then
A5: n = Sum <%d1.0%> + Sum (d1/^1) by A4,AFINSQ_2:55
.= d1.0 + Sum (d1/^1) by AFINSQ_2:53
.= Sum (d1/^1) + (d.0)*(b|^0) by A4,A3
.= Sum (d1/^1) + d.0*1 by NEWTON:4;
consider e being XFinSequence of NAT such that
A6: (dom e = dom (d/^1) & for i being Nat st i in dom e holds
e.i = ((d/^1).i)*(b|^i)) & value(d/^1,b) = Sum e by NUMERAL1:def 1;
A7: dom (d1/^1)= len (d1/^1) .= len d1 -' 1 by AFINSQ_2:def 2
.= len d -'1 by A4
.= len (d/^1) by AFINSQ_2:def 2 .= dom(d/^1);
now
let n1 be object;
assume A8: n1 in dom e; then
reconsider n=n1 as Nat;
n in len (d/^1) by A6,A8; then
n in Segm(len d -' 1) by AFINSQ_2:def 2; then
n+1 < len d -' 1 + 1 by NAT_1:44,XREAL_1:8; then
n+1 < len d by XREAL_1:235,A2; then
A9: n+1 in Segm(dom d) by NAT_1:44;
thus (d1/^1).n1 = d1.(n+1) by A7,A6,A8,AFINSQ_2:def 2
.= d.(n+1)*(b|^(n+1)) by A4,A9
.= d.(n+1)*((b|^n)*b) by NEWTON:6
.= b*(d.(n+1)*(b|^n))
.= b*(((d/^1).n)*(b|^n)) by A8,A6,AFINSQ_2:def 2
.= b*e.n1 by A8,A6;
end; then
Sum (d1/^1) = b*Sum e by A7,A6,Th18;
hence thesis by Th3,A6,A5;
end;
theorem Th20:
for n,k being Nat st k=10|^(2*n) - 1 holds 11 divides k
proof
defpred P[Nat] means ex k being Nat st k=10|^(2*$1)-1 & 11 divides k;
let n,k be Nat;
A1:
now
let k be Nat;
assume P[k];
then consider l being Nat such that
A2: l=10|^(2*k)-1 and
A3: 11 divides l;
consider m being Nat such that
A4: l = 11 * m by A3,NAT_D:def 3;
10|^(2*(k+1)) - 1 = 10|^(2*k+2) - 1
.= (11*m+1)*10|^(1+1) - 1 by A2,A4,NEWTON:8
.= (11*m+1)*(10|^1*10) - 1 by NEWTON:6
.= (11*m+1)*(10*10) - 1
.= 11*(m*100+9);
hence P[k+1] by NAT_D:def 3;
end;
(10|^0) -1 = 1-1 by NEWTON:4
.= 0; then
A5: P[0] by NAT_D:6;
for k being Nat holds P[k] from NAT_1:sch 2(A5,A1); then
A6: ex l being Nat st l=10|^(2*n) - 1 & 11 divides l;
assume k=10|^(2*n) - 1;
hence thesis by A6;
end;
theorem Th21:
for n,k being Nat st k=10|^(2*n+1) + 1 holds 11 divides k
proof
defpred P[Nat] means ex k being Nat st k=10|^(2*$1+1)+1 & 11 divides k;
let n,k be Nat;
A1: now
let k be Nat;
assume P[k];
then consider l being Nat such that
A2: l=10|^(2*k+1)+1 and
A3: 11 divides l;
consider m being Nat such that
A4: l = 11 * m by A3,NAT_D:def 3;
10|^(2*(k+1)+1) + 1 = 10|^(2*k+1+2) + 1
.= (11*m-1)*10|^(1+1) + 1 by A2,A4,NEWTON:8
.= (11*m-1)*((10|^1)*10) + 1 by NEWTON:6
.= (11*m-1)*(10*10) + 1
.= 11*(m*100-9);
hence P[k+1] by INT_1:def 3;
end;
A5: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A5,A1); then
A6: ex l being Nat st l=10|^(2*n+1) + 1 & 11 divides l;
assume k=10|^(2*n+1) + 1;
hence thesis by A6;
end;
theorem Th22:
7,10 are_coprime
proof
2,7 are_coprime & 5,7 are_coprime by NAT_4:26,EULER_1:2;
then 2*5,7 are_coprime by INT_2:26;
hence thesis;
end;
theorem Th23:
29 is prime
proof
now
let n be Element of NAT;
29 = 2*14 + 1;
then
A1: not 2 divides 29 by NAT_4:9;
29 = 3*9 + 2;
then
A2: not 3 divides 29 by NAT_4:9;
29 = 5*5 + 4;
then
A3: not 5 divides 29 by NAT_4:9;
29 = 7*4 + 1;
then
A4: not 7 divides 29 by NAT_4:9;
29 = 11*2 + 7;
then
A5: not 11 divides 29 by NAT_4:9;
29 = 13*2 + 3;
then
A6: not 13 divides 29 by NAT_4:9;
29 = 17*1 + 12;
then
A7: not 17 divides 29 by NAT_4:9;
29 = 19*1 + 10;
then
A8: not 19 divides 29 by NAT_4:9;
29 = 23*1 + 6;
then
A9: not 23 divides 29 by NAT_4:9;
assume 1<n & n*n<=29 & n is prime;
hence not n divides 29 by A1,A2,A9,A8,A4,A3,A6,A5,A7,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th24:
31 is prime
proof
now
let n be Element of NAT;
31 = 2*15 + 1;
then
A1: not 2 divides 31 by NAT_4:9;
31 = 3*10 + 1;
then
A2: not 3 divides 31 by NAT_4:9;
31 = 5*6 + 1;
then
A3: not 5 divides 31 by NAT_4:9;
31 = 7*4 + 3;
then
A4: not 7 divides 31 by NAT_4:9;
31 = 11*2 + 9;
then
A5: not 11 divides 31 by NAT_4:9;
31 = 13*2 + 5;
then
A6: not 13 divides 31 by NAT_4:9;
31 = 17*1 + 14;
then
A7: not 17 divides 31 by NAT_4:9;
31 = 19*1 + 12;
then
A8: not 19 divides 31 by NAT_4:9;
31 = 23*1 + 8;
then
A9: not 23 divides 31 by NAT_4:9;
assume 1<n & n*n<=31 & n is prime;
hence not n divides 31 by A1,A2,A9,A8,A4,A3,A6,A5,A7,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th25:
41 is prime
proof
now
let n be Element of NAT;
41 = 2*20 + 1;
then
A1: not 2 divides 41 by NAT_4:9;
41 = 3*13 + 2;
then
A2: not 3 divides 41 by NAT_4:9;
41 = 5*8 + 1;
then
A3: not 5 divides 41 by NAT_4:9;
41 = 7*5 + 6;
then
A4: not 7 divides 41 by NAT_4:9;
41 = 11*3 + 8;
then
A5: not 11 divides 41 by NAT_4:9;
41 = 13*3 + 2;
then
A6: not 13 divides 41 by NAT_4:9;
41 = 17*2 + 7;
then
A7: not 17 divides 41 by NAT_4:9;
41 = 19*2 + 3;
then
A8: not 19 divides 41 by NAT_4:9;
41 = 23*1 + 18;
then
A9: not 23 divides 41 by NAT_4:9;
assume 1<n & n*n<=41 & n is prime;
hence not n divides 41 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th26:
47 is prime
proof
now
let n be Element of NAT;
47 = 2*23 + 1;
then
A1: not 2 divides 47 by NAT_4:9;
47 = 3*15 + 2;
then
A2: not 3 divides 47 by NAT_4:9;
47 = 5*9 + 2;
then
A3: not 5 divides 47 by NAT_4:9;
47 = 7*6 + 5;
then
A4: not 7 divides 47 by NAT_4:9;
47 = 11*4 + 3;
then
A5: not 11 divides 47 by NAT_4:9;
47 = 13*3 + 8;
then
A6: not 13 divides 47 by NAT_4:9;
47 = 17*2 + 13;
then
A7: not 17 divides 47 by NAT_4:9;
47 = 19*2 + 9;
then
A8: not 19 divides 47 by NAT_4:9;
47 = 23*2 + 1;
then
A9: not 23 divides 47 by NAT_4:9;
assume 1<n & n*n<=47 & n is prime;
hence not n divides 47 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th27:
53 is prime
proof
now
let n be Element of NAT;
53 = 2*26 + 1;
then
A1: not 2 divides 53 by NAT_4:9;
53 = 3*17 + 2;
then
A2: not 3 divides 53 by NAT_4:9;
53 = 5*10 + 3;
then
A3: not 5 divides 53 by NAT_4:9;
53 = 7*7 + 4;
then
A4: not 7 divides 53 by NAT_4:9;
53 = 11*4 + 9;
then
A5: not 11 divides 53 by NAT_4:9;
53 = 13*4 + 1;
then
A6: not 13 divides 53 by NAT_4:9;
53 = 17*3 + 2;
then
A7: not 17 divides 53 by NAT_4:9;
53 = 19*2 + 15;
then
A8: not 19 divides 53 by NAT_4:9;
53 = 23*2 + 7;
then
A9: not 23 divides 53 by NAT_4:9;
assume 1<n & n*n<=53 & n is prime;
hence not n divides 53 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th28:
59 is prime
proof
now
let n be Element of NAT;
59 = 2*29 + 1;
then
A1: not 2 divides 59 by NAT_4:9;
59 = 3*19 + 2;
then
A2: not 3 divides 59 by NAT_4:9;
59 = 5*11 + 4;
then
A3: not 5 divides 59 by NAT_4:9;
59 = 7*8 + 3;
then
A4: not 7 divides 59 by NAT_4:9;
59 = 11*5 + 4;
then
A5: not 11 divides 59 by NAT_4:9;
59 = 13*4 + 7;
then
A6: not 13 divides 59 by NAT_4:9;
59 = 17*3 + 8;
then
A7: not 17 divides 59 by NAT_4:9;
59 = 19*3 + 2;
then
A8: not 19 divides 59 by NAT_4:9;
59 = 23*2 + 13;
then
A9: not 23 divides 59 by NAT_4:9;
assume 1<n & n*n<=59 & n is prime;
hence not n divides 59 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th29:
61 is prime
proof
now
let n be Element of NAT;
61 = 2*30 + 1;
then
A1: not 2 divides 61 by NAT_4:9;
61 = 3*20 + 1;
then
A2: not 3 divides 61 by NAT_4:9;
61 = 5*12 + 1;
then
A3: not 5 divides 61 by NAT_4:9;
61 = 7*8 + 5;
then
A4: not 7 divides 61 by NAT_4:9;
61 = 11*5 + 6;
then
A5: not 11 divides 61 by NAT_4:9;
61 = 13*4 + 9;
then
A6: not 13 divides 61 by NAT_4:9;
61 = 17*3 + 10;
then
A7: not 17 divides 61 by NAT_4:9;
61 = 19*3 + 4;
then
A8: not 19 divides 61 by NAT_4:9;
61 = 23*2 + 15;
then
A9: not 23 divides 61 by NAT_4:9;
assume 1<n & n*n<=61 & n is prime;
hence not n divides 61 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th30:
67 is prime
proof
now
let n be Element of NAT;
67 = 2*33 + 1;
then
A1: not 2 divides 67 by NAT_4:9;
67 = 3*22 + 1;
then
A2: not 3 divides 67 by NAT_4:9;
67 = 5*13 + 2;
then
A3: not 5 divides 67 by NAT_4:9;
67 = 7*9 + 4;
then
A4: not 7 divides 67 by NAT_4:9;
67 = 11*6 + 1;
then
A5: not 11 divides 67 by NAT_4:9;
67 = 13*5 + 2;
then
A6: not 13 divides 67 by NAT_4:9;
67 = 17*3 + 16;
then
A7: not 17 divides 67 by NAT_4:9;
67 = 19*3 + 10;
then
A8: not 19 divides 67 by NAT_4:9;
67 = 23*2 + 21;
then
A9: not 23 divides 67 by NAT_4:9;
assume 1<n & n*n<=67 & n is prime;
hence not n divides 67 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th31:
71 is prime
proof
now
let n be Element of NAT;
71 = 2*35 + 1;
then
A1: not 2 divides 71 by NAT_4:9;
71 = 3*23 + 2;
then
A2: not 3 divides 71 by NAT_4:9;
71 = 5*14 + 1;
then
A3: not 5 divides 71 by NAT_4:9;
71 = 7*10 + 1;
then
A4: not 7 divides 71 by NAT_4:9;
71 = 11*6 + 5;
then
A5: not 11 divides 71 by NAT_4:9;
71 = 13*5 + 6;
then
A6: not 13 divides 71 by NAT_4:9;
71 = 17*4 + 3;
then
A7: not 17 divides 71 by NAT_4:9;
71 = 19*3 + 14;
then
A8: not 19 divides 71 by NAT_4:9;
71 = 23*3 + 2;
then
A9: not 23 divides 71 by NAT_4:9;
assume 1<n & n*n<=71 & n is prime;
hence not n divides 71 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th32:
73 is prime
proof
now
let n be Element of NAT;
73 = 2*36 + 1;
then
A1: not 2 divides 73 by NAT_4:9;
73 = 3*24 + 1;
then
A2: not 3 divides 73 by NAT_4:9;
73 = 5*14 + 3;
then
A3: not 5 divides 73 by NAT_4:9;
73 = 7*10 + 3;
then
A4: not 7 divides 73 by NAT_4:9;
73 = 11*6 + 7;
then
A5: not 11 divides 73 by NAT_4:9;
73 = 13*5 + 8;
then
A6: not 13 divides 73 by NAT_4:9;
73 = 17*4 + 5;
then
A7: not 17 divides 73 by NAT_4:9;
73 = 19*3 + 16;
then
A8: not 19 divides 73 by NAT_4:9;
73 = 23*3 + 4;
then
A9: not 23 divides 73 by NAT_4:9;
assume 1<n & n*n<=73 & n is prime;
hence not n divides 73 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th33:
79 is prime
proof
now
let n be Element of NAT;
79 = 2*39 + 1;
then
A1: not 2 divides 79 by NAT_4:9;
79 = 3*26 + 1;
then
A2: not 3 divides 79 by NAT_4:9;
79 = 5*15 + 4;
then
A3: not 5 divides 79 by NAT_4:9;
79 = 7*11 + 2;
then
A4: not 7 divides 79 by NAT_4:9;
79 = 11*7 + 2;
then
A5: not 11 divides 79 by NAT_4:9;
79 = 13*6 + 1;
then
A6: not 13 divides 79 by NAT_4:9;
79 = 17*4 + 11;
then
A7: not 17 divides 79 by NAT_4:9;
79 = 19*4 + 3;
then
A8: not 19 divides 79 by NAT_4:9;
79 = 23*3 + 10;
then
A9: not 23 divides 79 by NAT_4:9;
assume 1<n & n*n<=79 & n is prime;
hence not n divides 79 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th34:
89 is prime
proof
now
let n be Element of NAT;
89 = 2*44 + 1;
then
A1: not 2 divides 89 by NAT_4:9;
89 = 3*29 + 2;
then
A2: not 3 divides 89 by NAT_4:9;
89 = 5*17 + 4;
then
A3: not 5 divides 89 by NAT_4:9;
89 = 7*12 + 5;
then
A4: not 7 divides 89 by NAT_4:9;
89 = 11*8 + 1;
then
A5: not 11 divides 89 by NAT_4:9;
89 = 13*6 + 11;
then
A6: not 13 divides 89 by NAT_4:9;
89 = 17*5 + 4;
then
A7: not 17 divides 89 by NAT_4:9;
89 = 19*4 + 13;
then
A8: not 19 divides 89 by NAT_4:9;
89 = 23*3 + 20;
then
A9: not 23 divides 89 by NAT_4:9;
assume 1<n & n*n<=89 & n is prime;
hence not n divides 89 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th35:
97 is prime
proof
now
let n be Element of NAT;
97 = 2*48 + 1;
then
A1: not 2 divides 97 by NAT_4:9;
97 = 3*32 + 1;
then
A2: not 3 divides 97 by NAT_4:9;
97 = 5*19 + 2;
then
A3: not 5 divides 97 by NAT_4:9;
97 = 7*13 + 6;
then
A4: not 7 divides 97 by NAT_4:9;
97 = 11*8 + 9;
then
A5: not 11 divides 97 by NAT_4:9;
97 = 13*7 + 6;
then
A6: not 13 divides 97 by NAT_4:9;
97 = 17*5 + 12;
then
A7: not 17 divides 97 by NAT_4:9;
97 = 19*5 + 2;
then
A8: not 19 divides 97 by NAT_4:9;
97 = 23*4 + 5;
then
A9: not 23 divides 97 by NAT_4:9;
assume 1<n & n*n<=97 & n is prime;
hence not n divides 97 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th36:
101 is prime
proof
now
let n be Element of NAT;
101 = 2*50 + 1;
then
A1: not 2 divides 101 by NAT_4:9;
101 = 3*33 + 2;
then
A2: not 3 divides 101 by NAT_4:9;
101 = 5*20 + 1;
then
A3: not 5 divides 101 by NAT_4:9;
101 = 7*14 + 3;
then
A4: not 7 divides 101 by NAT_4:9;
101 = 11*9 + 2;
then
A5: not 11 divides 101 by NAT_4:9;
101 = 13*7 + 10;
then
A6: not 13 divides 101 by NAT_4:9;
101 = 17*5 + 16;
then
A7: not 17 divides 101 by NAT_4:9;
101 = 19*5 + 6;
then
A8: not 19 divides 101 by NAT_4:9;
101 = 23*4 + 9;
then
A9: not 23 divides 101 by NAT_4:9;
assume 1<n & n*n<=101 & n is prime;
hence not n divides 101 by A1,A2,A3,A4,A5,A6,A7,A8,A9,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
begin :: Divisibility criteria for primes up to 101
theorem Th37:
for p being Prime, n,f,b being Nat st
(ex k being Nat st b*f + 1 = p*k)
& b > 1 & p,b are_coprime holds
p divides n iff p divides
value(mid(digits(n,b),2,len(digits(n,b))),b) - f*digits(n,b).0
proof
let p be Prime, n,f,b be Nat such that
A1: ex k being Nat st b*f + 1 = p*k and
A2: b > 1 and
A3: p,b are_coprime;
consider k being Nat such that
A4: b*f + 1 = p*k by A1;
thus p divides n implies p divides
value(mid(digits(n,b),2,len(digits(n,b))),b)
- f*digits(n,b).0
proof
assume p divides n; then
consider i being Nat such that
A5: n = p*i by NAT_D:def 3;
A6: b * value(mid(digits(n,b),2,len(digits(n,b))),b) +
digits(n,b).0 = p*i by A2,A5,Th19;
p*k*digits(n,b).0 = (b*f+1)*digits(n,b).0 by A4; then
A7: b*(value(mid(digits(n,b),2,len(digits(n,b))),b)
- f*digits(n,b).0)/b
= (p*(i - k*digits(n,b).0))/b by A6; then
value(mid(digits(n,b),2,len(digits(n,b))),b)
- f*digits(n,b).0
= (p*(i - k*digits(n,b).0))/b by A2,XCMPLX_1:89; then
b divides p*(i - k*digits(n,b).0) by A2,WSIERP_1:17; then
consider j being Integer such that
A8: i - (k*digits(n,b).0)=b*j by A3,INT_2:25,INT_1:def 3;
value(mid(digits(n,b),2,len(digits(n,b))),b) -
f*digits(n,b).0 = (p*(b*j))/b by A8,A7,A2,XCMPLX_1:89
.= p*j*(b/b)
.= p*j*1 by A2,XCMPLX_1:60;
hence p divides value(mid(digits(n,b),2,len(digits(n,b))),b)
- f*digits(n,b).0 by INT_1:def 3;
end;
assume p divides value(mid(digits(n,b),2,len(digits(n,b))),b) -
f*digits(n,b).0; then
consider i being Integer such that
A9: value(mid(digits(n,b),2,len(digits(n,b))),b) -
f*digits(n,b).0 = p*i by INT_1:def 3;
n = b*(p*i + f*digits(n,b).0) + digits(n,b).0 by A2,A9,Th19
.= b*p*i + (b*f+1)*(digits(n,b).0)
.= b*p*i + (p*k)*(digits(n,b).0) by A4
.= p*(b*i + k*(digits(n,b).0));
hence p divides n by INT_1:def 3;
end;
theorem Th38:
for p being Prime, n,f,b being Nat st
(ex k being Nat st b*f - 1 = p*k)
& b > 1 & p,b are_coprime holds
p divides n iff p divides
value(mid(digits(n,b),2,len(digits(n,b))),b) + f*digits(n,b).0
proof
let p be Prime, n,f,b be Nat such that
A1: ex k being Nat st b*f - 1 = p*k and
A2: b > 1 and
A3: p,b are_coprime;
consider k being Nat such that
A4: b*f - 1 = p*k by A1;
thus p divides n implies p divides
value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0
proof
assume p divides n; then
consider i being Nat such that
A5: n = p*i by NAT_D:def 3;
A6: b * value(mid(digits(n,b),2,len(digits(n,b))),b) +
digits(n,b).0 = p*i by A2,A5,Th19;
p*k*digits(n,b).0 = (b*f-1)*digits(n,b).0 by A4; then
A7: b*(value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0)/b
= (p*(i + k*digits(n,b).0))/b by A6; then
value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0
= (p*(i + k*digits(n,b).0))/b by A2,XCMPLX_1:89; then
b divides p*(i + k*digits(n,b).0) by A2,WSIERP_1:17; then
consider j being Integer such that
A8: i + (k*digits(n,b).0)=b*j by A3,INT_2:25,INT_1:def 3;
value(mid(digits(n,b),2,len(digits(n,b))),b) +
f*digits(n,b).0 = (p*(b*j))/b by A8,A7,A2,XCMPLX_1:89
.= p*j*(b/b)
.= p*j*1 by A2,XCMPLX_1:60;
hence p divides value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0 by INT_1:def 3;
end;
assume p divides value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0; then
consider i being Integer such that
A9: value(mid(digits(n,b),2,len(digits(n,b))),b)
+ f*digits(n,b).0 = p*i by INT_1:def 3;
n = b*(p*i - f*digits(n,b).0) + digits(n,b).0 by A2,A9,Th19
.= b*p*i - (b*f-1)*(digits(n,b).0)
.= b*p*i - (p*k)*(digits(n,b).0) by A4
.= p*(b*i - k*(digits(n,b).0));
hence p divides n by INT_1:def 3;
end;
::$N Divisibility rule#Divisibility by 7
::$L https://en.wikipedia.org/wiki/Divisibility_rule Divisibility rules
theorem Th39:
7 divides n iff 7 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 2*digits(n,10).0
proof
reconsider p=7 as Prime by NAT_4:26;
10*2 + 1 = p*3;
hence thesis by Th37,Th22;
end;
theorem
7 divides n iff 7 divides value(digits(n,10)/^1,10) - 2*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th39;
end;
theorem Th41:
11 divides n iff 11 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - digits(n,10).0
proof
reconsider p=11 as Prime by NAT_4:27;
A1: 10*1 + 1 = p*1;
p,10 are_coprime by EULER_1:2; then
11 divides n iff 11 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 1*digits(n,10).0
by Th37,A1;
hence thesis;
end;
theorem
11 divides n iff 11 divides value(digits(n,10)/^1,10) - digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th41;
end;
::$N Divisibility rule#Divisibility by 11
::$L https://en.wikipedia.org/wiki/Divisibility_rule Divisibility rules
theorem
11 divides n iff 11 divides
Sum SubXFinS(digits(n,10),EvenNAT) - Sum SubXFinS(digits(n,10),OddNAT)
proof
set d = digits(n,10);
consider p being XFinSequence of NAT such that
A1: dom p = dom d and
A2: for i being Nat st i in dom p holds p.i = (d.i)*(10|^i) and
A3: value(d,10) = Sum p by NUMERAL1:def 1;
set pe = SubXFinS(p,EvenNAT);
set po = SubXFinS(p,OddNAT);
A4: Sum pe + Sum po = Sum SubXFinS(p,NAT) by Th10,Th7,Th8
.= Sum p by Th11;
set de = SubXFinS(d,EvenNAT);
set dod = SubXFinS(d,OddNAT);
A5: dom pe = dom Sgm0(EvenNAT/\len d) by Th6,A1
.= dom de by Th6;
A6: dom po = dom Sgm0(OddNAT/\len d) by Th6,A1
.= dom dod by Th6;
A7: for i being Nat st i in dom de holds de.i = d.(2*i)
proof
set se = Sgm0 (EvenNAT /\ len d);
let i be Nat;
assume A8: i in dom de;
then A9: i in dom se & se.i in dom d by FUNCT_1:11;
thus de.i = d.(se.i) by A8,FUNCT_1:12
.= d.(2*i) by A9,Th12;
end;
A10: for i being Nat st i in dom pe holds pe.i = de.i * 10|^(2*i)
proof
set se = Sgm0 (EvenNAT /\ len p);
let i be Nat;
assume A11: i in dom pe;
then A12: i in dom se & se.i in dom p by FUNCT_1:11;
then A13: se.i = 2*i by Th12;
thus pe.i = p.(se.i) by A11,FUNCT_1:12
.= (d.(2*i))*(10|^(2*i)) by A12,A13,A2
.= (de.i)*(10|^(2*i)) by A12,A1,FUNCT_1:11,A7;
end;
A14: for i being Nat st i in dom dod holds dod.i = d.(2*i+1)
proof
set so = Sgm0 (OddNAT /\ len d);
let i be Nat;
assume A15: i in dom dod;
then A16: i in dom so & so.i in dom d by FUNCT_1:11;
thus dod.i = d.(so.i) by A15,FUNCT_1:12
.= d.(2*i+1) by A16,Th13;
end;
A17: for i being Nat st i in dom po holds po.i = dod.i * 10|^(2*i+1)
proof
set so = Sgm0 (OddNAT /\ len p);
let i be Nat;
assume A18: i in dom po;
then A19: i in dom so & so.i in dom p by FUNCT_1:11;
then A20: so.i = 2*i+1 by Th13;
thus po.i = p.(so.i) by A18,FUNCT_1:12
.= (d.(2*i+1))*(10|^(2*i+1)) by A19,A20,A2
.= (dod.i)*(10|^(2*i+1)) by A19,A1,FUNCT_1:11,A14;
end;
defpred E[set,set] means $2 = pe . $1 - de . $1;
A21: for k being Nat st k in Segm dom pe
ex x being Element of INT st E[k,x]
proof
let k be Nat;
assume k in Segm dom pe;
take pe.k - de.k;
thus thesis by INT_1:def 2;
end;
consider pede being XFinSequence of INT such that
A22: dom pede = Segm dom pe & for k being Nat st k in Segm dom pe
holds E[k,pede.k] from STIRL2_1:sch 5(A21);
now
let i be Nat;
reconsider dz = (10|^(2*i) - 1) as Nat by NAT_1:20,NEWTON:83;
assume A23: i in dom pede;
then pede . i = pe . i - de . i by A22
.= (de.i)*(10|^(2*i)) - de . i by A10,A23,A22
.= (de.i)*dz;
hence 11 divides pede.i by Th20,NAT_D:9;
end;
then 11 divides Sum pede by Th16;
then A24: Sum pede mod 11 = 0 by INT_1:62;
A25: len pede = len de by A22,A5;
A26: len pede = len pe by A22;
A27: for i being Nat st i in dom pe holds
pe.i = addint.(pede.i,de.i)
proof
let i be Nat;
assume A28: i in dom pe;
thus addint.(pede.i,de.i) = pede.i + de.i by BINOP_2:def 20
.= (pe.i - de.i) + de.i by A28,A22
.= pe.i;
end;
A29: Sum pe = addint "**" pe by AFINSQ_2:50
.= addint "**" pede^de by A25,A26,A27,AFINSQ_2:46
.= Sum (pede^de) by AFINSQ_2:50
.= Sum pede + Sum de by AFINSQ_2:55;
defpred O[set,set] means $2 = po . $1 + dod . $1;
A30: for k being Nat st k in Segm dom po
ex x being Element of NAT st O[k,x];
consider podo being XFinSequence of NAT such that
A31: dom podo = Segm dom po & for k being Nat st k in Segm dom po holds
O[k,podo.k] from STIRL2_1:sch 5(A30);
now
let i be Nat;
reconsider dz = (10|^(2*i) - 1) as Nat by NAT_1:20,NEWTON:83;
assume A32: i in dom podo;
then podo . i = po . i + dod . i by A31
.= (dod.i)*(10|^(2*i+1)) + dod . i by A17,A32,A31
.= (dod.i)*(10|^(2*i+1) + 1);
hence 11 divides podo.i by Th21,NAT_D:9;
end;
then 11 divides Sum podo by Th16;
then A33: Sum podo mod 11 = 0 by INT_1:62;
set mdo = (-1)(#)dod;
A34: len podo = len mdo by A31,A6,VALUED_1:def 5;
A35: len podo = len po by A31;
A36: for i being Nat st i in dom po holds
po.i = addint.(podo.i,mdo.i)
proof
let i be Nat;
assume A37: i in dom po;
then A38: i in dom mdo by A6,VALUED_1:def 5;
thus addint.(podo.i,mdo.i) = podo.i + mdo.i by BINOP_2:def 20
.= podo.i + (-1) * dod.i by A38,VALUED_1:def 5
.= (po.i + dod.i) - dod.i by A37,A31
.= po.i;
end;
A39: Sum po = addint "**" po by AFINSQ_2:50
.= addint "**" podo^mdo by A34,A35,A36,AFINSQ_2:46
.= Sum (podo^mdo) by AFINSQ_2:50
.= Sum podo + Sum mdo by AFINSQ_2:55
.= Sum podo + (-1) * Sum dod by AFINSQ_2:64
.= Sum podo - Sum dod;
thus 11 divides n implies
11 divides Sum de - Sum dod
proof
assume 11 divides n;
then 11 divides Sum p by A3,NUMERAL1:5;
then 0 = ((Sum pede + Sum podo) + (Sum de - Sum dod)) mod 11
by INT_1:62,A4,A29,A39
.= (((Sum pede + Sum podo) mod 11) +
((Sum de - Sum dod) mod 11)) mod 11 by NAT_D:66
.= ((((Sum pede mod 11) + (Sum podo mod 11)) mod 11) +
((Sum de - Sum dod) mod 11)) mod 11 by NAT_D:66
.= (0 qua Integer + ((Sum de - Sum dod) mod 11)) mod 11
by A24,A33,NAT_D:26
.= (Sum de - Sum dod) mod 11 by Th14;
hence 11 divides Sum de - Sum dod by INT_1:62;
end;
thus 11 divides Sum de - Sum dod
implies 11 divides n
proof
assume 11 divides Sum de - Sum dod;
then 0 = (Sum de - Sum dod) mod 11 by INT_1:62
.= (0 qua Integer + ((Sum de - Sum dod) mod 11)) mod 11 by Th14
.= ((((Sum pede mod 11) + (Sum podo mod 11)) mod 11) +
((Sum de - Sum dod) mod 11)) mod 11 by A24,A33,NAT_D:26
.= (((Sum pede + Sum podo) mod 11) +
((Sum de - Sum dod) mod 11)) mod 11 by NAT_D:66
.= ((Sum pede + Sum podo) + (Sum de - Sum dod)) mod 11 by NAT_D:66
.= n mod 11 by A4,A29,A39,A3,NUMERAL1:5;
hence 11 divides n by INT_1:62;
end;
end;
::$N Divisibility rule#Divisibility by 13
::$L https://en.wikipedia.org/wiki/Divisibility_rule Divisibility rules
theorem Th44:
13 divides n iff 13 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 4*digits(n,10).0
proof
reconsider p=13 as Prime by NAT_4:28;
A1: 10*4 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
13 divides n iff 13 divides value(digits(n,10)/^1,10) + 4*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th44;
end;
theorem Th46:
17 divides n iff 17 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 5*digits(n,10).0
proof
reconsider p=17 as Prime by PEPIN:60;
A1: 10*5 + 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
17 divides n iff 17 divides value(digits(n,10)/^1,10) - 5*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th46;
end;
theorem Th48:
19 divides n iff 19 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 2*digits(n,10).0
proof
reconsider p=19 as Prime by NAT_4:29;
A1: 10*2 - 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
19 divides n iff 19 divides value(digits(n,10)/^1,10) + 2*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th48;
end;
theorem Th50:
23 divides n iff 23 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 7*digits(n,10).0
proof
reconsider p=23 as Prime by NAT_4:30;
A1: 10*7 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
23 divides n iff 23 divides value(digits(n,10)/^1,10) + 7*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th50;
end;
theorem Th52:
29 divides n iff 29 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 3*digits(n,10).0
proof
reconsider p=29 as Prime by Th23;
A1: 10*3 - 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
29 divides n iff 29 divides value(digits(n,10)/^1,10) + 3*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th52;
end;
theorem Th54:
31 divides n iff 31 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 3*digits(n,10).0
proof
reconsider p=31 as Prime by Th24;
A1: 10*3 + 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
31 divides n iff 31 divides value(digits(n,10)/^1,10) - 3*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th54;
end;
theorem Th56:
37 divides n iff 37 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 11*digits(n,10).0
proof
reconsider p=37 as Prime by NAT_4:31;
A1: 10*11 + 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
37 divides n iff 37 divides value(digits(n,10)/^1,10) - 11*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th56;
end;
theorem Th58:
41 divides n iff 41 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 4*digits(n,10).0
proof
reconsider p=41 as Prime by Th25;
A1: 10*4 + 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
41 divides n iff 41 divides value(digits(n,10)/^1,10) - 4*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th58;
end;
theorem Th60:
43 divides n iff 43 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 13*digits(n,10).0
proof
reconsider p=43 as Prime by NAT_4:32;
A1: 10*13 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
43 divides n iff 43 divides value(digits(n,10)/^1,10) + 13*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th60;
end;
theorem Th62:
47 divides n iff 47 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 14*digits(n,10).0
proof
reconsider p=47 as Prime by Th26;
A1: 10*14 + 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
47 divides n iff 47 divides value(digits(n,10)/^1,10) - 14*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th62;
end;
theorem Th64:
53 divides n iff 53 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 16*digits(n,10).0
proof
reconsider p=53 as Prime by Th27;
A1: 10*16 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
53 divides n iff 53 divides value(digits(n,10)/^1,10) + 16*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th64;
end;
theorem Th66:
59 divides n iff 59 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 6*digits(n,10).0
proof
reconsider p=59 as Prime by Th28;
A1: 10*6 - 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
59 divides n iff 59 divides value(digits(n,10)/^1,10) + 6*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th66;
end;
theorem Th68:
61 divides n iff 61 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 6*digits(n,10).0
proof
reconsider p=61 as Prime by Th29;
A1: 10*6 + 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
61 divides n iff 61 divides value(digits(n,10)/^1,10) - 6*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th68;
end;
theorem Th70:
67 divides n iff 67 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 20*digits(n,10).0
proof
reconsider p=67 as Prime by Th30;
A1: 10*20 + 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
67 divides n iff 67 divides value(digits(n,10)/^1,10) - 20*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th70;
end;
theorem Th72:
71 divides n iff 71 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 7*digits(n,10).0
proof
reconsider p=71 as Prime by Th31;
A1: 10*7 + 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
71 divides n iff 71 divides value(digits(n,10)/^1,10) - 7*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th72;
end;
theorem Th74:
73 divides n iff 73 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 22*digits(n,10).0
proof
reconsider p=73 as Prime by Th32;
A1: 10*22 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
73 divides n iff 73 divides value(digits(n,10)/^1,10) + 22*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th74;
end;
theorem Th76:
79 divides n iff 79 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 8*digits(n,10).0
proof
reconsider p=79 as Prime by Th33;
A1: 10*8 - 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
79 divides n iff 79 divides value(digits(n,10)/^1,10) + 8*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th76;
end;
theorem Th78:
83 divides n iff 83 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 25*digits(n,10).0
proof
reconsider p=83 as Prime by NAT_4:33;
A1: 10*25 - 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
83 divides n iff 83 divides value(digits(n,10)/^1,10) + 25*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th78;
end;
theorem Th80:
89 divides n iff 89 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) + 9*digits(n,10).0
proof
reconsider p=89 as Prime by Th34;
A1: 10*9 - 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th38,A1;
end;
theorem
89 divides n iff 89 divides value(digits(n,10)/^1,10) + 9*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th80;
end;
theorem Th82:
97 divides n iff 97 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 29*digits(n,10).0
proof
reconsider p=97 as Prime by Th35;
A1: 10*29 + 1 = p*3;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
97 divides n iff 97 divides value(digits(n,10)/^1,10) - 29*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th82;
end;
theorem Th84:
101 divides n iff 101 divides
value(mid(digits(n,10),2,len(digits(n,10))),10) - 10*digits(n,10).0
proof
reconsider p=101 as Prime by Th36;
A1: 10*10 + 1 = p*1;
p,10 are_coprime by EULER_1:2;
hence thesis by Th37,A1;
end;
theorem
101 divides n iff 101 divides value(digits(n,10)/^1,10) - 10*digits(n,10).0
proof
digits(n,10)/^1=mid(digits(n,10),2,len(digits(n,10))) by Th3;
hence thesis by Th84;
end;