:: Elementary Number Theory Problems. Part III
:: by Artur Korni{\l}owicz
::
:: Received July 23, 2022
:: Copyright (c) 2022-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, NAT_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_3, XCMPLX_0,
CARD_1, INT_1, NEWTON, INT_2, ARYTM_1, SUBSET_1, XBOOLE_0, TARSKI,
FINSET_1, PBOOLE, COMPLEX1, ABIAN, NAT_6, SQUARE_1, EULER_1, MEMBERED,
ZFMISC_1, ORDINAL1, POWER, PREPOWER, NUMBER03, FUNCT_3, REAL_1, SERIES_1,
PARTFUN3, VALUED_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PBOOLE, FINSET_1, MEMBERED,
VALUED_0, PARTFUN3, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, XXREAL_0,
PREPOWER, POWER, SQUARE_1, NEWTON, ABIAN, QUIN_1, EULER_1, SERIES_1,
NAT_6;
constructors NAT_D, RELSET_1, NEWTON, ABIAN, NAT_6, ENUMSET1, EULER_1, PEPIN,
PYTHTRIP, PREPOWER, QUIN_1, SERIES_1, PARTFUN3;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, CARD_1, SQUARE_1, NEWTON,
NEWTON02, NEWTON03, FOMODEL0, ABIAN, NAT_6, JORDAN1D, POWER, SERIES_1,
LIOUVIL1, WSIERP_1, QUIN_1, AFINSQ_2, NAT_5;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RELAT_1, MEMBERED, TARSKI, XBOOLE_0, NAT_D, INT_2, SEQM_3;
equalities SQUARE_1, NAT_6, QUIN_1, ORDINAL1;
expansions ORDINAL1, INT_1, INT_2, ZFMISC_1;
theorems NEWTON, WSIERP_1, INT_1, INT_2, NEWTON02, NAT_D, NEWTON03, PEPIN,
EULER_2, NUMBER02, NAT_4, ORDINAL1, XREAL_1, XXREAL_0, NAT_1, INT_4,
XCMPLX_1, WEDDWITT, NAT_3, XBOOLE_0, INT_6, PYTHTRIP, FUNCT_1, PARTFUN1,
INT_5, ABSVALUE, NAT_6, TARSKI, POLYEQ_5, NAT_5, EULER_1, ENUMSET1,
CARD_1, POWER, PREPOWER, SEQM_3, PARTFUN3, NUMPOLY1, NEWTON05, POLYFORM,
QUIN_1, GLIBPRE0, SERIES_1, FIB_NUM, SEQ_1, XPRIMES0;
schemes NAT_1, PBOOLE;
begin :: Preliminaries
registration
cluster natural -> natural-membered for set;
coherence
proof
let X be set;
assume X is natural;
then reconsider X as Nat;
let x be object;
X c= omega;
hence thesis;
end;
end;
reserve a,b,i,k,m,n for Nat;
reserve s,z for non zero Nat;
reserve r for Real;
reserve c for Complex;
reserve e1,e2,e3,e4,e5 for ExtReal;
theorem Th1:
e1 <= e2 <= e3 <= e4 implies e1 <= e4
proof
assume e1 <= e2 <= e3;
then e1 <= e3 by XXREAL_0:2;
hence thesis by XXREAL_0:2;
end;
theorem Th2:
e1 <= e2 <= e3 <= e4 <= e5 implies e1 <= e5
proof
assume e1 <= e2 <= e3 <= e4;
then e1 <= e4 by Th1;
hence thesis by XXREAL_0:2;
end;
theorem
2|^10+1 = 1025
proof
thus 2|^10+1 = 2*2*2*2*2*2*2*2*2*2+1 by NUMBER02:6
.= 1025;
end;
theorem Th4:
3|^10+1 = 5905 * 10
proof
thus 3|^10+1 = 3*3*3*3*3*3*3*3*3*3+1 by NUMBER02:6
.= 5905 * 10;
end;
theorem Th5:
4|^10+1 = 1048*1000+577 :: 1 048 577
proof
thus 4|^10+1 = 4*4*4*4*4*4*4*4*4*4+1 by NUMBER02:6
.= 1048*1000+577;
end;
theorem Th6:
5|^10+1 = 9765*1000+626 :: 9 765 626
proof
thus 5|^10+1 = 5*5*5*5*5*5*5*5*5*5+1 by NUMBER02:6
.= 9765*1000+626;
end;
theorem Th7:
6|^10+1 = 6046*10000+6177 :: 60 466 177
proof
thus 6|^10+1 = 6*6*6*6*6*6*6*6*6*6+1 by NUMBER02:6
.= 6046*10000+6177;
end;
theorem Th8:
7|^10+1 = (2824*10000+7525) * 10 :: 282 475 250
proof
thus 7|^10+1 = 7*7*7*7*7*7*7*7*7*7+1 by NUMBER02:6
.= (2824*10000+7525) * 10;
end;
theorem Th9:
8|^10+1 = (1073*100+74)*10000+1825 :: 1 073 741 825
proof
thus 8|^10+1 = 8*8*8*8*8*8*8*8*8*8+1 by NUMBER02:6
.= (1073*100+74)*10000+1825;
end;
theorem Th10:
9|^10+1 = (3486*100+78)*10000+4402 :: 3 486 784 402
proof
thus 9|^10+1 = 9*9*9*9*9*9*9*9*9*9+1 by NUMBER02:6
.= (3486*100+78)*10000+4402;
end;
Lm1: 1 mod 3 = 1 by NAT_D:24;
Lm2: 2 mod 3 = 2 by NAT_D:24;
Lm3: (3*1+1) mod 3 = 1 mod 3 by NAT_D:21;
Lm4: (3*5+1) mod 3 = 1 mod 3 by NAT_D:21;
Lm5: (3*10+2) mod 3 = 2 mod 3 by NAT_D:21;
Lm6: 1 mod 4 = 1 by NAT_D:24;
Lm7: 2 mod 4 = 2 by NAT_D:24;
Lm8: 3 mod 4 = 3 by NAT_D:24;
Lm9: (3*5+1) mod 5 = 1 mod 5 by NAT_D:21;
Lm10: (1*5+2) mod 5 = 2 mod 5 by NAT_D:21;
Lm11: (1*5+3) mod 5 = 3 mod 5 by NAT_D:21;
Lm12: (6*5+2) mod 5 = 2 mod 5 by NAT_D:21;
Lm13: 1 mod 5 = 1 by NAT_D:24;
Lm14: 2 mod 5 = 2 by NAT_D:24;
Lm15: 3 mod 5 = 3 by NAT_D:24;
Lm16: 4 mod 5 = 4 by NAT_D:24;
theorem Th11:
for n being Integer holds n mod (m+1) = 0 or ... or n mod (m+1) = m
proof
let n be Integer;
reconsider i = n mod (m+1) as Element of NAT by INT_1:3;
take i;
thus 0 <= i;
i < m + 1 by INT_1:58;
hence i <= m by NAT_1:13;
thus thesis;
end;
Lm17:
not 3 divides a or a mod 3 <> 0 implies a mod 3 = 1 or a mod 3 = 2
proof
a mod 3 < 2+1 by INT_1:58;
then a mod 3 <= 2 by NAT_1:13;
then a mod 3 = 0 or ... or a mod 3 = 2;
hence thesis by INT_1:62;
end;
Lm18:
not 5 divides a or a mod 5 <> 0 implies
a mod 5 = 1 or a mod 5 = 2 or a mod 5 = 3 or a mod 5 = 4
proof
a mod 5 < 4+1 by INT_1:58;
then a mod 5 <= 4 by NAT_1:13;
then a mod 5 = 0 or ... or a mod 5 = 4;
hence thesis by INT_1:62;
end;
theorem Th12:
n divides 8 implies n in {1,2,4,8}
proof
assume
A1: n divides 8;
then n <= 8 by INT_2:27;
then
A2: n = 0 or ... or n = 8;
n <> 0 by A1;
A3: 8 mod n = 0 by A1;
(3*2+2) mod 3 = 2 mod 3 & (5*1+3) mod 5 = 3 mod 5 &
(6*1+2) mod 6 = 2 mod 6 & (7*1+1) mod 7 = 1 mod 7 by NAT_D:21;
hence thesis by A1,A2,ENUMSET1:def 2,NAT_D:24;
end;
theorem Th13:
0 < m implies m gcd n <= m
proof
m gcd n divides m by INT_2:def 2;
hence thesis by INT_2:27;
end;
theorem Th14:
for i,j being Integer st i,j are_coprime holds
i <> j or i = j = 1 or i = j = -1
proof
let i,j be Integer;
A1: i gcd i = |.i.| by INT_5:12;
|.i.| = i or |.i.| = -i by ABSVALUE:1;
hence thesis by A1;
end;
theorem
for i,j being Nat st i,j are_coprime holds i <> j or i = j = 1 by Th14;
theorem Th16:
a < n & b < n & n divides a-b implies a = b
proof
assume that
A1: a < n and
A2: b < n and
A3: n divides a-b;
A4: n divides -(a-b) by A3,INT_2:10;
assume a <> b;
then a > b or b > a by XXREAL_0:1;
then a-b > 0 or b-a > 0 by XREAL_1:50;
then n <= a-b or n <= b-a by A3,A4,INT_2:27;
then a < a-b or b < b-a by A1,A2,XXREAL_0:2;
hence thesis by XREAL_1:43;
end;
theorem Th17:
for a,b,m being Integer st a < b
ex k st m < (b-a)*k+1-a & k = |. [/ (m+a-1)/(b-a) + 1 \] .|
proof
let a,b,m be Integer;
assume a < b;
then
A1: a-a < b-a by XREAL_1:14;
set x = (m+a-1)/(b-a) + 1;
A2: (b-a)*x/(b-a) = x by A1,XCMPLX_1:89;
A3: now
assume m >= (b-a)*x+1-a;
then m+a >= (b-a)*x+1-a+a by XREAL_1:6;
then m+a-1 >= (b-a)*x+1-1 by XREAL_1:9;
then (m+a-1)/(b-a) >= x+0 by A1,A2,XREAL_1:72;
hence contradiction by XREAL_1:8;
end;
take k = |.[/x\].|;
A4: x <= [/x\] by INT_1:def 7;
[/x\] <= k by ABSVALUE:4;
then x <= k by A4,XXREAL_0:2;
then (b-a)*x <= (b-a)*k by A1,XREAL_1:64;
then (b-a)*x+1 <= (b-a)*k+1 by XREAL_1:6;
then (b-a)*x+1-a <= (b-a)*k+1-a by XREAL_1:9;
hence thesis by A3,XXREAL_0:2;
end;
Lm19:
not 2 divides 1025
proof
1025 = 2*512+1;
hence thesis;
end;
Lm20:
not 2 divides 1048*1000+577
proof
1048*1000+577 = 2*(5242*100+88)+1;
hence thesis;
end;
Lm21:
not 5 divides 9765*1000+626
proof
9765*1000+626 = 5*(1953*1000+125)+1;
hence thesis by NUMBER02:33;
end;
Lm22:
not 2 divides 6046*10000+6177
proof
6046*10000+6177 = 2*(3023*10000+3088)+1;
hence thesis;
end;
Lm23:
not 2 divides (1073*100+74)*10000+1825
proof
(1073*100+74)*10000+1825 = 2*((536*100+87)*10000+912)+1;
hence thesis;
end;
Lm24:
not 5 divides (3486*100+78)*10000+4402
proof
(3486*100+78)*10000+4402 = 5*((6973*10+5)*10000+6880)+2;
hence thesis by NUMBER02:33;
end;
Lm25: not 2*5 divides 1025 by Lm19,NEWTON03:11;
Lm26: not 2*5 divides 1048*1000+577 by Lm20,NEWTON03:11;
Lm27: not 2*5 divides 9765*1000+626 by Lm21,NEWTON03:11;
Lm28: not 2*5 divides 6046*10000+6177 by Lm22,NEWTON03:11;
Lm29: not 2*5 divides (1073*100+74)*10000+1825 by Lm23,NEWTON03:11;
Lm30: not 2*5 divides (3486*100+78)*10000+4402 by Lm24,NEWTON03:11;
registration
let i be Integer;
cluster i GeoSeq -> INT-valued;
coherence
proof
set f = i GeoSeq;
let y be object;
assume y in rng f;
then consider x being object such that
A1: x in dom f and
A2: y = f.x by FUNCT_1:def 3;
A3: dom f = NAT by SEQ_1:1;
defpred P[Nat] means f.$1 in INT;
f.0 = 1 by PREPOWER:3;
then
A4: P[0] by INT_1:def 1;
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
f.(k+1) = f.k * i by PREPOWER:3;
then f.(k+1) is integer by A6;
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis by A1,A2,A3;
end;
end;
registration
let n;
cluster n GeoSeq -> NAT-valued;
coherence
proof
set f = n GeoSeq;
let y be object;
assume y in rng f;
then consider x being object such that
A1: x in dom f and
A2: y = f.x by FUNCT_1:def 3;
A3: dom f = NAT by SEQ_1:1;
defpred P[Nat] means f.$1 in NAT;
f.0 = 1 by PREPOWER:3;
then
A4: P[0];
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
f.(k+1) = f.k * n by PREPOWER:3;
then f.(k+1) is natural by A6;
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis by A1,A2,A3;
end;
end;
registration
let f be nonnegative-yielding real-valued ManySortedSet of NAT;
cluster Partial_Sums(f) -> non-decreasing;
coherence
proof
set P = Partial_Sums(f);
let m,n;
assume m in dom P & n in dom P;
defpred P[Nat] means m <= $1 implies P.m <= P.$1;
A1: P[0];
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
assume m <= k+1;
then per cases by NAT_1:8;
suppose
A4: m <= k;
A5: P.(k+1) = P.k + f.(k+1) by SERIES_1:def 1;
dom f = NAT by PARTFUN1:def 2;
then f.(k+1) in rng f by FUNCT_1:def 3;
then P.k + 0 <= P.k + f.(k+1) by XREAL_1:6,PARTFUN3:def 4;
hence thesis by A3,A4,A5,XXREAL_0:2;
end;
suppose m = k+1;
hence thesis;
end;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th18:
a <> 0 or b <> 0 implies
ex A,B being Nat st a = (a gcd b)*A & b = (a gcd b)*B & A,B are_coprime
proof
set d = a gcd b;
assume
A1: a <> 0 or b <> 0;
then consider A,B being Integer such that
A2: a = d*A & b = d*B and
A3: A,B are_coprime by INT_2:23;
0 <= A & 0 <= B by A1,A2;
then reconsider A,B as Element of NAT by INT_1:3;
take A,B;
thus thesis by A2,A3;
end;
theorem Th19:
n <> 0 implies
for p,m being Integer st p divides m holds p divides (m GeoSeq).n
proof
assume
A1: n <> 0;
let p,m be Integer such that
A2: p divides m;
set G = m GeoSeq;
defpred P[Nat] means $1 <> 0 implies p divides G.$1;
A3: G.0 = 1 by PREPOWER:3;
G.(0+1) = G.0 * m by PREPOWER:3;
then
A4: P[1] by A2,A3;
A5: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
G.(k+1) = G.k * m by PREPOWER:3;
hence thesis by INT_2:2;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A4,A5);
hence thesis by A1;
end;
theorem Th20:
(r GeoSeq).(a+b) = (r GeoSeq).a * r|^b
proof
set S = r GeoSeq;
defpred P[Nat] means S.(a+$1) = S.a * r|^$1;
A1: P[0]
proof
r|^0 = 1 by NEWTON:4;
hence thesis;
end;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
a+(k+1) = a+k+1;
hence S.(a+(k+1)) = S.(a+k) * r|^1 by PREPOWER:3
.= S.a * (r|^k * r) by A3
.= S.a * r|^(k+1) by NEWTON:6;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th21:
for p,m being Integer st p divides m holds
p divides (Partial_Sums (m GeoSeq)).n - 1
proof
let p,m be Integer such that
A1: p divides m;
set G = m GeoSeq;
set P = Partial_Sums G;
defpred P[Nat] means p divides P.$1 - 1;
P.0 = G.0 by SERIES_1:def 1
.= 1 by PREPOWER:3;
then
A2: P[0] by INT_2:12;
A3: for k st P[k] holds P[k+1]
proof
let k such that
A4: P[k];
A5: P.(k+1) = P.k + G.(k+1) by SERIES_1:def 1;
p divides G.(k+1) by A1,Th19;
then p divides P.k - 1 + G.(k+1) by A4,WSIERP_1:4;
hence P[k+1] by A5;
end;
for k holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th22:
(Partial_Sums (m GeoSeq)).n, m|^(n+1) are_coprime
proof
set P = (Partial_Sums (m GeoSeq)).n;
assume not thesis;
then consider p being Prime such that
A1: p divides P and
A2: p divides m|^(n+1) by PYTHTRIP:def 2;
p divides P - 1 by A2,Th21,NAT_3:5;
then p divides P - (P-1) by A1,INT_5:1;
then p = 1 by WSIERP_1:15;
hence thesis by INT_2:def 4;
end;
theorem Th23:
(Partial_Sums(a GeoSeq)).k gcd (Partial_Sums(a GeoSeq)).(k+i)
= (Partial_Sums(a GeoSeq)).k
gcd ( (Partial_Sums(a GeoSeq)).(k+i) - (Partial_Sums(a GeoSeq)).k )
proof
set P = Partial_Sums(a GeoSeq);
reconsider N = P.(k+i) - P.k as Element of NAT by INT_1:5,SEQM_3:5;
P.(k+i) = P.k + N;
hence thesis by FIB_NUM:1;
end;
theorem Th24:
(Partial_Sums(r GeoSeq)).(k+i+1) - (Partial_Sums(r GeoSeq)).k
= r|^(k+1) * (Partial_Sums(r GeoSeq)).i
proof
set S = r GeoSeq;
set P = Partial_Sums(S);
defpred P[Nat] means P.(k+$1+1) - P.k = r|^(k+1) * P.$1;
A1: P[0]
proof
A2: P.0 = (r GeoSeq).0 by SERIES_1:def 1
.= 1 by PREPOWER:3;
P.(k+1) = P.k + S.(k+1) by SERIES_1:def 1;
hence thesis by A2,PREPOWER:def 1;
end;
A3: for a st P[a] holds P[a+1]
proof
let a such that
A4: P[a];
A5: P.(a+1) = P.a + S.(a+1) by SERIES_1:def 1;
A6: S.(k+(a+1)) = S.(a+1) * r|^k by Th20;
A7: S.(k+(a+1)+1) = S.(k+(a+1)) * r by PREPOWER:3
.= S.(a+1) * (r|^k * r) by A6
.= r|^(k+1) * S.(a+1) by NEWTON:6;
P.(k+(a+1)+1) = P.(k+(a+1)) + S.(k+(a+1)+1) by SERIES_1:def 1;
hence P.(k+(a+1)+1) - P.k = P.(k+(a+1)) - P.k + S.(k+(a+1)+1)
.= r|^(k+1) * P.a + S.(k+(a+1)+1) by A4
.= r|^(k+1) * P.(a+1) by A5,A7;
end;
for k holds P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
Lm31:
for x being Nat st n+1,m+1 are_coprime & n < m holds
(Partial_Sums(x GeoSeq)).n, (Partial_Sums(x GeoSeq)).m are_coprime
proof
let x be Nat;
assume that
A1: n+1,m+1 are_coprime and
A2: n < m;
set P = Partial_Sums(x GeoSeq);
A3: P.0 = (x GeoSeq).0 by SERIES_1:def 1
.= 1 by PREPOWER:3;
defpred P[Nat] means
for z being Nat st $1+1,$1+z+1 are_coprime holds P.$1,P.($1+z) are_coprime;
A4: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
let k be Nat such that
A5: for n being Nat st n < k holds P[n];
defpred Q[Nat] means
k+1,k+$1+1 are_coprime implies P.k,P.(k+$1) are_coprime;
A6: for i being Nat st for n being Nat st n < i holds Q[n] holds Q[i]
proof
let i be Nat such that
A7: for n being Nat st n < i holds Q[n] and
A8: k+1,k+i+1 are_coprime;
k+1+0 <> k+1+i or k+1 = k+i+1 = 0+1 by A8,Th14;
then per cases;
suppose k = i = 0;
hence P.k gcd P.(k+i) = 1 by A3;
end;
suppose i <> 0;
then reconsider i1 = i - 1 as Element of NAT by INT_1:5,NAT_1:14;
A9: k+i+1 = k+1+i;
then
A10: (k+1) gcd i = 1 by A8,FIB_NUM:1;
A11: P.k, x|^(k+1) are_coprime by Th22;
A12: P.(k+i1+1) - P.k = x|^(k+1) * P.i1 by Th24;
A13: P.k gcd P.(k+i) = P.k gcd (P.(k+i) - P.k) by Th23
.= P.k gcd P.i1 by A11,A12,FIB_NUM:2;
now
per cases by XXREAL_0:1;
suppose
A14: i1 < k;
then reconsider z = k-i1 as Element of NAT by INT_1:5;
i1+1,i1+z+1 are_coprime implies P.i1,P.(i1+z) are_coprime
by A14,A5;
hence P.k gcd P.i1 = 1 by A8,A9,FIB_NUM:1;
end;
suppose i1 > k;
then consider j being Nat such that
A15: i1 = k+j by NAT_1:10;
A16: j = i-(1+k) by A15;
k+1,k+j+1 are_coprime by A8,A9,A15,FIB_NUM:1;
then P.k,P.(k+j) are_coprime by A16,A7,XREAL_1:44;
hence P.k gcd P.i1 = 1 by A15;
end;
suppose
A17: i1 = k;
then (k+1) gcd i = i by NAT_D:32;
hence P.k gcd P.i1 = 1 by A10,A3;
end;
end;
hence P.k gcd P.(k+i) = 1 by A13;
end;
end;
for k being Nat holds Q[k] from NAT_1:sch 4(A6);
hence P[k];
end;
A18: for k being Nat holds P[k] from NAT_1:sch 4(A4);
reconsider z = m-n as Element of NAT by A2,INT_1:5;
m = z+n;
hence thesis by A1,A18;
end;
theorem Th25:
n+1,m+1 are_coprime implies
(Partial_Sums(a GeoSeq)).n, (Partial_Sums(a GeoSeq)).m are_coprime
proof
assume
A1: n+1,m+1 are_coprime;
A2: Partial_Sums(a GeoSeq).0 = (a GeoSeq).0 by SERIES_1:def 1
.= 1 by PREPOWER:3;
n+1 <> m+1 or n+1 = m+1 = 1 by A1,Th14;
then per cases by XXREAL_0:1;
suppose n < m or m < n;
hence thesis by A1,Lm31;
end;
suppose n = m = 0;
hence thesis by A2;
end;
end;
theorem Th26:
a <> 0 & b <> 0 & i <> 0 implies (i|^a - 1) gcd (i|^b - 1) = i|^(a gcd b) - 1
proof
set d = a gcd b;
assume that
A1: a <> 0 & b <> 0 and
A2: i <> 0;
1 <= i by A2,NAT_1:14;
then per cases by XXREAL_0:1;
suppose
A3: i = 1;
then (i|^a - 1) gcd (i|^b - 1) = 0 gcd (1|^b-1)
.= i|^(a gcd b) - 1 by A3;
hence thesis;
end;
suppose
A4: 1 < i;
consider A,B being Nat such that
A5: a = d*A and
A6: b = d*B and
A7: A,B are_coprime by A1,Th18;
A <> 0 & B <> 0 by A1,A5,A6;
then reconsider a1 = A-1, b1 = B-1 as Nat;
set x = i|^d;
set P = Partial_Sums(x GeoSeq);
A = a1+1 & B = b1+1;
then P.a1,P.b1 are_coprime by A7,Th25;
then
A8: (x-1)*(P.a1 gcd P.b1) = x-1;
A9: 1 <= d by A1,NAT_1:14;
1+1 <= i by A4,NAT_1:13;
then
A10: x > d by NEWTON:86;
then
A11: x-1 <> 1-1 by A9;
A12: |.x-1.| = x-1 by A4,ABSVALUE:def 1;
P.a1 = (1 - x to_power (a1+1)) / (1-x) by A9,A10,SERIES_1:22
.= (-(1 - x to_power (a1+1))) / -(1-x) by XCMPLX_1:191
.= (x to_power A - 1) / (x-1);
then
A13: (P.a1)*(x-1) = x|^A-1 by A11,XCMPLX_1:87;
P.b1 = (1 - x to_power (b1+1)) / (1-x) by A9,A10,SERIES_1:22
.= (-(1 - x to_power (b1+1))) / -(1-x) by XCMPLX_1:191
.= (x to_power B - 1) / (x-1);
then
A14: (P.b1)*(x-1) = x|^B-1 by A11,XCMPLX_1:87;
i|^a = x|^A & i|^b = x|^B by A5,A6,NEWTON:9;
hence (i|^a - 1) gcd (i|^b - 1) = i|^d - 1 by A8,A13,A14,A12,INT_6:16;
end;
end;
theorem
for a,b,k being Integer st a+b > 0 & (a mod k)+(b mod k) > 0 holds
((a+b) to_power n) mod k = (((a mod k) + (b mod k)) to_power n) mod k
proof
let a,b,k be Integer;
set ak = a mod k;
set bk = b mod k;
assume that
A1: a+b > 0 and
A2: ak+bk > 0;
defpred P[Nat] means
((a+b) to_power $1) mod k = ((ak+bk) to_power $1) mod k;
A3: P[0]
proof
thus ((a+b) to_power 0) mod k = 1 mod k by POWER:24
.= (((a mod k) + (b mod k)) to_power 0) mod k by POWER:24;
end;
A4: for x being Nat st P[x] holds P[x+1]
proof
let x be Nat such that
A5: P[x];
A6: (a+b) to_power (x+1) = (a+b) to_power x * (a+b) to_power 1
by A1,POWER:27;
A7: (a+b) mod k = (ak+bk) mod k by NAT_D:66;
thus ((a+b) to_power (x+1)) mod k
= (((a+b) to_power x mod k) * ((a+b) mod k)) mod k by A6,NAT_D:67
.= ((ak+bk) to_power x * (ak+bk) to_power 1) mod k by A5,A7,NAT_D:67
.= ((ak+bk) to_power (x+1)) mod k by A2,POWER:27;
end;
for x being Nat holds P[x] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th28:
for a,b,k being Integer holds
((a+b)|^n) mod k = (((a mod k) + (b mod k)) |^ n) mod k
proof
let a,b,k be Integer;
set ak = a mod k;
set bk = b mod k;
defpred P[Nat] means ((a+b)|^$1) mod k = ((ak+bk)|^$1) mod k;
A1: P[0]
proof
thus ((a+b)|^0) mod k = 1 mod k by NEWTON:4
.= (((a mod k) + (b mod k)) |^ 0) mod k by NEWTON:4;
end;
A2: for x being Nat st P[x] holds P[x+1]
proof
let x be Nat such that
A3: P[x];
A4: (a+b)|^(x+1) = (a+b)|^ x * (a+b) by NEWTON:6;
A5: (a+b) mod k = (ak+bk) mod k by NAT_D:66;
thus ((a+b)|^(x+1)) mod k
= (((a+b)|^x mod k) * ((a+b) mod k)) mod k by A4,NAT_D:67
.= ((ak+bk)|^x * (ak+bk)) mod k by A3,A5,NAT_D:67
.= ((ak+bk)|^(x+1)) mod k by NEWTON:6;
end;
for x being Nat holds P[x] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th29:
1 < m implies (m divides a|^b + 1 iff m divides (a mod m)|^b + 1)
proof
set r = a mod m;
assume
A1: 1 < m; then
A2: 1 mod m = 1 by NAT_D:24;
A3: ((-1 mod m) + (1 mod m)) mod m = (-1+1) mod m by NAT_D:66
.= 0;
thus m divides a|^b + 1 implies m divides r|^b+1
proof
assume
A4: m divides a|^b + 1;
set k = a div m;
(a|^b+1) mod m = 0 by A4;
then
A5: (a|^b+1-1) mod m = (0-1) mod m by A2,INT_6:7;
A6: a = m*k+r by A1,NAT_D:2;
A7: m*k mod m = 0;
((m*k+r)|^n) mod m = (((m*k mod m) + (r mod m))|^n) mod m
by Th28;
then (a|^b) mod m = ((r mod m)|^b) mod m by A6;
then (r|^b+1) mod m = 0 by A3,A5,NAT_D:66;
hence m divides r|^b+1 by A1,INT_1:62;
end;
assume m divides r|^b+1;
then (r|^b+1) mod m = 0;
then
A8: (r|^b+1-1) mod m = (0-1) mod m by A2,INT_6:7;
(a|^b) mod m = ((a mod m)|^b) mod m by PEPIN:12;
then (a|^b+1) mod m = 0 by A3,A8,NAT_D:66;
hence thesis by A1,INT_1:62;
end;
theorem Th30:
10 divides a|^10 + 1 iff
ex r,k being Nat st
a = 10*k+r & 10 divides r|^10+1 & (r = 0 or ... or r = 9)
proof
thus 10 divides a|^10 + 1 implies
ex r,k being Nat st
a = 10*k+r & 10 divides r|^10+1 & (r = 0 or ... or r = 9)
proof
assume
A1: 10 divides a|^10 + 1;
take r = a mod 10;
take k = a div 10;
thus a = 10*k+r by NAT_D:2;
thus 10 divides r|^10+1 by A1,Th29;
thus r = 0 or ... or r = 9 by NUMPOLY1:8;
end;
given r,k being Nat such that
A2: a = 10*k+r and
A3: 10 divides r|^10+1 and
A4: r = 0 or ... or r = 9;
r = a mod 10 by A2,A4,NAT_D:def 2;
hence thesis by A3,Th29;
end;
theorem Th31:
for a,b being odd Nat st a-b = 2 holds a,b are_coprime
proof
let a,b be odd Nat such that
A1: a-b = 2;
assume not a,b are_coprime;
then consider k being Nat such that
A2: k divides a & k divides b and
A3: k <> 1 by PYTHTRIP:def 1;
k <= 2 by A1,A2,INT_5:1,INT_2:27;
then k = 0 or ... or k = 2;
hence contradiction by A2,A3;
end;
theorem Th32:
for a,b,c being odd Nat st c-b = 2 & b-a = 2 holds
3 divides a or 3 divides b or 3 divides c
proof
let a,b,c be odd Nat such that
A1: c-b = 2 and
A2: b-a = 2;
assume
A3: not 3 divides a & not 3 divides b;
A4: (b-a) mod 3 = ((b mod 3)-(a mod 3)) mod 3 by INT_6:7;
per cases by A3,Lm17;
suppose a mod 3 = 1 & b mod 3 = 1;
hence 3 divides c by A2,A4,NAT_D:24,INT_1:73;
end;
suppose a mod 3 = 1 & b mod 3 = 2;
hence 3 divides c by A2,A4,NAT_D:24;
end;
suppose that
a mod 3 = 2 and
A5: b mod 3 = 1;
A6: (c-b) mod 3 = ((c mod 3)-(b mod 3)) mod 3 by INT_6:7;
assume not 3 divides c;
then per cases by Lm17;
suppose c mod 3 = 1;
hence contradiction by A1,A6,A5,NAT_D:24,INT_1:73;
end;
suppose c mod 3 = 2;
hence contradiction by A1,A6,A5,NAT_D:24;
end;
end;
suppose a mod 3 = 2 & b mod 3 = 2;
hence 3 divides c by A2,A4,INT_1:73;
end;
end;
theorem Th33:
for a,b,c being odd Prime st c-b = 2 & b-a = 2 holds a = 3 & b = 5 & c = 7
proof
let a,b,c be odd Prime such that
A1: c-b = 2 & b-a = 2;
3 divides a or 3 divides b or 3 divides c by A1,Th32;
then a = 3 or b = 3 or c = 3 by INT_2:def 4;
hence thesis by A1,INT_2:def 4;
end;
theorem Th34:
a|^n is prime implies n = 1
proof
set p = a|^n;
assume that
A1: p > 1 and
A2: for n being Nat st n divides p holds n = 1 or n = p;
per cases by NAT_1:6;
suppose n = 0;
hence thesis by A1,NEWTON:4;
end;
suppose ex k st n = k+1;
then consider k such that
A3: n = k+1;
A4: p = a|^k*a by A3,NEWTON:6;
A5: k in NAT by ORDINAL1:def 12;
a divides a|^k*a;
then per cases by A2,A4;
suppose a = 1;
hence thesis by A1;
end;
suppose a = p;
then 1*a = a|^k*a by A3,NEWTON:6;
then k = 0 by A1,A4,A5,WEDDWITT:1,XCMPLX_1:5;
hence thesis by A3;
end;
end;
end;
theorem Th35:
1 < a implies ex k st 1 < k & n < a|^k
proof
assume
A1: 1 < a;
per cases by NAT_1:14;
suppose
A2: n = 0;
take 2;
thus thesis by A1,A2;
end;
suppose n >= 1;
then per cases by XXREAL_0:1;
suppose
A3: n = 1;
take 2;
thus 1 < 2;
1*1 < a*a by A1,XREAL_1:96;
hence thesis by A3,WSIERP_1:1;
end;
suppose
A4: n > 1;
take n;
thus thesis by A1,A4,NAT_3:2;
end;
end;
end;
theorem
2|^n mod 3 = 1 or 2|^n mod 3 = 2
proof
defpred P[Nat] means 2|^$1 mod 3 = 1 or 2|^$1 mod 3 = 2;
A1: P[0] by Lm1,NEWTON:4;
A2: for k st P[k] holds P[k+1]
proof
let k;
(2|^k*2) mod 3 = ((2|^k mod 3) * (2 mod 3)) mod 3 by NAT_D:67;
hence thesis by Lm1,Lm2,Lm3,NEWTON:6;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th37:
3|^m divides 2|^(3|^m)+1
proof
defpred P[Nat] means 3|^$1 divides 2|^(3|^$1)+1;
A1: P[0]
proof
3|^0 = 1 by NEWTON:4;
hence thesis by INT_2:12;
end;
A2: for m st P[m] holds P[m+1]
proof
let m;
set a = 3|^m;
given k being Nat such that
A3: 2|^a+1 = a*k;
set z = a*k;
per cases;
suppose
A4: m = 0;
2|^(3|^1)+1 = 2*2*2+1 by POLYEQ_5:2
.= 3*3;
then 3|^1 divides 2|^(3|^1)+1;
hence thesis by A4;
end;
suppose 0 < m;
then reconsider m1 = m-1 as Nat;
set t = 3|^m1*3|^m*k*k*k - 3*(3|^m1*k*k) + k;
A5: 3|^(m+1) = 3*a by NEWTON:6;
A6: z|^3 = z*z*z by POLYEQ_5:2
.= a*a*a*k*k*k
.= 3|^(m+(m1+1))*3|^m*k*k*k by NEWTON:8
.= 3|^(m+1+m1)*3|^m*k*k*k
.= 3|^(m+1)*3|^m1*3|^m*k*k*k by NEWTON:8
.= 3|^(m+1)*(3|^m1*3|^m*k*k*k);
A7: z|^2 = z*z by POLYEQ_5:1
.= a*a*k*k
.= 3|^(m+(m1+1))*k*k by NEWTON:8
.= 3|^(m+1+m1)*k*k
.= 3|^(m+1)*3|^m1*k*k by NEWTON:8
.= 3|^(m+1)*(3|^m1*k*k);
2|^(3|^(m+1)) = (z-1)|^3 by A3,A5,NEWTON:9
.= z|^3 - 3*z|^2*1 + 3*1|^2*z - 1|^3 by POLYEQ_5:5
.= 3|^(m+1)*t-1 by A5,A6,A7;
then 3|^(m+1) divides 2|^(3|^(m+1))+1;
hence thesis;
end;
end;
for m holds P[m] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th38:
Euler 0 = 0
proof
set A = {k where k is Element of NAT: 0,k are_coprime & k >= 1 & k <= 0};
assume Euler 0 <> 0;
then card A <> 0 by EULER_1:def 1;
then consider a being object such that
A1: a in A by XBOOLE_0:7,CARD_1:27;
ex k being Element of NAT st k = a & 0,k are_coprime & k >= 1 & k <= 0
by A1;
hence contradiction;
end;
registration
cluster Euler 0 -> zero;
coherence by Th38;
end;
registration
let n be positive Nat;
cluster Euler n -> positive;
coherence
proof
Euler n <> 0 by PEPIN:42;
hence thesis;
end;
end;
begin :: Main problems
deffunc an(Nat) = 2|^(2*$1+1)-2|^($1+1)+1;
deffunc bn(Nat) = 2|^(2*$1+1)+2|^($1+1)+1;
Lm32: now
let k;
(2*2*2*2) mod 5 = 1 by Lm9,NAT_D:24;
then (2|^4) mod 5 = 1 by POLYEQ_5:3;
hence (2|^4)|^k mod 5 = 1|^k mod 5 by INT_4:8
.= 1 by NAT_D:24;
end;
Lm33: now
let k;
A1: (2|^4)|^k mod 5 = 1 by Lm32;
A2: (2|^4)|^k = 2|^(4*k) by NEWTON:9;
2|^(2*(4*k)) = 2|^(4*k)|^2 by NEWTON:9;
hence 2|^(2*(4*k)) mod 5 = (1|^k)|^2 mod 5 by A1,A2,INT_4:8
.= 1 by NAT_D:24;
end;
Lm34: now
let k;
set x = 2|^(2*(4*k)+1);
set y = 2|^(4*k+1);
A1: 2|^(2*(4*k)) mod 5 = 1 by Lm33;
A2: (2|^4)|^k mod 5 = 1 by Lm32;
A3: (2|^4)|^k = 2|^(4*k) by NEWTON:9;
x = 2 * (2|^(2*(4*k))) by NEWTON:6;
then
A4: x mod 5 = (2*1) mod 5 by A1,Lm14,NAT_D:67
.= 2 by NAT_D:24;
y = 2 * (2|^(4*k)) by NEWTON:6;
then
A5: y mod 5 = (2 * 1) mod 5 by A2,A3,Lm14,NAT_D:67
.= 2 by NAT_D:24;
thus an(4*k) mod 5 = (((x-y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((2-2) mod 5+1) mod 5 by A4,A5,INT_6:7
.= (0+1) mod 5
.= 1 by NAT_D:24;
thus bn(4*k) mod 5 = (((x+y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((2+2) mod 5+1) mod 5 by A4,A5,NAT_D:66
.= 0 by Lm16,INT_1:50;
end;
Lm35: now
let k;
set x = 2|^(2*(4*k+1)+1);
set y = 2|^(4*k+1+1);
A1: 2|^(2*(4*k)) mod 5 = 1 by Lm33;
A2: (2|^4)|^k mod 5 = 1 by Lm32;
A3: (2|^4)|^k = 2|^(4*k) by NEWTON:9;
A4: 2|^3 = 2*2*2 by POLYEQ_5:2;
A5: 7 mod 5 = 2 by Lm10,NAT_D:24;
A6: 8 mod 5 = 3 by Lm11,NAT_D:24;
x = 2|^(8*k+3);
then x = 2|^(2*(4*k)) * 2|^3 by NEWTON:8;
then
A7: x mod 5 = (1*3) mod 5 by A1,A4,A6,NAT_D:67
.= 3 by NAT_D:24;
A8: 2|^2 = 2*2 by POLYEQ_5:1;
A9: 4 mod 5 = 4 by NAT_D:24;
y = 2|^(4*k+2);
then y = 2|^(4*k) * 2|^2 by NEWTON:8;
then
A10: y mod 5 = (1*4) mod 5 by A2,A3,A8,A9,NAT_D:67
.= 4 by NAT_D:24;
thus an(4*k+1) mod 5 = (((x-y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((3-4) mod 5+1) mod 5 by A7,A10,INT_6:7
.= ((3-4) mod 5+(1 mod 5)) mod 5 by NAT_D:24
.= ((3-4+1) mod 5) mod 5 by NAT_D:66
.= 0;
thus bn(4*k+1) mod 5 = (((x+y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((3+4) mod 5+1) mod 5 by A7,A10,NAT_D:66
.= 3 by A5,NAT_D:24;
end;
Lm36: now
let k;
set x = 2|^(2*(4*k+2)+1);
set y = 2|^(4*k+2+1);
A1: 2|^(2*(4*k)) mod 5 = 1 by Lm33;
A2: (2|^4)|^k mod 5 = 1 by Lm32;
A3: (2|^4)|^k = 2|^(4*k) by NEWTON:9;
A4: 2|^5 = 2*2*2*2*2 by NUMBER02:1;
A5: (6*5+2) mod 5 = 2 by Lm12,NAT_D:24;
x = 2|^(8*k+5);
then x = 2|^(2*(4*k)) * 2|^5 by NEWTON:8;
then
A6: x mod 5 = (1*2) mod 5 by A1,A4,A5,NAT_D:67
.= 2 by NAT_D:24;
A7: 2|^3 = 2*2*2 by POLYEQ_5:2;
A8: 8 mod 5 = 3 by Lm11,NAT_D:24;
y = 2|^(4*k+3);
then y = 2|^(4*k) * 2|^3 by NEWTON:8;
then
A9: y mod 5 = (1*3) mod 5 by A2,A3,A7,A8,NAT_D:67
.= 3 by NAT_D:24;
thus an(4*k+2) mod 5 = (((x-y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((2-3) mod 5+1) mod 5 by A6,A9,INT_6:7
.= ((2-3) mod 5+(1 mod 5)) mod 5 by NAT_D:24
.= ((2-3+1) mod 5) mod 5 by NAT_D:66
.= 0;
thus bn(4*k+2) mod 5 = (((x+y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((2+3) mod 5+1) mod 5 by A6,A9,NAT_D:66
.= (0+1) mod 5 by NAT_D:25
.= 1 by NAT_D:24;
end;
Lm37: now
let k;
set x = 2|^(2*(4*k+3)+1);
set y = 2|^(4*k+3+1);
A1: 2|^(2*(4*k)) mod 5 = 1 by Lm33;
A2: (2|^4)|^k mod 5 = 1 by Lm32;
A3: (2|^4)|^k = 2|^(4*k) by NEWTON:9;
A4: 2|^7 = 2*2*2*2*2*2*2 by NUMBER02:3;
A5: (5*25+3) mod 5 = 3 by Lm15,NAT_D:21;
x = 2|^(8*k+7);
then x = 2|^(2*(4*k)) * 2|^7 by NEWTON:8;
then
A6: x mod 5 = (1*3) mod 5 by A1,A4,A5,NAT_D:67
.= 3 by NAT_D:24;
A7: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
y = 2|^(4*k+4);
then y = 2|^(4*k) * 2|^4 by NEWTON:8;
then
A8: y mod 5 = (1*1) mod 5 by A2,A3,A7,Lm9,NAT_D:67
.= 1 by NAT_D:24;
thus an(4*k+3) mod 5 = (((x-y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((3-1) mod 5+1) mod 5 by A6,A8,INT_6:7
.= 3 by Lm14,NAT_D:24;
thus bn(4*k+3) mod 5 = (((x+y) mod 5) + 1) mod 5 by Lm13,NAT_D:66
.= ((3+1) mod 5+1) mod 5 by A6,A8,NAT_D:66
.= (4+1) mod 5 by NAT_D:24
.= 0 by NAT_D:25;
end;
:: Problem 11 a
theorem Th39:
5 divides 2|^(2*n+1) - 2|^(n+1) + 1 iff n mod 4 = 1 or n mod 4 = 2
proof
consider k such that
A1: n = 4*k or n = 4*k+1 or n = 4*k+2 or n = 4*k+3 by NUMBER02:24;
thus 5 divides an(n) implies n mod 4 = 1 or n mod 4 = 2
proof
assume 5 divides an(n);
then an(n) mod 5 = 0;
hence thesis by A1,Lm6,Lm7,Lm34,Lm37,NAT_D:21;
end;
A2: an(4*k+1) mod 5 = 0 by Lm35;
A3: an(4*k+2) mod 5 = 0 by Lm36;
4*k+0 = 4*k;
thus thesis by A1,A2,A3,Lm8,NAT_D:21,INT_1:62;
end;
:: Problem 11 b
theorem Th40:
5 divides 2|^(2*n+1) + 2|^(n+1) + 1 iff n mod 4 = 0 or n mod 4 = 3
proof
consider k such that
A1: n = 4*k or n = 4*k+1 or n = 4*k+2 or n = 4*k+3 by NUMBER02:24;
A2: 4*k+0 = 4*k;
thus 5 divides bn(n) implies n mod 4 = 0 or n mod 4 = 3
proof
assume 5 divides bn(n);
then bn(n) mod 5 = 0;
hence thesis by A1,Lm8,Lm35,Lm36,NAT_D:21;
end;
A3: bn(4*k) mod 5 = 0 by Lm34;
bn(4*k+3) mod 5 = 0 by Lm37;
hence thesis by A1,A3,Lm6,Lm7,NAT_D:21,INT_1:62;
end;
:: Problem 11 c
theorem
5 divides 2|^(2*n+1) - 2|^(n+1) + 1 iff
not 5 divides 2|^(2*n+1) + 2|^(n+1) + 1
proof
n mod (3+1) = 0 or ... or n mod (3+1) = 3 by Th11;
hence thesis by Th39,Th40;
end;
:: Problem 16 a
theorem
{n where n is Nat: n divides 2|^n+1} is infinite
proof
set S = {n where n is Nat: n divides 2|^n+1};
deffunc F(Nat) = 3|^$1;
consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT holds f.i = F(i) from PBOOLE:sch 5;
set R = rng f;
A2: dom f = NAT by PARTFUN1:def 2;
A3: R c= S
proof
let x be object;
assume x in R;
then consider m being object such that
A4: m in dom f and
A5: x = f.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A4,PARTFUN1:def 2;
A6: f.m = F(m) by A1;
3|^m divides 2|^(3|^m)+1 by Th37;
hence x in S by A5,A6;
end;
for m being Nat ex N being Nat st N >= m & N in R
proof
let m be Nat;
take n = F(m+1);
A7: m <= 3|^m by NEWTON:86;
m+0 <= m+1 by XREAL_1:6;
then 3|^m <= 3|^(m+1) by NAT_6:1;
hence n >= m by A7,XXREAL_0:2;
f.(m+1) = n by A1;
hence n in R by A2,FUNCT_1:def 3;
end;
hence thesis by A3,PYTHTRIP:9;
end;
:: Problem 16 b
theorem
{n where n is Nat: n divides 2|^n+1 & n is prime} = {3}
proof
set S = {n where n is Nat: n divides 2|^n+1 & n is prime};
thus S c= {3}
proof
let x be object;
assume x in S;
then consider n such that
A1: x = n and
A2: n divides 2|^n+1 and
A3: n is prime;
A4: (2|^n+1) mod n = 0 by A2;
A5: n <> 2 by A2;
1+1 <= n by A3,NAT_1:13;
then 2 < n by A5,XXREAL_0:1;
then
A6: 2 mod n = 2 by NAT_D:24;
A7: (2|^n) mod n = 2 mod n by A3,EULER_2:19;
A8: (2|^n+1-2|^n) mod n = (((2|^n+1) mod n) - ((2|^n) mod n)) mod n
by INT_6:7;
(1--2) mod n = ((1 mod n) - ((-2) mod n)) mod n by INT_6:7;
then n divides 3 by A3,A4,A7,A6,A8,INT_1:62;
then n = 3 by A3,PEPIN:41;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {3};
then
A9: x = 3 by TARSKI:def 1;
3|^1 divides 2|^(3|^1)+1 by Th37;
hence thesis by A9,PEPIN:41;
end;
:: Problem 19
theorem
10 divides a|^10 + 1 iff ex k st a = 10*k+3 or a = 10*k+7
proof
thus 10 divides a|^10 + 1 implies ex k st a = 10*k+3 or a = 10*k+7
proof
assume 10 divides a|^10 + 1;
then consider r,k being Nat such that
A1: a = 10*k+r and
A2: 10 divides r|^10+1 and
A3: r = 0 or ... or r = 9 by Th30;
take k;
per cases by A3;
suppose r = 0;
hence a = 10*k+3 or a = 10*k+7 by A2,INT_2:27;
end;
suppose r = 1;
hence a = 10*k+3 or a = 10*k+7 by A2,INT_2:27;
end;
suppose r = 2;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm25;
end;
suppose r = 3;
hence a = 10*k+3 or a = 10*k+7 by A1;
end;
suppose r = 4;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm26,Th5;
end;
suppose r = 5;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm27,Th6;
end;
suppose r = 6;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm28,Th7;
end;
suppose r = 7;
hence a = 10*k+3 or a = 10*k+7 by A1;
end;
suppose r = 8;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm29,Th9;
end;
suppose r = 9;
hence a = 10*k+3 or a = 10*k+7 by A2,Lm30,Th10;
end;
end;
given k such that
A4: a = 10*k+3 or a = 10*k+7;
per cases by A4;
suppose
A5: a = 10*k+3;
3 = 0 or ... or 3 = 9;
hence 10 divides a|^10 + 1 by A5,Th4,INT_1:def 3,Th30;
end;
suppose
A6: a = 10*k+7;
7 = 0 or ... or 7 = 9;
hence 10 divides a|^10 + 1 by A6,Th8,INT_1:def 3,Th30;
end;
end;
theorem Th45:
(a <> 0 or b <> 0) & n > 0 & a divides b|^n - 1 implies a,b are_coprime
proof
set g = a gcd b;
assume (a <> 0 or b <> 0) & n > 0 & a divides b|^n - 1;
then g divides b|^n & g divides b|^n - 1 by INT_2:2,21,NEWTON02:14;
then g divides b|^n - (b|^n - 1) by INT_5:1;
hence thesis by WSIERP_1:15;
end;
:: Problem 20
theorem
not ex n being Nat st 1 < n & n divides 2|^n-1
proof
given n being Nat such that
A1: 1 < n and
A2: n divides 2|^n-1;
defpred P[Nat] means 1 < $1 & $1 divides 2|^$1-1;
A3: ex k being Nat st P[k] by A1,A2;
consider N being Nat such that
A4: P[N] and
A5: for n being Nat st P[n] holds N <= n from NAT_1:sch 5(A3);
N divides 2|^N-1 by A4;
then reconsider N as odd Element of NAT by A4,ORDINAL1:def 12;
set E = Euler N;
set d = N gcd E;
A6: 1 mod N = 1 by A4,NAT_D:14;
reconsider k = 2|^N-1 as Nat;
2,N are_coprime by A4,Th45;
then 2|^E mod N = 1 by A4,EULER_2:18;
then 2|^E-1 mod N = (1-1) mod N by A6,INT_6:7
.= 0;
then N divides 2|^E-1 by INT_1:62;
then
A7: N divides (2|^N - 1) gcd (2|^E - 1) by A4,INT_2:def 2;
A8: (2|^N - 1) gcd (2|^E - 1) = 2|^d - 1 by Th26;
A9: now
assume d <= 1;
then d < 1 or d = 1 by XXREAL_0:1;
hence contradiction by A4,A7,A8,NAT_1:14,WSIERP_1:15;
end;
A10: d <= E by Th13;
A11: d divides N by INT_2:def 2;
A12: E <= N-1 by A4,EULER_1:19;
N-1 < N-0 by XREAL_1:15;
then E < N by A12,XXREAL_0:2;
then d < N by A10,XXREAL_0:2;
hence contradiction by A5,A11,A9,A7,A8,INT_2:9;
end;
:: Problem 21
theorem
{n where n is odd Nat: n divides 3|^n+1} = {1}
proof
set A = {n where n is odd Nat: n divides 3|^n+1};
thus A c= {1}
proof
let x be object;
assume x in A;
then consider n being odd Nat such that
A1: n = x and
A2: n divides 3|^n+1;
n = 1
proof
assume
A3: n <> 1;
A4: (3*3)|^n = 3|^n*3|^n by NEWTON:7;
(3|^n)^2-1^2 = (3|^n-1)*(3|^n+1);
then
A5: n divides 9|^n-1 by A2,A4,INT_2:2;
defpred P[Nat] means $1 is odd & 1 < $1 & $1 divides 9|^$1-1;
A6: ex k being Nat st P[k] by A3,A5,NAT_1:25;
consider N being Nat such that
A7: P[N] and
A8: for n being Nat st P[n] holds N <= n from NAT_1:sch 5(A6);
reconsider N as odd Element of NAT by A7,ORDINAL1:def 12;
set E = Euler N;
set d = N gcd E;
A9: 1 mod N = 1 by A7,NAT_D:14;
reconsider k = 9|^N-1 as Nat;
9,N are_coprime by A7,Th45;
then 9|^E mod N = 1 by A7,EULER_2:18;
then 9|^E-1 mod N = (1-1) mod N by A9,INT_6:7
.= 0;
then N divides 9|^E-1 by INT_1:62;
then
A10: N divides (9|^N - 1) gcd (9|^E - 1) by A7,INT_2:def 2;
A11: (9|^N - 1) gcd (9|^E - 1) = 9|^d - 1 by Th26;
A12: now
assume d <= 1;
then d < 1 or d = 1 by XXREAL_0:1;
then N in {1,2,4,8} by A10,A11,Th12,NAT_1:14;
then N = 2*1 or N = 2*2 or N = 2*4 by A7,ENUMSET1:def 2;
hence contradiction;
end;
A13: d <= E by Th13;
A14: d divides N by INT_2:def 2;
A15: E <= N-1 by A7,EULER_1:19;
N-1 < N-0 by XREAL_1:15;
then E < N by A15,XXREAL_0:2;
then d < N by A13,XXREAL_0:2;
hence contradiction by A8,A14,A12,A10,A11,INT_2:9;
end;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {1};
then
A16: x = 1 by TARSKI:def 1;
A17: 1 = 2*0+1;
1 divides 3|^1+1 by INT_2:12;
hence thesis by A16,A17;
end;
:: Problem 22
theorem
{n where n is positive Nat : 3 divides n*2|^n+1} =
the set of all 6*k+1 where k is Nat \/
the set of all 6*k+2 where k is Nat
proof
set A = {n where n is positive Nat : 3 divides n*2|^n+1};
set B = the set of all 6*k+1 where k is Nat;
set C = the set of all 6*k+2 where k is Nat;
2|^6 = 2*2*2*2*2*2 by NUMBER02:2;
then
A1: 2|^6 mod 3 = (3*21+1) mod 3
.= 1 mod 3 by NAT_D:21;
thus A c= B \/ C
proof
let x be object;
assume x in A;
then consider n being positive Nat such that
A2: x = n and
A3: 3 divides n*2|^n+1;
A4: (n*2|^n+1) mod 3 = ((n*2|^n) mod 3 + (1 mod 3)) mod 3 by NAT_D:66;
A5: (n*2|^n) mod 3 = ((n mod 3) * (2|^n mod 3)) mod 3 by NAT_D:67;
A6: n mod 3 <> 0 by Lm1,A5,A4,A3;
consider k such that
A7: n = 6*k or n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or
n = 6*k+4 or n = 6*k+5 by NUMBER02:26;
A8: (2|^6|^k) mod 3 = (1|^k) mod 3 by Lm1,A1,PEPIN:12
.= 1 by NAT_D:24;
per cases by A7;
suppose n = 3*(2*k);
hence thesis by A6;
end;
suppose n = 6*k+1;
then n in B;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose n = 6*k+2;
then n in C;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose n = 3*(2*k+1);
hence thesis by A6;
end;
suppose
A9: n = 6*k+4;
then
A10: n mod 3 = (3*(2*k+1)+1) mod 3
.= 1 mod 3 by NAT_D:21;
2|^(6*k+3+1) = 2|^(6*k+2+1)*2 by NEWTON:6
.= 2|^(6*k+1+1)*2*2 by NEWTON:6
.= 2|^(6*k+1)*2*2*2 by NEWTON:6
.= 2|^(6*k)*2*2*2*2 by NEWTON:6
.= 2|^(6*k)*(2*2*2*2)
.= 2|^6|^k*16 by NEWTON:9;
then
A11: (2|^n) mod 3 = (1*1) mod 3 by A8,Lm4,A9,NAT_D:67;
n * 2|^n + 1 mod 3
= ((n*2|^n) mod 3 + (1 mod 3)) mod 3 by NAT_D:66
.= (1+1) mod 3 by A11,Lm1,A10,NAT_D:67
.= 2 by NAT_D:24;
hence thesis by A3;
end;
suppose
A12: n = 6*k+5;
then
A13: n mod 3 = (3*(2*k+1)+2) mod 3
.= 2 mod 3 by NAT_D:21;
2|^(6*k+4+1) = 2|^(6*k+3+1)*2 by NEWTON:6
.= 2|^(6*k+2+1)*2*2 by NEWTON:6
.= 2|^(6*k+1+1)*2*2*2 by NEWTON:6
.= 2|^(6*k+1)*2*2*2*2 by NEWTON:6
.= 2|^(6*k)*2*2*2*2*2 by NEWTON:6
.= 2|^(6*k)*(2*2*2*2*2)
.= 2|^6|^k*32 by NEWTON:9;
then
A14: (2|^n) mod 3 = ((2|^6|^k mod 3) * (32 mod 3)) mod 3 by A12,NAT_D:67
.= (1*2) mod 3 by A8,Lm5;
n * 2|^n + 1 mod 3
= ((n*2|^n) mod 3 + 1) mod 3 by Lm1,NAT_D:66
.= ((2*2) mod 3 + 1) mod 3 by Lm2,A14,A13,NAT_D:67
.= 2 by Lm1,Lm3,NAT_D:24;
hence thesis by A3;
end;
end;
let n be object;
assume n in B \/ C;
then per cases by XBOOLE_0:def 3;
suppose n in B;
then consider k such that
A15: n = 6*k+1;
reconsider n as Nat by A15;
A16: (2|^6|^k) mod 3 = (1|^k) mod 3 by Lm1,A1,PEPIN:12
.= 1 by NAT_D:24;
A17: n mod 3 = (3*(2*k)+1) mod 3 by A15
.= 1 mod 3 by NAT_D:21;
2|^(6*k+1) = 2|^(6*k)*2 by NEWTON:6
.= 2|^6|^k*2 by NEWTON:9;
then
A18: (2|^n) mod 3 = ((2|^6|^k mod 3) * (2 mod 3)) mod 3 by A15,NAT_D:67
.= (1*2) mod 3 by A16;
n * 2|^n + 1 mod 3 = ((n*2|^n) mod 3 + 1) mod 3 by Lm1,NAT_D:66
.= (2+1) mod 3 by Lm2,A18,Lm1,A17,NAT_D:67
.= 0 by INT_1:50;
then 3 divides n*2|^n+1 by INT_1:62;
hence thesis by A15;
end;
suppose n in C;
then consider k such that
A19: n = 6*k+2;
reconsider n as Nat by A19;
A20: (2|^6|^k) mod 3 = (1|^k) mod 3 by Lm1,A1,PEPIN:12
.= 1 by NAT_D:24;
A21: n mod 3 = (3*(2*k)+2) mod 3 by A19
.= 2 mod 3 by NAT_D:21;
2|^(6*k+1+1) = 2|^(6*k+1)*2 by NEWTON:6
.= 2|^(6*k)*2*2 by NEWTON:6
.= 2|^(6*k)*(2*2)
.= 2|^6|^k*4 by NEWTON:9;
then
A22: (2|^n) mod 3 = (1*1) mod 3 by Lm3,A20,A19,NAT_D:67;
n * 2|^n + 1 mod 3
= ((n*2|^n) mod 3 + 1) mod 3 by Lm1,NAT_D:66
.= (((n mod 3)*((2|^n) mod 3)) mod 3 + 1) mod 3 by NAT_D:67
.= 0 by Lm2,Lm1,A22,A21,INT_1:50;
then 3 divides n*2|^n+1 by INT_1:62;
hence thesis by A19;
end;
end;
theorem Th49:
for p being odd Prime st n = (p-1)*(k*p+1) holds 2|^n mod p = 1
proof
let p be odd Prime such that
A1: n = (p-1)*(k*p+1);
A2: 1 < p by INT_2:def 4;
then
A3: p-'1 = p-1 by XREAL_1:233;
A4: 2|^n = 2|^(p-1)|^(k*p+1) by A1,NEWTON:9;
2|^1,p are_coprime by NAT_5:3;
then 2|^(p-'1) mod p = 1 by PEPIN:37;
hence thesis by A2,A3,A4,PEPIN:35;
end;
theorem Th50:
for p being odd Prime st n = (p-1)*(k*p+1) holds p divides CullenNumber n
proof
let p be odd Prime;
assume
A1: n = (p-1)*(k*p+1);
then
A2: 2|^n mod p = 1 by Th49;
p-1 < p-0 by XREAL_1:15;
then
A3: (p-1) mod p = p-1 by NAT_D:24;
A4: (k*p+1) mod p = 1 mod p by NAT_D:21
.= 1 by INT_2:def 4,NAT_D:14;
A5: ((p-1)*(k*p+1)) mod p = (((p-1) mod p)*((k*p+1) mod p)) mod p by NAT_D:67
.= (p-1) mod p by A4;
(n*2|^n) mod p = ((n mod p)*(2|^n mod p)) mod p by NAT_D:67;
then (CullenNumber n) mod p = (p-1+1) mod p by A1,A2,A3,A5,NAT_D:22
.= 0 by NAT_D:25;
hence thesis by INT_1:62;
end;
:: Problem 23
theorem
for p being odd Prime holds
{n where n is Nat: p divides CullenNumber n} is infinite
proof
let p be odd Prime;
set S = {n where n is Nat: p divides CullenNumber n};
deffunc F(Nat) = (p-1)*($1*p+1);
consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT holds f.i = F(i) from PBOOLE:sch 5;
set R = rng f;
A2: dom f = NAT by PARTFUN1:def 2;
A3: R c= S
proof
let x be object;
assume x in R;
then consider m being object such that
A4: m in dom f and
A5: x = f.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A4,PARTFUN1:def 2;
A6: f.m = F(m) by A1;
set n = (p-1)*(m*p+1);
p divides CullenNumber n by Th50;
hence x in S by A5,A6;
end;
for m being Nat ex N being Nat st N >= m & N in R
proof
let m be Nat;
take n = F(m+1);
A7: m+0 <= m+1 by XREAL_1:6;
1 < p by INT_2:def 4;
then
A8: (m+1)*1 <= (m+1)*p by XREAL_1:64;
A9: (m+1)*p+0 <= (m+1)*p+1 by XREAL_1:6;
1 <= p-1 by INT_2:def 4,INT_1:52;
then 1*((m+1)*p+1) <= (p-1)*((m+1)*p+1) by XREAL_1:64;
hence n >= m by A7,A8,A9,Th2;
f.(m+1) = n by A1;
hence n in R by A2,FUNCT_1:def 3;
end;
hence thesis by A3,PYTHTRIP:9;
end;
:: Problem 24
theorem
ex x,y being Nat st x > n & not x divides y & x|^x divides y|^y
proof
consider k such that
A1: 1 < k and
A2: n < 2|^k by Th35;
reconsider k as non zero Nat by A1;
A4: 0+1 <= 2|^(k-1) by NAT_1:13;
1*2|^(k-1) <= (2|^(k-1))*k by A1,XREAL_1:68;
then consider p being prime Nat such that
A5: (2|^(k-1))*k < p and
p <= 2*((2|^(k-1))*k) by A4,XXREAL_0:2,NAT_4:56;
take x = 2|^k;
take y = 2*p;
thus n < x by A2;
hereby
assume
A6: x divides y;
2|^(k-1+1) = 2*2|^(k-1) by NEWTON:6;
then 2|^(k-1) divides p by A6,INT_4:7;
then per cases by INT_2:def 4;
suppose
A7: 2|^(k-1) = 1;
1 = 2|^0 by NEWTON:4;
then k-1 = 0 by A7;
hence contradiction by A1;
end;
suppose
A8: 2|^(k-1) = p;
then k-1 = 1 by Th34;
hence contradiction by A5,A8;
end;
end;
A9: 2*(2|^(k-1))*k = (2|^(k-1+1))*k by NEWTON:6;
A10: 2*((2|^(k-1))*k) = 2*(2|^(k-1))*k;
(2|^k)*k < 2*p by A5,A9,A10,XREAL_1:68;
then
A11: 2|^((2|^k)*k) divides 2|^(2*p) by NEWTON03:16;
2 divides 2*p;
then 2|^(2*p) divides (2*p)|^(2*p) by WSIERP_1:14;
then 2|^((2|^k)*k) divides (2*p)|^(2*p) by A11,INT_2:9;
hence x|^x divides y|^y by NEWTON:9;
end;
Lm38:
for a,n,r being Integer st 0 < n & 0 <= r < n & r <> (-a) mod n holds
not n divides a+r
proof
let a,n,r be Integer;
set r1 = (-a) mod n;
assume that
A1: 0 < n and
A2: 0 <= r and
A3: r < n and
A4: r <> r1 and
A5: n divides a+r;
A6: 0 <= r1 < n by A1,INT_1:58;
then
A7: n is Nat & r is Nat & r1 is Nat by A2,TARSKI:1;
(r-r1) mod n = ((r mod n) - (((-a) mod n) mod n)) mod n by INT_6:7
.= (r-(-a)) mod n by INT_6:7
.= 0 by A5;
then n divides r-r1 by A1,INT_1:62;
hence contradiction by A3,A4,A6,A7,Th16;
end;
:: Problem 39
theorem
for a,b,c,n being Integer st 3 < n
ex k being Integer st
not n divides k+a & not n divides k+b & not n divides k+c
proof
let a,b,c,n be Integer such that
A1: 3 < n;
set r1 = (-a) mod n;
set r2 = (-b) mod n;
set r3 = (-c) mod n;
reconsider X = n as Nat by A1,TARSKI:1;
3+1 <= n by A1,NAT_1:13;
then card Segm 4 c= card Segm X by NAT_1:40;
then consider r being object such that
A2: r in X and
A3: r1 <> r & r2 <> r & r3 <> r by GLIBPRE0:17;
reconsider r as Nat by A2;
take r;
Segm X = X;
then r < n by A2,NAT_1:44;
hence thesis by A3,Lm38;
end;
Lm39:
for a,b being Integer st a < b holds
{n where n is Nat: a+n,b+n are_coprime} is infinite
proof
let a,b be Integer such that
A1: a < b;
set S = {n where n is Nat: a+n,b+n are_coprime};
defpred P[Nat,object] means
ex k being Nat st 0 < (b-a)*k+1-a & $1 <= (b-a)*k+1-a & $2 = (b-a)*k+1-a;
A2: for i being Element of NAT ex j being object st P[i,j]
proof
let i be Element of NAT;
consider k such that
A3: i < (b-a)*k+1-a and
k = |. [/ (i+a-1)/(b-a) + 1 \] .| by A1,Th17;
take (b-a)*k+1-a;
take k;
thus thesis by A3;
end;
consider f being ManySortedSet of NAT such that
A4: for i being Element of NAT holds P[i,f.i] from PBOOLE:sch 6(A2);
set R = rng f;
A5: dom f = NAT by PARTFUN1:def 2;
A6: R c= S
proof
let x be object;
assume x in R;
then consider t being object such that
A7: t in dom f and
A8: x = f.t by FUNCT_1:def 3;
reconsider t as Element of NAT by A7,PARTFUN1:def 2;
P[t,f.t] by A4;
then consider k being Nat such that
A9: 0 < (b-a)*k+1-a and
A10: f.t = (b-a)*k+1-a;
reconsider n = (b-a)*k+1-a as Nat by A9;
A11: 0 < b-a by A1,XREAL_1:50;
then reconsider an = a+n as Element of NAT by INT_1:3;
0 <= (b-a)*(k+1)+1 by A11;
then reconsider bn = b+n as Element of NAT by INT_1:3;
A12: 1 divides an & 1 divides bn by INT_2:12;
for d being Integer st d divides an & d divides bn holds d divides 1
proof
let d be Integer such that
A13: d divides an and
A14: d divides bn;
A15: an - (b-a)*k = 1;
A16: a-b = -(b-a);
d divides an-bn by A13,A14,INT_5:1;
then d divides b-a by A16,INT_2:10;
then d divides (b-a)*k by INT_2:2;
hence d divides 1 by A13,A15,INT_5:1;
end;
then a+n,b+n are_coprime by A12,INT_2:def 2;
hence x in S by A8,A10;
end;
for m being Nat ex N being Nat st N >= m & N in R
proof
let m be Nat;
consider k being Nat such that
A17: 0 < (b-a)*k+1-a and
A18: m+1 <= (b-a)*k+1-a and
A19: f.(m+1) = (b-a)*k+1-a by A4;
reconsider N = (b-a)*k+1-a as Element of NAT by A17,ORDINAL1:def 12;
take N;
m+0 <= m+1 by XREAL_1:6;
hence N >= m by A18,XXREAL_0:2;
thus N in R by A5,A19,FUNCT_1:def 3;
end;
hence thesis by A6,PYTHTRIP:9;
end;
:: Problem 44
theorem
for a,b being Integer st a <> b holds
{n where n is Nat: a+n,b+n are_coprime} is infinite
proof
let a,b be Integer;
assume a <> b;
then a < b or b < a by XXREAL_0:1;
hence thesis by Lm39;
end;
definition
let a,b,c be Integer;
pred a,b,c are_mutually_coprime means
a,b are_coprime & a,c are_coprime & b,c are_coprime;
let d be Integer;
pred a,b,c,d are_mutually_coprime means
a,b are_coprime & a,c are_coprime & a,d are_coprime &
b,c are_coprime & b,d are_coprime & c,d are_coprime;
end;
theorem
for a,b,c being Prime st a,b,c are_mutually_distinct
holds a,b,c are_mutually_coprime by INT_2:30;
theorem
for a,b,c,d being Prime st a,b,c,d are_mutually_distinct
holds a,b,c,d are_mutually_coprime by INT_2:30;
:: Problem 46
theorem
1,2,3,4 are_mutually_distinct &
not ex n being positive Nat st 1+n,2+n,3+n,4+n are_mutually_coprime
proof
thus 1,2,3,4 are_mutually_distinct;
given n being positive Nat such that
A1: 1+n,2+n,3+n,4+n are_mutually_coprime;
per cases;
suppose n is odd;
hence thesis by A1,NEWTON05:35,POLYFORM:6;
end;
suppose n is even;
hence thesis by A1,NEWTON05:35,POLYFORM:7;
end;
end;
:: Problem 74
theorem
for n being even Nat st n > 6
ex p,q being Prime st n-p,n-q are_coprime & p = 3 & q = 5
proof
let n be even Nat such that
A1: n > 6;
3 = 2*1+1;
then reconsider p = 3 as odd Prime by PEPIN:41;
5 = 2*2+1;
then reconsider q = 5 as odd Prime by PEPIN:59;
take p,q;
A2: n-p-(n-q) = 2;
6-3 < n-3 & 6-5 < n-5 by A1,XREAL_1:14;
hence thesis by A2,Th31;
end;
:: Problem 75
theorem
{p where p is Prime:
(ex a,b being Prime st p = a+b) & (ex c,d being Prime st p = c-d)}
= {5}
proof
set A = {p where p is Prime:
(ex a,b being Prime st p = a+b) & (ex c,d being Prime st p = c-d)};
thus A c= {5}
proof
let x be object;
assume x in A;
then consider r being Prime such that
A1: x = r and
A2: ex a,b being Prime st r = a+b and
A3: ex c,d being Prime st r = c-d;
consider a,b being Prime such that
A4: r = a+b by A2;
consider c,d being Prime such that
A5: r = c-d by A3;
A6: 1 < a & 1 < b by INT_2:def 4;
then
A7: 1+1 < r by A4,XREAL_1:8;
then
A8: r is odd by PEPIN:17;
A9: 1+1 <= a & 1+1 <= b by A6,NAT_1:13;
not a is odd or not b is odd by A4,A7,PEPIN:17;
then a <= 2 or b <= 2 by PEPIN:17;
then a = 2 or b = 2 by A9,XXREAL_0:1;
then consider p being Prime such that
A10: r = p+2 by A4;
1 < c & 1 < d by INT_2:def 4;
then
A11: 1+1 <= c & 1+1 <= d by NAT_1:13;
not c is odd or not d is odd by A5,A7,PEPIN:17;
then c <= 2 or d <= 2 by PEPIN:17;
then
A12: c = 2 or d = 2 by A11,XXREAL_0:1;
2-d <= d-d by A11,XREAL_1:9;
then 2-d <= 0;
then consider q being Prime such that
A13: r = q-2 by A5,A12;
(r+2)-r = 2 & r-(r-2) = 2;
then r-2 = 3 & r = 5 & r+2 = 7 by A8,A10,A13,Th33;
hence thesis by A1,TARSKI:def 1;
end;
let x be object;
assume x in {5};
then
A14: x = 5 by TARSKI:def 1;
5 = 3+2 & 5 = 7-2;
hence thesis by A14,PEPIN:41,59,INT_2:28,NAT_4:26;
end;
::$N A corrollary from the Fermat Theorem
theorem Th60:
for p being Prime st p = 4*k+1
ex a,b being positive Nat st a > b & p = a^2+b^2
proof
let p be Prime;
assume
A1: p = 4*k+1;
then p mod 4 = 1 by Lm6,NAT_D:21;
then consider a,b such that
A2: p = a^2+b^2 by NAT_5:23;
now
assume 0 >= a;
then a = 0;
hence contradiction by A2;
end;
then reconsider a as positive Nat;
now
assume 0 >= b;
then b = 0;
hence contradiction by A2;
end;
then reconsider b as positive Nat;
a <> b
proof
assume a = b;
then
A3: p = 2*(a^2) by A2;
p = 2*(2*k)+1 by A1;
hence contradiction by A3;
end;
then per cases by XXREAL_0:1;
suppose
A4: a < b;
take b,a;
thus thesis by A2,A4;
end;
suppose
A5: a > b;
take a,b;
thus thesis by A2,A5;
end;
end;
:: Problem 77
theorem
for p being Prime st p = 4*k+1
ex a,b being positive Nat st p^2 = a^2+b^2
proof
let p be Prime;
assume p = 4*k+1;
then consider a,b being positive Nat such that
A1: a > b and
A2: p = a^2+b^2 by Th60;
A3: a-b > b-b by A1,XREAL_1:9;
then reconsider c = a-b as Nat by INT_1:3;
c > 0 by A3;
then reconsider c as positive Nat;
a^2-b^2 = c*(a+b);
then reconsider x = a^2-b^2 as positive Nat;
reconsider y = 2*a*b as positive Nat;
take x,y;
thus thesis by A2;
end;
theorem Th62:
5 divides n+1 or 5 divides n+7 or 5 divides n+9 or
5 divides n+13 or 5 divides n+15
proof
assume that
A1: not 5 divides n+1 and
A2: not 5 divides n+7 and
A3: not 5 divides n+9 and
A4: not 5 divides n+13;
A5: 1 mod 5 = 1 by NAT_D:24;
A6: 2 mod 5 = 2 by NAT_D:24;
A7: 3 mod 5 = 3 by NAT_D:24;
A8: 4 mod 5 = 4 by NAT_D:24;
A9: 5*1+2 mod 5 = 2 mod 5 by NAT_D:21;
A10: 5*2+3 mod 5 = 3 mod 5 by NAT_D:21;
A11: 5*1+4 mod 5 = 4 mod 5 by NAT_D:21;
A12: 5*3 mod 5 = 0;
A13: n+1-1 mod 5 = ((n+1 mod 5)-(1 mod 5)) mod 5 by INT_6:7;
A14: (n+15) mod 5 = ((n mod 5)+(15 mod 5)) mod 5 by NAT_D:66;
per cases by A1,Lm18;
suppose n+1 mod 5 = 1;
hence 5 divides n+15 by A12,A13,A14,INT_1:62;
end;
suppose n+1 mod 5 = 2;
then n+9 mod 5 = (2-1+4) mod 5 by A13,A5,A8,A11,NAT_D:66
.= 0 by NAT_D:25;
hence 5 divides n+15 by A3,INT_1:62;
end;
suppose (n+1) mod 5 = 3;
then n+13 mod 5 = (3-1+3) mod 5 by A5,A6,A13,A10,NAT_D:66
.= 0 by NAT_D:25;
hence 5 divides n+15 by A4,INT_1:62;
end;
suppose (n+1) mod 5 = 4;
then n+7 mod 5 = (4-1+2) mod 5 by A5,A9,A6,A7,A13,NAT_D:66
.= 0 by NAT_D:25;
hence 5 divides n+15 by A2,INT_1:62;
end;
end;
:: Problem 82
theorem
{n where n is Nat: n+1 is prime & n+3 is prime & n+7 is prime &
n+9 is prime & n+13 is prime & n+15 is prime} = {4}
proof
set A = {n where n is Nat: n+1 is prime & n+3 is prime & n+7 is prime &
n+9 is prime & n+13 is prime & n+15 is prime};
A1: 5 = 4+1;
thus A c= {4}
proof
let x be object;
assume x in A;
then consider n such that
A2: x = n and
A3: n+1 is prime and
A4: n+3 is prime and
A5: n+7 is prime and
A6: n+9 is prime and
A7: n+13 is prime and
A8: n+15 is prime;
now
assume n <> 4;
then per cases by XXREAL_0:1;
suppose n < 3+1;
then n <= 3 by NAT_1:13;
then n = 0 or ... or n = 3;
then per cases;
suppose n = 0;
hence contradiction by A3;
end;
suppose n = 1;
hence contradiction by A4,INT_2:29;
end;
suppose n = 2;
hence contradiction by A5,NAT_4:57;
end;
suppose n = 3;
hence contradiction by A3,INT_2:29;
end;
end;
suppose
A9: n > 4;
5 divides n+1 or 5 divides n+7 or 5 divides n+9 or 5 divides n+13 or
5 divides n+15 by Th62;
then 5 = n+1 or 5 = n+7 or 5 = n+9 or 5 = n+13 or 5 = n+15
by A3,A5,A6,A7,A8;
hence contradiction by A1,A9,XREAL_1:8;
end;
end;
hence thesis by A2,TARSKI:def 1;
end;
let x be object;
assume x in {4};
then
A10: x = 4 by TARSKI:def 1;
4+3 = 7 & 4+7 = 11 & 4+9 = 13 & 4+13 = 17 & 4+15 = 19;
hence thesis by A1,A10,PEPIN:59,60,NAT_4:26,27,28,29;
end;
:: Problem 176
theorem
r|^3 + (r+1)|^3 + (r+2)|^3 = (r+3)|^3 iff r = 3
proof
A1: r|^3 = r*r*r & (r+1)|^3 = (r+1)*(r+1)*(r+1) &
(r+2)|^3 = (r+2)*(r+2)*(r+2) &
(r+3)|^3 = (r+3)*(r+3)*(r+3) by POLYEQ_5:2;
thus r|^3 + (r+1)|^3 + (r+2)|^3 = (r+3)|^3 implies r = 3
proof
set t = r-3;
assume r|^3 + (r+1)|^3 + (r+2)|^3 = (r+3)|^3;
then
A2: (2*t)*(t*t+9*t+21) = 0 by A1;
delta(1,9,21) < 0;
then 1*t^2+9*t+21 > 0 by QUIN_1:3;
then 2*t = 0 by A2;
hence thesis;
end;
thus thesis by A1;
end;
begin :: Tools for computing prime numbers
reserve p for Prime;
theorem Th1:
p < 3 implies p = 2
proof
assume p < 3;
then p < 2+1;
then
A1: p <= 2 by NAT_1:13;
1 < p by INT_2:def 4;
then 1+1 <= p by NAT_1:13;
hence thesis by A1,XXREAL_0:1;
end;
theorem
p*p <= k < 9 implies p = 2
proof
assume p*p <= k < 9;
then p*p < 3*3 by XXREAL_0:2;
hence thesis by Th1,NAT_4:1;
end;
theorem Th3:
p < 5 implies p = 2 or p = 3
proof
assume p < 5;
then 1+1 < p+1 & p < 4+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 3;
hence thesis by Th1;
end;
suppose 3 <= p & p <= 3+1;
hence thesis by XPRIMES0:4,NAT_1:9;
end;
end;
theorem
p*p <= k < 25 implies p = 2 or p = 3
proof
assume p*p <= k < 25;
then p*p < 5*5 by XXREAL_0:2;
hence thesis by Th3,NAT_4:1;
end;
theorem Th5:
p < 7 implies p = 2 or p = 3 or p = 5
proof
assume p < 7;
then 1+1 < p+1 & p < 6+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 5;
hence thesis by Th3;
end;
suppose 5 <= p & p <= 5+1;
hence thesis by XPRIMES0:6,NAT_1:9;
end;
end;
theorem
p*p <= k < 49 implies p = 2 or p = 3 or p = 5
proof
assume p*p <= k < 49;
then p*p < 7*7 by XXREAL_0:2;
hence thesis by Th5,NAT_4:1;
end;
theorem Th7:
p < 11 implies p = 2 or p = 3 or p = 5 or p = 7
proof
assume p < 11;
then 1+1 < p+1 & p < 10+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 7;
hence thesis by Th5;
end;
suppose 7 <= p & p <= 7+1;
hence thesis by XPRIMES0:8,NAT_1:9;
end;
suppose 8 <= p & p <= 8+1;
hence thesis by XPRIMES0:8,9,NAT_1:9;
end;
suppose 9 <= p & p <= 9+1;
hence thesis by XPRIMES0:9,10,NAT_1:9;
end;
end;
theorem
p*p <= k < 121 implies p = 2 or p = 3 or p = 5 or p = 7
proof
assume p*p <= k < 121;
then p*p < 11*11 by XXREAL_0:2;
hence thesis by Th7,NAT_4:1;
end;
theorem Th9:
p < 13 implies p = 2 or p = 3 or p = 5 or p = 7 or p = 11
proof
assume p < 13;
then 1+1 < p+1 & p < 12+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 11;
hence thesis by Th7;
end;
suppose 11 <= p & p <= 11+1;
hence thesis by XPRIMES0:12,NAT_1:9;
end;
end;
theorem
p*p <= k < 169 implies p = 2 or p = 3 or p = 5 or p = 7 or p = 11
proof
assume p*p <= k < 169;
then p*p < 13*13 by XXREAL_0:2;
hence thesis by Th9,NAT_4:1;
end;
theorem Th11:
p < 17 implies p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13
proof
assume p < 17;
then 1+1 < p+1 & p < 16+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 13;
hence thesis by Th9;
end;
suppose 13 <= p & p <= 13+1;
hence thesis by XPRIMES0:14,NAT_1:9;
end;
suppose 14 <= p & p <= 14+1;
hence thesis by XPRIMES0:14,15,NAT_1:9;
end;
suppose 15 <= p & p <= 15+1;
hence thesis by XPRIMES0:15,16,NAT_1:9;
end;
end;
theorem
p*p <= k < 289 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13
proof
assume p*p <= k < 289;
then p*p < 17*17 by XXREAL_0:2;
hence thesis by Th11,NAT_4:1;
end;
theorem Th13:
p < 19 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17
proof
assume p < 19;
then 1+1 < p+1 & p < 18+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 17;
hence thesis by Th11;
end;
suppose 17 <= p & p <= 17+1;
hence thesis by XPRIMES0:18,NAT_1:9;
end;
end;
theorem
p*p <= k < 361 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17
proof
assume p*p <= k < 361;
then p*p < 19*19 by XXREAL_0:2;
hence thesis by Th13,NAT_4:1;
end;
theorem Th15:
p < 23 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
proof
assume p < 23;
then 1+1 < p+1 & p < 22+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 19;
hence thesis by Th13;
end;
suppose 19 <= p & p <= 19+1;
hence thesis by XPRIMES0:20,NAT_1:9;
end;
suppose 20 <= p & p <= 20+1;
hence thesis by XPRIMES0:20,21,NAT_1:9;
end;
suppose 21 <= p & p <= 21+1;
hence thesis by XPRIMES0:21,22,NAT_1:9;
end;
end;
theorem
p*p <= k < 529 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
proof
assume p*p <= k < 529;
then p*p < 23*23 by XXREAL_0:2;
hence thesis by Th15,NAT_4:1;
end;
theorem Th17:
p < 29 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
or p = 23
proof
assume p < 29;
then 1+1 < p+1 & p < 28+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 23;
hence thesis by Th15;
end;
suppose 23 <= p & p <= 23+1;
hence thesis by XPRIMES0:24,NAT_1:9;
end;
suppose 24 <= p & p <= 24+1;
hence thesis by XPRIMES0:24,25,NAT_1:9;
end;
suppose 25 <= p & p <= 25+1;
hence thesis by XPRIMES0:25,26,NAT_1:9;
end;
suppose 26 <= p & p <= 26+1;
hence thesis by XPRIMES0:26,27,NAT_1:9;
end;
suppose 27 <= p & p <= 27+1;
hence thesis by XPRIMES0:27,28,NAT_1:9;
end;
end;
theorem
p*p <= k < 841 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
or p = 23
proof
assume p*p <= k < 841;
then p*p < 29*29 by XXREAL_0:2;
hence thesis by Th17,NAT_4:1;
end;
theorem Th19:
p < 31 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
or p = 23 or p = 29
proof
assume p < 31;
then 1+1 < p+1 & p < 30+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 29;
hence thesis by Th17;
end;
suppose 29 <= p & p <= 29+1;
hence thesis by XPRIMES0:30,NAT_1:9;
end;
end;
theorem
p*p <= k < 961 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19
or p = 23 or p = 29
proof
assume p*p <= k < 961;
then p*p < 31*31 by XXREAL_0:2;
hence thesis by Th19,NAT_4:1;
end;
theorem Th21:
p < 37 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31
proof
assume p < 37;
then 1+1 < p+1 & p < 36+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 31;
hence thesis by Th19;
end;
suppose 31 <= p & p <= 31+1;
hence thesis by XPRIMES0:32,NAT_1:9;
end;
suppose 32 <= p & p <= 32+1;
hence thesis by XPRIMES0:32,33,NAT_1:9;
end;
suppose 33 <= p & p <= 33+1;
hence thesis by XPRIMES0:33,34,NAT_1:9;
end;
suppose 34 <= p & p <= 34+1;
hence thesis by XPRIMES0:34,35,NAT_1:9;
end;
suppose 35 <= p & p <= 35+1;
hence thesis by XPRIMES0:35,36,NAT_1:9;
end;
end;
theorem
p*p <= k < 1369 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31
proof
assume p*p <= k < 1369;
then p*p < 37*37 by XXREAL_0:2;
hence thesis by Th21,NAT_4:1;
end;
theorem Th23:
p < 41 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37
proof
assume p < 41;
then 1+1 < p+1 & p < 40+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 37;
hence thesis by Th21;
end;
suppose 37 <= p & p <= 37+1;
hence thesis by XPRIMES0:38,NAT_1:9;
end;
suppose 38 <= p & p <= 38+1;
hence thesis by XPRIMES0:38,39,NAT_1:9;
end;
suppose 39 <= p & p <= 39+1;
hence thesis by XPRIMES0:39,40,NAT_1:9;
end;
end;
theorem
p*p <= k < 1681 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37
proof
assume p*p <= k < 1681;
then p*p < 41*41 by XXREAL_0:2;
hence thesis by Th23,NAT_4:1;
end;
theorem Th25:
p < 43 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41
proof
assume p < 43;
then 1+1 < p+1 & p < 42+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 41;
hence thesis by Th23;
end;
suppose 41 <= p & p <= 41+1;
hence thesis by XPRIMES0:42,NAT_1:9;
end;
end;
theorem
p*p <= k < 1849 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41
proof
assume p*p <= k < 1849;
then p*p < 43*43 by XXREAL_0:2;
hence thesis by Th25,NAT_4:1;
end;
theorem Th27:
p < 47 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43
proof
assume p < 47;
then 1+1 < p+1 & p < 46+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 43;
hence thesis by Th25;
end;
suppose 43 <= p & p <= 43+1;
hence thesis by XPRIMES0:44,NAT_1:9;
end;
suppose 44 <= p & p <= 44+1;
hence thesis by XPRIMES0:44,45,NAT_1:9;
end;
suppose 45 <= p & p <= 45+1;
hence thesis by XPRIMES0:45,46,NAT_1:9;
end;
end;
theorem
p*p <= k < 2209 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43
proof
assume p*p <= k < 2209;
then p*p < 47*47 by XXREAL_0:2;
hence thesis by Th27,NAT_4:1;
end;
theorem Th29:
p < 53 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47
proof
assume p < 53;
then 1+1 < p+1 & p < 52+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 47;
hence thesis by Th27;
end;
suppose 47 <= p & p <= 47+1;
hence thesis by XPRIMES0:48,NAT_1:9;
end;
suppose 48 <= p & p <= 48+1;
hence thesis by XPRIMES0:48,49,NAT_1:9;
end;
suppose 49 <= p & p <= 49+1;
hence thesis by XPRIMES0:49,50,NAT_1:9;
end;
suppose 50 <= p & p <= 50+1;
hence thesis by XPRIMES0:50,51,NAT_1:9;
end;
suppose 51 <= p & p <= 51+1;
hence thesis by XPRIMES0:51,52,NAT_1:9;
end;
end;
theorem
p*p <= k < 2809 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47
proof
assume p*p <= k < 2809;
then p*p < 53*53 by XXREAL_0:2;
hence thesis by Th29,NAT_4:1;
end;
theorem Th31:
p < 59 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
proof
assume p < 59;
then 1+1 < p+1 & p < 58+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 53;
hence thesis by Th29;
end;
suppose 53 <= p & p <= 53+1;
hence thesis by XPRIMES0:54,NAT_1:9;
end;
suppose 54 <= p & p <= 54+1;
hence thesis by XPRIMES0:54,55,NAT_1:9;
end;
suppose 55 <= p & p <= 55+1;
hence thesis by XPRIMES0:55,56,NAT_1:9;
end;
suppose 56 <= p & p <= 56+1;
hence thesis by XPRIMES0:56,57,NAT_1:9;
end;
suppose 57 <= p & p <= 57+1;
hence thesis by XPRIMES0:57,58,NAT_1:9;
end;
end;
theorem
p*p <= k < 3481 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
proof
assume p*p <= k < 3481;
then p*p < 59*59 by XXREAL_0:2;
hence thesis by Th31,NAT_4:1;
end;
theorem Th33:
p < 61 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59
proof
assume p < 61;
then 1+1 < p+1 & p < 60+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 59;
hence thesis by Th31;
end;
suppose 59 <= p & p <= 59+1;
hence thesis by XPRIMES0:60,NAT_1:9;
end;
end;
theorem
p*p <= k < 3721 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59
proof
assume p*p <= k < 3721;
then p*p < 61*61 by XXREAL_0:2;
hence thesis by Th33,NAT_4:1;
end;
theorem Th35:
p < 67 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61
proof
assume p < 67;
then 1+1 < p+1 & p < 66+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 61;
hence thesis by Th33;
end;
suppose 61 <= p & p <= 61+1;
hence thesis by XPRIMES0:62,NAT_1:9;
end;
suppose 62 <= p & p <= 62+1;
hence thesis by XPRIMES0:62,63,NAT_1:9;
end;
suppose 63 <= p & p <= 63+1;
hence thesis by XPRIMES0:63,64,NAT_1:9;
end;
suppose 64 <= p & p <= 64+1;
hence thesis by XPRIMES0:64,65,NAT_1:9;
end;
suppose 65 <= p & p <= 65+1;
hence thesis by XPRIMES0:65,66,NAT_1:9;
end;
end;
theorem
p*p <= k < 4489 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61
proof
assume p*p <= k < 4489;
then p*p < 67*67 by XXREAL_0:2;
hence thesis by Th35,NAT_4:1;
end;
theorem Th37:
p < 71 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67
proof
assume p < 71;
then 1+1 < p+1 & p < 70+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 67;
hence thesis by Th35;
end;
suppose 67 <= p & p <= 67+1;
hence thesis by XPRIMES0:68,NAT_1:9;
end;
suppose 68 <= p & p <= 68+1;
hence thesis by XPRIMES0:68,69,NAT_1:9;
end;
suppose 69 <= p & p <= 69+1;
hence thesis by XPRIMES0:69,70,NAT_1:9;
end;
end;
theorem
p*p <= k < 5041 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67
proof
assume p*p <= k < 5041;
then p*p < 71*71 by XXREAL_0:2;
hence thesis by Th37,NAT_4:1;
end;
theorem Th39:
p < 73 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71
proof
assume p < 73;
then 1+1 < p+1 & p < 72+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 71;
hence thesis by Th37;
end;
suppose 71 <= p & p <= 71+1;
hence thesis by XPRIMES0:72,NAT_1:9;
end;
end;
theorem
p*p <= k < 5329 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71
proof
assume p*p <= k < 5329;
then p*p < 73*73 by XXREAL_0:2;
hence thesis by Th39,NAT_4:1;
end;
theorem Th41:
p < 79 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73
proof
assume p < 79;
then 1+1 < p+1 & p < 78+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 73;
hence thesis by Th39;
end;
suppose 73 <= p & p <= 73+1;
hence thesis by XPRIMES0:74,NAT_1:9;
end;
suppose 74 <= p & p <= 74+1;
hence thesis by XPRIMES0:74,75,NAT_1:9;
end;
suppose 75 <= p & p <= 75+1;
hence thesis by XPRIMES0:75,76,NAT_1:9;
end;
suppose 76 <= p & p <= 76+1;
hence thesis by XPRIMES0:76,77,NAT_1:9;
end;
suppose 77 <= p & p <= 77+1;
hence thesis by XPRIMES0:77,78,NAT_1:9;
end;
end;
theorem
p*p <= k < 6241 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73
proof
assume p*p <= k < 6241;
then p*p < 79*79 by XXREAL_0:2;
hence thesis by Th41,NAT_4:1;
end;
theorem Th43:
p < 83 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79
proof
assume p < 83;
then 1+1 < p+1 & p < 82+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 79;
hence thesis by Th41;
end;
suppose 79 <= p & p <= 79+1;
hence thesis by XPRIMES0:80,NAT_1:9;
end;
suppose 80 <= p & p <= 80+1;
hence thesis by XPRIMES0:80,81,NAT_1:9;
end;
suppose 81 <= p & p <= 81+1;
hence thesis by XPRIMES0:81,82,NAT_1:9;
end;
end;
theorem
p*p <= k < 6889 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79
proof
assume p*p <= k < 6889;
then p*p < 83*83 by XXREAL_0:2;
hence thesis by Th43,NAT_4:1;
end;
theorem Th45:
p < 89 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
proof
assume p < 89;
then 1+1 < p+1 & p < 88+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 83;
hence thesis by Th43;
end;
suppose 83 <= p & p <= 83+1;
hence thesis by XPRIMES0:84,NAT_1:9;
end;
suppose 84 <= p & p <= 84+1;
hence thesis by XPRIMES0:84,85,NAT_1:9;
end;
suppose 85 <= p & p <= 85+1;
hence thesis by XPRIMES0:85,86,NAT_1:9;
end;
suppose 86 <= p & p <= 86+1;
hence thesis by XPRIMES0:86,87,NAT_1:9;
end;
suppose 87 <= p & p <= 87+1;
hence thesis by XPRIMES0:87,88,NAT_1:9;
end;
end;
theorem
p*p <= k < 7921 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
proof
assume p*p <= k < 7921;
then p*p < 89*89 by XXREAL_0:2;
hence thesis by Th45,NAT_4:1;
end;
theorem Th47:
p < 97 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
or p = 89
proof
assume p < 97;
then 1+1 < p+1 & p < 96+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 89;
hence thesis by Th45;
end;
suppose 89 <= p & p <= 89+1;
hence thesis by XPRIMES0:90,NAT_1:9;
end;
suppose 90 <= p & p <= 90+1;
hence thesis by XPRIMES0:90,91,NAT_1:9;
end;
suppose 91 <= p & p <= 91+1;
hence thesis by XPRIMES0:91,92,NAT_1:9;
end;
suppose 92 <= p & p <= 92+1;
hence thesis by XPRIMES0:92,93,NAT_1:9;
end;
suppose 93 <= p & p <= 93+1;
hence thesis by XPRIMES0:93,94,NAT_1:9;
end;
suppose 94 <= p & p <= 94+1;
hence thesis by XPRIMES0:94,95,NAT_1:9;
end;
suppose 95 <= p & p <= 95+1;
hence thesis by XPRIMES0:95,96,NAT_1:9;
end;
end;
theorem
p*p <= k < 9409 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
or p = 89
proof
assume p*p <= k < 9409;
then p*p < 97*97 by XXREAL_0:2;
hence thesis by Th47,NAT_4:1;
end;
theorem Th49:
p < 101 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
or p = 89 or p = 97
proof
assume p < 101;
then 1+1 < p+1 & p < 100+1 by XREAL_1:6,INT_2:def 4;
then per cases by NAT_1:13;
suppose 2 <= p & p < 97;
hence thesis by Th47;
end;
suppose 97 <= p & p <= 97+1;
hence thesis by XPRIMES0:98,NAT_1:9;
end;
suppose 98 <= p & p <= 98+1;
hence thesis by XPRIMES0:98,99,NAT_1:9;
end;
suppose 99 <= p & p <= 99+1;
hence thesis by XPRIMES0:99,100,NAT_1:9;
end;
end;
theorem
p*p <= k < 10201 implies
p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 or
p = 23 or p = 29 or p = 31 or p = 37 or p = 41 or p = 43 or p = 47 or p = 53
or p = 59 or p = 61 or p = 67 or p = 71 or p = 73 or p = 79 or p = 83
or p = 89 or p = 97
proof
assume p*p <= k < 10201;
then p*p < 101*101 by XXREAL_0:2;
hence thesis by Th49,NAT_4:1;
end;