:: Elementary Number Theory Problems. {P}art {VIII}
:: by Artur Korni{\l}owicz
::
:: Received June 30, 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, VALUED_0,
CARD_3, REALSET1, FINSEQ_1, ORDINAL1, PBOOLE, FUNCOP_1, PRE_POLY,
FUNCT_4, NAT_3, UPROOTS, SQUARE_1, VALUED_1, PARTFUN1, ORDINAL4,
ORDINAL2, PARTFUN3, PYTHTRIP, RFINSEQ2, CLASSES1, COMPLEX1, NAT_LAT,
RAT_1, MCART_1, XREAL_0, POWER, PREPOWER, NUMBER08;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, XTUPLE_0, DOMAIN_1,
ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, PBOOLE,
FINSET_1, MEMBERED, VALUED_0, VALUED_1, CLASSES1, XREAL_0, RAT_1, INT_1,
INT_2, NAT_1, XXREAL_0, XXREAL_2, SQUARE_1, FUNCOP_1, FINSEQ_1, FUNCT_4,
PARTFUN3, PYTHTRIP, RVSUM_1, RFINSEQ2, NEWTON, PREPOWER, POWER, ABIAN,
EULER_1, NAT_LAT, PRE_POLY, NAT_3, MOEBIUS1;
constructors NAT_D, RELSET_1, ABIAN, EULER_1, PEPIN, FIB_NUM2, XXREAL_2,
NAT_3, RVSUM_1, CLASSES1, NAT_LAT, PYTHTRIP, FUNCT_4, MOEBIUS1, RFINSEQ2,
PARTFUN3, NEWTON03, PREPOWER, POWER, DOMAIN_1;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, CARD_1, NEWTON, NEWTON02,
NEWTON03, ABIAN, NAT_6, JORDAN1D, WSIERP_1, XXREAL_2, NEWTON01, FINSEQ_1,
RVSUM_1, PRE_POLY, FUNCT_1, RELAT_1, XBOOLE_0, NAT_3, FUNCT_4, FUNCOP_1,
SUBSET_1, NUMBER02, PYTHTRIP, PBOOLE, VALUED_1, PARTFUN3, FINSEQ_9,
NAT_LAT, RAMSEY_1, XTUPLE_0, RAT_1, SQUARE_1, POWER;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, RELAT_1, TARSKI, FUNCT_1, PARTFUN1, PBOOLE, PYTHTRIP,
INT_2, VALUED_0, PRE_POLY, SEQM_3, PARTFUN3;
equalities SQUARE_1, FINSEQ_1, FUNCOP_1, MOEBIUS1, XCMPLX_0;
expansions INT_1, INT_2, ABIAN, TARSKI, ZFMISC_1, NAT_D;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, WSIERP_1, ORDINAL1, EULER_2,
XREAL_1, XXREAL_0, NAT_1, MOEBIUS1, INT_6, NAT_3, FUNCT_1, PARTFUN1,
NAT_6, TARSKI, POLYEQ_5, NAT_5, EULER_1, ENUMSET1, CARD_1, ABIAN,
XXREAL_2, XTUPLE_0, GR_CY_3, GROUPP_1, FINSEQ_1, RVSUM_1, FINSEQ_3,
XCMPLX_0, FUNCOP_1, FINSEQ_2, INT_8, PRE_POLY, FUNCT_4, GLIB_004,
XBOOLE_0, XREAL_0, XBOOLE_1, RELAT_1, XPRIMES0, XPRIMES1, NUMBER02,
NUMBER03, NUMBER04, XCMPLX_1, INT_5, NEWTON02, PREPOWER, NUMBER05,
NEWTON03, VALUED_1, FINSEQ_5, NEWTON04, PARTFUN3, VALUED_0, FILEREC1,
FUNCT_2, RFINSEQ2, CONVEX2, MOEBIUS2, NAT_LAT, GROUP_22, CLASSES1,
XPRIMET1, MCART_1, ZFMISC_1, RAT_1, POWER, NAT_2;
schemes NAT_1, PBOOLE, FUNCT_1, CLASSES1, RECDEF_1;
begin :: Preliminaries
Lm1: 2|^0 = 1 by NEWTON:4;
Lm2: 2|^1 = 2;
Lm3: 2|^2 = 2*2 by NEWTON:81;
Lm4: 2|^3 = 2*2*2 by POLYEQ_5:2;
Lm5: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
Lm6: 2|^5 = 2*2*2*2*2 by NUMBER02:1;
Lm7: 2|^7 = 2*2*2*2*2*2*2 by NUMBER02:3;
Lm8: 3|^2 = 3*3 by NEWTON:81;
Lm9: 3|^3 = 3*3*3 by POLYEQ_5:2;
Lm10: 3|^4 = 3*3*3*3 by POLYEQ_5:3;
Lm11: 11|^2 = 11*11 by NEWTON:81;
Lm12: 2|^3 = 2*2*2 by POLYEQ_5:2;
Lm13: 3,3 are_congruent_mod 4 by INT_1:11;
Lm14: 3,3 are_congruent_mod 8 by INT_1:11;
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;
registration
let n,r;
cluster n-r+r -> natural;
coherence;
cluster n+r-r -> natural;
coherence;
end;
theorem Th1:
for x,y being Nat st x < y < x+2 holds y = x+1
proof
let x,y be Nat;
assume x < y;
then
A1: x+1 <= y by NAT_1:13;
assume y < x+2;
then y < x+1+1;
then y <= x+1 by NAT_1:13;
hence y = x+1 by A1,XXREAL_0:1;
end;
theorem Th2:
NATPLUS = NAT \ {0}
proof
A1: NATPLUS c= NAT \ {0}
proof
let x be object;
assume
A2: x in NATPLUS;
then reconsider x as Element of NAT;
not x in {0} by A2,TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
NAT \ {0} c= NATPLUS
proof
let x be object;
assume
A3: x in NAT \ {0};
then reconsider x as Element of NAT;
not x in {0} by A3,XBOOLE_0:def 5;
then x <> 0 by TARSKI:def 1;
hence thesis by NAT_LAT:def 6;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
registration
cluster NATPLUS -> infinite;
coherence by Th2;
end;
theorem Th3:
for f,g being FinSequence holds
f^g is X-valued implies f is X-valued & g is X-valued
proof
let f,g be FinSequence;
set h = f^g;
assume h is X-valued;
then
A1: rng h c= X by RELAT_1:def 19;
rng f c= rng h & rng g c= rng h by FINSEQ_1:29,30;
then rng f c= X & rng g c= X by A1;
hence thesis by RELAT_1:def 19;
end;
theorem Th4:
for f1,f2,f3 being complex-valued ManySortedSet of X st
for x being object st x in X holds f1.x = f2.x * f3.x holds
f1 = f2(#)f3
proof
let f1,f2,f3 be complex-valued ManySortedSet of X such that
A1: for x being object st x in X holds f1.x = f2.x * f3.x;
A2: dom f1 = X & dom f2 = X & dom f3 = X by PARTFUN1:def 2;
dom(f2(#)f3) = dom f2 /\ dom f3 by VALUED_1:def 4;
hence thesis by A1,A2,VALUED_1:def 4;
end;
theorem
b <> 0 & c <> 0 implies (r*b+c) / b > r
proof
assume that
A1: b <> 0 and
A2: c <> 0;
A3: (r*b+c) / b = r*b/b + c/b
.= r + c/b by A1,XCMPLX_1:89;
r + c/b > r + 0 by A1,A2,XREAL_1:8;
hence thesis by A3;
end;
theorem Th6:
m <= n implies m! divides n!
proof
defpred P[Nat] means m <= $1 implies m! divides $1!;
A1: P[0];
A2: P[k] implies P[k+1]
proof
assume
A3: P[k];
assume m <= k+1;
then per cases by NAT_1:8;
suppose
A4: m <= k;
A5: (k+1)! = k!*(k+1) by NEWTON:15;
1 divides k+1 by INT_2:12;
then m!*1 divides (k+1)! by A3,A4,A5,NAT_3:1;
hence m! divides (k+1)!;
end;
suppose m = k+1;
hence m! divides (k+1)!;
end;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th7:
p1 divides p2 implies p1 = p2
proof
assume p1 divides p2;
then p1 = 1 or p1 = p2 by INT_2:def 4;
hence thesis by INT_2:def 4;
end;
theorem
m,n are_coprime implies a*n+m,n are_coprime
proof
a*n+m,m are_congruent_mod n;
hence thesis by WSIERP_1:43;
end;
theorem Th9:
n divides 9 implies n = 1 or n = 3 or n = 9
proof
assume
A1: n divides 9;
then n <= 9 by INT_2:27;
then
A2: n = 0 or ... or n = 9;
now
(2*4+1) mod 2 = 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24;
hence not 2 divides 9;
(4*2+1) mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24;
hence not 4 divides 9;
(5*1+4) mod 5 = 4 mod 5 by NAT_D:21
.= 4 by NAT_D:24;
hence not 5 divides 9;
(6*1+3) mod 6 = 3 mod 6 by NAT_D:21
.= 3 by NAT_D:24;
hence not 6 divides 9;
(7*1+2) mod 7 = 2 mod 7 by NAT_D:21
.= 2 by NAT_D:24;
hence not 7 divides 9;
(8*1+1) mod 8 = 1 mod 8 by NAT_D:21
.= 1 by NAT_D:24;
hence not 8 divides 9;
end;
hence thesis by A1,A2;
end;
theorem Th10:
n divides 25 implies n = 1 or n = 5 or n = 25
proof
assume
A1: n divides 25;
then n <= 25 by INT_2:27;
then
A2: n = 0 or ... or n = 25;
now
(2*12+1) mod 2 = 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24;
hence not 2 divides 25;
(3*8+1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24;
hence not 3 divides 25;
(4*6+1) mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24;
hence not 4 divides 25;
(6*4+1) mod 6 = 1 mod 6 by NAT_D:21
.= 1 by NAT_D:24;
hence not 6 divides 25;
(7*3+4) mod 7 = 4 mod 7 by NAT_D:21
.= 4 by NAT_D:24;
hence not 7 divides 25;
(8*3+1) mod 8 = 1 mod 8 by NAT_D:21
.= 1 by NAT_D:24;
hence not 8 divides 25;
(9*2+7) mod 9 = 7 mod 9 by NAT_D:21
.= 7 by NAT_D:24;
hence not 9 divides 25;
(10*2+5) mod 10 = 5 mod 10 by NAT_D:21
.= 5 by NAT_D:24;
hence not 10 divides 25;
(11*2+3) mod 11 = 3 mod 11 by NAT_D:21
.= 3 by NAT_D:24;
hence not 11 divides 25;
(12*2+1) mod 12 = 1 mod 12 by NAT_D:21
.= 1 by NAT_D:24;
hence not 12 divides 25;
(13*1+12) mod 13 = 12 mod 13 by NAT_D:21
.= 12 by NAT_D:24;
hence not 13 divides 25;
(14*1+11) mod 14 = 11 mod 14 by NAT_D:21
.= 11 by NAT_D:24;
hence not 14 divides 25;
(15*1+10) mod 15 = 10 mod 15 by NAT_D:21
.= 10 by NAT_D:24;
hence not 15 divides 25;
(16*1+9) mod 16 = 9 mod 16 by NAT_D:21
.= 9 by NAT_D:24;
hence not 16 divides 25;
(17*1+8) mod 17 = 8 mod 17 by NAT_D:21
.= 8 by NAT_D:24;
hence not 17 divides 25;
(18*1+7) mod 18 = 7 mod 18 by NAT_D:21
.= 7 by NAT_D:24;
hence not 18 divides 25;
(19*1+6) mod 19 = 6 mod 19 by NAT_D:21
.= 6 by NAT_D:24;
hence not 19 divides 25;
(20*1+5) mod 20 = 5 mod 20 by NAT_D:21
.= 5 by NAT_D:24;
hence not 20 divides 25;
(21*1+4) mod 21 = 4 mod 21 by NAT_D:21
.= 4 by NAT_D:24;
hence not 21 divides 25;
(22*1+3) mod 22 = 3 mod 22 by NAT_D:21
.= 3 by NAT_D:24;
hence not 22 divides 25;
(23*1+2) mod 23 = 2 mod 23 by NAT_D:21
.= 2 by NAT_D:24;
hence not 23 divides 25;
(24*1+1) mod 24 = 1 mod 24 by NAT_D:21
.= 1 by NAT_D:24;
hence not 24 divides 25;
end;
hence thesis by A1,A2;
end;
theorem Th11:
n divides 27 implies n = 1 or n = 3 or n = 9 or n = 27
proof
assume
A1: n divides 27;
then n <= 27 by INT_2:27;
then
A2: n = 0 or ... or n = 27;
now
(2*13+1) mod 2 = 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24;
hence not 2 divides 27;
(4*6+3) mod 4 = 3 mod 4 by NAT_D:21
.= 3 by NAT_D:24;
hence not 4 divides 27;
(5*5+2) mod 5 = 2 mod 5 by NAT_D:21
.= 2 by NAT_D:24;
hence not 5 divides 27;
(6*4+3) mod 6 = 3 mod 6 by NAT_D:21
.= 3 by NAT_D:24;
hence not 6 divides 27;
(7*3+6) mod 7 = 6 mod 7 by NAT_D:21
.= 6 by NAT_D:24;
hence not 7 divides 27;
(8*3+3) mod 8 = 3 mod 8 by NAT_D:21
.= 3 by NAT_D:24;
hence not 8 divides 27;
(10*2+7) mod 10 = 7 mod 10 by NAT_D:21
.= 7 by NAT_D:24;
hence not 10 divides 27;
(11*2+5) mod 11 = 5 mod 11 by NAT_D:21
.= 5 by NAT_D:24;
hence not 11 divides 27;
(12*2+3) mod 12 = 3 mod 12 by NAT_D:21
.= 3 by NAT_D:24;
hence not 12 divides 27;
(13*2+1) mod 13 = 1 mod 13 by NAT_D:21
.= 1 by NAT_D:24;
hence not 13 divides 27;
(14*1+13) mod 14 = 13 mod 14 by NAT_D:21
.= 13 by NAT_D:24;
hence not 14 divides 27;
(15*1+12) mod 15 = 12 mod 15 by NAT_D:21
.= 12 by NAT_D:24;
hence not 15 divides 27;
(16*1+11) mod 16 = 11 mod 16 by NAT_D:21
.= 11 by NAT_D:24;
hence not 16 divides 27;
(17*1+10) mod 17 = 10 mod 17 by NAT_D:21
.= 10 by NAT_D:24;
hence not 17 divides 27;
(18*1+9) mod 18 = 9 mod 18 by NAT_D:21
.= 9 by NAT_D:24;
hence not 18 divides 27;
(19*1+8) mod 19 = 8 mod 19 by NAT_D:21
.= 8 by NAT_D:24;
hence not 19 divides 27;
(20*1+7) mod 20 = 7 mod 20 by NAT_D:21
.= 7 by NAT_D:24;
hence not 20 divides 27;
(21*1+6) mod 21 = 6 mod 21 by NAT_D:21
.= 6 by NAT_D:24;
hence not 21 divides 27;
(22*1+5) mod 22 = 5 mod 22 by NAT_D:21
.= 5 by NAT_D:24;
hence not 22 divides 27;
(23*1+4) mod 23 = 4 mod 23 by NAT_D:21
.= 4 by NAT_D:24;
hence not 23 divides 27;
(24*1+3) mod 24 = 3 mod 24 by NAT_D:21
.= 3 by NAT_D:24;
hence not 24 divides 27;
(25*1+2) mod 25 = 2 mod 25 by NAT_D:21
.= 2 by NAT_D:24;
hence not 25 divides 27;
(26*1+1) mod 26 = 1 mod 26 by NAT_D:21
.= 1 by NAT_D:24;
hence not 26 divides 27;
end;
hence thesis by A1,A2;
end;
begin :: Problem 25
theorem Th12:
for f being Function holds support (EmptyBag X +* f) = support f
proof
let f be Function;
set F = EmptyBag X +* f;
support F c= support EmptyBag X \/ support f by GLIB_004:1;
hence support F c= support f;
let x be object;
assume
A1: x in support f;
then
A2: f.x <> 0 by PRE_POLY:def 7;
support f c= dom f by PRE_POLY:37;
then F.x = f.x by A1,FUNCT_4:13;
hence thesis by A2,PRE_POLY:def 7;
end;
registration
let X be set;
let f be finite-support Function;
cluster EmptyBag X +* f -> finite-support;
coherence
proof
support f is finite;
hence support (EmptyBag X +* f) is finite by Th12;
end;
end;
registration
let p be Prime;
let n be non zero Nat;
cluster p |-count (p|^n) -> non zero;
coherence by NAT_3:25,INT_2:def 4;
end;
theorem Th13:
for b being finite-support Function holds
dom(b*canFS(support b)) = dom canFS(support b)
proof
let b be finite-support Function;
A1: rng canFS(support b) c= support b by FINSEQ_1:def 4;
support b c= dom b by PRE_POLY:37;
then rng canFS(support b) c= dom b by A1;
hence thesis by RELAT_1:27;
end;
theorem Th14:
for f,g being complex-valued Function holds support(f(#)g) c= support f
proof
let f,g be complex-valued Function;
let x be object;
assume
A1: x in support(f(#)g);
(f(#)g).x = f.x * g.x by VALUED_1:5;
then f.x <> 0 by A1,PRE_POLY:def 7;
hence thesis by PRE_POLY:def 7;
end;
registration
let f,g be finite-support complex-valued Function;
cluster f(#)g -> finite-support;
coherence
proof
support(f(#)g) c= support f by Th14;
hence support(f(#)g) is finite;
end;
end;
theorem Th15:
for f,g being complex-valued Function st
support(f) = support(g) holds support(f(#)g) = support f
proof
let f,g be complex-valued Function such that
A1: support(f) = support g;
thus support(f(#)g) c= support f by Th14;
let x be object;
assume x in support(f);
then
A2: f.x <> 0 & g.x <> 0 by A1,PRE_POLY:def 7;
(f(#)g).x = f.x * g.x by VALUED_1:5;
hence thesis by A2,PRE_POLY:def 7;
end;
theorem Th16:
for b1,b2 being finite-support complex-valued ManySortedSet of X st
support b1 = support b2 holds Product(b1(#)b2) = Product(b1) * Product(b2)
proof
let b1,b2 be finite-support complex-valued ManySortedSet of X;
set b0 = b1(#)b2;
assume
A1: support b1 = support b2;
A2: support b0 = support b1 by A1,Th15;
A3: support b0 = support b2 by A1,Th15;
consider f0 being FinSequence of COMPLEX such that
A4: Product b0 = Product f0 and
A5: f0 = b0*canFS(support b0) by NAT_3:def 5;
consider f1 being FinSequence of COMPLEX such that
A6: Product b1 = Product f1 and
A7: f1 = b1*canFS(support b1) by NAT_3:def 5;
consider f2 being FinSequence of COMPLEX such that
A8: Product b2 = Product f2 and
A9: f2 = b2*canFS(support b2) by NAT_3:def 5;
A10: f1 is (len f1)-element by CARD_1:def 7;
A11: f2 is (len f2)-element by CARD_1:def 7;
A12: dom(b0*canFS(support b0)) = dom canFS(support b0) by Th13;
then
A13: dom f0 = dom f1 by A2,A5,A7,Th13;
then
A14: len f0 = len f1 by FINSEQ_3:29;
A15: dom f0 = dom f2 by A3,A5,A9,A12,Th13;
then
A16: len f0 = len f2 by FINSEQ_3:29;
A17: dom f0 = dom f1 /\ dom f2 by A13,A15;
for c being object st c in dom f0 holds f0.c = f1.c * f2.c
proof
let c be object such that
A18: c in dom f0;
set x = (canFS(support b0)).c;
A19: f1.c = b1.x by A2,A7,A13,A18,FUNCT_1:12;
A20: f2.c = b2.x by A3,A9,A15,A18,FUNCT_1:12;
thus f0.c = b0.x by A5,A18,FUNCT_1:12
.= f1.c * f2.c by A19,A20,VALUED_1:5;
end;
then f0 = f1(#)f2 by A17,VALUED_1:def 4;
hence thesis by A4,A6,A8,A10,A11,A14,A16,NEWTON04:63;
end;
definition
let n be non zero Nat;
set A = support ppf n;
func Euler_factorization n -> Function means :Def1:
dom it = support ppf n &
for p being Nat st p in dom it
ex c being non zero Nat st c = p |-count n & it.p = p|^c - p|^(c-1);
existence
proof
n >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose
A1: n = 1;
take {};
support ppf 1 = support pfexp 1 by NAT_3:def 9;
hence thesis by A1;
end;
suppose n > 1;
then reconsider A as non empty natural-membered set by NAT_3:57;
A2: A = support pfexp n by NAT_3:def 9;
defpred P[object,object] means
ex a st a = $1 &
ex c being non zero Nat st c = a |-count n & $2 = a|^c - a|^(c-1);
A3: for e being object st e in A ex u being object st P[e,u]
proof
let e be object;
assume
A4: e in A;
then reconsider e as Prime by A2,NAT_3:34;
A5: e > 1 by INT_2:def 4;
set c = e |-count n;
now
assume c = 0;
then
A6: not e divides n by A5,NAT_3:27;
e in support pfexp n by A4,NAT_3:def 9;
hence contradiction by A6,NAT_3:36;
end;
then reconsider c as non zero Nat;
take e|^c - e|^(c-1);
thus thesis;
end;
consider f being Function such that
A7: dom f = A and
A8: for e being object st e in A holds P[e,f.e] from CLASSES1:sch 1(A3);
take f;
thus dom f = support ppf n by A7;
let p be Nat such that
A9: p in dom f;
A = support pfexp n by NAT_3:def 9;
then reconsider p as Prime by A7,A9,NAT_3:34;
A10: p > 1 by INT_2:def 4;
set c = p |-count n;
now
assume c = 0;
then
A11: not p divides n by A10,NAT_3:27;
p in support pfexp n by A7,A9,NAT_3:def 9;
hence contradiction by A11,NAT_3:36;
end;
then reconsider c as non zero Nat;
take c;
P[p,f.p] by A7,A8,A9;
hence thesis;
end;
end;
uniqueness
proof
let f,g be Function such that
A12: dom f = A and
A13: for p being Nat st p in dom f holds
ex c being non zero Nat st c = p |-count n & f.p = p|^c - p|^(c-1) and
A14: dom g = A and
A15: for p being Nat st p in dom g holds
ex c being non zero Nat st c = p |-count n & g.p = p|^c - p|^(c-1);
thus dom f = dom g by A12,A14;
let p be object such that
A16: p in dom f;
reconsider p as Nat by A12,A16;
A17: ex c being non zero Nat st c = p |-count n & f.p = p|^c - p|^(c-1)
by A13,A16;
ex c being non zero Nat st c = p |-count n & g.p = p|^c - p|^(c-1)
by A12,A14,A15,A16;
hence thesis by A17;
end;
end;
registration
let n be non zero Nat;
cluster dom Euler_factorization n -> finite;
coherence
proof
dom Euler_factorization n = support ppf n by Def1;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization n -> SetPrimes-defined;
coherence
proof
dom Euler_factorization n = support ppf n by Def1;
hence dom Euler_factorization n c= SetPrimes;
end;
end;
theorem Th17:
for n being non zero Nat, p being object
st p in dom Euler_factorization n holds p is Prime
proof
let n be non zero Nat, p be object;
dom Euler_factorization n c= SetPrimes by RELAT_1:def 18;
hence thesis by NEWTON:def 6;
end;
theorem Th18:
for n being non zero Nat
for p being Nat st p in dom Euler_factorization n holds
ex c being non zero Nat st c = p |-count n &
(Euler_factorization n).p = p|^(c-1) * (p-1)
proof
let n be non zero Nat;
let p be Nat;
set f = Euler_factorization n;
assume p in dom f;
then consider c being non zero Nat such that
A1: c = p |-count n & f.p = p|^c - p|^(c-1) by Def1;
take c;
p|^c = p|^(c-1+1)
.= p|^(c-1)*p by NEWTON:6;
hence thesis by A1;
end;
registration
let n be non zero Nat;
cluster Euler_factorization n -> natural-valued;
coherence
proof
set f = Euler_factorization n;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th17;
consider c being non zero Nat such that
A2: c = p |-count n & f.p = p|^c - p|^(c-1) by A1,Def1;
c-1 <= c-0 by XREAL_1:7;
then p|^c - p|^(c-1) in NAT by INT_1:5,NAT_6:1;
hence thesis by A2;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization n -> finite-support;
coherence
proof
support Euler_factorization n c= dom Euler_factorization n by PRE_POLY:37;
hence support Euler_factorization n is finite;
end;
end;
registration
cluster Euler_factorization 1 -> empty;
coherence
proof
A1: dom Euler_factorization 1 = support ppf 1 by Def1;
support ppf 1 = support pfexp 1 by NAT_3:def 9;
hence thesis by A1;
end;
end;
theorem Th19:
for n being non zero Nat holds
Euler_factorization (p|^n) = p .--> (p|^n-p|^(n-1))
proof
let n be non zero Nat;
set x = p|^n-p|^(n-1);
set f = Euler_factorization (p|^n);
set g = p .--> x;
A1: dom f = support ppf (p|^n) by Def1
.= support pfexp (p|^n) by NAT_3:def 9
.= {p} by NAT_3:42;
A2: dom g = {p};
A3: p |-count (p|^n) = n by NAT_3:25,INT_2:def 4;
p in {p} by TARSKI:def 1;
then
consider c being non zero Nat such that
A4: c = p |-count (p|^n) & f.p = p|^c - p|^(c-1) by A1,Def1;
now
let a be object;
assume a in dom f;
then a = p by A1,TARSKI:def 1;
hence f.a = g.a by A3,A4,FUNCOP_1:72;
end;
hence thesis by A1,A2,FUNCT_1:def 11;
end;
theorem
Euler_factorization p = p .--> (p-1)
proof
Euler_factorization (p|^1) = p .--> (p|^1-p|^(1-1)) by Th19;
hence thesis by NEWTON:4;
end;
theorem Th21:
for n being non zero Nat holds
support Euler_factorization n = dom Euler_factorization n
proof
let n be non zero Nat;
set f = Euler_factorization n;
thus support f c= dom f by PRE_POLY:37;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th17;
consider c being non zero Nat such that
A2: c = p |-count n & f.p = p|^c - p|^(c-1) by A1,Def1;
c-1 < c-0 by XREAL_1:15;
then f.p <> 0 by A2,NAT_6:2;
hence thesis by PRE_POLY:def 7;
end;
theorem Th22:
for n being non zero Nat st n > 1 holds
support Euler_factorization n is non empty
proof
let n be non zero Nat such that
A1: n > 1;
set f = Euler_factorization n;
n >= 1+1 by A1,NAT_1:13;
then consider p being Element of NAT such that
A2: p is prime and
A3: p divides n by INT_2:31;
dom f = support ppf n by Def1
.= support pfexp n by NAT_3:def 9;
then consider c being non zero Nat such that
A4: c = p |-count n & f.p = p|^c - p|^(c-1) by A2,A3,NAT_3:37,Def1;
c-1 < c-0 by XREAL_1:15;
then f.p <> 0 by A2,A4,NAT_6:2;
hence thesis by PRE_POLY:def 7;
end;
theorem
for n being non zero Nat st n > 1 holds Euler_factorization n is non empty
proof
let n be non zero Nat;
support Euler_factorization n c= dom Euler_factorization n by PRE_POLY:37;
hence thesis by Th22;
end;
set B = EmptyBag SetPrimes;
theorem Th24:
for s,t being non zero Nat st s,t are_coprime holds
dom Euler_factorization s misses dom Euler_factorization t
proof
let s,t be non zero Nat;
A1: dom Euler_factorization s = support ppf s by Def1;
A2: dom Euler_factorization t = support ppf t by Def1;
A3: support ppf s = support pfexp s by NAT_3:def 9;
support ppf t = support pfexp t by NAT_3:def 9;
hence thesis by A1,A2,A3,NAT_3:44;
end;
theorem Th25:
for s,t being non zero Nat st s,t are_coprime holds
(EmptyBag SetPrimes +* Euler_factorization(s*t)) =
(EmptyBag SetPrimes +* Euler_factorization s) +
(EmptyBag SetPrimes +* Euler_factorization t)
proof
let s,t be non zero Nat such that
A1: s,t are_coprime;
set n = s*t;
set N = Euler_factorization n;
set S = Euler_factorization s;
set T = Euler_factorization t;
for x being object st x in SetPrimes holds (B+*N).x = (B+*S).x+(B+*T).x
proof
let x be object;
assume x in SetPrimes;
then
reconsider p = x as Prime by NEWTON:def 6;
A2: p |-count n = (p |-count s) + (p |-count t) by NAT_3:28;
A3: dom S = support ppf s by Def1;
A4: dom T = support ppf t by Def1;
A5: dom N = support ppf n by Def1;
ppf n = ppf s + ppf t by A1,NAT_3:58;
then
A6: dom N = dom S \/ dom T by A3,A4,A5,PRE_POLY:38;
per cases;
suppose
A7: x in dom S;
then
A8: not x in dom T by A1,Th24,XBOOLE_0:3;
then
A9: (B+*T).x = B.x by FUNCT_4:11;
A10: p |-count t = 0 by A4,A8,MOEBIUS1:15;
A11: x in dom N by A6,A7,XBOOLE_0:def 3;
then
A12: ex c being non zero Nat st c = p |-count n & N.p = p|^c - p|^(c-1)
by Def1;
ex c being non zero Nat st c = p |-count s & S.p = p|^c - p|^(c-1)
by A7,Def1;
hence (B+*S).x+(B+*T).x = N.x by A2,A7,A9,A10,A12,FUNCT_4:13
.= (B+*N).x by A11,FUNCT_4:13;
end;
suppose
A13: x in dom T;
A14: not x in dom S by A1,A13,Th24,XBOOLE_0:3;
then
A15: (B+*S).x = B.x by FUNCT_4:11;
A16: p |-count s = 0 by A3,A14,MOEBIUS1:15;
A17: x in dom N by A6,A13,XBOOLE_0:def 3;
then
A18: ex c being non zero Nat st c = p |-count n & N.p = p|^c - p|^(c-1)
by Def1;
ex c being non zero Nat st c = p |-count t & T.p = p|^c - p|^(c-1)
by A13,Def1;
hence (B+*S).x+(B+*T).x = N.x by A2,A13,A15,A16,A18,FUNCT_4:13
.= (B+*N).x by A17,FUNCT_4:13;
end;
suppose
A19: not x in dom S & not x in dom T;
then
A20: not x in dom N by A6,XBOOLE_0:def 3;
(B+*S).x = B.x & (B+*T).x = B.x by A19,FUNCT_4:11;
hence (B+*N).x = (B+*S).x+(B+*T).x by A20,FUNCT_4:11;
end;
end;
hence thesis by PRE_POLY:33;
end;
theorem Th26:
for n being non zero Nat holds
Euler n = Product ((EmptyBag SetPrimes) +* Euler_factorization n)
proof
let n be non zero Nat;
set N = Euler_factorization n;
defpred P[Nat] means for n being non zero Nat st
support (B +* Euler_factorization n) c= Seg $1 holds
Product (B +* Euler_factorization n) = Euler n;
A1: P[0]
proof
let n be non zero Nat;
set N = Euler_factorization n;
set G = B+*N;
A2: support G = support N by Th12;
assume
A3: support G c= Seg 0;
then
A4: n = 1 by A2,Th22,NAT_1:53;
support G = {} by A3;
then G = B by PRE_POLY:81;
hence Product G = Euler n by A4,NAT_3:20,EULER_1:17;
end;
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: P[k];
let n be non zero Nat;
set N = Euler_factorization n;
set p = k+1;
set e = p |-count n;
set s = p|^e;
set G = B+*N;
assume
A7: support G c= Seg p;
per cases;
suppose support G c= Seg k;
hence Product G = Euler n by A6;
end;
suppose
A8: not support G c= Seg k;
A9: support ppf n = support pfexp n by NAT_3:def 9;
A10: dom N = support ppf n by Def1;
A11: support G = support N by Th12;
A12: support N = dom N by Th21;
A13: now
assume
A14: not p in support G;
support G c= Seg k
proof
let x be object;
assume
A15: x in support G;
then reconsider m = x as Nat;
m <= p by A7,A15,FINSEQ_1:1;
then m < p by A14,A15,XXREAL_0:1;
then
A16: m <= k by NAT_1:13;
x is Prime by A11,A12,A15,Th17;
then 1 <= m by INT_2:def 4;
hence thesis by A16;
end;
hence contradiction by A8;
end;
then
A17: p is Prime by A11,A12,Th17;
then
A18: p > 1 by INT_2:def 4;
then s divides n by NAT_3:def 7;
then consider t being Nat such that
A19: n = s * t;
reconsider s, t as non zero Nat by A19;
set S = Euler_factorization s;
set T = Euler_factorization t;
A20: dom(B+*S) = SetPrimes by PARTFUN1:def 2;
(pfexp n).p = e by A17,NAT_3:def 8;
then
A21: e <> 0 by A9,A13,A10,A11,A12,PRE_POLY:def 7;
A22: support ppf t = support pfexp t by NAT_3:def 9;
A23: support (B+*T) = support T by Th12;
A24: support T = dom T by Th21;
A25: dom T = support ppf t by Def1;
A26: support T c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A27: x in support T;
then reconsider x as Nat by A24,A25;
A28: x in support pfexp t by A24,A25,A27,NAT_3:def 9;
A29: now
assume
A30: x = p;
(pfexp t).p = f by A17,NAT_3:def 8;
then f <> 0 by A28,A30,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A31: f = 1+g by NAT_1:10;
p|^f divides t by A18,NAT_3:def 7;
then consider u being Nat such that
A32: t = (p|^f)*u;
n = s * (((p|^g)*p)*u) by A19,A31,A32,NEWTON:6
.= s*p *((p|^g)*u)
.= (p|^(e+1))*((p|^g)*u) by NEWTON:6;
then p|^(e+1) divides n;
hence contradiction by A18,NAT_3:def 7;
end;
support ppf t c= support ppf n by A9,A19,A22,NAT_3:45;
then x in support N by A10,A12,A24,A25,A27;
then x <= p by A11,A7,FINSEQ_1:1;
then x < p by A29,XXREAL_0:1;
then
A33: x <= k by NAT_1:13;
x is Prime by A28,NAT_3:34;
then 1 <= x by INT_2:def 4;
hence thesis by A33;
end;
A34: s,t are_coprime
proof
set u = s gcd t;
A35: u divides t by NAT_D:def 5;
A36: 0+1 <= u by NAT_1:13;
assume s gcd t <> 1;
then u > 1 by A36,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider r being Element of NAT such that
A37: r is prime and
A38: r divides u by INT_2:31;
u divides s by NAT_D:def 5;
then r divides s by A38,NAT_D:4;
then r = 1 or r = p by A17,A37,NAT_3:5,INT_2:def 4;
then p in support pfexp t by A37,A38,A35,NAT_D:4,NAT_3:37;
then k+1 <= k by A26,A24,A25,A22,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
consider f being FinSequence of COMPLEX such that
A39: Product(B+*S) = Product f and
A40: f = (B+*S)*canFS(support(B+*S)) by NAT_3:def 5;
A41: dom S = support ppf s by Def1
.= support pfexp s by NAT_3:def 9;
A42: support pfexp s = {p} by A17,A21,NAT_3:42;
then
A43: p in dom S by A41,TARSKI:def 1;
A44: support S c= dom S by PRE_POLY:37;
consider c being non zero Nat such that
A45: c = p |-count s & S.p = p|^c - p|^(c-1) by A43,Def1;
A46: c-'1 = c-1 by XREAL_0:def 2;
{p} c= support S
proof
let x be object;
assume x in {p};
then
A47: x = p by TARSKI:def 1;
c-1 < c-0 by XREAL_1:15;
then S.p <> 0 by A45,A18,PEPIN:66;
hence thesis by A47,PRE_POLY:def 7;
end;
then support S = {p} by A41,A42,A44,XBOOLE_0:def 10;
then
A48: support(B+*S) = {p} by Th12;
then f = (B+*S)*<*p*> by A40,FINSEQ_1:94
.= <* (B+*S).p *> by A13,A20,FINSEQ_2:34;
then
A49: Product(B+*S) = S.p by A39,A43,FUNCT_4:13
.= Euler s by A17,A45,A46,NAT_1:14,INT_8:8;
Product((B+*S)+(B+*T)) = (Product(B+*S)) * (Product(B+*T))
by A23,A24,A34,A48,A41,A42,Th24,NAT_3:19;
then
A50: Product((B+*S)+(B+*T)) = Euler s * Euler t by A6,A49,A23,A26;
Euler n = Euler s * Euler t by A19,A34,EULER_1:21;
hence Product G = Euler n by A50,A19,A34,Th25;
end;
end;
A51: for k being Nat holds P[k] from NAT_1:sch 2(A1,A5);
set G = B+*N;
A52: support G = support N by Th12;
per cases;
suppose
A53: support G is empty;
then
A54: n = 1 by A52,Th22,NAT_1:53;
G = B by A53,PRE_POLY:81;
hence Product G = Euler n by A54,NAT_3:20,EULER_1:17;
end;
suppose support G is non empty;
then reconsider M = support G as finite non empty Subset of NAT
by XBOOLE_1:1;
A55: max M is Nat by TARSKI:1;
support G c= Seg max M
proof
let x be object;
assume
A56: x in support G;
then reconsider m = x as Nat;
A57: support G = support N by Th12;
support N c= dom N by PRE_POLY:37;
then x is Prime by A56,A57,Th17;
then
A58: 1 <= m by INT_2:def 4;
m <= max M by A56,XXREAL_2:def 8;
hence thesis by A58;
end;
hence thesis by A51,A55;
end;
end;
definition
let n be non zero Nat;
set A = support ppf n;
func Euler_factorization_1 n -> Function means :Def2:
dom it = support ppf n &
for p being Nat st p in dom it
ex c being non zero Nat st c = p |-count n & it.p = p|^(c-1);
existence
proof
n >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose
A1: n = 1;
take {};
support ppf 1 = support pfexp 1 by NAT_3:def 9;
hence thesis by A1;
end;
suppose n > 1;
then reconsider A as non empty natural-membered set by NAT_3:57;
A2: A = support pfexp n by NAT_3:def 9;
defpred P[object,object] means
ex a st a = $1 &
ex c being non zero Nat st c = a |-count n & $2 = a|^(c-1);
A3: for e being object st e in A ex u being object st P[e,u]
proof
let e be object;
assume
A4: e in A;
then reconsider e as Prime by A2,NAT_3:34;
A5: e > 1 by INT_2:def 4;
set c = e |-count n;
now
assume c = 0;
then
A6: not e divides n by A5,NAT_3:27;
e in support pfexp n by A4,NAT_3:def 9;
hence contradiction by A6,NAT_3:36;
end;
then reconsider c as non zero Nat;
take e|^(c-1);
thus thesis;
end;
consider f being Function such that
A7: dom f = A and
A8: for e being object st e in A holds P[e,f.e] from CLASSES1:sch 1(A3);
take f;
thus dom f = support ppf n by A7;
let p be Nat such that
A9: p in dom f;
A = support pfexp n by NAT_3:def 9;
then reconsider p as Prime by A7,A9,NAT_3:34;
A10: p > 1 by INT_2:def 4;
set c = p |-count n;
now
assume c = 0;
then
A11: not p divides n by A10,NAT_3:27;
p in support pfexp n by A7,A9,NAT_3:def 9;
hence contradiction by A11,NAT_3:36;
end;
then reconsider c as non zero Nat;
take c;
P[p,f.p] by A7,A8,A9;
hence thesis;
end;
end;
uniqueness
proof
let f,g be Function such that
A12: dom f = A and
A13: for p being Nat st p in dom f holds
ex c being non zero Nat st c = p |-count n & f.p = p|^(c-1) and
A14: dom g = A and
A15: for p being Nat st p in dom g holds
ex c being non zero Nat st c = p |-count n & g.p = p|^(c-1);
thus dom f = dom g by A12,A14;
let p be object such that
A16: p in dom f;
reconsider p as Nat by A12,A16;
A17: ex c being non zero Nat st c = p |-count n & f.p = p|^(c-1) by A13,A16;
ex c being non zero Nat st c = p |-count n & g.p = p|^(c-1) by A12,A14,A15,
A16;
hence thesis by A17;
end;
end;
registration
let n be non zero Nat;
cluster dom Euler_factorization_1 n -> finite;
coherence
proof
dom Euler_factorization_1 n = support ppf n by Def2;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_1 n -> SetPrimes-defined;
coherence
proof
dom Euler_factorization_1 n = support ppf n by Def2;
hence dom Euler_factorization_1 n c= SetPrimes;
end;
end;
theorem Th27:
for n being non zero Nat, p being object
st p in dom Euler_factorization_1 n holds p is Prime
proof
let n be non zero Nat, p be object;
dom Euler_factorization_1 n c= SetPrimes by RELAT_1:def 18;
hence thesis by NEWTON:def 6;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_1 n -> natural-valued;
coherence
proof
set f = Euler_factorization_1 n;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th27;
ex c being non zero Nat st c = p |-count n & f.p = p|^(c-1) by A1,Def2;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_1 n -> finite-support;
coherence
proof
support Euler_factorization_1 n c= dom Euler_factorization_1 n
by PRE_POLY:37;
hence support Euler_factorization_1 n is finite;
end;
end;
theorem Th28:
for n being non zero Nat holds
support Euler_factorization_1 n = dom Euler_factorization_1 n
proof
let n be non zero Nat;
set f = Euler_factorization_1 n;
thus support f c= dom f by PRE_POLY:37;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th27;
ex c being non zero Nat st c = p |-count n & f.p = p|^(c-1) by A1,Def2;
hence thesis by PRE_POLY:def 7;
end;
definition
let n be non zero Nat;
set A = support ppf n;
deffunc F(Nat) = $1-1;
func Euler_factorization_2 n -> Function means :Def3:
dom it = support ppf n &
for p being Nat st p in dom it holds it.p = p-1;
existence
proof
n >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose
A1: n = 1;
take {};
support ppf 1 = support pfexp 1 by NAT_3:def 9;
hence thesis by A1;
end;
suppose n > 1;
then reconsider A as non empty natural-membered set by NAT_3:57;
consider f being Function such that
A2: dom f = A & for d be Element of A holds f.d = F(d)
from FUNCT_1:sch 4;
take f;
thus thesis by A2;
end;
end;
uniqueness
proof
let f,g be Function such that
A3: dom f = A and
A4: for p being Nat st p in dom f holds f.p = F(p) and
A5: dom g = A and
A6: for p being Nat st p in dom g holds g.p = F(p);
thus dom f = dom g by A3,A5;
let p be object such that
A7: p in dom f;
reconsider p as Nat by A3,A7;
f.p = F(p) by A4,A7
.= g.p by A3,A5,A6,A7;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster dom Euler_factorization_2 n -> finite;
coherence
proof
dom Euler_factorization_2 n = support ppf n by Def3;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_2 n -> SetPrimes-defined;
coherence
proof
dom Euler_factorization_2 n = support ppf n by Def3;
hence dom Euler_factorization_2 n c= SetPrimes;
end;
end;
theorem Th29:
for n being non zero Nat, p being object
st p in dom Euler_factorization_2 n holds p is Prime
proof
let n be non zero Nat, p be object;
dom Euler_factorization_2 n c= SetPrimes by RELAT_1:def 18;
hence thesis by NEWTON:def 6;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_2 n -> natural-valued;
coherence
proof
set f = Euler_factorization_2 n;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th29;
f.p = p-1 by A1,Def3;
hence thesis;
end;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_2 n -> finite-support;
coherence
proof
support Euler_factorization_2 n c= dom Euler_factorization_2 n
by PRE_POLY:37;
hence support Euler_factorization_2 n is finite;
end;
end;
theorem Th30:
for n being non zero Nat holds
support Euler_factorization_2 n = dom Euler_factorization_2 n
proof
let n be non zero Nat;
set f = Euler_factorization_2 n;
thus support f c= dom f by PRE_POLY:37;
let p be object;
assume
A1: p in dom f;
then reconsider p as Prime by Th29;
f.p = p-1 by A1,Def3;
hence thesis by PRE_POLY:def 7;
end;
theorem Th31:
for n being non zero Nat holds
EmptyBag SetPrimes +* Euler_factorization n =
(EmptyBag SetPrimes +* Euler_factorization_1 n) (#)
(EmptyBag SetPrimes +* Euler_factorization_2 n)
proof
let n be non zero Nat;
set N = Euler_factorization n;
set S = Euler_factorization_1 n;
set T = Euler_factorization_2 n;
A1: dom N = support ppf n by Def1;
A2: dom S = support ppf n by Def2;
A3: dom T = support ppf n by Def3;
for x being object st x in SetPrimes holds (B+*N).x = (B+*S).x*(B+*T).x
proof
let x be object;
assume x in SetPrimes;
then reconsider p = x as Prime by NEWTON:def 6;
per cases;
suppose
A4: x in dom N;
then
A5: (B+*N).x = N.x & (B+*S).x = S.x & (B+*T).x = T.x
by A1,A2,A3,FUNCT_4:13;
consider c being non zero Nat such that
A6: c = p |-count n & S.p = p|^(c-1) by A1,A2,A4,Def2;
ex c being non zero Nat st
c = p |-count n & N.p = p|^(c-1) * (p-1) by A4,Th18;
hence thesis by A1,A3,A4,A5,A6,Def3;
end;
suppose not x in dom N;
then (B+*N).x = B.x & (B+*S).x = B.x & (B+*T).x = B.x
by A1,A2,A3,FUNCT_4:11;
hence thesis;
end;
end;
hence thesis by Th4;
end;
theorem Th32:
for f1,f2 being integer-valued FinSequence st len f1 = len f2 &
for n st 1 <= n <= len f1 holds f1.n divides f2.n holds
Product f1 divides Product f2
proof
let f1,f2 be integer-valued FinSequence such that
A1: len f1 = len f2 and
A2: for n st 1 <= n <= len f1 holds f1.n divides f2.n;
per cases by NAT_1:13;
suppose len f1 = 0;
then f1 = {} & f2 = {} by A1;
hence thesis;
end;
suppose
A3: 0+1 <= len f1;
defpred P[Nat] means
1 <= $1 <= len f1 implies Product(f1|$1) divides Product(f2|$1);
A4: P[0];
A5: P[k] implies P[k+1]
proof
assume that
A6: P[k] and
A7: 1 <= k+1 and
A8: k+1 <= len f1;
A9: k+0 < k+1 by XREAL_1:8;
per cases;
suppose
A10: k = 0;
f1 is non empty by A8;
then
A11: f1|1 = <*f1.1*> by FINSEQ_5:20;
f2 is non empty by A1,A8;
then f2|1 = <*f2.1*> by FINSEQ_5:20;
hence thesis by A2,A3,A10,A11;
end;
suppose k > 0;
then
A12: k >= 0+1 by NAT_1:13;
f1|(k+1) = f1|k ^ <*f1.(k+1)*> by A8,INT_6:5;
then
A13: Product(f1|(k+1)) = Product(f1|k) * f1.(k+1) by RVSUM_1:96;
f2|(k+1) = f2|k ^ <*f2.(k+1)*> by A1,A8,INT_6:5;
then
A14: Product(f2|(k+1)) = Product(f2|k) * f2.(k+1) by RVSUM_1:96;
f1.(k+1) divides f2.(k+1) by A2,A7,A8;
hence thesis by A6,A8,A9,A12,A13,A14,NEWTON02:2,XXREAL_0:2;
end;
end;
A15: P[k] from NAT_1:sch 2(A4,A5);
f1|len f1 = f1 & f2|len f2 = f2 by FINSEQ_3:113;
hence thesis by A1,A3,A15;
end;
end;
theorem Th33:
for n being non zero Nat holds
Product (EmptyBag SetPrimes +* Euler_factorization_1 n) divides n
proof
let n be non zero Nat;
set E = Euler n;
set b0 = ppf n;
set F1 = Euler_factorization_1 n;
set b1 = B+*F1;
consider f0 being FinSequence of COMPLEX such that
A1: Product b0 = Product f0 and
A2: f0 = b0*canFS(support b0) by NAT_3:def 5;
consider f1 being FinSequence of COMPLEX such that
A3: Product b1 = Product f1 and
A4: f1 = b1*canFS(support b1) by NAT_3:def 5;
A5: support b0 = support pfexp n by NAT_3:def 9;
A6: support b1 = support F1 by Th12;
A7: support F1 = dom F1 by Th28;
A8: dom F1 = support b0 by Def2;
A9: dom f0 = dom canFS(support b0) by A2,Th13;
A10: rng canFS(support b1) c= support b1 by FINSEQ_1:def 4;
A11: dom f1 = dom canFS(support b1) by A4,Th13;
then
A12: len f0 = len f1 by A6,A7,A8,A9,FINSEQ_3:29;
rng f0 c= NAT by A2,ORDINAL1:def 12;
then reconsider f0 as FinSequence of NAT by FINSEQ_1:def 4;
rng f1 c= NAT by A4,ORDINAL1:def 12;
then reconsider f1 as FinSequence of NAT by FINSEQ_1:def 4;
for x being Nat st 1 <= x <= len f1 holds f1.x divides f0.x
proof
let x be Nat such that
A13: 1 <= x and
A14: x <= len f1;
set p = (canFS(support b1)).x;
A15: x in dom f1 by A13,A14,FINSEQ_3:25;
dom(b1*canFS(support b1)) c= dom canFS(support b1) by RELAT_1:25;
then
A16: p in rng canFS(support b1) by A4,A15,FUNCT_1:def 3;
then consider c being non zero Nat such that
A17: c = p |-count n and
A18: F1.p = p|^(c-1) by A6,A7,A10,Def2;
A19: f1.x = b1.p by A4,A15,FUNCT_1:12
.= p|^(c-1) by A6,A7,A10,A16,A18,FUNCT_4:13;
A20: f0.x = b0.p by A2,A6,A7,A8,A9,A11,A13,A14,FINSEQ_3:25,FUNCT_1:12
.= p|^c by A5,A6,A7,A8,A10,A16,A17,NAT_3:def 9;
c-1 <= c-0 by XREAL_1:7;
hence f1.x divides f0.x by A19,A20,NEWTON:89;
end;
then Product f1 divides Product f0 by A12,Th32;
hence thesis by A1,A3,NAT_3:61;
end;
definition
let f be real-valued Function;
let r be Real;
pred f <= r means
for x being object st x in dom f holds f.x <= r;
end;
theorem
for f being real-valued Function, r1,r2 being Real st f <= r1 <= r2
holds f <= r2
proof
let f be real-valued Function;
let r1,r2 be Real such that
A1: f <= r1 and
A2: r1 <= r2;
let x be object;
assume x in dom f;
then f.x <= r1 by A1;
hence f.x <= r2 by A2,XXREAL_0:2;
end;
theorem Th35:
for f,g being real-valued Function st rng g c= rng f & f <= n holds g <= n
proof
let f,g be real-valued Function such that
A1: rng g c= rng f and
A2: f <= n;
let x be object;
assume x in dom g;
then g.x in rng g by FUNCT_1:def 3;
then ex a being object st a in dom f & f.a = g.x by A1,FUNCT_1:def 3;
hence g.x <= n by A2;
end;
theorem Th36:
for f,g being ext-real-valued FinSequence holds
f^g is increasing implies f is increasing & g is increasing
proof
let f,g be ext-real-valued FinSequence;
assume
A1: f^g is increasing;
A2: dom f c= dom(f^g) by FINSEQ_1:26;
thus f is increasing
proof
let e1,e2 be ExtReal;
assume e1 in dom f;
then
A3: e1 in dom (f^g) & f.e1 = (f^g).e1 by A2,FINSEQ_1:def 7;
assume e2 in dom f;
then e2 in dom (f^g) & f.e2 = (f^g).e2 by A2,FINSEQ_1:def 7;
hence thesis by A1,A3,VALUED_0:def 13;
end;
thus g is increasing
proof
let e1,e2 be ExtReal;
assume
A4: e1 in dom g;
then consider k1 being Nat such that
A5: e1 = k1 and
A6: len f + k1 in dom(f^g) by FINSEQ_1:27;
A7: g.e1 = (f^g).(len f + k1) by A4,A5,FINSEQ_1:def 7;
assume
A8: e2 in dom g;
then consider k2 being Nat such that
A9: e2 = k2 and
A10: len f + k2 in dom(f^g) by FINSEQ_1:27;
A11: g.e2 = (f^g).(len f + k2) by A8,A9,FINSEQ_1:def 7;
assume e1 < e2;
then len f + k1 < len f + k2 by A5,A9,XREAL_1:8;
hence thesis by A1,A6,A7,A10,A11,VALUED_0:def 13;
end;
end;
theorem Th37:
for f,g being ext-real-valued FinSequence holds
f^g is positive-yielding implies
f is positive-yielding & g is positive-yielding
proof
let f,g be ext-real-valued FinSequence;
assume
A1: f^g is positive-yielding;
thus f is positive-yielding
proof
let r;
assume r in rng f;
then consider x being object such that
A2: x in dom f and
A3: f.x = r by FUNCT_1:def 3;
A4: f.x in rng f by A2,FUNCT_1:def 3;
rng f c= rng(f^g) by FINSEQ_1:29;
hence thesis by A1,A3,A4,PARTFUN3:def 1;
end;
thus g is positive-yielding
proof
let r;
assume r in rng g;
then consider x being object such that
A5: x in dom g and
A6: g.x = r by FUNCT_1:def 3;
A7: g.x in rng g by A5,FUNCT_1:def 3;
rng g c= rng(f^g) by FINSEQ_1:30;
hence thesis by A1,A6,A7,PARTFUN3:def 1;
end;
end;
theorem Th38:
for f being natural-valued FinSequence st
f <= n & f is increasing positive-yielding holds
Product(f) divides n!
proof
let f be natural-valued FinSequence;
set x = f.len f;
assume that
A1: f <= n and
A2: f is increasing and
A3: f is positive-yielding;
per cases;
suppose len f = 0;
then f = {};
hence thesis by INT_2:12,RVSUM_1:94;
end;
suppose
A4: len f > 0;
defpred P[Nat] means
for f being natural-valued FinSequence st 0 < len f = $1 &
f <= n & f is increasing positive-yielding holds
Product(f) divides (f.len f)!;
A5: P[0];
A6: P[k] implies P[k+1]
proof
assume
A7: P[k];
let f being natural-valued FinSequence such that
A8: 0 < len f and
A9: len f = k+1 and
A10: f <= n and
A11: f is increasing and
A12: f is positive-yielding;
f <> {} by A8;
then consider g being FinSequence, x being object such that
A13: f = g^<*x*> by FINSEQ_1:46;
g is NAT-valued by A13,Th3;
then reconsider g as natural-valued FinSequence;
len(g^<*x*>) = len g + len <*x*> by FINSEQ_1:22;
then
A14: len f = len g + 1 by A13,FINSEQ_1:39;
then
A15: x = f.len f by A13,FINSEQ_1:42;
then reconsider x as Nat;
set y = g.len g;
0+1 <= len f by A8,NAT_1:13;
then
A16: len f in dom f by FINSEQ_3:25;
then
A17: x in rng f by A15,FUNCT_1:def 3;
per cases;
suppose len g = 0;
then f = <*x*> by A13,FILEREC1:3;
hence thesis by A12,A15,NEWTON:35;
end;
suppose
A18: 0 < len g;
A19: len f - 1 < len f - 0 by XREAL_1:8;
A20: 0+1 <= len g by A18,NAT_1:13;
then
A21: len g in dom f by A14,A19,FINSEQ_3:25;
A22: g <= n
proof
let q be object such that
A23: q in dom g;
A24: dom g c= dom f by A13,FINSEQ_1:26;
f.q = g.q by A13,A23,FINSEQ_1:def 7;
hence g.q <= n by A10,A23,A24;
end;
A25: <*x*> is ext-real-valued;
then
A26: g is increasing by A11,A13,Th36;
g is positive-yielding by A12,A13,A25,Th37;
then
A27: Product(g) divides y! by A7,A9,A14,A18,A22,A26;
A28: Product(g)*x divides y!*x by A27,NAT_3:1;
0+1 <= x by A12,A17,NAT_1:13;
then reconsider x1 = x-1 as Element of NAT by INT_1:5;
len g in dom g by A20,FINSEQ_3:25;
then y = f.len g by A13,FINSEQ_1:def 7;
then y <= x1 by A11,A14,A15,A16,A19,A21,VALUED_0:def 13,INT_1:52;
then y! divides x1! by Th6;
then
A29: y!*x divides x1!*x by NAT_3:1;
A30: (x1+1)! = (x1!) * (x1+1) by NEWTON:15;
Product(f) = Product(g)*x by A13,RVSUM_1:96;
hence thesis by A15,A28,A29,A30,INT_2:9;
end;
end;
P[k] from NAT_1:sch 2(A5,A6);
then
A31: Product(f) divides x! by A1,A2,A3,A4;
0+1 <= len f by A4,NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then x! divides n! by A1,Th6;
hence thesis by A31,INT_2:9;
end;
end;
registration
let f be natural-valued FinSequence;
cluster sort_a(f) -> natural-valued;
coherence
proof
rng f = rng sort_a(f) by CLASSES1:75,RFINSEQ2:def 6;
hence thesis by VALUED_0:def 6,RELAT_1:def 19;
end;
cluster sort_d(f) -> natural-valued;
coherence
proof
rng f = rng sort_d(f) by CLASSES1:75,RFINSEQ2:def 5;
hence thesis by VALUED_0:def 6,RELAT_1:def 19;
end;
end;
registration
let f be integer-valued FinSequence;
cluster sort_a(f) -> integer-valued;
coherence
proof
rng f = rng sort_a(f) by CLASSES1:75,RFINSEQ2:def 6;
hence thesis by VALUED_0:def 5,RELAT_1:def 19;
end;
cluster sort_d(f) -> integer-valued;
coherence
proof
rng f = rng sort_d(f) by CLASSES1:75,RFINSEQ2:def 5;
hence thesis by VALUED_0:def 5,RELAT_1:def 19;
end;
end;
registration
let f be rational-valued FinSequence;
cluster sort_a(f) -> rational-valued;
coherence
proof
rng f = rng sort_a(f) by CLASSES1:75,RFINSEQ2:def 6;
hence thesis by VALUED_0:def 4,RELAT_1:def 19;
end;
cluster sort_d(f) -> rational-valued;
coherence
proof
rng f = rng sort_d(f) by CLASSES1:75,RFINSEQ2:def 5;
hence thesis by VALUED_0:def 4,RELAT_1:def 19;
end;
end;
theorem Th39:
for P,R being Relation st rng R c= rng P & P is positive-yielding holds
R is positive-yielding
proof
let P,R be Relation;
assume
A1: rng R c= rng P & P is positive-yielding;
let r be Real;
thus thesis by A1,PARTFUN3:def 1;
end;
registration
let f be positive-yielding real-valued FinSequence;
cluster sort_a(f) -> positive-yielding;
coherence
proof
rng f = rng sort_a(f) by CLASSES1:75,RFINSEQ2:def 6;
hence thesis by Th39;
end;
end;
registration
cluster SetPrimes-defined -> NAT-defined for Function;
coherence
proof
let f be Function;
assume f is SetPrimes-defined;
then
A1: dom f c= SetPrimes by RELAT_1:def 18;
SetPrimes c= NAT;
hence dom f c= NAT by A1;
end;
end;
theorem Th40:
for f being real-valued finite-support Function holds
f <= n implies
for F being real-valued FinSequence st
F = ((EmptyBag SetPrimes)+*f)*canFS(support((EmptyBag SetPrimes)+*f))
holds F <= n
proof
let f be real-valued finite-support Function;
assume
A1: f <= n;
set b = B+*f;
set C = canFS(support b);
let F be real-valued FinSequence such that
A2: F = b*C;
let x be object such that
A3: x in dom F;
set y = C.x;
A4: F.x = b.y by A2,A3,FUNCT_1:12;
per cases;
suppose
A5: y in dom f;
then b.y = f.y by FUNCT_4:13;
hence F.x <= n by A1,A4,A5;
end;
suppose not y in dom f;
then b.y = B.y by FUNCT_4:11;
hence thesis by A2,A3,FUNCT_1:12;
end;
end;
theorem Th41:
for f being natural-valued finite-support Function
for F being real-valued FinSequence st
F = ((EmptyBag SetPrimes)+*f)*canFS(support((EmptyBag SetPrimes)+*f))
holds F is positive-yielding
proof
let f be natural-valued finite-support Function;
set b = B+*f;
set C = canFS(support b);
let F be real-valued FinSequence such that
A1: F = b*C;
A2: dom(b*C) = dom C by Th13;
A3: rng C = support b by FUNCT_2:def 3;
let r;
assume r in rng F;
then consider x being object such that
A4: x in dom F and
A5: F.x = r by FUNCT_1:def 3;
C.x in rng C by A1,A2,A4,FUNCT_1:def 3;
then b.(C.x) <> 0 by A3,PRE_POLY:def 7;
hence 0 < r by A1,A4,A5,FUNCT_1:12;
end;
theorem
for f being natural-valued finite-support SetPrimes-defined Function holds
f is increasing implies
for F being real-valued FinSequence st
F = ((EmptyBag SetPrimes)+*f)*canFS(support((EmptyBag SetPrimes)+*f))
holds sort_a(F) is one-to-one
proof
let f be natural-valued finite-support SetPrimes-defined Function such that
A1: f is increasing;
set b = B+*f;
set C = canFS(support b);
let F be real-valued FinSequence such that
A2: F = b*C;
set S = sort_a(F);
A3: F,S are_fiberwise_equipotent by RFINSEQ2:def 6;
A4: rng C = support b by FUNCT_2:def 3;
A5: support b = support f by Th12;
A6: support f c= dom f by PRE_POLY:37;
let e1,e2 be object such that
A7: e1 in dom S & e2 in dom S and
A8: S.e1 = S.e2 and
A9: e1 <> e2;
consider z1,z2 being set such that
A10: z1 in dom F & z2 in dom F and
A11: z1 <> z2 and
A12: F.z1 = S.e1 & F.z2 = S.e2 by A3,A7,A9,CONVEX2:13;
A13: z1 in dom C & z2 in dom C by A2,A10,Th13;
then
A14: C.z1 <> C.z2 by A11,FUNCT_1:def 4;
A15: C.z1 in rng C & C.z2 in rng C by A13,FUNCT_1:def 3;
then b.(C.z1) = f.(C.z1) & b.(C.z2) = f.(C.z2) by A4,A5,A6,FUNCT_4:13;
then F.z1 = f.(C.z1) & F.z2 = f.(C.z2) by A2,A10,FUNCT_1:12;
hence contradiction by A1,A4,A5,A6,A8,A12,A14,A15,FUNCT_1:def 4;
end;
theorem Th43:
for f being natural-valued finite-support SetPrimes-defined Function holds
f is increasing implies
for F being real-valued FinSequence st
F = ((EmptyBag SetPrimes)+*f)*canFS(support((EmptyBag SetPrimes)+*f))
holds sort_a(F) is increasing
proof
let f be natural-valued finite-support SetPrimes-defined Function such that
A1: f is increasing;
set b = B+*f;
set C = canFS(support b);
let F be real-valued FinSequence such that
A2: F = b*C;
set S = sort_a(F);
A3: F,S are_fiberwise_equipotent by RFINSEQ2:def 6;
A4: dom(b*C) = dom C by Th13;
A5: rng C = support b by FUNCT_2:def 3;
A6: support b = support f by Th12;
A7: support f c= dom f by PRE_POLY:37;
let e1,e2 be Nat such that
A8: e1 in dom S & e2 in dom S and
A9: e1 < e2;
consider z1,z2 being set such that
A10: z1 in dom F & z2 in dom F and
A11: z1 <> z2 and
A12: F.z1 = S.e1 & F.z2 = S.e2 by A3,A8,A9,CONVEX2:13;
A13: C.z1 <> C.z2 by A2,A4,A10,A11,FUNCT_1:def 4;
A14: C.z1 in rng C & C.z2 in rng C by A2,A4,A10,FUNCT_1:def 3;
then b.(C.z1) = f.(C.z1) & b.(C.z2) = f.(C.z2) by A5,A6,A7,FUNCT_4:13;
then
A15: F.z1 = f.(C.z1) & F.z2 = f.(C.z2) by A2,A10,FUNCT_1:12;
S.e1 <= S.e2 by A8,A9,RFINSEQ2:17;
hence thesis by A1,A5,A6,A7,A12,A13,A14,A15,FUNCT_1:def 4,XXREAL_0:1;
end;
theorem Th44:
for f being natural-valued finite-support SetPrimes-defined Function holds
f <= n & f is increasing implies
Product (EmptyBag SetPrimes +* f) divides n!
proof
let f be natural-valued finite-support SetPrimes-defined Function;
assume that
A1: f <= n and
A2: f is increasing;
set b = B+*f;
set C = canFS(support b);
consider F being FinSequence of COMPLEX such that
A3: Product b = Product F and
A4: F = b*C by NAT_3:def 5;
reconsider F as natural-valued FinSequence by A4;
set S = sort_a(F);
A5: Product F = Product S by EULER_2:10,RFINSEQ2:def 6;
A6: F <= n by A1,A4,Th40;
A7: F is positive-yielding by A4,Th41;
A8: rng F = rng S by RFINSEQ2:def 6,CLASSES1:75;
S is increasing by A2,A4,Th43;
hence Product b divides n! by A3,A5,A6,A7,A8,Th35,Th38;
end;
theorem Th45:
for n being non zero Nat holds Euler_factorization_2 n <= n-1
proof
let n be non zero Nat;
set f = Euler_factorization_2 n;
let x be object such that
A1: x in dom f;
reconsider p = x as Prime by A1,Th29;
A2: f.p = p-1 by A1,Def3;
A3: support ppf n = support pfexp n by NAT_3:def 9;
dom f = support ppf n by Def3;
then p <= n by A1,A3,NAT_3:36,NAT_D:7;
hence f.x <= n-1 by A2,XREAL_1:7;
end;
registration
let n be non zero Nat;
cluster Euler_factorization_2 n -> increasing;
coherence
proof
set f = Euler_factorization_2 n;
let e1,e2 be ExtReal such that
A1: e1 in dom f & e2 in dom f;
reconsider p1 = e1, p2 = e2 as Prime by A1,Th29;
f.p1 = p1-1 & f.p2 = p2-1 by A1,Def3;
hence thesis by XREAL_1:8;
end;
cluster Euler_factorization_2 n -> positive-yielding;
coherence
proof
set f = Euler_factorization_2 n;
let r;
assume r in rng f;
then consider x being object such that
A2: x in dom f and
A3: f.x = r by FUNCT_1:def 3;
reconsider p = x as Prime by A2,Th29;
f.p = p-1 by A2,Def3;
hence thesis by A3;
end;
end;
theorem
for n being non zero Nat holds
Product (EmptyBag SetPrimes +* Euler_factorization_2 n) divides (n-1)!
by Th45,Th44;
theorem Th47:
for n being non zero Nat holds Euler n divides n!
proof
let n be non zero Nat;
set F0 = Euler_factorization n;
set F1 = Euler_factorization_1 n;
set F2 = Euler_factorization_2 n;
set b0 = B+*F0;
set b1 = B+*F1;
set b2 = B+*F2;
A1: Euler n = Product(b0) by Th26;
A2: Product(b1) divides n by Th33;
A3: Product(b2) divides (n-1)! by Th45,Th44;
A4: support b1 = support F1 by Th12;
A5: support F1 = dom F1 by Th28;
A6: support b2 = support F2 by Th12;
A7: support F2 = dom F2 by Th30;
A8: dom F1 = support ppf n by Def2;
A9: dom F2 = support ppf n by Def3;
b0 = b1(#)b2 by Th31;
then
A10: Product(b0) = Product(b1) * Product(b2) by A4,A5,A6,A7,A8,A9,Th16;
(n-1+1)! = (n-1)! * (n-1+1) by NEWTON:15;
hence thesis by A1,A2,A3,A10,NEWTON02:2;
end;
:: Problem 25
theorem
for n being odd Nat holds n divides 2|^(n!) - 1
proof
let n be odd Nat;
set E = Euler n;
per cases;
suppose n <= 1;
then n = 1 by NAT_1:25;
hence thesis by NAT_D:6;
end;
suppose n > 1;
then (2|^E) mod n = 1 by Lm2,NAT_5:3,EULER_2:18;
then
A1: n divides 2|^E-1 by PEPIN:8;
2|^E-1 divides 2|^(n!)-1 by Th47,NUMBER05:19;
hence n divides 2|^(n!)-1 by A1,INT_2:9;
end;
end;
begin :: Problem 86
theorem Th49:
p1,p2,p3 are_mutually_distinct implies
p1 >= 2 & p2 >= 3 & p3 >= 5 or p1 >= 2 & p2 >= 5 & p3 >= 3 or
p1 >= 3 & p2 >= 2 & p3 >= 5 or p1 >= 3 & p2 >= 5 & p3 >= 2 or
p1 >= 5 & p2 >= 2 & p3 >= 3 or p1 >= 5 & p2 >= 3 & p3 >= 2
proof
assume that
A1: p1,p2,p3 are_mutually_distinct and
A2: p1 < 2 or p2 < 3 or p3 < 5 and
A3: p1 < 2 or p2 < 5 or p3 < 3 and
A4: p1 < 3 or p2 < 2 or p3 < 5 and
A5: p1 < 3 or p2 < 5 or p3 < 2 and
A6: p1 < 5 or p2 < 2 or p3 < 3 and
A7: p1 < 5 or p2 < 3 or p3 < 2;
per cases by A2;
suppose p1 < 1+1;
then p1 <= 1 by NAT_1:13;
hence contradiction by INT_2:def 4;
end;
suppose that
p1 >= 2 and
A8: p2 < 3;
A9: p2 = 2 by A8,NUMBER03:65;
then p3 = 3 by A1,A4,XPRIMET1:3,NUMBER03:65;
hence contradiction by A1,A6,A9,XPRIMET1:3;
end;
suppose that
A10: p1 >= 2 and
A11: p2 >= 3 and
A12: p3 < 5;
per cases by A12,XPRIMET1:3;
suppose
A13: p3 = 2;
then p1 = 3 by A1,A7,A11,XPRIMET1:3;
hence contradiction by A1,A5,A13,XPRIMET1:3;
end;
suppose p3 = 3;
then p2 = 2 by A1,A3,A10,XPRIMET1:3;
hence contradiction by A11;
end;
end;
end;
definition
let n be Nat;
pred n satisfies_Sierpinski_problem_86 means
ex p1,p2,p3 be Prime st p1,p2,p3 are_mutually_distinct & n|^2-1 = p1*p2*p3;
end;
Lm15:
for a1,b1,c1,a2,b2,c2 being Nat st a1 <= a2 & b1 <= b2 & c1 <= c2 holds
a1*b1*c1 <= a2*b2*c2
proof
let a1,b1,c1,a2,b2,c2 be Nat;
assume a1 <= a2 & b1 <= b2;
then a1*b1 <= a2*b2 by XREAL_1:66;
hence thesis by XREAL_1:66;
end;
theorem Th50:
n satisfies_Sierpinski_problem_86 implies n >= 6
proof
given a,b,c being Prime such that
A1: a,b,c are_mutually_distinct and
A2: n|^2-1 = a*b*c;
a >= 2 & b >= 3 & c >= 5 or a >= 2 & b >= 5 & c >= 3 or
a >= 3 & b >= 2 & c >= 5 or a >= 3 & b >= 5 & c >= 2 or
a >= 5 & b >= 2 & c >= 3 or a >= 5 & b >= 3 & c >= 2 by A1,Th49;
then
A3: a*b*c >= 2*3*5 or a*b*c >= 3*5*2 or a*b*c >= 5*2*3 by Lm15;
A4: 5 = 6-1;
A5: n|^2 = n*n by WSIERP_1:1;
assume n < 6;
then n = 0 or ... or n = 5 by A4,NUMBER02:7;
hence thesis by A2,A3,A5;
end;
theorem Th51:
for a,b,c being Prime st n|^2-1 = a*b*c holds n-1 is prime or n+1 is prime
proof
let a,b,c be Prime such that
A1: n|^2-1 = a*b*c;
A2: n|^2 = n^2 by WSIERP_1:1;
then
A3: n|^2-1 = (n-1)*(n+1);
A4: now
assume n < 1;
then n = 0 by NAT_1:14;
hence contradiction by A1;
end;
c divides (n-1)*(n+1) by A1,A2;
then per cases by INT_5:7;
suppose c divides n-1;
then c*(n+1) divides (n-1)*(n+1) by NAT_3:1;
then n+1 = 0+1 or n+1 = a or n+1 = b or n+1 = a*b
by A1,A2,GROUP_22:1,GR_CY_3:1;
then per cases by A1;
suppose n+1 = a or n+1 = b;
hence thesis;
end;
suppose n+1 = a*b;
hence thesis by A1,A3,XCMPLX_1:5;
end;
end;
suppose c divides n+1;
then c*(n-1) divides (n+1)*(n-1) by NAT_3:1;
then per cases by A1,A2,A4,GROUP_22:1,GR_CY_3:1;
suppose n-1 = 1;
hence thesis by XPRIMES1:3;
end;
suppose n-1 = a or n-1 = b;
hence thesis;
end;
suppose n-1 = a*b;
hence thesis by A1,A3,XCMPLX_1:5;
end;
end;
end;
theorem Th52:
n satisfies_Sierpinski_problem_86 implies
n-1 is prime & (ex x,y being Prime st x <> y & n+1 = x*y) or
n+1 is prime & (ex x,y being Prime st x <> y & n-1 = x*y)
proof
assume n satisfies_Sierpinski_problem_86;
then consider a,b,c being Prime such that
A1: a,b,c are_mutually_distinct and
A2: a*b*c = n|^2-1;
A3: n|^2 = n^2 by WSIERP_1:1;
then
A4: a*b*c = (n-1)*(n+1) by A2;
c divides a*b*c;
then
A5: c divides n-1 or c divides n+1 by A4,INT_5:7;
A6: c > 1 by INT_2:def 4;
A7: a*b*c = b*c*a;
A8: a*b*c = a*c*b;
A9: now
assume 1 > n;
then n = 0 by NAT_1:14;
hence contradiction by A2;
end;
per cases by A2,Th51;
suppose
A10: n-1 is prime;
then per cases by A5,A6;
suppose c = n-1;
hence thesis by A1,A4,XCMPLX_1:5;
end;
suppose c divides n+1;
then c*(n-1) divides (n+1)*(n-1) by NAT_3:1;
then per cases by A2,A3,A9,A10,GROUP_22:1,GR_CY_3:1;
suppose a = n-1;
hence thesis by A1,A4,A7,XCMPLX_1:5;
end;
suppose b = n-1;
hence thesis by A1,A4,A8,XCMPLX_1:5;
end;
end;
end;
suppose
A11: n+1 is prime;
then per cases by A5,A6;
suppose c = n+1;
hence thesis by A1,A4,XCMPLX_1:5;
end;
suppose c divides n-1;
then c*(n+1) divides (n-1)*(n+1) by NAT_3:1;
then per cases by A2,A3,A11,GROUP_22:1,GR_CY_3:1;
suppose a = n+1;
hence thesis by A1,A4,A7,XCMPLX_1:5;
end;
suppose b = n+1;
hence thesis by A1,A4,A8,XCMPLX_1:5;
end;
end;
end;
end;
theorem Th53:
n satisfies_Sierpinski_problem_86 implies n is even
proof
assume
A1: n satisfies_Sierpinski_problem_86;
assume n is odd;
then
A2: n-1 is even & n+1 is even;
n-1 is prime or n+1 is prime by A1,Th52;
then n-1 = 2 or n+1 = 2 by A2;
then n = 3 or n = 1;
hence thesis by A1,Th50;
end;
theorem Th54:
14|^2 - 1 = 3*5*13
proof
14|^2 = 14*14 by WSIERP_1:1;
hence thesis;
end;
theorem Th55:
16|^2 - 1 = 3*5*17
proof
16|^2 = 16*16 by WSIERP_1:1;
hence thesis;
end;
theorem Th56:
20|^2 - 1 = 3*7*19
proof
20|^2 = 20*20 by WSIERP_1:1;
hence thesis;
end;
theorem Th57:
22|^2 - 1 = 3*7*23
proof
22|^2 = 22*22 by WSIERP_1:1;
hence thesis;
end;
theorem Th58:
32|^2 - 1 = 3*11*31
proof
32|^2 = 32*32 by WSIERP_1:1;
hence thesis;
end;
::Problem 86 a
theorem
14 satisfies_Sierpinski_problem_86
proof
reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 13 as Prime by XPRIMES1:13;
take a,b,c;
thus thesis by Th54;
end;
::Problem 86 b
theorem
16 satisfies_Sierpinski_problem_86
proof
reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 17 as Prime by XPRIMES1:17;
take a,b,c;
thus thesis by Th55;
end;
::Problem 86 c
theorem
20 satisfies_Sierpinski_problem_86
proof
reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 7 as Prime by XPRIMES1:7;
reconsider c = 19 as Prime by XPRIMES1:19;
take a,b,c;
thus thesis by Th56;
end;
::Problem 86 d
theorem
22 satisfies_Sierpinski_problem_86
proof
reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 7 as Prime by XPRIMES1:7;
reconsider c = 23 as Prime by XPRIMES1:23;
take a,b,c;
thus thesis by Th57;
end;
::Problem 86 e
theorem
32 satisfies_Sierpinski_problem_86
proof
reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 11 as Prime by XPRIMES1:11;
reconsider c = 31 as Prime by XPRIMES1:31;
take a,b,c;
thus thesis by Th58;
end;
Lm16:
not 6 satisfies_Sierpinski_problem_86
proof
assume 6 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 6-1 is prime and
A1: ex x,y being Prime st x <> y & 6+1 = x*y;
thus contradiction by A1,XPRIMES1:7;
end;
suppose that 6+1 is prime and
A2: ex x,y being Prime st x <> y & 6-1 = x*y;
thus contradiction by A2,XPRIMES1:5;
end;
end;
Lm17:
not 7 satisfies_Sierpinski_problem_86
proof
7 = 2*3+1;
hence thesis by Th53;
end;
Lm18:
not 8 satisfies_Sierpinski_problem_86
proof
assume 8 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 8-1 is prime and
A1: ex x,y being Prime st x <> y & 8+1 = x*y;
consider x,y being Prime such that
A2: x <> y and
A3: x*y = 9 by A1;
x divides x*y;
then x = 1 or x = 3 or x = 9 by A3,Th9;
hence contradiction by A2,A3;
end;
suppose that 8+1 is prime and
A4: ex x,y being Prime st x <> y & 8-1 = x*y;
thus contradiction by A4,XPRIMES1:7;
end;
end;
Lm19:
not 9 satisfies_Sierpinski_problem_86
proof
9 = 2*4+1;
hence thesis by Th53;
end;
Lm20:
not 10 satisfies_Sierpinski_problem_86
proof
assume 10 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 10-1 is prime and
A1: ex x,y being Prime st x <> y & 10+1 = x*y;
thus contradiction by A1,XPRIMES1:11;
end;
suppose that 10+1 is prime and
A2: ex x,y being Prime st x <> y & 10-1 = x*y;
consider x,y being Prime such that
A3: x <> y and
A4: x*y = 9 by A2;
x divides x*y;
then x = 1 or x = 3 or x = 9 by A4,Th9;
hence contradiction by A3,A4;
end;
end;
Lm21:
not 11 satisfies_Sierpinski_problem_86
proof
11 = 2*5+1;
hence thesis by Th53;
end;
Lm22:
not 12 satisfies_Sierpinski_problem_86
proof
assume 12 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 12-1 is prime and
A1: ex x,y being Prime st x <> y & 12+1 = x*y;
thus contradiction by A1,XPRIMES1:13;
end;
suppose that 12+1 is prime and
A2: ex x,y being Prime st x <> y & 12-1 = x*y;
thus contradiction by A2,XPRIMES1:11;
end;
end;
Lm23:
not 13 satisfies_Sierpinski_problem_86
proof
13 = 2*6+1;
hence thesis by Th53;
end;
Lm24:
not 15 satisfies_Sierpinski_problem_86
proof
15 = 2*7+1;
hence thesis by Th53;
end;
Lm25:
not 17 satisfies_Sierpinski_problem_86
proof
17 = 2*8+1;
hence thesis by Th53;
end;
Lm26:
not 18 satisfies_Sierpinski_problem_86
proof
assume 18 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 18-1 is prime and
A1: ex x,y being Prime st x <> y & 18+1 = x*y;
thus contradiction by A1,XPRIMES1:19;
end;
suppose that 18+1 is prime and
A2: ex x,y being Prime st x <> y & 18-1 = x*y;
thus contradiction by A2,XPRIMES1:17;
end;
end;
Lm27:
not 19 satisfies_Sierpinski_problem_86
proof
19 = 2*9+1;
hence thesis by Th53;
end;
Lm28:
not 21 satisfies_Sierpinski_problem_86
proof
21 = 2*10+1;
hence thesis by Th53;
end;
Lm29:
not 23 satisfies_Sierpinski_problem_86
proof
23 = 2*11+1;
hence thesis by Th53;
end;
Lm30:
not 24 satisfies_Sierpinski_problem_86
proof
assume 24 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 24-1 is prime and
A1: ex x,y being Prime st x <> y & 24+1 = x*y;
consider x,y being Prime such that
A2: x <> y and
A3: 25 = x*y by A1;
x divides x*y;
then x = 1 or x = 5 or x = 25 by A3,Th10;
hence contradiction by A2,A3;
end;
suppose that 24+1 is prime and
A4: ex x,y being Prime st x <> y & 24-1 = x*y;
thus contradiction by A4,XPRIMES1:23;
end;
end;
Lm31:
not 25 satisfies_Sierpinski_problem_86
proof
25 = 2*12+1;
hence thesis by Th53;
end;
Lm32:
not 26 satisfies_Sierpinski_problem_86
proof
assume 26 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that
A1: 26-1 is prime and
ex x,y being Prime st x <> y & 26+1 = x*y;
thus contradiction by A1,XPRIMES0:25;
end;
suppose that 26+1 is prime and
A2: ex x,y being Prime st x <> y & 26-1 = x*y;
consider x,y being Prime such that
A3: x <> y and
A4: 25 = x*y by A2;
x divides x*y;
then x = 1 or x = 5 or x = 25 by A4,Th10;
hence contradiction by A3,A4;
end;
end;
Lm33:
not 27 satisfies_Sierpinski_problem_86
proof
27 = 2*13+1;
hence thesis by Th53;
end;
Lm34:
not 28 satisfies_Sierpinski_problem_86
proof
assume 28 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that
A1: 28-1 is prime and
ex x,y being Prime st x <> y & 28+1 = x*y;
thus contradiction by A1,XPRIMES0:27;
end;
suppose that 28+1 is prime and
A2: ex x,y being Prime st x <> y & 28-1 = x*y;
consider x,y being Prime such that
x <> y and
A3: 27 = x*y by A2;
x divides x*y;
then x = 1 or x = 3 or x = 9 or x = 27 by A3,Th11;
hence contradiction by A3,XPRIMES0:9;
end;
end;
Lm35:
not 29 satisfies_Sierpinski_problem_86
proof
29 = 2*14+1;
hence thesis by Th53;
end;
Lm36:
not 30 satisfies_Sierpinski_problem_86
proof
assume 30 satisfies_Sierpinski_problem_86;
then per cases by Th52;
suppose that 30-1 is prime and
A1: ex x,y being Prime st x <> y & 30+1 = x*y;
thus contradiction by A1,XPRIMES1:31;
end;
suppose that 30+1 is prime and
A2: ex x,y being Prime st x <> y & 30-1 = x*y;
thus contradiction by A2,XPRIMES1:29;
end;
end;
Lm37:
not 31 satisfies_Sierpinski_problem_86
proof
31 = 2*15+1;
hence thesis by Th53;
end;
:: Problem 86
theorem
n satisfies_Sierpinski_problem_86 & n <= 32 implies n in {14,16,20,22,32}
proof
assume
A1: n satisfies_Sierpinski_problem_86;
assume n <= 32;
then n = 0 or ... or n = 32;
hence thesis by A1,Th50,Lm16,Lm17,Lm18,Lm19,Lm20,Lm21,
Lm22,Lm23,Lm24,Lm25,Lm26,Lm27,Lm28,Lm29,Lm30,
Lm31,Lm32,Lm33,Lm34,Lm35,Lm36,Lm37,ENUMSET1:def 3;
end;
begin :: Problem 184
theorem Th65:
3|^(2*k),1 are_congruent_mod 8
proof
3|^2,1 are_congruent_mod 8 by Lm8;
then 3|^2|^k,1|^k are_congruent_mod 8 by GR_CY_3:34;
hence 3|^(2*k),1 are_congruent_mod 8 by NEWTON:9;
end;
theorem Th66:
not 8 divides 3|^n+1
proof
per cases;
suppose n is odd;
then consider k such that
A1: n = 2*k+1 by ABIAN:9;
A2: 3|^(2*k+1) = 3|^(2*k)*3 by NEWTON:6;
3|^(2*k),1 are_congruent_mod 8 by Th65;
then 3|^(2*k)*3,1*3 are_congruent_mod 8 by Lm14,INT_1:18;
then 3|^(2*k+1)+1,4 are_congruent_mod 8 by A2;
then (3|^n+1) mod 8 = 4 mod 8 by A1,NAT_D:64
.= 4 by NAT_D:24;
hence thesis;
end;
suppose n is even;
then consider k such that
A3: n = 2*k;
3|^(2*k),1 are_congruent_mod 8 by Th65;
then 3|^(2*k)+1,1+1 are_congruent_mod 8;
then (3|^n+1) mod 8 = 2 mod 8 by A3,NAT_D:64
.= 2 by NAT_D:24;
hence thesis;
end;
end;
:: Problem 184
theorem Th67:
n <> 0 & 2|^m - 3|^n = 1 implies m = 2 & n = 1
proof
assume that
A1: n <> 0 and
A2: 2|^m - 3|^n = 1;
A3: 3|^0 = 1 by NEWTON:4;
per cases by NAT_1:13;
suppose m <= 2;
then m = 0 or ... or m = 2;
then per cases;
suppose m = 0;
then 2|^0 - 3|^n = 1 by A2;
hence thesis by Lm1;
end;
suppose m = 1;
then 2|^1 - 3|^n = 1 by A2;
hence thesis by A1,A3,PEPIN:30;
end;
suppose
A4: m = 2;
then 2|^2 - 3|^n = 1 by A2;
then 3|^n = 3|^1 by Lm3;
hence thesis by A4,PEPIN:30;
end;
end;
suppose
A5: m >= 2+1;
not 8 divides 3|^n+1 by Th66;
hence thesis by A2,A5,Lm12,NEWTON:89;
end;
end;
begin :: Problem 185
theorem Th68:
3|^(2*k),1 are_congruent_mod 4
proof
(2*4+1) mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24;
then 3|^2,1 are_congruent_mod 4 by Lm8;
then 3|^2|^k,1|^k are_congruent_mod 4 by GR_CY_3:34;
hence 3|^(2*k),1 are_congruent_mod 4 by NEWTON:9;
end;
theorem Th69:
2|^n mod 4 = 2 implies n = 1
proof
assume
A1: 2|^n mod 4 = 2;
n = 0 or n >= 0+1 by NAT_1:13;
then per cases by XXREAL_0:1;
suppose n = 0;
then 2|^n = 1 by NEWTON:4;
hence thesis by A1,NAT_D:24;
end;
suppose n = 0+1;
hence thesis;
end;
suppose n > 0+1;
then n >= 1+1 by NAT_1:13;
then 2|^2 divides 2|^n by NEWTON:89;
hence thesis by A1,Lm3;
end;
end;
theorem Th70:
2|^m - 2|^n = 2 implies m = 2 & n = 1
proof
assume
A1: 2|^m - 2|^n = 2;
now
assume n >= m;
then 2|^m - 2|^n <= 2|^n - 2|^n by XREAL_1:9,PREPOWER:93;
hence contradiction by A1;
end;
then consider k such that
A2: m = n+k by NAT_1:10;
per cases;
suppose 1 <= n;
then reconsider n1 = n-1 as Element of NAT by INT_1:3;
A3: 2|^(n+k) = 2|^n * 2|^k by NEWTON:8;
2|^n = 2|^(n1+1)
.= 2|^n1*2 by NEWTON:6;
then 2|^n1*2*(2|^k-1) = 2*1 by A1,A2,A3;
then 2|^n1*(2|^k-1) = 1;
then 2|^n1 = 1 & 2|^k-1 = 1 by NAT_1:15;
then 2|^n1 = 2|^0 & 2|^k = 2|^1 by NEWTON:4;
then n1 = 0 & k = 1 by PEPIN:30;
hence thesis by A2;
end;
suppose n < 1;
then
A4: n = 0 by NAT_1:14;
then m = 0 by A1;
hence thesis by A1,A4;
end;
end;
theorem Th71:
n is odd & 3|^n - 2|^m = 1 implies n = m = 1
proof
assume that
A1: n is odd and
A2: 3|^n - 2|^m = 1;
A3: 3|^n = 1 + 2|^m by A2;
consider k such that
A4: n = 2*k+1 by A1,ABIAN:9;
3|^(2*k),1 are_congruent_mod 4 by Th68;
then 3|^(2*k)*3,1*3 are_congruent_mod 4 by Lm13,INT_1:18;
then 3|^n,3 are_congruent_mod 4 by A4,NEWTON:6;
then 2|^m,3-1 are_congruent_mod 4 by A2;
then 2|^m mod 4 = 2 mod 4 by NAT_D:64
.= 2 by NAT_D:24;
then
A5: m = 1 by Th69;
then 3|^n = 3|^1 by A3;
hence thesis by A5,PEPIN:30;
end;
theorem Th72:
n is even & 3|^n - 2|^m = 1 implies n = 2 & m = 3
proof
assume that
A1: n is even and
A2: 3|^n - 2|^m = 1;
consider k such that
A3: n = 2*k by A1;
A4: 3|^(2*k) = 3|^k|^2 by NEWTON:9
.= (3|^k)^2 by WSIERP_1:1;
A5: 2|^m = 3|^n - 1 by A2;
3|^k+1 divides (3|^k+1)*(3|^k-1);
then consider a such that
A6: 3|^k+1 = 2|^a by A5,A3,A4,NEWTON03:36,XPRIMES1:2;
3|^k-1 divides (3|^k+1)*(3|^k-1);
then consider b such that
A7: 3|^k-1 = 2|^b by A5,A3,A4,NEWTON03:36,XPRIMES1:2;
2|^a - 2|^b = 2 by A6,A7;
then 3|^k+1 = 4 by A6,Lm3,Th70;
then 3|^k = 3|^1;
then k = 1 by PEPIN:30;
hence thesis by A3,A5,Lm8,Lm12,PEPIN:30;
end;
:: Problem 185
theorem Th73:
3|^n - 2|^m = 1 implies n = m = 1 or n = 2 & m = 3
proof
per cases;
suppose n is odd;
hence thesis by Th71;
end;
suppose n is even;
hence thesis by Th72;
end;
end;
begin :: Problem 88
definition
let n;
attr n is having_exactly_one_prime_divisor means
ex p being Prime st p divides n &
for r being Prime st r <> p holds not r divides n;
end;
definition
let n;
assume
A1: n is having_exactly_one_prime_divisor;
func the_only_divisor_of n -> Prime means :Def7:
it divides n & for r being Prime st r <> it holds not r divides n;
existence by A1;
uniqueness;
end;
theorem
n is having_exactly_one_prime_divisor & p divides n implies
the_only_divisor_of n = p by Def7;
registration
cluster prime -> having_exactly_one_prime_divisor for Nat;
coherence
proof
let n;
assume n is prime;
then reconsider n as Prime;
take n;
thus thesis by Th7;
end;
end;
theorem
the_only_divisor_of p = p by Def7;
registration
cluster zero -> non having_exactly_one_prime_divisor for Nat;
coherence
proof
let n be Nat;
assume
A1: n is zero;
given p being Prime such that
p divides n and
A2: for r being Prime st r <> p holds not r divides n;
ex p1 being Prime st p < p1 by NEWTON:72;
hence contradiction by A1,A2,INT_2:12;
end;
end;
theorem
1 is non having_exactly_one_prime_divisor by NAT_D:7,INT_2:def 4;
registration
let p be Prime;
cluster p|^0 -> non having_exactly_one_prime_divisor;
coherence
proof
let p1 be Prime;
p|^0 = 1 by NEWTON:4;
hence thesis by NAT_D:7,INT_2:def 4;
end;
end;
registration
let p be Prime;
let k be non zero Nat;
cluster p|^k -> having_exactly_one_prime_divisor;
coherence
proof
take p;
thus p divides p|^k by NAT_3:3;
thus thesis by NAT_3:6;
end;
end;
theorem Th77:
p1 <> p2 implies not p1*p2 is having_exactly_one_prime_divisor
proof
assume
A1: p1 <> p2;
given p being Prime such that
p divides p1*p2 and
A2: for r being Prime st r <> p holds not r divides p1*p2;
p1 divides p1*p2 & p2 divides p1*p2;
then p1 = p & p2 = p by A2;
hence thesis by A1;
end;
theorem Th78:
n is having_exactly_one_prime_divisor implies
ex k being non zero Nat st n = (the_only_divisor_of n) |^ k
proof
assume
A1: n is having_exactly_one_prime_divisor;
then consider p being Prime such that
A2: p divides n and
A3: for r being Prime st r <> p holds not r divides n;
A4: the_only_divisor_of n = p by A1,A2,Def7;
now
assume for k being Nat holds n <> p|^k;
then ex s being Element of NAT st
s is prime & s divides n & s <> p by GROUPP_1:1;
hence contradiction by A3;
end;
then consider k being Nat such that
A5: n = (the_only_divisor_of n) |^ k by A4;
reconsider k as non zero Nat by A1,A5;
take k;
thus thesis by A5;
end;
:: Problem 88
theorem
n > 7 implies
ex m being Nat, p, q being Prime st p <> q &
(m = n or m = n+1 or m = n+2) & p divides m & q divides m
proof
assume
A1: n > 7;
assume
A2: not thesis;
then not 2 divides n or not 3 divides n by XPRIMES1:2,3;
then
A3: not 2*3 divides n by NUMBER04:3;
not 2 divides n+1 or not 3 divides n+1 by A2,XPRIMES1:2,3;
then
A4: not 2*3 divides n+1 by NUMBER04:3;
not 2 divides n+2 or not 3 divides n+2 by A2,XPRIMES1:2,3;
then
A5: not 2*3 divides n+2 by NUMBER04:3;
consider k such that
A6: 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;
A7: n is having_exactly_one_prime_divisor
proof
consider p being Element of NAT such that
A8: p is prime and
A9: p divides n by A1,XXREAL_0:2,INT_2:31;
reconsider p as Prime by A8;
take p;
thus thesis by A2,A9;
end;
A10: n+1 is having_exactly_one_prime_divisor
proof
n+1 > n+0 by XREAL_1:8;
then n+1 > 7 by A1,XXREAL_0:2;
then consider p being Element of NAT such that
A11: p is prime and
A12: p divides n+1 by INT_2:31,XXREAL_0:2;
reconsider p as Prime by A11;
take p;
thus thesis by A2,A12;
end;
A13: n+2 is having_exactly_one_prime_divisor
proof
n+2 > n+0 by XREAL_1:8;
then n+2 > 7 by A1,XXREAL_0:2;
then consider p being Element of NAT such that
A14: p is prime and
A15: p divides n+2 by INT_2:31,XXREAL_0:2;
reconsider p as Prime by A14;
take p;
thus thesis by A2,A15;
end;
per cases by A6;
suppose n = 6*k;
hence thesis by A3;
end;
suppose
A16: n = 6*k+1;
consider m being non zero Nat such that
A17: n+1 = (the_only_divisor_of (n+1)) |^ m by A10,Th78;
n+1 = 2*(3*k+1) by A16;
then 2 divides n+1;
then
A18: the_only_divisor_of (n+1) = 2 by A10,Def7,XPRIMES1:2;
consider s being non zero Nat such that
A19: n+2 = (the_only_divisor_of (n+2)) |^ s by A13,Th78;
n+2 = 3*(2*k+1) by A16;
then 3 divides n+2;
then
A20: the_only_divisor_of (n+2) = 3 by A13,Def7,XPRIMES1:3;
A21: now
assume m <= 3;
then n+1 <= 7+1 by A17,A18,Lm12,PREPOWER:93;
hence contradiction by A1,XREAL_1:8;
end;
3|^s - 2|^m = 1 by A17,A19,A18,A20;
then s = m = 1 or s = 2 & m = 3 by Th73;
hence thesis by A21;
end;
suppose
A22: n = 6*k+2;
consider m being non zero Nat such that
A23: n = (the_only_divisor_of n) |^ m by A7,Th78;
n = 2*(3*k+1) by A22;
then 2 divides n;
then
A24: the_only_divisor_of n = 2 by A7,Def7,XPRIMES1:2;
consider s being non zero Nat such that
A25: n+1 = (the_only_divisor_of (n+1)) |^ s by A10,Th78;
n+1 = 3*(2*k+1) by A22;
then 3 divides n+1;
then
A26: the_only_divisor_of (n+1) = 3 by A10,Def7,XPRIMES1:3;
A27: now
assume m <= 3;
then
A28: n <= 7+1 by A23,A24,Lm12,PREPOWER:93;
n >= 7+1 by A1,NAT_1:13;
then
A29: n = 8 by A28,XXREAL_0:1;
not 2*5 is having_exactly_one_prime_divisor by Th77,XPRIMES1:2,5;
hence contradiction by A13,A29;
end;
3|^s - 2|^m = 1 by A23,A25,A24,A26;
then s = m = 1 or s = 2 & m = 3 by Th73;
hence thesis by A27;
end;
suppose
A30: n = 6*k+3;
consider s being non zero Nat such that
A31: n = (the_only_divisor_of n) |^ s by A7,Th78;
n = 3*(2*k+1) by A30;
then 3 divides n;
then
A32: the_only_divisor_of n = 3 by A7,Def7,XPRIMES1:3;
consider m being non zero Nat such that
A33: n+1 = (the_only_divisor_of (n+1)) |^ m by A10,Th78;
n+1 = 2*(3*k+2) by A30;
then 2 divides n+1;
then
A34: the_only_divisor_of (n+1) = 2 by A10,Def7,XPRIMES1:2;
A35: now
assume m <= 3;
then n+1 <= 7+1 by A33,A34,Lm12,PREPOWER:93;
hence contradiction by A1,XREAL_1:8;
end;
2|^m - 3|^s = 1 by A33,A31,A34,A32;
then s = 1 & m = 2 by Th67;
hence thesis by A35;
end;
suppose n = 6*k+4;
then n+2 = 6*(k+1);
hence thesis by A5;
end;
suppose n = 6*k+5;
then n+1 = 6*(k+1);
hence thesis by A4;
end;
end;
begin :: Problem 105
definition
let n;
attr n is having_at_least_three_different_prime_divisors means
ex q1,q2,q3 being Prime st q1,q2,q3 are_mutually_distinct &
q1 divides n & q2 divides n & q3 divides n;
end;
definition
let n be non zero Nat;
pred n satisfies_Sierpinski_problem_105 means
n-1 is having_at_least_three_different_prime_divisors &
n+1 is having_at_least_three_different_prime_divisors;
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;
theorem
n is having_exactly_one_prime_divisor implies
not n is having_at_least_three_different_prime_divisors
proof
given p being Prime such that
p divides n and
A1: for r being Prime st r <> p holds not r divides n;
given q1,q2,q3 being Prime such that
A2: q1,q2,q3 are_mutually_distinct and
A3: q1 divides n & q2 divides n and q3 divides n;
q1 = p & q2 = p by A1,A3;
hence contradiction by A2;
end;
registration
cluster zero -> having_at_least_three_different_prime_divisors for Nat;
coherence
proof
let n such that
A1: n is zero;
take P2,P3,P5;
thus thesis by A1,NAT_D:6;
end;
end;
theorem Th81:
n > 0 & n is having_at_least_three_different_prime_divisors implies n >= 30
proof
assume
A1: n > 0;
given p1,p2,p3 being Prime such that
A2: p1,p2,p3 are_mutually_distinct and
A3: p1 divides n & p2 divides n & p3 divides n;
p1 >= 2 & p2 >= 3 & p3 >= 5 or p1 >= 2 & p2 >= 5 & p3 >= 3 or
p1 >= 3 & p2 >= 2 & p3 >= 5 or p1 >= 3 & p2 >= 5 & p3 >= 2 or
p1 >= 5 & p2 >= 2 & p3 >= 3 or p1 >= 5 & p2 >= 3 & p3 >= 2 by A2,Th49;
then
A4: p1*p2*p3 >= 2*3*5 or p1*p2*p3 >= 3*5*2 or p1*p2*p3 >= 5*2*3 by Lm15;
A5: p1*p2 divides n by A2,A3,PEPIN:4,INT_2:30;
p1,p3 are_coprime & p2,p3 are_coprime by A2,INT_2:30;
then
p1*p2,p3 are_coprime by EULER_1:14;
then p1*p2*p3 <= n by A1,A3,A5,NAT_D:7,PEPIN:4;
hence thesis by A4,XXREAL_0:2;
end;
registration
cluster prime -> non having_at_least_three_different_prime_divisors for Nat;
coherence
proof
let n be Nat;
assume
A1: n is prime;
given q1,q2,q3 being Prime such that
A2: q1,q2,q3 are_mutually_distinct and
A3: q1 divides n & q2 divides n & q3 divides n;
q1 = n & q2 = n & q3 = n by A1,A3,Th7;
hence contradiction by A2;
end;
end;
registration
let p1,p2;
cluster p1*p2 -> non having_at_least_three_different_prime_divisors;
coherence
proof
set n = p1*p2;
given q1,q2,q3 being Prime such that
A1: q1,q2,q3 are_mutually_distinct and
A2: q1 divides n & q2 divides n & q3 divides n;
(q1 divides p1 or q1 divides p2) &
(q2 divides p1 or q2 divides p2) &
(q3 divides p1 or q3 divides p2) by A2,INT_5:7;
then (q1 = p1 or q1 = p2) & (q2 = p1 or q2 = p2) &
(q3 = p1 or q3 = p2) by Th7;
hence contradiction by A1;
end;
end;
registration
let p,n;
cluster p|^n -> non having_at_least_three_different_prime_divisors;
coherence
proof
given q1,q2,q3 being Prime such that
A1: q1,q2,q3 are_mutually_distinct and
A2: q1 divides p|^n & q2 divides p|^n & q3 divides p|^n;
q1 = p & q2 = p & q3 = p by A2,Th7,NAT_3:5;
hence thesis by A1;
end;
end;
registration
let p1,p2,m,n;
cluster p1|^m * p2|^n -> non having_at_least_three_different_prime_divisors;
coherence
proof
set a = p1|^m;
set b = p2|^n;
given q1,q2,q3 being Prime such that
A1: q1,q2,q3 are_mutually_distinct and
A2: q1 divides a*b & q2 divides a*b & q3 divides a*b;
(q1 divides a or q1 divides b) & (q2 divides a or q2 divides b) &
(q3 divides a or q3 divides b) by A2,INT_5:7;
then (q1 = p1 or q1 = p2) & (q2 = p1 or q2 = p2) & (q3 = p1 or q3 = p2)
by Th7,NAT_3:5;
hence thesis by A1;
end;
end;
:: Problem 105 a
theorem
131 satisfies_Sierpinski_problem_105
proof
A1: 130 = 2*5*13;
A2: 2,5,13 are_mutually_distinct;
130 = 5*13*2 & 130 = 13*2*5;
then 2 divides 130 & 5 divides 130 & 13 divides 130 by A1;
hence 131-1 is having_at_least_three_different_prime_divisors
by A2,XPRIMES1:2,5,13;
A3: 132 = 2*2*3*11;
A4: 2,3,11 are_mutually_distinct;
132 = 3*11*2*2 & 132 = 11*2*2*3;
then 2 divides 132 & 3 divides 132 & 11 divides 132 by A3;
hence 131+1 is having_at_least_three_different_prime_divisors
by A4,XPRIMES1:2,3,11;
end;
Lm38:
not 37 satisfies_Sierpinski_problem_105
proof
36 = 2|^2 * 3|^2 by Lm3,Lm8;
hence thesis by XPRIMES1:2,3;
end;
Lm39:
not 41 satisfies_Sierpinski_problem_105
proof
40 = 2|^3 * 5|^1 by Lm4;
hence thesis by XPRIMES1:2,5;
end;
Lm40:
not 43 satisfies_Sierpinski_problem_105
proof
44 = 2|^2 * 11|^1 by Lm3;
hence thesis by XPRIMES1:2,11;
end;
Lm41:
not 47 satisfies_Sierpinski_problem_105
proof
46 = 2*23;
hence thesis by XPRIMES1:2,23;
end;
Lm42:
not 53 satisfies_Sierpinski_problem_105
proof
54 = 2|^1 * 3|^3 by Lm9;
hence thesis by XPRIMES1:2,3;
end;
Lm43:
not 59 satisfies_Sierpinski_problem_105
proof
58 = 2*29;
hence thesis by XPRIMES1:2,29;
end;
Lm44:
not 61 satisfies_Sierpinski_problem_105
proof
62 = 2*31;
hence thesis by XPRIMES1:2,31;
end;
Lm45:
not 67 satisfies_Sierpinski_problem_105
proof
68 = 2|^2 * 17|^1 by Lm3;
hence thesis by XPRIMES1:2,17;
end;
Lm46:
not 71 satisfies_Sierpinski_problem_105
proof
72 = 2|^3 * 3|^2 by Lm4,Lm8;
hence thesis by XPRIMES1:2,3;
end;
Lm47:
not 73 satisfies_Sierpinski_problem_105
proof
74 = 2*37;
hence thesis by XPRIMES1:2,37;
end;
Lm48:
not 79 satisfies_Sierpinski_problem_105
proof
80 = 2|^4 * 5|^1 by Lm5;
hence thesis by XPRIMES1:2,5;
end;
Lm49:
not 83 satisfies_Sierpinski_problem_105
proof
82 = 2*41;
hence thesis by XPRIMES1:2,41;
end;
Lm50:
not 89 satisfies_Sierpinski_problem_105
proof
88 = 2|^3 * 11|^1 by Lm4;
hence thesis by XPRIMES1:2,11;
end;
Lm51:
not 97 satisfies_Sierpinski_problem_105
proof
7|^2 = 7*7 by NEWTON:81;
then 98 = 2|^1 * 7|^2;
hence thesis by XPRIMES1:2,7;
end;
Lm52:
not 101 satisfies_Sierpinski_problem_105
proof
5|^2 = 5*5 by NEWTON:81;
then 100 = 2|^2 * 5|^2 by Lm3;
hence thesis by XPRIMES1:2,5;
end;
Lm53:
not 103 satisfies_Sierpinski_problem_105
proof
104 = 2|^3 * 13|^1 by Lm4;
hence thesis by XPRIMES1:2,13;
end;
Lm54:
not 107 satisfies_Sierpinski_problem_105
proof
108 = 2|^2 * 3|^3 by Lm3,Lm9;
hence thesis by XPRIMES1:2,3;
end;
Lm55:
not 109 satisfies_Sierpinski_problem_105
proof
108 = 2|^2 * 3|^3 by Lm3,Lm9;
hence thesis by XPRIMES1:2,3;
end;
Lm56:
not 113 satisfies_Sierpinski_problem_105
proof
112 = 2|^4 * 7|^1 by Lm5;
hence thesis by XPRIMES1:2,7;
end;
:: Problem 105
theorem
not ex p being Prime st p <= 130 & p satisfies_Sierpinski_problem_105
proof
given p being Prime such that
A1: p <= 130 and
A2: p satisfies_Sierpinski_problem_105;
p < 130+1 by A1,NAT_1:13;
then per cases by XPRIMET1:61;
suppose p = 2;
hence thesis by A2,Th81;
end;
suppose p = 3;
hence thesis by A2,Th81;
end;
suppose p = 5;
hence thesis by A2,Th81;
end;
suppose p = 7;
hence thesis by A2,Th81;
end;
suppose p = 11;
hence thesis by A2,Th81;
end;
suppose p = 13;
hence thesis by A2,Th81;
end;
suppose p = 17;
hence thesis by A2,Th81;
end;
suppose p = 19;
hence thesis by A2,Th81;
end;
suppose p = 23;
hence thesis by A2,Th81;
end;
suppose p = 29;
hence thesis by A2,Th81;
end;
suppose p = 31;
hence thesis by A2,Lm6,XPRIMES1:2;
end;
suppose p = 37;
hence thesis by A2,Lm38;
end;
suppose p = 41;
hence thesis by A2,Lm39;
end;
suppose p = 43;
hence thesis by A2,Lm40;
end;
suppose p = 47;
hence thesis by A2,Lm41;
end;
suppose p = 53;
hence thesis by A2,Lm42;
end;
suppose p = 59;
hence thesis by A2,Lm43;
end;
suppose p = 61;
hence thesis by A2,Lm44;
end;
suppose p = 67;
hence thesis by A2,Lm45;
end;
suppose p = 71;
hence thesis by A2,Lm46;
end;
suppose p = 73;
hence thesis by A2,Lm47;
end;
suppose p = 79;
hence thesis by A2,Lm48;
end;
suppose p = 83;
hence thesis by A2,Lm49;
end;
suppose p = 89;
hence thesis by A2,Lm50;
end;
suppose p = 97;
hence thesis by A2,Lm51;
end;
suppose p = 101;
hence thesis by A2,Lm52;
end;
suppose p = 103;
hence thesis by A2,Lm53;
end;
suppose p = 107;
hence thesis by A2,Lm54;
end;
suppose p = 109;
hence thesis by A2,Lm55;
end;
suppose p = 113;
hence thesis by A2,Lm56;
end;
suppose p = 127;
hence thesis by A2,Lm7,XPRIMES1:2;
end;
end;
begin :: Problem 111
theorem
1 + 3 + 3|^2 + 3|^3 + 3|^4 = 11|^2 by Lm8,Lm9,Lm10,Lm11;
theorem Th85:
m divides p|^4 iff m in {1,p,p|^2,p|^3,p|^4}
proof
thus m divides p|^4 implies m in {1,p,p|^2,p|^3,p|^4}
proof
assume m divides p|^4;
then consider r being Nat such that
A1: m = p|^r and
A2: r <= 4 by GROUPP_1:2;
r = 0 or ... or r = 4 by A2;
then m = 1 or m = p or m = p|^2 or m = p|^3 or m = p|^4 by A1,NEWTON:4;
hence thesis by ENUMSET1:def 3;
end;
assume m in {1,p,p|^2,p|^3,p|^4};
then m = 1 or m = p|^1 or m = p|^2 or m = p|^3 or m = p|^4
by ENUMSET1:def 3;
hence thesis by INT_2:12,NEWTON:89;
end;
theorem Th86:
1 + p + p|^2 + p|^3 + p|^4 is square iff p = 3
proof
set x = 1 + p + p|^2 + p|^3 + p|^4;
thus x is square implies p = 3
proof
given n being Nat such that
A1: x = n^2;
A2: p|^2 = p^2 by WSIERP_1:1;
A3: p|^3 = p^2*p by POLYEQ_5:2;
A4: p|^4 = p*p*p*p by POLYEQ_5:3
.= p^2*p^2;
(4 + 4*p + 4*p^2 + 4*p|^3 + 4*p|^4) - (4*p|^4 + 4*p|^3 + p^2)
= 4 + 4*p + 3*p^2;
then (2*p^2+p)^2 < (2*n)^2 by A1,A2,A3,A4,XREAL_1:47;
then
A5: 2*p^2+p < 2*n by XREAL_1:66;
(2*p^2+p+2)^2 - (4 + 4*p + 4*p^2 + 4*p|^3 + 4*p|^4)
= 5*p^2 by A3,A4;
then (2*n)^2 < (2*p^2+p+2)^2 by A1,A2,XREAL_1:47;
then 2*n < 2*p^2+p+2 by XREAL_1:66;
then (2*n)^2 = (2*p^2+p+1)^2 by A5,Th1;
then (p+1)*(p-3) = 0 by A1,A2,A3,A4;
then p+1 = 0 or p-3 = 0;
hence thesis;
end;
thus thesis by Lm8,Lm9,Lm10,Lm11;
end;
:: Problem 111 a
theorem
NatDivisors(p|^4) = {1,p,p|^2,p|^3,p|^4}
proof
set A = NatDivisors(p|^4);
set B = {1,p,p|^2,p|^3,p|^4};
thus A c= B
proof
let x be object;
assume x in A;
then ex k st x = k & k <> 0 & k divides p|^4;
hence thesis by Th85;
end;
let m be object;
assume
A1: m in B;
then reconsider m as Nat by ENUMSET1:def 3;
m divides p|^4 by A1,Th85;
hence thesis by A1;
end;
:: Problem 111
theorem
{ p where p is Prime: 1 + p + p|^2 + p|^3 + p|^4 is square } = {3}
proof
set A = { p where p is Prime: 1 + p + p|^2 + p|^3 + p|^4 is square };
thus A c= {3}
proof
let x be object;
assume x in A;
then ex p being Prime st x = p & 1 + p + p|^2 + p|^3 + p|^4 is square;
then x = 3 by Th86;
hence thesis by TARSKI:def 1;
end;
let p be object;
assume p in {3};
then
A1: p = 3 by TARSKI:def 1;
then reconsider p as Prime by XPRIMES1:3;
1 + p + p|^2 + p|^3 + p|^4 is square by A1,Th86;
hence thesis;
end;
begin :: Problem 137
registration
let D be non empty set;
cluster -> total for sequence of D;
coherence
proof
let f be sequence of D;
thus dom f = NAT by FUNCT_2:def 1;
end;
end;
registration
let D be non empty set;
let f be [:COMPLEX,D:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`1 -> complex;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:COMPLEX,D:] by RELAT_1:def 19;
then (f.n)`1 in COMPLEX by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:D,COMPLEX:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`2 -> complex;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:D,COMPLEX:] by RELAT_1:def 19;
then (f.n)`2 in COMPLEX by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:REAL,D:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`1 -> real;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:REAL,D:] by RELAT_1:def 19;
then (f.n)`1 in REAL by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:D,REAL:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`2 -> real;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:D,REAL:] by RELAT_1:def 19;
then (f.n)`2 in REAL by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:RAT,D:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`1 -> rational;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:RAT,D:] by RELAT_1:def 19;
then (f.n)`1 in RAT by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:D,RAT:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`2 -> rational;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:D,RAT:] by RELAT_1:def 19;
then (f.n)`2 in RAT by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:INT,D:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`1 -> integer;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:INT,D:] by RELAT_1:def 19;
hence thesis by A1,MCART_1:10;
end;
end;
registration
let D be non empty set;
let f be [:D,INT:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`2 -> integer;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:D,INT:] by RELAT_1:def 19;
hence thesis by A1,MCART_1:10;
end;
end;
registration
let D be non empty set;
let f be [:NAT,D:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`1 -> natural;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:NAT,D:] by RELAT_1:def 19;
then (f.n)`1 in NAT by A1,MCART_1:10;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be [:D,NAT:]-valued ManySortedSet of NAT;
let n be Nat;
cluster (f.n)`2 -> natural;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
dom f = NAT by PARTFUN1:def 2;
then
A1: f.n in rng f by FUNCT_1:def 3;
rng f c= [:D,NAT:] by RELAT_1:def 19;
then (f.n)`2 in NAT by A1,MCART_1:10;
hence thesis;
end;
end;
definition
let a,b,x1,x2,x3,y1,y2,y3 be Complex;
func recSeqCart(a,b,x1,x2,x3,y1,y2,y3) ->
[:COMPLEX,COMPLEX:]-valued ManySortedSet of NAT
means :Def10:
it.0 = [a,b] &
for n being Nat holds
it.(n+1) = [x1*(it.n)`1 + x2*(it.n)`2 + x3 , y1*(it.n)`1 + y2*(it.n)`2 + y3];
existence
proof
reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
deffunc p1(Complex,Complex) = x1*$1+x2*$2+x3;
deffunc p2(Complex,Complex) = y1*$1+y2*$2+y3;
defpred
P[object,Element of [:COMPLEX,COMPLEX:],Element of [:COMPLEX,COMPLEX:]]
means
$3 = [p1($2`1,$2`2),p2($2`1,$2`2)];
A1: for n being Nat for x being Element of [:COMPLEX,COMPLEX:]
ex y being Element of [:COMPLEX,COMPLEX:] st P[n,x,y]
proof
let n;
let x be Element of [:COMPLEX,COMPLEX:];
reconsider a1 = p1(x`1,x`2), a2 = p2(x`1,x`2) as Element of COMPLEX
by XCMPLX_0:def 2;
take [a1,a2];
thus thesis;
end;
consider f being sequence of [:COMPLEX,COMPLEX:] such that
A2: f.0 = [a,b] & for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be [:COMPLEX,COMPLEX:]-valued ManySortedSet of NAT such that
A3: f.0 = [a,b] and
A4: for n being Nat holds
f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] and
A5: g.0 = [a,b] and
A6: for n being Nat holds
g.(n+1) = [x1*(g.n)`1+x2*(g.n)`2+x3,y1*(g.n)`1+y2*(g.n)`2+y3];
defpred P[Nat] means f.$1 = g.$1;
A7: P[0] by A3,A5;
A8: P[n] implies P[n+1]
proof
assume
A9: P[n];
thus f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] by A4
.= g.(n+1) by A6,A9;
end;
A10: P[n] from NAT_1:sch 2(A7,A8);
let n be object;
thus thesis by A10;
end;
end;
registration
let a,b,x1,x2,x3,y1,y2,y3 be Real;
cluster recSeqCart(a,b,x1,x2,x3,y1,y2,y3) -> [:REAL,REAL:]-valued;
coherence
proof
set f = recSeqCart(a,b,x1,x2,x3,y1,y2,y3);
A1: a in REAL & b in REAL by XREAL_0:def 1;
defpred P[Nat] means f.$1 in [:REAL,REAL:];
A2: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1,ZFMISC_1:87;
end;
A3: P[n] implies P[n+1]
proof
assume P[n];
then (f.n)`1 in REAL & (f.n)`2 in REAL by MCART_1:10;
then
A4: x1*(f.n)`1+x2*(f.n)`2+x3 in REAL & y1*(f.n)`1+y2*(f.n)`2+y3 in REAL
by XREAL_0:def 1;
f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] by Def10;
hence thesis by A4,ZFMISC_1:87;
end;
A5: P[n] from NAT_1:sch 2(A2,A3);
thus rng f c= [:REAL,REAL:]
proof
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A5;
end;
end;
end;
registration
let a,b,x1,x2,x3,y1,y2,y3 be Rational;
cluster recSeqCart(a,b,x1,x2,x3,y1,y2,y3) -> [:RAT,RAT:]-valued;
coherence
proof
set f = recSeqCart(a,b,x1,x2,x3,y1,y2,y3);
A1: a in RAT & b in RAT by RAT_1:def 2;
defpred P[Nat] means f.$1 in [:RAT,RAT:];
A2: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1,ZFMISC_1:87;
end;
A3: P[n] implies P[n+1]
proof
assume P[n];
then (f.n)`1 in RAT & (f.n)`2 in RAT by MCART_1:10;
then
A4: x1*(f.n)`1+x2*(f.n)`2+x3 in RAT & y1*(f.n)`1+y2*(f.n)`2+y3 in RAT
by RAT_1:def 2;
f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] by Def10;
hence thesis by A4,ZFMISC_1:87;
end;
A5: P[n] from NAT_1:sch 2(A2,A3);
thus rng f c= [:RAT,RAT:]
proof
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A5;
end;
end;
end;
registration
let a,b,x1,x2,x3,y1,y2,y3 be Integer;
cluster recSeqCart(a,b,x1,x2,x3,y1,y2,y3) -> [:INT,INT:]-valued;
coherence
proof
set f = recSeqCart(a,b,x1,x2,x3,y1,y2,y3);
A1: a in INT & b in INT by INT_1:def 2;
defpred P[Nat] means f.$1 in [:INT,INT:];
A2: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1,ZFMISC_1:87;
end;
A3: P[n] implies P[n+1]
proof
assume P[n];
then (f.n)`1 in INT & (f.n)`2 in INT by MCART_1:10;
then
A4: x1*(f.n)`1+x2*(f.n)`2+x3 in INT & y1*(f.n)`1+y2*(f.n)`2+y3 in INT
by INT_1:def 2;
f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] by Def10;
hence thesis by A4,ZFMISC_1:87;
end;
A5: P[n] from NAT_1:sch 2(A2,A3);
thus rng f c= [:INT,INT:]
proof
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A5;
end;
end;
end;
registration
let a,b,x1,x2,x3,y1,y2,y3 be Nat;
cluster recSeqCart(a,b,x1,x2,x3,y1,y2,y3) -> [:NAT,NAT:]-valued;
coherence
proof
set f = recSeqCart(a,b,x1,x2,x3,y1,y2,y3);
A1: a in NAT & b in NAT by ORDINAL1:def 12;
defpred P[Nat] means f.$1 in [:NAT,NAT:];
A2: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1,ZFMISC_1:87;
end;
A3: P[n] implies P[n+1]
proof
assume P[n];
then (f.n)`1 in NAT & (f.n)`2 in NAT by MCART_1:10;
then
A4: x1*(f.n)`1+x2*(f.n)`2+x3 in NAT & y1*(f.n)`1+y2*(f.n)`2+y3 in NAT
by ORDINAL1:def 12;
f.(n+1) = [x1*(f.n)`1+x2*(f.n)`2+x3,y1*(f.n)`1+y2*(f.n)`2+y3] by Def10;
hence thesis by A4,ZFMISC_1:87;
end;
A5: P[n] from NAT_1:sch 2(A2,A3);
thus rng f c= [:NAT,NAT:]
proof
let y be object;
assume y in rng f;
then ex x being object st x in dom f & f.x = y by FUNCT_1:def 3;
hence thesis by A5;
end;
end;
end;
theorem Th89:
for a,b,a1,a2,a3,b1,b2,b3 being Real st a > 0 & b > 0 & a3 >= 0 & b3 >= 0 &
(a1 > 0 & a2 >= 0 or a1 >= 0 & a2 > 0) &
(b1 > 0 & b2 >= 0 or b1 >= 0 & b2 > 0) holds
for n being Nat holds
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`1 > 0 &
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`2 > 0
proof
let a,b,a1,a2,a3,b1,b2,b3 be Real such that
A1: a > 0 & b > 0 and
B1: a3 >= 0 & b3 >= 0 and
A2: (a1 > 0 & a2 >= 0 or a1 >= 0 & a2 > 0) &
(b1 > 0 & b2 >= 0 or b1 >= 0 & b2 > 0);
set f = recSeqCart(a,b,a1,a2,a3,b1,b2,b3);
defpred P[Nat] means (f.$1)`1 > 0 & (f.$1)`2 > 0;
A3: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1;
end;
A4: P[k] implies P[k+1]
proof
f.(k+1) = [a1*(f.k)`1+a2*(f.k)`2+a3,b1*(f.k)`1+b2*(f.k)`2+b3] by Def10;
hence thesis by B1,A2;
end;
P[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th90:
for a,b,a1,a2,a3,b1,b2,b3 being Real st a >= 0 & b >= 0 &
a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0 holds
for n being Nat holds
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`1 >= 0 &
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`2 >= 0
proof
let a,b,a1,a2,a3,b1,b2,b3 be Real such that
A1: a >= 0 & b >= 0 and
A2: a1 >= 0 & a2 >= 0 & a3 >= 0 & b1 >= 0 & b2 >= 0 & b3 >= 0;
set f = recSeqCart(a,b,a1,a2,a3,b1,b2,b3);
defpred P[Nat] means (f.$1)`1 >= 0 & (f.$1)`2 >= 0;
A3: P[0]
proof
f.0 = [a,b] by Def10;
hence thesis by A1;
end;
A4: P[k] implies P[k+1]
proof
f.(k+1) = [a1*(f.k)`1+a2*(f.k)`2+a3,b1*(f.k)`1+b2*(f.k)`2+b3] by Def10;
hence thesis by A2;
end;
P[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th91:
for a,b,a1,a2,a3,b1,b2,b3 being Real st
a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 holds
for m,n being Nat st m > n holds
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).m)`1
> (recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`1 &
(recSeqCart(a,b,a1,a2,a3,b1,b2,b3).m)`2
> (recSeqCart(a,b,a1,a2,a3,b1,b2,b3).n)`2
proof
let a,b,a1,a2,a3,b1,b2,b3 be Real such that
A1: a > 0 & b > 0 and
A2: a1 >= 1 & a2 > 0 & a3 >= 0 and
A3: b1 > 0 & b2 >= 1 & b3 >= 0;
set f = recSeqCart(a,b,a1,a2,a3,b1,b2,b3);
let m,n such that
A4: m > n;
defpred P[Nat] means
$1 > n implies (f.$1)`1 > (f.n)`1 & (f.$1)`2 > (f.n)`2;
A5: P[0];
A6: P[k] implies P[k+1]
proof
assume that
A7: P[k] and
A8: k+1 > n;
A9: f.(k+1) = [a1*(f.k)`1+a2*(f.k)`2+a3,b1*(f.k)`1+b2*(f.k)`2+b3] by Def10;
(f.k)`1 >= 0 by A1,A2,A3,Th90;
then
A10: 1*(f.k)`1 <= a1*(f.k)`1 by A2,XREAL_1:64;
(f.k)`2 > 0 by A1,A2,A3,Th89;
then
B11: a1*(f.k)`1+0 < a1*(f.k)`1+a2*(f.k)`2 by A2,XREAL_1:6;
a1*(f.k)`1+a2*(f.k)`2+0 <= a1*(f.k)`1+a2*(f.k)`2+a3 by A2,XREAL_1:6;
then
A11: a1*(f.k)`1+0 < a1*(f.k)`1+a2*(f.k)`2+a3 by B11,XXREAL_0:2;
(f.k)`2 >= 0 by A1,A2,A3,Th90;
then
A12: 1*(f.k)`2 <= b2*(f.k)`2 by A3,XREAL_1:64;
(f.k)`1 > 0 by A1,A2,A3,Th89;
then
B13: b2*(f.k)`2+0 < b1*(f.k)`1+b2*(f.k)`2 by A3,XREAL_1:6;
b1*(f.k)`1+b2*(f.k)`2+0 <= b1*(f.k)`1+b2*(f.k)`2+b3 by A3,XREAL_1:6;
then
A13: b2*(f.k)`2+0 < b1*(f.k)`1+b2*(f.k)`2+b3 by B13,XXREAL_0:2;
k >= n by A8,NAT_1:13;
then per cases by XXREAL_0:1;
suppose
A14: k > n;
then (f.n)`1 < a1*(f.k)`1 by A7,A10,XXREAL_0:2;
hence (f.(k+1))`1 > (f.n)`1 by A9,A11,XXREAL_0:2;
(f.n)`2 < b2*(f.k)`2 by A7,A12,A14,XXREAL_0:2;
hence (f.(k+1))`2 > (f.n)`2 by A9,A13,XXREAL_0:2;
end;
suppose k = n;
hence thesis by A9,A10,A11,A12,A13,XXREAL_0:2;
end;
end;
P[k] from NAT_1:sch 2(A5,A6);
hence thesis by A4;
end;
theorem Th92:
for a,b,a1,a2,a3,b1,b2,b3 being Real st
a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0 holds
recSeqCart(a,b,a1,a2,a3,b1,b2,b3) is one-to-one
proof
let a,b,a1,a2,a3,b1,b2,b3 be Real such that
A1: a > 0 & b > 0 & a1 >= 1 & a2 > 0 & a3 >= 0 & b1 > 0 & b2 >= 1 & b3 >= 0;
set f = recSeqCart(a,b,a1,a2,a3,b1,b2,b3);
let x1,x2 be object such that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2;
reconsider x1,x2 as Element of NAT by A2,PARTFUN1:def 2;
now
assume x1 <> x2;
then x1 < x2 or x2 < x1 by XXREAL_0:1;
then (f.x1)`1 < (f.x2)`1 or (f.x2)`1 < (f.x1)`1 by A1,Th91;
hence contradiction by A3;
end;
hence thesis;
end;
::Problem 137
theorem
{ [x,y] where x,y is positive Nat: 3*x^2-7*y^2+1 = 0 } is infinite
proof
deffunc R(Complex,Complex) = 3*$1^2-7*$2^2+1;
set A = {[x,y] where x,y is positive Nat: R(x,y) = 0};
A1: R(3,2) = 0;
then [3,2] in A;
then reconsider A as non empty set;
deffunc p1(Real,Real) = 55*$1+84*$2+0;
deffunc p2(Real,Real) = 36*$1+55*$2+0;
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,2,55,84,0,36,55,0);
A2: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [3,2] by Def10;
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 Def10;
A7: m > 0 & n > 0 by Th89;
R(p1(m,n),p2(m,n)) = 0 by A5;
hence thesis by A6,A7;
end;
A8: N[a] from NAT_1:sch 2(A3,A4);
A9: rng f c= A
proof
let y be object;
assume y in rng f;
then ex k being object st k in dom f & f.k = y by FUNCT_1:def 3;
hence thesis by A8;
end;
f is one-to-one by Th92;
hence thesis by A2,A9,CARD_1:59;
end;
begin :: Problem 138
registration
cluster infinite natural-membered for set;
existence
proof
take NAT;
thus thesis;
end;
end;
theorem Th94:
i divides p implies i = 1 or i = -1 or i = p or i = -p
proof
assume
A1: i divides p;
per cases;
suppose i >= 0;
then i in NAT by INT_1:3;
hence thesis by A1,INT_2:def 4;
end;
suppose i < 0;
then -i in NAT by INT_1:3;
then -i = 1 or -i = p by A1,INT_2:10,def 4;
hence thesis;
end;
end;
:: Problem 138 a
theorem
{ [x,y] where x,y is Integer: 2*x|^3 + x*y - 7 = 0 } =
{ [1,5], [7,-97], [-1,-9], [-7,-99] }
proof
set A = { [x,y] where x,y is Integer: 2*x|^3 + x*y - 7 = 0 };
set B = { [1,5], [7,-97], [-1,-9], [-7,-99] };
thus A c= B
proof
let a be object;
assume a in A;
then consider x,y being Integer such that
A1: a = [x,y] and
A2: 2*x|^3 + x*y - 7 = 0;
A3: x|^3 = x*x*x by POLYEQ_5:2;
then x*(2*x*x+y) = 7 by A2;
then x divides 7;
then x = 1 or x = 7 or x = -1 or x = -7 by Th94,XPRIMES1:7;
hence thesis by A1,A2,A3,ENUMSET1:def 2;
end;
let a be object;
assume a in B;
then per cases by ENUMSET1:def 2;
suppose
A4: a = [1,5];
2*1|^3 + 1*5 - 7 = 0;
hence thesis by A4;
end;
suppose
A5: a = [7,-97];
7|^3 = 7*7*7 by POLYEQ_5:2;
then 2*7|^3 + 7*(-97) - 7 = 0;
hence thesis by A5;
end;
suppose
A6: a = [-1,-9];
(-1)|^3 = (-1)*(-1)*(-1) by POLYEQ_5:2;
then 2*(-1)|^3 + (-1)*(-9) - 7 = 0;
hence thesis by A6;
end;
suppose
A7: a = [-7,-99];
(-7)|^3 = (-7)*(-7)*(-7) by POLYEQ_5:2;
then 2*(-7)|^3 + (-7)*(-99) - 7 = 0;
hence thesis by A7;
end;
end;
theorem Th96:
for r being Complex st r <> 0 holds 2*(7/r)|^3 + 7/r*(r-98/r^2) - 7 = 0
proof
let r be Complex;
assume
A1: r <> 0;
A2: (7/r)|^3 = (7/r)*(7/r)*(7/r) by POLYEQ_5:2
.= 343*(r"*r"*r")
.= 343*((r*r)"*r") by XCMPLX_1:204
.= 343/(r*r*r) by XCMPLX_1:204;
A3: 7/r*r = 7 by A1,XCMPLX_1:87;
7/r*(98/r^2) = 686*(r"*(r*r)")
.= 686/(r*r*r) by XCMPLX_1:204;
hence thesis by A2,A3;
end;
theorem Th97:
n|^3 <= 98 implies n <= 4
proof
assume
A1: n|^3 <= 98;
A2: n|^3 = n*n*n by POLYEQ_5:2;
assume n > 4;
then
A3: n >= 4+1 by NAT_1:13;
then n*n >= 5*5 by XREAL_1:66;
then n*n*n >= 25*5 by A3,XREAL_1:66;
hence thesis by A1,A2,XXREAL_0:2;
end;
:: Problem 138 b
theorem
{ [x,y] where x,y is positive Rational: 2*x|^3 + x*y - 7 = 0 } is infinite
proof
deffunc R(Rational,Rational) = 2*$1|^3 + $1*$2 - 7;
set A = { [x,y] where x,y is positive Rational: R(x,y) = 0 };
deffunc p1(Nat) = 7/$1;
deffunc p2(Nat) = $1-98/$1^2;
deffunc F(Nat) = [ p1($1) , p2($1) ];
set D = NAT \ {0,1,2,3,4};
reconsider D as infinite natural-membered set;
consider f being ManySortedSet of D such that
A1: for d being Element of D holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = D 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 D by A4,PARTFUN1:def 2;
A6: not k in {0,1,2,3,4} by XBOOLE_0:def 5;
then
A7: k <> 0 by ENUMSET1:def 3;
then
A8: R(p1(k),p2(k)) = 0 by Th96;
now
assume
A9: p2(k) <= 0;
(k-98/k^2)*k^2 = k*k^2-98/k^2*k^2
.= k*k*k-98 by A7,XCMPLX_1:87;
then k*k*k-98+98 <= 0+98 by A9,XREAL_1:6;
then k|^3 <= 98 by POLYEQ_5:2;
then k <= 4 by Th97;
then k = 0 or ... or k = 4;
hence contradiction by A6,ENUMSET1:def 3;
end;
then F(k) in A by A7,A8;
hence thesis by A1,A5;
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 D by A10,PARTFUN1:def 2;
f.x1 = F(x1) & f.x2 = F(x2) by A1;
then p1(x1) = p1(x2) by A11,XTUPLE_0:1;
hence thesis by XCMPLX_1:201;
end;
hence thesis by A2,A3,CARD_1:59;
end;
begin :: Problem 139
:: Problem 139
theorem
{ [x,y] where x,y is positive Nat : (x-1)^2+(x+1)^2 = y^2+1 } is infinite
proof
deffunc R(Nat,Nat) = ($1-1)^2+($1+1)^2 - ($2^2+1);
set A = { [x,y] where x,y is positive Nat : R(x,y) = 0 };
A1: R(2,3) = 0;
then [2,3] in A;
then reconsider A as non empty set;
deffunc p1(Nat,Nat) = 3*$1+2*$2+0;
deffunc p2(Nat,Nat) = 4*$1+3*$2+0;
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(2,3,3,2,0,4,3,0);
A2: dom f = NAT by PARTFUN1:def 2;
defpred N[Nat] means f.$1 in A;
f.0 = [2,3] by Def10;
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;
reconsider m,n as Nat by A5;
A6: f.(a+1) = [p1(m,n),p2(m,n)] by Def10;
A7: m > 0 & n > 0 by Th89;
R(p1(m,n),p2(m,n)) = 0 by A5;
hence thesis by A6,A7;
end;
A8: N[a] from NAT_1:sch 2(A3,A4);
A9: rng f c= A
proof
let y be object;
assume y in rng f;
then ex k being object st k in dom f & f.k = y by FUNCT_1:def 3;
hence thesis by A8;
end;
A10: f is one-to-one by Th92;
defpred R[Nat,Nat] means ($1-1)^2+($1+1)^2 = $2^2+1;
set B = { [x,y] where x,y is positive Nat : R[x,y] };
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] & R(x,y) = 0;
hence thesis;
end;
let a be object;
assume a in B;
then consider x,y being positive Nat such that
A11: a = [x,y] and
A12: R[x,y];
R(x,y) = 0 by A12;
hence thesis by A11;
end;
hence thesis by A2,A9,A10,CARD_1:59;
end;
begin :: Problem 140
registration
let a be Rational, n be Nat;
cluster a |^ n -> rational;
coherence
proof
defpred P[Nat] means a|^$1 is rational;
A1: P[0] by NEWTON:4;
A2: P[k] implies P[k+1]
proof
a|^(k+1) = a|^k*a by NEWTON:6;
hence thesis;
end;
P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
registration
let a be Rational, i be Integer;
cluster a #Z i -> rational;
coherence
proof
per cases;
suppose i < 0;
then a #Z i = (a |^ |.i.|)" by PREPOWER:def 3;
hence thesis;
end;
suppose i >= 0;
then a #Z i = a |^ |.i.| by PREPOWER:def 3;
hence thesis;
end;
end;
end;
registration
let a be Rational, i be Integer;
cluster a to_power i -> rational;
coherence
proof
ex k being Integer st k = i & a to_power i = a #Z k by POWER:def 2;
hence thesis;
end;
end;
Lm57: 3 is non trivial by NAT_2:def 1;
theorem Th100:
n > 1 implies 3|^n - 3 to_power(1-n) - 2 > 0
proof
assume
A1: n > 1;
set a = 3 to_power n;
A2: 3 to_power(1-n) = 3 to_power 1 / 3 to_power n by POWER:29
.= 3 / a;
A3: a*3/a = 3 by XCMPLX_1:89;
A4: a*(a-3/a-2) = a*a-a*3/a-2*a
.= (a+1)*(a-3) by A3;
now
assume a-3/a-2 <= 0;
then a-3 <= 0 by A4;
then a-3+3 <= 0+3|^1 by XREAL_1:6;
hence contradiction by A1,Lm57,NAT_6:2;
end;
hence thesis by A2;
end;
theorem Th101:
n > 1 implies 3|^n + 3 to_power(1-n) - 4 > 0
proof
assume
A1: n > 1;
set a = 3 to_power n;
A2: 3 to_power(1-n) = 3 to_power 1 / 3 to_power n by POWER:29
.= 3 / a;
A3: a*3/a = 3 by XCMPLX_1:89;
A4: a*(a+3/a-4) = a*a+a*3/a-4*a
.= (a-1)*(a-3) by A3;
a > 3|^1 by A1,Lm57,NAT_6:2;
then
A5: a-1 > 3-1 by XREAL_1:9;
now
assume a+3/a-4 <= 0;
then a-3 <= 0 by A4,A5;
then a-3+3 <= 0+3|^1 by XREAL_1:6;
hence contradiction by A1,Lm57,NAT_6:2;
end;
hence thesis by A2;
end;
theorem Th102:
for x,y being Complex st
x = (3|^n-3 to_power(1-n)-2)/4 & y = (3|^n+3 to_power(1-n)-4)/8
holds x*(x+1) = 4*y*(y+1)
proof
let x,y be Complex;
set a = 3 to_power(1-n);
set b = 3|^n;
assume that
A1: x = (b-a-2)/4 and
A2: y = (b+a-4)/8;
b = 3 to_power n;
then a*b = 3 to_power (1-n+n) by POWER:27;
then
A3: 4*(a*b-3) = 0;
thus x*(x+1) = (b-a-2)*(b-a+2)/(4*4) by A1
.= (b+a-4)*((b+a+4)/(2*8)) by A3
.= 4*y*(y+1) by A2;
end;
theorem Th103:
m < n implies 3|^m - 3 to_power(1-m) < 3|^n - 3 to_power(1-n)
proof
assume
A1: m < n;
A2: 3|^m < 3|^n by A1,Lm57,NAT_6:2;
1-n < 1-m by A1,XREAL_1:15;
then 3 to_power(1-n) < 3 to_power(1-m) by POWER:39;
hence thesis by A2,XREAL_1:14;
end;
:: Problem 140 a
theorem
not ex x,y being positive Nat st x*(x+1) = 4*y*(y+1)
proof
given x,y being positive Nat such that
A1: x*(x+1) = 4*y*(y+1);
(2*(2*y+1))^2 - (2*x+1)^2 = (4*y-2*x+1)*(4*y+2*x+3);
then
A2: (4*y+2*x+3) divides 3 by A1;
0+3 < 4*y+2*x+3 by XREAL_1:8;
hence contradiction by A2,NAT_D:7;
end;
:: Problem 140 b
theorem
{ [x,y] where x,y is positive Rational: x*(x+1) = 4*y*(y+1) } is infinite
proof
deffunc R(Complex,Complex) = $1*($1+1) - 4*$2*($2+1);
set A = { [x,y] where x,y is positive Rational: R(x,y) = 0 };
deffunc p1(Nat) = (3|^$1-3 to_power(1-$1)-2)/4;
deffunc p2(Nat) = (3|^$1+3 to_power(1-$1)-4)/8;
deffunc F(Nat) = [ p1($1) , p2($1) ];
set D = NAT \ {0,1};
reconsider D as infinite natural-membered set;
consider f being ManySortedSet of D such that
A1: for d being Element of D holds f.d = F(d) from PBOOLE:sch 5;
A2: dom f = D 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 D by A4,PARTFUN1:def 2;
A6: not k in {0,1} by XBOOLE_0:def 5;
A7: now
assume k <= 1;
then k = 0 or ... or k = 1;
hence contradiction by A6,TARSKI:def 2;
end;
p1(k)*(p1(k)+1) = 4*p2(k)*(p2(k)+1) by Th102;
then
A8: R(p1(k),p2(k)) = 0;
A9: 3|^k-3 to_power(1-k)-2 > 0 by A7,Th100;
3|^k+3 to_power(1-k)-4 > 0 by A7,Th101;
then F(k) in A by A8,A9;
hence thesis by A1,A5;
end;
A10: f is one-to-one
proof
let x1,x2 be object such that
A11: x1 in dom f & x2 in dom f and
A12: f.x1 = f.x2;
reconsider x1,x2 as Element of D by A11,PARTFUN1:def 2;
f.x1 = F(x1) & f.x2 = F(x2) by A1;
then
A13: p1(x1) = p1(x2) by A12,XTUPLE_0:1;
now
assume x1 <> x2;
then x1 < x2 or x1 > x2 by XXREAL_0:1;
hence contradiction by A13,Th103;
end;
hence thesis;
end;
defpred R[Complex,Complex] means $1*($1+1) = 4*$2*($2+1);
set B = { [x,y] where x,y is positive Rational : R[x,y] };
A = B
proof
thus A c= B
proof
let a be object;
assume a in A;
then ex x,y being positive Rational st a = [x,y] & R(x,y) = 0;
hence thesis;
end;
let a be object;
assume a in B;
then consider x,y being positive Rational such that
A14: a = [x,y] and
A15: R[x,y];
R(x,y) = 0 by A15;
hence thesis by A14;
end;
hence thesis by A2,A3,A10,CARD_1:59;
end;
begin :: Problem 141
theorem
m <> 0 & p|^m divides a*b implies p divides a or p divides b
proof
assume that
A1: m <> 0 and
A2: p|^m divides a*b;
p divides p|^m by A1,NAT_3:3;
then p divides a*b by A2,INT_2:9;
hence thesis by INT_5:7;
end;
theorem Th107:
a,b are_coprime & p|^n divides a*b implies p|^n divides a or p|^n divides b
proof
per cases;
suppose a = 0 or b = 0;
hence thesis;
end;
suppose n = 0;
then p|^n = 1 by NEWTON:4;
hence thesis by INT_2:12;
end;
suppose that
A1: a <> 0 and
A2: b <> 0 and
A3: n <> 0;
assume
A4: a,b are_coprime & p|^n divides a*b &
not p|^n divides a & not p|^n divides b;
p divides p|^n by A3,NEWTON02:6;
then
A5: p divides a*b by A4,NAT_D:4;
A6: p > 1 by INT_2:def 4;
per cases;
suppose p divides a & p divides b;
then p divides 1 by A4,NAT_D:def 5;
hence contradiction by INT_2:27,def 4;
end;
suppose not p divides a & p divides b;
then p|-count a = 0 by A6,NAT_3:27;
then p |-count (a*b) = 0 + p |-count b by A1,A2,NAT_3:28;
then n <= p |-count b by A1,A2,A4,MOEBIUS2:40;
hence contradiction by A2,A4,MOEBIUS1:9;
end;
suppose p divides a & not p divides b;
then p|-count b = 0 by A6,NAT_3:27;
then p |-count (a*b) = 0 + p |-count a by A1,A2,NAT_3:28;
then n <= p |-count a by A1,A2,A4,MOEBIUS2:40;
hence contradiction by A1,A4,MOEBIUS1:9;
end;
suppose not p divides a & not p divides b;
then p|-count a = 0 & p|-count b = 0 by A6,NAT_3:27;
then p |-count (a*b) = 0+0 by A1,A2,NAT_3:28;
hence contradiction by A1,A2,A5,A6,NAT_3:27;
end;
end;
end;
:: Problem 141
theorem
n <> 0 implies not ex x,y being positive Nat st x*(x+1) = p|^(2*n)*y*(y+1)
proof
assume
A1: n <> 0;
given x,y being positive Nat such that
A2: x*(x+1) = p|^(2*n)*y*(y+1);
A3: x+0 < x+1 by XREAL_1:8;
A4: x,x+1 are_coprime;
p|^(2*n) divides p|^(2*n)*(y*(y+1));
then p|^(2*n) divides x or p|^(2*n) divides x+1 by A2,A4,Th107;
then x+0 >= p|^(2*n) or x+1 >= p|^(2*n) by NAT_D:7;
then x+1 >= p|^(2*n) by A3,XXREAL_0:2;
then
A5: 2*(x+1) >= 2*p|^(2*n) by XREAL_1:64;
A6: p|^(2*n) = p|^n|^2 by NEWTON:9;
A7: p|^n|^2 = (p|^n)^2 by NEWTON:81;
A8: (p|^n*(2*y+1)+(2*x+1)) * (p|^n*(2*y+1)-(2*x+1))
= (p|^n*p|^n*(2*y+1))*(2*y+1) - (4*p|^n|^2*y*(y+1)+1) by A2,A6
.= (p|^n)^2-1 by A7;
then
A9: p|^n*(2*y+1)-(2*x+1) >= 0;
A10: p|^(2*n)-1 = (p|^n*(2*y+1)+(2*x+1)) * (p|^n*(2*y+1)-(2*x+1))
by A6,A8,NEWTON:81;
now
assume
A11: p|^n*(2*y+1)-(2*x+1) < 1;
(p|^n*(2*y+1)-(2*x+1)) in NAT by A9,INT_1:3;
then p|^n*(2*y+1)-(2*x+1) = 0 by A11,NAT_1:14;
hence contradiction by A1,A10;
end;
then
A12: (p|^n*(2*y+1)-(2*x+1))*(p|^n*(2*y+1)+(2*x+1)) >= 1*(p|^n*(2*y+1)+(2*x+1))
by XREAL_1:64;
p|^n*(2*y+1)+(2*x+1) > 0+(2*x+1) by XREAL_1:6;
then p|^(2*n)-1 > 2*x+1 by A10,A12,XXREAL_0:2;
then p|^(2*n)-1+1 > 2*x+1+1 by XREAL_1:8;
then 1*p|^(2*n) > 2*p|^(2*n) by A5,XXREAL_0:2;
hence contradiction by XREAL_1:64;
end;
begin :: Problem 142
:: Problem 142
theorem
for k,x,y being Nat st x^2 - 2*y^2 = k
for t,u being Nat st t = x-2*y & u = x-y holds
t^2 - 2*u^2 = -k;