:: Elementary Number Theory Problems. {P}art {IX}
:: 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, MEMBERED, REAL_1, MOEBIUS1, ZFMISC_1, PEPIN,
VALUED_0, CARD_3, FINSEQ_1, NUMBER02, ORDINAL1, PBOOLE, SQUARE_1,
NUMBER07, NAT_LAT, GR_CY_3, NUMBER09, NUMBER08, EC_PF_2, NUMBER06,
SETFAM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, XTUPLE_0, SETFAM_1,
ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PBOOLE, FINSET_1,
MEMBERED, VALUED_0, XREAL_0, INT_1, INT_2, NAT_1, XXREAL_0, XXREAL_2,
SQUARE_1, FINSEQ_1, PEPIN, EC_PF_2, NEWTON, WSIERP_1, ABIAN, EULER_1,
NAT_LAT, GR_CY_3, MOEBIUS1, NUMBER02, NUMBER06, NUMBER07, NUMBER08;
constructors NAT_D, RELSET_1, ABIAN, EULER_1, PEPIN, XXREAL_2, NUMBER02,
NAT_LAT, GR_CY_3, MOEBIUS1, NUMBER07, DOMAIN_1, EC_PF_2, NUMBER06,
NUMBER08, WSIERP_1;
registrations ORDINAL1, RELSET_1, FINSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, VALUED_0, CARD_1, NEWTON, NEWTON02, ABIAN, NAT_6,
JORDAN1D, XXREAL_2, NEWTON01, FINSEQ_1, XBOOLE_0, NAT_3, NUMBER02,
MOEBIUS1, VALUED_1, NAT_LAT, RAMSEY_1, SQUARE_1, NUMBER08;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, TARSKI, FUNCT_1, EC_PF_2, NUMBER02, VALUED_0, NUMBER08,
FINSEQ_1;
equalities SQUARE_1, FINSEQ_1, MOEBIUS1, XCMPLX_0, GR_CY_3, PEPIN;
expansions INT_1, INT_2, ABIAN, ZFMISC_1, NUMBER07, NAT_D;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, WSIERP_1, ORDINAL1, EULER_2,
XREAL_1, XXREAL_0, NAT_1, NAT_3, FUNCT_1, PARTFUN1, NAT_6, SQUARE_1,
NUMBER06, INT_4, TARSKI, POLYEQ_5, EULER_1, ENUMSET1, CARD_1, ABIAN,
XXREAL_2, XTUPLE_0, GR_CY_3, NAT_4, FINSEQ_1, XBOOLE_0, XPRIMES0,
XPRIMES1, NUMBER02, NUMBER04, XCMPLX_1, INT_5, NEWTON02, PREPOWER,
NUMBER07, NEWTON03, FUNCT_2, XPRIMES2, EC_PF_2, PYTHTRIP, SETFAM_1;
schemes NAT_1, PBOOLE;
begin :: Preliminaries
Lm1: 2|^0 = 1 by NEWTON:4;
Lm2: 2|^2 = 2*2 by NEWTON:81;
Lm3: 2|^3 = 2*2*2 by POLYEQ_5:2;
Lm4: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
Lm5: 2|^5 = 2*2*2*2*2 by NUMBER02:1;
Lm6: 2|^6 = 2*2*2*2*2*2 by NUMBER02:2;
Lm7: 2|^7 = 2*2*2*2*2*2*2 by NUMBER02:3;
Lm8: 2|^8 = 2*2*2*2*2*2*2*2 by NUMBER02:4;
Lm9: 2|^9 = 2*2*2*2*2*2*2*2*2 by NUMBER02:5;
reserve X for set;
reserve a,b,c,k,m,n for Nat;
reserve i,j for Integer;
reserve r,s for Real;
reserve p,p1,p2,p3 for Prime;
reserve z for Complex;
theorem Th1:
z|^11 = z*z*z*z*z*z*z*z*z*z*z
proof
A1: 11 = 10+1;
z|^10 = z*z*z*z*z*z*z*z*z*z by NUMBER02:6;
hence thesis by A1,NEWTON:6;
end;
theorem Th2:
z|^12 = z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 12 = 11+1;
z|^11 = z*z*z*z*z*z*z*z*z*z*z by Th1;
hence thesis by A1,NEWTON:6;
end;
theorem Th3:
z|^13 = z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 13 = 12+1;
z|^12 = z*z*z*z*z*z*z*z*z*z*z*z by Th2;
hence thesis by A1,NEWTON:6;
end;
theorem Th4:
z|^14 = z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 14 = 13+1;
z|^13 = z*z*z*z*z*z*z*z*z*z*z*z*z by Th3;
hence thesis by A1,NEWTON:6;
end;
theorem Th5:
z|^15 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 15 = 14+1;
z|^14 = z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th4;
hence thesis by A1,NEWTON:6;
end;
theorem Th6:
z|^16 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 16 = 15+1;
z|^15 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th5;
hence thesis by A1,NEWTON:6;
end;
theorem Th7:
z|^17 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 17 = 16+1;
z|^16 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th6;
hence thesis by A1,NEWTON:6;
end;
theorem Th8:
z|^18 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 18 = 17+1;
z|^17 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th7;
hence thesis by A1,NEWTON:6;
end;
theorem Th9:
z|^19 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 19 = 18+1;
z|^18 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th8;
hence thesis by A1,NEWTON:6;
end;
theorem Th10:
z|^20 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z
proof
A1: 20 = 19+1;
z|^19 = z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z*z by Th9;
hence thesis by A1,NEWTON:6;
end;
Lm10: 2|^11 = 2*2*2*2*2*2*2*2*2*2*2 by Th1;
Lm11: 2|^13 = 2*2*2*2*2*2*2*2*2*2*2*2*2 by Th3;
Lm12: 2|^15 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 by Th5;
Lm13: 2|^17 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 by Th7;
Lm14: 2|^19 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 by Th9;
theorem
n >= 2 implies ex k being positive Nat st 2|^n-1 = 4*k-1
proof
defpred P[Nat] means
$1 >= 2 implies ex k being positive Nat st 2|^$1-1 = 4*k-1;
A1: P[2]
proof
assume 2 >= 2;
take 1;
thus thesis by Lm2;
end;
A2: for j being Nat st 2 <= j holds P[j] implies P[j+1]
proof
let j be Nat such that
A3: 2 <= j;
assume P[j];
then consider k being positive Nat such that
A4: 2|^j-1 = 4*k-1 by A3;
assume j+1 >= 2;
take 2*k;
2|^(j+1) = 2|^j*2 by NEWTON:6;
hence thesis by A4;
end;
for i being Nat st 2 <= i holds P[i] from NAT_1:sch 8(A1,A2);
hence thesis;
end;
begin :: Problem 62
registration
cluster with_non-empty_elements -> included_in_Seg
for finite natural-membered set;
coherence
proof
let X be finite natural-membered set;
assume
A1: X is with_non-empty_elements;
per cases;
suppose X is non empty;
then reconsider Y = X as non empty finite natural-membered set;
reconsider k = max Y as Nat by TARSKI:1;
take k;
let x be object;
assume
A2: x in X;
then reconsider x as Nat;
A3: 1 <= x by A1,A2,NAT_1:25;
x <= k by A2,XXREAL_2:def 8;
hence thesis by A3;
end;
suppose X is empty;
hence thesis;
end;
end;
end;
registration let a,r be Nat;
cluster ArProg (a,r) -> natural-valued;
coherence
proof
set f = ArProg (a,r);
let x be object;
assume x in dom f;
then reconsider i = x as Nat;
defpred P[Nat] means f.$1 is natural;
A1: P[0] by NUMBER06:def 4;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
f.(k+1) = f.k + r by NUMBER06:def 4;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
then P[i];
hence thesis;
end;
end;
definition
::$CD
let i;
func Coprimes(i) -> Subset of INT equals
{ j where j is Integer: i,j are_coprime };
coherence
proof
set A = { j where j is Integer: i,j are_coprime };
A c= INT
proof
let x be object;
assume x in A;
then ex j being Integer st x = j & i,j are_coprime;
hence thesis by INT_1:def 2;
end;
hence thesis;
end;
end;
theorem Th12:
for X being included_in_Seg set st
X c= SetPrimes & p divides Product Sgm X holds p in X
proof
let X be included_in_Seg set such that
A1: X c= SetPrimes;
A2: rng Sgm X = X by FINSEQ_1:def 14;
then Sgm X is FinSequence of SetPrimes by A1,FINSEQ_1:def 4;
hence thesis by A2,NAT_3:8;
end;
Lm15:
now
let a,m;
set A = {p where p is Prime: p divides m & p divides a};
now
assume 0 in A;
then ex p being Prime st p = 0 & p divides m & p divides a;
hence contradiction;
end;
hence A is with_non-empty_elements by SETFAM_1:def 8;
end;
Lm16:
now
let a,b,m;
set A = {p where p is Prime: p divides m & not p divides a &
not p divides b};
now
assume 0 in A;
then ex p being Prime st p = 0 & p divides m & not p divides a
& not p divides b;
hence contradiction;
end;
hence A is with_non-empty_elements by SETFAM_1:def 8;
end;
Lm17:
now
let a;
let m be non zero Nat;
set A = {p where p is Prime: p divides m & p divides a};
A c= NatDivisors(m)
proof
let x be object;
assume x in A;
then ex p being Prime st x = p & p divides m & p divides a;
hence thesis;
end;
hence A is finite;
end;
Lm18:
now
let a,b;
let m be non zero Nat;
set A =
{p where p is Prime: p divides m & not p divides a & not p divides b};
A c= NatDivisors(m)
proof
let x be object;
assume x in A;
then ex p being Prime st x = p & p divides m & not p divides a &
not p divides b;
hence thesis;
end;
hence A is finite;
end;
Lm19:
now
let a;
let m be non zero Nat;
set A = {p where p is Prime: p divides m & p divides a};
A c= NAT
proof
let x be object;
assume x in A;
then ex p being Prime st x = p & p divides m & p divides a;
hence thesis by ORDINAL1:def 12;
end;
hence A is natural-membered;
end;
Lm20:
now
let a,b;
let m be non zero Nat;
set A =
{p where p is Prime: p divides m & not p divides a & not p divides b};
A c= NAT
proof
let x be object;
assume x in A;
then ex p being Prime st x = p & p divides m & not p divides a &
not p divides b;
hence thesis by ORDINAL1:def 12;
end;
hence A is natural-membered;
end;
Lm21:
now
let a;
let m be non zero Nat;
set A = {p where p is Prime: p divides m & p divides a};
A1: A is with_non-empty_elements by Lm15;
A2: A is finite by Lm17;
A is natural-membered by Lm19;
hence A is included_in_Seg by A1,A2;
end;
Lm22:
now
let a,b;
let m be non zero Nat;
set A = {p where p is Prime: p divides m & not p divides a &
not p divides b};
A1: A is with_non-empty_elements by Lm16;
A2: A is finite by Lm18;
A is natural-membered by Lm20;
hence A is included_in_Seg by A1,A2;
end;
Lm23:
now
let a,m;
thus {p where p is Prime: p divides m & p divides a} c= SetPrimes
proof
let x be object;
assume x in {p where p is Prime: p divides m & p divides a};
then ex p being Prime st x = p & p divides m & p divides a;
hence thesis by NEWTON:def 6;
end;
end;
Lm24:
now
let a,b,m;
thus {p where p is Prime: p divides m & not p divides a & not p divides b}
c= SetPrimes
proof
let x be object;
assume x in {p where p is Prime: p divides m & not p divides a &
not p divides b};
then ex p being Prime st x = p & p divides m & not p divides a &
not p divides b;
hence thesis by NEWTON:def 6;
end;
end;
theorem Th13:
for a,b being Nat, m being non zero Nat holds
a,b are_coprime implies
Product Sgm {p where p is Prime: p divides m & p divides a},
Product Sgm {q where q is Prime: q divides m & q divides b} are_coprime
proof
let a,b;
let m be non zero Nat such that
A1: a,b are_coprime;
set A = {p where p is Prime: p divides m & p divides a};
set B = {q where q is Prime: q divides m & q divides b};
assume not thesis;
then consider P being Prime such that
A2: P divides Product Sgm A and
A3: P divides Product Sgm B by PYTHTRIP:def 2;
A is included_in_Seg by Lm21;
then P in A by A2,Th12,Lm23;
then
A4: ex p being Prime st P = p & p divides m & p divides a;
B is included_in_Seg by Lm21;
then P in B by A3,Th12,Lm23;
then ex q being Prime st P = q & q divides m & q divides b;
hence contradiction by A1,A4,PYTHTRIP:def 2;
end;
theorem Th14:
for a,b being Nat, m being non zero Nat holds
Product Sgm {p where p is Prime: p divides m & p divides a},
Product Sgm
{r where r is Prime: r divides m & not r divides a & not r divides b}
are_coprime
proof
let a,b;
let m be non zero Nat;
set A = {p where p is Prime: p divides m & p divides a};
set B =
{r where r is Prime: r divides m & not r divides a & not r divides b};
assume not thesis;
then consider P being Prime such that
A1: P divides Product Sgm A and
A2: P divides Product Sgm B by PYTHTRIP:def 2;
A is included_in_Seg by Lm21;
then P in A by A1,Th12,Lm23;
then
A3: ex p being Prime st P = p & p divides m & p divides a;
B is included_in_Seg by Lm22;
then P in B by A2,Th12,Lm24;
then ex r being Prime st P = r & r divides m & not r divides a &
not r divides b;
hence thesis by A3;
end;
theorem Th15:
for a,b being Nat, m being non zero Nat holds
a,b are_coprime implies
Product Sgm {q where q is Prime: q divides m & q divides b},
Product Sgm
{r where r is Prime: r divides m & not r divides a & not r divides b}
are_coprime
proof
let a,b;
let m be non zero Nat;
set A =
{r where r is Prime: r divides m & not r divides a & not r divides b};
set B =
{r where r is Prime: r divides m & not r divides b & not r divides a};
A = B
proof
hereby
let x be object;
assume x in A;
then ex r being Prime st x = r &
r divides m & not r divides a & not r divides b;
hence x in B;
end;
let x be object;
assume x in B;
then ex r being Prime st x = r &
r divides m & not r divides b & not r divides a;
hence x in A;
end;
hence thesis by Th14;
end;
theorem Th16:
for X being included_in_Seg set holds a in X implies a divides Product Sgm X
proof
let X be included_in_Seg set;
rng Sgm X = X by FINSEQ_1:def 14;
hence thesis by NAT_3:7;
end;
:: Problem 62
theorem
for a,m being non zero Nat holds
a,b are_coprime implies rng ArProg(b,a) /\ Coprimes(m) is infinite
proof
let a,m be non zero Nat;
assume
A1: a,b are_coprime;
set P1 = {p where p is Prime: p divides m & p divides a};
set Q1 = {q where q is Prime: q divides m & q divides b};
set R1 =
{r where r is Prime: r divides m & not r divides a & not r divides b};
A2: P1 is with_non-empty_elements by Lm15;
A3: P1 is finite by Lm17;
A4: P1 is natural-membered by Lm19;
A5: Q1 is with_non-empty_elements by Lm15;
A6: Q1 is finite by Lm17;
A7: Q1 is natural-membered by Lm19;
A8: R1 is with_non-empty_elements by Lm16;
A9: R1 is finite by Lm18;
A10: R1 is natural-membered by Lm20;
set P = Product Sgm P1;
set Q = Product Sgm Q1;
set R = Product Sgm R1;
A11: a*P*R+b,m are_coprime
proof
assume not thesis;
then consider p being Prime such that
A12: p divides a*P*R+b and
A13: p divides m by PYTHTRIP:def 2;
A14: not p divides P
proof
assume
A15: p divides P;
then p divides a*R*P by INT_2:2;
then p divides a*P*R+b-a*P*R by A12,INT_5:1;
then p in Q1 by A13;
then p divides Q by A5,A6,A7,Th16;
hence thesis by A1,A15,Th13,PYTHTRIP:def 2;
end;
A16: not p divides Q
proof
assume
A17: p divides Q;
Q1 c= SetPrimes by Lm23;
then p in Q1 by A5,A6,A17,Th12;
then
A18: ex q being Prime st p = q & q divides m & q divides b;
then p divides a*P*R+b-b by A12,INT_5:1;
then p divides a*P or p divides R by INT_5:7;
then p divides a or p divides P or p divides R by INT_5:7;
hence thesis by A1,A17,A18,Th13,Th15,PYTHTRIP:def 2;
end;
A19: not p divides R
proof
assume
A20: p divides R;
then p divides a*P*R by INT_2:2;
then p divides a*P*R+b-a*P*R by A12,INT_5:1;
then p in Q1 by A13;
then p divides Q by A5,A6,A7,Th16;
hence thesis by A1,A20,Th15,PYTHTRIP:def 2;
end;
(p divides a or not p divides a) & (p divides b or not p divides b);
then p in P1 or p in Q1 or p in R1 by A13;
hence thesis by A2,A3,A4,A5,A6,A7,A8,A9,A10,A14,A16,A19,Th16;
end;
set g = ArProg(b,a);
set X = rng g /\ Coprimes(m);
A21: dom g = NAT by FUNCT_2:def 1;
A22: g.(P*R) in rng g by A21,FUNCT_1:def 3;
g.(P*R) = a*(P*R)+b by NUMBER06:7;
then g.(P*R) in Coprimes(m) by A11;
then
A23: X is non empty by A22,XBOOLE_0:def 4;
for x being Nat st x in X ex y being Nat st y > x & y in X
proof
let x be Nat;
assume
A24: x in X;
then x in rng g by XBOOLE_0:def 4;
then consider w being object such that
A25: w in dom g and
A26: g.w = x by FUNCT_1:def 3;
reconsider w as Element of NAT by A25,FUNCT_2:def 1;
take b+(m+w)*a;
A27: g.w = b + w*a by NUMBER06:7;
m+w > 0+w by XREAL_1:8;
then (m+w)*a > w*a by XREAL_1:68;
hence b+(m+w)*a > x by A26,A27,XREAL_1:8;
x in Coprimes(m) by A24,XBOOLE_0:def 4;
then ex j being Integer st x = j & j,m are_coprime;
then a*m+(b+w*a),m are_coprime by A26,A27,NUMBER04:64;
then
A28: b+(m+w)*a in Coprimes(m);
b+(m+w)*a = g.(m+w) by NUMBER06:7;
then b+(m+w)*a in rng g by A21,FUNCT_1:def 3;
hence thesis by A28,XBOOLE_0:def 4;
end;
hence thesis by A23,NUMBER04:1;
end;
begin :: Problem 91
definition
let n be Complex;
attr n is a_product_of_two_primes means
ex p1,p2 being Prime st n = p1*p2;
end;
notation
let n be Complex;
antonym n is not_a_product_of_two_primes for n is a_product_of_two_primes;
end;
registration
cluster -> not_a_product_of_two_primes for Prime;
coherence;
end;
registration
let p1,p2;
cluster p1*p2 -> a_product_of_two_primes;
coherence;
end;
theorem
a <> 1 & a <> n & a is non prime & a divides n implies
n is not_a_product_of_two_primes by GR_CY_3:1;
theorem Th19:
n is a_product_of_two_primes implies n >= 4
proof
given p,q being Prime such that
A1: n = p*q;
A2: 4 = 2*2;
1 < p & 1 < q by INT_2:def 4;
then 1+1 <= p & 1+1 <= q by NAT_1:13;
hence thesis by A1,A2,XREAL_1:66;
end;
theorem
c is_a_product_of_two_different_primes implies c is a_product_of_two_primes;
registration
let p1,p2,p3;
cluster p1*p2*p3 -> not_a_product_of_two_primes;
coherence
proof
given p,q being Prime such that
A1: p1*p2*p3 = p*q;
p1*p2 divides p1*p2*p3;
then p1*p2 = 1 or p1*p2 = p or p1*p2 = q or p1*p2 = p*q by A1,GR_CY_3:1;
then p1*p2*1 = p*q by A1;
then p3 = 1 by A1,XCMPLX_1:5;
hence contradiction by INT_2:def 4;
end;
end;
theorem
n is a_product_of_two_primes implies
for a,b st a <> 1 & b <> 1 & n = a*b holds a is prime & b is prime
by NUMBER07:59;
Lm25:
2|^n-1 <= 1000000 implies n = 0 or ... or n = 19
proof
assume
A1: 2|^n-1 <= 1000000;
A2: 2|^20 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 by Th10
.= 1048576;
per cases;
suppose n <= 19;
hence thesis;
end;
suppose n > 19;
then n >= 19+1 by NAT_1:13;
then 2|^n >= 2|^20 by PREPOWER:93;
then 2|^n-1 >= 2|^20-1 by XREAL_1:9;
hence thesis by A1,A2,XXREAL_0:2;
end;
end;
theorem Th22:
2|^n-1 is prime & 2|^n+1 is prime implies n = 2
proof
assume that
A1: 2|^n-1 is prime and
A2: 2|^n+1 is prime;
per cases;
suppose
A3: n is odd;
3 divides 2+1;
then 3 divides 2|^n + 1|^n by A3,NEWTON03:25;
then 2|^n+1 = 3 by A2;
hence thesis by A1;
end;
suppose n is even;
then consider k such that
A4: n = 2*k;
now
assume n <= 1;
then n = 0 or n = 1 by NAT_1:25;
then 1-1 is prime by A1,NEWTON:4;
hence contradiction;
end;
then
A5: n is prime by A1,GR_CY_3:28;
2 divides 2*k;
hence thesis by A4,A5;
end;
end;
registration
let n be zero Nat;
cluster Mersenne(n) -> zero;
coherence
proof
Mersenne(0) = 1-1 by NEWTON:4;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Mersenne(n) -> odd;
coherence;
end;
theorem Th23:
for p,q being Prime st p is odd & q divides Mersenne(p)
ex k being Nat st q = 2*k*p+1
proof
let p,q be Prime such that
A1: p is odd;
assume
A2: q divides Mersenne(p);
then 2|^p,1 are_congruent_mod q;
then
A3: (2|^p) mod q = 1 mod q by NAT_D:64;
A4: q > 1 by INT_2:def 4;
A5: now
assume q <= 2;
then q = 0 or ... or q = 2;
hence contradiction by A2,INT_2:def 4;
end;
then
A6: 2,q are_coprime by XPRIMES1:2,INT_2:30;
A7: now
assume order(2,q) = 1;
then (2|^1) mod q = 1 by A4,A6,PEPIN:def 2;
hence contradiction by A5,NAT_D:24;
end;
order(2,q) divides p by A3,A4,A6,PEPIN:47,NAT_D:24;
then
A8: p = order(2,q) by A7,INT_2:def 4;
A9: Euler q = q-1 by EULER_1:20;
(2 |^ Euler q) mod q = 1 by A6,EULER_2:18,INT_2:def 4;
then p divides q-1 by A4,A6,A8,A9,PEPIN:47;
then consider w being Nat such that
A10: q-1 = p*w;
A11: q = p*w+1 by A10;
then w is even by A1,A5,PEPIN:17;
then consider e being Nat such that
A12: w = 2*e;
take e;
thus thesis by A11,A12;
end;
Lm26:
now
let k;
set K = 34*k;
assume
A1: (K+1)*(K+1) <= 131071;
thus k <= 10
proof
assume k > 10;
then k >= 10+1 by NAT_1:13;
then K >= 34*11 by XREAL_1:64;
then K+1 >= 374+1 by XREAL_1:6;
then (K+1)^2 >= 375^2 by SQUARE_1:15;
hence contradiction by A1,XXREAL_0:2;
end;
end;
Lm27:
now
let k;
set K = 38*k;
assume
A1: (K+1)*(K+1) <= 524287;
thus k <= 19
proof
assume k > 19;
then k >= 19+1 by NAT_1:13;
then K >= 38*20 by XREAL_1:64;
then K+1 >= 760+1 by XREAL_1:6;
then (K+1)^2 >= 761^2 by SQUARE_1:15;
hence contradiction by A1,XXREAL_0:2;
end;
end;
theorem Th24:
Mersenne(17) is prime
proof
set M = Mersenne(17);
assume M is non prime;
then consider n being Element of NAT such that
A1: 1 < n and
A2: n*n <= M and
A3: n is prime and
A4: n divides M by Lm13,NAT_4:14;
set p = 2*8+1;
consider k being Nat such that
A5: n = 2*k*p+1 by A3,A4,XPRIMES1:17,Th23;
n = 34*k+1 by A5;
then k = 0 or ... or k = 10 by A2,Lm13,Lm26,NAT_1:60;
then per cases;
suppose k = 0;
hence contradiction by A1,A5;
end;
suppose k = 1;
hence contradiction by A3,A5,XPRIMES0:35;
end;
suppose k = 2;
hence contradiction by A3,A5,XPRIMES0:69;
end;
suppose
A6: k = 3;
M = 103*1272+55 by Lm13;
hence contradiction by A4,A5,A6,NAT_4:9;
end;
suppose
A7: k = 4;
M = 137*956+99 by Lm13;
hence contradiction by A4,A5,A7,NAT_4:9;
end;
suppose k = 5;
hence contradiction by A3,A5,XPRIMES0:171;
end;
suppose k = 6;
hence contradiction by A3,A5,XPRIMES0:205;
end;
suppose
A8: k = 7;
M = 239*548+99 by Lm13;
hence contradiction by A4,A5,A8,NAT_4:9;
end;
suppose k = 8;
hence contradiction by A3,A5,XPRIMES0:273;
end;
suppose
A9: k = 9;
M = 307*426+289 by Lm13;
hence contradiction by A4,A5,A9,NAT_4:9;
end;
suppose k = 10;
hence contradiction by A3,A5,XPRIMES0:341;
end;
end;
theorem Th25:
Mersenne(19) is prime
proof
set M = Mersenne(19);
assume M is non prime;
then consider n being Element of NAT such that
A1: 1 < n and
A2: n*n <= M and
A3: n is prime and
A4: n divides M by Lm14,NAT_4:14;
set p = 2*9+1;
consider k being Nat such that
A5: n = 2*k*p+1 by A3,A4,XPRIMES1:19,Th23;
n = 38*k+1 by A5;
then k = 0 or ... or k = 19 by A2,Lm14,Lm27,NAT_1:60;
then per cases;
suppose k = 0;
hence contradiction by A1,A5;
end;
suppose k = 1;
hence contradiction by A3,A5,XPRIMES0:39;
end;
suppose k = 2;
hence contradiction by A3,A5,XPRIMES0:77;
end;
suppose k = 3;
hence contradiction by A3,A5,XPRIMES0:115;
end;
suppose k = 4;
hence contradiction by A3,A5,XPRIMES0:153;
end;
suppose
A6: k = 5;
M = 191*2744+183 by Lm14;
hence contradiction by A4,A5,A6,NAT_4:9;
end;
suppose
A7: k = 6;
M = 229*2289+106 by Lm14;
hence contradiction by A4,A5,A7,NAT_4:9;
end;
suppose k = 7;
hence contradiction by A3,A5,XPRIMES0:267;
end;
suppose k = 8;
hence contradiction by A3,A5,XPRIMES0:305;
end;
suppose k = 9;
hence contradiction by A3,A5,XPRIMES0:343;
end;
suppose k = 10;
hence contradiction by A3,A5,XPRIMES0:381;
end;
suppose
A8: k = 11;
M = 419*1251+118 by Lm14;
hence contradiction by A4,A5,A8,NAT_4:9;
end;
suppose
A9: k = 12;
M = 457*1147+108 by Lm14;
hence contradiction by A4,A5,A9,NAT_4:9;
end;
suppose k = 13;
hence contradiction by A3,A5,XPRIMES0:495;
end;
suppose k = 14;
hence contradiction by A3,A5,XPRIMES0:533;
end;
suppose
A10: k = 15;
M = 571*918+109 by Lm14;
hence contradiction by A4,A5,A10,NAT_4:9;
end;
suppose k = 16;
hence contradiction by A3,A5,XPRIMES0:609;
end;
suppose
A11: k = 17;
M = 647*810+217 by Lm14;
hence contradiction by A4,A5,A11,NAT_4:9;
end;
suppose k = 18;
hence contradiction by A3,A5,XPRIMES0:685;
end;
suppose k = 19;
hence contradiction by A3,A5,XPRIMES0:723;
end;
end;
:: Problem 91 a
theorem
{2|^n-1 where n is Nat: 2|^n-1 <= 10|^6 & 2|^n-1 is a_product_of_two_primes}
= { 2|^4-1, 2|^9-1, 2|^11-1 }
proof
set A =
{2|^n-1: 2|^n-1 <= 10|^6 & 2|^n-1 is a_product_of_two_primes};
set B = {2|^4-1,2|^9-1,2|^11-1};
A1: 10|^6 = 10*10*10*10*10*10 by NUMBER02:2;
thus A c= B
proof
let x be object;
assume x in A;
then consider n such that
A2: x = 2|^n-1 and
A3: 2|^n-1 <= 10|^6 and
A4: 2|^n-1 is a_product_of_two_primes;
A5: now
assume n < 2+1 & 2 = 3-1;
then n = 0 or ... or n = 2 by NUMBER02:7;
hence contradiction by A4,Th19,Lm1,Lm2;
end;
A6: now
assume n is even;
then consider k such that
A7: n = 2*k;
A8: 2|^k+1 <> 0+1;
now
assume 2|^k = 2|^1;
then k = 1 by PEPIN:30;
hence contradiction by A7,A4,Th19,Lm2;
end;
then
A9: 2|^k-1 <> 2-1;
2|^(2*k) = 2|^k|^2 by NEWTON:9
.= (2|^k)^2 by WSIERP_1:1;
then 2|^n-1 = (2|^k+1)*(2|^k-1) by A7;
then 2|^k+1 is prime & 2|^k-1 is prime by A4,A8,A9,NUMBER07:59;
then k = 2 by Th22;
hence n > 4 implies contradiction by A7;
end;
n = 0 or ... or n = 19 by A1,A3,Lm25;
then per cases by A5;
suppose n = 3;
hence thesis by A4,Lm3,XPRIMES1:7;
end;
suppose n = 4;
hence thesis by A2,ENUMSET1:def 1;
end;
suppose n = 5;
hence thesis by A4,Lm5,XPRIMES1:31;
end;
suppose n = 2*3;
hence thesis by A6;
end;
suppose n = 7;
hence thesis by A4,Lm7,XPRIMES1:127;
end;
suppose n = 2*4;
hence thesis by A6;
end;
suppose n = 9;
hence thesis by A2,ENUMSET1:def 1;
end;
suppose n = 2*5;
hence thesis by A6;
end;
suppose n = 11;
hence thesis by A2,ENUMSET1:def 1;
end;
suppose n = 2*6;
hence thesis by A6;
end;
suppose n = 13;
hence thesis by A4,Lm11,XPRIMES2:8191;
end;
suppose n = 2*7;
hence thesis by A6;
end;
suppose
A10: n = 15;
2|^15-1 = 7*31*151 by Lm12;
hence thesis by A4,A10,XPRIMES1:7,31,151;
end;
suppose n = 2*8;
hence thesis by A6;
end;
suppose n = 17;
hence thesis by A4,Th24;
end;
suppose n = 2*9;
hence thesis by A6;
end;
suppose n = 19;
hence thesis by A4,Th25;
end;
end;
thus B c= A
proof
let x be object;
assume x in B;
then per cases by ENUMSET1:def 1;
suppose
A11: x = 2|^4-1;
2|^4-1 = 3*5 by Lm4;
hence thesis by A1,A11,XPRIMES1:3,5;
end;
suppose
A12: x = 2|^9-1;
2|^9-1 = 7*73 by Lm9;
hence thesis by A1,A12,XPRIMES1:7,73;
end;
suppose
A13: x = 2|^11-1;
2|^11-1 = 23*89 by Lm10;
hence thesis by A1,A13,XPRIMES1:23,89;
end;
end;
end;
definition
let n;
attr n is having_at_least_three_different_divisors means
ex q1,q2,q3 being Nat st q1,q2,q3 are_mutually_distinct &
q1 > 1 & q2 > 1 & q3 > 1 & q1 divides n & q2 divides n & q3 divides n;
end;
registration
cluster having_at_least_three_different_prime_divisors ->
having_at_least_three_different_divisors for Nat;
coherence
proof
let n;
given q1,q2,q3 being Prime such that
A1: q1,q2,q3 are_mutually_distinct &
q1 divides n & q2 divides n & q3 divides n;
q1 > 1 & q2 > 1 & q3 > 1 by INT_2:def 4;
hence thesis by A1;
end;
end;
registration
cluster having_at_least_three_different_prime_divisors
-> not_a_product_of_two_primes for Nat;
coherence;
end;
theorem
n is having_at_least_three_different_prime_divisors
implies not n is_a_product_of_two_different_primes;
:: Problem 91 b
theorem
n is even & n > 4 implies 2|^n-1 is having_at_least_three_different_divisors
proof
assume n is even;
then consider k such that
A1: n = 2*k;
assume that
A2: n > 4 and
A3: not 2|^n-1 is having_at_least_three_different_divisors;
reconsider k as non zero Nat by A1,A2;
A4: now
assume 2|^k-1 <= 1;
then 2|^k-1 = 0 or 2|^k-1 = 1 by NAT_1:25;
then 2|^k = 2|^1;
then k = 1 by PEPIN:30;
hence contradiction by A1,A2;
end;
2|^(2*k) = 2|^k|^2 by NEWTON:9
.= (2|^k)^2 by WSIERP_1:1;
then
A5: 2|^n-1 = (2|^k+1)*(2|^k-1) by A1;
then
A6: 2|^k-1 divides 2|^n-1;
A7: 2|^k+1 divides 2|^n-1 by A5;
A8: 2|^k-1 < 2|^k+1 by XREAL_1:8;
then
A9: 2|^k+1 > 1 by A4,XXREAL_0:2;
now
assume not 2|^k+1 is prime or not 2|^k-1 is prime;
then per cases;
suppose not 2|^k-1 is prime;
then consider a such that
A10: a divides 2|^k-1 and
A11: a <> 1 and
A12: a <> 2|^k-1 by A4;
A13: now
assume a <= 1;
then a = 0 or a = 1 by NAT_1:25;
hence contradiction by A10,A11;
end;
A14: a,2|^k-1,2|^k+1 are_mutually_distinct by A8,A10,A12,NAT_D:7;
a divides 2|^n-1 by A6,A10,INT_2:9;
hence contradiction by A3,A4,A6,A7,A9,A13,A14;
end;
suppose not 2|^k+1 is prime;
then consider a such that
A15: a divides 2|^k+1 and
A16: a <> 1 and
A17: a <> 2|^k+1 by A4,A8,XXREAL_0:2;
A18: now
assume a <= 1;
then a = 0 or a = 1 by NAT_1:25;
hence contradiction by A15,A16;
end;
now
assume a = 2|^k-1;
then 2|^k-1 divides (2|^k+1)-(2|^k-1) by A15,INT_5:1;
hence contradiction by A4,NUMBER07:9;
end;
then
A19: a,2|^k-1,2|^k+1 are_mutually_distinct by A17;
a divides 2|^n-1 by A7,A15,INT_2:9;
hence contradiction by A3,A4,A6,A7,A9,A18,A19;
end;
end;
then k = 2 by Th22;
hence contradiction by A1,A2;
end;
begin :: Problem 125
Lm28:
for a being even Nat st 1 < a <= 100 holds
a = 2 or a = 4 or a = 6 or a = 8 or a = 10 or a = 12 or a = 14 or a = 16 or
a = 18 or a = 20 or a = 22 or a = 24 or a = 26 or a = 28 or a = 30 or
a = 32 or a = 34 or a = 36 or a = 38 or a = 40 or a = 42 or a = 44 or
a = 46 or a = 48 or a = 50 or a = 52 or a = 54 or a = 56 or a = 58 or
a = 60 or a = 62 or a = 64 or a = 66 or a = 68 or a = 70 or a = 72 or
a = 74 or a = 76 or a = 78 or a = 80 or a = 82 or a = 84 or a = 86 or
a = 88 or a = 90 or a = 92 or a = 94 or a = 96 or a = 98 or a = 100
proof
let a be even Nat such that
A1: 1 < a;
assume a <= 100;
then
A2: a = 0 or ... or a = 100;
3 = 1*2+1 & 5 = 2*2+1 & 7 = 3*2+1 & 9 = 4*2+1 & 11 = 5*2+1 & 13 = 6*2+1 &
15 = 7*2+1 & 17 = 8*2+1 & 19 = 9*2+1 & 21 = 10*2+1 & 23 = 11*2+1 &
25 = 12*2+1 & 27 = 13*2+1 & 29 = 14*2+1 & 31 = 15*2+1 & 33 = 16*2+1 &
35 = 17*2+1 & 37 = 18*2+1 & 39 = 19*2+1 & 41 = 20*2+1 & 43 = 21*2+1 &
45 = 22*2+1 & 47 = 23*2+1 & 49 = 24*2+1 & 51 = 25*2+1 & 53 = 26*2+1 &
55 = 27*2+1 & 57 = 28*2+1 & 59 = 29*2+1 & 61 = 30*2+1 & 63 = 31*2+1 &
65 = 32*2+1 & 67 = 33*2+1 & 69 = 34*2+1 & 71 = 35*2+1 & 73 = 36*2+1 &
75 = 37*2+1 & 77 = 38*2+1 & 79 = 39*2+1 & 81 = 40*2+1 & 83 = 41*2+1 &
85 = 42*2+1 & 87 = 43*2+1 & 89 = 44*2+1 & 91 = 45*2+1 & 93 = 46*2+1 &
95 = 47*2+1 & 97 = 48*2+1 & 99 = 49*2+1;
hence thesis by A1,A2;
end;
theorem
Fermat m = Fermat n implies m = n
proof
assume Fermat m = Fermat n;
then 2 |^ m = 2 |^ n by PEPIN:30;
hence m = n by PEPIN:30;
end;
theorem Th30:
m < n implies Fermat m < Fermat n
proof
assume m < n;
then 2 |^ m < 2 |^ n by PEPIN:66;
then 2 |^ (2 |^ m) < 2 |^ (2 |^ n) by PEPIN:66;
hence thesis by XREAL_1:6;
end;
theorem
m <= n implies Fermat m <= Fermat n
proof
assume m <= n;
then m < n or m = n by XXREAL_0:1;
hence thesis by Th30;
end;
theorem Th32:
i,j are_congruent_mod j implies j divides i
proof
assume i,j are_congruent_mod j;
then consider k being Integer such that
A1: i = k * j + j by NAT_6:9;
i = j * (k+1) by A1;
hence j divides i;
end;
theorem Th33:
i*n,n are_congruent_mod n
proof
A1: i*n,0 are_congruent_mod n;
0,n are_congruent_mod n by INT_1:12;
hence thesis by A1,INT_1:15;
end;
Lm29:
17 divides 2|^(2|^2) + 1 by Lm2,Lm4;
Lm30:
17 divides 4|^(2|^1) + 1
proof
4|^2 = 4*4 by WSIERP_1:1;
hence thesis;
end;
Lm31:
17 divides 6|^(2|^3) + 1
proof
A1: 6|^8 = 6*6*6*6*6*6*6*6 by NUMBER02:4;
1679617 = 17*98801;
hence thesis by A1,Lm3;
end;
Lm32: 8|^4 = 8*8*8*8 by POLYEQ_5:3;
Lm33: 4097 = 17*241;
Lm34:
17 divides 8|^(2|^2) + 1 by Lm32,Lm33,Lm2;
Lm35:
17 divides 10|^(2|^3) + 1
proof
A1: 10|^8 = 10*10*10*10*10*10*10*10 by NUMBER02:4;
100000001 = 17*5882353;
hence thesis by A1,Lm3;
end;
Lm36:
17 divides 12|^(2|^3) + 1
proof
A1: 12|^8 = 12*12*12*12*12*12*12*12 by NUMBER02:4;
429981697 = 17*25293041;
hence thesis by A1,Lm3;
end;
Lm37:
17 divides 14|^(2|^3) + 1
proof
A1: 14|^8 = 14*14*14*14*14*14*14*14 by NUMBER02:4;
1475789057 = 17*86811121;
hence thesis by A1,Lm3;
end;
Lm38:
17 divides 20|^(2|^3) + 1
proof
A1: 20|^(2|^3) = 20|^2|^4 by Lm3,NEWTON:9;
A2: 20|^2 = 20*20 by WSIERP_1:1;
A3: 9|^4 = 9*9*9*9 by POLYEQ_5:3;
17+3,3 are_congruent_mod 17;
then 20*20,3*3 are_congruent_mod 17 by INT_1:18;
then 20|^2|^4,9|^4 are_congruent_mod 17 by A2,GR_CY_3:34;
then
A4: 20|^2|^4+1,9|^4+1 are_congruent_mod 17;
17*386,17 are_congruent_mod 17 by Th33;
hence thesis by A1,A3,A4,Th32,INT_1:15;
end;
Lm39:
17 divides 22|^(2|^3) + 1
proof
A1: 22|^2 = 22*22 by WSIERP_1:1;
17+5,5 are_congruent_mod 17;
then
A2: 22*22,5*5 are_congruent_mod 17 by INT_1:18;
1*17+8,8 are_congruent_mod 17;
then 22*22,8 are_congruent_mod 17 by A2,INT_1:15;
then 22|^2|^4,8|^4 are_congruent_mod 17 by A1,GR_CY_3:34;
then
A3: 22|^2|^4+1,8|^4+1 are_congruent_mod 17;
8|^4+1,0 are_congruent_mod 17 by Lm32,Lm33;
then 22|^2|^4+1,0 are_congruent_mod 17 by A3,INT_1:15;
hence thesis by Lm3,NEWTON:9;
end;
Lm40:
17 divides 24|^(2|^3) + 1
proof
A1: 24|^2 = 24*24 by WSIERP_1:1;
A2: 49|^4 = 49*49*49*49 by POLYEQ_5:3;
17+7,7 are_congruent_mod 17;
then 24*24,7*7 are_congruent_mod 17 by INT_1:18;
then 24|^2|^4,49|^4 are_congruent_mod 17 by A1,GR_CY_3:34;
then
A3: 24|^2|^4+1,49|^4+1 are_congruent_mod 17;
17*339106,0 are_congruent_mod 17;
then 24|^2|^4+1,0 are_congruent_mod 17 by A3,A2,INT_1:15;
hence thesis by Lm3,NEWTON:9;
end;
Lm41:
17 divides 26|^(2|^2) + 1
proof
A1: 26|^4 = 26*26*26*26 by POLYEQ_5:3;
456977 = 17*26881;
hence thesis by A1,Lm2;
end;
Lm42:
17 divides 28|^(2|^3) + 1
proof
A1: 28|^(2|^3) = 28|^2|^4 by Lm3,NEWTON:9;
A2: 28|^2 = 28*28 by WSIERP_1:1;
17+11,11 are_congruent_mod 17;
then
A3: 28*28,11*11 are_congruent_mod 17 by INT_1:18;
7*17+2,2 are_congruent_mod 17;
then 28*28,2 are_congruent_mod 17 by A3,INT_1:15;
then 28|^2|^4,2|^4 are_congruent_mod 17 by A2,GR_CY_3:34;
then 28|^2|^4+1,2|^4+1 are_congruent_mod 17;
hence thesis by A1,Lm4,Th32;
end;
Lm43:
17 divides 30|^(2|^1) + 1
proof
A1: 30|^2 = 30*30 by WSIERP_1:1;
901 = 17*53;
hence thesis by A1;
end;
Lm44:
17 divides 32|^(2|^2) + 1
proof
A1: 32|^4 = 32*32*32*32 by POLYEQ_5:3;
1048577 = 17*61681;
hence thesis by A1,Lm2;
end;
Lm45:
257 divides 84|^(2|^6) + 1
proof
A1: 84|^(2|^6) = 84|^2|^32 by Lm6,NEWTON:9;
A2: 84|^2 = 84*84 by WSIERP_1:1;
257*27+117,117 are_congruent_mod 257;
then
A3: 84|^2|^32,117|^32 are_congruent_mod 257 by A2,GR_CY_3:34;
A4: 117|^(2*16) = 117|^2|^16 by NEWTON:9;
A5: 117|^2 = 117*117 by WSIERP_1:1;
53*257+68,68 are_congruent_mod 257;
then 117|^2|^16,68|^16 are_congruent_mod 257 by A5,GR_CY_3:34;
then
A6: 84|^(2|^6),68|^16 are_congruent_mod 257 by A1,A3,A4,INT_1:15;
A7: 4|^4 = 4*4*4*4 by POLYEQ_5:3;
A8: 68|^4 = 68*68*68*68 by POLYEQ_5:3;
A9: 68|^(4*4) = 68|^4|^4 by NEWTON:9;
21381376 = 83196*257+4;
then 68|^4,4 are_congruent_mod 257 by A8;
then 68|^4|^4,4|^4 are_congruent_mod 257 by GR_CY_3:34;
then 84|^(2|^6),4|^4 are_congruent_mod 257 by A6,A9,INT_1:15;
then 84|^(2|^6)+1,256+1 are_congruent_mod 257 by A7;
hence thesis by Th32;
end;
theorem Th34:
a divides m|^k + 1 implies a divides (a*n+m)|^k + 1
proof
assume
A1: a divides m|^k + 1;
then
A2: a <> 0;
A3: (m|^k+1) mod a = 0 by A1;
(a*n+m) mod a = m mod a by NAT_D:21;
then ((a*n+m)|^k) mod a = (m|^k) mod a by INT_4:8;
then 0 = ((a*n+m)|^k mod a + (1 mod a)) mod a by A3,NAT_D:66
.= ((a*n+m)|^k + 1) mod a by NAT_D:66;
hence thesis by A2,INT_1:62;
end;
theorem Th35:
17 divides (34*k+2)|^(2|^2) + 1
proof
17 divides (17*(2*k)+2)|^(2|^2) + 1 by Th34,Lm29;
hence thesis;
end;
theorem Th36:
17 divides (34*k+4)|^(2|^1) + 1
proof
17 divides (17*(2*k)+4)|^(2|^1) + 1 by Th34,Lm30;
hence thesis;
end;
theorem Th37:
17 divides (34*k+6)|^(2|^3) + 1
proof
17 divides (17*(2*k)+6)|^(2|^3) + 1 by Th34,Lm31;
hence thesis;
end;
theorem Th38:
17 divides (34*k+8)|^(2|^2) + 1
proof
17 divides (17*(2*k)+8)|^(2|^2) + 1 by Th34,Lm34;
hence thesis;
end;
theorem Th39:
17 divides (34*k+10)|^(2|^3) + 1
proof
17 divides (17*(2*k)+10)|^(2|^3) + 1 by Th34,Lm35;
hence thesis;
end;
theorem Th40:
17 divides (34*k+12)|^(2|^3) + 1
proof
17 divides (17*(2*k)+12)|^(2|^3) + 1 by Th34,Lm36;
hence thesis;
end;
theorem Th41:
17 divides (34*k+14)|^(2|^3) + 1
proof
17 divides (17*(2*k)+14)|^(2|^3) + 1 by Th34,Lm37;
hence thesis;
end;
theorem Th42:
17 divides (34*k+20)|^(2|^3) + 1
proof
17 divides (17*(2*k)+20)|^(2|^3) + 1 by Th34,Lm38;
hence thesis;
end;
theorem Th43:
17 divides (34*k+22)|^(2|^3) + 1
proof
17 divides (17*(2*k)+22)|^(2|^3) + 1 by Th34,Lm39;
hence thesis;
end;
theorem Th44:
17 divides (34*k+24)|^(2|^3) + 1
proof
17 divides (17*(2*k)+24)|^(2|^3) + 1 by Th34,Lm40;
hence thesis;
end;
theorem Th45:
17 divides (34*k+26)|^(2|^2) + 1
proof
17 divides (17*(2*k)+26)|^(2|^2) + 1 by Th34,Lm41;
hence thesis;
end;
theorem Th46:
17 divides (34*k+28)|^(2|^3) + 1
proof
17 divides (17*(2*k)+28)|^(2|^3) + 1 by Th34,Lm42;
hence thesis;
end;
theorem Th47:
17 divides (34*k+30)|^(2|^1) + 1
proof
17 divides (17*(2*k)+30)|^(2|^1) + 1 by Th34,Lm43;
hence thesis;
end;
theorem Th48:
17 divides (34*k+32)|^(2|^2) + 1
proof
17 divides (17*(2*k)+32)|^(2|^2) + 1 by Th34,Lm44;
hence thesis;
end;
Lm46:
2|^(2|^(4+1)) = 2|^(2|^4*2|^1) by NEWTON:8
.= 2|^(2|^4)|^2 by NEWTON:9
.= 2|^(2|^4)*2|^(2|^4) by WSIERP_1:1
.= (2*2)|^(2|^4) by NEWTON:7;
Lm47:
2|^(2|^(4+1)) = 4|^(2|^(3+1)) by Lm46
.= 4|^((2|^3)*(2|^1)) by NEWTON:8
.= 4|^(2|^3)|^(2|^1) by NEWTON:9
.= 4|^(2|^3)*4|^(2|^3) by WSIERP_1:1
.= (4*4)|^(2|^3) by NEWTON:7;
Lm48:
a > 4 & n > 0 implies a|^(2|^n) + 1 > 25
proof
A1: 5|^2 = 5*5 by WSIERP_1:1;
assume
A2: a > 4;
then
a >= 4+1 by NAT_1:13;
then
A3: a|^2 >= 5|^2 by NEWTON02:41;
A4: a >= 1 by A2,XXREAL_0:2;
assume n > 0;
then 2|^n >= 1+1 by Lm1,NAT_1:13,PEPIN:66;
then a|^(2|^n) >= a|^2 by A4,PREPOWER:93;
then a|^(2|^n) >= 25 by A1,A3,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
Lm49:
a > 4 & n > 0 implies a|^(2|^n) + 1 > 17
proof
assume a > 4 & n > 0;
then a|^(2|^n) + 1 > 25 by Lm48;
hence thesis by XXREAL_0:2;
end;
Lm50: 256|^4 = 256*256*256*256 by POLYEQ_5:3;
Lm51: Fermat 5 = 2|^(4*8) + 1 by Lm5
.= 256|^4+1 by Lm8,NEWTON:9;
:: Problem 125
theorem
1 < a <= 100 implies
ex n being positive Nat st n <= 6 & a|^(2|^n) + 1 is composite
proof
assume that
A1: 1 < a and
A2: a <= 100;
deffunc G(Nat) = a|^(2|^$1);
deffunc F(Nat) = G($1) + 1;
per cases by A1,A2,Lm28;
suppose
A3: a is odd;
take n = 1;
thus n <= 6;
0+1 <= G(n) by A1,NAT_1:13;
then 1+1 <= F(n) by XREAL_1:6;
hence 2 <= F(n);
A4: F(n) is even by A3;
a|^2 = a*a by WSIERP_1:1;
then F(n) <> 2 by A1,NAT_1:15;
hence F(n) is non prime by A4;
end;
suppose
A5: a = 2;
take n = 5;
thus n <= 6;
thus 2 <= F(n) by A5,Lm51,Lm50;
thus F(n) is non prime by A5,NAT_6:44;
end;
suppose
A6: a = 4;
take n = 4;
thus n <= 6;
thus 2 <= F(n) by A6,Lm46,Lm51,Lm50;
thus F(n) is non prime by A6,Lm46,NAT_6:44;
end;
suppose
A7: a = 6;
take n = 3;
thus n <= 6;
A8: 17 < F(n) by A7,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+6)|^(2|^3)+1 by Th37;
hence thesis by A7,A8;
end;
suppose
A9: a = 8;
take n = 2;
thus n <= 6;
A10: 17 < F(n) by A9,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+8)|^(2|^2)+1 by Th38;
hence thesis by A9,A10;
end;
suppose
A11: a = 10;
take n = 3;
thus n <= 6;
A12: 17 < F(n) by A11,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+10)|^(2|^3)+1 by Th39;
hence thesis by A11,A12;
end;
suppose
A13: a = 12;
take n = 3;
thus n <= 6;
A14: 17 < F(n) by A13,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+12)|^(2|^3)+1 by Th40;
hence thesis by A13,A14;
end;
suppose
A15: a = 14;
take n = 3;
thus n <= 6;
A16: 17 < F(n) by A15,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+14)|^(2|^3)+1 by Th41;
hence thesis by A15,A16;
end;
suppose
A17: a = 16;
take n = 3;
thus n <= 6;
thus 2 <= F(n) by A17,Lm51,Lm50,Lm47;
thus F(n) is non prime by A17,Lm47,NAT_6:44;
end;
suppose
A18: a = 18;
take n = 1;
thus n <= 6;
A19: G(n) = 18*18 by A18,WSIERP_1:1;
hence 2 <= F(n);
325 = 5*65;
then 5 divides 325;
hence F(n) is non prime by A19;
end;
suppose
A20: a = 20;
take n = 3;
thus n <= 6;
A21: 17 < F(n) by A20,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+20)|^(2|^3)+1 by Th42;
hence thesis by A20,A21;
end;
suppose
A22: a = 22;
take n = 3;
thus n <= 6;
A23: 17 < F(n) by A22,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+22)|^(2|^3)+1 by Th43;
hence thesis by A22,A23;
end;
suppose
A24: a = 24;
take n = 3;
thus n <= 6;
A25: 17 < F(n) by A24,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+24)|^(2|^3)+1 by Th44;
hence thesis by A24,A25;
end;
suppose
A26: a = 26;
take n = 2;
thus n <= 6;
A27: 17 < F(n) by A26,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+26)|^(2|^2)+1 by Th45;
hence thesis by A26,A27;
end;
suppose
A28: a = 28;
take n = 3;
thus n <= 6;
A29: 17 < F(n) by A28,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+28)|^(2|^3)+1 by Th46;
hence thesis by A28,A29;
end;
suppose
A30: a = 30;
take n = 1;
thus n <= 6;
A31: 17 < F(n) by A30,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+30)|^(2|^1)+1 by Th47;
hence thesis by A30,A31;
end;
suppose
A32: a = 32;
take n = 2;
thus n <= 6;
A33: 17 < F(n) by A32,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*0+32)|^(2|^2)+1 by Th48;
hence thesis by A32,A33;
end;
suppose
A34: a = 34;
take n = 1;
thus n <= 6;
A35: G(n) = 34*34 by A34,WSIERP_1:1;
hence 2 <= F(n);
1157 = 13*89;
then 13 divides 1157;
hence F(n) is non prime by A35;
end;
suppose
A36: a = 36;
take n = 2;
thus n <= 6;
A37: 17 < F(n) by A36,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+2)|^(2|^2)+1 by Th35;
hence thesis by A36,A37;
end;
suppose
A38: a = 38;
take n = 1;
thus n <= 6;
A39: 17 < F(n) by A38,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+4)|^(2|^1)+1 by Th36;
hence thesis by A38,A39;
end;
suppose
A40: a = 40;
take n = 3;
thus n <= 6;
A41: 17 < F(n) by A40,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+6)|^(2|^3)+1 by Th37;
hence thesis by A40,A41;
end;
suppose
A42: a = 42;
take n = 2;
thus n <= 6;
A43: 17 < F(n) by A42,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+8)|^(2|^2)+1 by Th38;
hence thesis by A42,A43;
end;
suppose
A44: a = 44;
take n = 3;
thus n <= 6;
A45: 17 < F(n) by A44,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+10)|^(2|^3)+1 by Th39;
hence thesis by A44,A45;
end;
suppose
A46: a = 46;
take n = 3;
thus n <= 6;
A47: 17 < F(n) by A46,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+12)|^(2|^3)+1 by Th40;
hence thesis by A46,A47;
end;
suppose
A48: a = 48;
take n = 3;
thus n <= 6;
A49: 17 < F(n) by A48,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+14)|^(2|^3)+1 by Th41;
hence thesis by A48,A49;
end;
suppose
A50: a = 50;
take n = 1;
thus n <= 6;
A51: G(n) = 50*50 by A50,WSIERP_1:1;
hence 2 <= F(n);
2501 = 41*61;
then 41 divides 2501;
hence F(n) is non prime by A51;
end;
suppose
A52: a = 52;
take n = 1;
thus n <= 6;
A53: G(n) = 52*52 by A52,WSIERP_1:1;
hence 2 <= F(n);
2705 = 5*541;
then 5 divides 2705;
hence F(n) is non prime by A53;
end;
suppose
A54: a = 54;
take n = 3;
thus n <= 6;
A55: 17 < F(n) by A54,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+20)|^(2|^3)+1 by Th42;
hence thesis by A54,A55;
end;
suppose
A56: a = 56;
take n = 3;
thus n <= 6;
A57: 17 < F(n) by A56,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+22)|^(2|^3)+1 by Th43;
hence thesis by A56,A57;
end;
suppose
A58: a = 58;
take n = 3;
thus n <= 6;
A59: 17 < F(n) by A58,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+24)|^(2|^3)+1 by Th44;
hence thesis by A58,A59;
end;
suppose
A60: a = 60;
take n = 2;
thus n <= 6;
A61: 17 < F(n) by A60,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+26)|^(2|^2)+1 by Th45;
hence thesis by A60,A61;
end;
suppose
A62: a = 62;
take n = 3;
thus n <= 6;
A63: 17 < F(n) by A62,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+28)|^(2|^3)+1 by Th46;
hence thesis by A62,A63;
end;
suppose
A64: a = 64;
take n = 1;
thus n <= 6;
A65: 17 < F(n) by A64,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+30)|^(2|^1)+1 by Th47;
hence thesis by A64,A65;
end;
suppose
A66: a = 66;
take n = 2;
thus n <= 6;
A67: 17 < F(n) by A66,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*1+32)|^(2|^2)+1 by Th48;
hence thesis by A66,A67;
end;
suppose
A68: a = 68;
take n = 1;
thus n <= 6;
A69: G(n) = 68*68 by A68,WSIERP_1:1;
hence 2 <= F(n);
4625 = 5*925;
then 5 divides 4625;
hence F(n) is non prime by A69;
end;
suppose
A70: a = 70;
take n = 2;
thus n <= 6;
A71: 17 < F(n) by A70,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+2)|^(2|^2)+1 by Th35;
hence thesis by A70,A71;
end;
suppose
A72: a = 72;
take n = 1;
thus n <= 6;
A73: 17 < F(n) by A72,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+4)|^(2|^1)+1 by Th36;
hence thesis by A72,A73;
end;
suppose
A74: a = 74;
take n = 3;
thus n <= 6;
A75: 17 < F(n) by A74,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+6)|^(2|^3)+1 by Th37;
hence thesis by A74,A75;
end;
suppose
A76: a = 76;
take n = 2;
thus n <= 6;
A77: 17 < F(n) by A76,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+8)|^(2|^2)+1 by Th38;
hence thesis by A76,A77;
end;
suppose
A78: a = 78;
take n = 3;
thus n <= 6;
A79: 17 < F(n) by A78,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+10)|^(2|^3)+1 by Th39;
hence thesis by A78,A79;
end;
suppose
A80: a = 80;
take n = 3;
thus n <= 6;
A81: 17 < F(n) by A80,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+12)|^(2|^3)+1 by Th40;
hence thesis by A80,A81;
end;
suppose
A82: a = 82;
take n = 3;
thus n <= 6;
A83: 17 < F(n) by A82,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+14)|^(2|^3)+1 by Th41;
hence thesis by A82,A83;
end;
suppose
A84: a = 84;
take n = 6;
thus n <= 6;
A85: 84|^(2|^6) = 84|^2|^32 by Lm6,NEWTON:9;
A86: 84|^2 = 84*84 by WSIERP_1:1;
then 84|^2|^1 < 84|^2|^32 by PEPIN:66;
then 256 < 84|^(2|^6) by A85,A86,XXREAL_0:2;
then
A87: 256+1 < F(n) by A84,XREAL_1:8;
hence 2 <= F(n) by XXREAL_0:2;
thus thesis by A87,A84,Lm45;
end;
suppose
A88: a = 86;
take n = 1;
thus n <= 6;
A89: G(n) = 86*86 by A88,WSIERP_1:1;
hence 2 <= F(n);
7397 = 13*569;
then 13 divides 7397;
hence F(n) is non prime by A89;
end;
suppose
A90: a = 88;
take n = 3;
thus n <= 6;
A91: 17 < F(n) by A90,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+20)|^(2|^3)+1 by Th42;
hence thesis by A90,A91;
end;
suppose
A92: a = 90;
take n = 3;
thus n <= 6;
A93: 17 < F(n) by A92,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+22)|^(2|^3)+1 by Th43;
hence thesis by A92,A93;
end;
suppose
A94: a = 92;
take n = 3;
thus n <= 6;
A95: 17 < F(n) by A94,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+24)|^(2|^3)+1 by Th44;
hence thesis by A94,A95;
end;
suppose
A96: a = 94;
take n = 2;
thus n <= 6;
A97: 17 < F(n) by A96,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+26)|^(2|^2)+1 by Th45;
hence thesis by A96,A97;
end;
suppose
A98: a = 96;
take n = 3;
thus n <= 6;
A99: 17 < F(n) by A98,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+28)|^(2|^3)+1 by Th46;
hence thesis by A98,A99;
end;
suppose
A100: a = 98;
take n = 1;
thus n <= 6;
A101: 17 < F(n) by A100,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+30)|^(2|^1)+1 by Th47;
hence thesis by A100,A101;
end;
suppose
A102: a = 100;
take n = 2;
thus n <= 6;
A103: 17 < F(n) by A102,Lm49;
hence 2 <= F(n) by XXREAL_0:2;
17 divides (34*2+32)|^(2|^2)+1 by Th48;
hence thesis by A102,A103;
end;
end;
begin :: Problem 143
Lm52:
for D being Integer st D > 0 holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 } is infinite
proof
let D be Integer such that
A1: D > 0;
set A = { [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 };
deffunc m(Nat) = D*$1+1;
deffunc x(Nat,Real) = $2^2+D*$1^2;
deffunc y(Nat,Real) = 2*$2*$1;
deffunc z(Nat,Real) = $2^2-D*$1^2;
deffunc F(Element of NATPLUS) = [x($1,m($1)),y($1,m($1)),z($1,m($1))];
consider f being ManySortedSet of NATPLUS such that
A2: for d being Element of NATPLUS holds f.d = F(d) from PBOOLE:sch 5;
A3: dom f = NATPLUS 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 NATPLUS by A5,PARTFUN1:def 2;
A7: x(k,m(k)) is positive Element of NAT by A1,INT_1:3;
A8: y(k,m(k)) is positive Element of NAT by A1,INT_1:3;
D >= 0+1 by A1,INT_1:7;
then D*(D*k^2) >= 1*(D*k^2) by XREAL_1:64;
then k*(D*k)*D + (k*D + (D*k+1)) > D*k^2 + 0 by A1,XREAL_1:8;
then m(k)^2-D*k^2 > D*k^2-D*k^2 by XREAL_1:9;
then
A9: z(k,m(k)) is positive Element of NAT by INT_1:3;
x(k,m(k))^2-D*y(k,m(k))^2 = z(k,m(k))^2;
then F(k) in A by A7,A8,A9;
hence thesis by A2,A6;
end;
f is one-to-one
proof
let x1,x2 be object such that
A10: x1 in dom f & x2 in dom f and
A11: f.x1 = f.x2;
reconsider x1,x2 as Element of NATPLUS by A10,PARTFUN1:def 2;
A12: D*x1/D = x1 & D*x2/D = x2 by A1,XCMPLX_1:203;
f.x1 = F(x1) & f.x2 = F(x2) by A2;
then x(x1,m(x1)) = x(x2,m(x2)) & z(x1,m(x1)) = z(x2,m(x2))
by A11,XTUPLE_0:3;
then m(x1) = m(x2) or m(x1) = -m(x2) by SQUARE_1:40;
hence thesis by A1,A12;
end;
hence thesis by A3,A4,CARD_1:59;
end;
Lm53:
for D being Integer st D < 0 holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 } is infinite
proof
let D be Integer such that
A1: D < 0;
set A = { [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 };
deffunc m(Nat) = -D*$1^2+1;
deffunc x(Nat,Real) = $2^2+D*$1^2;
deffunc y(Nat,Real) = 2*$2*$1;
deffunc z(Nat,Real) = $2^2-D*$1^2;
deffunc F(Element of NATPLUS) = [x($1,m($1)),y($1,m($1)),z($1,m($1))];
consider f being ManySortedSet of NATPLUS such that
A2: for d being Element of NATPLUS holds f.d = F(d) from PBOOLE:sch 5;
A3: dom f = NATPLUS 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 NATPLUS by A5,PARTFUN1:def 2;
now
assume m(k)^2+D*k^2 <= 0;
then 1-D*k^2+(D*k^2)*(D*k^2) <= 0;
hence contradiction by A1;
end;
then
A7: x(k,m(k)) is positive Element of NAT by INT_1:3;
A8: y(k,m(k)) is positive Element of NAT by A1,INT_1:3;
A9: z(k,m(k)) is positive Element of NAT by A1,INT_1:3;
x(k,m(k))^2-D*y(k,m(k))^2 = z(k,m(k))^2;
then F(k) in A by A7,A8,A9;
hence thesis by A2,A6;
end;
f is one-to-one
proof
let x1,x2 be object such that
A10: x1 in dom f & x2 in dom f and
A11: f.x1 = f.x2;
reconsider x1,x2 as Element of NATPLUS by A10,PARTFUN1:def 2;
A12: D*(x1^2)/D = x1^2 & D*(x2^2)/D = x2^2 by A1,XCMPLX_1:203;
f.x1 = F(x1) & f.x2 = F(x2) by A2;
then x(x1,m(x1)) = x(x2,m(x2)) & z(x1,m(x1)) = z(x2,m(x2))
by A11,XTUPLE_0:3;
then x1 = x2 or x1 = -x2 by A12,SQUARE_1:40;
hence thesis;
end;
hence thesis by A3,A4,CARD_1:59;
end;
Lm54:
{ [x,y,z] where x,y,z is positive Nat : x^2-0*y^2 = z^2 } is infinite
proof
set D = 0;
set A = { [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 };
deffunc m(Nat) = $1;
deffunc x(Real) = $1^2;
deffunc y(Nat) = $1;
deffunc z(Real) = $1^2;
deffunc F(Element of NATPLUS) = [x(m($1)),y($1),z(m($1))];
consider f being ManySortedSet of NATPLUS such that
A1: for d being Element of NATPLUS holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = NATPLUS by PARTFUN1:def 2;
A3: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A4: k in dom f and
A5: f.k = y by FUNCT_1:def 3;
reconsider k as Element of NATPLUS by A4,PARTFUN1:def 2;
x(m(k))^2-D*y(k)^2 = z(m(k))^2;
then F(k) in A;
hence thesis by A1,A5;
end;
f is one-to-one
proof
let x1,x2 be object such that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
reconsider x1,x2 as Element of NATPLUS by A6,PARTFUN1:def 2;
f.x1 = F(x1) & f.x2 = F(x2) by A1;
hence thesis by A7,XTUPLE_0:3;
end;
hence thesis by A2,A3,CARD_1:59;
end;
:: Problem 143
theorem
for D being Integer holds
{ [x,y,z] where x,y,z is positive Nat : x^2-D*y^2 = z^2 } is infinite
proof
let D be Integer;
D < 0 or D = 0 or D > 0;
hence thesis by Lm52,Lm53,Lm54;
end;
begin :: Problem 146
theorem Th51:
n^2 mod 8 = 0 or n^2 mod 8 = 1 or n^2 mod 8 = 4
proof
consider k such that
A1: n = 8*k or n = 8*k+1 or n = 8*k+2 or n = 8*k+3 or
n = 8*k+4 or n = 8*k+5 or n = 8*k+6 or n = 8*k+7 by NUMBER02:28;
set a = n mod 8;
A2: n^2 mod 8 = (a*a) mod 8 by NAT_D:67;
per cases by A1;
suppose n = 8*k+0;
hence thesis by A2;
end;
suppose n = 8*k+1;
then a = 1 mod 8 by NAT_D:61
.= 1 by NAT_D:24;
hence thesis by A2;
end;
suppose n = 8*k+2;
then a = 2 mod 8 by NAT_D:61
.= 2 by NAT_D:24;
hence thesis by A2,NAT_D:24;
end;
suppose n = 8*k+3;
then
A3: a = 3 mod 8 by NAT_D:61
.= 3 by NAT_D:24;
(1+1*8) mod 8 = 1 mod 8 by NAT_D:61;
hence thesis by A2,A3,NAT_D:24;
end;
suppose n = 8*k+4;
then
A4: a = 4 mod 8 by NAT_D:61
.= 4 by NAT_D:24;
(0+2*8) mod 8 = 0 mod 8;
hence thesis by A2,A4;
end;
suppose n = 8*k+5;
then
A5: a = 5 mod 8 by NAT_D:61
.= 5 by NAT_D:24;
(1+3*8) mod 8 = 1 mod 8 by NAT_D:61;
hence thesis by A2,A5,NAT_D:24;
end;
suppose n = 8*k+6;
then
A6: a = 6 mod 8 by NAT_D:61
.= 6 by NAT_D:24;
(4+4*8) mod 8 = 4 mod 8 by NAT_D:61;
hence thesis by A2,A6,NAT_D:24;
end;
suppose n = 8*k+7;
then
A7: a = 7 mod 8 by NAT_D:61
.= 7 by NAT_D:24;
(1+6*8) mod 8 = 1 mod 8 by NAT_D:61;
hence thesis by A2,A7,NAT_D:24;
end;
end;
:: Problem 146
theorem
for x,y,z being Nat holds x^2 - 2*y^2 + 8*z <> 3
proof
let x,y,z be Nat;
assume
A1: x^2 - 2*y^2 + 8*z = 3;
per cases;
suppose y is even;
then consider k such that
A2: y = 2*k;
A3: x^2 - 2*(2*k)*(2*k) + 8*z = 3 by A1,A2;
(8*(k^2-z) + 3) mod 8 = 3 mod 8 by NAT_D:61
.= 3 by NAT_D:24;
hence thesis by A3,Th51;
end;
suppose y is odd;
then consider k such that
A4: y = 2*k+1 by ABIAN:9;
A5: x^2 - 2*(2*k+1)*(2*k+1) + 8*z = 3 by A1,A4;
(8*(k^2+k-z) + 5) mod 8 = 5 mod 8 by NAT_D:61
.= 5 by NAT_D:24;
hence thesis by A5,Th51;
end;
end;
begin :: Problem 147
:: Problem 147
theorem
{ [x,y] where x,y is Nat: y^2-x*(x+1)*(x+2)*(x+3) = 1 }
= { [x,y] where x,y is Nat: y = x^2+3*x+1 }
proof
set A = { [x,y] where x,y is Nat: y^2-x*(x+1)*(x+2)*(x+3) = 1 };
set B = { [x,y] where x,y is Nat: y = x^2+3*x+1 };
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y being Nat such that
A1: a = [x,y] and
A2: y^2-x*(x+1)*(x+2)*(x+3) = 1;
x*(x+1)*(x+2)*(x+3)+1 = (x^2+3*x+1)^2;
then y = x^2+3*x+1 by A2,PYTHTRIP:5;
hence a in B by A1;
end;
let a be object;
assume a in B;
then consider x,y being Nat such that
A3: a = [x,y] and
A4: y = x^2+3*x+1;
y^2-x*(x+1)*(x+2)*(x+3) = 1 by A4;
hence a in A by A3;
end;
begin :: Problem 158
theorem Th54:
for a,b,c,d being positive Real st a/b < 1 & c/d < 1 holds (a/b) * (c/d) < 1
proof
let a,b,c,d be positive Real;
assume a/b < 1;
then
A1: a < b by XREAL_1:181;
assume c/d < 1;
then c < d by XREAL_1:181;
then
A2: a*c < b*d by A1,XREAL_1:96;
(a/b) * (c/d) = (a*c) / (b*d) by XCMPLX_1:76;
hence (a/b) * (c/d) < 1 by A2,XREAL_1:189;
end;
:: Problem 158 a
theorem
for x,y,z,t being positive Nat holds x/y + y/z + z/t + t/x <> 1
proof
let x,y,z,t be positive Nat;
x/y >= 1 or y/z >= 1 or z/t >= 1 or t/x >= 1
proof
assume that
A1: x/y < 1 & y/z < 1 and
A2: z/t < 1 and
A3: t/x < 1;
A4: (x/y) * (y/z) = (x*y)/(y*z) by XCMPLX_1:76;
A5: ((x*y*z) / (y*z*t)) * (t/x) = (x*y*z*t) / (y*z*t*x) by XCMPLX_1:76
.= 1 by XCMPLX_1:60;
A6: (x/y) * (y/z) * (z/t) = (x*y*z)/(y*z*t) by A4,XCMPLX_1:76;
(x/y) * (y/z) < 1 by A1,Th54;
then (x/y) * (y/z) * (z/t) < 1 by A2,A4,Th54;
hence contradiction by A3,A5,A6,Th54;
end;
then per cases;
suppose x/y >= 1;
then x/y + (y/z + z/t + t/x) > 1+0 by XREAL_1:8;
hence thesis;
end;
suppose y/z >= 1;
then y/z + (x/y + z/t + t/x) > 1+0 by XREAL_1:8;
hence thesis;
end;
suppose z/t >= 1;
then z/t + (x/y + y/z + t/x) > 1+0 by XREAL_1:8;
hence thesis;
end;
suppose t/x >= 1;
then t/x + (x/y + y/z + z/t) > 1+0 by XREAL_1:8;
hence thesis;
end;
end;
definition
let n be Nat;
func GreaterOrEqualsNumbers(n) -> Subset of NAT equals
NAT \ Segm n;
coherence;
end;
registration
let n;
cluster GreaterOrEqualsNumbers(n) -> infinite;
coherence;
end;
theorem Th56:
k in GreaterOrEqualsNumbers(n) iff n <= k
proof
thus k in GreaterOrEqualsNumbers(n) implies n <= k
proof
assume k in GreaterOrEqualsNumbers(n);
then not k in Segm n by XBOOLE_0:def 5;
hence thesis by NAT_1:44;
end;
A1: k in NAT by ORDINAL1:def 12;
assume n <= k;
then not k in Segm n by NAT_1:44;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem
n+k in GreaterOrEqualsNumbers(n) by Th56,NAT_1:11;
theorem
n in GreaterOrEqualsNumbers(n) by Th56;
theorem
k > 0 implies not n in GreaterOrEqualsNumbers(n+k)
proof
assume k > 0;
then n+0 < n+k by XREAL_1:8;
hence thesis by Th56;
end;
registration
let n;
cluster -> n_or_greater for Element of GreaterOrEqualsNumbers(n);
coherence
proof
let k be Element of GreaterOrEqualsNumbers(n);
thus n <= k by Th56;
end;
end;
registration
let n;
cluster n_or_greater for Nat;
existence
proof
take n;
thus n <= n;
end;
end;
theorem
for k being n_or_greater Nat holds k in GreaterOrEqualsNumbers(n)
by EC_PF_2:def 1,Th56;
registration
let n;
let k be non zero Nat;
cluster k*n -> n_or_greater;
coherence
proof
1*n <= k*n by NAT_1:4,INT_1:74;
hence n <= k*n;
end;
end;
registration
let n;
let k be n_or_greater Nat;
cluster k-n -> natural;
coherence
proof
k-n in NAT by INT_1:5,EC_PF_2:def 1;
hence thesis;
end;
end;
:: Problem 158 b
theorem
{ [x,y,z,t] where x,y,z,t is Integer: x/y + y/z + z/t + t/x = 1 } is infinite
proof
set G2 = GreaterOrEqualsNumbers(2);
set A = { [x,y,z,t] where x,y,z,t is Integer: x/y + y/z + z/t + t/x = 1 };
deffunc x(Nat) = -$1^2;
deffunc y(Nat) = $1^2*($1^2-1);
deffunc z(Nat) = ($1^2-1)^2;
deffunc t(Nat) = -$1*($1^2-1);
deffunc F(Element of G2) = [x($1),y($1),z($1),t($1)];
consider f being ManySortedSet of G2 such that
A1: for d being Element of G2 holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = G2 by PARTFUN1:def 2;
A3: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A4: k in dom f and
A5: f.k = y by FUNCT_1:def 3;
reconsider k as Element of G2 by A4,PARTFUN1:def 2;
set q = k^2-1;
A6: x(k)/y(k) = ((-1)*k^2) / ((k^2-1)*k^2)
.= (-1)/q by XCMPLX_1:91;
A7: z(k)/t(k) = q^2 / ((-k)*q)
.= q/-k by XCMPLX_1:91
.= -q/k by XCMPLX_1:188;
A8: t(k)/x(k) = (k*q)/k^2 by XCMPLX_1:191
.= q/k by XCMPLX_1:91;
k^2/q - 1/q = q/q
.= 1 by XCMPLX_1:60;
then x(k)/y(k) + y(k)/z(k) + z(k)/t(k) + t(k)/x(k) = 1
by A6,A7,A8,XCMPLX_1:91;
then F(k) in A;
hence thesis by A1,A5;
end;
f is one-to-one
proof
let x1,x2 be object such that
A9: x1 in dom f & x2 in dom f and
A10: f.x1 = f.x2;
reconsider x1,x2 as Element of G2 by A9,PARTFUN1:def 2;
f.x1 = F(x1) & f.x2 = F(x2) by A1;
then x(x1) = x(x2) by A10,XTUPLE_0:5;
then x1 = x2 or x1 = -x2 by SQUARE_1:40;
hence thesis;
end;
hence thesis by A2,A3,CARD_1:59;
end;
begin :: Problem 166
:: Problem 166
theorem
1/2 = 1/2^2 + 1/3^2 + 1/4^2 + 1/6^2 + 1/7^2 + 1/9^2 + 1/12^2 + 1/14^2 +
1/21^2 + 1/36^2 + 1/45^2 + 1/60^2;
begin :: Problem 178
:: Problem 178
theorem
(n+1)|^3 + (n+2)|^3 + (n+3)|^3 + (n+4)|^3 <> (n+5)|^3
proof
assume
A1: (n+1)|^3 + (n+2)|^3 + (n+3)|^3 + (n+4)|^3 = (n+5)|^3;
(n+1)|^3 = (n+1)*(n+1)*(n+1) & (n+2)|^3 = (n+2)*(n+2)*(n+2) &
(n+3)|^3 = (n+3)*(n+3)*(n+3) & (n+4)|^3 = (n+4)*(n+4)*(n+4) &
(n+5)|^3 = (n+5)*(n+5)*(n+5) by POLYEQ_5:2;
then
A2: 3*(n*n*n+5*n*n+5*n) = 25 by A1;
not 3 divides 3*8+1 by NAT_4:9;
hence thesis by A2;
end;
begin :: Problem 180
:: Problem 180
theorem
2*(2+1) = 1*(1+1)*(1+2) & 14*(14+1) = 5*(5+1)*(5+2);
begin :: Problem 181
:: Problem 181
theorem
{ [x,y,z] where x,y,z is positive Nat : 1+x^2+y^2 = z^2 } is infinite
proof
set A = { [x,y,z] where x,y,z is positive Nat : 1+x^2+y^2 = z^2 };
deffunc x(Nat) = 2*$1;
deffunc y(Nat) = 2*$1^2;
deffunc z(Nat) = 2*$1^2+1;
deffunc F(Nat) = [x($1),y($1),z($1)];
consider f being ManySortedSet of NATPLUS such that
A1: for d being Element of NATPLUS holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = NATPLUS by PARTFUN1:def 2;
A3: rng f c= A
proof
let y be object;
assume y in rng f;
then consider k being object such that
A4: k in dom f and
A5: f.k = y by FUNCT_1:def 3;
reconsider k as Element of NATPLUS by A4,PARTFUN1:def 2;
A6: 1+x(k)^2+y(k)^2 = z(k)^2;
F(k) = f.k by A1;
hence thesis by A5,A6;
end;
f is one-to-one
proof
let x1,x2 be object such that
A7: x1 in dom f & x2 in dom f and
A8: f.x1 = f.x2;
reconsider x1,x2 as Element of NATPLUS by A7,PARTFUN1:def 2;
F(x1) = f.x1 & F(x2) = f.x2 by A1;
then x(x1) = x(x2) by A8,XTUPLE_0:3;
hence thesis;
end;
hence thesis by A2,A3,CARD_1:59;
end;