:: Elementary Number Theory Problems. Part {VII}
:: by Artur Korni{\l}owicz
::
:: Received March 31, 2023
:: Copyright (c) 2023-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, XXREAL_0, ARYTM_3, XCMPLX_0, CARD_1,
INT_1, NEWTON, INT_2, ARYTM_1, SUBSET_1, FINSET_1, ABIAN, EULER_1,
MEMBERED, REAL_1, ZFMISC_1, NUMBER02, SQUARE_1, NUMBER03, NUMBER07,
COMPLEX1;
notations ZFMISC_1, SUBSET_1, ENUMSET1, ORDINAL1, NUMBERS, XCMPLX_0, FINSET_1,
MEMBERED, XREAL_0, INT_1, INT_2, XXREAL_0, SQUARE_1, NEWTON, ABIAN,
EULER_1, NUMBER02, NUMBER03, NAT_D;
constructors NAT_D, ABIAN, NAT_6, ENUMSET1, EULER_1, PEPIN, NUMBER02,
NUMBER03, NEWTON, EULER_2;
registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
NEWTON02, NEWTON03, ABIAN, NAT_6, NUMBER02, PYTHTRIP;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions MEMBERED, INT_2, NUMBER03;
equalities SQUARE_1, XCMPLX_0;
expansions INT_1, INT_2, NUMBER03, ZFMISC_1;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, WSIERP_1, EULER_2, XREAL_1,
XXREAL_0, NAT_1, NUMBER06, INT_4, EULER_1, ENUMSET1, GR_CY_3, XPRIMES0,
XPRIMES1, NUMBER02, NUMBER03, NUMBER04, XCMPLX_1, INT_5, INT_6, PREPOWER,
NUMBER05;
begin :: Preliminaries
Lm1: 2|^2 = 2*2 by NEWTON:81;
Lm2: 5|^2 = 5*5 by NEWTON:81;
reserve X for set;
reserve a,b,c,k,m,n for Nat;
reserve i,j for Integer;
reserve r for Real;
reserve p,p1,p2 for Prime;
theorem Th1:
m gcd (m*n) = m
proof
A1: m divides m*n;
for d being Nat st d divides m & d divides m*n holds d divides m;
hence thesis by A1,NAT_D:def 5;
end;
theorem
m <> 1 implies not m,m*n are_coprime by Th1;
theorem Th3:
i <> -1 & i <> 1 & i divides j implies not i divides j+1
proof
assume
A1: i <> -1 & i <> 1;
assume i divides j & i divides j+1;
then i divides j+1-j by INT_5:1;
hence contradiction by A1,INT_2:13;
end;
theorem Th4:
i <> -1 & i <> 1 & i divides j implies not i divides j-1
proof
assume
A1: i <> -1 & i <> 1;
assume i divides j & i divides j-1;
then i divides j-1-j by INT_5:1;
hence contradiction by A1,INT_2:13;
end;
theorem Th5:
i divides j implies i,j+1 are_coprime
proof
assume
A1: i divides j;
A2: 1 divides i & 1 divides j+1 by INT_2:12;
for m being Integer st m divides i & m divides j+1 holds m divides 1
proof
let m be Integer;
assume m divides i;
then
A3: m divides j by A1,INT_2:9;
assume m divides j+1;
then m divides j+1-j by A3,INT_5:1;
hence thesis;
end;
hence i gcd (j+1) = 1 by A2,INT_2:def 2;
end;
theorem Th6:
i divides j implies i,j-1 are_coprime
proof
assume
A1: i divides j;
A2: 1 divides i & 1 divides j-1 by INT_2:12;
for m being Integer st m divides i & m divides j-1 holds m divides 1
proof
let m be Integer;
assume m divides i;
then
A3: m divides j by A1,INT_2:9;
assume m divides j-1;
then m divides j-1-j by A3,INT_5:1;
then m = 1 or m = -1 by INT_2:13;
hence thesis by INT_2:14;
end;
hence i gcd (j-1) = 1 by A2,INT_2:def 2;
end;
theorem Th7:
a+b+c is odd & a,b,c are_mutually_coprime implies
a is odd & b is odd & c is odd
proof
assume that
A1: a+b+c is odd and
A2: a,b,c are_mutually_coprime;
assume a is even or b is even or c is even;
then per cases;
suppose
A3: a is even;
then b is odd & c is even or b is even & c is odd by A1;
then not a,c are_coprime or not a,b are_coprime by A3;
hence contradiction by A2;
end;
suppose
A4: b is even;
then a is odd & c is even or a is even & c is odd by A1;
then not b,c are_coprime or not b,a are_coprime by A4;
hence contradiction by A2;
end;
suppose
A5: c is even;
then a is odd & b is even or a is even & b is odd by A1;
then not c,b are_coprime or not c,a are_coprime by A5;
hence contradiction by A2;
end;
end;
theorem
4*n mod 8 = 0 or 4*n mod 8 = 4
proof
A1: n mod (7+1) = 0 or ... or n mod (7+1) = 7 by NUMBER03:11;
A2: 1*8+0 mod 8 = 0 & 1*8+4 mod 8 = 4 & 2*8+0 mod 8 = 0 & 2*8+4 mod 8 = 4
& 3*8+0 mod 8 = 0 & 3*8+4 mod 8 = 4 by NAT_D:def 2;
4 mod 8 = 4 by NAT_D:24;
then 4*n mod (7+1) = 4*0 mod 8 or ... or 4*n mod (7+1) = 4*7 mod 8
by A1,NAT_D:67;
hence 4*n mod 8 = 0 or 4*n mod 8 = 4 by A2;
end;
Lem1:
n divides k*m implies ex a,b st a divides k & b divides m & n = a*b
proof
assume
A1: n divides k*m;
take a = k gcd n;
A2: a divides k & a divides n by INT_2:def 2;
per cases;
suppose
A3: a = 0;
take m;
thus thesis by A3;
end;
suppose
A3: a <> 0;
consider b such that
A4: n = a * b by A2,NAT_D:def 3;
take b;
A7: n divides m * n;
a * m = |.m.| * a .= (m*k) gcd (m*n) by INT_6:16;
then n divides a * m by A1,A7,INT_2:def 2;
then b divides m by A3,A4,INT_4:7;
hence thesis by A2,A4;
end;
end;
Lem2:
n divides p1*p2 implies n = 1 or n = p1 or n = p2 or n = p1*p2
proof
assume n divides p1*p2;
then consider a,b such that
A1: a divides p1 & b divides p2 & n = a*b by Lem1;
(a = 1 or a = p1) & (b = 1 or b = p2) by A1,INT_2:def 4;
hence thesis by A1;
end;
theorem Th9:
n divides 2 implies n = 1 or n = 2 by XPRIMES1:2;
theorem Th10:
n divides 6 implies n = 1 or n = 2 or n = 3 or n = 6
proof
6 = 2*3;
hence thesis by Lem2,XPRIMES1:2,3;
end;
theorem Th11:
n divides 9 implies n = 1 or n = 3 or n = 9
proof
9 = 3*3;
hence thesis by Lem2,XPRIMES1:3;
end;
theorem Th12:
n divides 10 implies n = 1 or n = 2 or n = 5 or n = 10
proof
10 = 2*5;
hence thesis by Lem2,XPRIMES1:2,5;
end;
theorem Th13:
n divides 25 implies n = 1 or n = 5 or n = 25
proof
25 = 5*5;
hence thesis by Lem2,XPRIMES1:5;
end;
theorem Th14:
n divides 26 implies n = 1 or n = 2 or n = 13 or n = 26
proof
26 = 2*13;
hence thesis by Lem2,XPRIMES1:2,13;
end;
theorem Th15:
n divides 36 implies n = 1 or n = 2 or n = 3 or n = 4 or n = 6 or n = 9
or n = 12 or n = 18 or n = 36
proof
assume n divides 36;
then n divides 6*6;
then consider a,b such that
A1: a divides 6 & b divides 6 and
A2: n = a*b by Lem1;
(a = 1 or a = 2 or a = 3 or a = 6) &
(b = 1 or b = 2 or b = 3 or b = 6) by A1,Th10;
hence thesis by A2;
end;
theorem Th16:
n divides 50 implies n = 1 or n = 2 or n = 5 or n = 10 or n = 25 or n = 50
proof
assume n divides 50;
then n divides 2*25;
then consider a,b such that
A1: a divides 2 & b divides 25 and
A2: n = a*b by Lem1;
(a = 1 or a = 2) & (b = 1 or b = 5 or b = 25) by A1,Th9,Th13;
hence thesis by A2;
end;
theorem Th17:
n divides 65 implies n = 1 or n = 5 or n = 13 or n = 65
proof
65 = 5*13;
hence thesis by Lem2,XPRIMES1:5,13;
end;
theorem Th18:
n divides 82 implies n = 1 or n = 2 or n = 41 or n = 82
proof
82 = 2*41;
hence thesis by Lem2,XPRIMES1:2,41;
end;
theorem Th19:
n divides 122 implies n = 1 or n = 2 or n = 61 or n = 122
proof
122 = 2*61;
hence thesis by Lem2,XPRIMES1:2,61;
end;
theorem Th20:
n divides 145 implies n = 1 or n = 5 or n = 29 or n = 145
proof
145 = 5*29;
hence thesis by Lem2,XPRIMES1:5,29;
end;
theorem Th21:
n divides 226 implies n = 1 or n = 2 or n = 113 or n = 226
proof
226 = 2*113;
hence thesis by Lem2,XPRIMES1:2,113;
end;
theorem Th22:
n divides 325 implies n = 1 or n = 5 or n = 13 or n = 25 or n = 65 or n = 325
proof
assume n divides 325;
then n divides 13*25;
then consider a,b such that
A1: a divides 13 & b divides 25 and
A2: n = a*b by Lem1;
(a = 1 or a = 13) &
(b = 1 or b = 5 or b = 25) by A1,Th13,XPRIMES1:13;
hence thesis by A2;
end;
theorem Th23:
n divides 362 implies n = 1 or n = 2 or n = 181 or n = 362
proof
362 = 2*181;
hence thesis by Lem2,XPRIMES1:2,181;
end;
theorem Th24:
n divides 485 implies n = 1 or n = 5 or n = 97 or n = 485
proof
485 = 5*97;
hence thesis by Lem2,XPRIMES1:5,97;
end;
theorem Th25:
n divides 626 implies n = 1 or n = 2 or n = 313 or n = 626
proof
626 = 2*313;
hence thesis by Lem2,XPRIMES1:2,313;
end;
theorem Th26:
m * n = p implies m = 1 & n = p or m = p & n = 1
proof
assume
A1: m*n = p;
m divides m*n & n divides m*n;
then (m = 1 or m = p) & (n = 1 or n = p) by A1,INT_2:def 4;
hence thesis by A1;
end;
theorem Th27:
m * n = 10 implies m = 1 & n = 10
or m = 2 & n = 5
or m = 5 & n = 2
or m = 10 & n = 1
proof
assume
A1: m*n = 10;
m divides m*n;
then m = 1 or m = 2 or m = 5 or m = 10 by A1,Th12;
hence thesis by A1;
end;
theorem Th28:
m * n = 25 implies m = 1 & n = 25
or m = 5 & n = 5
or m = 25 & n = 1
proof
assume
A1: m*n = 25;
m divides m*n;
then m = 1 or m = 5 or m = 25 by A1,Th13;
hence thesis by A1;
end;
theorem Th29:
m * n = 26 implies m = 1 & n = 26
or m = 2 & n = 13
or m = 13 & n = 2
or m = 26 & n = 1
proof
assume
A1: m*n = 26;
m divides m*n;
then m = 1 or m = 2 or m = 13 or m = 26 by A1,Th14;
hence thesis by A1;
end;
theorem Th30:
m * n = 50 implies m = 1 & n = 50
or m = 2 & n = 25
or m = 5 & n = 10
or m = 10 & n = 5
or m = 25 & n = 2
or m = 50 & n = 1
proof
assume
A1: m*n = 50;
m divides m*n;
then m = 1 or m = 2 or m = 5 or m = 10 or m = 25 or m = 50 by A1,Th16;
hence thesis by A1;
end;
theorem Th31:
m * n = 65 implies m = 1 & n = 65
or m = 5 & n = 13
or m = 13 & n = 5
or m = 65 & n = 1
proof
assume
A1: m*n = 65;
m divides m*n;
then m = 1 or m = 5 or m = 13 or m = 65 by A1,Th17;
hence thesis by A1;
end;
theorem Th32:
m * n = 82 implies m = 1 & n = 82
or m = 2 & n = 41
or m = 41 & n = 2
or m = 82 & n = 1
proof
assume
A1: m*n = 82;
m divides m*n;
then m = 1 or m = 2 or m = 41 or m = 82 by A1,Th18;
hence thesis by A1;
end;
theorem Th33:
m * n = 122 implies m = 1 & n = 122
or m = 2 & n = 61
or m = 61 & n = 2
or m = 122 & n = 1
proof
assume
A1: m*n = 122;
m divides m*n;
then m = 1 or m = 2 or m = 61 or m = 122 by A1,Th19;
hence thesis by A1;
end;
theorem Th34:
m * n = 145 implies m = 1 & n = 145
or m = 5 & n = 29
or m = 29 & n = 5
or m = 145 & n = 1
proof
assume
A1: m*n = 145;
m divides m*n;
then m = 1 or m = 5 or m = 29 or m = 145 by A1,Th20;
hence thesis by A1;
end;
theorem Th35:
m * n = 226 implies m = 1 & n = 226
or m = 2 & n = 113
or m = 113 & n = 2
or m = 226 & n = 1
proof
assume
A1: m*n = 226;
m divides m*n;
then m = 1 or m = 2 or m = 113 or m = 226 by A1,Th21;
hence thesis by A1;
end;
theorem Th36:
m * n = 325 implies m = 1 & n = 325
or m = 5 & n = 65
or m = 13 & n = 25
or m = 25 & n = 13
or m = 65 & n = 5
or m = 325 & n = 1
proof
assume
A1: m*n = 325;
m divides m*n;
then m = 1 or m = 5 or m = 13 or m = 25 or m = 65 or m = 325 by A1,Th22;
hence thesis by A1;
end;
theorem Th37:
m * n = 362 implies m = 1 & n = 362
or m = 2 & n = 181
or m = 181 & n = 2
or m = 362 & n = 1
proof
assume
A1: m*n = 362;
m divides m*n;
then m = 1 or m = 2 or m = 181 or m = 362 by A1,Th23;
hence thesis by A1;
end;
theorem Th38:
m * n = 485 implies m = 1 & n = 485
or m = 5 & n = 97
or m = 97 & n = 5
or m = 485 & n = 1
proof
assume
A1: m*n = 485;
m divides m*n;
then m = 1 or m = 5 or m = 97 or m = 485 by A1,Th24;
hence thesis by A1;
end;
theorem Th39:
m * n = 626 implies m = 1 & n = 626
or m = 2 & n = 313
or m = 313 & n = 2
or m = 626 & n = 1
proof
assume
A1: m*n = 626;
m divides m*n;
then m = 1 or m = 2 or m = 313 or m = 626 by A1,Th25;
hence thesis by A1;
end;
theorem Th40:
p1 <> p2 implies 2 <= p1 & 3 <= p2 or 3 <= p1 & 2 <= p2
proof
assume
A1: p1 <> p2;
assume 2 > p1 or 3 > p2;
then per cases;
suppose p1 < 1+1;
then p1 <= 1 by NAT_1:13;
hence thesis by INT_2:def 4;
end;
suppose
A2: p2 < 3;
1 < p2 by INT_2:def 4;
then
A3: 1+1 <= p2 by NAT_1:13;
1 < p1 by INT_2:def 4;
then
A4: 1+1 <= p1 by NAT_1:13;
2 = 3-1;
then p2 = 0 or ... or p2 = 2 by A2,NUMBER02:7;
then 2 < p1 by A1,A4,INT_2:def 4,XXREAL_0:1;
then 2+1 <= p1 by NAT_1:13;
hence thesis by A3;
end;
end;
begin :: Problem 48
definition
let n be Nat;
pred n satisfies_Sierpinski_problem_48 means
ex a,b,c being Nat st
n = a+b+c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime;
end;
theorem Th41:
n is even & n > 8 implies n satisfies_Sierpinski_problem_48
proof
assume that
A1: n is even and
A2: n > 8;
consider k such that
A3: 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;
6*k+1 = 2*(3*k)+1 & 6*k+3 = 2*(3*k+1)+1 & 6*k+5 = 2*(3*k+2)+1;
then per cases by A1,A3;
suppose
A4: n = 6*k;
then
A5: 6*k-5 > 8-5 by A2,XREAL_1:9;
then 6*k-5 > 3;
then reconsider c = 6*(k-1)+1 as Element of NAT by INT_1:3;
take a = 2, b = 3, c;
thus n = a+b+c by A4;
thus a > 1;
thus b > 1;
thus c > 1 by A5,XXREAL_0:2;
thus a,b are_coprime by XPRIMES1:2,3,INT_2:30;
2 divides 2*(3*(k-1));
hence a,c are_coprime by Th5;
3 divides 3*(2*(k-1));
hence b,c are_coprime by Th5;
end;
suppose
A6: n = 6*k+2;
then
A7: 6*k+2-7 > 8-7 by A2,XREAL_1:9;
then reconsider c = 6*(k-1)+1 as Element of NAT by INT_1:3;
take a = 3, b = 4, c;
thus n = a+b+c by A6;
thus a > 1;
thus b > 1;
thus c > 1 by A7;
4 = 3+1;
hence a,b are_coprime by Th5;
3 divides 3*(2*(k-1));
hence a,c are_coprime by Th5;
A8: 1 divides b by INT_2:12;
A9: 1 divides c by INT_2:12;
for d being Nat st d divides b & d divides c holds d divides 1
proof
let d be Nat such that
A10: d divides b and
A11: d divides c;
A12: 4 = 2*2;
A13: c = 2*(3*(k-1))+1;
d = 1 or d = 2 or d = 4 by A10,NUMBER05:21;
hence thesis by A11,A12,A13;
end;
hence b,c are_coprime by A8,A9,NAT_D:def 5;
end;
suppose
A14: n = 6*k+4;
then
A15: 6*k+4-5 > 8-5 by A2,XREAL_1:9;
then 6*k-1 > 3;
then reconsider c = 6*k-1 as Element of NAT by INT_1:3;
take a = 2, b = 3, c;
thus n = a+b+c by A14;
thus a > 1;
thus b > 1;
thus c > 1 by A15,XXREAL_0:2;
thus a,b are_coprime by XPRIMES1:2,3,INT_2:30;
2 divides 2*(3*k);
hence a,c are_coprime by Th6;
3 divides 3*(2*k);
hence b,c are_coprime by Th6;
end;
end;
:: Problem 48a
theorem
n > 17 implies n satisfies_Sierpinski_problem_48
proof
assume
A1: n > 17;
per cases;
suppose
A2: n is even;
n > 8 by A1,XXREAL_0:2;
hence thesis by A2,Th41;
end;
suppose
A3: n is odd;
consider k such that
A4: n = 12*k+(0 qua Nat) or ... or n = 12*k+(12-1) by NUMBER02:22;
consider i being Nat such that
A5: 0 <= i <= 11 and
A6: n = 12*k+i by A4;
A7: i = 0 or ... or i = 11 by A5;
A8: now
assume 9 divides 6*k-1;
then consider z being Integer such that
A9: 6*k-1 = 9*z;
3 divides 3*(2*k-3*z);
hence contradiction by A9,NAT_D:7;
end;
A10: now
assume 9 divides 6*k+1;
then consider z being Integer such that
A11: 6*k+1 = 9*z;
3 divides 3*(3*z-2*k);
hence contradiction by A11,NAT_D:7;
end;
12*k+0 = 2*(6*k) & 12*k+2 = 2*(6*k+1) & 12*k+4 = 2*(6*k+2) &
12*k+6 = 2*(6*k+3) & 12*k+8 = 2*(6*k+4) & 12*k+10 = 2*(6*k+5);
then per cases by A3,A6,A7;
suppose
A12: n = 12*k+1;
then 12*k+1-1 > 17-1 by A1,XREAL_1:9;
then 12*k/12 > 16/12 by XREAL_1:97;
then
A13: k > 1 by XXREAL_0:2;
then
A14: 6*k > 6*1 by XREAL_1:68;
k-1 > 1-1 by A13,XREAL_1:9;
then k-1 >= 0+1 by INT_1:7;
then 6*(k-1) >= 6*1 by XREAL_1:64;
then
A15: 6*(k-1)-1 >= 6-1 by XREAL_1:9;
then reconsider a = 6*(k-1)-1 as Element of NAT by INT_1:3;
A16: 6*k-1 > 6-1 by A14,XREAL_1:9;
then reconsider b = 6*(k-1)+5 as Element of NAT by INT_1:3;
set c = 9;
take a, b, c;
thus n = a+b+c by A12;
thus a > 1 by A15,XXREAL_0:2;
thus b > 1 by A16,XXREAL_0:2;
thus c > 1;
A17: 1 divides a by INT_2:12;
A18: 1 divides b by INT_2:12;
A19: 1 divides c by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A20: d divides a and
A21: d divides b;
A22: d divides b-a by A20,A21,INT_5:1;
A23: 3 divides 3*(2*(k-1)) & 6 divides 6*(k-1);
d = 1 or d = 2 or d = 3 or d = 6 by A22,Th10;
hence thesis by A20,A23,Th4;
end;
hence a,b are_coprime by A17,A18,NAT_D:def 5;
for d being Nat st d divides a & d divides c holds d divides 1
proof
let d be Nat such that
A24: d divides a and
A25: d divides c;
A26: 3 divides 3*(2*(k-1));
A27: now
assume 9 divides 6*k-7;
then consider z being Integer such that
A28: 6*k-7 = 9*z;
A29: 3 divides 3*(2*k-3*z);
(2*3+1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24;
hence contradiction by A28,A29;
end;
d = 1 or d = 3 or d = 9 by A25,Th11;
hence thesis by A24,A26,A27,Th4;
end;
hence a,c are_coprime by A17,A19,NAT_D:def 5;
for d being Nat st d divides b & d divides c holds d divides 1
proof
let d be Nat such that
A30: d divides b and
A31: d divides c;
A32: 3 divides 3*(2*k);
d = 1 or d = 3 or d = 9 by A31,Th11;
hence thesis by A30,A32,A8,Th4;
end;
hence b,c are_coprime by A18,A19,NAT_D:def 5;
end;
suppose
A33: n = 12*k+3;
then 12*k+3-3 > 17-3 by A1,XREAL_1:9;
then 12*k/12 > (1*12+2)/12 by XREAL_1:97;
then k > 1 by XXREAL_0:2;
then
A34: 6*k > 6*1 by XREAL_1:68;
then
A35: 6*k-1 > 6-1 by XREAL_1:9;
then reconsider a = 6*k-1 as Element of NAT by INT_1:3;
set b = 6*k+1;
set c = 3;
take a, b, c;
thus n = a+b+c by A33;
thus a > 1 by A35,XXREAL_0:2;
6*k+1 > 6+1 by A34,XREAL_1:6;
hence b > 1 by XXREAL_0:2;
thus c > 1;
A36: 1 divides a & 1 divides b by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A37: d divides a and
A38: d divides b;
A39: a = 2*(3*k)-1;
d divides b-a by A37,A38,INT_5:1;
then d = 1 or d = 2 by Th9;
hence thesis by A37,A39;
end;
hence a,b are_coprime by A36,NAT_D:def 5;
A40: 3 divides 3*(2*k);
hence a,c are_coprime by Th6;
thus b,c are_coprime by A40,Th5;
end;
suppose
A41: n = 12*k+5;
then 12*k+5-5 > 17-5 by A1,XREAL_1:9;
then 12*k/12 > 12/12 by XREAL_1:97;
then
A42: 6*k > 6*1 by XREAL_1:68;
then
A43: 6*k-5 > 6-5 by XREAL_1:9;
then reconsider a = 6*k-5 as Element of NAT by INT_1:3,XXREAL_0:2;
set b = 6*k+1;
set c = 9;
take a, b, c;
thus n = a+b+c by A41;
thus a > 1 by A43;
6*k+1 > 6+1 by A42,XREAL_1:8;
hence b > 1 by XXREAL_0:2;
thus c > 1;
A44: 1 divides a by INT_2:12;
A45: 1 divides b by INT_2:12;
A46: 1 divides c by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A47: d divides a and
A48: d divides b;
A49: 3 divides 3*(2*k) & 6 divides 6*k;
d divides b-a by A47,A48,INT_5:1;
then d = 1 or d = 2 or d = 3 or d = 6 by Th10;
hence thesis by A48,A49,Th3;
end;
hence a,b are_coprime by A44,A45,NAT_D:def 5;
for d being Nat st d divides a & d divides c holds d divides 1
proof
let d be Nat such that
A50: d divides a and
A51: d divides c;
A52: 3 divides 3*(2*(k-1));
A53: 6*k-5 = 6*(k-1)+1;
A54: now
assume 9 divides 6*k-5;
then consider z being Integer such that
A55: 6*k-5 = 9*z;
A56: 3 divides 3*(2*k-3*z);
(1*3+2) mod 3 = 2 mod 3 by NAT_D:21
.= 2 by NAT_D:24;
hence contradiction by A55,A56;
end;
d = 1 or d = 3 or d = 9 by A51,Th11;
hence thesis by A50,A52,A53,A54,Th3;
end;
hence a,c are_coprime by A44,A46,NAT_D:def 5;
for d being Nat st d divides b & d divides c holds d divides 1
proof
let d be Nat such that
A57: d divides b and
A58: d divides c;
A59: 3 divides 3*(2*k);
d = 1 or d = 3 or d = 9 by A58,Th11;
hence thesis by A57,A59,A10,Th3;
end;
hence b,c are_coprime by A45,A46,NAT_D:def 5;
end;
suppose
A60: n = 12*k+7;
set a = 6*k+6-1;
12*k+7-7 > 17-7 by A1,A60,XREAL_1:9;
then 12*k/12 > 10/12 by XREAL_1:97;
then
A61: k >= 0+1 by NAT_1:13;
then reconsider b = 6*k-1 as Element of NAT by INT_1:3;
set c = 3;
take a, b, c;
thus n = a+b+c by A60;
A62: 6*k >= 6*1 by A61,XREAL_1:64;
then 6*k+5 >= 6+5 by XREAL_1:6;
hence a > 1 by XXREAL_0:2;
6*k-1 >= 6-1 by A62,XREAL_1:9;
hence b > 1 by XXREAL_0:2;
thus c > 1;
A63: 1 divides a by INT_2:12;
A64: 1 divides b by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A65: d divides a and
A66: d divides b;
A67: 3 divides 3*(2*k) & 6 divides 6*k;
d divides a-b by A65,A66,INT_5:1;
then d = 1 or d = 2 or d = 3 or d = 6 by Th10;
hence thesis by A66,A67,Th4;
end;
hence a,b are_coprime by A63,A64,NAT_D:def 5;
3 divides 3*(2*(k+1));
hence a,c are_coprime by Th6;
3 divides 3*(2*k);
hence b,c are_coprime by Th6;
end;
suppose
A68: n = 12*k+9;
then 12*k+9-9 > 17-9 by A1,XREAL_1:9;
then
A69: 12*k/12 > 8/12 by XREAL_1:97;
then reconsider a = 6*k-1 as Element of NAT by INT_1:3;
set b = 6*k+1;
set c = 9;
take a, b, c;
thus n = a+b+c by A68;
k >= 0+1 by A69,NAT_1:13;
then
A70: 6*k >= 6*1 by XREAL_1:64;
then 6*k-1 >= 6-1 by XREAL_1:9;
hence a > 1 by XXREAL_0:2;
6*k+1 >= 6+1 by A70,XREAL_1:6;
hence b > 1 by XXREAL_0:2;
thus c > 1;
A71: 1 divides a by INT_2:12;
A72: 1 divides b by INT_2:12;
A73: 1 divides c by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A74: d divides a and
A75: d divides b;
A76: a = 2*(3*k)-1;
d divides b-a by A74,A75,INT_5:1;
then d = 1 or d = 2 by Th9;
hence thesis by A74,A76;
end;
hence a,b are_coprime by A71,A72,NAT_D:def 5;
for d being Nat st d divides a & d divides c holds d divides 1
proof
let d be Nat such that
A77: d divides a and
A78: d divides c;
A79: 3 divides 3*(2*k);
d = 1 or d = 3 or d = 9 by A78,Th11;
hence thesis by A8,A77,A79,Th4;
end;
hence a,c are_coprime by A71,A73,NAT_D:def 5;
for d being Nat st d divides b & d divides c holds d divides 1
proof
let d be Nat such that
A80: d divides b and
A81: d divides c;
A82: 3 divides 3*(2*k);
d = 1 or d = 3 or d = 9 by A81,Th11;
hence thesis by A10,A80,A82,Th3;
end;
hence b,c are_coprime by A72,A73,NAT_D:def 5;
end;
suppose
A83: n = 12*k+11;
set a = 6*k+1;
set b = 6*k+6+1;
set c = 3;
take a, b, c;
thus n = a+b+c by A83;
12*k+11-11 > 17-11 by A1,A83,XREAL_1:9;
then 12*k/12 > 6/12 by XREAL_1:97;
then k >= 0+1 by NAT_1:13;
then
A84: 6*k >= 6*1 by XREAL_1:64;
then 6*k+1 >= 6+1 by XREAL_1:6;
hence a > 1 by XXREAL_0:2;
6*k+7 >= 6+7 by A84,XREAL_1:6;
hence b > 1 by XXREAL_0:2;
thus c > 1;
A85: 1 divides a by INT_2:12;
A86: 1 divides b by INT_2:12;
for d being Nat st d divides a & d divides b holds d divides 1
proof
let d be Nat such that
A87: d divides a and
A88: d divides b;
A89: 3 divides 3*(2*k) & 6 divides 6*k;
d divides b-a by A87,A88,INT_5:1;
then d = 1 or d = 2 or d = 3 or d = 6 by Th10;
hence thesis by A87,A89,Th3;
end;
hence a,b are_coprime by A85,A86,NAT_D:def 5;
3 divides 3*(2*k);
hence a,c are_coprime by Th5;
3 divides 3*(2*k+2);
hence b,c are_coprime by Th5;
end;
end;
end;
Lm3:
now
let a,b,c such that
A1: 1 < b and
A2: 1 < c and
A3: a+b+c = 17;
assume a >= 15;
then a+b > 15+1 by A1,XREAL_1:8;
then a+b+c > 16+1 by A2,XREAL_1:8;
hence contradiction by A3;
end;
Lm4:
now
let n be odd Nat;
assume 1 < n & n < 15;
then 1 < n & n < 14+1;
then 1+1 <= n <= 14 by NAT_1:13;
then n = 2+0 or ... or n = 2+12 by NAT_1:62;
then n = 2*1 or n = 3 or n = 2*2 or n = 5 or n = 2*3 or n = 7 or n = 2*4
or n = 9 or n = 2*5 or n = 11 or n = 2*6 or n = 13 or n = 2*7;
hence n = 3 or n = 5 or n = 7 or n = 9 or n = 11 or n = 13;
end;
:: Problem 48b
theorem
not 17 satisfies_Sierpinski_problem_48
proof
given a,b,c being Nat such that
A1: 17 = a+b+c and
A2: a > 1 and
A3: b > 1 and
A4: c > 1 and
A5: a,b,c are_mutually_coprime;
A6: 17 = 2*8+1;
then a is odd by A1,A5,Th7;
then
A7: a = 3 or a = 5 or a = 7 or a = 9 or a = 11 or a = 13
by A1,A2,A3,A4,Lm4,Lm3;
b is odd by A1,A5,A6,Th7;
then
A8: b = 3 or b = 5 or b = 7 or b = 9 or b = 11 or b = 13
by A1,A2,A3,A4,Lm4,Lm3;
A9: c is odd by A1,A5,A6,Th7;
a+b+c = c+a+b;
then
A10: c = 3 or c = 5 or c = 7 or c = 9 or c = 11 or c = 13
by A1,A2,A3,A4,A9,Lm4,Lm3;
not 3,3*3 are_coprime by Th1;
hence contradiction by A1,A5,A7,A8,A10,EULER_1:1;
end;
begin :: Problem 80
theorem Th44:
for p,q being Prime, n being Nat st p*(p+1) + q*(q+1) = n*(n+1) holds
p = 2 & q = 2 & n = 3 or p = 5 & q = 3 & n = 6 or p = 3 & q = 5 & n = 6
proof
let p,q be Prime;
let n be Nat;
assume p*(p+1) + q*(q+1) = n*(n+1);
then
A1: p*(p+1) = (n-q) * (n+q+1);
A2: now
assume n <= q;
then n-q <= q-q by XREAL_1:9;
then n-q <= 0;
hence contradiction by A1;
end;
then
A3: n-q > q-q by XREAL_1:9;
A4: n-q in NAT by A2,INT_1:5;
p divides p*(p+1);
then per cases by A1,INT_5:7;
suppose p divides n-q;
then
A5: p <= n-q by A3,INT_2:27;
then
A6: p+1 <= n-q+1 by XREAL_1:6;
p*(p+1) <= (n-q)*(p+1) by A5,XREAL_1:64;
then n+q+1 <= p+1 by A1,A3,XREAL_1:68;
then n+q+1 <= n-q+1 by A6,XXREAL_0:2;
then n+q <= n-q by XREAL_1:8;
hence thesis by XREAL_1:6;
end;
suppose p divides n+q+1;
then consider k such that
A7: n+q+1 = p*k by NAT_D:def 3;
A8: p*(p+1) = (n-q)*(p*k) by A1,A7;
(n-q)*k*p/p = (n-q)*k by XCMPLX_1:89;
then
A9: p+1 = k*(n-q) by A8,XCMPLX_1:89;
k = 0 or k >= 0+1 by NAT_1:13;
then per cases by XXREAL_0:1;
suppose k = 0;
hence thesis by A7;
end;
suppose k = 1;
hence thesis by A7,A9;
end;
suppose k > 1;
then
A10: k+1 > 1+1 by XREAL_1:8;
A11: 2*q = k*p-1-(n-q) by A7
.= k*(k*(n-q)-1)-1-(n-q) by A9
.= (k+1) * ((k-1)*(n-q)-1);
then k+1 divides 2*q;
then per cases by A10,GR_CY_3:1,XPRIMES1:2;
suppose
A12: k+1 = q;
A13: 2*q/q = 2 by XCMPLX_1:89;
1 < q by INT_2:def 4;
then 1+1 <= q by NAT_1:13;
then
A14: q-2 in NAT by INT_1:5;
2 = ((k-1)*(n-q)-1) by A12,A11,A13,XCMPLX_1:89;
then per cases by A12,A14,A4,Th26,XPRIMES1:3;
suppose q-2 = 1 & n-q = 3;
then q = 3 & n = 6;
hence thesis by A9,A12;
end;
suppose q-2 = 3 & n-q = 1;
then q = 5 & n = 6;
hence thesis by A9,A12;
end;
end;
suppose
A15: k+1 = 2*q;
then (k+1)*1 = (k+1)*((k-1)*(n-q)-1) by A11;
then 1 = (k-1)*(n-q)-1 by XCMPLX_1:5;
then 2*(q-1)*(n-q) = 2*1 by A15;
then (q-1)*(n-q) = 1;
then q-1 = 1 & n-q = 1 by A4,NAT_1:15;
then q = 2 & n = 3;
hence thesis by A9,A15;
end;
end;
end;
end;
:: Problem 80
theorem
for p,q,r being Prime st p*(p+1) + q*(q+1) = r*(r+1) holds p = q = 2 & r = 3
proof
let p,q,r be Prime;
assume p*(p+1) + q*(q+1) = r*(r+1);
then per cases by Th44;
suppose p = 2 & q = 2 & r = 3;
hence thesis;
end;
suppose p = 5 & q = 3 & r = 6;
hence thesis by XPRIMES0:6;
end;
suppose p = 3 & q = 5 & r = 6;
hence thesis by XPRIMES0:6;
end;
end;
begin :: Problem 87
definition
let n be Nat;
pred n satisfies_Sierpinski_problem_87a means
ex a,b,c being Prime st a,b,c are_mutually_distinct & n|^2+1 = a*b*c;
pred n satisfies_Sierpinski_problem_87b means
ex a,b,c being odd Prime st a,b,c are_mutually_distinct & n|^2+1 = a*b*c;
end;
theorem Th46:
13|^2 + 1 = 2*5*17
proof
13|^2 = 13*13 by WSIERP_1:1;
hence thesis;
end;
theorem
13 satisfies_Sierpinski_problem_87a
proof
reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 17 as Prime by XPRIMES1:17;
take a,b,c;
thus thesis by Th46;
end;
theorem Th48:
17|^2 + 1 = 2*5*29
proof
17|^2 = 17*17 by WSIERP_1:1;
hence thesis;
end;
theorem
17 satisfies_Sierpinski_problem_87a
proof
reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 29 as Prime by XPRIMES1:29;
take a,b,c;
thus thesis by Th48;
end;
theorem Th50:
21|^2 + 1 = 2*13*17
proof
21|^2 = 21*21 by WSIERP_1:1;
hence thesis;
end;
theorem
21 satisfies_Sierpinski_problem_87a
proof
reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 13 as Prime by XPRIMES1:13;
reconsider c = 17 as Prime by XPRIMES1:17;
take a,b,c;
thus thesis by Th50;
end;
theorem Th52:
23|^2 + 1 = 2*5*53
proof
23|^2 = 23*23 by WSIERP_1:1;
hence thesis;
end;
theorem
23 satisfies_Sierpinski_problem_87a
proof
reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 53 as Prime by XPRIMES1:53;
take a,b,c;
thus thesis by Th52;
end;
theorem Th54:
27|^2 + 1 = 2*5*73
proof
27|^2 = 27*27 by WSIERP_1:1;
hence thesis;
end;
theorem
27 satisfies_Sierpinski_problem_87a
proof
reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 73 as Prime by XPRIMES1:73;
take a,b,c;
thus thesis by Th54;
end;
Lm5:
not 0 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 0|^2+1 = a*b*c;
a*b = 1 & c = 1 by A1,NAT_1:15;
hence thesis;
end;
Lm6:
not 1 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 1|^2+1 = a*b*c;
a*b = 1 & c = 2 or a*b = 2 & c = 1 by A1,Th26,XPRIMES1:2;
hence thesis by XPRIMES1:2,NAT_1:15;
end;
Lm7:
not 2 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 2|^2+1 = a*b*c;
2|^2 = 2*2 by WSIERP_1:1;
then a*b = 1 & c = 5 or a*b = 5 & c = 1 by A1,Th26,XPRIMES1:5;
hence thesis by XPRIMES1:5,NAT_1:15;
end;
Lm8:
not 3 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 3|^2+1 = a*b*c;
3|^2 = 3*3 by WSIERP_1:1;
then a*b = 1 & c = 10 or a*b = 2 & c = 5 or a*b = 5 & c = 2
or a*b = 10 & c = 1 by A1,Th27;
hence thesis by XPRIMES1:2,5,NAT_1:15,XPRIMES0:1;
end;
Lm9:
not 4 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 4|^2+1 = a*b*c;
4|^2 = 4*4 by WSIERP_1:1;
then a*b = 1 & c = 17 or a*b = 17 & c = 1 by A1,Th26,XPRIMES1:17;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm10:
not 5 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 5|^2+1 = a*b*c;
5|^2 = 5*5 by WSIERP_1:1;
then a*b = 1 & c = 26 or a*b = 2 & c = 13
or a*b = 13 & c = 2 or a*b = 26 & c = 1 by A1,Th29;
hence thesis by XPRIMES1:2,13,NAT_1:15,XPRIMES0:1;
end;
Lm11:
not 6 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 6|^2+1 = a*b*c;
6|^2 = 6*6 by WSIERP_1:1;
then a*b = 1 & c = 37 or a*b = 37 & c = 1 by A1,Th26,XPRIMES1:37;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm12:
not 7 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
A1: a,b,c are_mutually_distinct and
A2: 7|^2+1 = a*b*c;
7|^2 = 7*7 by WSIERP_1:1;
then per cases by A2,Th30;
suppose a*b = 1 & c = 50;
hence thesis by XPRIMES0:50;
end;
suppose a*b = 2 & c = 25;
hence thesis by XPRIMES0:25;
end;
suppose a*b = 5 & c = 10;
hence thesis by XPRIMES0:10;
end;
suppose a*b = 10 & c = 5;
hence thesis by A1,Th27;
end;
suppose a*b = 25 & c = 2;
then a = 1 & b = 25 or a = 5 & b = 5 or a = 25 & b = 1 by Th28;
hence thesis by A1,XPRIMES0:25;
end;
suppose a*b = 50 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm13:
not 8 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 8|^2+1 = a*b*c;
8|^2 = 8*8 by WSIERP_1:1;
then per cases by A1,Th31;
suppose a*b = 1 & c = 65;
hence thesis by XPRIMES0:65;
end;
suppose a*b = 5 & c = 13;
hence thesis by XPRIMES1:5;
end;
suppose a*b = 13 & c = 5;
hence thesis by XPRIMES1:13;
end;
suppose a*b = 65 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm14:
not 9 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 9|^2+1 = a*b*c;
9|^2 = 9*9 by WSIERP_1:1;
then per cases by A1,Th32;
suppose a*b = 1 & c = 82;
hence thesis by XPRIMES0:82;
end;
suppose a*b = 2 & c = 41;
hence thesis by XPRIMES1:2;
end;
suppose a*b = 41 & c = 2;
hence thesis by XPRIMES1:41;
end;
suppose a*b = 82 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm15:
not 10 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 10|^2+1 = a*b*c;
10|^2 = 10*10 by WSIERP_1:1;
then a*b = 1 & c = 101 or a*b = 101 & c = 1 by A1,Th26,XPRIMES1:101;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm16:
not 11 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 11|^2+1 = a*b*c;
11|^2 = 11*11 by WSIERP_1:1;
then per cases by A1,Th33;
suppose a*b = 1 & c = 122;
hence thesis by XPRIMES0:122;
end;
suppose a*b = 2 & c = 61;
hence thesis by XPRIMES1:2;
end;
suppose a*b = 61 & c = 2;
hence thesis by XPRIMES1:61;
end;
suppose a*b = 122 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm17:
not 12 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 12|^2+1 = a*b*c;
12|^2 = 12*12 by WSIERP_1:1;
then per cases by A1,Th34;
suppose a*b = 1 & c = 145;
hence thesis by XPRIMES0:145;
end;
suppose a*b = 5 & c = 29;
hence thesis by XPRIMES1:5;
end;
suppose a*b = 29 & c = 5;
hence thesis by XPRIMES1:29;
end;
suppose a*b = 145 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm18:
not 14 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 14|^2+1 = a*b*c;
14|^2 = 14*14 by WSIERP_1:1;
then a*b = 1 & c = 197 or a*b = 197 & c = 1 by A1,Th26,XPRIMES1:197;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm19:
not 15 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 15|^2+1 = a*b*c;
15|^2 = 15*15 by WSIERP_1:1;
then per cases by A1,Th35;
suppose a*b = 1 & c = 226;
hence thesis by XPRIMES0:226;
end;
suppose a*b = 2 & c = 113;
hence thesis by XPRIMES1:2;
end;
suppose a*b = 113 & c = 2;
hence thesis by XPRIMES1:113;
end;
suppose a*b = 226 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm20:
not 16 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 16|^2+1 = a*b*c;
16|^2 = 16*16 by WSIERP_1:1;
then a*b = 1 & c = 257 or a*b = 257 & c = 1 by A1,Th26,XPRIMES1:257;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm21:
not 18 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
A1: a,b,c are_mutually_distinct and
A2: 18|^2+1 = a*b*c;
18|^2 = 18*18 by WSIERP_1:1;
then per cases by A2,Th36;
suppose a*b = 1 & c = 325;
hence thesis by XPRIMES0:325;
end;
suppose a*b = 5 & c = 65;
hence thesis by XPRIMES1:5;
end;
suppose a*b = 13 & c = 25;
hence thesis by XPRIMES1:13;
end;
suppose a*b = 25 & c = 13;
then a = 1 & b = 25 or a = 5 & b = 5 or a = 25 & b = 1 by Th28;
hence thesis by A1,XPRIMES0:1;
end;
suppose that
A3: a*b = 65 and
A4: c = 5;
a = 1 & b = 65 or a = 5 & b = 13 or a = 13 & b = 5 or a = 65 & b = 1
by A3,Th31;
hence thesis by A1,A4,XPRIMES0:1;
end;
suppose a*b = 325 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm22:
not 19 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 19|^2+1 = a*b*c;
19|^2 = 19*19 by WSIERP_1:1;
then per cases by A1,Th37;
suppose a*b = 1 & c = 362;
hence thesis by XPRIMES0:362;
end;
suppose a*b = 2 & c = 181;
hence thesis by XPRIMES1:2;
end;
suppose a*b = 181 & c = 2;
hence thesis by XPRIMES1:181;
end;
suppose a*b = 362 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm23:
not 20 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 20|^2+1 = a*b*c;
20|^2 = 20*20 by WSIERP_1:1;
then a*b = 1 & c = 401 or a*b = 401 & c = 1 by A1,Th26,XPRIMES1:401;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm24:
not 22 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 22|^2+1 = a*b*c;
22|^2 = 22*22 by WSIERP_1:1;
then per cases by A1,Th38;
suppose a*b = 1 & c = 485;
hence thesis by XPRIMES0:485;
end;
suppose a*b = 5 & c = 97;
hence thesis by XPRIMES1:5;
end;
suppose a*b = 97 & c = 5;
hence thesis by XPRIMES1:97;
end;
suppose a*b = 485 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm25:
not 24 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 24|^2+1 = a*b*c;
24|^2 = 24*24 by WSIERP_1:1;
then a*b = 1 & c = 577 or a*b = 577 & c = 1 by A1,Th26,XPRIMES1:577;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
Lm26:
not 25 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 25|^2+1 = a*b*c;
25|^2 = 25*25 by WSIERP_1:1;
then per cases by A1,Th39;
suppose a*b = 1 & c = 626;
hence thesis by XPRIMES0:626;
end;
suppose a*b = 2 & c = 313;
hence thesis by XPRIMES1:2;
end;
suppose a*b = 313 & c = 2;
hence thesis by XPRIMES1:313;
end;
suppose a*b = 626 & c = 1;
hence thesis by XPRIMES0:1;
end;
end;
Lm27:
not 26 satisfies_Sierpinski_problem_87a
proof
given a,b,c being Prime such that
a,b,c are_mutually_distinct and
A1: 26|^2+1 = a*b*c;
26|^2 = 26*26 by WSIERP_1:1;
then a*b = 1 & c = 677 or a*b = 677 & c = 1 by A1,Th26,XPRIMES1:677;
hence thesis by NAT_1:15,XPRIMES0:1;
end;
:: Problem 87 a
theorem
n satisfies_Sierpinski_problem_87a & n <= 27 implies n in {13,17,21,23,27}
proof
assume
A1: n satisfies_Sierpinski_problem_87a;
assume n <= 27;
then n = 0 or ... or n = 27;
hence thesis by A1,Lm5,Lm6,
Lm7,Lm8,Lm9,Lm10,Lm11,Lm12,Lm13,Lm14,Lm15,Lm16,
Lm17,Lm18,Lm19,Lm20,Lm21,Lm22,Lm23,Lm24,Lm25,
Lm26,Lm27,ENUMSET1:def 3;
end;
theorem Th57:
112|^2 + 1 = 5*13*193
proof
112|^2 = 112*112 by WSIERP_1:1;
hence thesis;
end;
:: Problem 87 b
theorem
112 satisfies_Sierpinski_problem_87b
proof
5 = 2*2+1;
then reconsider a = 5 as odd Prime by XPRIMES1:5;
13 = 2*6+1;
then reconsider b = 13 as odd Prime by XPRIMES1:13;
193 = 2*96+1;
then reconsider c = 193 as odd Prime by XPRIMES1:193;
take a,b,c;
thus thesis by Th57;
end;
begin :: Problem 89
definition
let n;
pred n has_exactly_two_different_prime_divisors means
ex p,q being Prime st p <> q & p divides n & q divides n &
for r being Prime st r <> p & r <> q holds not r divides n;
end;
definition
let n be Complex;
pred n is_a_product_of_two_different_primes means
ex p,q being Prime st p <> q & n = p*q;
end;
theorem Th59:
for p,q being Prime, a,b being Nat st a <> 1 & b <> 1 & p*q = a*b holds
p = a & q = b or p = b & q = a
proof
let p,q be Prime, a,b be Nat such that
A1: a <> 1 and
A2: b <> 1 and
A3: p*q = a*b and
A4: p <> a or q <> b;
a divides a*b;
then per cases by A1,A3,GR_CY_3:1;
suppose
A5: a = p;
then q <> b by A4;
hence thesis by A3,A5,XCMPLX_1:5;
end;
suppose a = q;
hence thesis by A3,XCMPLX_1:5;
end;
suppose
A6: a = p*q;
then a*1 = a*b by A3;
hence thesis by A2,A6,XCMPLX_1:5;
end;
end;
theorem
n is_a_product_of_two_different_primes implies
for a,b st a <> 1 & b <> 1 & n = a*b holds a is prime & b is prime by Th59;
theorem Th61:
not p is_a_product_of_two_different_primes;
theorem
p1 <> p2 implies p1*p2 is_a_product_of_two_different_primes;
theorem Th63:
a <> 1 & a <> n & a is non prime & a divides n implies
not n is_a_product_of_two_different_primes by GR_CY_3:1;
theorem Th64:
not p*p is_a_product_of_two_different_primes
proof
given p1,q1 being Prime such that
A1: p1 <> q1 and
A2: p*p = p1*q1;
A3: p > 1 by INT_2:def 4;
A4: p1*p1/p1 = p1 & p1*q1/p1 = q1 by XCMPLX_1:89;
A5: q1*q1/q1 = q1 & p1*q1/q1 = p1 by XCMPLX_1:89;
p divides p*p;
then p divides p1 or p divides q1 by A2,INT_5:7;
then per cases by A3,INT_2:def 4;
suppose p = p1;
hence thesis by A1,A2,A4;
end;
suppose p = q1;
hence thesis by A1,A2,A5;
end;
end;
theorem Th65:
n is_a_product_of_two_different_primes implies n >= 6
proof
given p,q being Prime such that
A1: p <> q and
A2: n = p*q;
A3: 6 = 2*3;
2 <= p & 3 <= q or 3 <= p & 2 <= q by A1,Th40;
hence thesis by A2,A3,XREAL_1:66;
end;
definition
let n;
pred n satisfies_Sierpinski_problem_89 means
n is_a_product_of_two_different_primes &
n+1 is_a_product_of_two_different_primes &
n+2 is_a_product_of_two_different_primes;
end;
reconsider P2 = 2 as Prime by XPRIMES1:2;
reconsider P3 = 3 as Prime by XPRIMES1:3;
reconsider P5 = 5 as Prime by XPRIMES1:5;
reconsider P7 = 7 as Prime by XPRIMES1:7;
reconsider P11 = 11 as Prime by XPRIMES1:11;
reconsider P13 = 13 as Prime by XPRIMES1:13;
reconsider P17 = 17 as Prime by XPRIMES1:17;
reconsider P19 = 19 as Prime by XPRIMES1:19;
reconsider P23 = 23 as Prime by XPRIMES1:23;
reconsider P29 = 29 as Prime by XPRIMES1:29;
reconsider P31 = 31 as Prime by XPRIMES1:31;
reconsider P43 = 43 as Prime by XPRIMES1:43;
reconsider P47 = 47 as Prime by XPRIMES1:47;
reconsider P67 = 67 as Prime by XPRIMES1:67;
reconsider P71 = 71 as Prime by XPRIMES1:71;
reconsider P101 = 101 as Prime by XPRIMES1:101;
theorem
33 satisfies_Sierpinski_problem_89
proof
set n = 33;
thus n is_a_product_of_two_different_primes
proof
take P3,P11;
thus thesis;
end;
thus n+1 is_a_product_of_two_different_primes
proof
take P2,P17;
thus thesis;
end;
thus n+2 is_a_product_of_two_different_primes
proof
take P5,P7;
thus thesis;
end;
end;
theorem
85 satisfies_Sierpinski_problem_89
proof
set n = 85;
thus n is_a_product_of_two_different_primes
proof
take P5,P17;
thus thesis;
end;
thus n+1 is_a_product_of_two_different_primes
proof
take P2,P43;
thus thesis;
end;
thus n+2 is_a_product_of_two_different_primes
proof
take P3,P29;
thus thesis;
end;
end;
theorem
93 satisfies_Sierpinski_problem_89
proof
set n = 93;
thus n is_a_product_of_two_different_primes
proof
take P3,P31;
thus thesis;
end;
thus n+1 is_a_product_of_two_different_primes
proof
take P2,P47;
thus thesis;
end;
thus n+2 is_a_product_of_two_different_primes
proof
take P5,P19;
thus thesis;
end;
end;
theorem
141 satisfies_Sierpinski_problem_89
proof
set n = 141;
thus n is_a_product_of_two_different_primes
proof
take P3,P47;
thus thesis;
end;
thus n+1 is_a_product_of_two_different_primes
proof
take P2,P71;
thus thesis;
end;
thus n+2 is_a_product_of_two_different_primes
proof
take P11,P13;
thus thesis;
end;
end;
theorem
201 satisfies_Sierpinski_problem_89
proof
set n = 201;
thus n is_a_product_of_two_different_primes
proof
take P3,P67;
thus thesis;
end;
thus n+1 is_a_product_of_two_different_primes
proof
take P2,P101;
thus thesis;
end;
thus n+2 is_a_product_of_two_different_primes
proof
take P7,P29;
thus thesis;
end;
end;
:: Problem 89 a
theorem
n satisfies_Sierpinski_problem_89 & n <= 201 implies n in {33,85,93,141,201}
proof
assume that
A1: n satisfies_Sierpinski_problem_89 and
A2: n <= 201 and
A3: not n in {33,85,93,141,201};
4 < 6 <= n by A1,Th65;
then
A4: 4 < n by XXREAL_0:2;
set a = n div 4, b = n mod 4;
A5: n = a * 4 + b by INT_1:59;
A6: b = 1
proof
b < 3+1 by NAT_D:1;
then b <= 3 by NAT_1:13;
then b = 0 or ... or b = 3;
then per cases;
suppose b = 0;
then n = 4*a by A5;
then 4 <> n & 4 divides n by A4;
hence thesis by A1,Th63,XPRIMES0:4;
end;
suppose b = 1;
hence thesis;
end;
suppose b = 2;
then n+2 = 4*(a+1) by A5;
then 4 <> n+2 & 4 divides n+2 by A4;
hence thesis by A1,Th63,XPRIMES0:4;
end;
suppose b = 3;
then n+1 = 4*(a+1) by A5;
then 4 <> n+1 & 4 divides n+1 by A4,NAT_1:11;
hence thesis by A1,Th63,XPRIMES0:4;
end;
end;
A7: a <> 0 by A4,A5,A6;
a*4+1 <= 50*4+1 by A2,A5,A6;
then a*4 <= 50*4 by XREAL_1:6;
then 1 <= a <= 50 by XREAL_1:68,A7,NAT_1:14;
then n = 1*4+1 or ... or n = 50*4+1 by A5,A6;
then per cases by A3,ENUMSET1:def 3;
suppose n = 5;
hence thesis by A1,Th61,XPRIMES1:5;
end;
suppose n = 9;
hence thesis by A1,Th61,XPRIMES1:11;
end;
suppose n = 13;
hence thesis by A1,Th61,XPRIMES1:13;
end;
suppose n = 17;
hence thesis by A1,Th61,XPRIMES1:17;
end;
suppose n = 21;
hence thesis by A1,Th61,XPRIMES1:23;
end;
suppose A: n = 25;
25 = 5*5;
hence thesis by A1,A,Th64,XPRIMES1:5;
end;
suppose n = 29;
hence thesis by A1,Th61,XPRIMES1:29;
end;
suppose n = 37;
hence thesis by A1,Th61,XPRIMES1:37;
end;
suppose n = 41;
hence thesis by A1,Th61,XPRIMES1:41;
end;
suppose n = 45;
hence thesis by A1,Th61,XPRIMES1:47;
end;
suppose A: n = 49;
49 = 7*7;
hence thesis by A1,A,Th64,XPRIMES1:7;
end;
suppose n = 53;
hence thesis by A1,Th61,XPRIMES1:53;
end;
suppose n = 57;
hence thesis by A1,Th61,XPRIMES1:59;
end;
suppose n = 61;
hence thesis by A1,Th61,XPRIMES1:61;
end;
suppose n = 65;
hence thesis by A1,Th61,XPRIMES1:67;
end;
suppose n = 69;
hence thesis by A1,Th61,XPRIMES1:71;
end;
suppose n = 73;
hence thesis by A1,Th61,XPRIMES1:73;
end;
suppose n = 77;
hence thesis by A1,Th61,XPRIMES1:79;
end;
suppose n = 81;
hence thesis by A1,Th61,XPRIMES1:83;
end;
suppose n = 89;
hence thesis by A1,Th61,XPRIMES1:89;
end;
suppose n = 97;
hence thesis by A1,Th61,XPRIMES1:97;
end;
suppose n = 101;
hence thesis by A1,Th61,XPRIMES1:101;
end;
suppose n = 105;
hence thesis by A1,Th61,XPRIMES1:107;
end;
suppose n = 109;
hence thesis by A1,Th61,XPRIMES1:109;
end;
suppose n = 113;
hence thesis by A1,Th61,XPRIMES1:113;
end;
suppose A: n = 117;
9 divides 9*13;
hence thesis by A1,A,Th63,XPRIMES0:9;
end;
suppose A: n = 121;
121 = 11*11;
hence thesis by A1,A,Th64,XPRIMES1:11;
end;
suppose n = 125;
hence thesis by A1,Th61,XPRIMES1:127;
end;
suppose n = 129;
hence thesis by A1,Th61,XPRIMES1:131;
end;
suppose A: n = 133;
9 divides 9*15;
hence thesis by A1,A,Th63,XPRIMES0:9;
end;
suppose n = 137;
hence thesis by A1,Th61,XPRIMES1:137;
end;
suppose A: n = 145;
21 divides 21*7;
hence thesis by A1,A,Th63,XPRIMES0:21;
end;
suppose n = 149;
hence thesis by A1,Th61,XPRIMES1:149;
end;
suppose A: n = 153;
14 divides 14*11;
hence thesis by A1,A,Th63,XPRIMES0:14;
end;
suppose n = 157;
hence thesis by A1,Th61,XPRIMES1:157;
end;
suppose n = 161;
hence thesis by A1,Th61,XPRIMES1:163;
end;
suppose n = 165;
hence thesis by A1,Th61,XPRIMES1:167;
end;
suppose A: n = 169;
169 = 13*13;
hence thesis by A1,A,Th64,XPRIMES1:13;
end;
suppose n = 173;
hence thesis by A1,Th61,XPRIMES1:173;
end;
suppose n = 177;
hence thesis by A1,Th61,XPRIMES1:179;
end;
suppose n = 181;
hence thesis by A1,Th61,XPRIMES1:181;
end;
suppose A: n = 185;
6 divides 6*31;
hence thesis by A1,A,Th63,XPRIMES0:6;
end;
suppose n = 189;
hence thesis by A1,Th61,XPRIMES1:191;
end;
suppose n = 193;
hence thesis by A1,Th61,XPRIMES1:193;
end;
suppose n = 197;
hence thesis by A1,Th61,XPRIMES1:197;
end;
end;
:: Problem 89 b
theorem
not ex n st
n satisfies_Sierpinski_problem_89 & n+1 satisfies_Sierpinski_problem_89 &
n+2 satisfies_Sierpinski_problem_89 & n+3 satisfies_Sierpinski_problem_89
proof
given n such that
A1: n satisfies_Sierpinski_problem_89 and
n+1 satisfies_Sierpinski_problem_89 and
n+2 satisfies_Sierpinski_problem_89 and
A2: n+3 satisfies_Sierpinski_problem_89;
A3: n is_a_product_of_two_different_primes by A1;
A4: n+1 is_a_product_of_two_different_primes by A1;
A5: n+2 is_a_product_of_two_different_primes by A1;
A6: n+3 is_a_product_of_two_different_primes by A2;
per cases by NUMBER06:19;
suppose
A7: 4 divides n;
consider p,q being Prime such that
A8: p <> q and
A9: n = p*q by A3;
A10: p divides p*q & q divides p*q;
4 divides p*q by A9,A7;
then p*q = 4 by GR_CY_3:1,XPRIMES0:4;
then (p = 1 or p = 2) & (q = 1 or q = 2) by A10,NUMBER05:21;
hence thesis by A8,INT_2:def 4;
end;
suppose
A11: 4 divides n+1;
consider p,q being Prime such that
A12: p <> q and
A13: n+1 = p*q by A4;
A14: p divides p*q & q divides p*q;
4 divides p*q by A13,A11;
then p*q = 4 by GR_CY_3:1,XPRIMES0:4;
then (p = 1 or p = 2) & (q = 1 or q = 2) by A14,NUMBER05:21;
hence thesis by A12,INT_2:def 4;
end;
suppose
A15: 4 divides n+2;
consider p,q being Prime such that
A16: p <> q and
A17: n+2 = p*q by A5;
A18: p divides p*q & q divides p*q;
4 divides p*q by A17,A15;
then p*q = 4 by GR_CY_3:1,XPRIMES0:4;
then (p = 1 or p = 2) & (q = 1 or q = 2) by A18,NUMBER05:21;
hence thesis by A16,INT_2:def 4;
end;
suppose
A19: 4 divides n+3;
consider p,q being Prime such that
A20: p <> q and
A21: n+3 = p*q by A6;
A22: p divides p*q & q divides p*q;
4 divides p*q by A21,A19;
then p*q = 4 by GR_CY_3:1,XPRIMES0:4;
then (p = 1 or p = 2) & (q = 1 or q = 2) by A22,NUMBER05:21;
hence thesis by A20,INT_2:def 4;
end;
end;
:: Problem 89 Examples
theorem
33 = 3*11 & 33 has_exactly_two_different_prime_divisors
proof
thus
A1: 33 = 3*11;
take P3, P11;
thus P3 <> P11;
thus P3 divides 33 by A1;
thus P11 divides 33 by A1;
let r be Prime such that
A2: r <> P3 & r <> P11;
assume r divides 33;
then r divides 3 or r divides 11 by A1,INT_5:7;
hence thesis by A2,XPRIMES0:1,XPRIMES1:3,11;
end;
theorem
34 = 2*17 & 34 has_exactly_two_different_prime_divisors
proof
thus
A1: 34 = 2*17;
take P2, P17;
thus P2 <> P17;
thus P2 divides 34 by A1;
thus P17 divides 34 by A1;
let r be Prime such that
A2: r <> P2 & r <> P17;
assume r divides 34;
then r divides 2 or r divides 17 by A1,INT_5:7;
hence thesis by A2,XPRIMES0:1,XPRIMES1:2,17;
end;
theorem
35 = 5*7 & 35 has_exactly_two_different_prime_divisors
proof
thus
A1: 35 = 5*7;
take P5, P7;
thus P5 <> P7;
thus P5 divides 35 by A1;
thus P7 divides 35 by A1;
let r be Prime such that
A2: r <> P5 & r <> P7;
assume r divides 35;
then r divides 5 or r divides 7 by A1,INT_5:7;
hence thesis by A2,XPRIMES0:1,XPRIMES1:5,7;
end;
theorem
36 = 2*2*3*3 & 36 has_exactly_two_different_prime_divisors
proof
thus
A1: 36 = 2*2*3*3;
take P2, P3;
thus P2 <> P3;
2*2*3*3 = 2*(2*3*3);
hence P2 divides 36;
thus P3 divides 36 by A1;
let r be Prime such that
A2: r <> P2 & r <> P3;
assume r divides 36;
then r = 1 or r = 2 or r = 3 or r = 4 or r = 6 or r = 9 or
r = 12 or r = 18 or r = 36 by Th15;
then r = 2 or r = 3 by INT_2:def 4,XPRIMES0:4,6,9,12,18,36;
hence thesis by A2;
end;
begin :: Problem 124
theorem Th77:
n = 28*k+1 implies 29 divides (2|^(2*n)+1)|^2 + 2|^2
proof
assume
A1: n = 28*k+1;
set x = (2|^(2*n)+1)|^2+2|^2;
A2: Euler 29 = 29-1 by EULER_1:20,XPRIMES1:29;
A3: 2|^28|^(2*k) = 2|^(28*(2*k)) by NEWTON:9;
(2 |^ Euler 29) mod 29 = 1 by EULER_2:18,XPRIMES1:2,29,INT_2:30;
then 2|^28,1 are_congruent_mod 29 by A2,PEPIN:39;
then 2|^28|^(2*k),1|^(2*k) are_congruent_mod 29 by GR_CY_3:34;
then
A4: 2|^(2*(28*k))*4,1*4 are_congruent_mod 29 by A3,INT_4:11;
2|^(2*(28*k+1)) = 2|^(2*(28*k)+2)
.= 2|^(2*(28*k)) * 2|^2 by NEWTON:8;
then 2|^(2*n)+1,4+1 are_congruent_mod 29 by A1,A4,Lm1;
then (2|^(2*n)+1)|^2,5|^2 are_congruent_mod 29 by GR_CY_3:34;
then x,29 are_congruent_mod 29 by Lm1,Lm2;
then x mod 29 = 29 mod 29 by NAT_D:64
.= 0 by NAT_D:25;
hence thesis by INT_1:62;
end;
theorem Th78:
k > 0 & n = 28*k+1 implies (2|^(2*n)+1)|^2 + 2|^2 is composite
proof
assume that
A1: k > 0 and
A2: n = 28*k+1;
set x = (2|^(2*n)+1)|^2+2|^2;
A3: (2|^(2*n)+1)|^2 = (2|^(2*n)+1)^2 by WSIERP_1:1;
A4: 2|^(2*n) = 4|^n by Lm1,NEWTON:9;
k >= 0+1 by A1,NAT_1:13;
then 28*k >= 28*1 by XREAL_1:64;
then 28*k+1 >= 28+1 by XREAL_1:6;
then 28*k+1 > 1 by XXREAL_0:2;
then 4|^n > 4|^1 by A2,PEPIN:66;
then 2|^(2*n)+1 > 4+1 by A4,XREAL_1:8;
then (2|^(2*n)+1)^2 > 5*5 by XREAL_1:96;
then
A5: x > 25+4 by A3,Lm1,XREAL_1:8;
assume x is non composite;
then x is prime by A5,XXREAL_0:2,NUMBER02:def 1;
hence thesis by A2,A5,Th77;
end;
:: Problem 124
theorem
{ (2|^(2*n)+1)|^2 + 2|^2 where n is Nat:
(2|^(2*n)+1)|^2 + 2|^2 is composite }
is infinite
proof
set X =
{ (2|^(2*n)+1)|^2+2|^2 where n is Nat:
(2|^(2*n)+1)|^2+2|^2 is composite };
set n = 28*1+1;
(2|^(2*n)+1)|^2+2|^2 is composite by Th78;
then
A1: (2|^(2*n)+1)|^2+2|^2 in X;
A2: X is natural-membered
proof
let x be object;
assume x in X;
then ex n st x = (2|^(2*n)+1)|^2+2|^2 & (2|^(2*n)+1)|^2+2|^2
is composite;
hence thesis;
end;
for a st a in X ex b st b > a & b in X
proof
let a;
assume a in X;
then consider n such that
A3: a = (2|^(2*n)+1)|^2+2|^2 and
(2|^(2*n)+1)|^2+2|^2 is composite;
per cases;
suppose
A4: n <> 0;
take b = (2|^(2*(28*n+1))+1)|^2+2|^2;
A5: (2|^(2*n)+1)|^2 = (2|^(2*n)+1)^2 by WSIERP_1:1;
A6: (2|^(2*(28*n+1))+1)|^2 = (2|^(2*(28*n+1))+1)^2 by WSIERP_1:1;
A7: 1*n <= 28*n by XREAL_1:64;
28*n+0 < 28*n+1 by XREAL_1:8;
then n < 28*n+1 by A7,XXREAL_0:2;
then 2*n < 2*(28*n+1) by XREAL_1:68;
then 2|^(2*n) < 2|^(2*(28*n+1)) by PEPIN:66;
then 2|^(2*n)+1 < 2|^(2*(28*n+1))+1 by XREAL_1:8;
then (2|^(2*n)+1)^2 < (2|^(2*(28*n+1))+1)^2 by XREAL_1:96;
hence b > a by A3,A5,A6,XREAL_1:8;
b is composite by A4,Th78;
hence thesis;
end;
suppose n = 0;
then
A8: a = (1+1)|^2+4 by A3,Lm1,NEWTON:4
.= 4+4 by Lm1;
set z = 28*1+1;
take b = (2|^(2*z)+1)|^2 + 2|^2;
A9: 2|^0 = 1 by NEWTON:4;
2|^(2*z) > 2|^0 by PEPIN:66;
then 2|^(2*z)+1 > 1+1 by A9,XREAL_1:8;
then (2|^(2*z)+1)|^2 > 2|^2 by PREPOWER:10;
hence b > a by A8,Lm1,XREAL_1:8;
b is composite by Th78;
hence thesis;
end;
end;
hence thesis by A1,A2,NUMBER04:1;
end;