:: Elementary Number Theory Problems. Part {XIV} -- Diophantine Equations
:: by Artur Korni{\l}owicz
::
:: Received October 22, 2024
:: Copyright (c) 2024-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_3, XCMPLX_0,
CARD_1, INT_1, NEWTON, ARYTM_1, SUBSET_1, XBOOLE_0, TARSKI, ORDINAL1,
FINSET_1, ABIAN, MEMBERED, NUMBER02, PBOOLE, REAL_1, INT_2, SQUARE_1,
COMPLEX1, NUMBER09, ZFMISC_1, NUMBER03, NUMBER12, FINSEQ_1, INT_6,
CARD_3, VALUED_0, ORDINAL4, PARTFUN3, NAT_3, PRE_POLY, UPROOTS, RFINSEQ2,
ORDINAL2, FUNCT_7, CALCUL_2, VALUED_1, FIB_NUM2, RAT_1, EULER_1, NAT_LAT,
MCART_1, GROEB_1, NUMBER14;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, DOMAIN_1, ORDINAL1,
CARD_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, PBOOLE,
FINSET_1, MEMBERED, VALUED_0, VALUED_1, XREAL_0, INT_1, ABSVALUE, INT_2,
NAT_1, XXREAL_0, SQUARE_1, FINSEQ_1, PARTFUN3, FIB_NUM2, RVSUM_1,
RFINSEQ2, NEWTON, ABIAN, EULER_1, PRE_POLY, RAT_1, NAT_3, NAT_LAT, INT_6,
NUMBER02, NUMBER03, CALCUL_2, NUMBER09, NUMBER12;
constructors NAT_D, ABIAN, PEPIN, FIB_NUM2, NAT_3, NUMBER02, NUMBER03,
CLASSES1, PYTHTRIP, MOEBIUS1, RFINSEQ2, WELLORD2, NEWTON03, POWER,
DOMAIN_1, EC_PF_2, WSIERP_1, NUMBER09, INT_6, INT_7, CALCUL_2, NUMBER12,
NEWTON04, EULER_1, NAT_LAT;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, CARD_1, NEWTON, NEWTON02,
NEWTON03, ABIAN, NAT_6, JORDAN1D, WSIERP_1, NEWTON01, FINSEQ_1, FUNCT_1,
RELAT_1, XBOOLE_0, NAT_3, SUBSET_1, RAT_1, PYTHTRIP, VALUED_1, PARTFUN3,
FINSEQ_9, RAMSEY_1, SQUARE_1, NUMBER08, NUMBER09, FUZIMPL4, EULRPART,
INT_7, CALCUL_2, NUMBER04, FOMODEL0, INT_6, NAT_LAT, XTUPLE_0, NAT_5;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RELAT_1, MEMBERED, TARSKI, XBOOLE_0, FUNCT_1, INT_1, FINSEQ_1,
FUNCT_2, WELLORD2, NUMBER02, RVSUM_3, INT_6, EUCLID_7, PYTHTRIP;
equalities SQUARE_1, FINSEQ_1, XCMPLX_0, ORDINAL1, NUMBER12, CALCUL_2;
expansions INT_1, INT_2, ABIAN, NUMBER03, TARSKI, ZFMISC_1;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, CARD_2, XREAL_1, XXREAL_0, NAT_1,
FUNCT_1, PARTFUN1, TARSKI, NAT_5, CARD_1, ABIAN, XCMPLX_1, NUMBER05,
XTUPLE_0, XBOOLE_0, NUMBER04, COMPLEX1, EC_PF_2, NUMBER09, NEWTON05,
PYTHTRIP, NUMBER10, WSIERP_1, POLYEQ_5, NUMBER03, INT_4, NAT_3, INT_5,
NUMBER07, NAT_6, NUMBER12, FINSEQ_1, ABSVALUE, INT_6, NUMBER02, FINSEQ_3,
NAT_2, ZFMISC_1, RADIX_1, LIOUVIL2, XBOOLE_1, RELAT_1, NUMBERS, FINSEQ_2,
XPRIMES1, CLASSES1, RFINSEQ2, SUBSET_1, MEMBERED, NEWTON01, VALUED_0,
FUNCT_2, PRE_POLY, RAT_1, EUCLID_7, MOEBIUS1, EULER_1, INT_7, CALCUL_2,
XPRIMES0, ENUMSET1, VALUED_1, NUMBER06, NAGATA_2, INTEGRA3, NEWTON02,
PREPOWER, GR_CY_3, EULER_2, NAT_LAT, GROUP_22, TAYLOR_2, SQUARE_1,
NUMBER08, POWER, TOPREAL6, NEWTON03;
schemes NAT_1, PBOOLE, FINSEQ_1, FUNCT_2, RECDEF_1;
begin :: Preliminaries
Lm1: 2|^2 = 2*2 by NEWTON:81;
Lm2: 2|^3 = 2*2*2 by POLYEQ_5:2;
Lm3: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
Lm4: 2|^8 = 2*2*2*2*2*2*2*2 by NUMBER02:4;
Lm5: 1 mod 3 = 1 by NAT_D:24;
Lm6: (1*3+1) mod 3 = 1 mod 3 by NAT_D:21;
reserve a,b,c,h for Integer;
reserve k,m,n for Nat;
reserve i,j,z for Integer;
reserve p for Prime;
registration
let a,b,c be Integer;
reduce In([a,b,c],[:INT,INT,INT:]) to [a,b,c];
reducibility
proof
[In(a,INT),In(b,INT),In(c,INT)] in [:INT,INT,INT:];
hence thesis;
end;
end;
theorem
for a,b being Real holds 0 <= a & a < b implies |.a.| < |.b.|
proof
let a,b be Real;
assume
A1: 0 <= a;
then |.a.| = a by ABSVALUE:def 1;
hence thesis by A1,ABSVALUE:def 1;
end;
theorem Th2:
for a,b being Real holds b < a & a <= 0 implies |.a.| < |.b.|
proof
let a,b be Real;
assume that
A1: b < a and
A2: a <= 0;
A3: |.b.| = -b by A1,A2,ABSVALUE:def 1;
per cases by A2;
suppose a = 0;
hence thesis by A1;
end;
suppose a < 0;
then |.a.| = -a by ABSVALUE:def 1;
hence thesis by A1,A3,XREAL_1:24;
end;
end;
theorem
j <> 0 & z = i / j implies z divides i
proof
assume
A1: j <> 0 & z = i/j;
take j;
thus thesis by A1,XCMPLX_1:87;
end;
theorem Th4:
i divides j iff i divides |.j.|
proof
thus i divides j implies i divides |.j.|
proof
assume
A1: i divides j;
then consider a being Integer such that
A2: j = i * a;
per cases;
suppose j >= 0;
hence thesis by A1,ABSVALUE:def 1;
end;
suppose j < 0;
then
A3: -j = |.j.| by ABSVALUE:def 1;
take -a;
thus thesis by A2,A3;
end;
end;
assume
A4: i divides |.j.|;
then consider a being Integer such that
A5: |.j.| = i * a;
per cases;
suppose j >= 0;
hence thesis by A4,ABSVALUE:def 1;
end;
suppose j < 0;
then
A6: -j = |.j.| by ABSVALUE:def 1;
take -a;
thus thesis by A5,A6;
end;
end;
theorem
i divides j iff |.i.| divides j
proof
thus i divides j implies |.i.| divides j
proof
assume
A1: i divides j;
then consider a being Integer such that
A2: j = i * a;
per cases;
suppose i >= 0;
hence thesis by A1,ABSVALUE:def 1;
end;
suppose i < 0;
then
A3: -i = |.i.| by ABSVALUE:def 1;
take -a;
thus thesis by A2,A3;
end;
end;
assume
A4: |.i.| divides j;
then consider a being Integer such that
A5: j = |.i.| * a;
per cases;
suppose i >= 0;
hence thesis by A4,ABSVALUE:def 1;
end;
suppose i < 0;
then
A6: -i = |.i.| by ABSVALUE:def 1;
take -a;
thus thesis by A5,A6;
end;
end;
theorem Th6: ::: NAT_3:5 generalized
p divides i |^ n implies p divides i
proof
assume p divides i|^n;
then p divides |.i|^n.| by Th4;
then p divides |.i.| |^ n by TAYLOR_2:1;
then p divides |.i.| by NAT_3:5;
hence thesis by Th4;
end;
theorem Th7:
for m,n being Nat holds
m divides n*p implies m divides n or ex z being Nat st m = z*p & z divides n
proof
let m,n be Nat;
assume m divides n*p;
then consider a,b being Nat such that
A1: a divides n and
A2: b divides p and
A3: m = a * b by NUMBER12:14;
assume
A4: not m divides n;
per cases by A2,INT_2:def 4;
suppose b = 1;
hence thesis by A1,A3,A4;
end;
suppose
A5: b = p;
take a;
thus m = a*p by A3,A5;
thus a divides n by A1;
end;
end;
theorem Th8:
for m,n being Integer st
m divides n*p holds m divides n or ex z be Integer st m = z*p & z divides n
proof
let m,n be Integer;
assume m divides n*p;
then |.m.| divides |.n*p.| by INT_2:16;
then |.m.| divides |.n.|*|.p.| by COMPLEX1:65;
then per cases by Th7;
suppose |.m.| divides |.n.|;
hence thesis by INT_2:16;
end;
suppose ex z being Nat st |.m.| = z*|.p.| & z divides |.n.|;
then consider z being Nat such that
A1: |.m.| = z*|.p.| and
A2: z divides |.n.|;
now
per cases;
case
A3: m >= 0;
take z;
thus m = z*p by A1,A3,ABSVALUE:def 1;
thus z divides n by A2,Th4;
end;
case m < 0;
then
A4: |.m.| = -m by ABSVALUE:def 1;
take Z = -z;
thus m = -|.m.| by A4
.= Z*p by A1;
Z divides |.n.| by A2,INT_2:10;
hence Z divides n by Th4;
end;
end;
hence thesis;
end;
end;
theorem Th9:
i,j are_coprime iff |.i.|,|.j.| are_coprime by INT_2:34;
theorem Th10:
i,j are_coprime iff |.i.|,j are_coprime by INT_6:14;
theorem Th11:
i,j are_coprime iff -i,-j are_coprime
proof
(-i) gcd j = i gcd j & (-i) gcd j = (-i) gcd (-j) by NEWTON02:1;
hence thesis;
end;
theorem
i,j are_coprime iff -i,j are_coprime by NEWTON02:1;
theorem
for i,j,k being Integer st i <> 0 holds
i divides k & i*j,k are_coprime implies i = 1 or i = -1
proof
let i,j,k be Integer such that
A1: i <> 0 and
A2: i divides k;
A3: |.i*j.| = |.i.|*|.j.| by COMPLEX1:65;
assume i*j,k are_coprime;
then |.i*j.|,|.k.| are_coprime by INT_2:34;
then
A4: |.i.| = 1 by A1,A2,A3,INT_2:16,GROUP_22:2;
|.i.| = i or |.i.| = -i by COMPLEX1:71;
hence thesis by A4;
end;
theorem Th14:
for i,j,k being Integer st
i divides j & i,j are_coprime holds i = 1 or i = -1
proof
let i,j,k be Integer;
assume i divides j;
then
A1: |.i.| divides |.j.| by INT_2:16;
assume i,j are_coprime;
then |.i.|,|.j.| are_coprime by INT_2:34;
then
A2: |.i.| = 1 by A1,PYTHTRIP:def 1;
|.i.| = i or |.i.| = -i by COMPLEX1:71;
hence i = 1 or i = -1 by A2;
end;
theorem
i divides j implies j,0 are_congruent_mod i;
theorem Th16: ::: EULER_1:14
for a,b,c being Integer holds
a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime implies a*b,c are_coprime
proof
let a,b,c be Integer;
assume
A1: a <> 0 & c <> 0;
assume a,c are_coprime;
then
A2: |.a.|,|.c.| are_coprime by INT_2:34;
assume b,c are_coprime;
then |.b.|,|.c.| are_coprime by INT_2:34;
then
A3: |.a.|*|.b.|,|.c.| are_coprime by A1,A2,EULER_1:14;
|.a.|*|.b.| = |.a*b.| by COMPLEX1:65;
hence thesis by A3,INT_2:34;
end;
theorem
i,j are_congruent_mod 2 implies (i is odd iff j is odd);
theorem
i,j are_congruent_mod 2 implies (i is even iff j is even);
theorem Th19:
for i,j,k being Integer holds
i > 0 & j,k are_congruent_mod i implies (i divides j iff i divides k)
proof
let i,j,k be Integer;
assume
A1: i > 0;
assume j,k are_congruent_mod i;
then
A2: j mod i = k mod i by NAT_D:64;
thus i divides j implies i divides k
proof
assume i divides j;
then j mod i = 0;
hence thesis by A1,A2,INT_1:62;
end;
assume i divides k;
then k mod i = 0;
hence thesis by A1,A2,INT_1:62;
end;
theorem Th20:
for a,b being object, f being FinSequence holds
1 in dom (<*a,b*>^f) & 2 in dom (<*a,b*>^f)
proof
let a,b be object, f be FinSequence;
set g = <*a,b*>;
A1: dom g = {1,2} by FINSEQ_1:92;
A2: 1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
dom g c= dom(g^f) by FINSEQ_1:26;
hence thesis by A1,A2;
end;
theorem Th21:
for a,b being object, f being FinSequence holds
(<*a,b*>^f).1 = a & (<*a,b*>^f).2 = b
proof
let a,b be object, f be FinSequence;
set g = <*a,b*>;
set h = g^f;
dom g = {1,2} by FINSEQ_1:92;
then 1 in dom g & 2 in dom g by TARSKI:def 2;
then h.1 = g.1 & h.2 = g.2 by FINSEQ_1:def 7;
hence thesis;
end;
theorem Th22:
for a,b being object, f being FinSequence holds
n in dom f implies n+2 in dom (<*a,b*>^f)
proof
let a,b be object, f be FinSequence such that
A1: n in dom f;
A2: 1 <= n by A1,FINSEQ_3:25;
A3: n <= len f by A1,FINSEQ_3:25;
set g = <*a,b*>;
n+0 <= n+2 by XREAL_1:6;
then
A4: 1 <= n+2 by A2,XXREAL_0:2;
len g = 2 by FINSEQ_1:44;
then 2+n <= len g + len f by A3,XREAL_1:6;
then n+2 in Seg (len g + len f) by A4;
hence thesis by FINSEQ_1:def 7;
end;
theorem Th23:
for a,b being object, f being FinSequence st n in dom f holds
(<*a,b*>^f).(n+2) = f.n
proof
let a,b be object, f be FinSequence;
len <*a,b*> = 2 by FINSEQ_1:44;
hence thesis by FINSEQ_1:def 7;
end;
theorem
for f being decreasing real-valued FinSequence holds min_p(f) = len f
proof
let f be decreasing real-valued FinSequence;
per cases;
suppose len f = 0;
hence thesis by RFINSEQ2:def 2;
end;
suppose
A1: len f > 0;
then len f >= 0+1 by NAT_1:13;
then
A2: len f in dom f by FINSEQ_3:25;
A3: for i being Nat st i in dom f holds f.i >= f.len f
proof
let i be Nat such that
A4: i in dom f;
i <= len f by A4,FINSEQ_3:25;
then per cases by XXREAL_0:1;
suppose i = len f;
hence thesis;
end;
suppose i < len f;
hence thesis by A2,A4,VALUED_0:def 14;
end;
end;
dom f c= REAL by NUMBERS:19;
then f is REAL-defined by RELAT_1:def 18;
then for j being Nat st j in dom f & f.j = f.len f holds len f <= j
by A2,FUNCT_1:def 4;
hence thesis by A1,A2,A3,RFINSEQ2:def 2;
end;
end;
theorem
for f being increasing real-valued FinSequence holds max_p(f) = len f
proof
let f be increasing real-valued FinSequence;
per cases;
suppose len f = 0;
hence thesis by RFINSEQ2:def 1;
end;
suppose
A1: len f > 0;
then len f >= 0+1 by NAT_1:13;
then
A2: len f in dom f by FINSEQ_3:25;
A3: for i being Nat st i in dom f holds f.i <= f.len f
proof
let i be Nat such that
A4: i in dom f;
i <= len f by A4,FINSEQ_3:25;
then per cases by XXREAL_0:1;
suppose i = len f;
hence thesis;
end;
suppose i < len f;
hence thesis by A2,A4,VALUED_0:def 13;
end;
end;
for j being Nat st j in dom f & f.j = f.len f holds len f <= j
by A2,FUNCT_1:def 4;
hence thesis by A1,A2,A3,RFINSEQ2:def 1;
end;
end;
registration
let X be included_in_Seg real-membered set;
cluster Sgm X -> increasing;
coherence
proof
set f = Sgm X;
let a be Nat such that
A1: 1 <= a and
A2: a < len f;
A3: a+0 < a+1 by XREAL_1:8;
a+1 <= len f by A2,NAT_1:13;
hence f.a < f.(a+1) by A1,A3,FINSEQ_1:def 14;
end;
end;
begin :: Chinese Remainder Theorem
registration
let f be Chinese_Remainder integer-valued FinSequence;
cluster -f -> Chinese_Remainder;
coherence
proof
set g = -f;
let i,j be Nat;
A1: dom g = dom f by VALUED_1:8;
g.i = -f.i & g.j = -f.j by VALUED_1:8;
hence thesis by A1,Th11,INT_6:def 2;
end;
end;
registration
let f be Chinese_Remainder integer-valued non-empty FinSequence;
cluster f(#)f -> Chinese_Remainder;
coherence
proof
set g = f(#)f;
let i,j be Nat such that
A1: i in dom g & j in dom g and
A2: i <> j;
A3: dom g = dom f /\ dom f by VALUED_1:def 4;
then
A4: f.i <> 0 & f.j <> 0 by A1,FUNCT_1:def 9;
f.i,f.j are_coprime by A1,A2,A3,INT_6:def 2;
then
A5: f.i*f.i,f.j are_coprime by A4,Th16;
g.i = f.i * f.i & g.j = f.j * f.j by VALUED_1:5;
hence thesis by A4,A5,Th16;
end;
end;
definition
let a1,n1,a2,n2 be Integer;
let x be Integer;
pred x solves_CRT a1,n1,a2,n2 means
x,a1 are_congruent_mod n1 & x,a2 are_congruent_mod n2;
end;
theorem Th26:
for a1,n1,a2,n2 being Integer
for x being Integer st x solves_CRT a1,n1,a2,n2
for k being Integer holds x + k*n1*n2 solves_CRT a1,n1,a2,n2
proof
let a1,n1,a2,n2 be Integer;
let x be Integer such that
A1: x solves_CRT a1,n1,a2,n2;
let k be Integer;
set y = x + k*n1*n2;
k*n2*n1,0 are_congruent_mod n1;
then y,a1+0 are_congruent_mod n1 by A1,INT_1:16;
hence y,a1 are_congruent_mod n1;
k*n1*n2,0 are_congruent_mod n2;
then y,a2+0 are_congruent_mod n2 by A1,INT_1:16;
hence y,a2 are_congruent_mod n2;
end;
theorem Th27:
for a1,a2 being Integer
for n1,n2 being Nat st n1 > 0 & n2 > 0
for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1*n2) solves_CRT a1,n1,a2,n2
proof
let a1,a2 be Integer;
let n1,n2 be Nat such that
A1: n1 > 0 and
A2: n2 > 0;
let x be Integer such that
A3: x solves_CRT a1,n1,a2,n2;
A4: x mod n1 = a1 mod n1 by A3,NAT_D:64;
(x mod (n1*n2)) mod n1 = x mod n1 by A2,RADIX_1:7;
hence x mod (n1*n2),a1 are_congruent_mod n1 by A1,A4,NAT_D:64;
A5: x mod n2 = a2 mod n2 by A3,NAT_D:64;
(x mod (n1*n2)) mod n2 = x mod n2 by A1,RADIX_1:7;
hence x mod (n1*n2),a2 are_congruent_mod n2 by A2,A5,NAT_D:64;
end;
definition
let a1,a2 be Integer;
let n1,n2 be Nat such that
A1: n1,n2 are_coprime and
A2: n1 > 0 and
A3: n2 > 0;
func CRT(a1,n1,a2,n2) -> Element of NAT means :Def2:
it solves_CRT a1,n1,a2,n2 & it < n1*n2;
existence
proof
consider m1, m2 being Integer such that
A4: n1 gcd n2 = m1 * n1 + m2 * n2 by NAT_D:68;
set x = a1*m2*n2 + a2*m1*n1;
reconsider y = x mod (n1*n2) as Element of NAT by INT_1:3;
take y;
x solves_CRT a1,n1,a2,n2
proof
x = a1*(m2*n2) + a2*m1*n1
.= a1*(1-m1*n1) + a2*m1*n1 by A1,A4
.= a1 + (a2-a1)*m1*n1;
hence x,a1 are_congruent_mod n1;
x = a2*(m1*n1) + a1*m2*n2
.= a2*(1-m2*n2) + a1*m2*n2 by A1,A4
.= a2 + (a1-a2)*m2*n2;
hence x,a2 are_congruent_mod n2;
end;
hence y solves_CRT a1,n1,a2,n2 by A2,A3,Th27;
thus thesis by A2,A3,INT_1:58;
end;
uniqueness
proof
let x,y be Element of NAT such that
A5: x solves_CRT a1,n1,a2,n2 and
A6: x < n1*n2 and
A7: y solves_CRT a1,n1,a2,n2 and
A8: y < n1*n2;
A9: x,x are_congruent_mod n1*n2 by INT_1:11;
assume x <> y;
then per cases by XXREAL_0:1;
suppose
A10: x > y;
then
A11: x-y is Element of NAT by INT_1:5;
A12: x-y,a1-a1 are_congruent_mod n1 by A5,A7,INT_1:17;
x-y,a2-a2 are_congruent_mod n2 by A5,A7,INT_1:17;
then x,y are_congruent_mod n1*n2 by A1,A11,A12,PEPIN:4;
hence thesis by A6,A8,A9,A10,NAT_6:14;
end;
suppose
A13: x < y;
then
A14: y-x is Element of NAT by INT_1:5;
A15: y-x,a1-a1 are_congruent_mod n1 by A5,A7,INT_1:17;
y-x,a2-a2 are_congruent_mod n2 by A5,A7,INT_1:17;
then y,x are_congruent_mod n1*n2 by A1,A14,A15,PEPIN:4;
then x,y are_congruent_mod n1*n2 by INT_1:14;
hence thesis by A6,A8,A9,A13,NAT_6:14;
end;
end;
end;
theorem Th28:
for a1,a2 being Integer
for n1,n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
{ x where x is positive Nat: x solves_CRT a1,n1,a2,n2 } is infinite
proof
let a1,a2 be Integer;
let n1,n2 be Nat such that
A1: n1,n2 are_coprime and
A2: n1 > 0 & n2 > 0;
set X = { x where x is positive Nat: x solves_CRT a1,n1,a2,n2 };
CRT(a1,n1,a2,n2) solves_CRT a1,n1,a2,n2 by A1,A2,Def2;
then CRT(a1,n1,a2,n2) + 1*n1*n2 solves_CRT a1,n1,a2,n2 by Th26;
then
A3: CRT(a1,n1,a2,n2) + n1*n2 in X by A2;
A4: X is natural-membered
proof
let a be object;
assume a in X;
then ex x being positive Nat st a = x & x solves_CRT a1,n1,a2,n2;
hence thesis;
end;
for a being Nat st a in X ex b being Nat st b > a & b in X
proof
let a be Nat;
assume a in X;
then consider x being positive Nat such that
A5: a = x and
A6: x solves_CRT a1,n1,a2,n2;
take b = x + 1*n1*n2;
x + n1*n2 > x + 0 by A2,XREAL_1:8;
hence b > a by A5;
b solves_CRT a1,n1,a2,n2 by A6,Th26;
hence b in X;
end;
hence thesis by A3,A4,NUMBER04:1;
end;
theorem
for a1,a2 being Integer
for n1,n2 being Nat st n1,n2 are_coprime & n1 > 0 & n2 > 0 holds
{ x where x is Nat: x solves_CRT a1,n1,a2,n2 } is infinite
proof
let a1,a2 be Integer;
let n1,n2 be Nat;
set X = { x where x is positive Nat: x solves_CRT a1,n1,a2,n2 };
X c= { x where x is Nat: x solves_CRT a1,n1,a2,n2 }
proof
let e be object;
assume e in X;
then ex x being positive Nat st e = x & x solves_CRT a1,n1,a2,n2;
hence thesis;
end;
hence thesis by Th28;
end;
definition
let u, m be integer-valued FinSequence;
let z be Integer;
pred z solves_CRT u,m means
for i being Nat st i in dom u holds z,u.i are_congruent_mod m.i;
end;
definition
let u be integer-valued FinSequence;
let m be CR_Sequence;
assume
A1: dom u = dom m;
func CRT(u,m) -> Element of NAT means :Def4:
it solves_CRT u,m & it < Product(m);
existence
proof
len u = len m by A1,FINSEQ_3:29;
then consider z being Integer such that
A2: 0 <= z and
A3: z < Product(m) &
for i being Nat st i in dom u holds z,u.i are_congruent_mod m.i
by INT_6:41;
reconsider z as Element of NAT by A2,INT_1:3;
take z;
thus thesis by A3;
end;
uniqueness by A1,INT_6:42;
end;
theorem Th30:
for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for z being Integer st z solves_CRT u,m
for k being Integer holds z + k*Product(m) solves_CRT u,m
proof
let u be integer-valued FinSequence;
let m be CR_Sequence such that
A1: dom u = dom m;
let z be Integer such that
A2: z solves_CRT u,m;
let k be Integer;
let i be Nat such that
A3: i in dom u;
A4: z,u.i are_congruent_mod m.i by A2,A3;
A5: m.i in rng m by A1,A3,FUNCT_1:def 3;
then m.i divides Product(m) by LIOUVIL2:22;
then Product(m) mod m.i = 0;
then (k*Product(m)) mod m.i = ((k mod m.i) * 0) mod m.i by NAT_D:67
.= 0 mod m.i;
then k*Product(m),0 are_congruent_mod m.i by A1,A3,NAT_D:64;
then z+k*Product(m),u.i+0 are_congruent_mod m.i by A4,INT_1:16;
hence z+k*Product(m),u.i are_congruent_mod m.i;
end;
theorem Th31:
for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
{ z where z is positive Nat: z solves_CRT u,m } is infinite
proof
let u be integer-valued FinSequence;
let m be CR_Sequence;
assume
A1: dom u = dom m;
set X = { x where x is positive Nat: x solves_CRT u,m };
CRT(u,m) solves_CRT u,m by A1,Def4;
then CRT(u,m)+1*Product(m) solves_CRT u,m by A1,Th30;
then
A2: CRT(u,m)+1*Product(m) in X;
A3: X is natural-membered
proof
let a be object;
assume a in X;
then ex x being positive Nat st a = x & x solves_CRT u,m;
hence thesis;
end;
for a being Nat st a in X ex b being Nat st b > a & b in X
proof
let a be Nat;
assume a in X;
then consider x being positive Nat such that
A4: a = x and
A5: x solves_CRT u,m;
take b = x + 1*Product(m);
x + Product(m) > x + 0 by XREAL_1:8;
hence b > a by A4;
b solves_CRT u,m by A1,A5,Th30;
hence b in X;
end;
hence thesis by A2,A3,NUMBER04:1;
end;
theorem
for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
{ z where z is Nat: z solves_CRT u,m } is infinite
proof
let u be integer-valued FinSequence;
let m be CR_Sequence;
set X = { x where x is positive Nat: x solves_CRT u,m };
X c= { x where x is Nat: x solves_CRT u,m }
proof
let a be object;
assume a in X;
then ex x being positive Nat st a = x & x solves_CRT u,m;
hence thesis;
end;
hence thesis by Th31;
end;
begin :: Problem 45
definition
let a,b,c be Integer;
pred two_or_more_are_even_among a,b,c means
a is even & b is even & c is odd or
a is even & b is odd & c is even or
a is odd & b is even & c is even or
a is even & b is even & c is even;
pred two_or_more_are_odd_among a,b,c means
a is odd & b is odd & c is even or
a is odd & b is even & c is odd or
a is even & b is odd & c is odd or
a is odd & b is odd & c is odd;
end;
definition
let a,b,c,n be Integer;
pred a,b,c give_three_different_remainders_upon_dividing_by n means
a mod n, b mod n, c mod n are_mutually_distinct;
pred a,b,c at_least_two_are_not_divisible_by n means
not n divides a & not n divides b & n divides c or
not n divides a & n divides b & not n divides c or
n divides a & not n divides b & not n divides c or
not n divides a & not n divides b & not n divides c;
end;
definition
let a,b,c be Integer;
func numberR(a,b,c) -> Element of NAT equals :Def9:
1 if two_or_more_are_even_among a,b,c
otherwise 0;
correctness;
end;
theorem Th33:
for r being Nat st r = numberR(a,b,c) holds
two_or_more_are_odd_among a+r, b+r, c+r
proof
let r be Nat such that
A1: r = numberR(a,b,c);
per cases;
suppose
A2: two_or_more_are_even_among a,b,c;
then r = 1 by A1,Def9;
hence thesis by A2;
end;
suppose
A3: not two_or_more_are_even_among a,b,c;
then r = 0 by A1,Def9;
hence thesis by A3;
end;
end;
definition
let a,b,c be Integer;
func numberR0(a,b,c) -> Element of INT equals :Def10:
0 if a,b,c give_three_different_remainders_upon_dividing_by 3,
1 - (a mod 3) if a mod 3 = b mod 3 or a mod 3 = c mod 3
otherwise 1 - (b mod 3); :: b mod 3 = c mod 3
coherence by INT_1:def 2;
consistency by ZFMISC_1:def 5;
end;
theorem Th34:
for r0 being Integer st r0 = numberR0(a,b,c) holds
a+r0, b+r0, c+r0 at_least_two_are_not_divisible_by 3
proof
let r0 be Integer such that
A1: r0 = numberR0(a,b,c);
per cases;
suppose
A2: a,b,c give_three_different_remainders_upon_dividing_by 3;
then
A3: a mod 3, b mod 3, c mod 3 are_mutually_distinct;
A4: r0 = 0 by A1,A2,Def10;
assume 3 divides a+r0 or 3 divides b+r0 or not 3 divides c+r0;
hence thesis by A3,A4;
end;
suppose
A5: not a,b,c give_three_different_remainders_upon_dividing_by 3;
then
A6: not a mod 3, b mod 3, c mod 3 are_mutually_distinct;
assume
A7: not a+r0,b+r0,c+r0 at_least_two_are_not_divisible_by 3;
then
A8: (3 divides a+r0 or 3 divides b+r0 or not 3 divides c+r0) &
(3 divides a+r0 or not 3 divides b+r0 or 3 divides c+r0) &
(not 3 divides a+r0 or 3 divides b+r0 or 3 divides c+r0) &
(3 divides a+r0 or 3 divides b+r0 or 3 divides c+r0);
A9: a+r0 mod 3 = ((a mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A10: b+r0 mod 3 = ((b mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A11: c+r0 mod 3 = ((c mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
reconsider a3 = a mod 3 as Element of NAT by INT_1:3;
a mod 3 < 2+1 by INT_1:58;
then a3 <= 2 by NAT_1:13;
then
A12: a3 = 0 or ... or a3 = 2;
per cases by A6;
suppose
A13: a mod 3 = b mod 3;
then
A14: r0 = 1 - (a mod 3) by A1,Def10;
then per cases by A12;
suppose r0 = 1;
hence contradiction by A7,A9,A10,A13,A14,Lm5,INT_1:62;
end;
suppose r0 = 0;
hence contradiction by A8,A13,A14;
end;
suppose r0 = -1;
hence contradiction
by A7,A9,A10,A13,A14,Lm5,Lm6,INT_1:62,NUMBER02:9;
end;
end;
suppose
A15: a mod 3 = c mod 3;
then
A16: r0 = 1 - (a mod 3) by A1,Def10;
then per cases by A12;
suppose r0 = 1;
hence contradiction by A7,A9,A11,A15,A16,Lm5,INT_1:62;
end;
suppose r0 = 0;
hence contradiction by A8,A15,A16;
end;
suppose r0 = -1;
hence contradiction
by A7,A9,A11,A15,A16,Lm5,Lm6,INT_1:62,NUMBER02:9;
end;
end;
suppose that
A17: b mod 3 = c mod 3 and
A18: a mod 3 <> b mod 3 & a mod 3 <> c mod 3;
reconsider b3 = b mod 3 as Element of NAT by INT_1:3;
b mod 3 < 2+1 by INT_1:58;
then b3 <= 2 by NAT_1:13;
then
A19: b3 = 0 or ... or b3 = 2;
A20: r0 = 1 - (b mod 3) by A1,A5,A18,Def10;
then per cases by A19;
suppose r0 = 1;
hence contradiction by A7,A10,A11,A17,A20,Lm5,INT_1:62;
end;
suppose r0 = 0;
hence contradiction by A8,A17,A20;
end;
suppose r0 = -1;
hence contradiction
by A7,A10,A11,A17,A20,Lm5,Lm6,INT_1:62,NUMBER02:9;
end;
end;
end;
end;
definition
let h be Integer;
func PrimeDivisors>3(h) -> Subset of NAT equals
PrimeDivisors(h) /\ GreaterOrEqualsNumbers(4);
coherence;
end;
theorem Th35:
i in PrimeDivisors>3(h) implies i > 3
proof
assume i in PrimeDivisors>3(h);
then i >= 3+1 by NUMBER09:56;
hence thesis by NAT_1:13;
end;
theorem Th36:
i in PrimeDivisors>3(h) implies i divides h
proof
assume i in PrimeDivisors>3(h);
then i in PrimeDivisors(h);
then ex p being Prime st i = p & p divides h;
hence thesis;
end;
theorem Th37:
i in PrimeDivisors>3(h) implies i is prime
proof
assume i in PrimeDivisors>3(h);
then i in PrimeDivisors(h);
then ex p being Prime st i = p & p divides h;
hence thesis;
end;
theorem Th38:
i is prime & i > 3 & i divides h implies i in PrimeDivisors>3(h)
proof
assume that
A1: i is prime and
A2: i > 3 and
A3: i divides h;
A4: i is Element of NAT by A2,INT_1:3;
then
A5: i in PrimeDivisors(h) by A1,A3;
i >= 3+1 by A2,NAT_1:13;
then i in GreaterOrEqualsNumbers(4) by A4,NUMBER09:56;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th39:
h <> 0 implies PrimeDivisors>3(h) c= Seg |.h.|
proof
assume
A1: h <> 0;
let x be object;
assume
A2: x in PrimeDivisors>3(h);
then reconsider x as Element of NAT;
A3: x >= 1 by A2,Th35,XXREAL_0:2;
x divides h by A2,Th36;
then x <= |.h.| by A1,Th4,NAT_D:7;
hence thesis by A3;
end;
registration
let h be non zero Integer;
cluster PrimeDivisors>3(h) -> included_in_Seg;
coherence
proof
take |.h.|;
thus thesis by Th39;
end;
end;
theorem Th40:
h <> 0 implies
for n being Nat st n in dom Sgm PrimeDivisors>3(h) holds
(Sgm PrimeDivisors>3(h)).n > 3
proof
set X = PrimeDivisors>3(h);
set f = Sgm X;
assume
A1: h <> 0;
let n be Nat;
assume n in dom f;
then
A2: f.n in rng f by FUNCT_1:def 3;
rng f = X by A1,FINSEQ_1:def 14;
hence thesis by A2,Th35;
end;
theorem
h <> 0 implies
for n being Nat st n in dom Sgm PrimeDivisors>3(h) holds
(Sgm PrimeDivisors>3(h)).n divides h
proof
set X = PrimeDivisors>3(h);
set f = Sgm X;
assume
A1: h <> 0;
let n be Nat;
assume n in dom f;
then
A2: f.n in rng f by FUNCT_1:def 3;
rng f = X by A1,FINSEQ_1:def 14;
hence thesis by A2,Th36;
end;
theorem Th42:
h <> 0 implies
for n being Nat st n in dom Sgm PrimeDivisors>3(h) holds
(Sgm PrimeDivisors>3(h)).n is prime
proof
set X = PrimeDivisors>3(h);
set f = Sgm X;
assume
A1: h <> 0;
let n be Nat;
assume n in dom f;
then
A2: f.n in rng f by FUNCT_1:def 3;
rng f = X by A1,FINSEQ_1:def 14;
hence thesis by A2,Th37;
end;
definition
let a,b,c be Integer such that
A1: a,b,c are_mutually_distinct;
mode Sierp45FS of a,b,c -> FinSequence of INT means :Def12:
ex h being Integer, F being FinSequence of NAT st
h = (a-b)*(a-c)*(b-c) & F = Sgm PrimeDivisors>3(h) &
len it = len F &
for i being object st i in dom it holds
not F.i divides a+it.i & not F.i divides b+it.i & not F.i divides c+it.i;
existence
proof
set h = (a-b)*(a-c)*(b-c);
set F = Sgm PrimeDivisors>3(h);
A2: Seg len F = dom F by FINSEQ_1:def 3;
defpred P[object,Integer] means
not F.$1 divides a+$2 & not F.$1 divides b+$2 & not F.$1 divides c+$2;
A3: for i being Nat st i in Seg len F ex x being Element of INT st P[i,x]
proof
let i be Nat such that
A4: i in Seg len F;
set n = F.i;
A5: a-b <> 0 & a-c <> 0 & b-c <> 0 by A1;
n in rng F by A2,A4,FUNCT_1:def 3;
then n in PrimeDivisors>3(h) by A5,FINSEQ_1:def 14;
then consider k being Integer such that
A6: not n divides k+a & not n divides k+b & not n divides k+c
by Th35,NUMBER03:53;
reconsider k as Element of INT by INT_1:def 2;
take k;
thus thesis by A6;
end;
consider p being FinSequence of INT such that
A7: dom p = Seg len F and
A8: for k st k in Seg len F holds P[k,p.k] from FINSEQ_1:sch 5(A3);
take p, h, F;
thus h = (a-b)*(a-c)*(b-c);
thus F = Sgm PrimeDivisors>3(h);
thus len p = len F by A7,FINSEQ_1:def 3;
thus thesis by A7,A8;
end;
end;
Lm7:
for a,b,c,h st h = (a-b)*(a-c)*(b-c)
for S being Sierp45FS of a,b,c
for n being Nat st
a,b,c are_mutually_distinct &
n, numberR(a,b,c) are_congruent_mod 2 &
n, numberR0(a,b,c) are_congruent_mod 3 &
(for i being Nat st i in dom S holds
n, S.i are_congruent_mod (Sgm PrimeDivisors>3(h)).i) holds
a+n, b+n are_coprime
proof
let a,b,c,h such that
A1: h = (a-b)*(a-c)*(b-c);
set r = numberR(a,b,c);
set r0 = numberR0(a,b,c);
set SGM = Sgm PrimeDivisors>3(h);
let S be Sierp45FS of a,b,c;
let n be Nat such that
A2: a,b,c are_mutually_distinct and
A3: n,r are_congruent_mod 2 and
A4: n,r0 are_congruent_mod 3 and
A5: for i being Nat st i in dom S holds n, S.i are_congruent_mod SGM.i;
assume
A6: not a+n, b+n are_coprime;
consider q being Prime such that
A7: q divides |.a+n.| & q divides |.b+n.| by A6,Th9,PYTHTRIP:def 2;
A8: q divides a+n & q divides b+n by A7,Th4;
then
A9: q divides (a+n)-(b+n) by INT_5:1;
A10: h = (a-b)*((a-c)*(b-c)) by A1;
two_or_more_are_odd_among a+n,b+n,c+n
proof
r,n are_congruent_mod 2 by A3,INT_1:14;
then
A11: a+r,a+n are_congruent_mod 2 &
b+r,b+n are_congruent_mod 2 &
c+r,c+n are_congruent_mod 2;
two_or_more_are_odd_among a+r,b+r,c+r by Th33;
hence thesis by A11;
end;
then
A12: q <> 2 by A8;
a+n,b+n,c+n at_least_two_are_not_divisible_by 3
proof
A13: n mod 3 = r0 mod 3 by A4,NAT_D:64;
A14: a+r0 mod 3 = ((a mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A15: b+r0 mod 3 = ((b mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A16: c+r0 mod 3 = ((c mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A17: a+n mod 3 = ((a mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A18: b+n mod 3 = ((b mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A19: c+n mod 3 = ((c mod 3) + (n mod 3)) mod 3 by NAT_D:66;
now
a+r0,b+r0,c+r0 at_least_two_are_not_divisible_by 3 by Th34;
then per cases;
case not 3 divides a+r0 & not 3 divides b+r0 & 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 = 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case not 3 divides a+r0 & 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 = 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 = 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case not 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19;
end;
end;
hence thesis;
end;
then
A20: q <> 3 by A8;
consider h1 being Integer, F being FinSequence of NAT such that
A21: h1 = (a-b)*(a-c)*(b-c) and
A22: F = Sgm PrimeDivisors>3(h1) and
A23: len S = len F and
A24: for i being object st i in dom S holds
not F.i divides a+S.i & not F.i divides b+S.i & not F.i divides c+S.i
by A2,Def12;
a-b <> 0 & a-c <> 0 & b-c <> 0 by A2;
then
A25: PrimeDivisors>3(h) = rng SGM by A1,FINSEQ_1:def 14;
now
assume q <= 3;
then q = 0 or ... or q = 3;
hence contradiction by A12,A20,INT_2:def 4;
end;
then q in PrimeDivisors>3(h) by A9,A10,Th38,INT_2:2;
then consider i being object such that
A26: i in dom SGM and
A27: q = SGM.i by A25,FUNCT_1:def 3;
reconsider i as Nat by A26;
A28: dom S = dom SGM by A1,A21,A22,A23,FINSEQ_3:29;
then n, S.i are_congruent_mod q by A5,A26,A27;
then
A29: n+a,S.i+a are_congruent_mod q;
not q divides a+S.i & not q divides b+S.i & not q divides c+S.i
by A1,A21,A22,A26,A27,A28,A24;
hence contradiction by A8,A29,Th19;
end;
Lm8:
for a,b,c,h st h = (a-b)*(a-c)*(b-c)
for S being Sierp45FS of a,b,c
for n being Nat st
a,b,c are_mutually_distinct &
n, numberR(a,b,c) are_congruent_mod 2 &
n, numberR0(a,b,c) are_congruent_mod 3 &
(for i being Nat st i in dom S holds
n, S.i are_congruent_mod (Sgm PrimeDivisors>3(h)).i) holds
a+n, c+n are_coprime
proof
let a,b,c,h such that
A1: h = (a-b)*(a-c)*(b-c);
set r = numberR(a,b,c);
set r0 = numberR0(a,b,c);
set SGM = Sgm PrimeDivisors>3(h);
let S be Sierp45FS of a,b,c;
let n be Nat such that
A2: a,b,c are_mutually_distinct and
A3: n,r are_congruent_mod 2 and
A4: n,r0 are_congruent_mod 3 and
A5: for i being Nat st i in dom S holds n, S.i are_congruent_mod SGM.i;
assume
A6: not a+n, c+n are_coprime;
consider q being Prime such that
A7: q divides |.a+n.| & q divides |.c+n.| by A6,Th9,PYTHTRIP:def 2;
A8: q divides a+n & q divides c+n by A7,Th4;
then
A9: q divides (a+n)-(c+n) by INT_5:1;
A10: h = (a-c)*((a-b)*(b-c)) by A1;
two_or_more_are_odd_among a+n,b+n,c+n
proof
r,n are_congruent_mod 2 by A3,INT_1:14;
then
A11: a+r,a+n are_congruent_mod 2 &
b+r,b+n are_congruent_mod 2 &
c+r,c+n are_congruent_mod 2;
two_or_more_are_odd_among a+r,b+r,c+r by Th33;
hence thesis by A11;
end;
then
A12: q <> 2 by A8;
a+n,b+n,c+n at_least_two_are_not_divisible_by 3
proof
A13: n mod 3 = r0 mod 3 by A4,NAT_D:64;
A14: a+r0 mod 3 = ((a mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A15: b+r0 mod 3 = ((b mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A16: c+r0 mod 3 = ((c mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A17: a+n mod 3 = ((a mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A18: b+n mod 3 = ((b mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A19: c+n mod 3 = ((c mod 3) + (n mod 3)) mod 3 by NAT_D:66;
now
a+r0,b+r0,c+r0 at_least_two_are_not_divisible_by 3 by Th34;
then per cases;
case not 3 divides a+r0 & not 3 divides b+r0 & 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 = 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case not 3 divides a+r0 & 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 = 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 = 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19,INT_1:62;
end;
case not 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A13,A14,A15,A16,A17,A18,A19;
end;
end;
hence thesis;
end;
then
A20: q <> 3 by A8;
consider h1 being Integer, F being FinSequence of NAT such that
A21: h1 = (a-b)*(a-c)*(b-c) and
A22: F = Sgm PrimeDivisors>3(h1) and
A23: len S = len F and
A24: for i being object st i in dom S holds
not F.i divides a+S.i & not F.i divides b+S.i & not F.i divides c+S.i
by A2,Def12;
a-b <> 0 & a-c <> 0 & b-c <> 0 by A2;
then
A25: PrimeDivisors>3(h) = rng SGM by A1,FINSEQ_1:def 14;
now
assume q <= 3;
then q = 0 or ... or q = 3;
hence contradiction by A12,A20,INT_2:def 4;
end;
then q in PrimeDivisors>3(h) by A9,A10,Th38,INT_2:2;
then consider i being object such that
A26: i in dom SGM and
A27: q = SGM.i by A25,FUNCT_1:def 3;
reconsider i as Nat by A26;
A28: dom S = dom SGM by A1,A21,A22,A23,FINSEQ_3:29;
then n, S.i are_congruent_mod q by A5,A26,A27;
then
A29: n+a,S.i+a are_congruent_mod q;
not q divides a+S.i & not q divides b+S.i & not q divides c+S.i
by A1,A21,A22,A26,A27,A28,A24;
hence contradiction by A8,A29,Th19;
end;
Lm9:
for a,b,c,h st h = (a-b)*(a-c)*(b-c)
for S being Sierp45FS of a,b,c
for n being Nat st
a,b,c are_mutually_distinct &
n, numberR(a,b,c) are_congruent_mod 2 &
n, numberR0(a,b,c) are_congruent_mod 3 &
(for i being Nat st i in dom S holds
n, S.i are_congruent_mod (Sgm PrimeDivisors>3(h)).i) holds
b+n, c+n are_coprime
proof
let a,b,c,h such that
A1: h = (a-b)*(a-c)*(b-c);
set r = numberR(a,b,c);
set r0 = numberR0(a,b,c);
set SGM = Sgm PrimeDivisors>3(h);
let S be Sierp45FS of a,b,c;
let n be Nat such that
A2: a,b,c are_mutually_distinct and
A3: n,r are_congruent_mod 2 and
A4: n,r0 are_congruent_mod 3 and
A5: for i being Nat st i in dom S holds n, S.i are_congruent_mod SGM.i;
assume
A6: not b+n, c+n are_coprime;
consider q being Prime such that
A7: q divides |.b+n.| & q divides |.c+n.| by A6,Th9,PYTHTRIP:def 2;
A8: q divides b+n & q divides c+n by A7,Th4;
then
A9: q divides (b+n)-(c+n) by INT_5:1;
two_or_more_are_odd_among a+n,b+n,c+n
proof
r,n are_congruent_mod 2 by A3,INT_1:14;
then
A10: a+r,a+n are_congruent_mod 2 &
b+r,b+n are_congruent_mod 2 &
c+r,c+n are_congruent_mod 2;
two_or_more_are_odd_among a+r,b+r,c+r by Th33;
hence thesis by A10;
end;
then
A11: q <> 2 by A8;
a+n,b+n,c+n at_least_two_are_not_divisible_by 3
proof
A12: n mod 3 = r0 mod 3 by A4,NAT_D:64;
A13: a+r0 mod 3 = ((a mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A14: b+r0 mod 3 = ((b mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A15: c+r0 mod 3 = ((c mod 3) + (r0 mod 3)) mod 3 by NAT_D:66;
A16: a+n mod 3 = ((a mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A17: b+n mod 3 = ((b mod 3) + (n mod 3)) mod 3 by NAT_D:66;
A18: c+n mod 3 = ((c mod 3) + (n mod 3)) mod 3 by NAT_D:66;
now
a+r0,b+r0,c+r0 at_least_two_are_not_divisible_by 3 by Th34;
then per cases;
case not 3 divides a+r0 & not 3 divides b+r0 & 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 = 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & 3 divides c+n
by A12,A13,A14,A15,A16,A17,A18,INT_1:62;
end;
case not 3 divides a+r0 & 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 = 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & 3 divides b+n & not 3 divides c+n
by A12,A13,A14,A15,A16,A17,A18,INT_1:62;
end;
case 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 = 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A12,A13,A14,A15,A16,A17,A18,INT_1:62;
end;
case not 3 divides a+r0 & not 3 divides b+r0 & not 3 divides c+r0;
then a+r0 mod 3 <> 0 & b+r0 mod 3 <> 0 & c+r0 mod 3 <> 0 by INT_1:62;
hence not 3 divides a+n & not 3 divides b+n & not 3 divides c+n
by A12,A13,A14,A15,A16,A17,A18;
end;
end;
hence thesis;
end;
then
A19: q <> 3 by A8;
consider h1 being Integer, F being FinSequence of NAT such that
A20: h1 = (a-b)*(a-c)*(b-c) and
A21: F = Sgm PrimeDivisors>3(h1) and
A22: len S = len F and
A23: for i being object st i in dom S holds
not F.i divides a+S.i & not F.i divides b+S.i & not F.i divides c+S.i
by A2,Def12;
a-b <> 0 & a-c <> 0 & b-c <> 0 by A2;
then
A24: PrimeDivisors>3(h) = rng SGM by A1,FINSEQ_1:def 14;
now
assume q <= 3;
then q = 0 or ... or q = 3;
hence contradiction by A11,A19,INT_2:def 4;
end;
then q in PrimeDivisors>3(h) by A9,A1,Th38,INT_2:2;
then consider i being object such that
A25: i in dom SGM and
A26: q = SGM.i by A24,FUNCT_1:def 3;
reconsider i as Nat by A25;
A27: dom S = dom SGM by A1,A20,A21,A22,FINSEQ_3:29;
then n, S.i are_congruent_mod q by A5,A25,A26;
then
A28: n+b,S.i+b are_congruent_mod q;
not q divides a+S.i & not q divides b+S.i & not q divides c+S.i
by A1,A20,A21,A25,A26,A27,A23;
hence contradiction by A8,A28,Th19;
end;
theorem Th43:
for a,b,c,h being Integer st h = (a-b)*(a-c)*(b-c)
for S being Sierp45FS of a,b,c st a,b,c are_mutually_distinct
for n being Nat st
n, numberR(a,b,c) are_congruent_mod 2 &
n, numberR0(a,b,c) are_congruent_mod 3 &
for i being Nat st i in dom S holds
n, S.i are_congruent_mod (Sgm PrimeDivisors>3(h)).i
holds a+n, b+n, c+n are_mutually_coprime
proof
let a,b,c,h be Integer such that
A1: h = (a-b)*(a-c)*(b-c);
let S be Sierp45FS of a,b,c such that
A2: a,b,c are_mutually_distinct;
let n be Nat such that
A3: n, numberR(a,b,c) are_congruent_mod 2 and
A4: n, numberR0(a,b,c) are_congruent_mod 3 and
A5: for i being Nat st i in dom S holds
n, S.i are_congruent_mod (Sgm PrimeDivisors>3(h)).i;
assume not thesis;
then per cases;
suppose not a+n,b+n are_coprime;
hence thesis by A1,A2,A3,A4,A5,Lm7;
end;
suppose not a+n,c+n are_coprime;
hence thesis by A1,A2,A3,A4,A5,Lm8;
end;
suppose not b+n,c+n are_coprime;
hence thesis by A1,A2,A3,A4,A5,Lm9;
end;
end;
Lm10:
now
let n be Nat;
assume
A1: n >= 1 & n <> 1 & n <> 2;
assume n <= 2;
then n = 0 or ... or n = 2;
hence contradiction by A1;
end;
theorem Th44:
h <> 0 implies rng (<*2,3*> ^ Sgm PrimeDivisors>3(h)) c= SetPrimes
proof
set X = PrimeDivisors>3(h);
set F = Sgm X;
set f = <*2,3*>;
assume
A1: h <> 0;
A2: rng(f^F) = rng f \/ rng F by FINSEQ_1:31;
A3: rng f c= SetPrimes
proof
let x be object;
assume x in rng f;
then x in {2,3} by FINSEQ_2:127;
then x = 2 or x = 3 by TARSKI:def 2;
hence thesis by NEWTON:def 6,XPRIMES1:2,3;
end;
rng F c= SetPrimes
proof
let x be object;
assume x in rng F;
then x in X by A1,FINSEQ_1:def 14;
then x is prime Nat by Th37;
hence thesis by NEWTON:def 6;
end;
hence thesis by A2,A3,XBOOLE_1:8;
end;
theorem Th45:
h <> 0 implies <*2,3*> ^ Sgm PrimeDivisors>3(h) is Chinese_Remainder
proof
set X = PrimeDivisors>3(h);
set F = Sgm X;
set m = <*2,3*>^F;
assume
A1: h <> 0;
then
A2: rng m c= SetPrimes by Th44;
A3: for i st i in dom m holds m.i is prime
proof
let i;
assume i in dom m;
then m.i in rng m by FUNCT_1:def 3;
hence m.i is prime by A2,NEWTON:def 6;
end;
A4: len <*2,3*> = 2 by FINSEQ_1:44;
A5: m.1 = 2 by Th21;
A6: m.2 = 3 by Th21;
let i,j be Nat;
assume
A7: i in dom m;
then
A8: m.i is prime by A3;
assume
A9: j in dom m;
then
A10: m.j is prime by A3;
A11: 1 <= j by A9,FINSEQ_3:25;
A12: len m = len <*2,3*> + len F by FINSEQ_1:22;
assume
A13: i <> j;
A14: now
assume
A15: j > 2;
then reconsider j2 = j-2 as Element of NAT by INT_1:5;
j2 > 2-2 by A15,XREAL_1:8;
hence
A16: j-2 >= 0+1 by NAT_1:13;
j <= len m by A9,FINSEQ_3:25;
then
A17: j2 <= 2 + len F - 2 by A4,A12,XREAL_1:7;
hence j-2 <= len F;
thus
A18: j-2 in dom F by A16,A17,FINSEQ_3:25;
hence F.(j-2) > 3 by A1,Th40;
thus m.j = m.(2+j2)
.= F.(j-2) by A18,Th23;
thus F.(j-2) is prime by A1,A18,Th42;
end;
1 <= i by A7,FINSEQ_3:25;
then per cases by Lm10;
suppose
A19: i = 1;
per cases by A11,Lm10;
suppose j = 1;
hence m.i,m.j are_coprime by A13,A19;
end;
suppose j = 2;
hence m.i,m.j are_coprime by A5,A6,A8,A10,A19,INT_2:30;
end;
suppose
A20: j > 2;
then 2,F.(j-2) are_coprime or 2 = F.(j-2) by A14,INT_2:30,XPRIMES1:2;
hence m.i,m.j are_coprime by A14,A19,A20,Th21;
end;
end;
suppose
A21: i = 2;
per cases by A11,Lm10;
suppose j = 1;
hence m.i,m.j are_coprime by A5,A6,A21,INT_2:30,XPRIMES1:2,3;
end;
suppose j = 2;
hence m.i,m.j are_coprime by A13,A21;
end;
suppose j > 2;
hence m.i,m.j are_coprime by A6,A14,A21,INT_2:30,XPRIMES1:3;
end;
end;
suppose
A22: i > 2;
then reconsider i2 = i-2 as Element of NAT by INT_1:5;
i2 > 2-2 by A22,XREAL_1:8;
then
A23: i2 >= 0+1 by NAT_1:13;
i <= len m by A7,FINSEQ_3:25;
then
A24: i2 <= 2 + len F - 2 by A4,A12,XREAL_1:7;
then
A25: i-2 in dom F by A23,FINSEQ_3:25;
then
A26: F.(i-2) > 3 by A1,Th40;
A27: m.i = m.(2+i2)
.= F.(i-2) by A25,Th23;
A28: F.(i-2) is prime by A1,A25,Th42;
per cases by A11,Lm10;
suppose
A29: j = 1;
2,F.(i-2) are_coprime or 2 = F.(i-2) by A28,INT_2:30,XPRIMES1:2;
hence m.i,m.j are_coprime by A1,A25,A27,A29,Th40,Th21;
end;
suppose j = 2;
hence m.i,m.j are_coprime by A6,A26,A27,A28,INT_2:30,XPRIMES1:3;
end;
suppose
A30: j > 2;
then reconsider j2 = j-2 as Element of NAT by A14;
per cases by A13,XXREAL_0:1;
suppose i < j;
then i2 < j2 by XREAL_1:8;
then F.i2 < F.j2 by A1,A14,A23,A30,FINSEQ_1:def 14;
hence m.i,m.j are_coprime by A8,A14,A27,A30,INT_2:30;
end;
suppose i > j;
then i2 > j2 by XREAL_1:8;
then F.i2 > F.j2 by A1,A14,A24,A30,FINSEQ_1:def 14;
hence m.i,m.j are_coprime by A8,A14,A27,A30,INT_2:30;
end;
end;
end;
end;
:: Problem 45
theorem
a,b,c are_mutually_distinct implies
{ n where n is positive Nat: a+n,b+n,c+n are_mutually_coprime } is infinite
proof
set A = { n where n is positive Nat: a+n,b+n,c+n are_mutually_coprime };
assume
A1: a,b,c are_mutually_distinct;
set S = the Sierp45FS of a,b,c;
set r = numberR(a,b,c);
set r0 = numberR0(a,b,c);
consider h being Integer, F being FinSequence of NAT such that
A2: h = (a-b)*(a-c)*(b-c) and
A3: F = Sgm PrimeDivisors>3(h) and
A4: len S = len F and
for i being object st i in dom S holds
not F.i divides a+S.i & not F.i divides b+S.i & not F.i divides c+S.i
by A1,Def12;
set X = PrimeDivisors>3(h);
set m = <*2,3*>^F;
set u = <*r,r0*>^S;
reconsider u as integer-valued FinSequence;
len <*r,r0*> = 2 by FINSEQ_1:44;
then
A5: dom u = Seg (2 + len S) by FINSEQ_1:def 7;
len <*2,3*> = 2 by FINSEQ_1:44;
then
A6: dom m = Seg (2 + len F) by FINSEQ_1:def 7;
A7: m.1 = 2 by Th21;
A8: m.2 = 3 by Th21;
A9: a-b <> 0 & a-c <> 0 & b-c <> 0 by A1;
m is positive-yielding
proof
let n be Nat;
assume n in dom m;
then
A10: m.n in rng m by FUNCT_1:def 3;
rng m c= SetPrimes by A2,A3,A9,Th44;
then m.n is prime by A10,NEWTON:def 6;
hence thesis;
end;
then reconsider m as CR_Sequence by A2,A3,A9,Th45;
set Z = { z where z is positive Nat: z solves_CRT u,m };
Z c= A
proof
let s be object;
assume s in Z;
then consider z being positive Nat such that
A11: s = z and
A12: z solves_CRT u,m;
u.1 = r by Th21;
then
A13: z,r are_congruent_mod 2 by A7,A12,Th20;
u.2 = r0 by Th21;
then
A14: z,r0 are_congruent_mod 3 by A8,A12,Th20;
for i being Nat st i in dom S holds z, S.i are_congruent_mod F.i
proof
let i be Nat;
assume
A15: i in dom S;
then
A16: z,u.(i+2) are_congruent_mod m.(i+2) by A12,Th22;
dom F = dom S by A4,FINSEQ_3:29;
then m.(i+2) = F.i by A15,Th23;
hence z, S.i are_congruent_mod F.i by A15,A16,Th23;
end;
then a+z,b+z,c+z are_mutually_coprime by A1,A2,A3,A13,A14,Th43;
hence thesis by A11;
end;
hence A is infinite by A4,A5,A6,Th31;
end;
begin :: Problem 49
registration
let n be non zero Nat;
cluster PrimeDivisors(n) -> finite;
coherence
proof
PrimeDivisors(n) c= Seg(n) by NUMBER12:46;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster PrimeDivisors(n) -> included_in_Seg;
coherence
proof
take n;
thus PrimeDivisors(n) c= Seg(n) by NUMBER12:46;
thus thesis;
end;
end;
registration
let X be non trivial natural-membered set;
cluster non empty included_in_Seg for Subset of X;
existence
proof
X c= NAT by MEMBERED:6;
then consider d1,d2 being Element of NAT such that
A1: d1 in X and
A2: d2 in X and
A3: d1 <> d2 by SUBSET_1:45;
per cases by A3,XXREAL_0:1;
suppose d1 < d2;
then
A4: 0+1 <= d2 by NAT_1:13;
reconsider A = {d2} as Subset of X by A2,ZFMISC_1:31;
take A;
thus A is non empty;
take d2;
let x be object;
assume x in A;
then x = d2 by TARSKI:def 1;
hence thesis by A4;
end;
suppose d2 < d1;
then
A5: 0+1 <= d1 by NAT_1:13;
reconsider A = {d1} as Subset of X by A1,ZFMISC_1:31;
take A;
thus A is non empty;
take d1;
let x be object;
assume x in A;
then x = d1 by TARSKI:def 1;
hence thesis by A5;
end;
end;
end;
registration
let X be non empty included_in_Seg Subset of SetPrimes;
cluster Sgm X -> non empty;
coherence
proof
rng Sgm X = X by FINSEQ_1:def 14;
hence thesis;
end;
end;
registration
let X be included_in_Seg Subset of SetPrimes;
set f = Sgm X;
A1: rng f = X by FINSEQ_1:def 14;
cluster Sgm X -> positive-yielding;
coherence
proof
let m;
assume m in dom f;
then f.m in X by A1,FUNCT_1:def 3;
then f.m is prime by NEWTON:def 6;
hence f.m > 0;
end;
cluster Sgm X -> Chinese_Remainder;
coherence
proof
let i,j be Nat;
assume
A2: i in dom f;
then
A3: f.i in rng f by FUNCT_1:def 3;
assume
A4: j in dom f;
then
A5: f.j in rng f by FUNCT_1:def 3;
A6: 1 <= i <= len f by A2,FINSEQ_3:25;
A7: 1 <= j <= len f by A4,FINSEQ_3:25;
assume i <> j;
then i < j or i > j by XXREAL_0:1;
then
A8: f.i < f.j or f.i > f.j by A6,A7,FINSEQ_1:def 14;
f.i is prime & f.j is prime by A1,A3,A5,NEWTON:def 6;
hence thesis by A8,INT_2:30;
end;
end;
definition
let n be non zero Nat;
func PrimeDivisorsFS(n) -> FinSequence of SetPrimes equals
Sgm PrimeDivisors(n);
coherence
proof
rng Sgm PrimeDivisors(n) = PrimeDivisors(n) by FINSEQ_1:def 14;
hence thesis by NUMBER12:45,FINSEQ_1:def 4;
end;
end;
registration
let n be non zero Nat;
cluster PrimeDivisorsFS(n) -> increasing;
coherence;
end;
theorem Th47:
for n being non zero Nat, i being Nat st i in dom PrimeDivisorsFS(n) holds
PrimeDivisorsFS(n).i is prime
proof
let n be non zero Nat;
set f = PrimeDivisorsFS(n);
let i be Nat;
assume i in dom f;
then f.i in rng f by FUNCT_1:def 3;
then f.i in PrimeDivisors(n) by FINSEQ_1:def 14;
then ex p being Prime st p = f.i & p divides n;
hence thesis;
end;
definition
let m be non zero Nat;
let k be Nat;
mode Sierp49FS of m,k -> FinSequence of INT means :Def14:
len it = len PrimeDivisorsFS(m) &
for i being object st i in dom it holds
not PrimeDivisorsFS(m).i divides it.i * (it.i + 2*k);
existence
proof
set q = PrimeDivisorsFS(m);
A1: dom q = Seg len q by FINSEQ_1:def 3;
defpred P[object,Integer] means not q.$1 divides $2 * ($2 + 2*k);
A2: for z being Nat st z in Seg len q ex x being Element of INT st P[z,x]
proof
let z be Nat such that
A3: z in Seg len q;
for i being Nat st i in dom q holds
not for x being Integer holds q.i divides x*(x+2*k)
proof
let i be Nat such that
A4: i in dom q and
A5: for x being Integer holds q.i divides x*(x+2*k);
A6: q.i is prime by A4,Th47;
A7: q.i divides 1*(1+2*k) & q.i divides (-1)*(-1+2*k) by A5;
then q.i divides (2*k+1)+-(2*k-1) by WSIERP_1:4;
then q.i divides 2*k by INT_2:2;
then q.i divides 2*k+-(2*k-1) by A7,WSIERP_1:4;
hence thesis by A6,INT_2:27;
end;
then consider x being Integer such that
A8: not q.z divides x*(x+2*k) by A1,A3;
reconsider x as Element of INT by INT_1:def 2;
take x;
thus thesis by A8;
end;
consider p being FinSequence of INT such that
A9: dom p = Seg len q &
for k st k in Seg len q holds P[k,p.k] from FINSEQ_1:sch 5(A2);
take p;
thus thesis by A9,FINSEQ_1:def 3;
end;
end;
registration
let n be non zero Nat;
cluster PrimeDivisorsFS(n) -> Chinese_Remainder positive-yielding;
coherence
proof
reconsider X = PrimeDivisors(n) as included_in_Seg Subset of SetPrimes
by NUMBER12:45;
PrimeDivisorsFS(n) = Sgm X;
hence thesis;
end;
end;
registration
cluster PrimeDivisorsFS(1) -> empty;
coherence
proof
rng Sgm PrimeDivisors(1) = PrimeDivisors(1) by FINSEQ_1:def 14;
hence thesis by NUMBER12:51;
end;
end;
theorem Th48:
for n being non zero Nat holds support pfexp n = PrimeDivisors(n)
proof
let n be non zero Nat;
set S = support pfexp n;
set X = PrimeDivisors(n);
thus S c= X
proof
let x be object;
assume
A1: x in S;
then reconsider x as Prime by NAT_3:34;
x divides n by A1,NAT_3:36;
hence thesis;
end;
let x be object;
assume x in X;
then ex p being Prime st x = p & p divides n;
then (pfexp n).x <> 0 by NAT_3:38;
hence thesis by PRE_POLY:def 7;
end;
theorem Th49:
for n being non zero Nat st PrimeDivisors(n) is empty holds n = 1
proof
let n be non zero Nat;
set X = PrimeDivisors(n);
assume
A1: X is empty;
assume n <> 1;
then consider p being Prime such that
A2: p divides n by MOEBIUS1:5;
p in X by A2;
hence thesis by A1;
end;
theorem Th50:
for n being non zero Nat st PrimeDivisorsFS(n) is empty holds n = 1
proof
let n be non zero Nat;
rng PrimeDivisorsFS(n) = PrimeDivisors(n) by FINSEQ_1:def 14;
hence thesis by Th49;
end;
registration
let n be non trivial Nat;
A1: n <> 1 by NAT_2:29;
cluster PrimeDivisors(n) -> non empty;
coherence by A1,Th49;
cluster PrimeDivisorsFS(n) -> non empty;
coherence by A1,Th50;
end;
theorem Th51:
for n being non zero Nat holds
PrimeDivisorsFS(n) = sort_a canFS support pfexp n
proof
let n be non zero Nat;
set X = PrimeDivisors(n);
set P = PrimeDivisorsFS(n);
set f = canFS support pfexp n;
set S = sort_a f;
A1: P is FinSequence of REAL by FINSEQ_1:106;
f is FinSequence of REAL by FINSEQ_1:106;
then
A2: S is one-to-one by EUCLID_7:13;
A3: rng P = X by FINSEQ_1:def 14;
rng f = support pfexp n by FUNCT_2:def 3;
then rng S = support pfexp n by CLASSES1:75,RFINSEQ2:def 6;
hence thesis by A1,A2,A3,Th48,INTEGRA3:6;
end;
theorem Th52:
for n being non zero Nat holds
PrimeDivisorsFS(n) = sort_a canFS support ppf n
proof
let n be non zero Nat;
PrimeDivisorsFS(n) = sort_a canFS support pfexp n by Th51;
hence thesis by NAT_3:def 9;
end;
theorem Th53:
for j being Integer st j <> 0
for n being positive Nat st
for i being Nat st i in dom PrimeDivisorsFS(n) holds
j,PrimeDivisorsFS(n).i are_coprime holds
j,n are_coprime
proof
let j be Integer;
assume j <> 0;
then reconsider j1 = |.j.| as non zero Nat;
let n be positive Nat;
set X = PrimeDivisors(n);
set q = PrimeDivisorsFS(n);
assume
A1: for i being Nat st i in dom q holds j,q.i are_coprime;
set N = ppf n;
set J = ppf j1;
A2: now
assume support J meets support N;
then consider y being object such that
A3: y in support J and
A4: y in support N by XBOOLE_0:3;
set C = canFS support N;
q = sort_a C by Th52;
then
A5: rng C = rng q by CLASSES1:75,RFINSEQ2:def 6;
support N = support pfexp n by NAT_3:def 9;
then reconsider y as Prime by A4,NAT_3:34;
support J = support pfexp j1 by NAT_3:def 9;
then
A6: y divides j1 by A3,NAT_3:36;
rng C = support N by FUNCT_2:def 3;
then consider x being object such that
A7: x in dom q and
A8: q.x = y by A4,A5,FUNCT_1:def 3;
j,q.x are_coprime by A1,A7;
hence contradiction by A6,A8,Th10,PYTHTRIP:def 2;
end;
Product N = n & Product J = j1 by NAT_3:61;
hence j,n are_coprime by A2,Th10,INT_7:12;
end;
:: Problem 49 with example solution
theorem Th54:
for m being positive Nat, k being Nat
for S being Sierp49FS of m,k
for q being CR_Sequence st q = PrimeDivisorsFS(m)
ex a,b being positive Nat st 2*k = a-b & a,m are_coprime & b,m are_coprime &
a = CRT(S,q) + Product(q) + 2*k & b = CRT(S,q) + Product(q)
proof
let m be positive Nat;
let k be Nat;
let S be Sierp49FS of m,k;
let q be CR_Sequence such that
A1: q = PrimeDivisorsFS(m);
deffunc F(Integer) = In($1*($1+2*k),INT);
consider f being Function of INT,INT such that
A2: for x being Element of INT holds f.x = F(x) from FUNCT_2:sch 4;
set X = PrimeDivisors(m);
set x0 = CRT(S,q) + 1*Product(q);
take a = x0 + 2*k;
take b = x0;
thus 2*k = a-b;
len S = len q by A1,Def14;
then
A3: dom S = dom q by FINSEQ_3:29;
x0 in INT by INT_1:def 2;
then
A4: f.x0 = F(x0) by A2;
A5: for i being Nat st i in dom q holds f.x0,f.(S.i) are_congruent_mod q.i
proof
let i be Nat such that
A6: i in dom q;
S.i in INT by INT_1:def 2;
then
A7: f.(S.i) = F(S.i) by A2;
CRT(S,q) solves_CRT S,q by A3,Def4;
then x0 solves_CRT S,q by A3,Th30;
then
A8: x0,S.i are_congruent_mod q.i by A3,A6;
then x0+2*k,S.i+2*k are_congruent_mod q.i;
hence thesis by A4,A7,A8,INT_1:18;
end;
A9: for i being Nat st i in dom q holds not f.(S.i),0 are_congruent_mod q.i
proof
let i be Nat;
S.i in INT by INT_1:def 2;
then f.(S.i) = F(S.i) by A2;
hence thesis by A1,A3,Def14;
end;
for i being Nat st i in dom q holds f.x0,q.i are_coprime
proof
let i be Nat such that
A10: i in dom q;
A11: q.i is prime by A1,A10,Th47;
A12: |.q.i.| = q.i;
A13: f.x0,f.(S.i) are_congruent_mod q.i by A5,A10;
not 0,f.(S.i) are_congruent_mod q.i by A9,A10,INT_1:14;
then not 0,f.x0 are_congruent_mod q.i by A13,INT_1:15;
then not f.x0,0 are_congruent_mod q.i by INT_1:14;
then |.f.x0.|,q.i are_coprime by A11,Th4,NUMBER10:4;
hence f.x0,q.i are_coprime by A12,INT_2:34;
end;
then f.x0, m*1 are_coprime by A1,A4,Th53;
hence thesis by A4,NEWTON01:41;
end;
:: Problem 49
theorem
for m being positive Nat, k being Nat
ex a,b being positive Nat st 2*k = a-b & a,m are_coprime & b,m are_coprime
proof
let m be positive Nat;
let k be Nat;
set S = the Sierp49FS of m,k;
set q = PrimeDivisorsFS(m);
per cases;
suppose q is non empty;
then reconsider q as CR_Sequence;
ex a,b being positive Nat st
2*k = a-b & a,m are_coprime & b,m are_coprime &
a = CRT(S,q) + Product(q) + 2*k & b = CRT(S,q) + Product(q) by Th54;
hence thesis;
end;
suppose q is empty;
then
A1: m = 1 by Th50;
take a = 2*k+2;
take b = 2;
thus 2*k = a-b;
thus thesis by A1;
end;
end;
begin :: Problem 120
:: Problem 120
theorem
for m being non zero Nat
ex s being Nat st for n being Nat st n > s holds
(2|^m) * 2|^(2|^n) + 1 is composite
proof
let m be non zero Nat;
set k = 2|^m;
consider s,z being Nat such that
A1: m = (2|^s)*(2*z+1) by NAGATA_2:1;
set h = 2*z+1;
take s;
let n be Nat such that
A2: n > s;
reconsider ns = n-s as non zero Element of NAT by A2,INT_1:5;
0+1 <= k * 2|^(2|^n) by NAT_1:13;
then 1+1 <= k * 2|^(2|^n) + 1 by XREAL_1:6;
hence 2 <= k * 2|^(2|^n) + 1;
A3: k * 2|^(2|^n) = 2|^m * 2|^(2|^n)
.= 2|^(2|^(s+ns)+2|^s*h) by A1,NEWTON:8
.= 2|^(2|^s*2|^ns+2|^s*h) by NEWTON:8
.= 2|^(2|^s*(2|^ns+h))
.= 2|^(2|^s)|^(2|^ns+h) by NEWTON:9;
consider z being Nat such that
A4: 2|^ns + h = 2*z+1 by ABIAN:9;
A5: 2|^(2|^s) + 1|^(2|^ns+h) divides k * 2|^(2|^n) + 1|^(2|^ns+h)
by A3,A4,NEWTON01:35;
A6: 2 is non trivial by NAT_2:def 1;
then 2|^0 < 2|^m by NAT_6:2;
then
A7: 1 < k by NEWTON:4;
2|^s < 2|^n by A2,A6,NAT_6:2;
then 2|^(2|^s) < 2|^(2|^n) by A6,NAT_6:2;
then 1 * 2|^(2|^s) < k * 2|^(2|^n) by A7,XREAL_1:96;
then
A8: 2|^(2|^s) + 1 < k * 2|^(2|^n) + 1 by XREAL_1:6;
2|^(2|^s) + 1 > 0 + 1 by XREAL_1:6;
hence k * 2|^(2|^n) + 1 is non prime by A5,A8;
end;
begin :: Problem 131
definition
let i be Integer;
mode Multiple of i -> Integer means :Def15:
i divides it;
existence;
end;
theorem Th57:
i*j is Multiple of i
proof
i divides i*j;
hence thesis by Def15;
end;
theorem Th58:
j is Multiple of i implies j+h*i is Multiple of i
proof
assume
A1: i divides j;
i divides h*i;
hence i divides j+h*i by A1,WSIERP_1:4;
end;
theorem Th59:
i <> 1 & i <> -1 implies for m being Multiple of i st m is prime holds
m = i or m = -i
proof
assume that
A1: i <> 1 and
A2: i <> -1;
let m be Multiple of i such that
A3: m is prime;
per cases;
suppose i >= 0;
then i in NAT by INT_1:3;
hence thesis by A1,A3,Def15;
end;
suppose i < 0;
then
A4: -i in NAT by INT_1:3;
-i divides m by Def15,INT_2:10;
then -i = 1 or -i = m by A3,A4;
hence thesis by A2;
end;
end;
theorem Th60:
n <> 1 implies for m being Multiple of n st m is prime holds m = n
proof
assume
A1: n <> 1;
let m be Multiple of n such that
A2: m is prime;
m = n or m = -n by A1,A2,Th59;
hence thesis by A2;
end;
definition
let i;
func multiples(i) -> Subset of INT equals
the set of all m where m is Multiple of i;
coherence
proof
set M = the set of all m where m is Multiple of i;
M c= INT
proof
let x be object;
assume x in M;
then ex m being Multiple of i st x = m;
hence thesis by INT_1:def 2;
end;
hence thesis;
end;
end;
theorem Th61:
for x being object holds
x in multiples(i) implies x is Multiple of i
proof
let x be object;
assume x in multiples(i);
then ex m being Multiple of i st x = m;
hence thesis;
end;
theorem Th62:
j in multiples(i) iff i divides j
proof
thus j in multiples(i) implies i divides j
proof
assume j in multiples(i);
then j is Multiple of i by Th61;
hence thesis by Def15;
end;
assume i divides j;
then j is Multiple of i by Def15;
hence thesis;
end;
theorem Th63:
i*j in multiples(i)
proof
i*j is Multiple of i by Th57;
hence thesis;
end;
registration
let i;
cluster multiples(i) -> non empty;
coherence by Th63;
end;
theorem
multiples(0) = { 0 }
proof
set M = multiples(0);
thus M c= {0}
proof
let x be object;
assume x in M;
then reconsider m = x as Multiple of 0 by Th61;
0 divides m by Def15;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {0};
then
A1: x = 0;
0 is Multiple of 0 by Def15;
hence thesis by A1;
end;
theorem
multiples(1) = INT
proof
thus multiples(1) c= INT;
let x be object;
assume x in INT;
then reconsider x as Integer;
x is Multiple of 1 by Def15,INT_2:12;
hence thesis;
end;
theorem
multiples(-1) = INT
proof
thus multiples(-1) c= INT;
let x be object;
assume x in INT;
then reconsider x as Integer;
x is Multiple of -1 by Def15,INT_2:12;
hence thesis;
end;
registration
let i be non zero Integer;
cluster i (#) id INT -> one-to-one;
coherence
proof
set I = id INT;
set f = i(#)I;
let x1,x2 be object;
assume x1 in dom f & x2 in dom f;
then reconsider x1, x2 as Element of INT;
f.x1 = i*I.x1 & f.x2 = i*I.x2 by VALUED_1:6;
hence thesis by XCMPLX_1:5;
end;
end;
theorem Th67:
for i being non zero Integer holds INT,multiples(i) are_equipotent
proof
let i be non zero Integer;
set M = multiples(i);
set I = id INT;
set f = i(#)I;
take f;
thus f is one-to-one;
thus dom f = INT by VALUED_1:def 5;
thus rng f = M
proof
thus rng f c= M
proof
let y be object;
assume y in rng f;
then consider x being object such that
x in dom f and
A1: f.x = y by FUNCT_1:def 3;
reconsider y as Integer by A1;
f.x = i*I.x by VALUED_1:6;
then i divides y by A1;
then y is Multiple of i by Def15;
hence thesis;
end;
let y be object;
assume y in M;
then reconsider m = y as Multiple of i by Th61;
i divides m by Def15;
then consider j such that
A2: m = i*j;
reconsider j as Element of INT by INT_1:def 2;
A3: dom f = INT by VALUED_1:def 5;
f.j = i*I.j by VALUED_1:6
.= y by A2;
hence thesis by A3,FUNCT_1:def 3;
end;
end;
registration
let i be non zero Integer;
cluster multiples(i) -> infinite;
coherence
proof
INT,multiples(i) are_equipotent by Th67;
hence thesis by CARD_1:38;
end;
end;
theorem
i <> 1 & i <> -1 & not i is prime & not -i is prime implies
multiples(i) misses SetPrimes
proof
assume that
A1: i <> 1 and
A2: i <> -1 and
A3: not i is prime and
A4: not -i is prime;
assume multiples(i) meets SetPrimes;
then consider x being object such that
A5: x in multiples(i) and
A6: x in SetPrimes by XBOOLE_0:3;
reconsider m = x as Multiple of i by A5,Th61;
A7: i divides m by Def15;
A8: m is prime by A6,NEWTON:def 6;
per cases;
suppose i >= 0;
then i in NAT by INT_1:3;
hence contradiction by A1,A3,A8,Def15;
end;
suppose i < 0;
then -i in NAT by INT_1:3;
then -i = 1 or -i = x by A7,A8,INT_2:10;
hence contradiction by A2,A4,A6,NEWTON:def 6;
end;
end;
definition :: search operation
let m,n;
func primeNumbers(m,n) -> Subset of NAT equals
seq(m,n) /\ SetPrimes;
coherence;
end;
registration
let m,n;
cluster primeNumbers(m,n) -> finite;
coherence;
end;
theorem Th69:
primeNumbers(0,10) = { 2,3,5,7 }
proof
thus primeNumbers(0,10) c= { 2,3,5,7 }
proof
let x be object;
assume
A1: x in primeNumbers(0,10);
then x in seq(0,10);
then consider k being Element of NAT such that
A2: x = k and
A3: 1+0 <= k & k <= 0+10;
A4: k is prime by A1,A2,NEWTON:def 6;
k = 1 or ... or k = 10 by A3;
hence thesis by A2,A4,ENUMSET1:def 2,XPRIMES0:4,6,8,9,10;
end;
let x be object;
assume x in { 2,3,5,7 };
then
A5: x = 2 or x = 3 or x = 5 or x = 7 by ENUMSET1:def 2;
then
A6: x in SetPrimes by NEWTON:def 6,XPRIMES1:2,3,5,7;
x in seq(0,10) by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
theorem Th70:
primeNumbers(1,10) = { 2,3,5,7,11 }
proof
thus primeNumbers(1,10) c= { 2,3,5,7,11 }
proof
let x be object;
assume
A1: x in primeNumbers(1,10);
then x in seq(1,10);
then consider k being Element of NAT such that
A2: x = k and
A3: 1+1 <= k & k <= 1+10;
k = 2 or ... or k = 11 by A3;
hence thesis by A1,A2,ENUMSET1:def 3,XPRIMES0:4,6,8,9,10,NEWTON:def 6;
end;
let x be object;
assume x in { 2,3,5,7,11 };
then
A4: x = 2 or x = 3 or x = 5 or x = 7 or x = 11 by ENUMSET1:def 3;
then
A5: x in SetPrimes by NEWTON:def 6,XPRIMES1:2,3,5,7,11;
x in seq(1,10) by A4;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th71:
primeNumbers(2,10) = { 3,5,7,11 }
proof
thus primeNumbers(2,10) c= { 3,5,7,11 }
proof
let x be object;
assume
A1: x in primeNumbers(2,10);
then x in seq(2,10);
then consider k being Element of NAT such that
A2: x = k and
A3: 1+2 <= k & k <= 2+10;
k = 3 or ... or k = 12 by A3;
hence thesis by A1,A2,ENUMSET1:def 2,XPRIMES0:4,6,8,9,10,12,NEWTON:def 6;
end;
let x be object;
assume x in { 3,5,7,11 };
then
A4: x = 3 or x = 5 or x = 7 or x = 11 by ENUMSET1:def 2;
then
A5: x in SetPrimes by NEWTON:def 6,XPRIMES1:3,5,7,11;
x in seq(2,10) by A4;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem
primeNumbers(3,10) = { 5,7,11,13 }
proof
thus primeNumbers(3,10) c= { 5,7,11,13 }
proof
let x be object;
assume
A1: x in primeNumbers(3,10);
then x in seq(3,10);
then consider k being Element of NAT such that
A2: x = k and
A3: 1+3 <= k & k <= 3+10;
k = 4 or ... or k = 13 by A3;
hence thesis by A1,A2,ENUMSET1:def 2,XPRIMES0:4,6,8,9,10,12,NEWTON:def 6;
end;
let x be object;
assume x in { 5,7,11,13 };
then
A4: x = 5 or x = 7 or x = 11 or x = 13 by ENUMSET1:def 2;
then
A5: x in SetPrimes by NEWTON:def 6,XPRIMES1:5,7,11,13;
x in seq(3,10) by A4;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th73:
card seq(m,n) = n
proof
card seq(m,n) = card n by CARD_1:5,CALCUL_2:6;
hence thesis;
end;
theorem Th74:
seq(m,n) misses { m+n+1,m+n+2 }
proof
assume seq(m,n) meets { m+n+1,m+n+2 };
then consider x being object such that
A1: x in seq(m,n) and
A2: x in { m+n+1,m+n+2 } by XBOOLE_0:3;
consider k being Element of NAT such that
A3: x = k and
1+m <= k and
A4: k <= m+n by A1;
per cases by A2,TARSKI:def 2;
suppose x = m+n+1;
then m+n+1 <= m+n+0 by A3,A4;
hence contradiction by XREAL_1:6;
end;
suppose x = m+n+2;
then m+n+2 <= m+n+0 by A3,A4;
hence contradiction by XREAL_1:6;
end;
end;
theorem Th75:
a is even implies a is Multiple of 2
proof
assume a is even;
hence 2 divides a;
end;
theorem Th76:
a is even implies a in multiples(2)
proof
assume a is even;
then a is Multiple of 2 by Th75;
hence thesis;
end;
theorem Th77:
a is odd implies not a is Multiple of 2
proof
assume a is odd;
hence not 2 divides a;
end;
theorem
a is odd implies not a in multiples(2)
proof
assume
A1: a is odd;
assume a in multiples(2);
then a is Multiple of 2 by Th61;
hence thesis by A1,Th77;
end;
theorem Th79:
a is even implies multiples(2) /\ {a,a+1} = {a}
proof
set M = multiples(2);
assume
A1: a is even;
thus M /\ {a,a+1} c= {a}
proof
let x be object;
assume
A2: x in M /\ {a,a+1};
then per cases by TARSKI:def 2;
suppose x = a;
hence thesis by TARSKI:def 1;
end;
suppose
A3: x = a+1;
reconsider x as Multiple of 2 by A2,Th61;
2 divides x by Def15;
hence thesis by A3,A1;
end;
end;
let x be object;
assume x in {a};
then
A4: x = a by TARSKI:def 1;
A5: a in M by A1,Th76;
a in {a,a+1} by TARSKI:def 2;
hence thesis by A4,A5,XBOOLE_0:def 4;
end;
theorem Th80:
a is odd implies multiples(2) /\ {a,a+1} = {a+1}
proof
set M = multiples(2);
assume
A1: a is odd;
thus M /\ {a,a+1} c= {a+1}
proof
let x be object;
assume
A2: x in M /\ {a,a+1};
then per cases by TARSKI:def 2;
suppose x = a+1;
hence thesis by TARSKI:def 1;
end;
suppose
A3: x = a;
reconsider x as Multiple of 2 by A2,Th61;
2 divides x by Def15;
hence thesis by A3,A1;
end;
end;
let x be object;
assume x in {a+1};
then
A4: x = a+1 by TARSKI:def 1;
A5: a+1 in M by A1,Th76;
a+1 in {a,a+1} by TARSKI:def 2;
hence thesis by A4,A5,XBOOLE_0:def 4;
end;
theorem
multiples(2) /\ {a,a+1} = {a} or multiples(2) /\ {a,a+1} = {a+1}
by Th79,Th80;
theorem Th82:
card (multiples(2) /\ {a,a+1}) = 1
proof
multiples(2) /\ {a,a+1} = {a} or multiples(2) /\ {a,a+1} = {a+1}
by Th79,Th80;
hence thesis by CARD_1:30;
end;
theorem Th83:
card (multiples(2) /\ seq(k,2*m)) = m
proof
set M = multiples(2);
defpred P[Nat] means card (M /\ seq(k,2*$1)) = $1;
A1: P[0]
proof
seq(k,2*0) = {} by CALCUL_2:2;
hence thesis;
end;
A2: for z being Nat st P[z] holds P[z+1]
proof
let z be Nat;
assume
A3: P[z];
seq(k,2*(z+1)) = seq(k,2*z+1+1)
.= seq(k,2*z+1) \/ {k+(2*z+1)+1} by CALCUL_2:5
.= seq(k,2*z) \/ {k+2*z+1} \/ {k+(2*z+1)+1} by CALCUL_2:5;
then
A4: M /\ seq(k,2*(z+1)) = M /\ (seq(k,2*z) \/ ({k+2*z+1} \/ {k+(2*z+1)+1}))
by XBOOLE_1:4
.= M /\ seq(k,2*z) \/ M /\ ({k+2*z+1} \/ {k+(2*z+1)+1}) by XBOOLE_1:23;
A5: {k+2*z+1} \/ {k+(2*z+1)+1} = {k+2*z+1,k+(2*z+1)+1} by ENUMSET1:1;
seq(k,2*z) misses {k+2*z+1,k+2*z+2} by Th74;
then card (M /\ seq(k,2*z) \/ M /\ ({k+2*z+1} \/ {k+(2*z+1)+1}))
= card (M /\ seq(k,2*z)) + card (M /\ ({k+2*z+1} \/ {k+(2*z+1)+1}))
by A5,XBOOLE_1:76,CARD_2:40;
hence thesis by A3,A4,A5,Th82;
end;
for z being Nat holds P[z] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th84:
n >= 8 implies ex m being Multiple of 3 st m in seq(k,n) & m is odd
proof
assume
A1: n >= 8;
per cases by NUMBER06:18;
suppose 3 divides k;
then
A2: k is Multiple of 3 by Def15;
per cases;
suppose
A3: k is even;
reconsider m = k+1*(2+1) as Multiple of 3 by A2,Th58;
take m;
A4: 1+k <= k+1+2 by NAT_1:12;
3 <= n by A1,XXREAL_0:2;
then k+3 <= k+n by XREAL_1:6;
hence m in seq(k,n) by A4;
m = k+2+1;
hence thesis by A3;
end;
suppose
A5: k is odd;
reconsider m = k+2*(2+1) as Multiple of 3 by A2,Th58;
take m;
A6: 1+k <= k+1+5 by NAT_1:12;
6 <= n by A1,XXREAL_0:2;
then k+6 <= k+n by XREAL_1:6;
hence m in seq(k,n) by A6;
thus thesis by A5;
end;
end;
suppose 3 divides k+1;
then
A7: k+1 is Multiple of 3 by Def15;
per cases;
suppose
A8: k is even;
reconsider m = k+1+2*(2+1) as Multiple of 3 by A7,Th58;
take m;
A9: 1+k <= k+1+6 by NAT_1:12;
7 <= n by A1,XXREAL_0:2;
then k+7 <= k+n by XREAL_1:6;
hence m in seq(k,n) by A9;
thus thesis by A8;
end;
suppose
A10: k is odd;
reconsider m = k+1+1*(2+1) as Multiple of 3 by A7,Th58;
take m;
A11: 1+k <= k+1+3 by NAT_1:12;
4 <= n by A1,XXREAL_0:2;
then k+4 <= k+n by XREAL_1:6;
hence m in seq(k,n) by A11;
m = k+2*2;
hence thesis by A10;
end;
end;
suppose 3 divides k+2;
then
A12: k+2 is Multiple of 3 by Def15;
per cases;
suppose
A13: k is even;
reconsider m = k+2+1*(2+1) as Multiple of 3 by A12,Th58;
take m;
A14: 1+k <= k+1+4 by NAT_1:12;
5 <= n by A1,XXREAL_0:2;
then k+5 <= k+n by XREAL_1:6;
hence m in seq(k,n) by A14;
m = k+2*2+1;
hence thesis by A13;
end;
suppose
A15: k is odd;
reconsider m = k+2+2*(2+1) as Multiple of 3 by A12,Th58;
take m;
A16: 1+k <= k+1+7 by NAT_1:12;
k+8 <= k+n by A1,XREAL_1:6;
hence m in seq(k,n) by A16;
thus thesis by A15;
end;
end;
end;
theorem
for p being Prime holds
p <= k implies multiples(p) /\ seq(k,m) misses primeNumbers(k,m)
proof
let p be Prime;
set A = primeNumbers(k,m);
set D = multiples(p) /\ seq(k,m);
assume
A1: p <= k;
assume D meets A;
then consider x being object such that
A2: x in D and
A3: x in A by XBOOLE_0:3;
A4: x is Multiple of p by A2,Th61;
x in seq(k,m) by A2;
then consider n being Element of NAT such that
A5: x = n and
A6: k+1 <= n and n <= k+m;
A7: p+1 <= k+1 by A1,XREAL_1:6;
n is prime by A3,A5,NEWTON:def 6;
then p = 1 or p = n by A4,A5,Def15;
then p+1 <= p+0 by A6,A7,XXREAL_0:2,INT_2:def 4;
hence thesis by XREAL_1:6;
end;
:: Problem 131 a
theorem
card primeNumbers(0,10) = 4 by Th69,CARD_2:59;
:: Problem 131 b
theorem
card primeNumbers(1,10) = 5
proof
2,3,5,7,11 are_mutually_distinct;
hence thesis by Th70,CARD_2:63;
end;
:: Problem 131 c
theorem
2 <= k implies card primeNumbers(k,10) <= 4
proof
set A = primeNumbers(k,10);
assume 2 <= k;
then per cases by XXREAL_0:1;
suppose k = 2;
hence thesis by Th71,CARD_2:59;
end;
suppose
A1: k > 2;
consider m being Multiple of 3 such that
A2: m in seq(k,10) and
A3: m is odd by Th84;
set D = multiples(2) /\ seq(k,10);
A4: now
assume m in D;
then reconsider m as Multiple of 2 by Th61;
2 divides m by Def15;
hence contradiction by A3;
end;
set W = D \/ {m};
10 = 2*5;
then card D = 5 by Th83;
then
A5: card W = 5 + 1 by A4,CARD_2:41;
A6: card seq(k,10) = 10 by Th73;
A7: k+1 > 2+1 by A1,XREAL_1:6;
now
assume W meets A;
then consider x being object such that
A8: x in W and
A9: x in A by XBOOLE_0:3;
reconsider x as Prime by A9,NEWTON:def 6;
A10: 1+k <= x by A9,CALCUL_2:1;
per cases by A8,XBOOLE_0:def 3;
suppose x in D;
then x = 1 or x = 2 by Th62,INT_2:def 4;
hence contradiction by A7,A10,XXREAL_0:2;
end;
suppose x in {m};
then x = m by TARSKI:def 1;
hence contradiction by A7,A10,Th60;
end;
end;
then
A11: card (W \/ A) = 6 + card A by A5,CARD_2:40;
{m} c= seq(k,10) by A2,ZFMISC_1:31;
then W c= seq(k,10) by XBOOLE_1:8;
then W \/ A c= seq(k,10) by XBOOLE_1:8;
then card A <= 10-6 by A6,A11,XREAL_1:19,NAT_1:43;
hence thesis;
end;
end;
begin :: Problem 144
Lm11:
for D being odd Integer holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 & x,y are_coprime }
is infinite
proof
set G2 = GreaterOrEqualsNumbers(2);
let D be odd Integer;
set A =
{[x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 & x,y are_coprime};
deffunc X(Element of G2) = |. D + 2|^($1-2) .|;
deffunc Y(Element of G2) = 2|^$1;
deffunc Z(Element of G2) = |. D - 2|^($1-2) .|;
defpred P[Element of G2,object] means
ex fx being Element of G2 st fx = 2*$1 & $2 = [X(fx),Y($1),Z(fx)];
A1: for i being Element of G2 ex j being object st P[i,j]
proof
let i be Element of G2;
reconsider i2 = 2*i as Element of G2 by EC_PF_2:def 1,NUMBER09:56;
take [X(i2),Y(i),Z(i2)];
thus thesis;
end;
consider f being ManySortedSet of G2 such that
A2: for d being Element of G2 holds P[d,f.d] from PBOOLE:sch 6(A1);
A3: dom f = G2 by PARTFUN1:def 2;
A4: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A5: k in dom f and
A6: f.k = y by FUNCT_1:def 3;
reconsider k as Element of G2 by A5;
consider fx being Element of G2 such that
A7: fx = 2*k and
A8: f.k = [X(fx),Y(k),Z(fx)] by A2;
A9: 2 <= k by NUMBER09:56;
1*k < 2*k by XREAL_1:68;
then 2 < fx by A7,A9,XXREAL_0:2;
then
A10: fx-2 > fx-fx by XREAL_1:10;
then
A11: X(fx) is positive Element of NAT by INT_1:3;
A12: Z(fx) is positive Element of NAT by A10,INT_1:3;
A13: X(fx)^2 = (D + 2|^(fx-2))^2 by COMPLEX1:75;
A14: Z(fx)^2 = (D - 2|^(fx-2))^2 by COMPLEX1:75;
A15: (2|^(fx-2))|^2 = (2|^(fx-2))^2 by PEPIN:24;
A16: 2*D*2|^(fx-2) = D*(2*2|^(fx-2))
.= D*2|^(fx-2+1) by NEWTON:6;
A17: D*Y(k)^2 = D*(2|^k)|^2 by PEPIN:24
.= D*2|^(k*2) by NEWTON:9;
A18: 2|^(fx-1+1) = 2*2|^(fx-1) by NEWTON:6;
A19: D*2|^(fx-1) - D*2|^(k*2) = -D*2|^(fx-1) by A7,A18
.= -2*D*2|^(fx-2) by A16;
A20: X(fx)^2 - D*Y(k)^2
= D^2 + 2*D*2|^(fx-2) + (2|^(fx-2))|^2 - D*Y(k)^2 by A13,A15
.= D^2 + D*2|^(fx-1) + (2|^(fx-2))|^2 - D*Y(k)^2 by A16
.= Z(fx)^2 by A14,A15,A17,A19;
X(fx),Y(k) are_coprime by A10,PEPIN:18,NAT_5:3;
hence thesis by A6,A8,A11,A12,A20;
end;
f is one-to-one
proof
let x1,x2 be object such that
A21: x1 in dom f & x2 in dom f and
A22: f.x1 = f.x2;
reconsider x1,x2 as Element of G2 by A21;
(ex fx1 being Element of G2 st fx1 = 2*x1 & f.x1 = [X(fx1),Y(x1),Z(fx1)])
&
ex fx2 being Element of G2 st fx2 = 2*x2 & f.x2 = [X(fx2),Y(x2),Z(fx2)]
by A2;
then Y(x1) = Y(x2) by A22,XTUPLE_0:3;
hence thesis by PEPIN:30;
end;
hence thesis by A3,A4,CARD_1:59;
end;
registration
let A be set;
cluster -> even for Element of EvenNAT \ A;
coherence
proof
let e be Element of EvenNAT \ A;
per cases;
suppose EvenNAT \ A = {};
hence thesis by SUBSET_1:def 1;
end;
suppose EvenNAT \ A <> {};
then reconsider e as Element of EvenNAT by XBOOLE_0:def 5;
e is even;
hence thesis;
end;
end;
end;
registration
let A be set;
cluster even for Element of EvenNAT \ A;
existence
proof
per cases;
suppose EvenNAT \ A = {};
then reconsider e = 0 as Element of EvenNAT \ A by SUBSET_1:def 1;
take e;
thus thesis;
end;
suppose EvenNAT \ A <> {};
then consider e being object such that
A1: e in EvenNAT \ A by XBOOLE_0:7;
reconsider e as Element of EvenNAT \ A by A1;
take e;
thus thesis;
end;
end;
end;
Lm12:
for D being even Integer holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 & x,y are_coprime }
is infinite
proof
let D be even Integer;
consider d being Integer such that
A1: D = 2*d by ABIAN:11;
set A =
{[x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 & x,y are_coprime};
set G2 = EvenNAT \ {0};
deffunc X(Element of G2) = |. d/2*$1^2+1 .|;
deffunc Y(Element of G2) = $1;
deffunc Z(Element of G2) = |. d/2*$1^2-1 .|;
deffunc F(Element of G2) = [X($1),Y($1),Z($1)];
consider f being ManySortedSet of G2 such that
A2: for d being Element of G2 holds f.d = F(d) from PBOOLE:sch 5;
A3: dom f = G2 by PARTFUN1:def 2;
A4: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A5: k in dom f and
A6: f.k = y by FUNCT_1:def 3;
reconsider k as Element of G2 by A5;
consider kk being Nat such that
A7: k = 2*kk by ABIAN:def 2;
d/2*k^2+1 = d/2*(2*kk)^2+1 by A7
.= d/2*2*2*kk^2+1
.= d*2*kk^2+1;
then reconsider Xk = X(k) as positive Nat by TARSKI:1;
d/2*k^2-1 = d/2*(2*kk)^2-1 by A7
.= d/2*2*2*kk^2-1
.= d*2*kk^2-1;
then
A8: Z(k) is positive Nat by TARSKI:1;
Z(k)^2 = (d/2*k^2-1)^2 by COMPLEX1:75;
then
A9: Z(k)^2 = (d/2*k^2+1)^2 - 2*d*k^2
.= X(k)^2 - D*Y(k)^2 by A1,COMPLEX1:75;
A10: f.k = F(k) by A2;
2 divides 2*(d*kk^2);
then
A11: 2, 2*d*kk^2+1 are_coprime by NUMBER07:5;
k divides k^2;
then k divides 2*2*kk^2*d by A7,INT_2:2;
then 2*kk divides 2*(2*kk^2*d) by A7;
then kk divides 2*kk^2*d by INT_4:7;
then kk, 2*d*kk^2+1 are_coprime by NUMBER07:5;
then 2*kk, 2*d*kk^2+1 are_coprime by A11,Th16;
then Xk,k are_coprime by A7,INT_6:14;
hence thesis by A6,A8,A9,A10;
end;
f is one-to-one
proof
let x1,x2 be object;
assume x1 in dom f & x2 in dom f;
then reconsider x1,x2 as Element of G2;
f.x1 = F(x1) & f.x2 = F(x2) by A2;
hence thesis by XTUPLE_0:3;
end;
hence thesis by A3,A4,CARD_1:59;
end;
:: Problem 144
theorem
for D being non zero Integer holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 & x,y are_coprime }
is infinite
proof
let D be non zero Integer;
D is odd or D is even;
hence thesis by Lm11,Lm12;
end;
begin :: Problem 148
theorem
for x,y,z being Complex holds
x^2+y^2+z^2+x+y+z = 1 iff (2*x+1)^2+(2*y+1)^2+(2*z+1)^2 = 7;
theorem Th91:
for a,b,c being Integer st (a^2+b^2+c^2) mod 4 = 0 holds
a is even & b is even & c is even
proof
let a,b,c be Integer such that
A1: (a^2+b^2+c^2) mod 4 = 0;
A2: (a^2+b^2+c^2) mod 4 = ((a^2 mod 4)+(b^2 mod 4)+(c^2 mod 4)) mod 4
by NUMBER05:8;
assume not a is even or not b is even or not c is even;
then per cases;
suppose a is odd;
then
A3: a^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose b is even;
then
A4: b^2 mod 4 = 0 by PYTHTRIP:3;
per cases;
suppose c is odd;
then c^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A3,A4,NAT_D:24;
end;
suppose c is even;
then c^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A3,A4;
end;
end;
suppose b is odd;
then
A5: b^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose c is odd;
then c^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A3,A5,NAT_D:24;
end;
suppose c is even;
then c^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A3,A5,NAT_D:24;
end;
end;
end;
suppose b is odd;
then
A6: b^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose a is even;
then
A7: a^2 mod 4 = 0 by PYTHTRIP:3;
per cases;
suppose c is odd;
then c^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A6,A7,NAT_D:24;
end;
suppose c is even;
then c^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A6,A7;
end;
end;
suppose a is odd;
then
A8: a^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose c is odd;
then c^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A6,A8,NAT_D:24;
end;
suppose c is even;
then c^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A6,A8,NAT_D:24;
end;
end;
end;
suppose c is odd;
then
A9: c^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose a is even;
then
A10: a^2 mod 4 = 0 by PYTHTRIP:3;
per cases;
suppose b is odd;
then b^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A9,A10,NAT_D:24;
end;
suppose b is even;
then b^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A9,A10;
end;
end;
suppose a is odd;
then
A11: a^2 mod 4 = 1 by PYTHTRIP:4;
per cases;
suppose b is odd;
then b^2 mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1,A2,A9,A11,NAT_D:24;
end;
suppose b is even;
then b^2 mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1,A2,A9,A11,NAT_D:24;
end;
end;
end;
end;
theorem Th92:
(a^2+b^2+c^2) mod 8 = 0 or (a^2+b^2+c^2) mod 8 = 1 or (a^2+b^2+c^2) mod 8 = 2
or
(a^2+b^2+c^2) mod 8 = 3 or (a^2+b^2+c^2) mod 8 = 4 or (a^2+b^2+c^2) mod 8 = 5
or
(a^2+b^2+c^2) mod 8 = 6
proof
set x = a^2+b^2+c^2;
A1: x mod 8 = ((a^2 mod 8)+(b^2 mod 8)+(c^2 mod 8)) mod 8
by NUMBER05:8;
A2: (1*8+1) mod 8 = 1 mod 8 by NAT_D:21
.= 1 by NAT_D:24;
now
per cases by NUMBER10:61;
case
A3: a^2 mod 8 = 0;
per cases by NUMBER10:61;
case
A4: b^2 mod 8 = 0;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 0 by A1,A3,A4;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 1 by A1,A3,A4;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 4 by A1,A3,A4;
end;
end;
case
A5: b^2 mod 8 = 1;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 1 by A1,A3,A5;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 2 by A1,A3,A5,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 5 by A1,A3,A5,NAT_D:24;
end;
end;
case
A6: b^2 mod 8 = 4;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 4 by A1,A3,A6;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 5 by A1,A3,A6,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 0 by A1,A3,A6,NAT_D:25;
end;
end;
end;
case
A7: a^2 mod 8 = 1;
per cases by NUMBER10:61;
case
A8: b^2 mod 8 = 0;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 1 by A1,A7,A8;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 2 by A1,A7,A8,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 5 by A1,A7,A8,NAT_D:24;
end;
end;
case
A9: b^2 mod 8 = 1;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 2 by A1,A7,A9,NAT_D:24;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 3 by A1,A7,A9,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 6 by A1,A7,A9,NAT_D:24;
end;
end;
case
A10: b^2 mod 8 = 4;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 5 by A1,A7,A10,NAT_D:24;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 6 by A1,A7,A10,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 1 by A2,A1,A7,A10;
end;
end;
end;
case
A11: a^2 mod 8 = 4;
per cases by NUMBER10:61;
case
A12: b^2 mod 8 = 0;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 4 by A1,A11,A12;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 5 by A1,A11,A12,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 0 by A1,A11,A12,NAT_D:25;
end;
end;
case
A13: b^2 mod 8 = 1;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 5 by A1,A11,A13,NAT_D:24;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 6 by A1,A11,A13,NAT_D:24;
end;
case c^2 mod 8 = 4;
hence x mod 8 = 1 by A2,A1,A11,A13;
end;
end;
case
A14: b^2 mod 8 = 4;
per cases by NUMBER10:61;
case c^2 mod 8 = 0;
hence x mod 8 = 0 by A1,A11,A14,NAT_D:25;
end;
case c^2 mod 8 = 1;
hence x mod 8 = 1 by A2,A1,A11,A14;
end;
case c^2 mod 8 = 4;
hence x mod 8 = (1*8+4) mod 8 by A1,A11,A14
.= 4 mod 8 by NAT_D:21
.= 4 by NAT_D:24;
end;
end;
end;
end;
hence thesis;
end;
theorem Th93:
not ex x,y,z being Rational st x^2+y^2+z^2 = 7
proof
given x,y,z being Rational such that
A1: x^2+y^2+z^2 = 7;
consider n1,m1 being Integer such that
A2: m1 > 0 and
A3: x = n1/m1 by RAT_1:2;
consider n2,m2 being Integer such that
A4: m2 > 0 and
A5: y = n2/m2 by RAT_1:2;
consider n3,m3 being Integer such that
A6: m3 > 0 and
A7: z = n3/m3 by RAT_1:2;
set m = m1*m2*m3;
reconsider m as Element of NAT by A2,A4,A6,INT_1:3;
set a = n1*m2*m3;
set b = n2*m1*m3;
set c = n3*m1*m2;
defpred P[Nat] means
$1 <> 0 & ex a,b,c being Integer st 7*$1^2 = a^2+b^2+c^2;
A8: (n1/m1)^2 = n1^2/m1^2 & (n2/m2)^2 = n2^2/m2^2 & (n3/m3)^2 = n3^2/m3^2
by XCMPLX_1:76;
n1^2/m1^2+n2^2/m2^2 = (n1^2*m2^2+n2^2*m1^2)/(m1^2*m2^2)
by A2,A4,XCMPLX_1:116;
then
7 = (((n1^2*m2^2+n2^2*m1^2)*m3^2) + (n3^2*(m1^2*m2^2))) / (m1^2*m2^2*m3^2)
by A1,A2,A3,A4,A5,A6,A7,A8,XCMPLX_1:116
.= (a^2+b^2+c^2) / m^2;
then a^2+b^2+c^2 = 7*m^2 by A2,A4,A6,XCMPLX_1:87;
then
A9: ex k being Nat st P[k] by A2,A4,A6;
consider M being Nat such that
A10: P[M] and
A11: for n being Nat st P[n] holds M <= n from NAT_1:sch 5(A9);
consider a,b,c being Integer such that
A12: 7*M^2 = a^2+b^2+c^2 by A10;
per cases;
suppose M is even;
then consider n being Nat such that
A13: M = 2*n;
A14: 4*(7*n^2) mod 4 = 0;
a is even by A13,A12,A14,Th91;
then consider a1 being Integer such that
A15: a = 2*a1 by ABIAN:11;
b is even by A13,A12,A14,Th91;
then consider b1 being Integer such that
A16: b = 2*b1 by ABIAN:11;
c is even by A13,A12,A14,Th91;
then consider c1 being Integer such that
A17: c = 2*c1 by ABIAN:11;
A18: n <> 0 by A10,A13;
a1^2+b1^2+c1^2 = (a/2)^2+(b/2)^2+(c/2)^2 by A15,A16,A17
.= (7*M^2)/4 by A12
.= 7*n^2 by A13;
then 2*n <= 1*n by A18,A11,A13;
hence contradiction by A18,XREAL_1:68;
end;
suppose M is odd;
then M^2 mod 8 = 1 by NUMBER05:41;
then 7*M^2 mod 8 = ((7 mod 8)*1) mod 8 by NAT_D:67
.= 7 by NAT_D:24;
hence contradiction by A12,Th92;
end;
end;
:: Problem 148
theorem
not ex x,y,z being Rational st x^2+y^2+z^2+x+y+z = 1
proof
given x,y,z being Rational such that
A1: x^2+y^2+z^2+x+y+z = 1;
(2*x+1)^2+(2*y+1)^2+(2*z+1)^2 = 7 by A1;
hence contradiction by Th93;
end;
begin :: Problem 149
:: Problem 149 a
theorem
not ex x,y,z being positive Integer st 4*x*y-x-y = z^2
proof
given x,y,z being positive Integer such that
A1: 4*x*y-x-y = z^2;
consider p,k being Nat such that
A2: p = 4*k+3 and
A3: p is prime and
A4: p divides 4*(x-1)+3 by NUMBER05:3;
reconsider p as Prime by A3;
A5: p > 1 by INT_2:def 4;
A6: p-1 <> 1 by A2;
A7: Euler p = p-1 by EULER_1:20;
A8: (2*z)|^(p-1) = (2*z)|^(2*(2*k+1)) by A2
.= (2*z)|^2|^(2*k+1) by NEWTON:9;
A9: (2*z)|^2 = (2*z)^2 by WSIERP_1:1;
A10: (4*x-1)*(4*y-1) = (2*z)^2+1 by A1;
then
A11: p divides (2*z)^2+1 by A4,INT_2:2;
(2*z)^2,-1 are_congruent_mod p by A4,A10,INT_2:2;
then (2*z)^2|^(2*k+1),(-1)|^(2*k+1) are_congruent_mod p by GR_CY_3:34;
then
A12: (2*z)|^2|^(2*k+1) mod p = (-1) mod p by A9,NAT_D:64
.= p-1 by NUMBER10:5;
2*z,p are_coprime
proof
let w be Prime;
assume that
A13: w divides 2*z and
A14: w divides p;
w > 1 by INT_2:def 4;
then w = p by A14,INT_2:def 4;
then p divides (2*z)^2 by A13,INT_2:2;
then p divides (2*z)^2+1-(2*z)^2 by A11,INT_5:1;
hence contradiction by A5,WSIERP_1:15;
end;
hence contradiction by A6,A7,A8,A12,INT_2:def 4,EULER_2:18;
end;
deffunc X(Nat) = -1;
deffunc Y(Nat) = -5*$1^2-2*$1;
deffunc Z(Nat) = -5*$1-1;
deffunc F(Nat) = [X($1),Y($1),Z($1)];
definition
func exampleSierpinski149 -> Function of NATPLUS, [:INT,INT,INT:] means
:Def18:
for n being non zero Nat holds it.n = [-1,-5*n^2-2*n,-5*n-1];
existence
proof
deffunc F1(Nat) = In(F($1),[:INT,INT,INT:]);
consider f being Function of NATPLUS, [:INT,INT,INT:] such that
A1: for x being Element of NATPLUS holds f.x = F1(x) from FUNCT_2:sch 4;
take f;
let n be non zero Nat;
n in NATPLUS by NAT_LAT:def 6;
hence f.n = F1(n) by A1
.= F(n);
end;
uniqueness
proof
let f,g be Function of NATPLUS, [:INT,INT,INT:] such that
A2: for n being non zero Nat holds f.n = F(n) and
A3: for n being non zero Nat holds g.n = F(n);
let n be Element of NATPLUS;
thus f.n = F(n) by A2
.= g.n by A3;
end;
end;
set f = exampleSierpinski149;
registration
cluster exampleSierpinski149 -> one-to-one;
coherence
proof
let x1,x2 be object;
assume that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
reconsider x1,x2 as Element of NATPLUS by A1;
f.x1 = F(x1) & f.x2 = F(x2) by Def18;
then -5*x1-1 = -5*x2-1 by A2,XTUPLE_0:3;
hence thesis;
end;
end;
theorem Th96:
rng exampleSierpinski149 c=
{ [x,y,z] where x,y,z is negative Integer: 4*x*y-x-y = z^2 }
proof
let y be object;
assume y in rng f;
then consider k being object such that
A1: k in dom f and
A2: f.k = y by FUNCT_1:def 3;
reconsider k as Element of NATPLUS by A1;
4*X(k)*Y(k)-X(k)-Y(k) = Z(k)^2;
then F(k) in { [x,y,z] where x,y,z is negative Integer: 4*x*y-x-y = z^2 };
hence thesis by A2,Def18;
end;
:: Problem 149 b
theorem
{ [x,y,z] where x,y,z is negative Integer: 4*x*y-x-y = z^2 } is infinite
proof
dom f = NATPLUS by PARTFUN1:def 2;
hence thesis by Th96,CARD_1:59;
end;
begin :: Problem 150
definition
let m,D be Complex;
set R = [:COMPLEX,COMPLEX:];
func exampleSierpinski150(m,D) -> sequence of [:COMPLEX,COMPLEX:] means
:Def19:
it.0 = [ 2*m^2+1 , 2*m ] &
for n being Nat holds
it.(n+1) = [ (it.n)`1^2+D*(it.n)`2^2 , 2*(it.n)`1*(it.n)`2 ];
existence
proof
defpred P[Nat,Element of R,Element of R] means
$3 = [$2`1^2+D*$2`2^2,2*$2`1*$2`2];
A1: for n being Nat for x being Element of R
ex y being Element of R st P[n,x,y]
proof
let n be Nat;
let x be Element of R;
take In([In(x`1^2+D*x`2^2,COMPLEX),In(2*x`1*x`2,COMPLEX)],R);
thus thesis;
end;
ex f being sequence of R st
f.0 = In([In(2*m^2+1,COMPLEX),In(2*m,COMPLEX)],R) &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let f,g be sequence of R such that
A2: f.0 = [ 2*m^2+1 , 2*m ] and
A3: for n being Nat holds
f.(n+1) = [ (f.n)`1^2+D*(f.n)`2^2 , 2*(f.n)`1*(f.n)`2 ] and
A4: g.0 = [ 2*m^2+1 , 2*m ] and
A5: for n being Nat holds
g.(n+1) = [ (g.n)`1^2+D*(g.n)`2^2 , 2*(g.n)`1*(g.n)`2 ];
defpred P[Nat] means f.$1 = g.$1;
A6: P[0] by A2,A4;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A8: P[k];
thus f.(k+1) = [ (f.k)`1^2+D*(f.k)`2^2 , 2*(f.k)`1*(f.k)`2 ] by A3
.= g.(k+1) by A5,A8;
end;
A9: for k being Nat holds P[k] from NAT_1:sch 2(A6,A7);
let n be Element of NAT;
thus thesis by A9;
end;
end;
registration
let m,D be Real;
cluster exampleSierpinski150(m,D) -> [:REAL,REAL:]-valued;
coherence
proof
set f = exampleSierpinski150(m,D);
set A = REAL;
thus rng f c= [:A,A:]
proof
let y be object;
assume y in rng f;
then consider n being Element of NAT such that
A1: f.n = y by FUNCT_2:113;
defpred P[Nat] means f.$1 in [:A,A:];
A2: P[0]
proof
f.0 = In([In(2*m^2+1,A),In(2*m,A)],[:A,A:]) by Def19;
hence thesis;
end;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then reconsider fn = f.n as Element of [:A,A:];
f.(n+1) = In([In((fn)`1^2+D*(fn)`2^2,A),In(2*(fn)`1*(fn)`2,A)],[:A,A:])
by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
end;
end;
registration
let m,D be Rational;
cluster exampleSierpinski150(m,D) -> [:RAT,RAT:]-valued;
coherence
proof
set f = exampleSierpinski150(m,D);
set A = RAT;
thus rng f c= [:A,A:]
proof
let y be object;
assume y in rng f;
then consider n being Element of NAT such that
A1: f.n = y by FUNCT_2:113;
defpred P[Nat] means f.$1 in [:A,A:];
A2: P[0]
proof
reconsider r = 2*m^2+1, s = 2*m as Rational;
f.0 = In([In(r,A),In(s,A)],[:A,A:]) by Def19;
hence thesis;
end;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then reconsider fn = f.n as Element of [:A,A:];
reconsider r = (fn)`1^2+D*(fn)`2^2, s = 2*(fn)`1*(fn)`2 as Rational;
f.(n+1) = In([In(r,A),In(s,A)],[:A,A:]) by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
end;
end;
registration
let m,D be Integer;
cluster exampleSierpinski150(m,D) -> [:INT,INT:]-valued;
coherence
proof
set f = exampleSierpinski150(m,D);
set A = INT;
thus rng f c= [:A,A:]
proof
let y be object;
assume y in rng f;
then consider n being Element of NAT such that
A1: f.n = y by FUNCT_2:113;
defpred P[Nat] means f.$1 in [:A,A:];
A2: P[0]
proof
f.0 = In([In(2*m^2+1,A),In(2*m,A)],[:A,A:]) by Def19;
hence thesis;
end;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then reconsider fn = f.n as Element of [:A,A:];
f.(n+1) = In([In((fn)`1^2+D*(fn)`2^2,A),In(2*(fn)`1*(fn)`2,A)],[:A,A:])
by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
end;
end;
registration
let m,D be Nat;
cluster exampleSierpinski150(m,D) -> [:NAT,NAT:]-valued;
coherence
proof
set f = exampleSierpinski150(m,D);
set A = NAT;
thus rng f c= [:A,A:]
proof
let y be object;
assume y in rng f;
then consider n being Element of NAT such that
A1: f.n = y by FUNCT_2:113;
defpred P[Nat] means f.$1 in [:A,A:];
A2: P[0]
proof
f.0 = In([In(2*m^2+1,A),In(2*m,A)],[:A,A:]) by Def19;
hence thesis;
end;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then reconsider fn = f.n as Element of [:A,A:];
f.(n+1) = In([In((fn)`1^2+D*(fn)`2^2,A),In(2*(fn)`1*(fn)`2,A)],[:A,A:])
by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
end;
end;
registration
let m,D be positive natural Number;
let n be Nat;
set f = exampleSierpinski150(m,D);
cluster (exampleSierpinski150(m,D).n)`1 -> positive;
coherence
proof
defpred P[Nat] means (f.$1)`1 > 0;
A1: P[0]
proof
f.0 = [2*m^2+1,2*m] by Def19;
hence thesis;
end;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
f.(k+1) = [ (f.k)`1^2+D*(f.k)`2^2 , 2*(f.k)`1*(f.k)`2 ] by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
cluster (exampleSierpinski150(m,D).n)`2 -> positive;
coherence
proof
defpred P[Nat] means (f.$1)`2 > 0;
A3: P[0]
proof
f.0 = [2*m^2+1,2*m] by Def19;
hence thesis;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
f.(k+1) = [ (f.k)`1^2+D*(f.k)`2^2 , 2*(f.k)`1*(f.k)`2 ] by Def19;
hence thesis;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
end;
theorem Th98:
for m,D being positive natural Number, a,b being Nat st a < b holds
(exampleSierpinski150(m,D).a)`1 < (exampleSierpinski150(m,D).b)`1 &
(exampleSierpinski150(m,D).a)`2 < (exampleSierpinski150(m,D).b)`2
proof
let m,D be positive natural Number;
let a,b be Nat such that
A1: a < b;
set f = exampleSierpinski150(m,D);
defpred P[Nat] means
$1 > a implies (f.$1)`1 > (f.a)`1 & (f.$1)`2 > (f.a)`2;
A2: P[0];
A3: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume that
A4: P[k] and
A5: k+1 > a;
A6: f.(k+1) = [ (f.k)`1^2+D*(f.k)`2^2 , 2*(f.k)`1*(f.k)`2 ] by Def19;
A7: (f.k)`1 >= 0+1 by NAT_1:13;
then 2*(f.k)`1 >= 2*1 by XREAL_1:64;
then
A8: 2*(f.k)`1 > 1 by XXREAL_0:2;
A9: (f.k)`1^2 >= 1*(f.k)`1 by A7,XREAL_1:64;
k >= a by A5,NAT_1:13;
then per cases by XXREAL_0:1;
suppose
A10: k > a;
(f.k)`1^2 + D*(f.k)`2^2 >= (f.k)`1 + 0 by A9,XREAL_1:7;
hence (f.(k+1))`1 > (f.a)`1 by A4,A6,A10,XXREAL_0:2;
2*(f.k)`1*(f.k)`2 >= (f.k)`2*1 by A8,XREAL_1:68;
hence (f.(k+1))`2 > (f.a)`2 by A4,A6,A10,XXREAL_0:2;
end;
suppose
A11: k = a;
(f.k)`1^2 + D*(f.k)`2^2 > (f.k)`1 + 0 by A9,XREAL_1:8;
hence (f.(k+1))`1 > (f.a)`1 by A6,A11;
2*(f.k)`1 * (f.k)`2 > 1 * (f.k)`2 by A8,XREAL_1:68;
hence (f.(k+1))`2 > (f.a)`2 by A6,A11;
end;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
registration
let m,D be positive natural Number;
cluster exampleSierpinski150(m,D) -> one-to-one;
coherence
proof
set f = exampleSierpinski150(m,D);
let x1,x2 be object such that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
reconsider x1,x2 as Element of NAT by A1;
now
assume x1 <> x2;
then x1 < x2 or x2 < x1 by XXREAL_0:1;
then (f.x1)`1 < (f.x2)`1 or (f.x2)`1 < (f.x1)`1 by Th98;
hence contradiction by A2;
end;
hence thesis;
end;
end;
:: Problem 150
theorem
for D,m being positive Integer st D = m^2+1 holds
{ [x,y] where x,y is positive Integer: x^2 - D*y^2 = 1 } is infinite
proof
let D,m be positive Integer such that
A1: D = m^2+1;
set f = exampleSierpinski150(m,D);
defpred R[Complex,Complex] means $1^2-D*$2^2 = 1;
set A = {[x,y] where x,y is positive Integer: R[x,y]};
A2: R[2*m^2+1,2*m] by A1;
then [2*m^2+1,2*m] in A;
then reconsider A as non empty set;
deffunc F(Real,Real) = $1^2+D*$2^2;
deffunc G(Real,Real) = 2*$1*$2;
A3: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [2*m^2+1,2*m] by Def19;
then
A4: N[0] by A2;
A5: for a being Nat holds N[a] implies N[a+1]
proof
let a be Nat;
assume N[a];
then consider x,y being positive Integer such that
A6: f.a = [x,y] & R[x,y];
A7: f.(a+1) = [F((f.a)`1,(f.a)`2),G((f.a)`1,(f.a)`2)] by Def19;
(x^2+D*y^2)^2 - D*(2*x*y)^2 = (x^2-D*y^2)^2;
hence thesis by A6,A7;
end;
A8: for a being Nat holds N[a] from NAT_1:sch 2(A4,A5);
rng f c= A
proof
let y be object;
assume y in rng f;
then ex k being object st k in dom f & f.k = y by FUNCT_1:def 3;
hence thesis by A8;
end;
hence thesis by A3,CARD_1:59;
end;
begin :: Problem 151
theorem Th100:
2|^2 <= n & 2|^n divides i|^3 implies 2|^2 divides i
proof
per cases;
suppose i = 0;
hence thesis by INT_2:12;
end;
suppose
A1: i <> 0;
assume
A2: 2|^2 <= n;
assume 2|^n divides i|^3;
then 2|^n divides |.i|^3.| by Th4;
then
A3: 2|^n divides |.i.||^3 by TAYLOR_2:1;
consider a being Nat, b being odd Nat such that
A4: |.i.| = b * 2|^a by A1,NAT_6:3;
A5: |.i.||^3 = b|^3 * 2|^a|^3 by A4,NEWTON:7;
A6: b|^3,2|^n are_coprime by NAT_5:3;
2|^a|^3 = 2|^(3*a) by NEWTON:9;
then n <= 3*a by A3,A5,A6,INT_2:25,PEPIN:31;
then
A7: 2|^2 <= 3*a by A2,XXREAL_0:2;
now
assume a < 1+1;
then a <= 1 by NAT_1:13;
then 3*a <= 3*1 by XREAL_1:64;
hence contradiction by A7,Lm1,XXREAL_0:2;
end;
then 2|^2 divides |.i.| by A4,INT_2:2,PEPIN:31;
hence thesis by Th4;
end;
end;
theorem Th101:
2|^3 <= n & 2|^n divides i|^3 implies 2|^3 divides i
proof
per cases;
suppose i = 0;
hence thesis by INT_2:12;
end;
suppose
A1: i <> 0;
assume
A2: 2|^3 <= n;
assume 2|^n divides i|^3;
then 2|^n divides |.i|^3.| by Th4;
then
A3: 2|^n divides |.i.||^3 by TAYLOR_2:1;
consider a being Nat, b being odd Nat such that
A4: |.i.| = b * 2|^a by A1,NAT_6:3;
A5: |.i.||^3 = b|^3 * 2|^a|^3 by A4,NEWTON:7;
A6: b|^3,2|^n are_coprime by NAT_5:3;
2|^a|^3 = 2|^(3*a) by NEWTON:9;
then n <= 3*a by A3,A5,A6,INT_2:25,PEPIN:31;
then
A7: 2|^3 <= 3*a by A2,XXREAL_0:2;
now
assume a < 2+1;
then a <= 2 by NAT_1:13;
then 3*a <= 3*2 by XREAL_1:64;
hence contradiction by A7,Lm2,XXREAL_0:2;
end;
then 2|^3 divides |.i.| by A4,INT_2:2,PEPIN:31;
hence thesis by Th4;
end;
end;
theorem Th102:
i,j are_coprime & p|^n divides i*j implies p|^n divides i or p|^n divides j
proof
assume i,j are_coprime;
then
A1: |.i.|,|.j.| are_coprime by INT_2:34;
assume p|^n divides i*j;
then p|^n divides |.i*j.| by Th4;
then p|^n divides |.i.|*|.j.| by COMPLEX1:65;
then p|^n divides |.i.| or p|^n divides |.j.| by A1,NUMBER08:107;
hence thesis by Th4;
end;
theorem Th103:
n is odd & i,j are_coprime & i*j = z|^n implies ex k be Integer st i = k|^n
proof
assume
A1: n is odd;
assume i,j are_coprime;
then
A2: |.i.|,|.j.| are_coprime by INT_2:34;
assume
A3: i*j = z|^n;
A4: |.i.|*|.j.| = |.i*j.| by COMPLEX1:65;
|.z|^n.| = |.z.||^n by TAYLOR_2:1;
then consider k being Nat such that
A5: k|^n = |.i.| by A2,A3,A4,NEWTON02:30;
per cases;
suppose
A6: i >= 0;
take k;
thus k|^n = i by A5,A6,ABSVALUE:def 1;
end;
suppose i <= 0;
then
A7: |.i.| = -i by ABSVALUE:30;
take -k;
thus (-k)|^n = -(k|^n) by A1,POWER:2
.= i by A5,A7;
end;
end;
theorem Th104:
n is odd implies
for r,s being negative Real holds r <= s implies r|^n <= s|^n
proof
assume
A1: n is odd;
let r,s be negative Real;
assume r <= s;
then (-1)*r >= (-1)*s by XREAL_1:65;
then
A2: (-r)|^n >= (-s)|^n by NEWTON02:41;
(-r)|^n = -r|^n & (-s)|^n = -s|^n by A1,POWER:2;
then (-1)*(-r|^n) <= (-1)*(-s|^n) by A2,XREAL_1:65;
hence thesis;
end;
theorem Th105:
0 <= j & j^2 < z < (j+1)^2 implies not ex i being Integer st z = i^2
proof
assume that
A1: j >= 0 and
A2: j^2 < z and
A3: z < (j+1)^2;
given i such that
A4: i^2 = z;
sqrt (j^2) = j by A1,SQUARE_1:22;
then
A5: j < sqrt z by A2,SQUARE_1:27;
sqrt (j+1)^2 = j+1 by A1,SQUARE_1:22;
then sqrt(i^2) < j+1 by A3,A4,SQUARE_1:27;
hence thesis by A4,A5,INT_1:7;
end;
Lm13:
not ex i being Integer st i^2 = 464
proof
21^2 < 464 < (21+1)^2;
hence thesis by Th105;
end;
:: Problem 151
theorem
{ [x,y] where x,y is Integer: y|^2 = x|^3+(x+4)|^2 } = { [0,4], [0,-4] }
proof
set A = { [x,y] where x,y is Integer: y|^2 = x|^3+(x+4)|^2 };
thus A c= { [0,4], [0,-4] }
proof
let e be object;
assume e in A;
then consider x,y being Integer such that
A1: e = [x,y] and
A2: y|^2 = x|^3+(x+4)|^2;
A3: y|^2 = y^2 by WSIERP_1:1;
A4: 4|^2 = 4^2 by WSIERP_1:1;
per cases;
suppose
A5: x = 0;
then y = 4 or y = -4 by A2,A3,A4,SQUARE_1:40;
hence thesis by A1,A5,TARSKI:def 2;
end;
suppose
A6: x <> 0;
set d = (y-x-4) gcd (y+x+4);
A7: (x+4)|^2 = (x+4)^2 by WSIERP_1:1;
then
A8: x|^3 = (y-x-4)*(y+x+4) by A2,A3;
then
A9: y-x-4 <> 0 & y+x+4 <> 0 by A6;
A10: d divides y-x-4 by INT_2:def 2;
A11: d divides y+x+4 by INT_2:def 2;
A12: d divides (y-x-4)*(y+x+4) by A11,INT_2:2;
A13: d divides (y+x+4)-(y-x-4) by A10,A11,INT_5:1;
A14: x|^3 = x*x*x by POLYEQ_5:2;
A15: not ex p being odd Prime st p divides d
proof
given p being odd Prime such that
A16: p divides d;
A17: p divides 2*(x+4) by A13,A16,INT_2:2;
p divides (y-x-4)*(y+x+4) by A12,A16,INT_2:2;
then
A18: p divides x by A2,A3,A7,Th6;
A19: p divides x+y+4 by A11,A16,INT_2:2;
A20: p divides x+4 or ex z being Integer st p = z*2 & z divides x+4
by A17,Th8,XPRIMES1:2;
p divides y-x-4 by A10,A16,INT_2:2;
then p divides y-x-4+(x+4) by A20,WSIERP_1:4;
then p divides x+y by A18,WSIERP_1:4;
then p divides (y+x+4)-(x+y) by A19,INT_5:1;
then p = 1 or p = 2*1 or p = 2*2 by NUMBER05:21;
hence contradiction by INT_2:def 4;
end;
consider E being Nat, b being odd Nat such that
A21: d = b * 2|^E by A9,NAT_6:3;
A22: now
assume b <> 1;
then consider p being Element of NAT such that
A23: p is prime and
A24: p divides b by INT_2:31,NAT_1:23;
p is odd by A24;
hence contradiction by A15,A21,A23,A24,INT_2:2;
end;
consider m,n being Integer such that
A25: y-x-4 = d*m and
A26: y+x+4 = d*n and
A27: m,n are_coprime by A9,INT_2:23;
A28: 3 = 2*1+1;
per cases;
suppose
A29: 16 divides d;
then
A30: 16*16 divides d*d by NAT_3:1;
d*d divides (y-x-4)*(y+x+4) by A10,A11,NAT_3:1;
then 2|^8 divides x|^3 by A2,A3,A7,A30,Lm4,INT_2:9;
then 2|^3 divides x by Lm2,Th101;
then
A31: 2*2*2*2 divides 2*x by Lm2,NAT_3:1;
16 divides 2*x+8 by A13,A29,INT_2:9;
then 16 divides 2*x+8-2*x by A31,INT_5:1;
hence thesis by NAT_D:7;
end;
suppose not 2*2*2*2 divides d;
then not 2|^4 divides 2|^E by A21,A22,POLYEQ_5:3;
then 3+1 > E by NEWTON:89;
then E <= 3 by NAT_1:13;
then E = 0 or ... or E = 3;
then per cases;
suppose E = 0;
then
A32: y-x-4,y+x+4 are_coprime by A21,A22;
then consider a being Integer such that
A33: y-x-4 = a|^3 by A8,A28,Th103;
consider b being Integer such that
A34: y+x+4 = b|^3 by A8,A28,A32,Th103;
x|^3 = (a*b)|^3 by A8,A33,A34,NEWTON:7;
then
A35: x = a*b by A28,NEWTON03:13;
A36: 2*x+8 = b|^3-a|^3 by A33,A34;
A37: a|^3 = a*a*a by POLYEQ_5:2;
A38: b|^3 = b*b*b by POLYEQ_5:2;
per cases;
suppose a = b;
then 2*x+8 = 0 by A36;
then y|^2 = (-4)*(-4)*(-4)+0 by A2,POLYEQ_5:2;
hence thesis;
end;
suppose
A39: a <> b;
per cases;
suppose a*b = 0;
hence thesis by A6,A35;
end;
suppose
A40: a*b > 0;
A41: 2*a*b+8 = b|^3-a|^3 by A33,A34,A35
.= (b-a)*((b-a)^2+3*a*b) by A37,A38;
A42: b-a <> 1
proof
assume b-a = 1;
then 2*a*b+8 = 1+3*a*b by A41;
then y^2 = 7|^3+(7+4)^2 by A2,A3,A35,WSIERP_1:1
.= 7*7*7+121 by POLYEQ_5:2
.= 464;
hence contradiction by Lm13;
end;
A43: 3*(a*b) > 0 by A40;
then
A44: (b-a)^2+3*a*b >= 0;
2*(a*b) > 0 by A40;
then b-a > 0 by A41,A44;
then b-a >= 0+1 by NAT_1:13;
then b-a > 1 by A42,XXREAL_0:1;
then
A45: b-a >= 1+1 by NAT_1:13;
then
A46: (b-a)*((b-a)^2+3*a*b) >= 2*((b-a)^2+3*a*b) by A43,XREAL_1:64;
2*(b-a)^2+6*a*b > 0+6*a*b by A45,XREAL_1:6;
then (b-a)*((b-a)^2+3*a*b) > 6*a*b by A46,XXREAL_0:2;
then 6*a*b-2*a*b < 2*a*b+8-2*a*b by A41,XREAL_1:8;
then 4*(a*b) < 4*2;
then a*b = 1 by A40,NAT_1:23,XREAL_1:64;
then a = 1 & b = 1 or a = -1 & b = -1 by INT_1:9;
hence thesis by A39;
end;
suppose a*b < 0;
then per cases by XREAL_1:133;
suppose that
A47: a > 0 and
A48: b < 0;
A49: (-b)|^3 = -b|^3 by A28,POWER:2;
A50: (-b)|^3 = (-b)*(-b)*(-b) by POLYEQ_5:2;
0+1 <= a by A47,NAT_1:13;
then
A51: a*a*a >= a*a*1 by XREAL_1:64;
-b >= 0+1 by A48,NAT_1:13;
then b^2*(-b) >= b^2*1 by XREAL_1:64;
then
A52: a|^3+(-b)|^3 >= a^2+(-b)^2 by A37,A50,A51,XREAL_1:7;
a^2+(-b)^2+2*a*b = (a+b)^2;
then
a^2+(-b)^2+2*a*b-2*a*b >= 0-2*a*b by XREAL_1:9;
then
A53: a|^3-b|^3 >= -2*a*b by A49,A52,XXREAL_0:2;
A54: a|^3-b|^3 = -2*a*b-8 by A33,A34,A35;
-2*a*b-8 < -2*a*b-0 by XREAL_1:8;
hence thesis by A53,A54;
end;
suppose that
A55: a < 0 and
A56: b > 0;
b|^3 = a|^3+2*a*b+8 by A33,A34,A35;
then b|^3-8 < 0 by A37,A55,A56;
then b|^3 < 0+8 by XREAL_1:19;
then b = 1 by A56,Lm2,NAT_1:23,PREPOWER:9;
then
A57: 1|^3 = a|^3+2*a*1+8 by A33,A34,A35;
a <= 0-1 by A55,INT_1:52;
then per cases by XXREAL_0:1;
suppose a = -1;
hence thesis by A37,A57;
end;
suppose a < -1;
then
A58: a <= -1-1 by INT_1:52;
then a|^3 <= (-2)|^3 by A28,Th104;
then
A59: a|^3 <= (-2)*(-2)*(-2) by POLYEQ_5:2;
2*a <= 2*(-2) by A58,XREAL_1:64;
then a|^3+2*a <= -8+-4 by A59,XREAL_1:7;
then a|^3+2*a+7 <= -12+7 by XREAL_1:6;
hence thesis by A57;
end;
end;
end;
end;
end;
suppose
A60: E = 1;
then
A61: d = 2 by A21,A22;
A62: 2 divides x by A2,A3,A7,A12,A21,A22,A60,Th6,XPRIMES1:2;
A63: 2 divides y-x-4 by A21,A22,A25,A60;
2 divides 2*2;
then 2 divides y-x-4+4 by A63,WSIERP_1:4;
then 2 divides y-x+x by A62,WSIERP_1:4;
then
A64: 2 divides m+n by A25,A26,A61;
A65: now
per cases;
case m is odd & n is odd;
hence m is odd & n is odd;
end;
case m is even & n is odd;
hence contradiction by A64;
end;
case m is odd & n is even;
hence contradiction by A64;
end;
case m is even & n is even;
hence contradiction by A27,NEWTON05:35;
end;
end;
then consider m1 being Integer such that
A66: m = 2*m1+1 by ABIAN:1;
consider n1 being Integer such that
A67: n = 2*n1+1 by A65,ABIAN:1;
set u = 8*(m1*(2*n1+1)+n1);
A68: x|^3 = (2*m)*(2*n) by A8,A21,A22,A25,A26,A60
.= u+4 by A66,A67;
(u+4) mod 8 = ((u mod 8)+(4 mod 8)) mod 8 by NAT_D:66
.= (0+(4 mod 8)) mod 8
.= 4 by NAT_D:24;
then not 8 divides x|^3 by A68;
hence thesis by A62,Lm2,NEWTON02:15;
end;
suppose E = 2;
then
A69: d = 2^2 by A21,A22,WSIERP_1:1;
then
A70: x|^3 = (4*m)*(4*n) by A8,A25,A26
.= 16*(m*n);
then 2|^4 divides x|^3 by Lm3;
then
A71: 4 divides x by Lm1,Th100;
then consider w being Integer such that
A72: x = 4*w;
x*x*x = 16*4*w*w*w by A72;
then m*n = 4*(w*w*w) by A70,A14;
then
A73: 4 divides m*n;
A74: 4 divides y+x by A11,A69,INT_2:1;
A75: 2 divides 2*2;
4 divides m & n is odd or 4 divides n & m is odd
proof
assume not 4 divides m or n is even;
then per cases;
suppose that
A76: not 4 divides m and
A77: n is odd;
thus 4 divides n by A27,A73,A76,Lm1,Th102,XPRIMES1:2;
hence thesis by A75,A77;
end;
suppose that
A78: not 4 divides m and
A79: n is even;
thus 4 divides n by A27,A73,A78,Lm1,Th102,XPRIMES1:2;
thus m is odd by A27,A79,NEWTON05:35;
end;
suppose that
A80: 4 divides m and
A81: n is even;
2 divides m by A75,A80,INT_2:2;
then 2 divides 1 by A81,A27,INT_2:def 2;
hence thesis by NAT_D:7;
end;
end;
then per cases;
suppose that
A82: 4 divides m and
A83: n is odd;
consider n1 being Integer such that
A84: n = 2*n1+1 by A83,ABIAN:1;
A85: 4 divides 4*n1;
4 divides 2*(2*n1)+2*(m+1) by A74,A84,A25,A26,A69,A71,INT_2:1;
then
A86: 4 divides 2*m+2*1 by A85,INT_2:1;
4 divides 2*m by A82,INT_2:2;
hence thesis by A86,INT_2:1,NAT_D:7;
end;
suppose that
A87: 4 divides n and
A88: m is odd;
consider m1 being Integer such that
A89: m = 2*m1+1 by A88,ABIAN:1;
A90: 4 divides 4*m1;
4 divides 2*(2*m1)+2*(n+1) by A74,A89,A25,A26,A69,A71,INT_2:1;
then
A91: 4 divides 2*n+2*1 by A90,INT_2:1;
4 divides 2*n by A87,INT_2:2;
hence thesis by A91,INT_2:1,NAT_D:7;
end;
end;
suppose E = 3;
then
A92: d = 2*2*2 by A21,A22,POLYEQ_5:2;
then
A93: x|^3 = (8*m)*(8*n) by A8,A25,A26
.= 64*(m*n);
A94: m*n = (x/4)*(x/4)*(x/4) by A14,A93
.= (x/4)|^3 by POLYEQ_5:2;
16 divides 16*4;
then 2|^4 divides x|^3 by A93,Lm3,INT_2:2;
then
A95: 4 divides x by Lm1,Th100;
then consider a being Integer such that
A96: m = a|^3 by A27,A94,A28,Th103;
consider b being Integer such that
A97: n = b|^3 by A27,A94,A28,A95,Th103;
A98: a <> 0 by A6,A93,A96;
A99: b <> 0 by A6,A93,A97;
(x/4)|^3 = (a*b)|^3 by A94,A96,A97,NEWTON:7;
then x/4 = a*b by A28,NEWTON03:13;
then
A100: a*b+1 = b|^3-a|^3 by A25,A26,A92,A96,A97;
then
A101: a <> b by NEWTON:11;
A102: b|^3 = b*b*b & a|^3 = a*a*a by POLYEQ_5:2;
A103: now
assume |.b-a.| < 1;
then b-a = 0 by NAT_1:14;
hence contradiction by A101;
end;
per cases;
suppose a*b = 0;
hence thesis by A98,A99;
end;
suppose
A104: a*b > 0;
then a*b+1 > 0+1 by XREAL_1:8;
then
A105: (b-a)*((b-a)^2+3*a*b) > 1 by A100,A102;
A106: a*b*3 > 3*0 by A104;
now
assume b <= a;
then b < a by A101,XXREAL_0:1;
then b-a < a-a by XREAL_1:9;
hence contradiction by A105,A106;
end;
then b-a > a-a by XREAL_1:8;
then
A107: b-a >= 0+1 by NAT_1:13;
then (b-a)^2+3*a*b > 0+3*a*b by XREAL_1:6;
then (b-a)*((b-a)^2+3*a*b) > 1*(3*a*b) by A106,A107,XREAL_1:97;
then 3*a*b-a*b < a*b+1-a*b by A100,A102,XREAL_1:9;
then
A108: 2*a*b/2 < 1/2 by XREAL_1:74;
a*b >= 0+1 by A104,NAT_1:13;
hence thesis by A108,XXREAL_0:2;
end;
suppose
A109: a*b < 0;
then
A110: |.a*b.| = -a*b by ABSVALUE:def 1;
A111: |.b|^3-a|^3.| = |.(b-a)*((b+a)^2-a*b).| by A102
.= |.b-a.|*|.(b+a)^2-a*b.| by COMPLEX1:65;
A112: 1*|.(b+a)^2-a*b.| <= |.b-a.|*|.(b+a)^2-a*b.| by A103,XREAL_1:64;
0-a*b <= (b+a)^2-a*b by XREAL_1:9;
then |.-a*b.| <= |.(b+a)^2-a*b.| by A109,TOPREAL6:2;
then
A113: -a*b <= |.b-a.|*|.(b+a)^2-a*b.| by A110,A112,XXREAL_0:2;
A114: a*b+1 <= 0 by A109,INT_1:7;
a*b+0 < a*b+1 by XREAL_1:8;
hence thesis by A100,A111,A110,A113,A114,Th2;
end;
end;
end;
end;
end;
let e be object;
assume e in { [0,4], [0,-4] };
then
A115: e = [0,4] or e = [0,-4] by TARSKI:def 2;
(-4)|^2 = 0|^3+(0+4)|^2 by WSIERP_1:1;
hence thesis by A115;
end;
begin :: Problem 152
theorem Th107:
for m being Complex holds
for x,y,z being non zero Complex holds
x/y + y/z + z/x = m iff x^2*z + y^2*x + z^2*y = m*x*y*z
proof
let m be Complex;
let x,y,z be non zero Complex;
x/y + y/z = (x*z+y*y)/(y*z) by XCMPLX_1:116;
then
A1: x/y + y/z + z/x = ((x*z+y*y)*x+z*y*z)/(y*z*x) by XCMPLX_1:116;
thus x/y + y/z + z/x = m implies x^2*z + y^2*x + z^2*y = m*x*y*z
proof
assume x/y + y/z + z/x = m;
then ((x*z+y*y)*x+z*y*z)/(x*y*z)*(x*y*z) = m*(x*y*z) by A1;
hence thesis by XCMPLX_1:87;
end;
assume x^2*z + y^2*x + z^2*y = m*x*y*z;
then (x^2*z + y^2*x + z^2*y)/(x*y*z) = m*(x*y*z)/(x*y*z);
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th108:
for m being Integer
for x,y,z being non zero Integer st
x/y + y/z + z/x = m & x,y,z are_mutually_coprime holds
(x = 1 or x = -1) & (y = 1 or y = -1) & (z = 1 or z = -1)
proof
let m be Integer;
let x,y,z be non zero Integer;
assume x/y + y/z + z/x = m;
then
A1: x^2*z + y^2*x + z^2*y = m*x*y*z by Th107;
assume
A2: x,y,z are_mutually_coprime;
A3: y divides m*x*z*y;
A4: y divides z^2*y;
y divides x*y*y;
then y divides m*x*z*y - y^2*x by A3,INT_5:1;
then
A5: y divides m*x*z*y - y^2*x - z^2*y by A4,INT_5:1;
A6: z divides m*x*y*z;
A7: z divides y*z*z;
z divides x^2*z;
then z divides m*x*y*z - x^2*z by A6,INT_5:1;
then
A8: z divides m*x*y*z - x^2*z - z^2*y by A7,INT_5:1;
A9: x divides m*y*z*x;
A10: x divides x*z*x;
x divides y^2*x;
then x divides m*y*z*x - y^2*x by A9,INT_5:1;
then
A11: x divides m*y*z*x - y^2*x - x^2*z by A10,INT_5:1;
z^2 = z|^2 by WSIERP_1:1;
then z^2,x are_coprime by A2,WSIERP_1:10;
hence x = 1 or x = -1 by A1,A2,A11,INT_2:25,Th14;
x^2 = x|^2 by WSIERP_1:1;
then x^2,y are_coprime by A2,WSIERP_1:10;
hence y = 1 or y = -1 by A1,A2,A5,INT_2:25,Th14;
y^2 = y|^2 by WSIERP_1:1;
then y^2,z are_coprime by A2,WSIERP_1:10;
hence z = 1 or z = -1 by A1,A2,A8,INT_2:25,Th14;
end;
theorem
for m being Integer
for x,y,z being positive Integer st
x/y + y/z + z/x = m & x,y,z are_mutually_coprime holds
x = 1 & y = 1 & z = 1 by Th108;
Lm14: 1/1 + 1/1 + 1/1 = 3;
Lm15: (-1)/-1 + (-1)/-1 + (-1)/-1 = 3;
:: Problem 152 a
theorem
{ [x,y,z] where x,y,z is positive Integer:
x/y + y/z + z/x = 3 & x,y,z are_mutually_coprime } =
{ [1,1,1] }
proof
set A = { [x,y,z] where x,y,z is positive Integer:
x/y + y/z + z/x = 3 & x,y,z are_mutually_coprime };
set B = { [1,1,1] };
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y,z being positive Integer such that
A1: a = [x,y,z] and
A2: x/y + y/z + z/x = 3 & x,y,z are_mutually_coprime;
x = 1 & y = 1 & z = 1 by A2,Th108;
hence thesis by A1,TARSKI:def 1;
end;
let a be object;
assume a in B;
then
A3: a = [1,1,1] by TARSKI:def 1;
1,1,1 are_mutually_coprime by WSIERP_1:9;
hence thesis by A3,Lm14;
end;
:: Problem 152 b
theorem
{ [x,y,z] where x,y,z is non zero Integer:
x/y + y/z + z/x = 3 & x,y,z are_mutually_coprime } =
{ [1,1,1] , [-1,-1,-1] }
proof
set A = { [x,y,z] where x,y,z is non zero Integer:
x/y + y/z + z/x = 3 & x,y,z are_mutually_coprime };
set B = { [1,1,1] , [-1,-1,-1] };
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y,z being non zero Integer such that
A1: a = [x,y,z] and
A2: x/y + y/z + z/x = 3 and
A3: x,y,z are_mutually_coprime;
(x = 1 or x = -1) & (y = 1 or y = -1) & (z = 1 or z = -1)
by A2,A3,Th108;
hence thesis by A1,A2,TARSKI:def 2;
end;
let a be object;
assume a in B;
then
A4: a = [1,1,1] or a = [-1,-1,-1] by TARSKI:def 2;
A5: 1,1,1 are_mutually_coprime by WSIERP_1:9;
-1,-1,-1 are_mutually_coprime by Th11,WSIERP_1:9;
hence thesis by A4,A5,Lm14,Lm15;
end;
:: Problem 152 c
theorem
for m being Nat st m <> 3 holds
not ex x,y,z being non zero Integer st
x/y + y/z + z/x = m & x,y,z are_mutually_coprime
proof
let m be Nat such that
A1: m <> 3;
given x,y,z being non zero Integer such that
A2: x/y + y/z + z/x = m and
A3: x,y,z are_mutually_coprime;
(x = 1 or x = -1) & (y = 1 or y = -1) & (z = 1 or z = -1)
by A2,A3,Th108;
hence thesis by A1,A2;
end;