:: Elementary Number Theory Problems. {P}art {II}
:: by Artur Korni{\l}owicz and Dariusz Surowik
::
:: Received March 30, 2021
:: Copyright (c) 2021-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, FINSEQ_1, RELAT_1, FUNCT_1, XXREAL_0, XBOOLE_0,
SUBSET_1, ARYTM_3, TARSKI, XCMPLX_0, CARD_3, CARD_1, ARYTM_1, INT_2,
INT_1, FINSET_1, SQUARE_1, NEWTON, FINSEQ_3, ABIAN, PBOOLE, NAT_LAT,
NUMBER02;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, MEMBERED, VALUED_0,
FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCOP_1, INT_1, INT_2, NAT_1,
NAT_D, VALUED_1, PBOOLE, ABIAN, NAT_LAT, RVSUM_1, SQUARE_1, XXREAL_0,
NEWTON, WSIERP_1, NEWTON02;
constructors PARTFUN1, WELLORD2, REAL_1, SQUARE_1, NAT_1, NAT_D, BINOP_2,
FINSOP_1, RVSUM_1, FUNCOP_1, RELSET_1, FINSEQOP, NEWTON, WSIERP_1,
RECDEF_1, NEWTON02, ABIAN, NAT_LAT;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, VALUED_0,
CARD_1, SQUARE_1, PEPIN, NEWTON, NEWTON02, NEWTON03, FOMODEL0, NAT_2,
ABIAN, NAT_6, RAT_1, NUMPOLY1, NEWTON01, INT_2, JORDAN1D, NAT_LAT;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, INT_1, NAT_D;
equalities SQUARE_1, NEWTON02;
expansions INT_1, INT_2, NAT_D, ABIAN;
theorems NEWTON, INT_4, WSIERP_1, FINSEQ_3, NAT_1, XXREAL_0, XREAL_1, INT_1,
INT_2, NEWTON02, NAT_D, PEPIN, XCMPLX_1, NAT_6, TARSKI, EULER_2,
POLYEQ_5, INT_6, NAT_5, NAT_4, NUMERAL2, NEWTON05, PREPOWER, PYTHTRIP,
FUNCT_1, PARTFUN1, NAT_LAT;
schemes NAT_1, PBOOLE;
begin :: Preliminaries
reserve a,b,i,k,m,n for Nat;
reserve s,z for non zero Nat;
reserve c for Complex;
theorem Th1:
c|^5 = c*c*c*c*c
proof
A1: 5 = 4+1;
c|^4 = c*c*c*c by POLYEQ_5:3;
hence thesis by A1,NEWTON:6;
end;
theorem Th2:
c|^6 = c*c*c*c*c*c
proof
A1: 6 = 5+1;
c|^5 = c*c*c*c*c by Th1;
hence thesis by A1,NEWTON:6;
end;
theorem Th3:
c|^7 = c*c*c*c*c*c*c
proof
A1: 7 = 6+1;
c|^6 = c*c*c*c*c*c by Th2;
hence thesis by A1,NEWTON:6;
end;
theorem Th4:
c|^8 = c*c*c*c*c*c*c*c
proof
A1: 8 = 7+1;
c|^7 = c*c*c*c*c*c*c by Th3;
hence thesis by A1,NEWTON:6;
end;
theorem Th5:
c|^9 = c*c*c*c*c*c*c*c*c
proof
A1: 9 = 8+1;
c|^8 = c*c*c*c*c*c*c*c by Th4;
hence thesis by A1,NEWTON:6;
end;
theorem Th6:
c|^10 = c*c*c*c*c*c*c*c*c*c
proof
A1: 10 = 9+1;
c|^9 = c*c*c*c*c*c*c*c*c by Th5;
hence thesis by A1,NEWTON:6;
end;
theorem Th7:
a = n-1 & k < n implies k = 0 or ... or k = a
proof
assume a = n-1 & k < n;
then k <= a by INT_1:52;
hence thesis;
end;
theorem Th8:
-1 div 3 = -1
proof
(-1) / 3 - 1 < -1;
then [\ (-1) / 3 /] = -1 by INT_1:def 6;
hence thesis by INT_1:def 9;
end;
theorem Th9:
-1 mod 3 = 2
proof
-1 - ((-1) div 3) * 3 = 2 by Th8;
hence thesis by INT_1:def 10;
end;
theorem Th10:
not 30 is prime
proof
30 = 2*15;
then 2 divides 30;
hence thesis;
end;
begin :: Divisibility of natural numbers
Lm1:
not 12 is prime & not 14 is prime &
not 15 is prime & not 16 is prime by NAT_4:57;
Lm2:
not 18 is prime & not 20 is prime & not 21 is prime by NAT_4:57,58;
theorem Th11:
n < 31 & n is prime implies
n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or
n = 23 or n = 29
proof
assume that
A1: n < 31 and
A2: n is prime;
A3: 1+1 < n+1 & n < 30+1 by A2,A1,XREAL_1:6;
per cases by A3,NAT_1:13;
suppose
2 <= n & n < 5;
hence thesis by A2,NAT_4:59;
end;
suppose
A4: 5 <= n & n <= 29+1;
per cases by A4;
suppose
5 <= n & n <= 9+1;
then
5<=n & n<=5+1 or 6<=n & n<=6+1 or 7<=n & n<=7+1 or 8<=n & n<=8+1 or
9<=n & n<=9+1;
hence thesis by A2,NAT_4:57,NAT_1:9;
end;
suppose
10 <= n & n <= 15+1;
then
10<=n & n<=10+1 or 11<=n & n<=11+1 or 12<=n & n<=12+1 or
13<=n & n<=13+1 or 14<=n & n<=14+1 or 15<=n & n<=15+1;
hence thesis by A2,NAT_4:57,NAT_1:9;
end;
suppose
16 <= n & n <= 20+1;
then
16<=n & n<=16+1 or 17<=n & n<=17+1 or 18<=n & n<=18+1 or
19<=n & n<=19+1 or 20<=n & n<=20+1;
hence thesis by A2,Lm1,Lm2,NAT_1:9;
end;
suppose
21 <= n & n <= 27+1;
then
21<=n & n<=21+1 or 22<=n & n<=22+1 or 23<=n & n<=23+1 or
24<=n & n<=24+1 or 25<=n & n<=25+1 or 26<=n & n<=26+1 or
27<=n & n<=27+1;
hence thesis by A2,NAT_4:58,NAT_1:9;
end;
suppose
28 <= n & n <= 29+1;
then 28<=n & n<=28+1 or 29<=n & n<=29+1;
hence thesis by A2,NAT_4:58,Th10,NAT_1:9;
end;
end;
end;
theorem Th12:
k < 961 & n*n <= k & n is prime implies
n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or
n = 23 or n = 29
proof
assume
A1: k < 961;
assume that
A2: n*n <= k and
A3: n is prime;
n*n < 31*31 by A1,A2,XXREAL_0:2;
hence thesis by A3,Th11,NAT_4:1;
end;
theorem Th13:
113 is prime
proof
for n being Element of NAT holds 1 < n & n*n <= 113 & n is prime implies
not n divides 113
proof
let n be Element of NAT;
113 = 2*56 + 1;
then
A1: not 2 divides 113;
113 = 3*37 + 2;
then
A2: not 3 divides 113 by NAT_4:9;
113 = 5*22 + 3;
then
A3: not 5 divides 113 by NAT_4:9;
113 = 7*16 + 1;
then
A4: not 7 divides 113 by NAT_4:9;
113 = 11*10 + 3;
then
A5: not 11 divides 113 by NAT_4:9;
113 = 13*8 + 9;
then
A6: not 13 divides 113 by NAT_4:9;
113 = 17*6 + 11;
then
A7: not 17 divides 113 by NAT_4:9;
113 = 19*5 + 18;
then
A8: not 19 divides 113 by NAT_4:9;
113 = 23*4 + 21;
then
not 23 divides 113 by NAT_4:9;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th14:
337 is prime
proof
for n being Element of NAT holds 1 < n & n*n <= 337 & n is prime implies
not n divides 337
proof
let n be Element of NAT;
337 = 2*168 + 1;
then
A1: not 2 divides 337;
337 = 3*112 + 1;
then
A2: not 3 divides 337 by NAT_4:9;
337 = 5*67 + 2;
then
A3: not 5 divides 337 by NAT_4:9;
337 = 7*48 + 1;
then
A4: not 7 divides 337 by NAT_4:9;
337 = 11*30 + 7;
then
A5: not 11 divides 337 by NAT_4:9;
337 = 13*25 + 12;
then
A6: not 13 divides 337 by NAT_4:9;
337 = 17*19 + 14;
then
A7: not 17 divides 337 by NAT_4:9;
337 = 19*17 + 14;
then
A8: not 19 divides 337 by NAT_4:9;
337 = 23*14 + 15;
then
not 23 divides 337 by NAT_4:9;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,NAT_4:62;
end;
hence thesis by NAT_4:14;
end;
theorem Th15:
881 is prime
proof
for n being Element of NAT holds 1 < n & n*n <= 881 & n is prime implies
not n divides 881
proof
let n be Element of NAT;
881 = 2*440 + 1;
then
A1: not 2 divides 881;
881 = 3*293 + 2;
then
A2: not 3 divides 881 by NAT_4:9;
881 = 5*176 + 1;
then
A3: not 5 divides 881 by NAT_4:9;
881 = 7*125 + 6;
then
A4: not 7 divides 881 by NAT_4:9;
881 = 11*80 + 1;
then
A5: not 11 divides 881 by NAT_4:9;
881 = 13*67 + 10;
then
A6: not 13 divides 881 by NAT_4:9;
881 = 17*51 + 14;
then
A7: not 17 divides 881 by NAT_4:9;
881 = 19*46 + 7;
then
A8: not 19 divides 881 by NAT_4:9;
881 = 23*38 + 7;
then
A9: not 23 divides 881 by NAT_4:9;
881 = 29*30 + 11;
then
not 29 divides 881 by NAT_4:9;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,Th12;
end;
hence thesis by NAT_4:14;
end;
theorem Th16:
k < a implies (a*b+k) mod a = k
proof
assume k < a;
hence k = k mod a by NAT_D:24
.= (a*b+k) mod a by NAT_D:21;
end;
theorem
a divides a|^s + a|^z
proof
a|^(s-1+1) = a|^(s-1)*a & a|^(z-1+1) = a|^(z-1)*a by NEWTON:6;
then a|^s+a|^z = a*(a|^(s-1)+a|^(z-1));
hence thesis;
end;
theorem Th18:
a divides a|^s - a|^z
proof
a|^(s-1+1) = a|^(s-1)*a & a|^(z-1+1) = a|^(z-1)*a by NEWTON:6;
then a|^s-a|^z = a*(a|^(s-1)-a|^(z-1));
hence thesis;
end;
theorem
a divides a|^s * a|^z
proof
a|^(s-1+1) = a|^(s-1)*a & a|^(z-1+1) = a|^(z-1)*a by NEWTON:6;
then a|^s*a|^z = a*(a*(a|^(s-1)*a|^(z-1)));
hence thesis;
end;
registration
let p,q be prime Nat;
cluster p*q -> non prime;
coherence
proof
ex n being Nat st n divides p*q & n <> 1 & n <> p*q
proof
take p;
thus p divides p*q;
thus p <> 1 by INT_2:def 4;
assume p = p*q;
then p*q = p*1;
then q = 1 by XCMPLX_1:5;
hence thesis by INT_2:def 4;
end;
hence thesis;
end;
end;
theorem Th20:
11 divides 2|^341-2
proof
A1: (2|^10)|^34 = 2|^(10*34) by NEWTON:9;
A2: 1 mod 11 = 1 by NAT_D:24;
2|^10 = 2*2*2*2*2*2*2*2*2*2 by Th6
.= 11*93+1;
then 2|^10 mod 11 = 1 by NAT_D:def 2;
then (2|^10)|^34 mod 11 = 1 by NEWTON05:15;
then
A3: 2|^340,1 are_congruent_mod 11 by A1,A2,NAT_D:64;
2|^(340+1)-2 = (2|^340*2|^1)-(2*1) by NEWTON:8
.= 2*(2|^340-1);
hence thesis by A3,INT_2:2;
end;
theorem Th21:
31 divides 2|^341-2
proof
A1: (2|^5)|^68 = 2|^(5*68) by NEWTON:9;
A2: 1 mod 31 = 1 by NAT_D:24;
2|^5 = 2*2*2*2*2 by Th1
.= 31*1+1;
then 2|^5 mod 31 = 1 by NAT_D:def 2;
then (2|^5)|^68 mod 31 = 1 by NEWTON05:15;
then
A3: 2|^340,1 are_congruent_mod 31 by A1,A2,NAT_D:64;
2|^(340+1)-2 = (2|^340*2|^1)-(2*1) by NEWTON:8
.= 2*(2|^340-1);
hence thesis by A3,INT_2:2;
end;
theorem Th22:
ex k st n = z*k+(0 qua Nat) or ... or n = z*k+(z-1)
proof
per cases;
suppose
A1: z-1 <= n;
n,0 are_congruent_mod z or ... or n,z-1 are_congruent_mod z by NAT_6:13;
then consider i being Nat such that
0 <= i and
A2: i <= z-1 and
A3: n,i are_congruent_mod z;
consider k being Integer such that
A4: z*k = n-i by A3;
n-(z-1) >= n-n by A1,XREAL_1:10;
then z*k >= 0 by A2,A4,XREAL_1:10;
then k is non negative;
then reconsider k as Nat by TARSKI:1;
take k;
thus n = z*k+(0 qua Nat) or ... or n = z*k+(z-1)
proof
take i;
thus thesis by A2,A4;
end;
end;
suppose
A5: n < z-1;
take k = 0;
thus n = z*k+(0 qua Nat) or ... or n = z*k+(z-1)
proof
take n;
thus thesis by A5;
end;
end;
end;
theorem Th23:
ex k st n = 3*k or n = 3*k+1 or n = 3*k+2
proof
consider k such that
A1: n = 3*k+(0 qua Nat) or ... or n = 3*k+(3-1) by Th22;
consider i such that
A2: 0 <= i & i <= 2 and
A3: n = 3*k+i by A1;
take k;
i = 0 or ... or i = 2 by A2;
hence thesis by A3;
end;
theorem Th24:
ex k st n = 4*k or n = 4*k+1 or n = 4*k+2 or n = 4*k+3
proof
consider k such that
A1: n = 4*k+(0 qua Nat) or ... or n = 4*k+(4-1) by Th22;
consider i such that
A2: 0 <= i & i <= 3 and
A3: n = 4*k+i by A1;
take k;
i = 0 or ... or i = 3 by A2;
hence thesis by A3;
end;
theorem Th25:
ex k st n = 5*k or n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4
proof
consider k such that
A1: n = 5*k+(0 qua Nat) or ... or n = 5*k+(5-1) by Th22;
consider i such that
A2: 0 <= i & i <= 4 and
A3: n = 5*k+i by A1;
take k;
i = 0 or ... or i = 4 by A2;
hence thesis by A3;
end;
theorem Th26:
ex k st 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
proof
consider k such that
A1: n = 6*k+(0 qua Nat) or ... or n = 6*k+(6-1) by Th22;
consider i such that
A2: 0 <= i & i <= 5 and
A3: n = 6*k+i by A1;
take k;
i = 0 or ... or i = 5 by A2;
hence thesis by A3;
end;
theorem Th27:
ex k st n = 7*k or n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or
n = 7*k+4 or n = 7*k+5 or n = 7*k+6
proof
consider k such that
A1: n = 7*k+(0 qua Nat) or ... or n = 7*k+(7-1) by Th22;
consider i such that
A2: 0 <= i & i <= 6 and
A3: n = 7*k+i by A1;
take k;
i = 0 or ... or i = 6 by A2;
hence thesis by A3;
end;
theorem Th28:
ex k st n = 8*k or n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or
n = 8*k+4 or n = 8*k+5 or n = 8*k+6 or n = 8*k+7
proof
consider k such that
A1: n = 8*k+(0 qua Nat) or ... or n = 8*k+(8-1) by Th22;
consider i such that
A2: 0 <= i & i <= 7 and
A3: n = 8*k+i by A1;
take k;
i = 0 or ... or i = 7 by A2;
hence thesis by A3;
end;
theorem Th29:
ex k st n = 9*k or n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or
n = 9*k+4 or n = 9*k+5 or n = 9*k+6 or n = 9*k+7 or n = 9*k+8
proof
consider k such that
A1: n = 9*k+(0 qua Nat) or ... or n = 9*k+(9-1) by Th22;
consider i such that
A2: 0 <= i & i <= 8 and
A3: n = 9*k+i by A1;
take k;
i = 0 or ... or i = 8 by A2;
hence thesis by A3;
end;
theorem Th30:
ex k st n = 10*k or n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or
n = 10*k+4 or n = 10*k+5 or n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or
n = 10*k+9
proof
consider k such that
A1: n = 10*k+(0 qua Nat) or ... or n = 10*k+(10-1) by Th22;
consider i such that
A2: 0 <= i & i <= 9 and
A3: n = 10*k+i by A1;
take k;
i = 0 or ... or i = 9 by A2;
hence thesis by A3;
end;
theorem
not 3 divides n iff ex k st n = 3*k+1 or n = 3*k+2
proof
consider K being Nat such that
A1: n = 3*K or n = 3*K+1 or n = 3*K+2 by Th23;
thus not 3 divides n implies ex k st n = 3*k+1 or n = 3*k+2 by A1;
given k such that
A2: n = 3*k+1 or n = 3*k+2;
given t being Nat such that
A3: n = 3*t;
per cases by A2;
suppose n = 3*k+1;
then 1/3 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 3*k+2;
then 2/3 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem Th32:
not 4 divides n iff ex k st n = 4*k+1 or n = 4*k+2 or n = 4*k+3
proof
consider K being Nat such that
A1: n = 4*K or n = 4*K+1 or n = 4*K+2 or n = 4*K+3 by Th24;
thus not 4 divides n implies ex k st n = 4*k+1 or n = 4*k+2 or n = 4*k+3
by A1;
given k such that
A2: n = 4*k+1 or n = 4*k+2 or n = 4*k+3;
given t being Nat such that
A3: n = 4*t;
per cases by A2;
suppose n = 4*k+1;
then 1/4 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 4*k+2;
then 2/4 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 4*k+3;
then 3/4 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem
not 5 divides n
iff
ex k st n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4
proof
consider K being Nat such that
A1: n = 5*K or n = 5*K+1 or n = 5*K+2 or n = 5*K+3 or n = 5*K+4 by Th25;
thus not 5 divides n implies
ex k st n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4 by A1;
given k such that
A2: n = 5*k+1 or n = 5*k+2 or n = 5*k+3 or n = 5*k+4;
given t being Nat such that
A3: n = 5*t;
per cases by A2;
suppose n = 5*k+1;
then 1/5 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 5*k+2;
then 2/5 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 5*k+3;
then 3/5 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 5*k+4;
then 4/5 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem Th34:
not 6 divides n
iff
ex k st n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or n = 6*k+4 or n = 6*k+5
proof
consider K being Nat such that
A1: 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 Th26;
thus not 6 divides n implies
ex k st 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 A1;
given k such that
A2: n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or n = 6*k+4 or n = 6*k+5;
given t being Nat such that
A3: n = 6*t;
per cases by A2;
suppose n = 6*k+1;
then 1/6 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 6*k+2;
then 2/6 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 6*k+3;
then 3/6 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 6*k+4;
then 4/6 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 6*k+5;
then 5/6 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem Th35:
not 7 divides n
iff
ex k st n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or n = 7*k+4 or n = 7*k+5 or
n = 7*k+6
proof
consider K being Nat such that
A1: n = 7*K or n = 7*K+1 or n = 7*K+2 or n = 7*K+3 or n = 7*K+4 or n = 7*K+5 or
n = 7*K+6 by Th27;
thus not 7 divides n implies
ex k st n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or n = 7*k+4 or n = 7*k+5 or
n = 7*k+6 by A1;
given k such that
A2: n = 7*k+1 or n = 7*k+2 or n = 7*k+3 or n = 7*k+4 or n = 7*k+5 or n = 7*k+6;
given t being Nat such that
A3: n = 7*t;
per cases by A2;
suppose n = 7*k+1;
then 1/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 7*k+2;
then 2/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 7*k+3;
then 3/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 7*k+4;
then 4/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 7*k+5;
then 5/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 7*k+6;
then 6/7 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem
not 8 divides n
iff
ex k st n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or n = 8*k+4 or n = 8*k+5 or
n = 8*k+6 or n = 8*k+7
proof
consider K being Nat such that
A1: n = 8*K or n = 8*K+1 or n = 8*K+2 or n = 8*K+3 or n = 8*K+4 or n = 8*K+5 or
n = 8*K+6 or n = 8*K+7 by Th28;
thus not 8 divides n implies
ex k st n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or n = 8*k+4 or n = 8*k+5 or
n = 8*k+6 or n = 8*k+7 by A1;
given k such that
A2: n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or n = 8*k+4 or n = 8*k+5 or n = 8*k+6
or n = 8*k+7;
given t being Nat such that
A3: n = 8*t;
per cases by A2;
suppose n = 8*k+1;
then 1/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+2;
then 2/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+3;
then 3/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+4;
then 4/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+5;
then 5/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+6;
then 6/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 8*k+7;
then 7/8 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem
not 9 divides n
iff
ex k st n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or n = 9*k+4 or n = 9*k+5 or
n = 9*k+6 or n = 9*k+7 or n = 9*k+8
proof
consider K being Nat such that
A1: n = 9*K or n = 9*K+1 or n = 9*K+2 or n = 9*K+3 or n = 9*K+4 or n = 9*K+5 or
n = 9*K+6 or n = 9*K+7 or n = 9*K+8 by Th29;
thus not 9 divides n implies
ex k st n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or n = 9*k+4 or n = 9*k+5 or
n = 9*k+6 or n = 9*k+7 or n = 9*k+8 by A1;
given k such that
A2: n = 9*k+1 or n = 9*k+2 or n = 9*k+3 or n = 9*k+4 or n = 9*k+5 or n = 9*k+6
or n = 9*k+7 or n = 9*k+8;
given t being Nat such that
A3: n = 9*t;
per cases by A2;
suppose n = 9*k+1;
then 1/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+2;
then 2/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+3;
then 3/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+4;
then 4/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+5;
then 5/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+6;
then 6/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+7;
then 7/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 9*k+8;
then 8/9 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem
not 10 divides n
iff
ex k st n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or n = 10*k+4 or n = 10*k+5 or
n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or n = 10*k+9
proof
consider K being Nat such that
A1: n = 10*K or n = 10*K+1 or n = 10*K+2 or n = 10*K+3 or n = 10*K+4 or
n = 10*K+5 or n = 10*K+6 or n = 10*K+7 or n = 10*K+8 or n = 10*K+9
by Th30;
thus not 10 divides n implies
ex k st n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or n = 10*k+4 or
n = 10*k+5 or n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or n = 10*k+9 by A1;
given k such that
A2: n = 10*k+1 or n = 10*k+2 or n = 10*k+3 or n = 10*k+4 or n = 10*k+5 or
n = 10*k+6 or n = 10*k+7 or n = 10*k+8 or n = 10*k+9;
given t being Nat such that
A3: n = 10*t;
per cases by A2;
suppose n = 10*k+1;
then 1/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+2;
then 2/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+3;
then 3/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+4;
then 4/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+5;
then 5/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+6;
then 6/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+7;
then 7/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+8;
then 8/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
suppose n = 10*k+9;
then 9/10 = t-k by A3;
hence thesis by NAT_D:33;
end;
end;
theorem Th39:
2|^(2|^z) mod 3 = 1
proof
defpred P[non zero Nat] means 2|^(2|^$1) mod 3 = 1;
A1: P[1]
proof
2|^(2|^1) = 2*2 by POLYEQ_5:1
.= 3*1+1;
hence thesis by NAT_D:def 2;
end;
A2: for s st P[s] holds P[s+1]
proof
let s such that
A3: P[s];
2|^(s+1) = 2|^s*2 by NEWTON:6;
then
A4: 2|^(2|^(s+1)) = 2|^(2|^s)|^2 by NEWTON:9
.= 2|^(2|^s)*2|^(2|^s) by POLYEQ_5:1;
(2|^(2|^s)*2|^(2|^s)) mod 3 = (1*1) mod 3 by A3,NAT_D:67;
hence thesis by A4,NAT_D:24;
end;
for s holds P[s] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
definition
let n be Integer;
attr n is composite means :Def1:
2 <= n & n is non prime;
end;
registration
cluster composite for Integer;
existence
proof
take 4;
thus thesis by INT_2:29;
end;
cluster composite for Nat;
existence
proof
take 4;
thus thesis by INT_2:29;
end;
cluster composite -> positive for Integer;
coherence;
cluster prime -> non composite for Integer;
coherence;
cluster composite -> non prime for Integer;
coherence;
end;
registration
let m,n be composite Integer;
cluster m*n -> composite;
coherence
proof
A1: 2 <= m by Def1;
2 <= n by Def1;
then 2*2 <= m*n by A1,XREAL_1:66;
hence 2 <= m*n by XXREAL_0:2;
assume
A2: m*n is prime;
n divides m*n;
then n = 1 or 1*n = m*n by A2;
hence thesis by A2;
end;
end;
theorem
for n being Integer holds n is composite implies 4 <= n
proof
let n be Integer;
assume that
A1: 2 <= n and
A2: n is non prime;
reconsider m = n as Element of NAT by A1,INT_1:3;
assume
A3: n < 4;
then m = 2+0 or ... or m = 2+2 by A1,NAT_1:62;
hence thesis by A2,A3,INT_2:28,PEPIN:41;
end;
begin :: Main problems
theorem Th41:
1 <= i <= len ((a,b) In_Power n) - m implies
a|^m divides ((a,b) In_Power n).i
proof
set P = (a,b) In_Power n;
assume that
A1: 1 <= i and
A2: i <= len P - m;
reconsider M = i-1 as Element of NAT by A1,INT_1:5;
len P - m <= len P by XREAL_1:43;
then
A3: i <= len P by A2,XXREAL_0:2;
then
A4: i in dom P by A1,FINSEQ_3:25;
A5: len P = n+1 by NEWTON:def 4;
then i-1 <= n+1-1 by A3,XREAL_1:9;
then reconsider L = n-M as Element of NAT by INT_1:5;
P.i = (n choose M) * a|^L * b|^M by A4,NEWTON:def 4
.= a|^L * ((n choose M)*b|^M);
then
A6: a|^L divides P.i;
m <= n+1-i by A2,A5,XREAL_1:11;
then a|^m divides a|^L by NEWTON:89;
hence a|^m divides P.i by A6,INT_2:9;
end;
::Problem 14
theorem Th42:
n^2 divides (n+1)|^n - 1
proof
set P = (n,1) In_Power n;
A1: (n+1)|^n = Sum P by NEWTON:30;
set c = len P;
set F = Del(P,c);
A2: len P = n+1 by NEWTON:def 4;
then
A3: P.c = 1|^n by NEWTON:29;
1 <= c by A2,NAT_1:11;
then
A4: c in dom P by FINSEQ_3:25;
then
A5: Sum F + (P.c) = Sum(P) by WSIERP_1:20;
A6: len F + 1 = len P by A4,WSIERP_1:def 1;
for b being Nat st b in dom F holds n^2 divides F.b
proof
let b be Nat;
assume
A7: b in dom F;
then
A8: b <= len F by FINSEQ_3:25;
A9: 1 <= b by A7,FINSEQ_3:25;
A10: n < n+1 by XREAL_1:29;
then b < c by A2,A6,A8,XXREAL_0:2;
then
A11: F.b = P.b by FINSEQ_3:110;
per cases by A6,A8,XXREAL_0:1;
suppose b < c-1;
then b <= c-1-1 by INT_1:52;
then b <= c-2;
then n|^2 divides P.b by A9,Th41;
hence n^2 divides F.b by A11,WSIERP_1:1;
end;
suppose
A12: b = c-1;
reconsider M = b-1 as Element of NAT by A9,INT_1:5;
reconsider L = n-M as Element of NAT by A2,A12;
n in dom P by A2,A9,A10,A12,FINSEQ_3:25;
then P.b = (n choose M) * n|^L * 1|^M by A2,A12,NEWTON:def 4;
hence n^2 divides F.b by A2,A9,A11,A12,NEWTON:24;
end;
end;
hence n^2 divides (n+1)|^n - 1 by A1,A3,A5,INT_4:36;
end;
:: Problem 15
theorem
(2|^n-1)^2 divides 2|^((2|^n-1)*n) - 1
proof
set m = 2|^n-1;
(m+1)|^m = 2|^(m*n) by NEWTON:9;
hence thesis by Th42;
end;
:: Problem 29
theorem
not 6 divides 2|^6-2 & 6 divides 3|^6-3 &
not ex n being Nat st n < 6 & not n divides 2|^n-2 & n divides 3|^n-3
proof
2|^6-2 = 2*2*2*2*2*2-2 by Th2
.= 6*10+2;
hence not 6 divides 2|^6-2 by Th34;
3|^6-3 = 3*3*3*3*3*3-3 by Th2
.= 6*121;
hence 6 divides 3|^6-3;
let n be Nat such that
A1: n < 6 and
A2: not n divides 2|^n-2;
n = 0 or ... or n = 6-1 by A1,Th7;
then
A3: n = 0 or ... or n = 5;
per cases by A2,A3,INT_2:28,PEPIN:41,59,INT_2:12,NEWTON02:138;
suppose n = 0;
hence not n divides 3|^n-3 by NEWTON:4;
end;
suppose
A4: n = 4;
3|^4-3 = 3*3*3*3-3 by POLYEQ_5:3
.= 4*19+2;
hence not n divides 3|^n-3 by A4,Th32;
end;
end;
:: Problem 30
theorem
for a being non zero Nat
ex n being non prime Nat st n divides a|^n-a
proof
let a be non zero Nat;
per cases;
suppose a is non prime;
then reconsider n = a as non prime non zero Nat;
take n;
a divides a|^n-a|^1 by Th18;
hence thesis;
end;
suppose that
A1: a is prime and
A2: a > 2;
reconsider a as odd Nat by A1,A2,PEPIN:17;
2*a > 1*a by XREAL_1:68;
then 2*a > 2*1 by A2,XXREAL_0:2;
then reconsider n = 2*a as non prime Nat by PEPIN:17;
take n;
A3: 2 = 2|^1;
A4: a|^n-a is even;
a divides a|^n-a|^1 by Th18;
hence thesis by A3,A4,PEPIN:4,NAT_5:3;
end;
suppose that
A5: a is prime and
A6: a <= 2;
a >= 1+1 by A5,NAT_1:13;
then
A7: a = 2 by A6,XXREAL_0:1;
A8: 341 = 11*31;
then reconsider n = 341 as non prime Nat by NAT_4:27,NUMERAL2:24;
take n;
thus thesis by A7,A8,Th20,Th21,PEPIN:4,INT_2:30,NAT_4:27,NUMERAL2:24;
end;
end;
theorem Th46:
not 7 divides a implies
ex k st a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4
proof
assume not 7 divides a;
then consider k such that
A1: a = 7*k+1 or a = 7*k+2 or a = 7*k+3 or a = 7*k+4 or a = 7*k+5 or
a = 7*k+6 by Th35;
a^2 = 7*(k*(7*k+2))+1 or
a^2 = 7*(k*(7*k+4))+4 or
a^2 = 7*(k*(7*k+6)+1)+2 or
a^2 = 7*(k*(7*k+8)+2)+2 or
a^2 = 7*(k*(7*k+10)+3)+4 or
a^2 = 7*(k*(7*k+12)+5)+1 by A1;
hence thesis;
end;
theorem
ex k st a^2 = 7*k or a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4
proof
per cases;
suppose not 7 divides a;
hence thesis by Th46;
end;
suppose 7 divides a;
then 7 divides a^2 by INT_2:2;
hence thesis;
end;
end;
theorem Th48:
not 7 divides a implies a^2 mod 7 = 1 or a^2 mod 7 = 2 or a^2 mod 7 = 4
proof
assume not 7 divides a;
then ex k st a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4 by Th46;
hence thesis by Th16;
end;
theorem Th49:
a^2 mod 7 = 0 or a^2 mod 7 = 1 or a^2 mod 7 = 2 or a^2 mod 7 = 4
proof
per cases;
suppose not 7 divides a;
then ex k st a^2 = 7*k+1 or a^2 = 7*k+2 or a^2 = 7*k+4 by Th46;
hence thesis by Th16;
end;
suppose 7 divides a;
then 7 divides a^2 by INT_2:2;
hence thesis;
end;
end;
theorem
(ex k st a = 7*k+1 or a = 7*k+2 or a = 7*k+4) &
(ex k st b = 7*k+1 or b = 7*k+2 or b = 7*k+4) implies
ex k st a+b = 7*k+1 or ... or a+b = 7*k+6
proof
given k1 being Nat such that
A1: a = 7*k1+1 or a = 7*k1+2 or a = 7*k1+4;
given k2 being Nat such that
A2: b = 7*k2+1 or b = 7*k2+2 or b = 7*k2+4;
per cases by A1,A2;
suppose
A3: a = 7*k1+1 & b = 7*k2+1;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A3;
end;
hence thesis;
end;
suppose
A4: a = 7*k1+1 & b = 7*k2+2;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A4;
end;
hence thesis;
end;
suppose
A5: a = 7*k1+1 & b = 7*k2+4;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A5;
end;
hence thesis;
end;
suppose
A6: a = 7*k1+2 & b = 7*k2+1;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A6;
end;
hence thesis;
end;
suppose
A7: a = 7*k1+2 & b = 7*k2+2;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A7;
end;
hence thesis;
end;
suppose
A8: a = 7*k1+2 & b = 7*k2+4;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A8;
end;
hence thesis;
end;
suppose
A9: a = 7*k1+4 & b = 7*k2+1;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A9;
end;
hence thesis;
end;
suppose
A10: a = 7*k1+4 & b = 7*k2+2;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2;
thus thesis by A10;
end;
hence thesis;
end;
suppose
A11: a = 7*k1+4 & b = 7*k2+4;
ex k st a+b = 7*k+(1 qua Nat) or ... or a+b = 7*k+(6 qua Nat)
proof
take k1+k2+1;
thus thesis by A11;
end;
hence thesis;
end;
end;
theorem
(a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4) &
(b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4) implies
a+b mod 7 = 1 or ... or a+b mod 7 = 6
proof
A1: (a+b) mod 7 = ((a mod 7)+(b mod 7)) mod 7 by NAT_D:66;
assume (a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4) &
(b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4);
then per cases;
suppose
a mod 7 = 1 & b mod 7 = 1 or
a mod 7 = 1 & b mod 7 = 2 or
a mod 7 = 1 & b mod 7 = 4 or
a mod 7 = 2 & b mod 7 = 1 or
a mod 7 = 2 & b mod 7 = 2 or
a mod 7 = 2 & b mod 7 = 4 or
a mod 7 = 4 & b mod 7 = 1 or
a mod 7 = 4 & b mod 7 = 2;
hence thesis by A1,NAT_D:24;
end;
suppose
A2: a mod 7 = 4 & b mod 7 = 4;
thus a+b mod 7 = 1 or ... or a+b mod 7 = 6
proof
take 1;
(a+b) mod 7 = 7*1+1 mod 7 by A1,A2;
hence thesis by Th16;
end;
end;
end;
:: Problem 34
theorem
7 divides a^2+b^2 implies 7 divides a & 7 divides b
proof
assume
A1: 7 divides a^2+b^2;
A2: a^2-a^2 = 0;
A3: b^2-b^2 = 0;
A4: 1 mod 7 = 1 by NAT_D:24;
A5: 2 mod 7 = 2 by NAT_D:24;
A6: 4 mod 7 = 4 by NAT_D:24;
A7: 0,7 are_congruent_mod 7 by INT_1:12;
A8: a^2,-b^2 are_congruent_mod 7 by A1;
A9: b^2,-a^2 are_congruent_mod 7 by A1;
assume not thesis;
then per cases;
suppose not 7 divides a;
then a^2 mod 7 = 1 or a^2 mod 7 = 2 or a^2 mod 7 = 4 by Th48;
then
a^2,1 are_congruent_mod 7 or
a^2,2 are_congruent_mod 7 or
a^2,4 are_congruent_mod 7 by A4,A5,A6,NAT_D:64;
then
0,-b^2-1 are_congruent_mod 7 or
0,-b^2-2 are_congruent_mod 7 or
0,-b^2-4 are_congruent_mod 7 by A2,A8,INT_1:17;
then
(-1)*(-b^2),(-1)*1 are_congruent_mod 7 or
(-1)*(-b^2),(-1)*2 are_congruent_mod 7 or
(-1)*(-b^2),(-1)*4 are_congruent_mod 7;
then
b^2+0,-1+7 are_congruent_mod 7 or
b^2+0,-2+7 are_congruent_mod 7 or
b^2+0,-4+7 are_congruent_mod 7 by A7,INT_1:16;
then b^2 mod 7 = 6 or b^2 mod 7 = 5 or b^2 mod 7 = 3 by NAT_6:12;
hence thesis by Th49;
end;
suppose not 7 divides b;
then b^2 mod 7 = 1 or b^2 mod 7 = 2 or b^2 mod 7 = 4 by Th48;
then
b^2,1 are_congruent_mod 7 or
b^2,2 are_congruent_mod 7 or
b^2,4 are_congruent_mod 7 by A4,A5,A6,NAT_D:64;
then
0,-a^2-1 are_congruent_mod 7 or
0,-a^2-2 are_congruent_mod 7 or
0,-a^2-4 are_congruent_mod 7 by A3,A9,INT_1:17;
then
(-1)*(-a^2),(-1)*1 are_congruent_mod 7 or
(-1)*(-a^2),(-1)*2 are_congruent_mod 7 or
(-1)*(-a^2),(-1)*4 are_congruent_mod 7;
then
a^2+0,-1+7 are_congruent_mod 7 or
a^2+0,-2+7 are_congruent_mod 7 or
a^2+0,-4+7 are_congruent_mod 7 by A7,INT_1:16;
then a^2 mod 7 = 6 or a^2 mod 7 = 5 or a^2 mod 7 = 3 by NAT_6:12;
hence thesis by Th49;
end;
end;
:: Problem 78
theorem
13^2+1 = 7^2 + 11^2 & 17^2+1 = 11^2 + 13^2 &
23^2+1 = 13^2 + 19^2 & 31^2+1 = 11^2 + 29^2;
:: Problem 83
theorem
2 = 1|^4+1|^4 & 17 = 1|^4+2|^4 & 97 = 2|^4+3|^4 &
257 = 1|^4+4|^4 & 641 = 2|^4+5|^4
proof
A1: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
A2: 3|^4 = 3*3*3*3 by POLYEQ_5:3;
A3: 4|^4 = 4*4*4*4 by POLYEQ_5:3;
A4: 5|^4 = 5*5*5*5 by POLYEQ_5:3;
thus 2 = 1|^4+1|^4;
thus 17 = 1|^4+2|^4 by A1;
thus 97 = 2|^4+3|^4 by A1,A2;
thus 257 = 1|^4+4|^4 by A3;
thus 641 = 2|^4+5|^4 by A1,A4;
end;
Lm3: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
Lm4: 3|^4 = 3*3*3*3 by POLYEQ_5:3;
Lm5: 4|^4 = 4*4*4*4 by POLYEQ_5:3;
Lm6: 5|^4 = 5*5*5*5 by POLYEQ_5:3;
Lm7: 6|^4 = 6*6*6*6 by POLYEQ_5:3;
theorem
0|^4+(0+1)|^4 is non composite;
theorem Th56:
1|^4+(1+1)|^4 is non composite by Lm3,PEPIN:60;
theorem Th57:
2|^4+(2+1)|^4 is non composite by Lm3,Lm4,NUMERAL2:35;
theorem Th58:
3|^4+(3+1)|^4 is non composite by Lm4,Lm5,Th14;
theorem Th59:
4|^4+(4+1)|^4 is non composite by Lm5,Lm6,Th15;
:: Problem 97
theorem
5|^4+(5+1)|^4 is composite &
not ex n being Nat st n < 5 & n|^4+(n+1)|^4 is composite
proof
set x = 5|^4+(5+1)|^4;
thus 2 <= x by Lm6,Lm7;
x = 17 * 113 by Lm6,Lm7;
hence x is non prime by Th13,PEPIN:60;
given n being Nat such that
A1: n < 5 and
A2: n|^4+(n+1)|^4 is composite;
n <= 5-1 by A1,INT_1:52;
then n = 0 or ... or n = 4;
hence thesis by A2,Th56,Th57,Th58,Th59;
end;
theorem Th61:
1 <= a implies 2|^(2|^n) + (6*a-1) > 6
proof
assume 1 <= a;
then 6*1 <= 6*a by XREAL_1:64;
then
A1: 6*1-1 <= 6*a-1 by XREAL_1:9;
0+1 <= 2|^n by NAT_1:13;
then 2 <= 2|^(2|^n) by PREPOWER:12;
then 2+5 <= 2|^(2|^n) + (6*a-1) by A1,XREAL_1:7;
hence thesis by XXREAL_0:2;
end;
theorem Th62:
3 divides 2|^(2|^z) + (6*a-1)
proof
A1: 3*(2*a) mod 3 = 0;
A2: (6*a-1) mod 3 = ((6*a mod 3) - (1 mod 3)) mod 3 by INT_6:7
.= (0 - 1) mod 3 by A1,NAT_D:24
.= -1 mod 3
.= 2 by Th9;
( 2|^(2|^z) + (6*a-1) ) mod 3
= (2|^(2|^z) mod 3) + ((6*a-1) mod 3) mod 3 by NAT_D:66
.= (1+2) mod 3 by A2,Th39
.= 0 by NAT_D:25;
hence thesis by INT_1:62;
end;
theorem Th63:
1 <= a implies 2|^(2|^z) + (6*a-1) is non prime
proof
set p = 2|^(2|^z) + (6*a-1);
assume
A1: 1 <= a;
assume 2|^(2|^z) + (6*a-1) is prime;
then 3 = p by Th62;
hence thesis by A1,Th61;
end;
theorem Th64:
1 <= a implies 2|^(2|^z) + (6*a-1) is composite
proof
assume
A1: 1 <= a;
then 6 < 2|^(2|^z) + (6*a-1) by Th61;
hence 2 <= 2|^(2|^z) + (6*a-1) by XXREAL_0:2;
thus thesis by A1,Th63;
end;
:: Problem 116
theorem
for z being non zero Nat holds
{k where k is Nat: k is odd & 2|^(2|^z)+k is composite} is infinite
proof
let z;
set S = {k where k is Nat: k is odd & 2|^(2|^z)+k is composite};
deffunc F(Nat) = 6*$1-1;
consider f being ManySortedSet of NATPLUS such that
A1: for n being Element of NATPLUS holds f.n = F(n) from PBOOLE:sch 5;
set R = rng f;
A2: dom f = NATPLUS by PARTFUN1:def 2;
A3: R c= S
proof
let a be object;
assume a in R;
then consider t being object such that
A4: t in dom f and
A5: a = f.t by FUNCT_1:def 3;
reconsider t as Element of NATPLUS by A4,PARTFUN1:def 2;
A6: a = 6*t-1 by A1,A5;
A7: 2*(3*t)-1 is odd;
0+1 <= t by NAT_1:13;
then 2|^(2|^z)+(6*t-1) is composite by Th64;
hence a in S by A6,A7;
end;
for m being Nat ex n being Nat st n >= m & n in R
proof
let m be Nat;
1*m <= 6*m by XREAL_1:64;
then
A8: m+0 <= 6*m+5 by XREAL_1:7;
reconsider n = F(m+1) as Element of NAT by INT_1:3;
take n;
thus n >= m by A8;
A9: m+1 in NATPLUS by NAT_LAT:def 6;
then f.(m+1) = n by A1;
hence n in R by A2,A9,FUNCT_1:def 3;
end;
hence thesis by A3,PYTHTRIP:9;
end;