:: Elementary Number Theory Problems. {P}art {X}
:: by Artur Korni{\l}owicz
::
:: Received November 21, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_3, XCMPLX_0,
CARD_1, INT_1, NEWTON, INT_2, ARYTM_1, SUBSET_1, XBOOLE_0, TARSKI,
FINSET_1, ABIAN, EULER_1, REAL_1, ZFMISC_1, PEPIN, VALUED_0, CARD_3,
FINSEQ_1, NUMBER02, ORDINAL1, PBOOLE, SQUARE_1, NUMBER07, ORDINAL4,
PARTFUN3, COMPLEX1, MCART_1, POWER, NUMBER08, NUMBER10, FUNCT_3,
SETFAM_1, FINSEQ_2, FUNCT_7, NUMPOLY1, NUMBER09;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, XTUPLE_0, SETFAM_1,
DOMAIN_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, PBOOLE, FINSET_1, VALUED_0, XREAL_0, INT_1, INT_2,
NAT_1, NAT_D, XXREAL_0, XXREAL_2, COMPLEX1, SQUARE_1, FINSEQ_1, QUIN_1,
PARTFUN3, PEPIN, FINSEQ_2, RVSUM_1, NEWTON, POWER, ABIAN, EULER_1,
NUMPOLY1, NUMBER02, NUMBER07, NUMBER08;
constructors NAT_D, RELSET_1, ABIAN, EULER_1, PEPIN, XXREAL_2, NUMBER02,
QUIN_1, MOEBIUS1, WELLORD2, NUMBER07, PARTFUN3, POWER, DOMAIN_1, EC_PF_2,
WSIERP_1, NUMPOLY1, NUMBER08, NUMBER09;
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, WSIERP_1, XXREAL_2, FINSEQ_1, RVSUM_1, FUNCT_1,
XBOOLE_0, NUMBER02, PARTFUN3, FINSEQ_9, XTUPLE_0, SQUARE_1, POWER,
NUMPOLY1, NUMBER08, NUMBER09, NEWTON04;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, MEMBERED, TARSKI, FUNCT_1, FINSEQ_1, WELLORD2, SETFAM_1,
NUMBER02, PARTFUN3, NUMBER07;
equalities SQUARE_1, FINSEQ_1, FINSEQ_2, XCMPLX_0, QUIN_1, NUMPOLY1;
expansions INT_1, INT_2, ABIAN, ZFMISC_1, NAT_D;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, WSIERP_1, ORDINAL1, EULER_2,
XREAL_1, XXREAL_0, NAT_1, WELLORD2, INT_6, NAT_3, FUNCT_1, PARTFUN1,
NAT_6, TARSKI, POLYEQ_5, EULER_1, ENUMSET1, CARD_1, NEWTON01, ABIAN,
XXREAL_2, XTUPLE_0, GR_CY_3, NAT_4, FINSEQ_1, RVSUM_1, FINSEQ_3, INT_8,
XBOOLE_0, XREAL_0, XBOOLE_1, RELAT_1, XPRIMES0, XPRIMES1, NUMBER02,
NUMBER03, XCMPLX_1, INT_5, PREPOWER, NUMBER05, NUMBER07, NEWTON03,
PARTFUN3, FUNCT_2, ABSVALUE, COMPLEX1, MOEBIUS2, XPRIMET1, NAT_2, QUIN_1,
PYTHTRIP, NUMBER08, NUMBER09;
schemes NAT_1, PBOOLE, FINSEQ_2, CLASSES1, FUNCT_2;
begin :: Preliminaries
Lm1: 2|^2 = 2*2 by NEWTON:81;
Lm2: 2|^3 = 2*2*2 by POLYEQ_5:2;
reserve a,b,c,k,m,n for Nat;
reserve i,j,x,y for Integer;
reserve p,q for Prime;
reserve r,s for Real;
theorem Th1:
for i,j being natural Number holds
i < j implies ex k being positive Nat st j = i + k
proof
let i,j be natural Number;
assume
A1: i < j;
then consider k being Nat such that
A2: j = i + k by NAT_1:10;
now
assume k <= 0;
then k = 0;
hence contradiction by A1,A2;
end;
then reconsider k as positive Nat;
take k;
thus thesis by A2;
end;
theorem Th2:
for f being positive-yielding integer-valued FinSequence holds Product f >= 1
proof
let f be positive-yielding integer-valued FinSequence;
defpred P[set] means
for F being positive-yielding integer-valued FinSequence st F = $1
holds Product F >= 1;
A1: P[<*>INT] by RVSUM_1:94;
A2: for p being FinSequence of INT for x being Element of INT st
P[p] holds P[p^<*x*>]
proof
let p be FinSequence of INT;
let x be Element of INT such that
A3: P[p];
let F be positive-yielding integer-valued FinSequence such that
A4: F = p^<*x*>;
p is positive-yielding by A4,NUMBER08:37;
then
A5: Product p >= 1 by A3;
A6: <*x*> is positive-yielding by A4,NUMBER08:37;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by FINSEQ_1:38;
then
A7: x >= 0+1 by A6,INT_1:7;
Product F = Product p * x by A4,RVSUM_1:96;
then Product F >= 1*1 by A5,A7,XREAL_1:66;
hence Product F >= 1;
end;
A8: for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A1,A2);
f is FinSequence of INT by FINSEQ_1:104;
hence thesis by A8;
end;
theorem Th3:
m >= 2 & n >= 2 implies m*n is composite
proof
assume
A1: 2 <= m;
assume
A2: 2 <= n;
then 2*2 <= m*n by A1,XREAL_1:66;
hence 2 <= m*n by XXREAL_0:2;
ex N being Nat st N divides m*n & N <> 1 & N <> m*n
proof
take m;
thus m divides m*n;
thus m <> 1 by A1;
assume m = m*n;
then m*n = m*1;
then n = 1 by A1,XCMPLX_1:5;
hence thesis by A2;
end;
hence thesis;
end;
theorem Th4:
not p divides n implies n,p are_coprime
proof
assume
A1: not p divides n;
assume not n,p are_coprime;
then consider q being Prime such that
A2: q divides n and
A3: q divides p by PYTHTRIP:def 2;
q = p or q = 1 by A3,INT_2:def 4;
hence contradiction by A1,A2,INT_2:def 4;
end;
theorem Th5:
-1 mod p = p-1
proof
p-1 < p-0 by XREAL_1:8;
then p-1 = (p-1) mod p by NAT_D:24
.= ((p-1) + (-1)*p) mod p by NAT_D:61;
hence thesis;
end;
begin :: Problem 84
definition
let r,s be Complex;
pred r,s are_twin means
|.s-r.| = 2;
irreflexivity by COMPLEX1:44;
symmetry by COMPLEX1:60;
end;
notation
let r,s be Complex;
antonym r,s are_not_twin for r,s are_twin;
end;
theorem Th6:
r <= s implies (r,s are_twin iff s-r = 2)
proof
assume r <= s;
then s-r >= r-r by XREAL_1:7;
hence thesis by ABSVALUE:def 1;
end;
definition
let n;
func <=6n+1(n) -> Subset of NAT equals
{ a where a is Nat: a <= 6*n+1 };
coherence
proof
set A = {a where a is Nat: a <= 6*n+1};
A c= NAT
proof
let x be object;
assume x in A;
then ex a st x = a & a <= 6*n+1;
hence thesis by ORDINAL1:def 12;
end;
hence thesis;
end;
end;
theorem Th7:
a <= 6*n+1 iff a in <=6n+1(n)
proof
thus a <= 6*n+1 implies a in <=6n+1(n);
assume a in <=6n+1(n);
then ex b st a = b & b <= 6*n+1;
hence thesis;
end;
theorem Th8:
<=6n+1(n) c= Segm(6*n+2)
proof
let x be object;
assume x in <=6n+1(n);
then consider a such that
A1: x = a and
A2: a <= 6*n+1;
a < 6*n+1+1 by A2,NAT_1:13;
hence thesis by A1,NAT_1:44;
end;
registration
let n;
cluster <=6n+1(n) -> non empty finite;
coherence
proof
set A = <=6n+1(n);
0 in A;
hence A is non empty;
A c= Segm(6*n+2) by Th8;
hence A is finite;
end;
end;
theorem Th9:
m <= n implies <=6n+1(m) c= <=6n+1(n)
proof
assume
A1: m <= n;
let x be object;
assume
A2: x in <=6n+1(m);
then reconsider x as Element of NAT;
A3: x <= 6*m+1 by A2,Th7;
6*m <= 6*n by A1,XREAL_1:64;
then 6*m+1 <= 6*n+1 by XREAL_1:6;
hence thesis by A3,Th7,XXREAL_0:2;
end;
theorem Th10:
m < n implies <=6n+1(m) c< <=6n+1(n)
proof
assume
A1: m < n;
hence <=6n+1(m) c= <=6n+1(n) by Th9;
6*m < 6*n by A1,XREAL_1:68;
then 6*m+1 < 6*n+1 by XREAL_1:8;
then not 6*n+1 in <=6n+1(m) by Th7;
hence thesis;
end;
theorem
<=6n+1(m) = <=6n+1(n) implies m = n
proof
assume
A1: <=6n+1(m) = <=6n+1(n);
assume m <> n;
then m < n or m > n by XXREAL_0:1;
hence thesis by A1,Th10;
end;
theorem Th12:
for n being non zero Nat holds 2 in <=6n+1(n) /\ SetPrimes
proof
let n be non zero Nat;
0+1 <= n by NAT_1:13;
then 6*1 <= 6*n by XREAL_1:64;
then 6+1 <= 6*n+1 by XREAL_1:6;
then 2 <= 6*n+1 by XXREAL_0:2;
then
A1: 2 in <=6n+1(n);
2 in SetPrimes by XPRIMES1:2,NEWTON:def 6;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
for n being non zero Nat holds 3 in <=6n+1(n) /\ SetPrimes
proof
let n be non zero Nat;
0+1 <= n by NAT_1:13;
then 6*1 <= 6*n by XREAL_1:64;
then 6+1 <= 6*n+1 by XREAL_1:6;
then 3 <= 6*n+1 by XXREAL_0:2;
then
A1: 3 in <=6n+1(n);
3 in SetPrimes by XPRIMES1:3,NEWTON:def 6;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
for n being non zero Nat holds 5 in <=6n+1(n) /\ SetPrimes
proof
let n be non zero Nat;
0+1 <= n by NAT_1:13;
then 6*1 <= 6*n by XREAL_1:64;
then 6+1 <= 6*n+1 by XREAL_1:6;
then 5 <= 6*n+1 by XXREAL_0:2;
then
A1: 5 in <=6n+1(n);
5 in SetPrimes by XPRIMES1:5,NEWTON:def 6;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
for n being non zero Nat holds 7 in <=6n+1(n) /\ SetPrimes
proof
let n be non zero Nat;
0+1 <= n by NAT_1:13;
then 6*1 <= 6*n by XREAL_1:64;
then 6+1 <= 6*n+1 by XREAL_1:6;
then
A1: 7 in <=6n+1(n);
7 in SetPrimes by XPRIMES1:7,NEWTON:def 6;
hence thesis by A1,XBOOLE_0:def 4;
end;
registration
let n be non zero Nat;
cluster <=6n+1(n) /\ SetPrimes -> non empty;
coherence by Th12;
end;
definition :: largest prime
let n be non zero Nat;
func LP<=6n+1(n) -> Prime equals
max ( <=6n+1(n) /\ SetPrimes );
coherence
proof
max ( <=6n+1(n) /\ SetPrimes ) in <=6n+1(n) /\ SetPrimes by XXREAL_2:def 8;
then max ( <=6n+1(n) /\ SetPrimes ) in SetPrimes by XBOOLE_0:def 4;
hence thesis by NEWTON:def 6;
end;
end;
theorem Th16:
for m,n being non zero Nat st m <= n holds LP<=6n+1(m) <= LP<=6n+1(n)
proof
let m,n be non zero Nat;
assume m <= n;
then <=6n+1(m) c= <=6n+1(n) by Th9;
hence thesis by XXREAL_2:59,XBOOLE_1:26;
end;
theorem
LP<=6n+1(20) = LP<=6n+1(19)
proof
set a = 20;
set b = 19;
set X = <=6n+1(a);
set A = LP<=6n+1(a);
set Y = <=6n+1(b);
set B = LP<=6n+1(b);
A1: B in SetPrimes by NEWTON:def 6;
B in Y /\ SetPrimes by XXREAL_2:def 8;
then B in Y by XBOOLE_0:def 4;
then B <= 6*b+1 by Th7;
then B <= 6*a+1 by XXREAL_0:2;
then B in X;
then
A2: B in X /\ SetPrimes by A1,XBOOLE_0:def 4;
for x being ExtReal st x in X /\ SetPrimes holds x <= B
proof
let x be ExtReal such that
A3: x in X /\ SetPrimes;
A4: x in SetPrimes by A3,XBOOLE_0:def 4;
reconsider x as Nat by A3;
now
assume x > 115;
then
A5: x >= 115+1 by NAT_1:13;
x in X by A3,XBOOLE_0:def 4;
then x <= 6*a+1 by Th7;
then x = 116+0 or ... or x = 116+5 by A5,NAT_1:62;
hence contradiction
by A4,NEWTON:def 6,XPRIMES0:116,117,118,119,120,121;
end;
then x in Y;
then x in Y /\ SetPrimes by A4,XBOOLE_0:def 4;
hence thesis by XXREAL_2:def 8;
end;
hence thesis by A2,XXREAL_2:def 8;
end;
theorem
<=6n+1(1) = {0,1,2,3,4,5,6,7}
proof
set A = <=6n+1(1);
set B = {0,1,2,3,4,5,6,7};
let x be Nat;
hereby
assume x in A;
then consider a being Nat such that
A1: a = x and
A2: a <= 6*1+1;
a = 0 or ... or a = 7 by A2;
hence x in B by A1,ENUMSET1:def 6;
end;
assume x in B;
then
x = 0 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7
by ENUMSET1:def 6;
hence thesis;
end;
theorem
LP<=6n+1(1) = 7
proof
set A = <=6n+1(1);
set X = A /\ SetPrimes;
A1: 7 in A;
7 in SetPrimes by XPRIMES1:7,NEWTON:def 6;
then
A2: 7 in X by A1,XBOOLE_0:def 4;
now
let x be ExtReal;
assume x in X;
then x in A by XBOOLE_0:def 4;
then ex a being Nat st a = x & a <= 6*1+1;
hence x <= 7;
end;
hence thesis by A2,XXREAL_2:def 8;
end;
theorem Th20:
primenumber m = primenumber n implies m = n
proof
assume
A1: primenumber m = primenumber n;
assume m <> n;
then m < n or m > n by XXREAL_0:1;
hence thesis by A1,MOEBIUS2:21;
end;
definition
let p be Nat such that
A1: p is prime;
func primeindex(p) -> Element of NAT means :Def4:
primenumber it = p;
existence
proof
take card SetPrimenumber p;
p in NAT by ORDINAL1:def 12;
hence thesis by A1,NEWTON:def 8;
end;
uniqueness by Th20;
end;
theorem
primeindex p = primeindex q implies p = q
proof
primenumber primeindex p = p & primenumber primeindex q = q by Def4;
hence thesis;
end;
theorem
primeindex(2) = 0 by Def4,MOEBIUS2:8;
theorem
primeindex(3) = 1 by Def4,MOEBIUS2:10;
theorem
primeindex(5) = 2 by Def4,MOEBIUS2:12;
theorem
primeindex(7) = 3 by Def4,MOEBIUS2:15;
theorem
primeindex(11) = 4 by Def4,MOEBIUS2:17;
theorem
primeindex(13) = 5 by Def4,MOEBIUS2:19;
theorem Th28:
n > 0 implies p < primenumber(n+primeindex p)
proof
assume
A1: n > 0;
A2: p = primenumber primeindex p by Def4;
assume p >= primenumber(n+primeindex p);
then 0+primeindex p >= n+primeindex p by A2,MOEBIUS2:21;
hence thesis by A1,XREAL_1:6;
end;
theorem Th29:
for n being non zero Nat holds
primenumber (1 + primeindex LP<=6n+1(n)) >= 6*n+5
proof
let n be non zero Nat;
set M = LP<=6n+1(n);
set N = 1+primeindex M;
assume primenumber(N) < 6*n+5;
then
A1: primenumber(N) < 6*n+4+1;
A2: n >= 0+1 by NAT_1:13;
then
A3: 3*n >= 3*1 by XREAL_1:66;
then 3*n+1 >= 3+1 by XREAL_1:6;
then
A4: 6*n+2 <> 2;
2 divides 2*(3*n+1);
then
A5: not 6*n+2 is prime by A4;
2*n >= 2*1 by A2,XREAL_1:66;
then 2*n+1 >= 2+1 by XREAL_1:6;
then
A6: 6*n+3 <> 3;
3 divides 3*(2*n+1);
then
A7: not 6*n+3 is prime by A6;
3*n+2 >= 3+2 by A3,XREAL_1:6;
then 2*(3*n+2) >= 2*5 by XREAL_1:64;
then
A8: 6*n+4 <> 2;
2 divides 2*(3*n+2);
then
A9: not 6*n+4 is prime by A8;
A10: primenumber(N) in SetPrimes by NEWTON:def 6;
primenumber(N) <= 6*n+3+1 by A1,NAT_1:13;
then primenumber(N) < 6*n+3+1 by A9,XXREAL_0:1;
then primenumber(N) <= 6*n+3 by NAT_1:13;
then primenumber(N) < 6*n+2+1 by A7,XXREAL_0:1;
then primenumber(N) <= 6*n+1+1 by NAT_1:13;
then primenumber(N) < 6*n+1+1 by A5,XXREAL_0:1;
then primenumber(N) <= 6*n+1 by NAT_1:13;
then primenumber(N) in <=6n+1(n);
then primenumber(N) in <=6n+1(n) /\ SetPrimes by A10,XBOOLE_0:def 4;
then primenumber(N) <= M by XXREAL_2:def 8;
hence thesis by Th28;
end;
theorem Th30:
for n being non zero Nat holds
(primenumber (1 + primeindex LP<=6n+1(n))) - LP<=6n+1(n) >= 4
proof
let n be non zero Nat;
set LP = LP<=6n+1(n);
set s = primenumber(1+primeindex LP);
set r = LP;
r in <=6n+1(n) /\ SetPrimes by XXREAL_2:def 8;
then r in <=6n+1(n) by XBOOLE_0:def 4;
then
A1: r <= 6*n+1 by Th7;
s >= 6*n+5 by Th29;
then s-r >= (6*n+5) - (6*n+1) by A1,XREAL_1:13;
hence thesis;
end;
theorem Th31:
for n being non zero Nat holds
LP<=6n+1(n), primenumber (1+primeindex LP<=6n+1(n)) are_not_twin
proof
let n be non zero Nat;
set LP = LP<=6n+1(n);
set s = primenumber(1+primeindex LP);
A1: LP <= s by Th28;
s - LP <> 2 by Th30;
hence thesis by A1,Th6;
end;
theorem Th32:
for m being non zero Nat st 6*m+1 is prime holds 6*m+1 = LP<=6n+1(m)
proof
let m be non zero Nat such that
A1: 6*m+1 is prime;
set x = 6*m+1;
set A = <=6n+1(m);
A2: x in A;
x in SetPrimes by A1,NEWTON:def 6;
then
A3: x in A /\ SetPrimes by A2,XBOOLE_0:def 4;
for a being ExtReal st a in A /\ SetPrimes holds a <= x
proof
let a be ExtReal;
assume a in A /\ SetPrimes;
then a in A by XBOOLE_0:def 4;
hence a <= x by Th7;
end;
hence thesis by A3,XXREAL_2:def 8;
end;
theorem Th33:
for m,n being non zero Nat holds
6*n+1 is prime & m < n implies LP<=6n+1(m) < LP<=6n+1(n)
proof
let m,n be non zero Nat;
set A = <=6n+1(m);
set x = LP<=6n+1(m);
set y = LP<=6n+1(n);
assume that
A1: 6*n+1 is prime and
A2: m < n;
A3: x <= y by A2,Th16;
now
assume
A4: x = y;
x in A /\ SetPrimes by XXREAL_2:def 8;
then
A5: x in A by XBOOLE_0:def 4;
6*n+1 = y by A1,Th32;
then 6*n <= 6*m by A4,A5,Th7,XREAL_1:6;
hence contradiction by A2,XREAL_1:68;
end;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th34:
for m,n being non zero Nat st 6*m+1 is prime & 6*n+1 is prime &
LP<=6n+1(m) = LP<=6n+1(n) holds m = n
proof
let m,n be non zero Nat such that
A1: 6*m+1 is prime & 6*n+1 is prime & LP<=6n+1(m) = LP<=6n+1(n);
assume m <> n;
then m < n or n < m by XXREAL_0:1;
hence thesis by A1,Th33;
end;
definition
func 6n+1_Primes -> Subset of NAT equals
{ 6*n+1 where n is Nat: 6*n+1 is prime };
coherence
proof
set A = { 6*n+1 where n is Nat: 6*n+1 is prime };
A c= NAT
proof
let a be object;
assume a in A;
then ex k st a = 6*k+1 & 6*k+1 is prime;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster 6n+1_Primes -> with_non-empty_elements;
coherence
proof
assume {} in 6n+1_Primes;
then ex k st 0 = 6*k+1 & 6*k+1 is prime;
hence contradiction;
end;
end;
theorem
6n+1_Primes c= SetPrimes
proof
let a be object;
assume a in 6n+1_Primes;
then ex k st a = 6*k+1 & 6*k+1 is prime;
hence thesis by NEWTON:def 6;
end;
registration
cluster 6n+1_Primes -> infinite;
coherence
proof
set P = 6n+1_Primes;
assume
A1: P is finite;
set N = 6*Product Sgm P;
A2: Sgm P is positive-yielding
proof
let r be Real;
assume
A3: r in rng Sgm P;
P is included_in_Seg by A1;
then r in 6n+1_Primes by A3,FINSEQ_1:def 14;
hence thesis;
end;
then
A4: N >= 6*1 by Th2,XREAL_1:64;
A5: now
assume N^2-N < 1;
then N*(N-1) = 0 by A2,NAT_1:14;
then N = 0 or N-1 = 0;
hence contradiction by A4;
end;
then reconsider M = N^2-N+1 as Element of NAT by INT_1:3;
N^2-N+1 >= 1+1 by A5,XREAL_1:6;
then consider p being Element of NAT such that
A6: p is prime and
A7: p divides M by INT_2:31;
reconsider p as Prime by A6;
A8: N*N*N = N|^3 by POLYEQ_5:2;
A9: N|^3*N|^3 = N|^(3+3) by NEWTON:8;
A10: p > 1 by INT_2:def 4;
A11: now
assume
A12: p divides N;
N divides N^2;
then p divides N^2 by A12,INT_2:9;
then p divides N^2-N by A12,INT_5:1;
then p divides M-(N^2-N) by A7,INT_5:1;
hence contradiction by INT_2:def 4,NAT_D:7;
end;
then
A13: N,p are_coprime by Th4;
then
A14: (N|^order(N,p)) mod p = 1 by A10,PEPIN:def 2;
A15: -1 mod p = p-1 by Th5;
A16: p-'1 = p-1 by XREAL_0:def 2;
N^2-N+1 divides (N^2-N+1)*(N+1);
then p divides (N^2-N+1)*(N+1) by A7,INT_2:9;
then p divides N|^3--1 by A8;
then
A17: N|^3,-1 are_congruent_mod p;
then
A18: (N|^3) mod p = -1 mod p by NAT_D:64
.= p-1 by Th5;
A19: 1 mod p = 1 by INT_2:def 4,NAT_D:24;
A20: now
assume N,1 are_congruent_mod p;
then
A21: (N|^3) mod p = 1|^3 by A10,NAT_6:12,GR_CY_3:34;
N = 2*(3*Product Sgm P);
hence contradiction by A18,A21,NAT_2:21;
end;
A22: now
assume
A23: p = 2 or p = 3;
2 divides 2*(3*Product Sgm P) & 3 divides 3*(2*Product Sgm P);
hence contradiction by A11,A23;
end;
N|^3*N|^3,(-1)*(-1) are_congruent_mod p by A17,INT_1:18;
then (N|^6) mod p = 1 by A9,INT_2:def 4,NAT_6:12;
then order(N,p) divides 6 by A10,A11,Th4,PEPIN:47;
then per cases by NUMBER07:10;
suppose order(N,p) = 1;
hence contradiction by A14,A19,A20,NAT_D:64;
end;
suppose order(N,p) = 2;
then N,-1 are_congruent_mod p by A14,A19,A20,NAT_D:64,NAT_6:18;
then
A24: p divides (N+1) gcd M by A7,INT_2:def 2;
M-3 = (N+1)*(N-2);
then M,3 are_congruent_mod N+1;
then
A25: (N+1) gcd M = (N+1) gcd 3 by WSIERP_1:43;
A26: (N+1) gcd 3 <= 3 by NUMBER03:13;
now
assume p <= (N+1) gcd 3;
then p <= 3 by A26,XXREAL_0:2;
then p < 3 or p = 3 by XXREAL_0:1;
hence contradiction by A22,XPRIMET1:1;
end;
hence contradiction by A24,A25,NAT_D:7;
end;
suppose
A27: order(N,p) = 3;
then -1 mod p = 1 by A14,A17,NAT_D:64;
hence contradiction by A13,A15,A16,A27,PEPIN:49,NAT_D:7;
end;
suppose
A28: order(N,p) = 6;
Euler p = p-1 by EULER_1:20;
then 6 divides p-1 by A10,A11,A28,Th4,INT_8:9;
then consider i such that
A29: p-1 = 6*i;
i >= 0 by A29;
then reconsider i as Element of NAT by INT_1:3;
p = 6*i+1 by A29;
then p in P;
then
A30: p divides Product Sgm P by A1,NUMBER09:16;
Product Sgm P divides N;
hence contradiction by A11,A30,INT_2:9;
end;
end;
end;
:: Problem 84
theorem
{ [p,q] where p,q is Prime: p,q are_not_twin } is infinite
proof
set A = {[p,q] where p,q is Prime: p,q are_not_twin};
deffunc pk(non zero Nat) = LP<=6n+1($1);
deffunc F(non zero Nat) = [ pk($1) , primenumber(1+primeindex pk($1)) ];
defpred P[Nat,object] means ex n being non zero Nat st n = $1 & $2 = F(n);
set P = 6n+1_Primes;
deffunc C(Element of P) = In(($1-1) div 6,NAT);
consider C being Function of P,NAT such that
A1: for p being Element of P holds C.p = C(p) from FUNCT_2:sch 4;
A2: dom C = P by FUNCT_2:def 1;
A3: now
let p be Element of P;
p in P;
then ex n st p = 6*n+1 & 6*n+1 is prime;
hence 6*((p-1) div 6) = p-1;
end;
C is one-to-one
proof
let x1,x2 be object such that
A4: x1 in dom C and
A5: x2 in dom C and
A6: C.x1 = C.x2;
reconsider x1,x2 as Element of P by A4,A5;
C.x1 = C(x1) & C.x2 = C(x2) by A1;
then
A7: 6*((x1-1) div 6) = 6*((x2-1) div 6) by A6;
6*((x1-1) div 6) = x1-1 & 6*((x2-1) div 6) = x2-1 by A3;
hence thesis by A7;
end;
then reconsider D = rng C as infinite Subset of NAT
by A2,CARD_1:59,RELAT_1:def 19;
A8: for d being Element of D holds 6*d+1 is prime
proof
let d be Element of D;
consider p being Element of P such that
A9: d = C.p by FUNCT_2:113;
A10: C(p) = (p-1) div 6;
p in P;
then
A11: ex n st p = 6*n+1 & 6*n+1 is prime;
6*((p-1) div 6) = p-1 by A3;
thus thesis by A1,A9,A10,A11;
end;
A12: now
let d be Element of D;
assume d = 0;
then 6*0+1 is prime by A8;
hence contradiction;
end;
A13: for i being Element of D ex j being object st P[i,j]
proof
let i be Element of D;
reconsider a = i as non zero Nat by A12;
take F(a);
thus thesis;
end;
consider f being ManySortedSet of D such that
A14: for d being Element of D holds P[d,f.d] from PBOOLE:sch 6(A13);
A15: dom f = D by PARTFUN1:def 2;
A16: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A17: k in dom f and
A18: f.k = y by FUNCT_1:def 3;
reconsider k as non zero Element of NAT by A12,A15,A17;
A19: P[k,f.k] by A14,A17;
pk(k), primenumber(1+primeindex pk(k)) are_not_twin by Th31;
hence thesis by A18,A19;
end;
f is one-to-one
proof
let x1,x2 be object such that
A20: x1 in dom f and
A21: x2 in dom f and
A22: f.x1 = f.x2;
reconsider x1 as non zero Nat by A12,A20;
reconsider x2 as non zero Nat by A12,A21;
P[x1,f.x1] & P[x2,f.x2] by A14,A20,A21;
then
A23: pk(x1) = pk(x2) by A22,XTUPLE_0:1;
6*x1+1 is prime & 6*x2+1 is prime by A8,A20,A21;
hence thesis by A23,Th34;
end;
hence thesis by A15,A16,CARD_1:59;
end;
begin :: Problem 94
definition
let c be Complex;
attr c is a_product_of_three_different_primes means
ex p,q,r being Prime st p,q,r are_mutually_distinct & c = p*q*r;
end;
theorem Th37:
n > 4 implies ex k being Nat st n = 2*k & k > 2 or n = 2*k+1 & k > 1
proof
assume
A1: n > 4;
per cases;
suppose n is even;
then consider k being Nat such that
A2: n = 2*k;
take k;
4 = 2*2;
hence thesis by A1,A2,XREAL_1:66;
end;
suppose n is odd;
then consider k such that
A3: n = 2*k+1 by ABIAN:9;
take k;
now
assume k <= 1;
then 2*k <= 2*1 by XREAL_1:64;
then 2*k+1 <= 2+1 by XREAL_1:6;
hence contradiction by A1,A3,XXREAL_0:2;
end;
hence thesis by A3;
end;
end;
reconsider p2 = 2 as Prime by XPRIMES1:2;
reconsider p3 = 3 as Prime by XPRIMES1:3;
reconsider p5 = 5 as Prime by XPRIMES1:5;
:: Problem 94 a
theorem
n > 4 implies
ex m being Nat st n < m < 2*n & m is_a_product_of_two_different_primes
proof
assume n > 4;
then consider k being Nat such that
A1: n = 2*k & k > 2 or n = 2*k+1 & k > 1 by Th37;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider p2 = 2 as Prime by XPRIMES1:2;
per cases by A1;
suppose that
A2: n = 2*k and
A3: k > 2;
consider P being Prime such that
A4: k < P and
A5: P <= 2*k by A3,XXREAL_0:2,NAT_4:56;
take m = p2*P;
thus n < m by A2,A4,XREAL_1:68;
2*k is composite by A3,Th3;
then P < n by A2,A5,XXREAL_0:1;
hence m < 2*n by XREAL_1:68;
take p2,P;
thus p2 <> P by A3,A4;
thus m = p2*P;
end;
suppose that
A6: n = 2*k+1 and
A7: k > 1;
consider P being Prime such that
A8: k < P and
A9: P <= 2*k by A7,NAT_4:56;
take m = p2*P;
k+1 <= P by A8,NAT_1:13;
then
A10: 2*(k+1) <= 2*P by XREAL_1:64;
2*k+1 < 2*k+2 by XREAL_1:6;
hence n < m by A6,A10,XXREAL_0:2;
A11: 2*P <= 2*(2*k) by A9,XREAL_1:64;
4*k+0 < 4*k+2 by XREAL_1:6;
hence m < 2*n by A6,A11,XXREAL_0:2;
take p2,P;
k >= 1+1 by A7,NAT_1:13;
hence p2 <> P by A8;
thus m = p2*P;
thus thesis;
end;
end;
:: Problem 94 b
theorem
n > 15 implies
ex m being Nat st n < m < 2*n & m is a_product_of_three_different_primes
proof
assume
A1: n > 15;
per cases;
suppose n <= 29;
then
A2: n = 0 or ... or n = 29;
take p2*p3*p5;
thus n < p2*p3*p5 < 2*n by A1,A2;
take p2,p3,p5;
thus thesis;
end;
suppose
A3: n > 29;
consider k such that
A4: n = 6*k or n = 6*k+1 or n = 6*k+2 or n = 6*k+3 or n = 6*k+4 or n = 6*k+5
by NUMBER02:26;
reconsider k as Element of NAT by ORDINAL1:def 12;
A5: now
assume k < 4+1;
then k <= 4 by NAT_1:13;
then
A6: 6*k <= 6*4 by XREAL_1:64;
then 6*k+1 <= 6*4+1 & 6*k+2 <= 6*4+2 & 6*k+3 <= 6*4+3
& 6*k+4 <= 6*4+4 & 6*k+5 <= 6*4+5 by XREAL_1:6;
hence contradiction by A3,A4,A6,XXREAL_0:2;
end;
then consider P being Prime such that
A7: k < P and
A8: P <= 2*k by NAT_4:56,XXREAL_0:2;
take p2*p3*P;
2 <= k by A5,XXREAL_0:2;
then 2*k is composite by Th3;
then
A9: P < 2*k by A8,XXREAL_0:1;
A10: 6*k+0 < 6*k+6 & 6*k+1 < 6*k+6 & 6*k+2 < 6*k+6
& 6*k+3 < 6*k+6 & 6*k+4 < 6*k+6 & 6*k+5 < 6*k+6 by XREAL_1:6;
k+1 <= P by A7,NAT_1:13;
then 6*(k+1) <= 6*P & 6*(k+1) <= 6*P & 6*(k+1) <= 6*P
& 6*(k+1) <= 6*P & 6*(k+1) <= 6*P & 6*(k+1) <= 6*P by XREAL_1:64;
hence n < p2*p3*P by A4,A10,XXREAL_0:2;
A11: 6*P < 6*(2*k) by A9,XREAL_1:68;
12*k+0 <= 12*k+2 & 12*k+0 <= 12*k+4 & 12*k+0 <= 12*k+6
& 12*k+0 <= 12*k+8 & 12*k+0 <= 12*k+10 by XREAL_1:6;
hence p2*p3*P < 2*n by A4,A11,XXREAL_0:2;
take p2,p3,P;
thus thesis by A5,A7,XXREAL_0:2;
end;
end;
begin :: Problem 99
theorem Th40:
5 divides 2|^(4*n+2) + 1
proof
A1: 2|^2+1 divides 2|^2|^(2*n+1) + 1|^(2*n+1) by NEWTON01:35;
2|^2|^(2*n+1) = 2|^(2*(2*n+1)) by NEWTON:9;
hence thesis by A1,Lm1;
end;
registration
let n;
cluster 1/5 * (2|^(4*n+2)+1) -> natural;
coherence
proof
5 divides 2|^(4*n+2)+1 by Th40;
hence thesis;
end;
end;
:: Problem 99
theorem
n > 1 implies 1/5 * (2|^(4*n+2)+1) is composite
proof
assume
A1: n > 1;
set W = 2|^(4*n+2)+1;
set L = 2|^(2*n+1)-2|^(n+1)+1;
set R = 2|^(2*n+1)+2|^(n+1)+1;
A2: 2|^(2*n+1)*2|^(2*n+1) = 2|^((2*n+1)+(2*n+1)) by NEWTON:8;
A3: 2*2|^(2*n+1) = 2|^(2*n+1+1) by NEWTON:6;
A4: 2|^(n+1)*2|^(n+1) = 2|^(n+1+(n+1)) by NEWTON:8;
2|^(2*n+1+1) = 2|^(n+1+(n+1));
then
A5: 2|^(4*n+2) = 2|^(2*n+1)*2|^(2*n+1) + 2*2|^(2*n+1) - 2|^(n+1)*2|^(n+1)
by A2,A3,A4;
A6: 2|^(n+1+n) = 2|^(n+1)*2|^n by NEWTON:8;
A7: n >= 1+1 by A1,NAT_1:13;
then n+1 >= 2+1 by XREAL_1:6;
then
A8: 2|^(n+1) >= 2|^3 by PREPOWER:93;
A9: 2|^n >= 2|^2 by A7,PREPOWER:93;
then 2|^n-1 >= 4-1 by Lm1,XREAL_1:9;
then
A10: 2|^(n+1)*(2|^n-1) >= 8*3 by A8,Lm2,XREAL_1:66;
then
A11: 2|^(n+1)*(2|^n-1)+1 >= 24+1 by XREAL_1:6;
then L*R >= 25*R by A6,XREAL_1:64;
then
A12: 1/5*W >= 1/5 * (25*R) by A5,XREAL_1:64;
reconsider L as Element of NAT by A6,A11;
2|^n+1 >= 4+1 by A9,Lm1,XREAL_1:6;
then
A13: 2|^(n+1)*(2|^n+1) >= 8*5 by A8,Lm2,XREAL_1:66;
then
A14: 2|^(n+1)*(2|^n+1)+1 >= 40+1 by XREAL_1:6;
then 5*R >= 5*41 by A6,XREAL_1:64;
then 2 <= 5*R by XXREAL_0:2;
hence 2 <= 1/5*W by A12,XXREAL_0:2;
A15: W = L*R by A5;
then per cases by Th40,XPRIMES1:5,INT_5:7;
suppose 5 divides L;
then consider N being Nat such that
A16: L = 5*N;
A17: 1/5*W = 1/5*(5*N*R) by A15,A16
.= N*R;
A18: now
assume N < 2;
then N = 0 or N = 1 by NAT_1:23;
hence thesis by A6,A10,A16;
end;
R >= 2 by A6,A14,XXREAL_0:2;
hence thesis by A17,A18,Th3;
end;
suppose 5 divides R;
then consider N being Nat such that
A19: R = 5*N;
A20: 1/5*W = 1/5*(5*N*L) by A15,A19
.= N*L;
A21: now
assume N < 2;
then N = 0 or N = 1 by NAT_1:23;
hence thesis by A6,A13,A19;
end;
L >= 2 by A6,A11,XXREAL_0:2;
hence thesis by A20,A21,Th3;
end;
end;
begin :: Problem 170
Lm3:
for x,y being Integer st x*y = 8 holds
x = 1 & y = 8 or x = 2 & y = 4 or x = 4 & y = 2 or x = 8 & y = 1 or
x = -1 & y = -8 or x = -2 & y = -4 or x = -4 & y = -2 or x = -8 & y = -1
proof
let x,y be Integer;
assume
A1: x*y = 8;
A2: x divides x*y;
per cases;
suppose x >= 0;
then x in NAT by INT_1:3;
then x in {1,2,4,8} by A1,A2,NUMBER03:12;
then x = 1 or x = 2 or x = 4 or x = 8 by ENUMSET1:def 2;
hence thesis by A1;
end;
suppose x < 0;
then -x in NAT by INT_1:3;
then -x in {1,2,4,8} by A1,A2,INT_2:10,NUMBER03:12;
then -x = 1 or -x = 2 or -x = 4 or -x = 8 by ENUMSET1:def 2;
then x = -1 or x = -2 or x = -4 or x = -8;
hence thesis by A1;
end;
end;
Lm4:
for x,y being Integer st x*y = -8 holds
x = 1 & y = -8 or x = 2 & y = -4 or x = 4 & y = -2 or x = 8 & y = -1 or
x = -1 & y = 8 or x = -2 & y = 4 or x = -4 & y = 2 or x = -8 & y = 1
proof
let x,y be Integer;
assume x*y = -8;
then (-x)*y = 8;
then
-x = 1 & y = 8 or -x = 2 & y = 4 or -x = 4 & y = 2 or -x = 8 & y = 1 or
-x = -1 & y = -8 or -x = -2 & y = -4 or -x = -4 & y = -2 or -x = -8 & y = -1
by Lm3;
hence thesis;
end;
Lm5:
for x,y being Integer st x*y = 4 holds
x = 1 & y = 4 or x = 2 & y = 2 or x = 4 & y = 1 or x = -1 & y = -4 or
x = -2 & y = -2 or x = -4 & y = -1
proof
let x,y be Integer;
assume
A1: x*y = 4;
A2: x divides x*y;
per cases;
suppose x >= 0;
then x in NAT by INT_1:3;
then x = 1 or x = 2 or x = 4 by A1,A2,NUMBER05:21;
hence thesis by A1;
end;
suppose x < 0;
then -x in NAT by INT_1:3;
then -x = 1 or -x = 2 or -x = 4 by A1,A2,INT_2:10,NUMBER05:21;
then x = -1 or x = -2 or x = -4;
hence thesis by A1;
end;
end;
Lm6:
for x,y being Integer st x*y = -4 holds
x = 1 & y = -4 or x = 2 & y = -2 or x = 4 & y = -1 or
x = -1 & y = 4 or x = -2 & y = 2 or x = -4 & y = 1
proof
let x,y be Integer;
assume x*y = -4;
then (-x)*y = 4;
then
-x = 1 & y = 4 or -x = 2 & y = 2 or -x = 4 & y = 1 or -x = -1 & y = -4 or
-x = -2 & y = -2 or -x = -4 & y = -1 by Lm5;
hence thesis;
end;
Lm7:
for x,y being Integer st x*y = 2 holds
x = 1 & y = 2 or x = 2 & y = 1 or x = -1 & y = -2 or x = -2 & y = -1
proof
let x,y be Integer such that
A1: x*y = 2;
A2: x divides x*y;
per cases;
suppose x >= 0;
then x in NAT by INT_1:3;
then x = 1 or x = 2 by A1,A2,XPRIMES1:2;
hence thesis by A1;
end;
suppose x < 0;
then -x in NAT by INT_1:3;
then -x = 1 or -x = 2 by A1,A2,INT_2:10,XPRIMES1:2;
then x = -1 or x = -2;
hence thesis by A1;
end;
end;
Lm8:
for x,y being Integer st x*y = -2 holds x = 1 & y = -2 or x = 2 & y = -1
or x = -1 & y = 2 or x = -2 & y = 1
proof
let x,y be Integer;
assume x*y = -2;
then (-x)*y = 2;
then
-x = 1 & y = 2 or -x = 2 & y = 1 or -x = -1 & y = -2 or -x = -2 & y = -1
by Lm7;
hence thesis;
end;
Lm9:
2*0-1 is odd & 2*1-1 is odd;
Lm10:
2*1 is even & 2*(-1) is even & 2*2 is even & 2*(-2) is even & 2*(-4) is even;
Lm11:
for x,y,z being even Integer st x*y*z = 8 holds
x = 2 & y = 2 & z = 2 or x = -2 & y = -2 & z = 2 or x = -2 & y = 2 & z = -2
or x = 2 & y = -2 & z = -2
proof
let x,y,z be even Integer;
assume x*y*z = 8;
then x*y = 2 & z = 4 or x*y = 4 & z = 2 or x*y = -2 & z = -4 or
x*y = -4 & z = -2 by Lm3,Lm9;
hence thesis by Lm6,Lm9,Lm5,Lm7,Lm8;
end;
Lm12:
for x being even Integer, y,z being odd Integer st x*y*z = 8 holds
x = 8 & y = 1 & z = 1 or x = 8 & y = -1 & z = -1 or x = -8 & y = 1 & z = -1
or x = -8 & y = -1 & z = 1
proof
let x be even Integer;
let y,z be odd Integer;
assume x*y*z = 8;
then x*y = 8 & z = 1 or x*y = -8 & z = -1 by Lm3,Lm10;
hence thesis by Lm3,Lm4,Lm10;
end;
:: Problem 170
theorem
{ [x,y,z] where x,y,z is Integer: x+y+z = 3 & x|^3+y|^3+z|^3 = 3 }
= { [1,1,1], [-5,4,4], [4,-5,4], [4,4,-5] }
proof
set A = { [x,y,z] where x,y,z is Integer: x+y+z = 3 & x|^3+y|^3+z|^3 = 3 };
set B = { [1,1,1], [-5,4,4], [4,-5,4], [4,4,-5] };
A1: (-5)|^3 = (-5)*(-5)*(-5) by POLYEQ_5:2;
A2: 4|^3 = 4*4*4 by POLYEQ_5:2;
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y,z being Integer such that
A3: a = [x,y,z] and
A4: x+y+z = 3 and
A5: x|^3+y|^3+z|^3 = 3;
A6: 3|^3 = 3*3*3 by POLYEQ_5:2;
x|^3 = x*x*x & y|^3 = y*y*y & z|^3 = z*z*z &
(x+y+z)|^3 = (x+y+z)*(x+y+z)*(x+y+z) by POLYEQ_5:2;
then (x+y+z)|^3 - (x|^3+y|^3+z|^3) = 3*(x+y)*(x+z)*(y+z);
then 27-3 = 3*(x+y)*(x+z)*(y+z) by A4,A5,A6;
then
A7: 8 = (x+y)*(x+z)*(y+z)
.= (3-z)*(3-y)*(3-x) by A4;
then
A8: (3-x)*(3-y)*(3-z) = 8;
(3-z)+(3-y)+(3-x) = 2*3 by A4;
then per cases;
suppose 3-z is even & 3-y is even & 3-x is even;
then 3-x = 2 & 3-y = 2 & 3-z = 2 or 3-x = -2 & 3-y = -2 & 3-z = 2 or
3-x = -2 & 3-y = 2 & 3-z = -2 or 3-x = 2 & 3-y = -2 & 3-z = -2
by A7,Lm11;
hence thesis by A3,A4,ENUMSET1:def 2;
end;
suppose 3-z is even & 3-y is odd & 3-x is odd;
then 3-z = 8 & 3-y = 1 & 3-x = 1 or 3-z = 8 & 3-y = -1 & 3-x = -1 or
3-z = -8 & 3-y = 1 & 3-x = -1 or 3-z = -8 & 3-y = -1 & 3-x = 1
by A7,Lm12;
hence thesis by A3,A4,ENUMSET1:def 2;
end;
suppose 3-z is odd & 3-y is even & 3-x is odd;
then 3-y = 8 & 3-z = 1 & 3-x = 1 or 3-y = 8 & 3-z = -1 & 3-x = -1 or
3-y = -8 & 3-z = 1 & 3-x = -1 or 3-y = -8 & 3-z = -1 & 3-x = 1
by A7,Lm12;
hence thesis by A3,A4,ENUMSET1:def 2;
end;
suppose 3-z is odd & 3-y is odd & 3-x is even;
then 3-x = 8 & 3-y = 1 & 3-z = 1 or 3-x = 8 & 3-y = -1 & 3-z = -1 or
3-x = -8 & 3-y = 1 & 3-z = -1 or 3-x = -8 & 3-y = -1 & 3-z = 1
by A8,Lm12;
hence thesis by A3,A4,ENUMSET1:def 2;
end;
end;
let a be object;
assume a in B;
then
A9: a = [1,1,1] or a = [-5,4,4] or a = [4,-5,4] or a = [4,4,-5]
by ENUMSET1:def 2;
-5+4+4 = 3 & 4+4+-5 = 3 & 1|^3+1|^3+1|^3 = 3
& 4|^3+(-5)|^3+4|^3 = 3 & 4|^3+4|^3+(-5)|^3 = 3 by A1,A2;
hence thesis by A9;
end;
begin :: Problem 173
:: Problem 173
theorem
for m,n being positive Nat ex a,b,c being Integer st
{ [x,y] where x,y is Nat: a*x + b*y = c } = { [m,n] }
proof
let m,n be positive Nat;
consider a being Prime such that
A1: a > m+n by NEWTON:72;
consider b being Prime such that
A2: b > a by NEWTON:72;
take a, b, c = a*m+b*n;
set A = { [x,y] where x,y is Nat: a*x + b*y = c };
set B = { [m,n] };
A3: b > m+n by A1,A2,XXREAL_0:2;
thus A c= B
proof
let z be object;
assume z in A;
then consider x,y being Nat such that
A4: z = [x,y] and
A5: a*x+b*y = c;
per cases by XXREAL_0:1;
suppose m = x & n = y;
hence thesis by A4,TARSKI:def 1;
end;
suppose x > m & y >= n or x >= m & y > n;
then a*x > a*m & b*y >= b*n or a*x >= a*m & b*y > b*n by XREAL_1:64,68;
hence thesis by A5,XREAL_1:8;
end;
suppose x < m;
then
A6: m-x > x-x by XREAL_1:8;
then
A7: m-x in NAT by INT_1:3;
b divides b*n & b divides b*y;
then b divides a*(m-x)+b*n-b*n by A5,INT_5:1;
then b divides a or b divides m-x by INT_5:7;
then b <= m-x by A2,A6,A7,NAT_D:7;
then m+n < m-x by A3,XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
suppose y < n;
then
A8: n-y > y-y by XREAL_1:8;
then
A9: n-y in NAT by INT_1:3;
A10: a > 1 by INT_2:def 4;
a divides a*m & a divides a*x;
then a divides b*(n-y)+a*m-a*m by A5,INT_5:1;
then a divides b or a divides n-y by INT_5:7;
then a <= n-y by A2,A8,A9,A10,NAT_D:7,INT_2:def 4;
then m+n < n-y by A1,XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
end;
let z be object;
assume z in B;
then z = [m,n] by TARSKI:def 1;
hence thesis;
end;
begin :: Problem 174
theorem Th44:
for m being positive Nat holds
card { [x,y] where x,y is positive Nat: x+y = m+1 } = m
proof
let m be positive Nat;
set A = { [x,y] where x,y is positive Nat: x+y = m+1 };
A1: Seg m,A are_equipotent
proof
defpred P[object,object] means
ex k being Nat st k = $1 & $2 = [k,m-k+1];
A2: for e being object st e in Seg m ex u being object st P[e,u]
proof
let e be object;
assume e in Seg m;
then reconsider e as Nat;
take [e,m-e+1], e;
thus thesis;
end;
consider f being Function such that
A3: dom f = Seg m and
A4: for e being object st e in Seg m holds P[e,f.e] from CLASSES1:sch 1(A2);
take f;
thus f is one-to-one
proof
let x1,x2 be object such that
A5: x1 in dom f & x2 in dom f and
A6: f.x1 = f.x2;
reconsider x1,x2 as Element of NAT by A3,A5;
P[x1,f.x1] & P[x2,f.x2] by A3,A4,A5;
hence thesis by A6,XTUPLE_0:1;
end;
thus dom f = Seg m by A3;
thus rng f c= A
proof
let b be object;
assume b in rng f;
then consider a being object such that
A7: a in dom f and
A8: f.a = b by FUNCT_1:def 3;
consider k being Nat such that
A9: k = a and
A10: f.a = [k,m-k+1] by A3,A4,A7;
A11: 1 <= k by A3,A7,A9,FINSEQ_1:1;
k <= m by A3,A7,A9,FINSEQ_1:1;
then m-k >= m-m by XREAL_1:10;
then
A12: m-k+1 is positive Element of NAT by INT_1:3;
k+(m-k+1) = m+1;
hence thesis by A8,A10,A11,A12;
end;
let b be object;
assume b in A;
then consider x,y being positive Nat such that
A13: b = [x,y] and
A14: x+y = m+1;
A15: 0+1 <= x by NAT_1:13;
x+0 < x+y by XREAL_1:6;
then x <= m by A14,NAT_1:13;
then
A16: x in Seg m by A15;
then P[x,f.x] by A4;
then f.x = [x,m-x+1]
.= [x,y] by A14;
hence thesis by A3,A13,A16,FUNCT_1:def 3;
end;
A17: Seg m,m are_equipotent by FINSEQ_1:54;
card m = m;
hence thesis by A1,A17,WELLORD2:15,CARD_1:5;
end;
:: Problem 174
theorem
for m being positive Nat ex a,b,c being positive Nat st
card { [x,y] where x,y is positive Nat: a*x + b*y = c } = m
proof
let m be positive Nat;
take 1, 1, m+1;
set A = { [x,y] where x,y is positive Nat: 1*x+1*y = m+1 };
set B = { [x,y] where x,y is positive Nat: x+y = m+1 };
A = B
proof
thus A c= B
proof
let a be object;
assume a in A;
then ex x,y being positive Nat st a = [x,y] & 1*x+1*y = m+1;
hence thesis;
end;
let a be object;
assume a in B;
then consider x,y being positive Nat such that
A1: a = [x,y] & x+y = m+1;
1*x+1*y = x+y;
hence thesis by A1;
end;
hence thesis by Th44;
end;
begin :: Problem 175
:: Problem 175
theorem
for m being positive Nat holds
card { [x,y] where x,y is positive Nat: x^2+y^2+2*x*y-m*x-m*y-m-1 = 0 } = m
proof
let m be positive Nat;
set A = { [x,y] where x,y is positive Nat: x^2+y^2+2*x*y-m*x-m*y-m-1 = 0 };
set B = { [x,y] where x,y is positive Nat: x+y = m+1 };
A = B
proof
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y being positive Nat such that
A1: a = [x,y] and
A2: x^2+y^2+2*x*y-m*x-m*y-m-1 = 0;
x^2+y^2+2*x*y-m*x-m*y-m-1 = (x+y-m-1)*(x+y+1);
then x+y-m-1 = 0 by A2;
hence thesis by A1;
end;
let a be object;
assume a in B;
then consider x,y being positive Nat such that
A3: a = [x,y] & x+y = m+1;
x^2+y^2+2*x*y-m*x-m*y-m-1 = (x+y-m-1)*(x+y+1);
hence thesis by A3;
end;
hence thesis by Th44;
end;
begin :: Problem 177
definition
let b,e be Real;
let n be Nat;
func powersFS(b,e,n) -> FinSequence of REAL means :Def7:
len it = n &
for i being Nat st 1 <= i <= n holds it.i = (b+i) to_power e;
existence
proof
deffunc F(Nat) = In((b+$1) to_power e,REAL);
consider f being FinSequence of REAL such that
A1: len f = n and
A2: for j being Nat st j in dom f holds f.j = F(j) from FINSEQ_2:sch 1;
take f;
thus len f = n by A1;
let i be Nat;
assume 1 <= i <= n;
then i in dom f by A1,FINSEQ_3:25;
then f.i = F(i) by A2;
hence thesis;
end;
uniqueness
proof
let p,q be FinSequence of REAL such that
A3: len p = n and
A4: for i being Nat st 1 <= i <= n holds p.i = (b+i) to_power e and
A5: len q = n and
A6: for i being Nat st 1 <= i <= n holds q.i = (b+i) to_power e;
thus len p = len q by A3,A5;
let k such that
A7: 1 <= k & k <= len p;
thus p.k = (b+k) to_power e by A3,A4,A7
.= q.k by A3,A6,A7;
end;
end;
theorem Th47:
powersFS(-(k+1),r,2*(k+1)) =
<* (-k) to_power r *> ^ powersFS(-k,r,2*k) ^ <* (k+1) to_power r *>
proof
set F = powersFS(-(k+1),r,2*(k+1));
set f = powersFS(-k,r,2*k);
set g = <*(-k) to_power r*>;
set h = <*(k+1) to_power r*>;
A1: len F = 2*(k+1) by Def7;
A2: len g = 1 by FINSEQ_1:39;
A3: len f = 2*k by Def7;
A4: len h = 1 by FINSEQ_1:39;
A5: len(g^f) = len g + len f by FINSEQ_1:22;
then len(g^f^h) = len g + len f + len h by FINSEQ_1:22;
hence len F = len(g^f^h) by A2,A3,A4,Def7;
let a such that
A6: 1 <= a & a <= len F;
A7: F.a = (-(k+1)+a) to_power r by A1,A6,Def7;
per cases by A6,XXREAL_0:1;
suppose a = 1;
hence F.a = (g^(f^h)).a by A7
.= (g^f^h).a by FINSEQ_1:32;
end;
suppose that
A8: 1 < a and
A9: a < len F;
a < len g + len f + 1 by A2,A3,A9,Def7;
then
A10: a <= len g + len f by NAT_1:13;
then
A11: a in dom(g^f) by A5,A8,FINSEQ_3:25;
A12: len g + 1 <= a by A2,A8,NAT_1:13;
A13: 1 <= a-1 by A8,INT_1:52;
A14: a-1 <= 1+len f-1 by A2,A10,XREAL_1:9;
thus F.a = (-k+(a-1)) to_power r by A7
.= f.(a-1) by A3,A8,A13,A14,Def7
.= (g^f).a by A2,A10,A12,FINSEQ_1:23
.= (g^f^h).a by A11,FINSEQ_1:def 7;
end;
suppose
A15: a = len F;
then a = len(g^f)+1 by A2,A3,A5,Def7;
hence (g^f^h).a = F.a by A1,A7,A15;
end;
end;
theorem Th48:
for k being positive Nat holds
powersFS(-(k+1),r,2*(k+1)-1) =
<* (-k) to_power r *> ^ powersFS(-k,r,2*k-1) ^ <* k to_power r *>
proof
let k be positive Nat;
set F = powersFS(-(k+1),r,2*(k+1)-1);
set f = powersFS(-k,r,2*k-1);
set g = <*(-k) to_power r*>;
set h = <*k to_power r*>;
A1: len F = 2*(k+1)-1 by Def7;
A2: len g = 1 by FINSEQ_1:39;
A3: len f = 2*k-1 by Def7;
A4: len h = 1 by FINSEQ_1:39;
A5: len(g^f) = len g + len f by FINSEQ_1:22;
then len(g^f^h) = len g + len f + len h by FINSEQ_1:22;
hence len F = len(g^f^h) by A2,A3,A4,Def7;
let a such that
A6: 1 <= a & a <= len F;
A7: F.a = (-(k+1)+a) to_power r by A1,A6,Def7;
per cases by A6,XXREAL_0:1;
suppose a = 1;
hence F.a = (g^(f^h)).a by A7
.= (g^f^h).a by FINSEQ_1:32;
end;
suppose that
A8: 1 < a and
A9: a < len F;
a < len g + len f + 1 by A2,A3,A9,Def7;
then
A10: a <= len g + len f by NAT_1:13;
then
A11: a in dom(g^f) by A5,A8,FINSEQ_3:25;
A12: len g + 1 <= a by A2,A8,NAT_1:13;
A13: 1 <= a-1 by A8,INT_1:52;
thus F.a = (-k+(a-1)) to_power r by A7
.= f.(a-1) by A2,A3,A8,A13,A10,XREAL_1:9,Def7
.= (g^f).a by A2,A10,A12,FINSEQ_1:23
.= (g^f^h).a by A11,FINSEQ_1:def 7;
end;
suppose
A14: a = len F;
then a = len(g^f)+1 by A2,A3,A5,Def7;
hence (g^f^h).a = F.a by A1,A7,A14;
end;
end;
theorem Th49:
Sum powersFS(-k,3,2*k) = k|^3
proof
defpred P[Nat] means Sum powersFS(-$1,3,2*$1) = $1|^3;
A1: P[0]
proof
set f = powersFS(-0,3,2*0);
len f = 0 by Def7;
then f = {};
hence Sum f = 0|^3;
end;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: P[n];
set f = powersFS(-(n+1),3,2*(n+1));
set g = powersFS(-n,3,2*n);
set a = (-n) to_power 3;
set b = (n+1) to_power 3;
A4: Sum(<*a*>^g) = a + Sum g by RVSUM_1:76;
A5: n|^3 = n*n*n & (n+1)|^3 = (n+1)*(n+1)*(n+1) &
(-n) to_power 3 = (-n)*(-n)*(-n) & (n+1) to_power 3 = (n+1)*(n+1)*(n+1)
by POLYEQ_5:2;
f = <*a*> ^ g ^ <*b*> by Th47;
hence Sum f = Sum(<*a*>^g) + b by RVSUM_1:74
.= (n+1)|^3 by A3,A4,A5;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th50:
for k being positive Nat holds Sum powersFS(-k,3,2*k-1) = 0
proof
let k be positive Nat;
defpred P[non zero Nat] means Sum powersFS(-$1,3,2*$1-1) = 0;
A1: P[1]
proof
set f = powersFS(-1,3,2*1-1);
len f = 1 & f.1 = (-1+1) to_power 3 by Def7;
then f = <*0*> by FINSEQ_1:40;
hence Sum f = 0;
end;
A2: for n being non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat such that
A3: P[n];
set f = powersFS(-(n+1),3,2*(n+1)-1);
set g = powersFS(-n,3,2*n-1);
set a = (-n) to_power 3;
set b = n to_power 3;
A4: Sum(<*a*>^g) = a + Sum g by RVSUM_1:76;
A5: (-n) to_power 3 = (-n)*(-n)*(-n) & n to_power 3 = n*n*n
by POLYEQ_5:2;
f = <*a*> ^ g ^ <*b*> by Th48;
hence Sum f = a + b by A3,A4,RVSUM_1:74
.= 0 by A5;
end;
for n being non zero Nat holds P[n] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
:: Problem 177
theorem
for n being positive Nat
ex x being Integer, y being Nat st Sum powersFS(x,3,n) = y|^3
proof
let n be positive Nat;
per cases;
suppose n is even;
then consider k such that
A1: n = 2*k;
take -k,k;
thus thesis by A1,Th49;
end;
suppose n is odd;
then consider k such that
A2: n = 2*k+1 by ABIAN:9;
take -(k+1),0;
n = 2*(k+1)-1 by A2;
hence thesis by Th50;
end;
end;
begin :: Problem 179
:: Problem 179
theorem
for x being Real holds
(x+1)|^3 + (x+2)|^3 + (x+3)|^3 + (x+4)|^3 = (x+10)|^3 iff x = 10
proof
let x be Real;
A1: (x+1)|^3 = (x+1)*(x+1)*(x+1) by POLYEQ_5:2;
A2: (x+2)|^3 = (x+2)*(x+2)*(x+2) by POLYEQ_5:2;
A3: (x+3)|^3 = (x+3)*(x+3)*(x+3) by POLYEQ_5:2;
A4: (x+4)|^3 = (x+4)*(x+4)*(x+4) by POLYEQ_5:2;
A5: (x+10)|^3 = (x+10)*(x+10)*(x+10) by POLYEQ_5:2;
thus (x+1)|^3 + (x+2)|^3 + (x+3)|^3 + (x+4)|^3 = (x+10)|^3 implies x = 10
proof
set t = x-10;
assume (x+1)|^3 + (x+2)|^3 + (x+3)|^3 + (x+4)|^3 = (x+10)|^3;
then t*(t*t+30*t+230) = 0 by A1,A2,A3,A4,A5;
then
A6: t = 0 or 1*t^2+30*t+230 = 0;
delta(1,30,230) = -20;
hence thesis by A6,QUIN_1:3;
end;
thus thesis by A1,A2,A3,A4,A5;
end;
begin :: Problem 186
:: Problem 186
theorem
{ [x,y] where x,y is positive Nat: 2|^x + 1 = y^2 } = { [3,3] }
proof
set A = { [x,y] where x,y is positive Nat: 2|^x + 1 = y^2 };
thus A c= {[3,3]}
proof
let a be object;
assume a in A;
then consider x,y being positive Nat such that
A1: a = [x,y] and
A2: 2|^x + 1 = y^2;
A3: (y+1)*(y-1) = 2|^x by A2;
y-1 divides (y+1)*(y-1);
then consider k being Nat such that
A4: y-1 = 2|^k by A2,XPRIMES1:2,NEWTON03:36;
y+1 divides (y+1)*(y-1);
then consider s being Nat such that
A5: y+1 = 2|^s by A2,XPRIMES1:2,NEWTON03:36;
y-1 < y+1 by XREAL_1:8;
then
A6: k < s by A4,A5,PREPOWER:93;
(2|^k)*(2|^s) = 2|^(k+s) by NEWTON:8;
then
A7: x = k+s by A3,A4,A5,PEPIN:30;
A8: 2|^s - 2|^k = 2 by A4,A5;
A9: now
assume k <= 0;
then k = 0;
then y-1 = 1 by A4,NEWTON:4;
then 2|^s = 2*1+1 by A5;
hence contradiction by A6;
end;
2|^k divides 2|^s by A6,PEPIN:31;
then
A10: 2|^k divides 2|^1 by A8,INT_5:1;
then
A11: k = 1 by A9,NAT_1:25,PEPIN:31;
2|^s = 2|^k + 2 by A4,A5;
then
A12: s = 2 by A11,Lm1,PEPIN:30;
y-1 = 2 by A4,A9,A10,NAT_1:25,PEPIN:31;
hence thesis by A1,A7,A11,A12,TARSKI:def 1;
end;
let a be object;
assume a in {[3,3]};
then
A13: a = [3,3] by TARSKI:def 1;
2|^3 + 1 = 3^2 by Lm2;
hence thesis by A13;
end;
begin :: Problem 187
:: Problem 187
theorem
{ [x,y] where x,y is positive Nat: 2|^x - 1 = y^2 } = { [1,1] }
proof
set A = { [x,y] where x,y is positive Nat: 2|^x - 1 = y^2 };
thus A c= {[1,1]}
proof
let a be object;
assume a in A;
then consider x,y being positive Nat such that
A1: a = [x,y] and
A2: 2|^x - 1 = y^2;
per cases;
suppose x > 1;
then x >= 1+1 by NAT_1:13;
then consider k being positive Nat such that
A3: 2|^x-1 = 4*k-1 by NUMBER09:11;
A4: y^2 mod 4 = 0 or y^2 mod 4 = 1 by PYTHTRIP:3,4;
(4*k-1) mod 4 = ((4*k+0 mod 4) - (1 mod 4)) mod 4 by INT_6:7
.= (3+(-1)*4) mod 4 by NAT_D:24
.= 3 mod 4 by NAT_D:61;
hence thesis by A2,A3,A4,NAT_D:24;
end;
suppose x <= 1;
then
A5: x = 1 by NAT_1:25;
then y = 1 by A2,NAT_1:15;
hence thesis by A1,A5,TARSKI:def 1;
end;
end;
let a be object;
assume a in {[1,1]};
then
A6: a = [1,1] by TARSKI:def 1;
2|^1 - 1 = 1^2;
hence thesis by A6;
end;
begin :: Problem 189
theorem Th55:
{ [x,y] where x,y is positive Nat: (2*x+1)^2 - 2*y^2 + 1 = 0 } is infinite
proof
deffunc R(Complex,Complex) = (2*$1+1)^2-2*$2^2+1;
set A = {[x,y] where x,y is positive Nat: R(x,y) = 0};
A1: R(3,5) = 0;
then [3,5] in A;
then reconsider A as non empty set;
deffunc p1(Real,Real) = 3*$1+2*$2+1;
deffunc p2(Real,Real) = 4*$1+3*$2+2;
defpred P[object,Element of [:NAT,NAT:],Element of [:NAT,NAT:]] means
$3 = [p1($2`1,$2`2),p2($2`1,$2`2)];
set f = recSeqCart(3,5,3,2,1,4,3,2);
A2: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [3,5] by NUMBER08:def 10;
then
A3: N[0] by A1;
A4: N[a] implies N[a+1]
proof
assume N[a];
then consider x,y being positive Nat such that
A5: f.a = [x,y] & R(x,y) = 0;
set m = (f.a)`1;
set n = (f.a)`2;
A6: f.(a+1) = [p1(m,n),p2(m,n)] by NUMBER08:def 10;
R(p1(m,n),p2(m,n)) = 0 by A5;
hence thesis by A6;
end;
A7: N[a] from NAT_1:sch 2(A3,A4);
A8: 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 A7;
end;
f is one-to-one by NUMBER08:92;
hence thesis by A2,A8,CARD_1:59;
end;
:: Problem 189
theorem
{ [x,y] where x,y is positive Nat: x^2 + (x+1)^2 = y^2 } is infinite
proof
set A = { [x,y] where x,y is positive Nat: (2*x+1)^2-2*y^2+1 = 0 };
set B = { [x,y] where x,y is positive Nat: x^2+(x+1)^2 = y^2 };
A = B
proof
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y being positive Nat such that
A1: a = [x,y] & (2*x+1)^2-2*y^2+1 = 0;
(2*x+1)^2-2*y^2+1 = 2*(x^2+(x+1)^2-y^2);
hence thesis by A1;
end;
let a be object;
assume a in B;
then consider x,y being positive Nat such that
A2: a = [x,y] & x^2+(x+1)^2 = y^2;
(2*x+1)^2-2*y^2+1 = 2*(x^2+(x+1)^2-y^2);
hence thesis by A2;
end;
hence thesis by Th55;
end;
begin :: Problem 190
theorem Th57:
{ [x,y] where x,y is positive Nat: 3*x^2 + 3*x - y^2 + 1 = 0 } is infinite
proof
deffunc R(Complex,Complex) = 3*$1^2+3*$1-$2^2+1;
set A = {[x,y] where x,y is positive Nat: R(x,y) = 0};
A1: R(7,13) = 0;
then [7,13] in A;
then reconsider A as non empty set;
deffunc p1(Real,Real) = 7*$1+4*$2+3;
deffunc p2(Real,Real) = 12*$1+7*$2+6;
defpred P[object,Element of [:NAT,NAT:],Element of [:NAT,NAT:]] means
$3 = [p1($2`1,$2`2),p2($2`1,$2`2)];
set f = recSeqCart(7,13,7,4,3,12,7,6);
A2: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [7,13] by NUMBER08:def 10;
then
A3: N[0] by A1;
A4: N[a] implies N[a+1]
proof
assume N[a];
then consider x,y being positive Nat such that
A5: f.a = [x,y] & R(x,y) = 0;
set m = (f.a)`1;
set n = (f.a)`2;
A6: f.(a+1) = [p1(m,n),p2(m,n)] by NUMBER08:def 10;
R(p1(m,n),p2(m,n)) = 0 by A5;
hence thesis by A6;
end;
A7: N[a] from NAT_1:sch 2(A3,A4);
A8: 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 A7;
end;
f is one-to-one by NUMBER08:92;
hence thesis by A2,A8,CARD_1:59;
end;
Lm13:
now
let x,y be Complex;
(x+1)|^3 = (x+1)*(x+1)*(x+1) & x|^3 = x*x*x by POLYEQ_5:2;
hence (x+1)|^3 - x|^3 - y^2 = 3*x^2 + 3*x - y^2 + 1;
end;
:: Problem 190
theorem
{ [x,y] where x,y is positive Nat: (x+1)|^3 - x|^3 = y^2 } is infinite
proof
set A = { [x,y] where x,y is positive Nat: (x+1)|^3 - x|^3 = y^2 };
set B = { [x,y] where x,y is positive Nat: 3*x^2 + 3*x - y^2 + 1 = 0 };
A = B
proof
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y being positive Nat such that
A1: a = [x,y] & (x+1)|^3 - x|^3 = y^2;
(x+1)|^3 - x|^3 - y^2 = 3*x^2 + 3*x - y^2 + 1 by Lm13;
hence thesis by A1;
end;
let a be object;
assume a in B;
then consider x,y being positive Nat such that
A2: a = [x,y] & 3*x^2 + 3*x - y^2 + 1 = 0;
(x+1)|^3 - x|^3 - y^2 = 3*x^2 + 3*x - y^2 + 1 by Lm13;
hence thesis by A2;
end;
hence thesis by Th57;
end;
begin :: Problem 193
Lm14:
(2*n)^2 mod 8 = 0 or (2*n)^2 mod 8 = 4
proof
(2*n)^2 mod 8 = (4*n^2) mod 8;
hence thesis by NUMBER07:8;
end;
Lm15:
(2*i)^2 mod 8 = 0 or (2*i)^2 mod 8 = 4
proof
per cases;
suppose i >= 0;
then i in NAT by INT_1:3;
hence thesis by Lm14;
end;
suppose i < 0;
then
A1: -i in NAT by INT_1:3;
(2*i)^2 = (2*(-i))^2;
hence thesis by A1,Lm14;
end;
end;
theorem Th59:
i is even implies i^2 mod 8 = 0 or i^2 mod 8 = 4
proof
assume i is even;
then ex j st i = 2*j by ABIAN:11;
hence thesis by Lm15;
end;
Lm16:
(2*i+1)^2 mod 8 = 1
proof
per cases;
suppose 2*i+1 >= 0;
then 2*i+1 in NAT by INT_1:3;
hence thesis by NUMBER05:41;
end;
suppose 2*i+1 < 0;
then
A1: -(2*i+1) in NAT by INT_1:3;
(2*i+1)^2 = (-(2*i+1))^2;
hence thesis by A1,NUMBER05:41;
end;
end;
theorem Th60:
i is odd implies i^2 mod 8 = 1
proof
assume i is odd;
then ex j st i = 2*j+1 by ABIAN:1;
hence thesis by Lm16;
end;
theorem
i^2 mod 8 = 0 or i^2 mod 8 = 1 or i^2 mod 8 = 4 by Th59,Th60;
Lm17:
p = 4*k+3 & p divides a^2+b^2 implies p divides a & p divides b
proof
assume that
A1: p = 4*k+3 and
A2: p divides a^2+b^2;
assume
A3: not p divides a or not p divides b;
A4: a|^2 = a^2 by WSIERP_1:1;
A5: b|^2 = b^2 by WSIERP_1:1;
A6: now
assume
A7: not p divides a;
assume
A8: p divides b;
b divides b^2;
then p divides b^2 by A8,INT_2:9;
then p divides a^2+b^2-b^2 by A2,INT_5:1;
hence contradiction by A4,A7,NAT_3:5;
end;
A9: now
assume
A10: not p divides b;
assume
A11: p divides a;
a divides a^2;
then p divides a^2 by A11,INT_2:9;
then p divides a^2+b^2-a^2 by A2,INT_5:1;
hence contradiction by A5,A10,NAT_3:5;
end;
A12: Euler p = p-1 by EULER_1:20;
A13: 4*k+1+2 > 0+2 by XREAL_1:6;
per cases;
suppose a = 0 & b = 0;
hence thesis by A3,INT_2:12;
end;
suppose a <> 0 & b = 0 or a = 0 & b <> 0;
hence thesis by A2,A3,A4,A5,NAT_3:5,INT_2:12;
end;
suppose
A14: a <> 0 & b <> 0;
a,p are_coprime & b,p are_coprime by A3,A6,A9,Th4;
then a|^(p-1) mod p = 1 & b|^(p-1) mod p = 1
by A12,A14,EULER_2:18,INT_2:def 4;
then (a|^(p-1) + b|^(p-1)) mod p = (1+1) mod p by NAT_D:66
.= 2 by A1,A13,NAT_D:24;
then
A15: not p divides (a|^(p-1) + b|^(p-1));
A16: a|^(p-1) = a|^(2*(2*k+1)) by A1
.= a|^2|^(2*k+1) by NEWTON:9;
A17: b|^(p-1) = b|^(2*(2*k+1)) by A1
.= b|^2|^(2*k+1) by NEWTON:9;
a|^2+b|^2 divides a|^2|^(2*k+1)+b|^2|^(2*k+1) by NEWTON01:35;
hence thesis by A2,A4,A5,A15,A16,A17,INT_2:9;
end;
end;
theorem Th62:
p = 4*k+3 & p divides i^2+j^2 implies p divides i & p divides j
proof
assume
A1: p = 4*k+3 & p divides i^2+j^2;
A2: i^2 = (-i)^2;
A3: j^2 = (-j)^2;
per cases;
suppose i >= 0 & j >= 0;
then i in NAT & j in NAT by INT_1:3;
hence thesis by A1,Lm17;
end;
suppose i >= 0 & j < 0;
then i in NAT & -j in NAT by INT_1:3;
then p divides i & p divides -j by A1,A3,Lm17;
hence thesis by INT_2:10;
end;
suppose i < 0 & j >= 0;
then -i in NAT & j in NAT by INT_1:3;
then p divides -i & p divides j by A1,A2,Lm17;
hence thesis by INT_2:10;
end;
suppose i < 0 & j < 0;
then -i in NAT & -j in NAT by INT_1:3;
then p divides -i & p divides -j by A1,A2,A3,Lm17;
hence thesis by INT_2:10;
end;
end;
Lm18:
now
let n,i;
assume
A1: 4*n+3 is prime;
assume 4*n+3 divides i^2+1^2;
then 4*n+3 divides 1 by A1,Th62;
hence contradiction by A1,NAT_D:7;
end;
:: Problem 193
theorem
x|^2 - y|^3 <> 7
proof
assume
A1: x|^2 - y|^3 = 7;
A2: x|^2 = x^2 by WSIERP_1:1;
A3: y|^3 = y*y*y by POLYEQ_5:2;
per cases;
suppose y is even;
then consider i such that
A4: y = 2*i by ABIAN:11;
i|^3 = i*i*i by POLYEQ_5:2;
then
A5: y|^3 = 8*i|^3 + 0 by A3,A4;
A6: x^2 mod 8 = 0 or x^2 mod 8 = 1 or x^2 mod 8 = 4 by Th59,Th60;
(x|^2 - 7) mod 8 = (x|^2-7+8*1) mod 8 by NAT_D:61;
then (x|^2 - 7) mod 8 = (x|^2 + 1) mod 8
.= ((x|^2 mod 8) + (1 mod 8)) mod 8 by NAT_D:66;
then (x|^2 - 7) mod 8 = (0+1) mod 8 or (x|^2 - 7) mod 8 = (1+1) mod 8
or (x|^2 - 7) mod 8 = (4+1) mod 8 by A2,A6,NAT_D:24;
hence thesis by A1,A5,NAT_D:24;
end;
suppose y is odd;
then consider k being Integer such that
A7: y = 2*k+1 by ABIAN:1;
x|^2+1 = y|^3+8 by A1
.= (y+2)*((y-1)^2+3) by A3;
then
A8: 4*k^2+3 divides x|^2+1 by A7;
ex p,q being Nat st p = 4*q+3 & p is prime & p divides 4*k^2+3
by NUMBER05:3;
hence thesis by A2,A8,INT_2:9,Lm18;
end;
end;
begin :: Problem 194
Lm19:
now
let i;
(2*i)|^3 = (2*i)*(2*i)*(2*i) by POLYEQ_5:2
.= 8*(i*i*i)+0;
hence (2*i)|^3 mod 8 = 0;
end;
:: Problem 194
theorem
for c being odd Nat holds x|^2 - y|^3 <> (2*c)|^3 - 1
proof
A1: x|^2 = x^2 by WSIERP_1:1;
let c be odd Nat;
assume
A2: x|^2 - y|^3 = (2*c)|^3 - 1;
A3: (2*c)|^3 = (2*c)*(2*c)*(2*c) by POLYEQ_5:2;
per cases;
suppose y is odd;
then consider s being Integer such that
A4: y-c = 2*s by ABIAN:11;
A5: 3 mod 8 = 3 by NAT_D:24;
c^2 mod 8 = 1 by Th60;
then 3 = ((3 mod 8) * (c^2 mod 8)) mod 8 by NAT_D:24
.= 3*c^2 mod 8 by NAT_D:67;
then consider j such that
A6: 3*c^2 = j*8+3 by A5,NAT_D:64,NAT_6:9;
j*8+3-3 >= 3-3 by A6,XREAL_1:66;
then j >= 0;
then reconsider j as Element of NAT by INT_1:3;
(y-c)^2+3*c^2 = (2*s)^2+(8*j+3) by A4,A6
.= 4*(s^2+2*j)+3;
then consider p,q being Nat such that
A7: p = 4*q+3 and
A8: p is prime and
A9: p divides (y-c)^2+3*c^2 by NUMBER05:3;
y|^3 = y*y*y by POLYEQ_5:2;
then (y+2*c)*((y-c)^2+3*c^2) = (2*c)|^3 + y|^3 by A3
.= x|^2 + 1 by A2;
then (y-c)^2+3*c^2 divides x^2+1 by A1;
hence thesis by A7,A8,A9,Lm18,INT_2:9;
end;
suppose y is even;
then consider i such that
A10: y = 2*i by ABIAN:11;
(2*i)|^3 mod 8 = 0 & (2*c)|^3 mod 8 = 0 by Lm19;
then (y|^3 + (2*c)|^3) mod 8 = (0+0) mod 8 by A10,NAT_D:66;
then (y|^3 + (2*c)|^3 - 1) mod 8 = ((0 mod 8) - (1 mod 8)) mod 8
by INT_6:7
.= (7+(-1)*8) mod 8 by NAT_D:24
.= 7 mod 8 by NAT_D:61;
then x^2 mod 8 = 7 by A1,A2,NAT_D:24;
hence thesis by Th59,Th60;
end;
end;
begin :: Problem 197
registration
let f,g be positive-yielding FinSequence;
cluster f^g -> positive-yielding;
coherence
proof
let r be Real;
assume r in rng(f^g);
then r in rng f \/ rng g by FINSEQ_1:31;
then r in rng f or r in rng g by XBOOLE_0:def 3;
hence thesis by PARTFUN3:def 1;
end;
end;
registration
let x be positive Real;
cluster <*x*> -> positive-yielding;
coherence
proof
let r be Real;
assume r in rng <*x*>;
then r in {x} by FINSEQ_1:38;
hence thesis by TARSKI:def 1;
end;
end;
registration
let x,y be positive Real;
cluster <*x,y*> -> positive-yielding;
coherence;
end;
:: Problem 197
theorem
n > 0 implies
ex f being positive-yielding FinSequence of NAT st
len f = n & Sum f = Product f
proof
assume
A1: n > 0;
(n = 0 or ... or n = 2) or n > 2;
then per cases by A1;
suppose
A2: n = 1;
set f = <*the positive Nat*>;
reconsider f as positive-yielding FinSequence of NAT by FINSEQ_1:103;
take f;
thus len f = n by A2,FINSEQ_1:39;
thus thesis;
end;
suppose n >= 2;
then reconsider n2 = n-2 as Element of NAT by INT_1:5;
set g = n2|->1;
set f = g^<*2,n*>;
reconsider f as positive-yielding FinSequence of NAT
by A1,FINSEQ_1:102;
take f;
len <*2,n*> = 2 by FINSEQ_1:44;
hence n = len g + len <*2,n*>
.= len f by FINSEQ_1:22;
A3: Product <*2,n*> = 2*n by RVSUM_1:99;
A4: Product g = 1 by RVSUM_1:102;
A5: Sum <*2,n*> = 2+n by RVSUM_1:77;
A6: Sum g = (n-2)*1 by RVSUM_1:80;
thus Sum f = Sum g + Sum <*2,n*> by RVSUM_1:75
.= Product g * Product <*2,n*> by A3,A4,A5,A6
.= Product f by RVSUM_1:97;
end;
end;
begin :: Problem 199
theorem
for x,y being positive Nat st y*(3*y-1) = x*(x+1)
holds Polygon(3,x) = Polygon(5,y);
theorem Th67:
for m,n being positive Nat, s being natural Number
st Polygon(s,m) = Polygon(s,n) & s >= 2 holds m = n
proof
let m,n be positive Nat;
let s be natural Number;
assume Polygon(s,m) = Polygon(s,n);
then m^2*(s-2) - m*(s-4) - n^2*(s-2) + n*(s-4) = 0;
then (m-n) * ((s-2)*(m+n-1)+2) = 0;
then
A1: m-n = 0 or (s-2)*(m+n-1)+2 = 0;
assume
A2: s >= 2;
now
assume
A3: (s-2)*(m+n-1)+2 = 0;
s-2 >= 2-2 by A2,XREAL_1:6;
hence contradiction by A3;
end;
hence thesis by A1;
end;
theorem Th68:
{ [x,y] where x,y is positive Nat: y*(3*y-1) - x*(x+1) = 0 } is infinite
proof
deffunc R(Complex,Complex) = $2*(3*$2-1)-$1*($1+1);
set A = {[x,y] where x,y is positive Nat: R(x,y) = 0};
A1: R(1,1) = 0;
then [1,1] in A;
then reconsider A as non empty set;
deffunc p1(Real,Real) = 7*$1+12*$2+1;
deffunc p2(Real,Real) = 4*$1+7*$2+1;
defpred P[object,Element of [:NAT,NAT:],Element of [:NAT,NAT:]] means
$3 = [p1($2`1,$2`2),p2($2`1,$2`2)];
set f = recSeqCart(1,1,7,12,1,4,7,1);
A2: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [1,1] by NUMBER08:def 10;
then
A3: N[0] by A1;
A4: N[a] implies N[a+1]
proof
assume N[a];
then consider x,y being positive Nat such that
A5: f.a = [x,y] & R(x,y) = 0;
set m = (f.a)`1;
set n = (f.a)`2;
A6: f.(a+1) = [p1(m,n),p2(m,n)] by NUMBER08:def 10;
R(p1(m,n),p2(m,n)) = 0 by A5;
hence thesis by A6;
end;
A7: N[a] from NAT_1:sch 2(A3,A4);
A8: 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 A7;
end;
f is one-to-one by NUMBER08:92;
hence thesis by A2,A8,CARD_1:59;
end;
Lm20: 1/3 is not integer by NAT_D:33;
:: Problem 199
theorem
{ n where n is 3-gonal Nat: n is 5-gonal } is infinite
proof
set A = { n where n is 3-gonal Nat: n is 5-gonal };
set B = { [x,y] where x,y is positive Nat: y*(3*y-1) - x*(x+1) = 0 };
defpred P[object,object] means
ex n being positive Nat st n = $1`1 & $2 = Polygon(3,n);
A1: for e being object st e in B ex u being object st P[e,u]
proof
let e be object;
assume e in B;
then consider x,y being positive Nat such that
A2: e = [x,y] and y*(3*y-1) - x*(x+1) = 0;
take u = Polygon(3,x), n = x;
thus n = e`1 by A2;
thus u = Polygon(3,n);
end;
consider f being Function such that
A3: dom f = B and
A4: for e being object st e in B holds P[e,f.e] from CLASSES1:sch 1(A1);
A5: f is one-to-one
proof
let x1,x2 be object such that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1 = f.x2;
consider n1 being positive Nat such that
A9: n1 = x1`1 and
A10: f.x1 = Polygon(3,n1) by A3,A4,A6;
consider n2 being positive Nat such that
A11: n2 = x2`1 & f.x2 = Polygon(3,n2) by A3,A4,A7;
consider c1,d1 being positive Nat such that
A12: x1 = [c1,d1] and
A13: d1*(3*d1-1) - c1*(c1+1) = 0 by A3,A6;
consider c2,d2 being positive Nat such that
A14: x2 = [c2,d2] and
A15: d2*(3*d2-1) - c2*(c2+1) = 0 by A3,A7;
A16: 3*(d1*d1-d2*d2) = d1-d2 by A8,A9,A10,A11,A12,A13,A14,A15;
now
assume d1 <> d2;
then per cases by XXREAL_0:1;
suppose d1 < d2;
then consider z being positive Nat such that
A17: d2 = d1+z by Th1;
3*(d1*d1-(d1+z)*(d1+z)) = d1-d1-z by A16,A17;
then 3*(2*d1+z)*z = 1*z;
then 3*(2*d1+z) = 1 by XCMPLX_1:5;
hence contradiction by Lm20;
end;
suppose d2 < d1;
then consider z being positive Nat such that
A18: d1 = d2+z by Th1;
3*(2*d2+z)*z = 1*z by A16,A18;
then 3*(2*d2+z) = 1 by XCMPLX_1:5;
hence contradiction by Lm20;
end;
end;
hence thesis by A8,A9,A10,A11,A12,A14,Th67;
end;
rng f c= A
proof
let t be object;
assume t in rng f;
then consider s being object such that
A19: s in dom f and
A20: f.s = t by FUNCT_1:def 3;
consider x,y being positive Nat such that
A21: s = [x,y] & y*(3*y-1) - x*(x+1) = 0 by A3,A19;
A22: P[s,f.s] by A3,A4,A19;
then f.s = Polygon(5,y) by A21;
hence thesis by A20,A22;
end;
hence thesis by A3,A5,Th68,CARD_1:59;
end;