:: Elementary Number Theory Problems. {P}art {V}
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received September 30, 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, SUBSET_1, ORDINAL1, ORDINAL2, CARD_1, XBOOLE_0, ARYTM_1,
TARSKI, ARYTM_3, XXREAL_0, NAT_1, RELAT_1, INT_1, INT_2, SQUARE_1,
NEWTON, FINSET_1, PBOOLE, FUNCT_1, ABIAN, FINSEQ_1, CARD_3, ORDINAL5,
XCMPLX_0, ZFMISC_1, NUMBER05, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2,
NUMBERS, ENUMSET1, XCMPLX_0, NAT_1, XXREAL_0, INT_1, INT_2, NAT_D,
FINSEQ_1, MEMBERED, SQUARE_1, NEWTON, FINSET_1, PBOOLE, ABIAN, WSIERP_1,
ORDINAL5;
constructors NAT_D, RELSET_1, ABIAN, EULER_1, NAT_3, ORDINAL5, INT_5, PEPIN,
DOMAIN_1, WSIERP_1, POLYEQ_3;
registrations ORDINAL1, XXREAL_0, XREAL_0, NAT_1, CARD_1, INT_1, INT_2,
WSIERP_1, FOMODEL0, ABIAN, VALUED_0, FINSET_1, MEMBERED, NEWTON02,
ORDINAL5, NEWTON03, XCMPLX_0, NEWTON, NAT_6, PEPIN, RELAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions MEMBERED, TARSKI, FUNCT_1, INT_2, NAT_D;
equalities ORDINAL1, SQUARE_1;
expansions INT_1, INT_2, ABIAN;
theorems INT_1, INT_2, INT_5, XREAL_1, XXREAL_0, NEWTON03, TARSKI, NEWTON,
WSIERP_1, FUNCT_1, PARTFUN1, PYTHTRIP, NAT_1, NEWTON01, GR_CY_3,
POLYFORM, NAT_5, INT_6, EULER_2, NAT_4, EULER_1, PEPIN, XCMPLX_1,
SERIES_2, FINSEQ_1, ORDINAL1, NAT_3, ABIAN, CARD_1, ZFMISC_1, XBOOLE_1,
XBOOLE_0, NAT_D, ORDINAL5, SCHEME1, NAT_2, NUMBER02, HEYTING3, ENUMSET1,
POLYEQ_3, SERIES_4, NEWTON05, POLYEQ_5, INT_4, XTUPLE_0, NUMBER03,
XPRIMES0, XPRIMES1, SQUARE_1, LAGRA4SQ;
schemes PBOOLE, NAT_1, SUBSET_1;
begin :: Problem 12
theorem Th1:
for n,k being Nat st n|^|^k = 0 holds n = 0
proof
let n,k be Nat;
assume A1: n|^|^k = 0;
then k <> 0 by ORDINAL5:13;
then consider j being Nat such that
A2: k=j+1 by NAT_1:6;
n|^|^(j+1) = n|^|^(Segm (j+1))
.= n|^|^(succ Segm j) by NAT_1:38
.= exp(n,n|^|^j) by ORDINAL5:14
.= n|^(n|^|^j);
hence n=0 by A1,A2;
end;
registration
let x be odd Nat;
let i be Nat;
cluster x|^|^i -> odd;
coherence
proof
defpred P[Nat] means x|^|^$1 is odd;
A1: P[0] by ORDINAL5:13,POLYFORM:4;
A2:
now
let k be Nat;
assume P[k];
x|^|^(k+1) = x|^|^(Segm (k+1))
.= x|^|^(succ Segm k) by NAT_1:38
.= exp(x,x|^|^k) by ORDINAL5:14
.= x|^(x|^|^k);
hence P[k+1] by PEPIN:20;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence x|^|^i is odd;
end;
end;
registration
let x be non zero even Nat;
let i be non zero Nat;
cluster x|^|^i -> even;
coherence
proof
consider j being Nat such that
A1: i=j+1 by NAT_1:6;
A2: x|^|^(j+1) = x|^|^(Segm (j+1))
.= x|^|^(succ Segm j) by NAT_1:38
.= exp(x,x|^|^j) by ORDINAL5:14
.= x|^(x|^|^j);
per cases;
suppose x|^|^j > 0;
hence x|^|^i is even by A2,A1;
end;
suppose x|^|^j = 0;
hence thesis by Th1;
end;
end;
end;
:: Problem 12
theorem
for n being non zero Nat ex x being non zero Nat st
for i being Nat holds n divides x|^|^(i+1) + 1
proof
let n be non zero Nat;
A1: n divides 2*n & 2 divides 2*n;
set x=2*n-1;
reconsider x as non zero odd Nat;
take x;
let i be Nat;
A3: x|^|^((i)+1) = x|^|^(Segm((i)+1))
.= x|^|^(succ Segm(i)) by NAT_1:38
.= exp(x,x|^|^(i)) by ORDINAL5:14
.= x|^(x|^|^(i));
2*n divides x - -1; then
x|^(x|^|^(i)), (-1)|^(x|^|^(i)) are_congruent_mod 2*n
by GR_CY_3:34,INT_1:def 4;
then x|^|^(i+1),-1 are_congruent_mod 2*n by A3;
hence thesis by A1,INT_2:9;
end;
begin :: Problem 13
theorem Th3:
for i being Integer, n being Nat
st n = 4*i+3 ex p,q being Nat st p = 4*q+3 & p is prime & p divides n
proof
defpred P[Nat] means
(ex k being Nat st $1=4*k+3) implies
ex p,q being Nat st p=4*q+3 & p is prime & p divides $1;
let k be Integer, n be Nat such that
A1: n = 4*k+3;
now
assume k < 0;
then
B2: k+1 <= 0 by INT_1:7;
4*k+3-3 >= 0-3 by A1,XREAL_1:9;
then 4*k/4 >= (-3)/4 by XREAL_1:72;
then k+1 >= -3/4+1 by XREAL_1:7;
hence contradiction by B2,XXREAL_0:2;
end;
then reconsider k as Element of NAT by INT_1:3;
B1: n=4*k+3 by A1;
A2: for m being Nat st for l being Nat st l < m holds P[l] holds P[m]
proof
let m be Nat;
assume A3: for l being Nat st l < m holds P[l];
given k being Nat such that
A4: m=4*k+3;
m <> 0 & m <> 1 by A4,NAT_1:11;
then m is non trivial by NAT_2:28;
then consider l being prime Nat such that
A5: l divides m by NEWTON03:29;
reconsider l as Element of NAT by ORDINAL1:def 12;
consider t being Nat such that
A6: m = l*t by A5,NAT_D:def 3;
A7: t divides m by A6;
consider u being Element of NAT such that
A8: l=4*u or l=4*u+1 or l=4*u+2 or l=4*u+3 by SCHEME1:3;
per cases by A8;
suppose l=4*u;
then 4 divides l;
then 4 divides m by A5,NAT_D:4;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A4,NUMBER02:32;
end;
suppose A9: l=4*u+1;
reconsider t as Element of NAT by ORDINAL1:def 12;
consider v being Element of NAT such that
A10: t=4*v or t=4*v+1 or t=4*v+2 or t=4*v+3 by SCHEME1:3;
per cases by A10;
suppose t=4*v;
then 4 divides t;
then 4 divides m by A7,NAT_D:4;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A4,NUMBER02:32;
end;
suppose t=4*v+1;
then m=4*(4*u*v+u+v)+1 by A6,A9;
then A11: m mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24;
m mod 4 = 3 mod 4 by A4,NAT_D:21
.= 3 by NAT_D:24;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A11;
end;
suppose t=4*v+2;
then t=2*(2*v+1);
then A12: 2 divides t;
m=2*(2*k+1)+1 by A4;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A12,A7;
end;
suppose A13: t=4*v+3;
A14: t <= m by A6,NAT_D:def 3,INT_2:27;
now
assume t=m;
then l=1 by A6,A4,XCMPLX_1:7;
hence contradiction by INT_2:def 4;
end; then
t < m by A14,XXREAL_0:1;
then consider p,q being Nat such that
A15: p=4*q+3 & p is prime & p divides t by A13,A3;
take p,q;
thus p=4*q+3 & p is prime & p divides m by A15,A7,NAT_D:4;
end;
end;
suppose l=4*u+2;
then l=2*(2*u+1);
then A16: 2 divides l;
m=2*(2*k+1)+1 by A4;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A16,A5;
end;
suppose l=4*u+3;
hence ex p,q being Nat st
p=4*q+3 & p is prime & p divides m by A5;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 4(A2);
then consider p,q being Nat such that
A17: p=4*q+3 & p is prime & p divides n by B1;
take p,q;
thus thesis by A17;
end;
definition
defpred P[set] means ex k being Nat st $1=4*k+3 & 4*k+3 is prime;
func 4k+3_Primes -> Subset of NAT means :Def1:
for n being Nat holds n in it iff ex k being Nat st n=4*k+3 & n is prime;
existence
proof
consider s being Subset of NAT such that
A1: for x being set holds x in s iff x in NAT & P[x] from SUBSET_1:sch 1;
take s;
let n be Nat;
thus n in s implies ex k being Nat st n=4*k+3 & n is prime
proof
assume n in s;
then consider k being Nat such that
A2: n=4*k+3 & 4*k+3 is prime by A1;
thus thesis by A2;
end;
given k being Nat such that A3: n=4*k+3 & n is prime;
thus n in s by A3,A1;
end;
uniqueness
proof
let s1,s2 be Subset of NAT such that
A4: for n being Nat holds n in s1 iff
ex k being Nat st n=4*k+3 & n is prime
and
A5: for n being Nat holds n in s2 iff
ex k being Nat st n=4*k+3 & n is prime;
A6: for n being Element of NAT holds n in s1 iff P[n]
proof
let n be Element of NAT;
thus n in s1 implies P[n]
proof
assume n in s1;
then consider k being Nat such that
A7: n=4*k+3 & n is prime by A4;
thus P[n] by A7;
end;
assume P[n];
then consider k being Nat such that
A8: n=4*k+3 & 4*k+3 is prime;
thus n in s1 by A8,A4;
end;
A9: for n being Element of NAT holds n in s2 iff P[n]
proof
let n be Element of NAT;
thus n in s2 implies P[n]
proof
assume n in s2;
then consider k being Nat such that
A10: n=4*k+3 & n is prime by A5;
thus P[n] by A10;
end;
assume P[n];
then ex k being Nat st n=4*k+3 & 4*k+3 is prime;
hence n in s2 by A5;
end;
thus s1=s2 from SUBSET_1:sch 2(A6,A9);
end;
end;
theorem Th4:
for n being Nat st n in 4k+3_Primes holds n >= 3
proof
let n be Nat;
assume n in 4k+3_Primes;
then consider k being Nat such that
A1: n=4*k+3 & n is prime by Def1;
thus n >= 3 by A1,NAT_1:11;
end;
registration
cluster 4k+3_Primes -> infinite;
coherence
proof
3=4*0+3 & 3 is prime by PEPIN:41; then
A1: 3 in 4k+3_Primes by Def1;
assume 4k+3_Primes is finite;
then consider n being Element of NAT such that
A2: 4k+3_Primes c= Seg n \/ {0} by A1,HEYTING3:1;
A3: 4k+3_Primes c= Seg n by A2,ZFMISC_1:135,Th4;
set X=4k+3_Primes\{3};
X c= 4k+3_Primes by XBOOLE_1:36;
then X c= Seg n by A3,XBOOLE_1:1;
then a4: X is included_in_Seg by FINSEQ_1:def 13;
set N=4*(Product Sgm X) + 3;
consider p,q being Nat such that
A5: p=4*q+3 & p is prime & p divides N by Th3;
A6: p in 4k+3_Primes by Def1,A5;
rng Sgm X c= SetPrimes
proof
let a be object;
assume A7: a in rng Sgm X;
then a in X by a4,FINSEQ_1:def 14;
then A8: a in 4k+3_Primes by XBOOLE_0:def 5;
reconsider n=a as Nat by A7;
consider k being Nat such that
A9: n=4*k+3 & n is prime by A8,Def1;
thus a in SetPrimes by A9,NEWTON:def 6;
end;
then reconsider SX=Sgm X as FinSequence of SetPrimes by FINSEQ_1:def 4;
for p being prime Nat st p in 4k+3_Primes holds not p divides N
proof
let p be prime Nat;
assume A10: p in 4k+3_Primes;
assume A11: p divides N;
p >= 3 by A10,Th4;
then per cases by XXREAL_0:1;
suppose A12: p=3;
2,3 are_coprime by INT_2:30,INT_2:28,PEPIN:41;
then A13: 2*2,3 are_coprime by EULER_1:14;
p divides 4*(Product Sgm X) by A11,A12,INT_2:1;
then p in rng SX by A12,A13,EULER_1:13,NAT_3:8;
then p in X by a4,FINSEQ_1:def 14;
then not p in {3} by XBOOLE_0:def 5;
hence contradiction by A12,TARSKI:def 1;
end;
suppose A14: p>3;
then not p in {3} by TARSKI:def 1;
then p in X by A10,XBOOLE_0:def 5;
then p in rng SX by a4,FINSEQ_1:def 14;
then p divides 4*Product Sgm X by NAT_D:9,NAT_3:7;
hence contradiction by A14,INT_2:1,27,A11;
end;
end;
hence contradiction by A5,A6;
end;
end;
:: Problem 13
theorem
for n being Nat st n in 4k+3_Primes
for x being even Nat
for i being Nat holds not n divides x|^|^(i+2) + 1
proof
let n be Nat;
assume A1: n in 4k+3_Primes;
then A2: n >= 3 by Th4;
let x be even Nat;
let i be Nat;
reconsider i2=i+2 as Nat;
consider m being Element of NAT such that
A3: i2 = 2*m or i2 = 2*m+1 by SCHEME1:1;
per cases;
suppose A4: x is zero;
per cases by A3;
suppose i+2=2*m;
then A5: x|^|^(i+2) = 1 by A4,ORDINAL5:20;
assume n divides x|^|^(i+2) + 1;
then n <= 2 by INT_2:27,A5;
hence contradiction by A2,XXREAL_0:2;
end;
suppose i+2=2*m+1;
then A6: x|^|^(i+2) = 0 by A4,ORDINAL5:20;
assume n divides x|^|^(i+2) + 1;
then n <= 1 by INT_2:27,A6;
hence contradiction by A2,XXREAL_0:2;
end;
end;
suppose x is non zero;
then consider m being Nat such that
A7: x|^|^(i+1) = 2*m by ABIAN:def 2;
A8: x|^|^((i+1)+1) = x|^|^(Segm((i+1)+1))
.= x|^|^(succ Segm(i+1)) by NAT_1:38
.= exp(x,x|^|^(i+1)) by ORDINAL5:14
.= x|^(m*2) by A7
.= (x|^m)|^2 by NEWTON:9;
assume n divides x|^|^(i+2) + 1;
then (x|^m)|^2 - -1 mod n = 0 by A8;
then A9: (x|^m)^2 - -1 mod n = 0 by WSIERP_1:1;
consider k being Nat such that
A10: n=4*k+3 & n is prime by A1,Def1;
A11: n mod 4 = 3 mod 4 by A10,NAT_D:21
.= 3 by NAT_D:24;
n > 2 by A2,XXREAL_0:2;
hence contradiction by A11,A9,INT_5:def 2,A10,INT_5:38;
end;
end;
begin :: Problem 31
theorem Th6:
for a being Integer st not 3 divides a holds a|^3 mod 9 = 1 or a|^3 mod 9 = 8
proof
let a be Integer;
assume not 3 divides a;
then a mod 3 <> 0 by INT_1:62;
then a mod 3 > 0 & a mod 3 < 3 by INT_1:58;
then A1: a mod 3 > 0 & a mod 3 in Segm 3 by NAT_1:44;
set d = a div 3;
A2:
now
assume a mod 3 = 1;
then a = d*3 + 1 by INT_1:59;
then a|^3 = (3*d)|^3+3*(3*d)|^2+3*(3*d)+1 by SERIES_2:2
.= (3|^3*d|^3)+3*(3*d)|^2+3*(3*d)+1 by NEWTON:7
.= ((3*3*3)*d|^3)+3*(3*d)|^2+3*(3*d)+1 by POLYEQ_3:27
.= ((3*3*3)*d|^3)+3*((3|^2*d|^2))+3*(3*d)+1 by NEWTON:7
.= ((3*3*3)*d|^3)+3*((3*3)*d|^2)+3*(3*d)+1 by WSIERP_1:1
.= 9*(3*d|^3+3*d|^2+d)+1;
hence a|^3 mod 9 = ((9*(3*d|^3+3*d|^2+d) mod 9) + (1 mod 9)) mod 9
by NAT_D:66
.= (0 + (1 mod 9)) mod 9
.= 1 by NAT_D:63;
end;
A3:
now
assume a mod 3 = 2;
then a = d*3 + 2 by INT_1:59;
then a|^3 = (3*d)|^3+3*(3*d)|^2*2+3*2|^2*(3*d)+2|^3 by SERIES_4:2
.= (3|^3*d|^3)+3*(3*d)|^2*2+3*2|^2*(3*d)+2|^3 by NEWTON:7
.= ((3*3*3)*d|^3)+3*(3*d)|^2*2+3*2|^2*(3*d)+2|^3 by POLYEQ_3:27
.= ((3*3*3)*d|^3)+3*(3|^2*d|^2)*2+3*2|^2*(3*d)+2|^3 by NEWTON:7
.= ((3*3*3)*d|^3)+3*((3*3)*d|^2)*2+3*2|^2*(3*d)+2|^3 by WSIERP_1:1
.= 9*(3*d|^3+3*d|^2*2+2|^2*d)+(2*2*2) by POLYEQ_3:27;
hence a|^3 mod 9 = ((9*(3*d|^3+3*d|^2*2+2|^2*d)) mod 9 +
((2*2*2) mod 9)) mod 9 by NAT_D:66
.= (0 + (8 mod 9)) mod 9
.= 8 by NAT_D:63;
end;
thus thesis by A2,A3,A1,ENUMSET1:def 1,CARD_1:51;
end;
:: Problem 31
theorem
for a,b,c being Integer st 9 divides a|^3+b|^3+c|^3 holds
3 divides a or 3 divides b or 3 divides c
proof
let a,b,c be Integer;
assume 9 divides a|^3+b|^3+c|^3;
then A1: a|^3+b|^3+c|^3 mod 9 = 0;
assume not 3 divides a & not 3 divides b & not 3 divides c;
then per cases by Th6;
suppose A2: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (2 + 1) mod 9 by A2,NAT_D:63;
hence contradiction by A1,NAT_D:63;
end;
suppose A3: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (2+8) mod 9 by A3,NAT_D:63
.= (1+9) mod 9
.= ((1 mod 9) + (9 mod 9)) mod 9 by NAT_D:66
.= ((1 mod 9) + 0) mod 9 by INT_1:50;
hence contradiction by A1,NAT_D:63;
end;
suppose A4: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (0+1) mod 9 by A4,INT_1:50;
hence contradiction by A1,NAT_D:63;
end;
suppose A5: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (0+8) mod 9 by A5,INT_1:50;
hence contradiction by A1,NAT_D:63;
end;
suppose A6: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (0+1) mod 9 by A6,INT_1:50;
hence contradiction by A1,NAT_D:63;
end;
suppose A7: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (0+8) mod 9 by A7,INT_1:50;
hence contradiction by A1,NAT_D:63;
end;
suppose A8: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (((9 + 7) mod 9) + 1) mod 9 by A8
.= ((((9 mod 9) + (7 mod 9)) mod 9) + 1) mod 9 by NAT_D:66
.= (((0 + (7 mod 9)) mod 9) + 1) mod 9 by INT_1:50
.= (7+1) mod 9 by NAT_D:63;
hence contradiction by A1,NAT_D:63;
end;
suppose A9: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3) mod 9 = (((a|^3+b|^3) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= ((((a|^3 mod 9) + (b|^3 mod 9)) mod 9) + (c|^3 mod 9)) mod 9
by NAT_D:66
.= (((9 + 7) mod 9) + 8) mod 9 by A9
.= ((((9 mod 9) + (7 mod 9)) mod 9) + 8) mod 9 by NAT_D:66
.= (((0 + (7 mod 9)) mod 9) + 8) mod 9 by INT_1:50
.= (7+8) mod 9 by NAT_D:63
.= (6+9) mod 9
.= ((6 mod 9) + (9 mod 9)) mod 9 by NAT_D:66
.= ((6 mod 9) + 0) mod 9 by INT_1:50
.= 6 mod 9;
hence contradiction by A1,NAT_D:63;
end;
end;
begin :: Problem 32
theorem Th8:
for a,b,c,n being Integer holds
(a+b+c) mod n = ((a mod n)+(b mod n)+(c mod n)) mod n
proof
let a,b,c,n be Integer;
thus (a+b+c) mod n = ((a+b) mod n + (c mod n)) mod n by NAT_D:66
.= ((((a mod n) + (b mod n)) mod n) + ((c mod n) mod n)) mod n by NAT_D:66
.= ((a mod n)+(b mod n)+(c mod n)) mod n by NAT_D:66;
end;
theorem Th9:
for a,b,c,d,n being Integer holds
(a+b+c+d) mod n = ((a mod n)+(b mod n)+(c mod n)+(d mod n)) mod n
proof
let a,b,c,d,n be Integer;
thus (a+b+c+d) mod n = ((a+b+c) mod n + (d mod n)) mod n by NAT_D:66
.= ((((a mod n)+(b mod n)+(c mod n)) mod n) +((d mod n) mod n)) mod n
by Th8
.= ((a mod n)+(b mod n)+(c mod n)+(d mod n)) mod n by NAT_D:66;
end;
theorem Th10:
for a,b,c,d,e,n being Integer holds
(a+b+c+d+e) mod n = ((a mod n)+(b mod n)+(c mod n)+(d mod n)+(e mod n)) mod n
proof
let a,b,c,d,e,n being Integer;
thus (a+b+c+d+e) mod n = ((a+b+c+d) mod n + (e mod n)) mod n by NAT_D:66
.= ((((a mod n)+(b mod n)+(c mod n)+(d mod n)) mod n) + ((e mod n) mod n))
mod n by Th9
.= ((a mod n)+(b mod n)+(c mod n)+(d mod n)+(e mod n)) mod n by NAT_D:66;
end;
:: Problem 32
theorem
for a1,a2,a3,a4,a5 being Integer st 9 divides a1|^3+a2|^3+a3|^3+a4|^3+a5|^3
holds 3 divides a1*a2*a3*a4*a5
proof
let a,b,c,d,e be Integer;
assume 9 divides a|^3+b|^3+c|^3+d|^3+e|^3;
then A1: a|^3+b|^3+c|^3+d|^3+e|^3 mod 9 = 0;
assume A2: not 3 divides a*b*c*d*e;
then A3: not 3 divides a*(b*c*d*e);
A4: not 3 divides b*(a*c*d*e) by A2;
A5: not 3 divides c*(a*b*d*e) by A2;
not 3 divides d*(a*b*c*e) by A2;
then per cases by Th6,A3,A4,A5,A2,INT_2:2;
suppose A6: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+1+1+1) mod 9 by A6,Th10;
hence contradiction by A1,NAT_D:63;
end;
suppose A7: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+1+1+8) mod 9 by A7,Th10
.= (9*1 + 3) mod 9
.= ((9*1) mod 9 + (3 mod 9)) mod 9 by NAT_D:66
.= ((9*1) mod 9 + 3) mod 9
.= (0 + 3) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A8: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+1+8+1) mod 9 by A8,Th10
.= (9*1 + 3) mod 9
.= ((9*1) mod 9 + (3 mod 9)) mod 9 by NAT_D:66
.= ((9*1) mod 9 + 3) mod 9
.= (0 + 3) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A9: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+1+8+8) mod 9 by A9,Th10
.= (9*2 + 1) mod 9
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A10: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+8+1+1) mod 9 by A10,Th10
.= (9*1 + 3) mod 9
.= ((9*1) mod 9 + (3 mod 9)) mod 9 by NAT_D:66
.= ((9*1) mod 9 + 3) mod 9
.= (0 + 3) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A11: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+8+1+8) mod 9 by A11,Th10
.= (9*2 + 1) mod 9
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A12: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+8+8+1) mod 9 by A12,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A13: a|^3 mod 9 = 1 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+1+8+8+8) mod 9 by A13,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A14: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+1+1+1) mod 9 by A14,Th10
.= (9*1 + 3) mod 9
.= ((9*1) mod 9 + (3 mod 9)) mod 9 by NAT_D:66
.= ((9*1) mod 9 + 3) mod 9
.= (0 + 3) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A15: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+1+1+8) mod 9 by A15,Th10
.= (9*2 + 1) mod 9
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A16: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+1+8+1) mod 9 by A16,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A17: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+1+8+8) mod 9 by A17,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A18: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+8+1+1) mod 9 by A18,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A19: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+8+1+8) mod 9 by A19,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A20: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+8+8+1) mod 9 by A20,Th10
.= (9*2 + 8) mod 9
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A21: a|^3 mod 9 = 1 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (1+8+8+8+8) mod 9 by A21,Th10
.= (9*3 + 6) mod 9
.= ((9*3) mod 9 + (6 mod 9)) mod 9 by NAT_D:66
.= ((9*3) mod 9 + 6) mod 9
.= (0 + 6) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A22: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+1+1+1) mod 9 by A22,Th10
.= (9*1 + 3) mod 9
.= ((9*1) mod 9 + (3 mod 9)) mod 9 by NAT_D:66
.= ((9*1) mod 9 + 3) mod 9
.= (0 + 3) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A23: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+1+1+8) mod 9 by A23,Th10
.= (9*2 + 1) mod 9
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A24: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+1+8+1) mod 9 by A24,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A25: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+1+8+8) mod 9 by A25,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A26: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+8+1+1) mod 9 by A26,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A27: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+8+1+8) mod 9 by A27,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A28: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+8+8+1) mod 9 by A28,Th10
.= (9*2 + 8) mod 9
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A29: a|^3 mod 9 = 8 & b|^3 mod 9 = 1 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+1+8+8+8) mod 9 by A29,Th10
.= (9*3 + 6) mod 9
.= ((9*3) mod 9 + (6 mod 9)) mod 9 by NAT_D:66
.= ((9*3) mod 9 + 6) mod 9
.= (0 + 6) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A30: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+1+1+1) mod 9 by A30,Th10
.= ((9*2) mod 9 + (1 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 1) mod 9
.= (0 + 1) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A31: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+1+1+8) mod 9 by A31,Th10
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A32: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+1+8+1) mod 9 by A32,Th10
.= (9*2 + 8) mod 9
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A33: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 1
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+1+8+8) mod 9 by A33,Th10
.= (9*3 + 6) mod 9
.= ((9*3) mod 9 + (6 mod 9)) mod 9 by NAT_D:66
.= ((9*3) mod 9 + 6) mod 9
.= (0 + 6) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A34: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+8+1+1) mod 9 by A34,Th10
.= (9*2 + 8) mod 9
.= ((9*2) mod 9 + (8 mod 9)) mod 9 by NAT_D:66
.= ((9*2) mod 9 + 8) mod 9
.= (0 + 8) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A35: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 1 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+8+1+8) mod 9 by A35,Th10
.= (9*3 + 6) mod 9
.= ((9*3) mod 9 + (6 mod 9)) mod 9 by NAT_D:66
.= ((9*3) mod 9 + 6) mod 9
.= (0 + 6) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A36: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 1;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+8+8+1) mod 9 by A36,Th10
.= (9*3 + 6) mod 9
.= ((9*3) mod 9 + (6 mod 9)) mod 9 by NAT_D:66
.= ((9*3) mod 9 + 6) mod 9
.= (0 + 6) mod 9;
hence contradiction by A1,NAT_D:63;
end;
suppose A37: a|^3 mod 9 = 8 & b|^3 mod 9 = 8 & c|^3 mod 9 = 8
& d|^3 mod 9 = 8 & e|^3 mod 9 = 8;
((a|^3+b|^3)+c|^3+d|^3+e|^3) mod 9 = (8+8+8+8+8) mod 9 by A37,Th10
.= (9*4 + 4) mod 9
.= ((9*4) mod 9 + (4 mod 9)) mod 9 by NAT_D:66
.= ((9*4) mod 9 + 4) mod 9
.= (0 + 4) mod 9;
hence contradiction by A1,NAT_D:63;
end;
end;
begin :: Problem 33
reserve a,b,c,k,m,n for Nat;
reserve p for Prime;
::$CT
Lm1:
for x,y,z being Nat st
x,y are_coprime & x|^2+y|^2 = z|^4 & x is odd holds 7 divides x*y
proof
let x,y,z be Nat such that
A1: x,y are_coprime and
A2: x|^2+y|^2 = z|^4;
per cases;
suppose 7 divides y;
hence thesis by INT_2:2;
end;
suppose
A3: not 7 divides y;
set c = z|^2;
A4: x|^2 = x^2 & y|^2 = y^2 by NEWTON:81;
A5: z|^2 = z^2 by NEWTON:81;
A6: z|^(2+2) = c^2 by NEWTON:8;
assume x is odd;
then consider n,m being Element of NAT such that
n <= m and
A7: x = m^2 - n^2 and
A8: y = 2*n*m and
A9: z^2 = m^2 + n^2 by A1,A2,A4,A5,A6,PYTHTRIP:11;
A10: not 7 divides m by A3,A8,INT_2:2;
y = n*(2*m) by A8;
then
A11: not 7 divides n by A3,INT_2:2;
A12: z^2 mod 7 = 0 or z^2 mod 7 = 1 or z^2 mod 7 = 2 or z^2 mod 7 = 4
by NUMBER02:49;
A13: m^2 mod 7 = ((m mod 7) * (m mod 7)) mod 7 &
n^2 mod 7 = ((n mod 7) * (n mod 7)) mod 7 by NAT_D:67;
A14: (m^2+n^2) mod 7 = ((m^2 mod 7) + (n^2 mod 7)) mod 7 by NAT_D:66;
A15: (1*7+2) mod 7 = 2 & (2*7+2) mod 7 = 2 & (3*7+4) mod 7 = 4 &
(5*7+1) mod 7 = 1 by NUMBER02:16;
(m mod (6+1) = 0 or ... or m mod (6+1) = 6) &
(n mod (6+1) = 0 or ... or n mod (6+1) = 6) by NUMBER03:11;
then ((m^2 mod 7) - (n^2 mod 7)) mod 7 = 0
by A9,A10,A11,A12,A13,A14,A15,NAT_D:24,INT_1:62;
then (m^2 - n^2) mod 7 = 0 by INT_6:7;
then 7 divides x by A7,INT_1:62;
hence thesis by INT_2:2;
end;
end;
:: Problem 33 a
theorem
for x,y,z being Nat st x,y are_coprime & x|^2+y|^2 = z|^4 holds 7 divides x*y
proof
let x,y,z be Nat;
assume
A1: x,y are_coprime;
then x is odd or y is odd by NEWTON05:35;
hence thesis by A1,Lm1;
end;
:: Problem 33 b
theorem
not 15,20 are_coprime & 15|^2+20|^2 = 5|^4 & not 7 divides 15*20
proof
(3*1+1) mod 3 = 1 by NUMBER02:16;
then
A1: 1 = 3 gcd (4 mod 3) by NEWTON:51
.= 4 gcd 3 by NAT_D:30;
(5*3) gcd (5*4) = 5*(3 gcd 4) by PYTHTRIP:8;
hence not 15,20 are_coprime by A1;
A2: 15|^2 = 15*15 & 20|^2 = 20*20 by WSIERP_1:1;
5|^4 = 5*5*5*5 by POLYEQ_5:3;
hence 15|^2+20|^2 = 5|^4 by A2;
15*20 = 7*42+6;
then 15*20 mod 7 = 6 by NUMBER02:16;
hence not 7 divides 15*20;
end;
begin :: Problem 35
definition
let x,y be Nat;
pred x,y satisfy_Sierpinski_problem_35 means
x*(x+1) divides y*(y+1) & not x divides y & not x+1 divides y &
not x divides y+1 & not x+1 divides y+1;
end;
theorem Th15:
for x,y being Nat st x = 36*k+14 & y = (12*k+5)*(18*k+7) holds
x,y satisfy_Sierpinski_problem_35
proof
let x,y be Nat such that
A1: x = 36*k+14 and
A2: y = (12*k+5)*(18*k+7);
A3: x*(x+1) = 2*3*(12*k+5)*(18*k+7) = 6*y by A1,A2;
y+1 = 6*(36*k*k+29*k+6) by A2;
then 6 divides y+1;
hence x*(x+1) divides y*(y+1) by A2,A3,INT_4:7;
A4: x = 2*(18*k+7) by A1;
y = 2*(108*k*k+87*k+17)+1 by A2;
hence not x divides y by A4;
A5: x+1 = 3*(12*k+5) by A1;
then
A6: 3 divides x+1;
y = 3*(72*k*k+58*k+11)+2 by A2;
hence not x+1 divides y by A6,INT_2:9,NAT_4:9;
0+7 <= 18*k+7 by XREAL_1:6;
then
A7: 18*k+7 <> 1;
A8: 18*k+7 divides x by A4;
18*k+7 divides y by A2;
then not 18*k+7 divides y+1 by A7,NEWTON:39;
hence not x divides y+1 by A8,INT_2:9;
0+5 <= 12*k+5 by XREAL_1:6;
then
A9: 12*k+5 <> 1;
A10: 12*k+5 divides x+1 by A5;
12*k+5 divides y by A2;
then not 12*k+5 divides y+1 by A9,NEWTON:39;
hence not x+1 divides y+1 by A10,INT_2:9;
end;
:: Problem 35 a
theorem
{[x,y] where x,y is Nat: x,y satisfy_Sierpinski_problem_35} is infinite
proof
set A = {[x,y] where x,y is Nat: x,y satisfy_Sierpinski_problem_35};
deffunc F(Nat) = [36*$1+14,(12*$1+5)*(18*$1+7)];
consider f being ManySortedSet of NAT such that
A1: for d being Element of NAT holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = NAT by PARTFUN1:def 2;
A3: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A4: k in dom f and
A5: f.k = y by FUNCT_1:def 3;
reconsider k as Element of NAT by A4,PARTFUN1:def 2;
36*k+14,(12*k+5)*(18*k+7) satisfy_Sierpinski_problem_35 by Th15;
then F(k) in A;
hence thesis by A1,A5;
end;
f is one-to-one
proof
let x1,x2 be object such that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
reconsider x1,x2 as Element of NAT by A6,PARTFUN1:def 2;
f.x1 = F(x1) & f.x2 = F(x2) by A1;
then 36*x1+14 = 36*x2+14 by A7,XTUPLE_0:1;
hence thesis;
end;
hence thesis by A2,A3,CARD_1:59;
end;
:: Problem 35 b
theorem
14,35 satisfy_Sierpinski_problem_35
proof
1260 = 6*210;
hence 14*(14+1) divides 35*(35+1);
35 = 2*14+7;
hence not 14 divides 35 by NAT_4:9;
35 = 2*15+5;
hence not 14+1 divides 35 by NAT_4:9;
36 = 2*14+8;
hence not 14 divides 35+1 by NAT_4:9;
36 = 2*15+6;
hence not 14+1 divides 35+1 by NAT_4:9;
end;
:: Problem 35 c
theorem
not ex x,y being Nat st x < 14 & y < 35 & x,y satisfy_Sierpinski_problem_35
proof
given x,y being Nat such that
A1: x < 14 and
A2: y < 35 and
A3: x,y satisfy_Sierpinski_problem_35;
14 = 13+1;
then x <= 13 by A1,NAT_1:13;
then
A4: x = 0 or ... or x = 13;
35 = 34+1;
then y <= 34 by A2,NAT_1:13;
then
A5: y = 0 or ... or y = 34;
per cases by A4;
suppose x = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose x = 1;
hence contradiction by A3,NAT_D:6;
end;
suppose
A6: x = 2;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A6;
end;
suppose y = 2;
hence contradiction by A3,A6;
end;
suppose y = 3;
hence contradiction by A3,A6;
end;
suppose
A7: y = 4;
2 divides 2*2;
hence contradiction by A3,A6,A7;
end;
suppose
A8: y = 5;
2 divides 2*3;
hence contradiction by A3,A6,A8;
end;
suppose
A9: y = 6;
2 divides 2*3;
hence contradiction by A3,A6,A9;
end;
suppose
A10: y = 7;
2 divides 2*4;
hence contradiction by A3,A6,A10;
end;
suppose
A11: y = 8;
2 divides 2*4;
hence contradiction by A3,A6,A11;
end;
suppose
A12: y = 9;
2 divides 2*5;
hence contradiction by A3,A6,A12;
end;
suppose
A13: y = 10;
2 divides 2*5;
hence contradiction by A3,A6,A13;
end;
suppose
A14: y = 11;
2 divides 2*6;
hence contradiction by A3,A6,A14;
end;
suppose
A15: y = 12;
2 divides 2*6;
hence contradiction by A3,A6,A15;
end;
suppose
A16: y = 13;
2 divides 2*7;
hence contradiction by A3,A6,A16;
end;
suppose
A17: y = 14;
2 divides 2*7;
hence contradiction by A3,A6,A17;
end;
suppose
A18: y = 15;
2 divides 2*8;
hence contradiction by A3,A6,A18;
end;
suppose
A19: y = 16;
2 divides 2*8;
hence contradiction by A3,A6,A19;
end;
suppose
A20: y = 17;
2 divides 2*9;
hence contradiction by A3,A6,A20;
end;
suppose
A21: y = 18;
2 divides 2*9;
hence contradiction by A3,A6,A21;
end;
suppose
A22: y = 19;
2 divides 2*10;
hence contradiction by A3,A6,A22;
end;
suppose
A23: y = 20;
2 divides 2*10;
hence contradiction by A3,A6,A23;
end;
suppose
A24: y = 21;
2 divides 2*11;
hence contradiction by A3,A6,A24;
end;
suppose
A25: y = 22;
2 divides 2*11;
hence contradiction by A3,A6,A25;
end;
suppose
A26: y = 23;
2 divides 2*12;
hence contradiction by A3,A6,A26;
end;
suppose
A27: y = 24;
2 divides 2*12;
hence contradiction by A3,A6,A27;
end;
suppose
A28: y = 25;
2 divides 2*13;
hence contradiction by A3,A6,A28;
end;
suppose
A29: y = 26;
2 divides 2*13;
hence contradiction by A3,A6,A29;
end;
suppose
A30: y = 27;
2 divides 2*14;
hence contradiction by A3,A6,A30;
end;
suppose
A31: y = 28;
2 divides 2*14;
hence contradiction by A3,A6,A31;
end;
suppose
A32: y = 29;
2 divides 2*15;
hence contradiction by A3,A6,A32;
end;
suppose
A33: y = 30;
2 divides 2*15;
hence contradiction by A3,A6,A33;
end;
suppose
A34: y = 31;
2 divides 2*16;
hence contradiction by A3,A6,A34;
end;
suppose
A35: y = 32;
2 divides 2*16;
hence contradiction by A3,A6,A35;
end;
suppose
A36: y = 33;
2 divides 2*17;
hence contradiction by A3,A6,A36;
end;
suppose
A37: y = 34;
2 divides 2*17;
hence contradiction by A3,A6,A37;
end;
end;
suppose
A38: x = 3;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A38,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A38;
end;
suppose y = 3;
hence contradiction by A3,A38;
end;
suppose y = 4;
hence contradiction by A3,A38;
end;
suppose
A39: y = 5;
3 divides 3*2;
hence contradiction by A3,A38,A39;
end;
suppose
A40: y = 6;
3 divides 3*2;
hence contradiction by A3,A38,A40;
end;
suppose
A41: y = 7;
4 divides 4*2;
hence contradiction by A3,A38,A41;
end;
suppose
A42: y = 8;
4 divides 4*2;
hence contradiction by A3,A38,A42;
end;
suppose
A43: y = 9;
3 divides 3*3;
hence contradiction by A3,A38,A43;
end;
suppose
A44: y = 10;
110 = 12*9+2;
hence contradiction by A3,A38,A44,NAT_4:9;
end;
suppose
A45: y = 11;
3 divides 3*4;
hence contradiction by A3,A38,A45;
end;
suppose
A46: y = 12;
3 divides 3*4;
hence contradiction by A3,A38,A46;
end;
suppose
A47: y = 13;
182 = 12*15+2;
hence contradiction by A3,A38,A47,NAT_4:9;
end;
suppose
A48: y = 14;
3 divides 3*5;
hence contradiction by A3,A38,A48;
end;
suppose
A49: y = 15;
3 divides 3*5;
hence contradiction by A3,A38,A49;
end;
suppose
A50: y = 16;
4 divides 4*4;
hence contradiction by A3,A38,A50;
end;
suppose
A51: y = 17;
3 divides 3*6;
hence contradiction by A3,A38,A51;
end;
suppose
A52: y = 18;
3 divides 3*6;
hence contradiction by A3,A38,A52;
end;
suppose
A53: y = 19;
380 = 12*31+8;
hence contradiction by A3,A38,A53,NAT_4:9;
end;
suppose
A54: y = 20;
4 divides 4*5;
hence contradiction by A3,A38,A54;
end;
suppose
A55: y = 21;
3 divides 3*7;
hence contradiction by A3,A38,A55;
end;
suppose
A56: y = 22;
506 = 12*42+2;
hence contradiction by A3,A38,A56,NAT_4:9;
end;
suppose
A57: y = 23;
3 divides 3*8;
hence contradiction by A3,A38,A57;
end;
suppose
A58: y = 24;
3 divides 3*8;
hence contradiction by A3,A38,A58;
end;
suppose
A59: y = 25;
650 = 12*54+2;
hence contradiction by A3,A38,A59,NAT_4:9;
end;
suppose
A60: y = 26;
3 divides 3*9;
hence contradiction by A3,A38,A60;
end;
suppose
A61: y = 27;
3 divides 3*9;
hence contradiction by A3,A38,A61;
end;
suppose
A62: y = 28;
4 divides 4*7;
hence contradiction by A3,A38,A62;
end;
suppose
A63: y = 29;
870 = 12*72+6;
hence contradiction by A3,A38,A63,NAT_4:9;
end;
suppose
A64: y = 30;
3 divides 3*10;
hence contradiction by A3,A38,A64;
end;
suppose
A65: y = 31;
992 = 12*82+8;
hence contradiction by A3,A38,A65,NAT_4:9;
end;
suppose
A66: y = 32;
4 divides 4*8;
hence contradiction by A3,A38,A66;
end;
suppose
A67: y = 33;
3 divides 3*11;
hence contradiction by A3,A38,A67;
end;
suppose
A68: y = 34;
1190 = 12*99+2;
hence contradiction by A3,A38,A68,NAT_4:9;
end;
end;
suppose
A69: x = 4;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A69,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A69,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A69;
end;
suppose y = 4;
hence contradiction by A3,A69;
end;
suppose y = 5;
hence contradiction by A3,A69;
end;
suppose
A70: y = 6;
42 = 20*2+2;
hence contradiction by A3,A69,A70,NAT_4:9;
end;
suppose
A71: y = 7;
56 = 20*2+16;
hence contradiction by A3,A69,A71,NAT_4:9;
end;
suppose
A72: y = 8;
4 divides 4*2;
hence contradiction by A3,A69,A72;
end;
suppose
A73: y = 9;
90 = 20*4+10;
hence contradiction by A3,A69,A73,NAT_4:9;
end;
suppose
A74: y = 10;
110 = 20*5+10;
hence contradiction by A3,A69,A74,NAT_4:9;
end;
suppose
A75: y = 11;
132 = 20*6+12;
hence contradiction by A3,A69,A75,NAT_4:9;
end;
suppose
A76: y = 12;
4 divides 4*3;
hence contradiction by A3,A69,A76;
end;
suppose
A77: y = 13;
182 = 20*9+2;
hence contradiction by A3,A69,A77,NAT_4:9;
end;
suppose
A78: y = 14;
210 = 20*10+10;
hence contradiction by A3,A69,A78,NAT_4:9;
end;
suppose
A79: y = 15;
4 divides 4*4;
hence contradiction by A3,A69,A79;
end;
suppose
A80: y = 16;
4 divides 4*4;
hence contradiction by A3,A69,A80;
end;
suppose
A81: y = 17;
306 = 20*15+6;
hence contradiction by A3,A69,A81,NAT_4:9;
end;
suppose
A82: y = 18;
342 = 20*17+2;
hence contradiction by A3,A69,A82,NAT_4:9;
end;
suppose
A83: y = 19;
4 divides 4*5;
hence contradiction by A3,A69,A83;
end;
suppose
A84: y = 20;
4 divides 4*5;
hence contradiction by A3,A69,A84;
end;
suppose
A85: y = 21;
462 = 20*23+2;
hence contradiction by A3,A69,A85,NAT_4:9;
end;
suppose
A86: y = 22;
506 = 20*25+6;
hence contradiction by A3,A69,A86,NAT_4:9;
end;
suppose
A87: y = 23;
4 divides 4*6;
hence contradiction by A3,A69,A87;
end;
suppose
A88: y = 24;
4 divides 4*6;
hence contradiction by A3,A69,A88;
end;
suppose
A89: y = 25;
650 = 20*32+10;
hence contradiction by A3,A69,A89,NAT_4:9;
end;
suppose
A90: y = 26;
702 = 20*35+2;
hence contradiction by A3,A69,A90,NAT_4:9;
end;
suppose
A91: y = 27;
4 divides 4*7;
hence contradiction by A3,A69,A91;
end;
suppose
A92: y = 28;
4 divides 4*7;
hence contradiction by A3,A69,A92;
end;
suppose
A93: y = 29;
870 = 20*43+10;
hence contradiction by A3,A69,A93,NAT_4:9;
end;
suppose
A94: y = 30;
930 = 20*46+10;
hence contradiction by A3,A69,A94,NAT_4:9;
end;
suppose
A95: y = 31;
4 divides 4*8;
hence contradiction by A3,A69,A95;
end;
suppose
A96: y = 32;
4 divides 4*8;
hence contradiction by A3,A69,A96;
end;
suppose
A97: y = 33;
1122 = 20*56+2;
hence contradiction by A3,A69,A97,NAT_4:9;
end;
suppose
A98: y = 34;
1190 = 20*59+10;
hence contradiction by A3,A69,A98,NAT_4:9;
end;
end;
suppose
A99: x = 5;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A99,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A99,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A99,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A99;
end;
suppose y = 5;
hence contradiction by A3,A99;
end;
suppose y = 6;
hence contradiction by A3,A99;
end;
suppose
A100: y = 7;
56 = 30*1+26;
hence contradiction by A3,A99,A100,NAT_4:9;
end;
suppose
A101: y = 8;
72 = 30*2+12;
hence contradiction by A3,A99,A101,NAT_4:9;
end;
suppose
A102: y = 9;
5 divides 5*2;
hence contradiction by A3,A99,A102;
end;
suppose
A103: y = 10;
5 divides 5*2;
hence contradiction by A3,A99,A103;
end;
suppose
A104: y = 11;
132 = 30*4+12;
hence contradiction by A3,A99,A104,NAT_4:9;
end;
suppose
A105: y = 12;
6 divides 6*2;
hence contradiction by A3,A99,A105;
end;
suppose
A106: y = 13;
182 = 30*6+2;
hence contradiction by A3,A99,A106,NAT_4:9;
end;
suppose
A107: y = 14;
5 divides 5*3;
hence contradiction by A3,A99,A107;
end;
suppose
A108: y = 15;
5 divides 5*3;
hence contradiction by A3,A99,A108;
end;
suppose
A109: y = 16;
272 = 30*9+2;
hence contradiction by A3,A99,A109,NAT_4:9;
end;
suppose
A110: y = 17;
306 = 30*10+6;
hence contradiction by A3,A99,A110,NAT_4:9;
end;
suppose
A111: y = 18;
6 divides 6*3;
hence contradiction by A3,A99,A111;
end;
suppose
A112: y = 19;
5 divides 5*4;
hence contradiction by A3,A99,A112;
end;
suppose
A113: y = 20;
5 divides 5*4;
hence contradiction by A3,A99,A113;
end;
suppose
A114: y = 21;
462 = 30*15+12;
hence contradiction by A3,A99,A114,NAT_4:9;
end;
suppose
A115: y = 22;
506 = 30*16+26;
hence contradiction by A3,A99,A115,NAT_4:9;
end;
suppose
A116: y = 23;
6 divides 6*4;
hence contradiction by A3,A99,A116;
end;
suppose
A117: y = 24;
6 divides 6*4;
hence contradiction by A3,A99,A117;
end;
suppose
A118: y = 25;
5 divides 5*5;
hence contradiction by A3,A99,A118;
end;
suppose
A119: y = 26;
702 = 30*23+12;
hence contradiction by A3,A99,A119,NAT_4:9;
end;
suppose
A120: y = 27;
756 = 30*25+6;
hence contradiction by A3,A99,A120,NAT_4:9;
end;
suppose
A121: y = 28;
812 = 30*27+2;
hence contradiction by A3,A99,A121,NAT_4:9;
end;
suppose
A122: y = 29;
5 divides 5*6;
hence contradiction by A3,A99,A122;
end;
suppose
A123: y = 30;
5 divides 5*6;
hence contradiction by A3,A99,A123;
end;
suppose
A124: y = 31;
992 = 30*33+2;
hence contradiction by A3,A99,A124,NAT_4:9;
end;
suppose
A125: y = 32;
1056 = 30*35+6;
hence contradiction by A3,A99,A125,NAT_4:9;
end;
suppose
A126: y = 33;
1122 = 30*37+12;
hence contradiction by A3,A99,A126,NAT_4:9;
end;
suppose
A127: y = 34;
5 divides 5*7;
hence contradiction by A3,A99,A127;
end;
end;
suppose
A128: x = 6;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A128,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A128,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A128,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A128,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A128;
end;
suppose y = 6;
hence contradiction by A3,A128;
end;
suppose y = 7;
hence contradiction by A3,A128;
end;
suppose
A129: y = 8;
72 = 42*1+30;
hence contradiction by A3,A128,A129,NAT_4:9;
end;
suppose
A130: y = 9;
90 = 42*2+6;
hence contradiction by A3,A128,A130,NAT_4:9;
end;
suppose
A131: y = 10;
110 = 42*2+26;
hence contradiction by A3,A128,A131,NAT_4:9;
end;
suppose
A132: y = 11;
6 divides 6*2;
hence contradiction by A3,A128,A132;
end;
suppose
A133: y = 12;
6 divides 6*2;
hence contradiction by A3,A128,A133;
end;
suppose
A134: y = 13;
7 divides 7*2;
hence contradiction by A3,A128,A134;
end;
suppose
A135: y = 14;
7 divides 7*2;
hence contradiction by A3,A128,A135;
end;
suppose
A136: y = 15;
240 = 42*5+30;
hence contradiction by A3,A128,A136,NAT_4:9;
end;
suppose
A137: y = 16;
272 = 42*6+20;
hence contradiction by A3,A128,A137,NAT_4:9;
end;
suppose
A138: y = 17;
6 divides 6*3;
hence contradiction by A3,A128,A138;
end;
suppose
A139: y = 18;
6 divides 6*3;
hence contradiction by A3,A128,A139;
end;
suppose
A140: y = 19;
380 = 42*9+2;
hence contradiction by A3,A128,A140,NAT_4:9;
end;
suppose
A141: y = 20;
7 divides 7*3;
hence contradiction by A3,A128,A141;
end;
suppose
A142: y = 21;
7 divides 7*3;
hence contradiction by A3,A128,A142;
end;
suppose
A143: y = 22;
506 = 42*12+2;
hence contradiction by A3,A128,A143,NAT_4:9;
end;
suppose
A144: y = 23;
6 divides 6*4;
hence contradiction by A3,A128,A144;
end;
suppose
A145: y = 24;
6 divides 6*4;
hence contradiction by A3,A128,A145;
end;
suppose
A146: y = 25;
650 = 42*15+20;
hence contradiction by A3,A128,A146,NAT_4:9;
end;
suppose
A147: y = 26;
702 = 42*16+30;
hence contradiction by A3,A128,A147,NAT_4:9;
end;
suppose
A148: y = 27;
7 divides 7*4;
hence contradiction by A3,A128,A148;
end;
suppose
A149: y = 28;
7 divides 7*4;
hence contradiction by A3,A128,A149;
end;
suppose
A150: y = 29;
6 divides 6*5;
hence contradiction by A3,A128,A150;
end;
suppose
A151: y = 30;
6 divides 6*5;
hence contradiction by A3,A128,A151;
end;
suppose
A152: y = 31;
992 = 42*23+26;
hence contradiction by A3,A128,A152,NAT_4:9;
end;
suppose
A153: y = 32;
1056 = 42*25+6;
hence contradiction by A3,A128,A153,NAT_4:9;
end;
suppose
A154: y = 33;
1122 = 42*26+30;
hence contradiction by A3,A128,A154,NAT_4:9;
end;
suppose
A155: y = 34;
7 divides 7*5;
hence contradiction by A3,A128,A155;
end;
end;
suppose
A156: x = 7;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A156,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A156,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A156,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A156,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A156,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A156;
end;
suppose y = 7;
hence contradiction by A3,A156;
end;
suppose y = 8;
hence contradiction by A3,A156;
end;
suppose
A157: y = 9;
90 = 56*1+34;
hence contradiction by A3,A156,A157,NAT_4:9;
end;
suppose
A158: y = 10;
110 = 56*1+54;
hence contradiction by A3,A156,A158,NAT_4:9;
end;
suppose
A159: y = 11;
132 = 56*2+20;
hence contradiction by A3,A156,A159,NAT_4:9;
end;
suppose
A160: y = 12;
156 = 56*2+44;
hence contradiction by A3,A156,A160,NAT_4:9;
end;
suppose
A161: y = 13;
7 divides 7*2;
hence contradiction by A3,A156,A161;
end;
suppose
A162: y = 14;
7 divides 7*2;
hence contradiction by A3,A156,A162;
end;
suppose
A163: y = 15;
8 divides 8*2;
hence contradiction by A3,A156,A163;
end;
suppose
A164: y = 16;
8 divides 8*2;
hence contradiction by A3,A156,A164;
end;
suppose
A165: y = 17;
306 = 56*5+26;
hence contradiction by A3,A156,A165,NAT_4:9;
end;
suppose
A166: y = 18;
342 = 56*6+6;
hence contradiction by A3,A156,A166,NAT_4:9;
end;
suppose
A167: y = 19;
380 = 56*6+44;
hence contradiction by A3,A156,A167,NAT_4:9;
end;
suppose
A168: y = 20;
7 divides 7*3;
hence contradiction by A3,A156,A168;
end;
suppose
A169: y = 21;
7 divides 7*3;
hence contradiction by A3,A156,A169;
end;
suppose
A170: y = 22;
506 = 56*9+2;
hence contradiction by A3,A156,A170,NAT_4:9;
end;
suppose
A171: y = 23;
8 divides 8*3;
hence contradiction by A3,A156,A171;
end;
suppose
A172: y = 24;
8 divides 8*3;
hence contradiction by A3,A156,A172;
end;
suppose
A173: y = 25;
650 = 56*11+34;
hence contradiction by A3,A156,A173,NAT_4:9;
end;
suppose
A174: y = 26;
702 = 56*12+30;
hence contradiction by A3,A156,A174,NAT_4:9;
end;
suppose
A175: y = 27;
7 divides 7*4;
hence contradiction by A3,A156,A175;
end;
suppose
A176: y = 28;
7 divides 7*4;
hence contradiction by A3,A156,A176;
end;
suppose
A177: y = 29;
870 = 56*15+30;
hence contradiction by A3,A156,A177,NAT_4:9;
end;
suppose
A178: y = 30;
930 = 56*16+34;
hence contradiction by A3,A156,A178,NAT_4:9;
end;
suppose
A179: y = 31;
8 divides 8*4;
hence contradiction by A3,A156,A179;
end;
suppose
A180: y = 32;
8 divides 8*4;
hence contradiction by A3,A156,A180;
end;
suppose
A181: y = 33;
1122 = 56*20+2;
hence contradiction by A3,A156,A181,NAT_4:9;
end;
suppose
A182: y = 34;
7 divides 7*5;
hence contradiction by A3,A156,A182;
end;
end;
suppose
A183: x = 8;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A183,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A183;
end;
suppose y = 8;
hence contradiction by A3,A183;
end;
suppose y = 9;
hence contradiction by A3,A183;
end;
suppose
A184: y = 10;
110 = 72*1+38;
hence contradiction by A3,A183,A184,NAT_4:9;
end;
suppose
A185: y = 11;
132 = 72*1+60;
hence contradiction by A3,A183,A185,NAT_4:9;
end;
suppose
A186: y = 12;
156 = 72*2+12;
hence contradiction by A3,A183,A186,NAT_4:9;
end;
suppose
A187: y = 13;
182 = 72*2+38;
hence contradiction by A3,A183,A187,NAT_4:9;
end;
suppose
A188: y = 14;
210 = 72*2+66;
hence contradiction by A3,A183,A188,NAT_4:9;
end;
suppose
A189: y = 15;
8 divides 8*2;
hence contradiction by A3,A183,A189;
end;
suppose
A190: y = 16;
8 divides 8*2;
hence contradiction by A3,A183,A190;
end;
suppose
A191: y = 17;
9 divides 9*2;
hence contradiction by A3,A183,A191;
end;
suppose
A192: y = 18;
9 divides 9*2;
hence contradiction by A3,A183,A192;
end;
suppose
A193: y = 19;
380 = 72*5+20;
hence contradiction by A3,A183,A193,NAT_4:9;
end;
suppose
A194: y = 20;
420 = 72*5+60;
hence contradiction by A3,A183,A194,NAT_4:9;
end;
suppose
A195: y = 21;
462 = 72*6+30;
hence contradiction by A3,A183,A195,NAT_4:9;
end;
suppose
A196: y = 22;
506 = 72*7+2;
hence contradiction by A3,A183,A196,NAT_4:9;
end;
suppose
A197: y = 23;
8 divides 8*3;
hence contradiction by A3,A183,A197;
end;
suppose
A198: y = 24;
8 divides 8*3;
hence contradiction by A3,A183,A198;
end;
suppose
A199: y = 25;
650 = 72*9+2;
hence contradiction by A3,A183,A199,NAT_4:9;
end;
suppose
A200: y = 26;
9 divides 9*3;
hence contradiction by A3,A183,A200;
end;
suppose
A201: y = 27;
9 divides 9*3;
hence contradiction by A3,A183,A201;
end;
suppose
A202: y = 28;
812 = 72*11+20;
hence contradiction by A3,A183,A202,NAT_4:9;
end;
suppose
A203: y = 29;
870 = 72*12+6;
hence contradiction by A3,A183,A203,NAT_4:9;
end;
suppose
A204: y = 30;
930 = 72*12+66;
hence contradiction by A3,A183,A204,NAT_4:9;
end;
suppose
A205: y = 31;
8 divides 8*4;
hence contradiction by A3,A183,A205;
end;
suppose
A206: y = 32;
8 divides 8*4;
hence contradiction by A3,A183,A206;
end;
suppose
A207: y = 33;
1122 = 72*15+42;
hence contradiction by A3,A183,A207,NAT_4:9;
end;
suppose
A208: y = 34;
1190 = 72*16+38;
hence contradiction by A3,A183,A208,NAT_4:9;
end;
end;
suppose
A209: x = 9;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A209,NAT_D:7;
end;
suppose y = 8;
hence contradiction by A3,A209;
end;
suppose y = 9;
hence contradiction by A3,A209;
end;
suppose y = 10;
hence contradiction by A3,A209;
end;
suppose
A210: y = 11;
132 = 90*1+42;
hence contradiction by A3,A209,A210,NAT_4:9;
end;
suppose
A211: y = 12;
156 = 90*1+66;
hence contradiction by A3,A209,A211,NAT_4:9;
end;
suppose
A212: y = 13;
182 = 90*2+2;
hence contradiction by A3,A209,A212,NAT_4:9;
end;
suppose
A213: y = 14;
210 = 90*2+30;
hence contradiction by A3,A209,A213,NAT_4:9;
end;
suppose
A214: y = 15;
240 = 90*2+60;
hence contradiction by A3,A209,A214,NAT_4:9;
end;
suppose
A215: y = 16;
272 = 90*3+2;
hence contradiction by A3,A209,A215,NAT_4:9;
end;
suppose
A216: y = 17;
9 divides 9*2;
hence contradiction by A3,A209,A216;
end;
suppose
A217: y = 18;
9 divides 9*2;
hence contradiction by A3,A209,A217;
end;
suppose
A218: y = 19;
10 divides 10*2;
hence contradiction by A3,A209,A218;
end;
suppose
A219: y = 20;
10 divides 10*2;
hence contradiction by A3,A209,A219;
end;
suppose
A220: y = 21;
462 = 90*5+12;
hence contradiction by A3,A209,A220,NAT_4:9;
end;
suppose
A221: y = 22;
506 = 90*5+56;
hence contradiction by A3,A209,A221,NAT_4:9;
end;
suppose
A222: y = 23;
552 = 90*6+12;
hence contradiction by A3,A209,A222,NAT_4:9;
end;
suppose
A223: y = 24;
600 = 90*6+60;
hence contradiction by A3,A209,A223,NAT_4:9;
end;
suppose
A224: y = 25;
650 = 90*7+20;
hence contradiction by A3,A209,A224,NAT_4:9;
end;
suppose
A225: y = 26;
9 divides 9*3;
hence contradiction by A3,A209,A225;
end;
suppose
A226: y = 27;
9 divides 9*3;
hence contradiction by A3,A209,A226;
end;
suppose
A227: y = 28;
812 = 90*9+2;
hence contradiction by A3,A209,A227,NAT_4:9;
end;
suppose
A228: y = 29;
10 divides 10*3;
hence contradiction by A3,A209,A228;
end;
suppose
A229: y = 30;
10 divides 10*3;
hence contradiction by A3,A209,A229;
end;
suppose
A230: y = 31;
992 = 90*11+2;
hence contradiction by A3,A209,A230,NAT_4:9;
end;
suppose
A231: y = 32;
1056 = 90*11+66;
hence contradiction by A3,A209,A231,NAT_4:9;
end;
suppose
A232: y = 33;
1122 = 90*12+42;
hence contradiction by A3,A209,A232,NAT_4:9;
end;
suppose
A233: y = 34;
1190 = 90*13+20;
hence contradiction by A3,A209,A233,NAT_4:9;
end;
end;
suppose
A234: x = 10;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 8;
hence contradiction by A3,A234,NAT_D:7;
end;
suppose y = 9;
hence contradiction by A3,A234;
end;
suppose y = 10;
hence contradiction by A3,A234;
end;
suppose y = 11;
hence contradiction by A3,A234;
end;
suppose
A235: y = 12;
156 = 110*1+46;
hence contradiction by A3,A234,A235,NAT_4:9;
end;
suppose
A236: y = 13;
182 = 110*1+72;
hence contradiction by A3,A234,A236,NAT_4:9;
end;
suppose
A237: y = 14;
210 = 110*1+100;
hence contradiction by A3,A234,A237,NAT_4:9;
end;
suppose
A238: y = 15;
240 = 110*2+20;
hence contradiction by A3,A234,A238,NAT_4:9;
end;
suppose
A239: y = 16;
272 = 110*2+52;
hence contradiction by A3,A234,A239,NAT_4:9;
end;
suppose
A240: y = 17;
306 = 110*2+86;
hence contradiction by A3,A234,A240,NAT_4:9;
end;
suppose
A241: y = 18;
342 = 110*3+12;
hence contradiction by A3,A234,A241,NAT_4:9;
end;
suppose
A242: y = 19;
10 divides 10*2;
hence contradiction by A3,A234,A242;
end;
suppose
A243: y = 20;
10 divides 10*2;
hence contradiction by A3,A234,A243;
end;
suppose
A244: y = 21;
11 divides 11*2;
hence contradiction by A3,A234,A244;
end;
suppose
A245: y = 22;
11 divides 11*2;
hence contradiction by A3,A234,A245;
end;
suppose
A246: y = 23;
552 = 110*5+2;
hence contradiction by A3,A234,A246,NAT_4:9;
end;
suppose
A247: y = 24;
600 = 110*5+50;
hence contradiction by A3,A234,A247,NAT_4:9;
end;
suppose
A248: y = 25;
650 = 110*5+100;
hence contradiction by A3,A234,A248,NAT_4:9;
end;
suppose
A249: y = 26;
702 = 110*6+42;
hence contradiction by A3,A234,A249,NAT_4:9;
end;
suppose
A250: y = 27;
756 = 110*6+96;
hence contradiction by A3,A234,A250,NAT_4:9;
end;
suppose
A251: y = 28;
812 = 110*7+42;
hence contradiction by A3,A234,A251,NAT_4:9;
end;
suppose
A252: y = 29;
10 divides 10*3;
hence contradiction by A3,A234,A252;
end;
suppose
A253: y = 30;
10 divides 10*3;
hence contradiction by A3,A234,A253;
end;
suppose
A254: y = 31;
992 = 110*9+2;
hence contradiction by A3,A234,A254,NAT_4:9;
end;
suppose
A255: y = 32;
11 divides 11*3;
hence contradiction by A3,A234,A255;
end;
suppose
A256: y = 33;
11 divides 11*3;
hence contradiction by A3,A234,A256;
end;
suppose
A257: y = 34;
1190 = 110*10+90;
hence contradiction by A3,A234,A257,NAT_4:9;
end;
end;
suppose
A258: x = 11;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 8;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 9;
hence contradiction by A3,A258,NAT_D:7;
end;
suppose y = 10;
hence contradiction by A3,A258;
end;
suppose y = 11;
hence contradiction by A3,A258;
end;
suppose y = 12;
hence contradiction by A3,A258;
end;
suppose
A259: y = 13;
182 = 132*1+50;
hence contradiction by A3,A258,A259,NAT_4:9;
end;
suppose
A260: y = 14;
210 = 132*1+78;
hence contradiction by A3,A258,A260,NAT_4:9;
end;
suppose
A261: y = 15;
240 = 132*1+108;
hence contradiction by A3,A258,A261,NAT_4:9;
end;
suppose
A262: y = 16;
272 = 132*2+8;
hence contradiction by A3,A258,A262,NAT_4:9;
end;
suppose
A263: y = 17;
306 = 132*2+42;
hence contradiction by A3,A258,A263,NAT_4:9;
end;
suppose
A264: y = 18;
342 = 132*2+78;
hence contradiction by A3,A258,A264,NAT_4:9;
end;
suppose
A265: y = 19;
380 = 132*2+116;
hence contradiction by A3,A258,A265,NAT_4:9;
end;
suppose
A266: y = 20;
420 = 132*3+24;
hence contradiction by A3,A258,A266,NAT_4:9;
end;
suppose
A267: y = 21;
11 divides 11*2;
hence contradiction by A3,A258,A267;
end;
suppose
A268: y = 22;
11 divides 11*2;
hence contradiction by A3,A258,A268;
end;
suppose
A269: y = 23;
12 divides 12*2;
hence contradiction by A3,A258,A269;
end;
suppose
A270: y = 24;
12 divides 12*2;
hence contradiction by A3,A258,A270;
end;
suppose
A271: y = 25;
650 = 132*4+122;
hence contradiction by A3,A258,A271,NAT_4:9;
end;
suppose
A272: y = 26;
702 = 132*5+42;
hence contradiction by A3,A258,A272,NAT_4:9;
end;
suppose
A273: y = 27;
756 = 132*5+96;
hence contradiction by A3,A258,A273,NAT_4:9;
end;
suppose
A274: y = 28;
812 = 132*6+20;
hence contradiction by A3,A258,A274,NAT_4:9;
end;
suppose
A275: y = 29;
870 = 132*6+78;
hence contradiction by A3,A258,A275,NAT_4:9;
end;
suppose
A276: y = 30;
930 = 132*7+6;
hence contradiction by A3,A258,A276,NAT_4:9;
end;
suppose
A277: y = 31;
992 = 132*7+68;
hence contradiction by A3,A258,A277,NAT_4:9;
end;
suppose
A278: y = 32;
11 divides 11*3;
hence contradiction by A3,A258,A278;
end;
suppose
A279: y = 33;
11 divides 11*3;
hence contradiction by A3,A258,A279;
end;
suppose
A280: y = 34;
1190 = 132*9+2;
hence contradiction by A3,A258,A280,NAT_4:9;
end;
end;
suppose
A281: x = 12;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 8;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 9;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 10;
hence contradiction by A3,A281,NAT_D:7;
end;
suppose y = 11;
hence contradiction by A3,A281;
end;
suppose y = 12;
hence contradiction by A3,A281;
end;
suppose y = 13;
hence contradiction by A3,A281;
end;
suppose
A282: y = 14;
210 = 156*1+54;
hence contradiction by A3,A281,A282,NAT_4:9;
end;
suppose
A283: y = 15;
240 = 156*1+84;
hence contradiction by A3,A281,A283,NAT_4:9;
end;
suppose
A284: y = 16;
272 = 156*1+116;
hence contradiction by A3,A281,A284,NAT_4:9;
end;
suppose
A285: y = 17;
306 = 156*1+150;
hence contradiction by A3,A281,A285,NAT_4:9;
end;
suppose
A286: y = 18;
342 = 156*2+30;
hence contradiction by A3,A281,A286,NAT_4:9;
end;
suppose
A287: y = 19;
380 = 156*2+68;
hence contradiction by A3,A281,A287,NAT_4:9;
end;
suppose
A288: y = 20;
420 = 156*2+108;
hence contradiction by A3,A281,A288,NAT_4:9;
end;
suppose
A289: y = 21;
462 = 156*2+150;
hence contradiction by A3,A281,A289,NAT_4:9;
end;
suppose
A290: y = 22;
506 = 156*3+38;
hence contradiction by A3,A281,A290,NAT_4:9;
end;
suppose
A291: y = 23;
12 divides 12*2;
hence contradiction by A3,A281,A291;
end;
suppose
A292: y = 24;
12 divides 12*2;
hence contradiction by A3,A281,A292;
end;
suppose
A293: y = 25;
13 divides 13*2;
hence contradiction by A3,A281,A293;
end;
suppose
A294: y = 26;
13 divides 13*2;
hence contradiction by A3,A281,A294;
end;
suppose
A295: y = 27;
756 = 156*4+132;
hence contradiction by A3,A281,A295,NAT_4:9;
end;
suppose
A296: y = 28;
812 = 156*5+32;
hence contradiction by A3,A281,A296,NAT_4:9;
end;
suppose
A297: y = 29;
870 = 156*5+90;
hence contradiction by A3,A281,A297,NAT_4:9;
end;
suppose
A298: y = 30;
930 = 156*5+150;
hence contradiction by A3,A281,A298,NAT_4:9;
end;
suppose
A299: y = 31;
992 = 156*6+56;
hence contradiction by A3,A281,A299,NAT_4:9;
end;
suppose
A300: y = 32;
1056 = 156*6+120;
hence contradiction by A3,A281,A300,NAT_4:9;
end;
suppose
A301: y = 33;
1122 = 156*7+30;
hence contradiction by A3,A281,A301,NAT_4:9;
end;
suppose
A302: y = 34;
1190 = 156*7+98;
hence contradiction by A3,A281,A302,NAT_4:9;
end;
end;
suppose
A303: x = 13;
per cases by A5;
suppose y = 0;
hence contradiction by A3,NAT_D:6;
end;
suppose y = 1;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 2;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 3;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 4;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 5;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 6;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 7;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 8;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 9;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 10;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 11;
hence contradiction by A3,A303,NAT_D:7;
end;
suppose y = 12;
hence contradiction by A3,A303;
end;
suppose y = 13;
hence contradiction by A3,A303;
end;
suppose y = 14;
hence contradiction by A3,A303;
end;
suppose
A304: y = 15;
240 = 182*1+58;
hence contradiction by A3,A303,A304,NAT_4:9;
end;
suppose
A305: y = 16;
272 = 182*1+90;
hence contradiction by A3,A303,A305,NAT_4:9;
end;
suppose
A306: y = 17;
306 = 182*1+124;
hence contradiction by A3,A303,A306,NAT_4:9;
end;
suppose
A307: y = 18;
342 = 182*1+160;
hence contradiction by A3,A303,A307,NAT_4:9;
end;
suppose
A308: y = 19;
380 = 182*2+16;
hence contradiction by A3,A303,A308,NAT_4:9;
end;
suppose
A309: y = 20;
420 = 182*2+56;
hence contradiction by A3,A303,A309,NAT_4:9;
end;
suppose
A310: y = 21;
462 = 182*2+98;
hence contradiction by A3,A303,A310,NAT_4:9;
end;
suppose
A311: y = 22;
506 = 182*2+142;
hence contradiction by A3,A303,A311,NAT_4:9;
end;
suppose
A312: y = 23;
552 = 182*3+6;
hence contradiction by A3,A303,A312,NAT_4:9;
end;
suppose
A313: y = 24;
600 = 182*3+54;
hence contradiction by A3,A303,A313,NAT_4:9;
end;
suppose
A314: y = 25;
13 divides 13*2;
hence contradiction by A3,A303,A314;
end;
suppose
A315: y = 26;
13 divides 13*2;
hence contradiction by A3,A303,A315;
end;
suppose
A316: y = 27;
14 divides 14*2;
hence contradiction by A3,A303,A316;
end;
suppose
A317: y = 28;
14 divides 14*2;
hence contradiction by A3,A303,A317;
end;
suppose
A318: y = 29;
870 = 182*4+142;
hence contradiction by A3,A303,A318,NAT_4:9;
end;
suppose
A319: y = 30;
930 = 182*5+20;
hence contradiction by A3,A303,A319,NAT_4:9;
end;
suppose
A320: y = 31;
992 = 182*5+82;
hence contradiction by A3,A303,A320,NAT_4:9;
end;
suppose
A321: y = 32;
1056 = 182*5+146;
hence contradiction by A3,A303,A321,NAT_4:9;
end;
suppose
A322: y = 33;
1122 = 182*6+30;
hence contradiction by A3,A303,A322,NAT_4:9;
end;
suppose
A323: y = 34;
1190 = 182*6+98;
hence contradiction by A3,A303,A323,NAT_4:9;
end;
end;
end;
begin :: Problem 40
theorem Th19:
a divides b implies n|^a - 1 divides n|^b - 1
proof
given m being Nat such that
A1: b = a*m;
n|^a - 1 divides n|^a|^m - 1|^m by NEWTON01:33;
hence thesis by A1,NEWTON:9;
end;
:: Problem 40
theorem
2|^(2|^n)+1 divides 2|^(2|^(2|^n)+1)-2
proof
set A = 2|^(2|^n);
set F = A+1;
set G = 2|^(2|^(n+1))-1;
set H = 2|^A-1;
set I = 2|^(A+1);
n+1 <= 2|^n by NEWTON:85;
then
A1: G divides H by Th19,NEWTON:89;
(A+1)*(A-1) = A|^2-1|^2 by NEWTON01:1
.= 2|^(2|^n*2|^1)-1 by NEWTON:9
.= 2|^(2|^(n+1))-1 by NEWTON:8;
then F divides G;
then
A2: F divides H by A1,INT_2:9;
2|^1*2|^A = I by NEWTON:8;
then 2*H = I-2;
then H divides I-2;
hence F divides 2|^F-2 by A2,INT_2:9;
end;
begin :: Problem 47
theorem Th21:
n divides 4 implies n = 1 or n = 2 or n = 4
proof
assume
A1: n divides 4;
then n <= 4 by INT_2:27;
then
A2: n = 0 or ... or n = 4;
now
(3*1+1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24;
hence not 3 divides 4;
end;
hence thesis by A1,A2;
end;
:: Problem 47
theorem
n > 6 implies ex a,b being Nat st a > 1 & b > 1 & n = a+b & a,b are_coprime
proof
assume
A1: n > 6;
per cases;
suppose
A2: n is odd;
2 = 2*1;
then reconsider a = 2 as even Nat;
reconsider b = n-a as Element of NAT by A1,XXREAL_0:2,INT_1:5;
take a, b;
thus a > 1;
n-a > 6-a by A1,XREAL_1:14;
hence b > 1 by XXREAL_0:2;
thus n = a+b;
2 = 2|^1;
hence thesis by A2,NAT_5:3;
end;
suppose
A3: n is even;
consider k such that
A4: n = 4*k or n = 4*k+1 or n = 4*k+2 or n = 4*k+3 by NUMBER02:24;
4*k+1 = 2*(2*k)+1 & 4*k+3 = 2*(2*k+1)+1;
then per cases by A3,A4;
suppose
A5: n = 4*k;
A6: now
assume 1 >= k;
then k = 0 or k = 1 by NAT_1:25;
hence contradiction by A1,A5;
end;
then
A7: 2*1 < 2*k by XREAL_1:68;
then reconsider a = 2*k-1 as odd Element of NAT by INT_1:5,XXREAL_0:2;
reconsider b = 2*k+1 as odd Element of NAT;
take a,b;
2*k-1 > 2-1 by A7,XREAL_1:9;
hence a > 1;
1+0 < 2*k+1 by A6,XREAL_1:8;
hence b > 1;
thus n = a+b by A5;
b - a = 2;
hence thesis by NUMBER03:31;
end;
suppose
A8: n = 4*k+2;
reconsider a = 2*k+2+1 as Nat;
4*k+2 > 4+2 by A1,A8;
then 2*(2*k) > 2*(2*1) by XREAL_1:6;
then
A9: 2*k > 2*1 by XREAL_1:64;
then
A10: 1 <= 2*k by XXREAL_0:2;
then reconsider b = 2*k-1 as Element of NAT by INT_1:5;
take a,b;
2*k+3 > 2*k+0 by XREAL_1:8;
hence a > 1 by A10,XXREAL_0:2;
2*k-1 > 1+1-1 by A9,XREAL_1:9;
hence b > 1;
thus n = a+b by A8;
A11: 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
A12: d divides a and
A13: d divides b;
d divides a-b by A12,A13,INT_5:1;
then d = 1 or d = 2*1 or d = 2*2 by Th21;
hence thesis by A12;
end;
hence a gcd b = 1 by A11,NAT_D:def 5;
end;
end;
end;
begin :: Problem 76
definition
let n be Nat;
pred n satisfies_Sierpinski_problem_76a means
for x being Nat st n < x < n+10 holds x is non prime;
end;
definition
let m be Nat;
pred m satisfies_Sierpinski_problem_76b means
for x being Nat st 10*m < x < 10*(m+1) holds x is non prime;
end;
theorem
113 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 113 < x < 113+10;
then 113 < x < 122+1;
then 113+1 <= x <= 122 by NAT_1:13;
then x = 114 or ... or x = 122;
hence thesis by XPRIMES0:114,115,116,117,118,119,120,121,122;
end;
theorem
114 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 114 < x < 114+10;
then 114 < x < 123+1;
then 114+1 <= x <= 123 by NAT_1:13;
then x = 115 or ... or x = 123;
hence thesis by XPRIMES0:115,116,117,118,119,120,121,122,123;
end;
theorem
115 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 115 < x < 115+10;
then 115 < x < 124+1;
then 115+1 <= x <= 124 by NAT_1:13;
then x = 116 or ... or x = 124;
hence thesis by XPRIMES0:116,117,118,119,120,121,122,123,124;
end;
theorem
116 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 116 < x < 116+10;
then 116 < x < 125+1;
then 116+1 <= x <= 125 by NAT_1:13;
then x = 117 or ... or x = 125;
hence thesis by XPRIMES0:117,118,119,120,121,122,123,124,125;
end;
theorem
117 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 117 < x < 117+10;
then 117 < x < 126+1;
then 117+1 <= x <= 126 by NAT_1:13;
then x = 118 or ... or x = 126;
hence thesis by XPRIMES0:118,119,120,121,122,123,124,125,126;
end;
theorem
139 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 139 < x < 139+10;
then 139 < x < 148+1;
then 139+1 <= x <= 148 by NAT_1:13;
then x = 140 or ... or x = 148;
hence thesis by XPRIMES0:140,141,142,143,144,145,146,147,148;
end;
theorem
181 satisfies_Sierpinski_problem_76a
proof
let x be Nat;
assume 181 < x < 181+10;
then 181 < x < 190+1;
then 181+1 <= x <= 190 by NAT_1:13;
then x = 182 or ... or x = 190;
hence thesis by XPRIMES0:182,183,184,185,186,187,188,189,190;
end;
:: Problem 76 a
theorem
n satisfies_Sierpinski_problem_76a & n <= 181 implies
n in {113,114,115,116,117,139,181}
proof
assume
A1: n satisfies_Sierpinski_problem_76a;
assume
A2: n <= 181;
per cases;
suppose n <= 99;
then n = 0 or ... or n = 99;
hence thesis by A1,XPRIMES1:2,11,19,23,31,37,43,47,53,59,67,73,79,83,89,
97,101;
end;
suppose n > 99;
then n >= 99+1 & n <= 181 by A2,NAT_1:13;
then n = 100 or ... or n = 181;
then n = 113 or n = 114 or n = 115 or n = 116 or n = 117 or
n = 139 or n = 181
by A1,XPRIMES1:107,113,127,131,139,149,157,163,167,173,181;
hence thesis by ENUMSET1:def 5;
end;
end;
theorem
20 satisfies_Sierpinski_problem_76b
proof
let x be Nat;
assume 10*20 < x < 10*(20+1);
then 200 < x < 209+1;
then 200+1 <= x <= 209 by NAT_1:13;
then x = 201 or ... or x = 209;
hence thesis by XPRIMES0:201,202,203,204,205,206,207,208,209;
end;
theorem
32 satisfies_Sierpinski_problem_76b
proof
let x be Nat;
assume 10*32 < x < 10*(32+1);
then 320 < x < 329+1;
then 320+1 <= x <= 329 by NAT_1:13;
then x = 321 or ... or x = 329;
hence thesis by XPRIMES0:321,322,323,324,325,326,327,328,329;
end;
theorem
51 satisfies_Sierpinski_problem_76b
proof
let x be Nat;
assume 10*51 < x < 10*(51+1);
then 510 < x < 519+1;
then 510+1 <= x <= 519 by NAT_1:13;
then x = 511 or ... or x = 519;
hence thesis by XPRIMES0:511,512,513,514,515,516,517,518,519;
end;
theorem
53 satisfies_Sierpinski_problem_76b
proof
let x be Nat;
assume 10*53 < x < 10*(53+1);
then 530 < x < 539+1;
then 530+1 <= x <= 539 by NAT_1:13;
then x = 531 or ... or x = 539;
hence thesis by XPRIMES0:531,532,533,534,535,536,537,538,539;
end;
theorem
62 satisfies_Sierpinski_problem_76b
proof
let x be Nat;
assume 10*62 < x < 10*(62+1);
then 620 < x < 629+1;
then 620+1 <= x <= 629 by NAT_1:13;
then x = 621 or ... or x = 629;
hence thesis by XPRIMES0:621,622,623,624,625,626,627,628,629;
end;
:: Problem 76 b
theorem
m satisfies_Sierpinski_problem_76b & m <= 62 implies m in {20,32,51,53,62}
proof
assume
A1: m satisfies_Sierpinski_problem_76b;
assume m <= 62;
then m = 0 or ... or m = 62;
then m = 20 or m = 32 or m = 51 or m = 53 or m = 62
by A1,XPRIMES1:2,13,23,31,41,53,61,71,83,97,101,113,127,131,149,151,163,
173,181,191,211,223,233,241,251,263,271,281,293,307,311,331,347,353,367,
373,383,397,401,419,421,431,443,457,461,479,487,491,503,521,541,557,563,
571,587,593,601,613;
hence thesis by ENUMSET1:def 3;
end;
begin :: Problem 79
theorem Th33:
c <> 0 & c < b implies not (a*b+c) / b is integer
proof
assume that
A1: c <> 0 and
A2: c < b;
A3: (a*b+c) mod b = c mod b by NAT_D:21;
c mod b = c by A2,NAT_D:24;
then not b divides a*b+c by A1,A3;
hence thesis by A2,WSIERP_1:17;
end;
Lm2:
not 5/4 is integer
proof
1*4+1 = 5;
hence thesis by Th33;
end;
theorem Th34:
not ex m,n being positive Nat st m^2 - n^2 = 1
proof
given m,n being positive Nat such that
A1: m^2 - n^2 = 1;
A2: now
assume m^2 <= n^2;
then m^2 - n^2 <= n^2 - n^2 by XREAL_1:9;
then m^2 - n^2 <= 0;
hence contradiction by A1;
end;
A3: sqrt(1+n*n) <= sqrt 1 + sqrt (n^2) by SQUARE_1:59;
sqrt(m^2) = m & sqrt(n^2) = n by SQUARE_1:def 2;
then m < 1+n or m = 1+n by A1,A3,XXREAL_0:1,SQUARE_1:18;
then per cases by NAT_1:13;
suppose m <= n;
hence thesis by A2,SQUARE_1:15;
end;
suppose m = 1+n;
then (1+n)^2 - n^2 = 1 by A1;
then 2*n = 0;
hence thesis;
end;
end;
theorem Th35:
not ex m,n being positive Nat st m^2 - n^2 = 4
proof
given m,n being positive Nat such that
A1: m^2 - n^2 = 4;
now
assume m^2 <= n^2;
then m^2 - n^2 <= n^2 - n^2 by XREAL_1:9;
then m^2 - n^2 <= 0;
hence contradiction by A1;
end;
then
A2: m > n by SQUARE_1:15;
per cases;
suppose m is even;
then consider a being Nat such that
A3: m = 2*a;
per cases;
suppose n is even;
then consider b being Nat such that
A4: n = 2*b;
4*a*a - 4*b*b = 4 by A1,A3,A4;
then
A5: a^2-b^2 = 1;
a is positive & b is positive by A3,A4;
hence thesis by A5,Th34;
end;
suppose n is odd;
then consider b being Nat such that
A6: n = 2*b+1 by ABIAN:9;
4*a*a - (4*b*b+4*b+1) = 4 by A1,A3,A6;
then a*a-b*b-b = 5/4;
hence contradiction by Lm2;
end;
end;
suppose m is odd;
then consider a being Nat such that
A7: m = 2*a+1 by ABIAN:9;
per cases;
suppose n is even;
then consider b being Nat such that
A8: n = 2*b;
4*a*a+4*a+1 - 4*b*b = 4 by A1,A7,A8;
then a*a+a-b*b = 3/4;
hence contradiction by NAT_D:33;
end;
suppose n is odd;
then consider b being Nat such that
A9: n = 2*b+1 by ABIAN:9;
A10: 4*a*a+4*a+1 - (4*b*b+4*b+1) = 4 by A1,A7,A9;
2*b+1-1 < 2*a+1-1 by A2,A7,A9,XREAL_1:9;
then
A11: b < a by XREAL_1:64;
then b^2 < a^2 by XREAL_1:96;
then a^2 - b^2 > b^2 - b^2 by XREAL_1:9;
then
A12: a^2 - b^2 >= 0+1 by INT_1:7;
a - b > b - b by A11,XREAL_1:9;
then a-b >= 0+1 by INT_1:7;
then a^2 - b^2 + (a-b) >= 1+1 by A12,XREAL_1:7;
hence contradiction by A10;
end;
end;
end;
theorem Th36:
(2*n+1)^2 mod 8 = 1
proof
defpred P[Nat] means (2*$1+1)^2 mod 8 = 1;
A1: P[0] by NAT_D:24;
A2: P[k] implies P[k+1]
proof
assume
A3: P[k];
thus (2*(k+1)+1)^2 mod 8 = (4*k^2+4*k+1 + 8*(k+1)) mod 8
.= (1 + (8*(k+1) mod 8)) mod 8 by A3,NAT_D:66
.= (1 + 0) mod 8
.= 1 by NAT_D:24;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th37:
n is odd implies n^2 mod 8 = 1
proof
assume n is odd;
then ex a st n = 2*a+1 by ABIAN:9;
hence thesis by Th36;
end;
Lm3:
p is odd implies 3 <= p
proof
1 < p by INT_2:def 4;
then 1+1 <= p by NAT_1:13;
then 2 = p or 2 < p by XXREAL_0:1;
then 2 = p or 2+1 <= p by NAT_1:13;
hence thesis;
end;
Lm4:
p is odd implies 9 <= p^2
proof
assume p is odd;
then 3 <= p by Lm3;
then 3*3 <= p*p by XREAL_1:66;
hence thesis;
end;
theorem Th38:
for q,s,t being Prime st q^2 = s^2 + t^2 holds
s is even & t is odd or s is odd & t is even
proof
let q,s,t be Prime such that
A1: q^2 = s^2 + t^2;
assume s is odd or t is even;
then per cases;
suppose
A2: s is odd;
now
assume
A3: t is odd;
then q is even by A1,A2;
then
A4: q = 2 by LAGRA4SQ:13;
9 <= s^2 & 9 <= t^2 by A2,A3,Lm4;
then 9+9 <= s^2 + t^2 by XREAL_1:7;
hence contradiction by A1,A4;
end;
hence thesis by A2;
end;
suppose t is even;
then t = 2 by LAGRA4SQ:13;
then q^2 - s^2 = 4 by A1;
hence thesis by Th35;
end;
end;
theorem Th39:
not ex q,s,t being Prime st q^2 = s^2 + t^2
proof
given q,s,t being Prime such that
A1: q^2 = s^2 + t^2;
per cases by A1,Th38;
suppose that
A2: s is even and t is odd;
s = 2 by A2,LAGRA4SQ:13;
then q^2 - t^2 = 4 by A1;
hence thesis by Th35;
end;
suppose that s is odd and
A3: t is even;
t = 2 by A3,LAGRA4SQ:13;
then q^2 - s^2 = 4 by A1;
hence thesis by Th35;
end;
end;
theorem
for p,q,r,s,t being Prime st p^2 + q^2 = r^2 + s^2 + t^2 holds
p is even or q is even or r is even or s is even or t is even;
:: Problem 79
theorem
not ex p,q,r,s,t being Prime st p^2 + q^2 = r^2 + s^2 + t^2
proof
given p,q,r,s,t being Prime such that
A1: p^2 + q^2 = r^2 + s^2 + t^2;
A2: now
assume p = r;
then p^2 + q^2 = p^2 + (s^2 + t^2) by A1;
hence contradiction by Th39;
end;
A3: now
assume p = s;
then p^2 + q^2 = p^2 + (r^2 + t^2) by A1;
hence contradiction by Th39;
end;
A4: p <> t by A1,Th39;
A5: now
assume q = r;
then p^2 + q^2 = q^2 + (s^2 + t^2) by A1;
hence contradiction by Th39;
end;
A6: now
assume q = s;
then p^2 + q^2 = q^2 + (r^2 + t^2) by A1;
hence contradiction by Th39;
end;
A7: q <> t by A1,Th39;
A8: (p^2 + q^2) mod 8 = ((p^2 mod 8) + (q^2 mod 8)) mod 8 by NAT_D:66;
A9: (r^2 + s^2) mod 8 = ((r^2 mod 8) + (s^2 mod 8)) mod 8 by NAT_D:66;
A10: (r^2 + s^2 + t^2) mod 8 = ((r^2 + s^2) mod 8 + (t^2 mod 8)) mod 8
by NAT_D:66;
A11: 2^2 mod 8 = 4 by NAT_D:24;
per cases;
suppose p is even or q is even;
then
A12: p = 2 or q = 2 by LAGRA4SQ:13;
then
A13: r is odd by A2,A5,LAGRA4SQ:13;
then
A14: r^2 mod 8 = 1 by Th37;
A15: s is odd by A3,A6,A12,LAGRA4SQ:13;
then
A16: s^2 mod 8 = 1 by Th37;
A17: t is odd by A4,A7,A12,LAGRA4SQ:13;
then
A18: t^2 mod 8 = 1 by Th37;
A19: p is even implies q is odd by A1,A13,A15,A17;
A20: (p^2 + q^2) mod 8 = (1 + 4) mod 8 by A8,A12,A11,A19,Th37
.= 5 by NAT_D:24;
(r^2 + s^2 + t^2) mod 8 = (2+1) mod 8 by A9,A10,A16,A18,A14,NAT_D:24
.= 3 by NAT_D:24;
hence contradiction by A1,A20;
end;
suppose
A21: p is odd & q is odd;
then p^2 mod 8 = 1 & q^2 mod 8 = 1 by Th37;
then
A22: (p^2 + q^2) mod 8 = 2 by A8,NAT_D:24;
per cases by A1,A21;
suppose that
A23: r is even and
A24: s is odd;
t is odd by A1,A21,A23,A24;
then
A25: t^2 mod 8 = 1 by Th37;
A26: s^2 mod 8 = 1 by A24,Th37;
r = 2 by A23,LAGRA4SQ:13;
then (r^2 + s^2) mod 8 = 5 by A9,A11,A26,NAT_D:24;
hence thesis by A1,A22,A10,A25,NAT_D:24;
end;
suppose that
A27: r is even and
A28: t is even;
s is even by A1,A21,A27,A28;
then
A29: s = 2 by LAGRA4SQ:13;
A30: t = 2 by A28,LAGRA4SQ:13;
r = 2 by A27,LAGRA4SQ:13;
then (r^2 + s^2) mod 8 = 0 by A29,NAT_D:25;
hence thesis by A1,A22,A10,A30,NAT_D:24;
end;
suppose that
A31: s is even and
A32: t is odd;
r is odd by A1,A21,A31,A32;
then
A33: r^2 mod 8 = 1 by Th37;
A34: t^2 mod 8 = 1 by A32,Th37;
s = 2 by A31,LAGRA4SQ:13;
then (r^2 + s^2) mod 8 = 5 by A9,A11,A33,NAT_D:24;
hence thesis by A1,A22,A10,A34,NAT_D:24;
end;
suppose that
A35: s is even and
A36: r is even;
t is even by A1,A21,A35,A36;
then
A37: t = 2 by LAGRA4SQ:13;
A38: s = 2 by A35,LAGRA4SQ:13;
r = 2 by A36,LAGRA4SQ:13;
then (r^2 + s^2) mod 8 = 0 by A38,NAT_D:25;
hence thesis by A1,A22,A10,A37,NAT_D:24;
end;
suppose that
A39: t is even and
A40: r is odd;
s is odd by A1,A21,A39,A40;
then
A41: s^2 mod 8 = 1 by Th37;
A42: t = 2 by A39,LAGRA4SQ:13;
r^2 mod 8 = 1 by A40,Th37;
hence thesis by A1,A11,A22,A9,A10,A42,A41,NAT_D:24;
end;
suppose that
A43: t is even and
A44: s is even;
A45: t = 2 by A43,LAGRA4SQ:13;
A46: s = 2 by A44,LAGRA4SQ:13;
r is even by A1,A21,A43,A44;
then r = 2 by LAGRA4SQ:13;
then (r^2 + s^2) mod 8 = 0 by A46,NAT_D:25;
hence thesis by A1,A22,A10,A45,NAT_D:24;
end;
end;
end;