:: Elementary Number Theory Problems. Part {XVII}
:: by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received December 12, 2025
:: Copyright (c) 2025-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 4.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/4.0/.
environ
vocabularies NUMBERS, NAT_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_3, XCMPLX_0,
CARD_1, INT_1, NEWTON, ARYTM_1, SUBSET_1, XBOOLE_0, TARSKI, FINSET_1,
ABIAN, MEMBERED, REAL_1, INT_2, NUMBER03, SQUARE_1, ZFMISC_1, ORDINAL4,
NAT_LAT, RAT_1, FINSEQ_3, FINSEQ_1, CARD_3, VALUED_0, PARTFUN3, EUCLID_3,
ORDINAL2, FUNCT_7, VALUED_1, NUMBER06, FINSEQ_2, POWER, PRE_POLY,
NUMPOLY1, PEPIN, RVSUM_3, NUMBER02, EULER_1, NUMBER15, NUMBER17, FUNCT_2,
PREPOWER, PBOOLE, RFINSEQ2, CLASSES1, MATRIX_1, FOMODEL1, CAYLEY,
UNIALG_1, AFINSQ_1, FUNCOP_1, NUMERAL1, NAT_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, DOMAIN_1, ORDINAL1,
CARD_1, NUMBERS, ENUMSET1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1,
FUNCT_2, PBOOLE, FINSET_1, MEMBERED, VALUED_0, VALUED_1, XREAL_0,
FUNCOP_1, AFINSQ_1, AFINSQ_2, NAT_D, INT_1, INT_2,
XXREAL_0, CLASSES1, SQUARE_1, FINSEQ_1, PARTFUN3, FINSEQ_2, FINSEQ_3,
FINSEQ_4, AOFA_A00, RVSUM_1, RFINSEQ2, PREPOWER, POWER, NEWTON, ABIAN,
PEPIN, EULER_1, PRE_POLY, RAT_1, NEWTON04, NAT_LAT, NUMPOLY1, RVSUM_3,
NAT_3, NUMERAL1, CAYLEY, NUMBER02, NUMBER03, NUMBER06, NUMBER15;
constructors NAT_D, ABIAN, PEPIN, NUMBER02, NUMBER03, CLASSES1, PYTHTRIP,
RFINSEQ2, POWER, DOMAIN_1, EC_PF_2, NUMBER06, INT_7, CALCUL_2, GROUP_4,
PREPOWER, NEWTON04, EULER_1, RVSUM_3, FINSEQ_4, RVSUM_2, AOFA_A00,
NUMBER15, NUMPOLY1, CAYLEY, RELSET_1, AFINSQ_2, RVSUM_1,
SERIES_1, RFINSEQ, NAT_3, FIB_NUM2, RECDEF_1, ORDINAL5, INT_5,
WSIERP_1, POLYEQ_3, NUMERAL1, PARTFUN3, FUNCT_7,
RELAT_1, FUNCT_1, XTUPLE_0, FUNCT_4, FUNCOP_1, CARD_1, WELLORD2;
registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, VALUED_0, CARD_1, NEWTON, NEWTON02, NEWTON03,
ABIAN, NAT_6, JORDAN1D, WSIERP_1, FINSEQ_1, RVSUM_1, PRE_POLY, FUNCT_1,
RELAT_1, XBOOLE_0, SUBSET_1, RAT_1, BINOP_2, NUMBER02, NUMPOLY1,
VALUED_1, PARTFUN3, FINSEQ_9, SQUARE_1, POWER, NUMBER08, NUMBER09,
NEWTON04, COMPLEX3, FINSEQ_2, FOMODEL0, NAT_LAT, NUMBER03, RVSUM_3,
FINSEQ_4, NUMBER10, EUCLID_9, NUMBER15, NEWTON07, FUNCT_2, CAYLEY,
AFINSQ_1, AFINSQ_2, MEMBERED, FUNCOP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions MEMBERED, TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2,
WELLORD2, NUMBER02, NUMBER06, VALUED_0, SEQM_3, FINSET_1, PRE_POLY;
equalities SQUARE_1, FINSEQ_1, FINSEQ_2, XCMPLX_0, ORDINAL1, PEPIN, FINSEQ_4,
RVSUM_3, AOFA_A00, CAYLEY, AFINSQ_1;
expansions INT_1, INT_2, ABIAN, NUMBER03, TARSKI, CARD_1, RELAT_1;
theorems NEWTON, INT_1, INT_2, NAT_D, PEPIN, CARD_2, XREAL_1, XXREAL_0, NAT_1,
FUNCT_1, PARTFUN1, TARSKI, NAT_5, CARD_1, ABIAN, XCMPLX_1, BAGORD_2,
XBOOLE_0, NUMBER04, COMPLSP2, PRE_FF, WSIERP_1, POLYEQ_5, INT_4, NAT_3,
NUMBER07, NAT_6, FINSEQ_1, XPRIMES1, FINSEQ_5, INT_6, NUMBER02, FINSEQ_3,
ZFMISC_1, RELAT_1, FINSEQ_2, VALUED_0, FUNCT_2, RVSUM_1, ENUMSET1,
VALUED_1, RVSUM_2, XCMPLX_0, PREPOWER, RVSUM_3, FINSEQ_4, NUMBER03,
NEWTON02, NUMBER14, SEQM_3, FUNCOP_1, RFINSEQ, FINSEQ_9, NUMBER15,
NUMBER08, EULER_2, GR_CY_3, NUMBER09, EULER_1, POWER, ENTROPY1, FINSET_1,
POLYNOM3, EULRPART, CFUNCT_1, NOMIN_2, NUMPOLY1, NUMBER06, XPRIMES3,
SPRECT_1, XTUPLE_0, ORDINAL1, NAT_LAT, SUBSET_1, RFINSEQ2,
NUMERAL2, AFINSQ_1, AFINSQ_2,
NUMERAL1, NUMBER11, FUNCT_7, XPRIMES0, NUMBER16, WELLORD2;
schemes NAT_1, FUNCT_2, FUNCT_1, FINSEQ_2, XXREAL_2, PBOOLE, RELAT_1,
FRAENKEL, AFINSQ_1;
begin :: Preliminaries
Lm1: 2|^2 = 2*2 by POLYEQ_5:1;
Lm2: 2|^3 = 2*2*2 by POLYEQ_5:2;
Lm3: 2|^4 = 2*2*2*2 by POLYEQ_5:3;
Lm4: 2|^5 = 2*2*2*2*2 by NUMBER02:1;
Lm5: 2|^6 = 2*2*2*2*2*2 by NUMBER02:2;
Lm6: 2|^8 = 2*2*2*2*2*2*2*2 by NUMBER02:4;
Lm7: 2|^10 = 2*2*2*2*2*2*2*2*2*2 by NUMBER02:6;
Lm8: 2|^11 = 2*2*2*2*2*2*2*2*2*2*2 by NUMBER09:1;
Lm9: 2|^14 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2 by NUMBER09:4;
Lm10: 2|^18 = 2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 by NUMBER09:8;
Lm11: 2|^(8*4) = 2|^8|^4 by NEWTON:9;
Lm12: 256|^4 = 256*256*256*256 by POLYEQ_5:3;
reserve A for set;
reserve a,k,m,n for Nat;
reserve s for positive Nat;
reserve i,j for Integer;
reserve r for Real;
reserve c,c1,c2,c3,c4,c5,c6,c7,c8 for Complex;
registration
let A be finite set;
cluster Segm A -> finite;
coherence;
end;
theorem Th1:
for a,b,c,d being object holds dom <*a,b,c,d*> = {1,2,3,4}
proof
let a,b,c,d be object;
thus dom <*a,b,c,d*> = Seg len <*a,b,c,d*> by FINSEQ_1:def 3
.= {1,2,3,4} by FINSEQ_4:76,FINSEQ_3:2;
end;
theorem Th2:
for a,b,c,d,e being object holds dom <*a,b,c,d,e*> = {1,2,3,4,5}
proof
let a,b,c,d,e be object;
thus dom <*a,b,c,d,e*> = Seg len <*a,b,c,d,e*> by FINSEQ_1:def 3
.= {1,2,3,4,5} by FINSEQ_4:78,FINSEQ_3:3;
end;
theorem Th3:
for a being object, A being set st <*a*> is A-valued holds a in A
proof
let a be object, A be set;
assume
A1: <*a*> is A-valued;
A2: rng <*a*> = {a} by FINSEQ_1:38;
a in {a} by TARSKI:def 1;
hence thesis by A1,A2;
end;
registration
let s be positive Nat;
let f be s-element FinSequence;
cluster f|(s-1) -> (s-1)-element;
coherence
proof
A1: s-1 <= s by XREAL_1:147;
len f = s by CARD_1:def 7;
hence thesis by A1,FINSEQ_1:59;
end;
end;
registration
let f be non empty positive-yielding real-valued FinSequence;
cluster f.1 -> positive;
coherence
proof
1 in dom f by FINSEQ_5:6;
hence thesis by RVSUM_3:def 1;
end;
end;
theorem Th4:
for f being s-element complex-valued FinSequence holds
Sum(f|(s-1)) = Sum f - f.s
proof
let f be s-element complex-valued FinSequence;
A1: len f = s by CARD_1:def 7;
s-1 < s by XREAL_1:147;
then Sum (f|(s-1+1)) = Sum (f|(s-1)) + f.(s-1+1) by A1,POLYNOM3:20;
hence thesis by A1;
end;
theorem Th5:
for D being non empty set holds
5-tuples_on D =
the set of all <*d1,d2,d3,d4,d5*> where d1,d2,d3,d4,d5 is Element of D
proof
let D be non empty set;
set A =
the set of all <*d1,d2,d3,d4,d5*> where d1,d2,d3,d4,d5 is Element of D;
hereby
let x be object;
assume x in 5-tuples_on D;
then consider s being Element of D* such that
A1: x = s and
A2: len s = 5;
1 in Seg(5) & 2 in Seg(5) & 3 in Seg(5) & 4 in Seg(5) & 5 in Seg(5);
then 1 in dom s & 2 in dom s & 3 in dom s & 4 in dom s & 5 in dom s
by A2,FINSEQ_1:def 3;
then reconsider d19 = s.1, d29 = s.2, d39 = s.3, d49 = s.4, d59 = s.5
as Element of D by FINSEQ_2:11;
s = <*d19,d29,d39,d49,d59*> by A2,FINSEQ_4:78;
hence x in A by A1;
end;
let x be object;
assume x in A;
then consider d1,d2,d3,d4,d5 being Element of D such that
A3: x = <*d1,d2,d3,d4,d5*>;
A4: len <*d1,d2,d3,d4,d5*> = 5 by FINSEQ_4:78;
<*d1,d2,d3,d4,d5*> is Element of D* by FINSEQ_1:def 11;
hence x in 5-tuples_on D by A3,A4;
end;
theorem Th6:
for D being non empty set
for z being Tuple of 5,D
ex d1,d2,d3,d4,d5 being Element of D st z = <*d1,d2,d3,d4,d5*>
proof
let D be non empty set;
let z be Tuple of 5,D;
A1: z is Element of D* by FINSEQ_1:def 11;
len z = 5 by CARD_1:def 7;
then z in 5-tuples_on D by A1;
then
z in the set of all <*d1,d2,d3,d4,d5*> where d1,d2,d3,d4,d5 is Element of D
by Th5;
hence thesis;
end;
theorem Th7:
<*c*>^2 = <*c^2*>
proof
A1: len(<*c*>^2) = len <*c*> by NUMBER15:54
.= 1 by FINSEQ_1:39;
hence len(<*c*>^2) = len <*c^2*> by FINSEQ_1:39;
let k be Nat;
assume 1 <= k & k <= len(<*c*>^2);
then k = 1 by A1,XXREAL_0:1;
hence <*c^2*>.k = (<*c*>.k)^2
.= <*c*>^2.k by VALUED_1:11;
end;
theorem Th8:
<*c1,c2*>^2 = <*c1^2,c2^2*>
proof
<*c1*>^2 = <*c1^2*> & <*c2*>^2 = <*c2^2*> by Th7;
hence thesis by NUMBER15:59;
end;
theorem Th9:
<*c1,c2,c3*>^2 = <*c1^2,c2^2,c3^2*>
proof
A1: <*c1,c2*>^2 = <*c1^2,c2^2*> by Th8;
<*c3*>^2 = <*c3^2*> by Th7;
hence thesis by A1,NUMBER15:59;
end;
theorem Th10:
<*c1,c2,c3,c4*>^2 = <*c1^2,c2^2,c3^2,c4^2*>
proof
A1: <*c1,c2,c3*>^2 = <*c1^2,c2^2,c3^2*> by Th9;
<*c4*>^2 = <*c4^2*> by Th7;
hence thesis by A1,NUMBER15:59;
end;
theorem Th11:
<*c1,c2,c3,c4,c5*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2*>
proof
A1: <*c1,c2,c3*>^2 = <*c1^2,c2^2,c3^2*> by Th9;
<*c4,c5*>^2 = <*c4^2,c5^2*> by Th8;
hence thesis by A1,NUMBER15:59;
end;
theorem Th12:
<*c1,c2,c3,c4,c5,c6*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2,c6^2*>
proof
A1: <*c1,c2,c3,c4,c5*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2*> by Th11;
<*c6*>^2 = <*c6^2*> by Th7;
hence thesis by A1,NUMBER15:59;
end;
theorem Th13:
<*c1,c2,c3,c4,c5,c6,c7*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2,c6^2,c7^2*>
proof
A1: <*c1,c2,c3,c4,c5*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2*> by Th11;
<*c6,c7*>^2 = <*c6^2,c7^2*> by Th8;
hence thesis by A1,NUMBER15:59;
end;
theorem Th14:
<*c1,c2,c3,c4,c5,c6,c7,c8*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2,c6^2,c7^2,c8^2*>
proof
A1: <*c1,c2,c3,c4,c5*>^2 = <*c1^2,c2^2,c3^2,c4^2,c5^2*> by Th11;
<*c6,c7,c8*>^2 = <*c6^2,c7^2,c8^2*> by Th9;
hence thesis by A1,NUMBER15:59;
end;
theorem Th15:
<*c1,c2,c3,c4*>" = <*c1",c2",c3",c4"*>
proof
<*c4*>" = <*c4"*> by NUMBER15:63;
hence <*c1",c2",c3",c4"*> = <*c1,c2,c3*>"^<*c4*>" by NUMBER15:65
.= <*c1,c2,c3,c4*>" by NUMBER15:60;
end;
theorem Th16:
<*c1,c2,c3,c4,c5*>" = <*c1",c2",c3",c4",c5"*>
proof
<*c4,c5*>" = <*c4",c5"*> by NUMBER15:64;
hence <*c1",c2",c3",c4",c5"*> = <*c1,c2,c3*>"^<*c4,c5*>" by NUMBER15:65
.= <*c1,c2,c3,c4,c5*>" by NUMBER15:60;
end;
theorem Th17:
<*c1,c2,c3,c4,c5,c6*>" = <*c1",c2",c3",c4",c5",c6"*>
proof
<*c6*>" = <*c6"*> by NUMBER15:63;
hence <*c1",c2",c3",c4",c5",c6"*> = <*c1,c2,c3,c4,c5*>"^<*c6*>" by Th16
.= <*c1,c2,c3,c4,c5,c6*>" by NUMBER15:60;
end;
theorem Th18:
<*c1,c2,c3,c4,c5,c6,c7*>" = <*c1",c2",c3",c4",c5",c6",c7"*>
proof
<*c6,c7*>" = <*c6",c7"*> by NUMBER15:64;
hence <*c1",c2",c3",c4",c5",c6",c7"*> = <*c1,c2,c3,c4,c5*>"^<*c6,c7*>"
by Th16
.= <*c1,c2,c3,c4,c5,c6,c7*>" by NUMBER15:60;
end;
theorem Th19:
<*c1,c2,c3,c4,c5,c6,c7,c8*>" = <*c1",c2",c3",c4",c5",c6",c7",c8"*>
proof
<*c6,c7,c8*>" = <*c6",c7",c8"*> by NUMBER15:65;
hence <*c1",c2",c3",c4",c5",c6",c7",c8"*>
= <*c1,c2,c3,c4,c5*>"^<*c6,c7,c8*>" by Th16
.= <*c1,c2,c3,c4,c5,c6,c7,c8*>" by NUMBER15:60;
end;
theorem Th20:
Sum <*c1,c2,c3,c4*> = c1+c2+c3+c4
proof
thus Sum <*c1,c2,c3,c4*> = Sum <*c1,c2,c3*> + c4 by RVSUM_2:31
.= c1+c2+c3+c4 by RVSUM_2:35;
end;
theorem Th21:
Sum <*c1,c2,c3,c4,c5*> = c1+c2+c3+c4+c5
proof
Sum <*c1,c2,c3*> = c1+c2+c3 by RVSUM_2:35;
then c1+c2+c3+(c4+c5) = Sum <*c1,c2,c3*> + Sum <*c4,c5*> by RVSUM_2:34
.= Sum <*c1,c2,c3,c4,c5*> by RVSUM_2:32;
hence thesis;
end;
theorem Th22:
Sum <*c1,c2,c3,c4,c5,c6*> = c1+c2+c3+c4+c5+c6
proof
Sum <*c1,c2,c3,c4,c5*> = c1+c2+c3+c4+c5 by Th21;
hence c1+c2+c3+c4+c5+c6 = Sum <*c1,c2,c3,c4,c5*> + Sum <*c6*>
.= Sum <*c1,c2,c3,c4,c5,c6*> by RVSUM_2:32;
end;
theorem Th23:
Sum <*c1,c2,c3,c4,c5,c6,c7*> = c1+c2+c3+c4+c5+c6+c7
proof
Sum <*c1,c2,c3,c4,c5*> = c1+c2+c3+c4+c5 by Th21;
then c1+c2+c3+c4+c5+(c6+c7) = Sum <*c1,c2,c3,c4,c5*> + Sum <*c6,c7*>
by RVSUM_2:34
.= Sum <*c1,c2,c3,c4,c5,c6,c7*> by RVSUM_2:32;
hence thesis;
end;
theorem Th24:
Sum <*c1,c2,c3,c4,c5,c6,c7,c8*> = c1+c2+c3+c4+c5+c6+c7+c8
proof
Sum <*c1,c2,c3,c4,c5*> = c1+c2+c3+c4+c5 by Th21;
then c1+c2+c3+c4+c5+(c6+c7+c8) = Sum <*c1,c2,c3,c4,c5*> + Sum <*c6,c7,c8*>
by RVSUM_2:35
.= Sum <*c1,c2,c3,c4,c5,c6,c7,c8*> by RVSUM_2:32;
hence thesis;
end;
theorem Th25:
m > 1 implies ex n being positive Nat st m|^(m|^n) > r
proof
assume
A1: m > 1;
per cases;
suppose
A2: r > 1;
set L = log(m,r);
set n = [/ L \];
A3: L <= n by INT_1:def 7;
L > 0 by A1,A2,ENTROPY1:4;
then reconsider n as positive Nat by TARSKI:1;
take n;
A4: m to_power L <= m to_power n by A1,A3,PRE_FF:8;
A5: m to_power L = r by A1,A2,POWER:def 3;
m|^n < m|^(m|^n) by A1,NAT_3:2;
hence thesis by A4,A5,XXREAL_0:2;
end;
suppose
A6: r <= 1;
take 1;
A7: m|^m > m|^1 by A1,PEPIN:66;
r < m by A1,A6,XXREAL_0:2;
hence thesis by A7,XXREAL_0:2;
end;
end;
theorem Th26:
for n being non zero Integer
ex k being Nat,
j being odd Integer st n = j * 2|^k
proof
let n be non zero Integer;
per cases;
suppose n > 0;
then n in NAT by INT_1:3;
then consider k being Nat, j being odd Nat such that
A1: n = j * 2|^k by NAT_6:3;
take k,j;
thus thesis by A1;
end;
suppose n < 0;
then -n in NAT by INT_1:3;
then consider k being Nat, j being odd Nat such that
A2: -n = j * 2|^k by NAT_6:3;
take k,-j;
thus thesis by A2;
end;
end;
theorem Th27:
i,j are_congruent_mod j implies i,0 are_congruent_mod j
proof
j,0 are_congruent_mod j;
hence thesis by INT_1:15;
end;
theorem Th28:
for x,y,n being Nat st n > 0 & x >= y
holds x,y are_congruent_mod n iff ex k being Nat st x = k * n + y
proof
let x,y,n be Nat such that
A1: n > 0;
assume x >= y;
then
A2: x - y >= y - y by XREAL_1:9;
hereby
assume x,y are_congruent_mod n;
then consider k being Integer such that
A3: n * k = x - y;
k >= 0 or n <= 0 by A2,A3;
then k in NAT by A1,INT_1:3;
then reconsider k as Nat;
take k;
thus x = k * n + y by A3;
end;
thus thesis;
end;
theorem Th29:
m <= n &
i|^m,i|^(m+k) are_congruent_mod a implies i|^n,i|^(n+k) are_congruent_mod a
proof
assume m <= n;
then consider x being Nat such that
A1: m+x = n by NAT_1:10;
i|^m*i|^x = i|^(m+x) & i|^(m+k)*i|^x = i|^(m+k+x) by NEWTON:8;
hence thesis by A1,INT_4:11;
end;
theorem Th30:
3 divides 2|^(2*n) - 1
proof
4-1 divides 4|^n-1 by GR_CY_3:27;
hence thesis by Lm1,NEWTON:9;
end;
theorem Th31:
5 divides 2|^(4*n) - 1
proof
3*5+1,1 are_congruent_mod 5;
then 2|^4|^n,1|^n are_congruent_mod 5 by Lm3,GR_CY_3:34;
hence thesis by NEWTON:9;
end;
theorem Th32:
7 divides 2|^(6*n) - 1
proof
9*7+1,1 are_congruent_mod 7;
then 2|^6|^n,1|^n are_congruent_mod 7 by Lm5,GR_CY_3:34;
hence thesis by NEWTON:9;
end;
theorem Th33:
11 divides 2|^(10*n) - 1
proof
93*11+1,1 are_congruent_mod 11;
then 2|^10|^n,1|^n are_congruent_mod 11 by Lm7,GR_CY_3:34;
hence thesis by NEWTON:9;
end;
theorem Th34:
9 divides 2|^(6*n) - 1
proof
9*7+1,1 are_congruent_mod 9;
then 2|^6|^n,1|^n are_congruent_mod 9 by Lm5,GR_CY_3:34;
hence thesis by NEWTON:9;
end;
registration
let F be rational-valued FinSequence;
A1: F is FinSequence of RAT by FINSEQ_1:102;
cluster Sum F -> rational;
coherence
proof
defpred P[FinSequence of RAT] means Sum $1 is rational;
A2: P[<*>RAT];
A3: now
let s be FinSequence of RAT;
let m be Element of RAT;
assume P[s];
then reconsider p = Sum s as Rational;
Sum(s^<*m*>) = p+m by RVSUM_1:74;
hence P[s^<*m*>];
end;
for f being FinSequence of RAT holds P[f] from FINSEQ_2:sch 2(A2,A3);
hence thesis by A1;
end;
cluster Product F -> rational;
coherence
proof
defpred P[FinSequence of RAT] means Product $1 is rational;
A4: P[<*>RAT];
A5: now
let s be FinSequence of RAT;
let m be Element of RAT;
assume P[s];
then reconsider p = Product s as Rational;
Product(s^<*m*>) = p*m by RVSUM_1:96;
hence P[s^<*m*>];
end;
for f being FinSequence of RAT holds P[f] from FINSEQ_2:sch 2(A4,A5);
hence thesis by A1;
end;
end;
registration
let n be Nat;
let f be (n+1)-element FinSequence;
cluster Del(f,1) -> n-element;
coherence
proof
A1: len f = n+1 by CARD_1:def 7;
1 <= n+1 by NAT_1:11;
then 1 in dom f by A1,FINSEQ_3:25;
then ex m being Nat st len f = m + 1 & len Del(f,1) = m by FINSEQ_3:104;
hence thesis by A1;
end;
end;
registration
let D be set;
let f be D-valued FinSequence;
let n be Nat;
cluster Del(f,n) -> D-valued;
coherence
proof
A1: rng f c= D;
rng Del(f,n) c= rng f by FINSEQ_3:106;
then rng Del(f,n) c= D by A1;
hence thesis;
end;
end;
registration
let f be increasing real-valued FinSequence;
let n be Nat;
cluster Del(f,n) -> increasing;
coherence
proof
set d = Del(f,n);
per cases;
suppose
A1: n in dom f;
then consider m being Nat such that
A2: len f = m + 1 and
A3: len d = m by FINSEQ_3:104;
let i,j be Nat such that
A4: i in dom d and
A5: j in dom d and
A6: i < j;
A7: dom d c= dom f by WSIERP_1:39;
A8: i <= len d & j <= len d by A4,A5,FINSEQ_3:25;
A9: 1 <= j+1 by NAT_1:11;
per cases;
suppose
A10: j < n;
then
A11: f.j = d.j by FINSEQ_3:110;
i < n by A6,A10,XXREAL_0:2;
then f.i = d.i by FINSEQ_3:110;
hence thesis by A4,A5,A6,A7,A11,VALUED_0:def 13;
end;
suppose
A12: i >= n;
then j > n by A6,XXREAL_0:2;
then
A13: d.j = f.(j+1) by A1,A2,A3,A8,FINSEQ_3:111;
A14: d.i = f.(i+1) by A1,A2,A3,A8,A12,FINSEQ_3:111;
1 <= i+1 by NAT_1:11;
then
A15: i+1 in dom f by A2,A3,A8,FINSEQ_3:25,XREAL_1:6;
A16: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
i+1 < j+1 by A6,XREAL_1:6;
hence thesis by A13,A14,A15,A16,VALUED_0:def 13;
end;
suppose that
A17: i < n and
A18: j >= n;
A19: d.i = f.i by A17,FINSEQ_3:110;
A20: d.j = f.(j+1) by A1,A2,A3,A8,A18,FINSEQ_3:111;
A21: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
j+0 < j+1 by XREAL_1:6;
then i < j+1 by A6,XXREAL_0:2;
hence thesis by A4,A7,A19,A20,A21,VALUED_0:def 13;
end;
end;
suppose not n in dom f;
hence thesis by FINSEQ_3:104;
end;
end;
end;
registration
let f be decreasing real-valued FinSequence;
let n be Nat;
cluster Del(f,n) -> decreasing;
coherence
proof
set d = Del(f,n);
per cases;
suppose
A1: n in dom f;
then consider m being Nat such that
A2: len f = m + 1 and
A3: len d = m by FINSEQ_3:104;
let i,j be Nat such that
A4: i in dom d and
A5: j in dom d and
A6: i < j;
A7: dom d c= dom f by WSIERP_1:39;
A8: i <= len d & j <= len d by A4,A5,FINSEQ_3:25;
A9: 1 <= j+1 by NAT_1:11;
per cases;
suppose
A10: j < n;
then
A11: f.j = d.j by FINSEQ_3:110;
i < n by A6,A10,XXREAL_0:2;
then f.i = d.i by FINSEQ_3:110;
hence thesis by A4,A5,A6,A7,A11,VALUED_0:def 14;
end;
suppose
A12: i >= n;
then j > n by A6,XXREAL_0:2;
then
A13: d.j = f.(j+1) by A1,A2,A3,A8,FINSEQ_3:111;
A14: d.i = f.(i+1) by A1,A2,A3,A8,A12,FINSEQ_3:111;
1 <= i+1 by NAT_1:11;
then
A15: i+1 in dom f by A2,A3,A8,FINSEQ_3:25,XREAL_1:6;
A16: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
i+1 < j+1 by A6,XREAL_1:6;
hence thesis by A13,A14,A15,A16,VALUED_0:def 14;
end;
suppose that
A17: i < n and
A18: j >= n;
A19: d.i = f.i by A17,FINSEQ_3:110;
A20: d.j = f.(j+1) by A1,A2,A3,A8,A18,FINSEQ_3:111;
A21: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
j+0 < j+1 by XREAL_1:6;
then i < j+1 by A6,XXREAL_0:2;
hence thesis by A4,A7,A19,A20,A21,VALUED_0:def 14;
end;
end;
suppose not n in dom f;
hence thesis by FINSEQ_3:104;
end;
end;
end;
registration
let f be non-increasing real-valued FinSequence;
let n be Nat;
cluster Del(f,n) -> non-increasing;
coherence
proof
set d = Del(f,n);
per cases;
suppose
A1: n in dom f;
then consider m being Nat such that
A2: len f = m + 1 and
A3: len d = m by FINSEQ_3:104;
let i,j be Nat such that
A4: i in dom d and
A5: j in dom d and
A6: i <= j;
A7: dom d c= dom f by WSIERP_1:39;
A8: i <= len d & j <= len d by A4,A5,FINSEQ_3:25;
A9: 1 <= j+1 by NAT_1:11;
per cases;
suppose
A10: j < n;
then
A11: f.j = d.j by FINSEQ_3:110;
i < n by A6,A10,XXREAL_0:2;
then f.i = d.i by FINSEQ_3:110;
hence thesis by A4,A5,A6,A7,A11,VALUED_0:def 16;
end;
suppose
A12: i >= n;
then j >= n by A6,XXREAL_0:2;
then
A13: d.j = f.(j+1) by A1,A2,A3,A8,FINSEQ_3:111;
A14: d.i = f.(i+1) by A1,A2,A3,A8,A12,FINSEQ_3:111;
1 <= i+1 by NAT_1:11;
then
A15: i+1 in dom f by A2,A3,A8,FINSEQ_3:25,XREAL_1:6;
A16: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
i+1 <= j+1 by A6,XREAL_1:6;
hence thesis by A13,A14,A15,A16,VALUED_0:def 16;
end;
suppose that
A17: i < n and
A18: j >= n;
A19: d.i = f.i by A17,FINSEQ_3:110;
A20: d.j = f.(j+1) by A1,A2,A3,A8,A18,FINSEQ_3:111;
A21: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
j+0 < j+1 by XREAL_1:6;
then i < j+1 by A6,XXREAL_0:2;
hence thesis by A4,A7,A19,A20,A21,VALUED_0:def 16;
end;
end;
suppose not n in dom f;
hence thesis by FINSEQ_3:104;
end;
end;
end;
registration
let f be non-decreasing real-valued FinSequence;
let n be Nat;
cluster Del(f,n) -> non-decreasing;
coherence
proof
set d = Del(f,n);
per cases;
suppose
A1: n in dom f;
then consider m being Nat such that
A2: len f = m + 1 and
A3: len d = m by FINSEQ_3:104;
let i,j be Nat such that
A4: i in dom d and
A5: j in dom d and
A6: i <= j;
A7: dom d c= dom f by WSIERP_1:39;
A8: i <= len d & j <= len d by A4,A5,FINSEQ_3:25;
A9: 1 <= j+1 by NAT_1:11;
per cases;
suppose
A10: j < n;
then
A11: f.j = d.j by FINSEQ_3:110;
i < n by A6,A10,XXREAL_0:2;
then f.i = d.i by FINSEQ_3:110;
hence thesis by A4,A5,A6,A7,A11,VALUED_0:def 15;
end;
suppose
A12: i >= n;
then j >= n by A6,XXREAL_0:2;
then
A13: d.j = f.(j+1) by A1,A2,A3,A8,FINSEQ_3:111;
A14: d.i = f.(i+1) by A1,A2,A3,A8,A12,FINSEQ_3:111;
1 <= i+1 by NAT_1:11;
then
A15: i+1 in dom f by A2,A3,A8,FINSEQ_3:25,XREAL_1:6;
A16: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
i+1 <= j+1 by A6,XREAL_1:6;
hence thesis by A13,A14,A15,A16,VALUED_0:def 15;
end;
suppose that
A17: i < n and
A18: j >= n;
A19: d.i = f.i by A17,FINSEQ_3:110;
A20: d.j = f.(j+1) by A1,A2,A3,A8,A18,FINSEQ_3:111;
A21: j+1 in dom f by A2,A3,A8,A9,FINSEQ_3:25,XREAL_1:6;
j+0 < j+1 by XREAL_1:6;
then i < j+1 by A6,XXREAL_0:2;
hence thesis by A4,A7,A19,A20,A21,VALUED_0:def 15;
end;
end;
suppose not n in dom f;
hence thesis by FINSEQ_3:104;
end;
end;
end;
registration
let m,n be Nat;
let f be positive-yielding n-element FinSequence;
cluster Del(f,m) -> positive-yielding;
coherence
proof
rng Del(f,m) c= rng f by FINSEQ_3:106;
hence thesis by NUMBER08:39;
end;
end;
theorem
for f,g being ext-real-valued FinSequence holds
f^g is decreasing implies f is decreasing & g is decreasing
proof
let f,g be ext-real-valued FinSequence;
assume
A1: f^g is decreasing;
A2: dom f c= dom(f^g) by FINSEQ_1:26;
thus f is decreasing
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 14;
end;
thus g is decreasing
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 14;
end;
end;
theorem
for f,g being ext-real-valued FinSequence holds
f^g is non-increasing implies f is non-increasing & g is non-increasing
proof
let f,g be ext-real-valued FinSequence;
assume
A1: f^g is non-increasing;
A2: dom f c= dom(f^g) by FINSEQ_1:26;
thus f is non-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 16;
end;
thus g is non-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:6;
hence thesis by A1,A6,A7,A10,A11,VALUED_0:def 16;
end;
end;
theorem Th37:
for f,g being ext-real-valued FinSequence holds
f^g is non-decreasing implies f is non-decreasing & g is non-decreasing
proof
let f,g be ext-real-valued FinSequence;
assume
A1: f^g is non-decreasing;
A2: dom f c= dom(f^g) by FINSEQ_1:26;
thus f is non-decreasing
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 15;
end;
thus g is non-decreasing
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:6;
hence thesis by A1,A6,A7,A10,A11,VALUED_0:def 15;
end;
end;
theorem Th38:
for p,q being increasing real-valued FinSequence st p.len(p) < q.1 holds
p ^ q is increasing
proof
let p,q be increasing real-valued FinSequence;
set pq = p ^ q;
per cases;
suppose p is empty or q is empty;
hence thesis by FINSEQ_1:34;
end;
suppose that
A1: p is non empty and
A2: q is non empty;
assume
A3: p.len(p) < q.1;
let e1,e2 be Nat;
assume that
A4: e1 in dom pq and
A5: e2 in dom pq and
A6: e1 < e2;
per cases by A4,A5,FINSEQ_1:25;
suppose
A7: e1 in dom p & e2 in dom p; then
pq.e1 = p.e1 & pq.e2 = p.e2 by FINSEQ_1:def 7;
hence pq.e1 < pq.e2 by A6,A7,VALUED_0:def 13;
end;
suppose
A8: e1 in dom p & ex n be Nat st n in dom q &
e2 = len p + n;
then consider n0 be Nat such that
A9: n0 in dom q and
A10: e2 = len p + n0;
A11: pq.e1 = p.e1 & pq.e2 = q.n0 by A8,A10,FINSEQ_1:def 7;
rng q <> {} by A2; then
A12: 1 in dom q by FINSEQ_3:32;
1 <= n0 by A9,FINSEQ_3:25;
then 1 = n0 or 1 < n0 by XXREAL_0:1; then
A13: q.1 <= q.n0 by A9,A12,VALUED_0:def 13;
rng p <> {} by A1;
then 1 in dom p by FINSEQ_3:32;
then 1 <= len p by FINSEQ_3:25; then
A14: len p in dom p by FINSEQ_3:25;
e1 <= len p by A8,FINSEQ_3:25;
then e1 < len p or e1 = len p by XXREAL_0:1;
then p.e1 <= p.len p by A14,A8,VALUED_0:def 13;
then p.e1 < q.1 by A3,XXREAL_0:2;
hence pq.e1 < pq.e2 by A11,A13,XXREAL_0:2;
end;
suppose
A15: (ex n be Nat st n in dom q & e1 = len p + n) & e2 in dom p;
then consider n0 be Nat such that
n0 in dom q and
A16: e1 = len p + n0;
A17: len p <= e1 by A16,NAT_1:11;
e2 in Seg len p by A15,FINSEQ_1:def 3;
then e2 <= len p by FINSEQ_1:1;
hence pq.e1 < pq.e2 by A6,A17,XXREAL_0:2;
end;
suppose
A18: (ex n be Nat st n in dom q & e1 = len p + n) &
(ex n be Nat st n in dom q & e2 = len p + n);
then consider n1 be Nat such that
A19: n1 in dom q and
A20: e1 = len p + n1;
consider n2 be Nat such that
A21: n2 in dom q and
A22: e2 = len p + n2 by A18;
A23: len p + n1 - len p < len p + n2 - len p by A6,A20,A22,XREAL_1:14;
q.n1 = pq.e1 & q.n2 = pq.e2 by A19,A20,A21,A22,FINSEQ_1:def 7;
hence pq.e1 < pq.e2 by A23,A19,A21,VALUED_0:def 13;
end;
end;
end;
theorem Th39:
for r1,r2 being Real st r1 < r2 holds <*r1,r2*> is increasing
proof
let r1,r2 be Real;
A1: <*r1*>.1 = r1 & <*r2*>.1 = r2;
len <*r1*> = 1 & len <*r2*> = 1 by FINSEQ_1:39;
hence thesis by A1,Th38;
end;
theorem Th40:
for r1,r2,r3 being Real st r1 < r2 < r3 holds <*r1,r2,r3*> is increasing
proof
let r1,r2,r3 be Real;
assume r1 < r2;
then
A1: <*r1,r2*> is increasing by Th39;
A2: len <*r1,r2*> = 2 by FINSEQ_1:44;
<*r1,r2*>.2 = r2 & <*r3*>.1 = r3;
hence thesis by A1,A2,Th38;
end;
theorem Th41:
for r1,r2,r3,r4 being Real st r1 < r2 < r3 < r4 holds
<*r1,r2,r3,r4*> is increasing
proof
let r1,r2,r3,r4 be Real;
assume r1 < r2 < r3;
then
A1: <*r1,r2,r3*> is increasing by Th40;
A2: len <*r1,r2,r3*> = 3 by CARD_1:def 7;
<*r1,r2,r3*>.3 = r3 & <*r4*>.1 = r4;
hence thesis by A1,A2,Th38;
end;
registration
let n be Nat;
cluster increasing positive-yielding n-element
for natural-valued FinSequence;
existence
proof
take idseq n;
thus thesis;
end;
end;
theorem Th42:
for f being positive-yielding real-valued FinSequence st len f >= 2
for k being Nat st k in dom f holds f.k < Sum(f)
proof
defpred P[Nat] means $1 >= 2 implies
for f being positive-yielding real-valued FinSequence st
len f = $1 for k being Nat st k in dom f holds f.k < Sum(f);
A1: P[0];
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A3: P[i];
assume
A4: 2 <= i+1;
let f be positive-yielding real-valued FinSequence such that
A5: len f = i+1;
let k be Nat such that
A6: k in dom f;
A7: 1 <= k by A6,FINSEQ_3:25;
set g = f|i;
A8: f = g^<*f.(i+1)*> by A5,RFINSEQ:7;
then
A9: Sum f = Sum g + f.(i+1) by RVSUM_1:74;
A10: len g = i by A5,NAT_1:11,FINSEQ_1:59;
A11: k <= i+1 by A5,A6,FINSEQ_3:25;
per cases by A4,NAT_1:8;
suppose
A12: 2 = i+1;
f is FinSequence of REAL by FINSEQ_1:106;
then f is Element of 2-tuples_on REAL by A5,A12,FINSEQ_2:92;
then consider a,b being object such that
A13: a in REAL & b in REAL and
A14: f = <*a,b*> by FINSEQ_2:137;
reconsider a,b as Real by A13;
A15: k = 1 or ... or k = 2 by A7,A11,A12;
A16: 1 in dom f & 2 in dom f by A5,A12,FINSEQ_3:25;
f.1 = a & f.2 = b by A14;
then 0+a < a+b & 0+b < a+b by A16,RVSUM_3:def 1,XREAL_1:6;
hence f.k < Sum(f) by A14,A15,RVSUM_1:77;
end;
suppose
A17: 2 <= i;
per cases by A11,NAT_1:8;
suppose
A18: k <= i;
then
A19: k in dom g by A7,A10,FINSEQ_3:25;
1 <= i+1 by NAT_1:11;
then i+1 in dom f by A5,FINSEQ_3:25;
then
A20: Sum g + f.(i+1) > Sum g + 0 by XREAL_1:6,RVSUM_3:def 1;
g.k = f.k by A7,A8,A10,A18,FINSEQ_1:64;
hence f.k < Sum(f) by A3,A9,A10,A17,A19,A20,XXREAL_0:2;
end;
suppose
A21: k = i+1;
g is non empty by A10,A17;
then Sum g + f.(i+1) > 0 + f.(i+1) by XREAL_1:6;
hence f.k < Sum(f) by A9,A21;
end;
end;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th43:
n|->(c") = (n|->c)"
proof
set f = n|->(c");
set g = n|->c;
set h = g";
A1: len f = n;
thus len f = len h by CARD_1:def 7;
let k be Nat;
assume 1 <= k & k <= len f;
then
A2: k in dom f;
hence f.k = c" by A1,FINSEQ_9:20
.= (g.k)" by A1,A2,FINSEQ_9:20
.= h.k by VALUED_1:10;
end;
registration
let a be non positive Real;
let b be Real;
cluster <*a,b*> -> non positive-yielding;
coherence
proof
<*a,b*>.1 = a;
hence thesis;
end;
end;
registration
let a be Real;
let b be non positive Real;
cluster <*a,b*> -> non positive-yielding;
coherence
proof
set f = <*a,b*>;
dom f = { 1,2 } by FINSEQ_1:92;
then
A1: 2 in dom f by TARSKI:def 2;
f.2 = b;
hence thesis by A1;
end;
end;
registration
let a be non positive Real;
let b,c be Real;
cluster <*a,b,c*> -> non positive-yielding;
coherence
proof
<*a,b,c*>.1 = a;
hence thesis;
end;
end;
registration
let b be non positive Real;
let a,c be Real;
cluster <*a,b,c*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c*>;
A1: 2 in dom f by FINSEQ_1:81;
f.2 = b;
hence thesis by A1;
end;
end;
registration
let c be non positive Real;
let a,b be Real;
cluster <*a,b,c*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c*>;
A1: 3 in dom f by FINSEQ_1:81;
f.3 = c;
hence thesis by A1;
end;
end;
registration
let a be non positive Real;
let b,c,d be Real;
cluster <*a,b,c,d*> -> non positive-yielding;
coherence
proof
<*a,b,c,d*>.1 = a;
hence thesis;
end;
end;
registration
let b be non positive Real;
let a,c,d be Real;
cluster <*a,b,c,d*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d*>;
dom f = {1,2,3,4} by Th1;
then
A1: 2 in dom f by ENUMSET1:def 2;
f.2 = b;
hence thesis by A1;
end;
end;
registration
let c be non positive Real;
let a,b,d be Real;
cluster <*a,b,c,d*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d*>;
dom f = {1,2,3,4} by Th1;
then
A1: 3 in dom f by ENUMSET1:def 2;
f.3 = c;
hence thesis by A1;
end;
end;
registration
let d be non positive Real;
let a,b,c be Real;
cluster <*a,b,c,d*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d*>;
dom f = {1,2,3,4} by Th1;
then
A1: 4 in dom f by ENUMSET1:def 2;
f.4 = d;
hence thesis by A1;
end;
end;
registration
let a be non positive Real;
let b,c,d,e be Real;
cluster <*a,b,c,d,e*> -> non positive-yielding;
coherence
proof
<*a,b,c,d,e*>.1 = a;
hence thesis;
end;
end;
registration
let b be non positive Real;
let a,c,d,e be Real;
cluster <*a,b,c,d,e*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d,e*>;
dom f = {1,2,3,4,5} by Th2;
then
A1: 2 in dom f by ENUMSET1:def 3;
f.2 = b;
hence thesis by A1;
end;
end;
registration
let c be non positive Real;
let a,b,d,e be Real;
cluster <*a,b,c,d,e*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d,e*>;
dom f = {1,2,3,4,5} by Th2;
then
A1: 3 in dom f by ENUMSET1:def 3;
f.3 = c;
hence thesis by A1;
end;
end;
registration
let d be non positive Real;
let a,b,c,e be Real;
cluster <*a,b,c,d,e*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d,e*>;
dom f = {1,2,3,4,5} by Th2;
then
A1: 4 in dom f by ENUMSET1:def 3;
f.4 = d;
hence thesis by A1;
end;
end;
registration
let e be non positive Real;
let a,b,c,d be Real;
cluster <*a,b,c,d,e*> -> non positive-yielding;
coherence
proof
set f = <*a,b,c,d,e*>;
dom f = {1,2,3,4,5} by Th2;
then
A1: 5 in dom f by ENUMSET1:def 3;
f.5 = e;
hence thesis by A1;
end;
end;
theorem
for f being positive natural-valued 1-element FinSequence
ex a being positive Nat st f = <*a*>
proof
let f be positive natural-valued 1-element FinSequence;
f is FinSequence of NAT by FINSEQ_1:103;
then consider a being Element of NAT such that
A1: f = <*a*> by FINSEQ_2:97;
reconsider a as positive Nat by A1;
take a;
thus thesis by A1;
end;
theorem Th45:
for f being positive natural-valued 2-element FinSequence
ex a,b being positive Nat st f = <*a,b*>
proof
let f be positive natural-valued 2-element FinSequence;
f is FinSequence of NAT by FINSEQ_1:103;
then consider a,b being Element of NAT such that
A1: f = <*a,b*> by FINSEQ_2:100;
reconsider a,b as positive Nat by A1;
take a,b;
thus thesis by A1;
end;
theorem
for f being increasing positive natural-valued 2-element FinSequence
ex a,b being positive Nat st f = <*a,b*> & a < b
proof
let f be increasing positive natural-valued 2-element FinSequence;
consider a,b being positive Nat such that
A1: f = <*a,b*> by Th45;
take a,b;
thus f = <*a,b*> by A1;
A2: f.1 = a & f.2 = b by A1;
A3: dom f = {1,2} by A1,FINSEQ_1:92;
1 in {1,2} & 2 in {1,2} by TARSKI:def 2;
hence thesis by A2,A3,VALUED_0:def 13;
end;
theorem Th47:
for f being positive natural-valued 3-element FinSequence
ex a,b,c being positive Nat st f = <*a,b,c*>
proof
let f be positive natural-valued 3-element FinSequence;
f is FinSequence of NAT by FINSEQ_1:103;
then consider a,b,c being Element of NAT such that
A1: f = <*a,b,c*> by FINSEQ_2:103;
reconsider a,b,c as positive Nat by A1;
take a,b,c;
thus thesis by A1;
end;
theorem Th48:
for f being increasing positive natural-valued 3-element FinSequence
ex a,b,c being positive Nat st f = <*a,b,c*> & a < b < c
proof
let f be increasing positive natural-valued 3-element FinSequence;
consider a,b,c being positive Nat such that
A1: f = <*a,b,c*> by Th47;
take a,b,c;
thus f = <*a,b,c*> by A1;
A2: f.1 = a & f.2 = b & f.3 = c by A1;
A3: dom f = {1,2,3} by A1,NOMIN_2:4;
1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} by ENUMSET1:def 1;
hence thesis by A2,A3,VALUED_0:def 13;
end;
theorem Th49:
for f,g being complex-valued Function st c(#)f = c(#)g & c <> 0 holds f = g
proof
let f,g be complex-valued Function such that
A1: c(#)f = c(#)g;
assume c <> 0;
then
A2: 1/c*c = 1 by XCMPLX_1:106;
(1/c*c)(#)f = (1/c)(#)(c(#)f) & (1/c*c)(#)g = (1/c)(#)(c(#)g)
by CFUNCT_1:22;
then 1(#)f = 1(#)g by A1,A2;
hence thesis;
end;
theorem Th50:
for f,g being complex-valued Function holds (f(#)g)" = f"(#)g"
proof
let f,g be complex-valued Function;
A1: dom((f(#)g)") = dom(f(#)g) by VALUED_1:def 7;
A2: dom(f(#)g) = dom f /\ dom g by VALUED_1:def 4;
dom(f") = dom(f) & dom(g") = dom(g) by VALUED_1:def 7;
hence
A3: dom((f(#)g)") = dom(f"(#)g") by A1,A2,VALUED_1:def 4;
let x be object;
assume
A4: x in dom((f(#)g)");
then
A5: (f(#)g).x = f.x*g.x by VALUED_1:def 4;
A6: f".x = (f.x)" & g".x = (g.x)" by VALUED_1:10;
thus ((f(#)g)").x = ((f(#)g).x)" by A4,VALUED_1:def 7
.= (f.x)"*(g.x)" by A5,XCMPLX_1:204
.= (f"(#)g").x by A3,A4,A6,VALUED_1:def 4;
end;
theorem Th51:
for f,g being complex-valued Function holds
(c1(#)f)(#)(c2(#)g) = (c1*c2)(#)(f(#)g)
proof
let f,g be complex-valued Function;
A1: (c2*c1)(#)f = c2(#)(c1(#)f) by CFUNCT_1:22;
thus (c1*c2)(#)(f(#)g) = (c1*c2)(#)f(#)g by CFUNCT_1:17
.= c2(#)((c1(#)f)(#)g) by A1,CFUNCT_1:17
.= (c1(#)f)(#)(c2(#)g) by CFUNCT_1:17;
end;
theorem Th52:
for f1,f2,g1,g2,h1,h2 being complex-valued FinSequence
st len f1 = len g1 = len h1 holds
(f1^f2) (#) (g1^g2) (#) (h1^h2) = (f1(#)g1(#)h1) ^ (f2(#)g2(#)h2)
proof
let f1,f2,g1,g2,h1,h2 be complex-valued FinSequence such that
A1: len f1 = len g1 and
A2: len g1 = len h1;
A3: (f1^f2)(#)(g1^g2) = (f1(#)g1)^(f2(#)g2) by A1,EULRPART:8;
len(f1(#)g1) = min(len f1,len g1) by INT_6:3;
hence thesis by A1,A2,A3,EULRPART:8;
end;
theorem Th53:
for n being Nat, e being object holds Segm(n+1) --> e = <%e%>^(Segm n --> e)
proof
let n be Nat, e be object;
set p = Segm n --> e, q = Segm(n+1) --> e;
A1: dom q = len <%e%> + len p by AFINSQ_1:33;
A2: for k being Nat st k in dom <%e%> holds q.k=<%e%>.k
proof
let k be Nat such that A3: k in dom<%e%>;
k in {0} by CARD_1:49,AFINSQ_1:def 4,A3;
then k = 0;
hence q.k = <%e%>.k by FUNCOP_1:7,NAT_1:44;
end;
for k being Nat st k in dom p holds q.(len <%e%> + k) = p.k
proof
let k be Nat;
assume A4: k in dom p;
then A5: k+1 < Segm (n+1) by XREAL_1:8,NAT_1:44;
thus p.k = e by A4,FUNCOP_1:7
.= q.(k+1) by A5,NAT_1:44,FUNCOP_1:7
.= q.(len <%e%> + k) by AFINSQ_1:34;
end;
hence thesis by A1,A2,AFINSQ_1:def 3;
end;
begin :: Problem 37
theorem Th54:
for n,b being Nat st n>0 & b>1 holds digits(n*b,b)=<%0%>^digits(n,b)
proof
let n,b be Nat;
assume A1: n>0 & b>1;
set d=digits(n,b);
reconsider d0=<%0%>^d as XFinSequence of NAT;
A2: len d >= 1 by A1,NUMERAL1:4;
then reconsider ld1=len d - 1 as Nat;
A3: len d >= len <%0%> by A2,AFINSQ_1:34;
A4: len d0 = len d+len <%0%> by AFINSQ_1:def 3
.= len d + 1 by AFINSQ_1:def 4;
then A5: len d < len d0 by NAT_1:13;
value(d,b)=n by A1,NUMERAL1:5;
then consider d9 being XFinSequence of NAT such that
A6: (dom d9 = dom d &
for i being Nat st i in dom d9 holds d9.i = (d.i)*(b|^i))
& n = Sum d9 by NUMERAL1:def 1;
deffunc A() = len d9;
deffunc F(Nat) = b*d9.$1;
consider d1 being XFinSequence such that
A7: len d1=A() &
for n being Nat st n in A() holds d1.n=F(n) from AFINSQ_1:sch 2;
rng d1 c= NAT
proof
let o be object;
assume o in rng d1;
then consider k being object such that
A8: k in dom d1 & d1.k = o by FUNCT_1:def 3;
reconsider k as Nat by A8;
d1.k=b*d9.k by A8,A7;
hence o in NAT by A8,ORDINAL1:def 12;
end;
then reconsider d1 as XFinSequence of NAT by RELAT_1:def 19;
for o being object st o in dom d1 holds d1.o = b*(d9.o) by A7;
then
A9: Sum d1 = b * Sum d9 by A7,NUMERAL2:18;
reconsider d10=<%0%>^d1 as XFinSequence of NAT;
A10: Sum d10=Sum <%0%> + Sum d1 by AFINSQ_2:55
.= 0 + n*b by AFINSQ_2:53,A6,A9
.= n*b;
A11: dom d10 = len <%0%> + len d by A6,A7,AFINSQ_1:17
.= dom d0 by AFINSQ_1:17;
now
let i be Nat;
assume i in dom d0;
then per cases by AFINSQ_1:20;
suppose
A12: i in dom <%0%>;
then i in 1 by AFINSQ_1:33;
then A13: i = 0 by CARD_1:49;
thus d10.i=<%0%>.i by A12,AFINSQ_1:def 3
.=d0.i*1 by A12,AFINSQ_1:def 3
.=(d0.i)*(b|^i) by NEWTON:4,A13;
end;
suppose ex k being Nat st k in dom d & i=len <%0%> + k;
then consider k being Nat such that
A14: k in dom d & i=len <%0%> + k;
thus d10.i = d1.k by A14,AFINSQ_1:def 3,A6,A7
.= F(k) by A14,A6,A7
.= b*((d.k)*(b|^k)) by A6,A14
.= (d.k)*(b*(b|^k))
.= (d.k)*(b|^(k+1)) by NEWTON:6
.= (d.k)*(b|^i) by A14,AFINSQ_1:34
.= (d0.i)*(b|^i) by A14,AFINSQ_1:def 3;
end;
end;
then A15: value(d0,b)=n*b by A10,A11,NUMERAL1:def 1;
d0.(len(d0)-1) = d.(len d - len <%0%>) by AFINSQ_1:19,A3,A5,A4
.= d.ld1 by AFINSQ_1:34;
then A16: d0.(len(d0)-1) <> 0 by A1,NUMERAL1:def 2;
now
let i be Nat;
assume i in dom d0;
then d0.i in rng d0 by FUNCT_1:3;
then d0.i in rng <%0%> \/ rng d by AFINSQ_1:26;
then per cases by XBOOLE_0:def 3;
suppose d0.i in rng <%0%>;
then d0.i in {0} by AFINSQ_1:33;
hence 0 <= d0.i & d0.i < b by A1;
end;
suppose d0.i in rng d;
then consider o being object such that
A17: o in dom d & d0.i=d.o by FUNCT_1:def 3;
thus 0 <= d0.i & d0.i < b by A17,A1,NUMERAL1:def 2;
end;
end;
hence thesis by A15,A16,A1,NUMERAL1:def 2;
end;
theorem Th55:
for n,b being Nat st n>0 & b>1
for i being Nat holds digits(n*(b|^i),b)=(i-->0)^digits(n,b)
proof
let n,b be Nat;
assume A1: n>0 & b>1;
defpred P[Nat] means digits(n*(b|^$1),b)=($1-->0)^digits(n,b);
digits(n*(b|^0),b) = digits(n*1,b) by NEWTON:4
.= {}^digits(n,b)
.= (0-->0)^digits(n,b);
then A2: P[0];
A3:
now
let i be Nat;
assume A4: P[i];
digits(n*(b|^(i+1)),b) = digits(n*(b*(b|^i)),b) by NEWTON:6
.= digits((n*(b|^i))*b,b)
.= <%0%>^digits(n*(b|^i),b)
by A1,Th54
.= (<%0%>^(Segm i-->0))^digits(n,b)
by A4,AFINSQ_1:27
.= (Segm (i+1)-->0)^digits(n,b) by Th53;
hence P[i+1];
end;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
for s being Nat ex n being Nat st Sum digits(n,10) = s & s divides n
proof
let s be Nat;
per cases;
suppose A1: s=0;
take n=0;
digits(n,10)=<%0%> by NUMERAL1:def 2;
hence Sum digits(n,10) = s by A1,AFINSQ_2:53;
thus s divides n by A1;
end;
suppose A2: s>0;
set a=2 |-count s;
set b=5 |-count s;
A3: 2|^a divides s & 5|^b divides s by A2,NAT_3:def 7;
A4: 2|^a, 5|^b are_coprime by WSIERP_1:11,EULER_1:2,PEPIN:59;
then consider t being Nat such that
A5: s=((2|^a)*(5|^b))*t by NAT_D:def 3,A3,PEPIN:4;
A6: t divides s by A5;
A7: t<>0 by A5,A2;
then A8: Euler t <> 0;
deffunc L()=s*(Euler t)+1;
defpred P[Nat,object] means
((ex l being Nat st 1 <= l & l <= s & $1=l*(Euler t)) & $2=1)
or
((not ex l being Nat st 1 <= l & l <= s & $1=l*(Euler t)) & $2=0);
A9: for k being Nat st k in L() ex x being object st P[k,x]
proof
let k be Nat such that k in L();
per cases;
suppose A10: ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
take x=1;
thus thesis by A10;
end;
suppose A11: not ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
take x=0;
thus thesis by A11;
end;
end;
consider d being XFinSequence such that
A12: dom d = L() &
for k being Nat st k in L() holds P[k,d.k]
from AFINSQ_1:sch 1(A9);
rng d c= NAT
proof
let o be object;
assume o in rng d;
then consider k being object such that
A13: k in dom d & o=d.k by FUNCT_1:def 3;
reconsider k as Nat by A13;
per cases;
suppose ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
then d.k=1 by A13,A12;
hence thesis by A13;
end;
suppose not ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
then d.k=0 by A13,A12;
hence thesis by A13;
end;
end;
then reconsider d as XFinSequence of NAT by RELAT_1:def 19;
A14: s >= 0+1 by A2,NAT_1:13;
then 1*Euler t < s*(Euler t)+1 by NAT_1:13,XREAL_1:64;
then A15: 1*Euler t in Segm L() by NAT_1:44;
then A16: d.(1*Euler t)=1 by A14,A12;
set o=value(d,10);
consider e being XFinSequence of NAT such that
A17: (dom e = dom d &
for i being Nat st i in dom e holds e.i = (d.i)*(10|^i)) &
value(d,10) = Sum e by NUMERAL1:def 1;
e.(Euler t)=1*(10|^(Euler t)) by A17,A12,A15,A16;
then A18: o > 0 by A17,A12,A15,AFINSQ_2:61;
take n=10|^(a+b)*o;
s*Euler t < s*(Euler t)+1 by NAT_1:13;
then s*Euler t in Segm L() by NAT_1:44;
then
A19: d.((len d)-1) <> 0 by A12,A14;
now
let i be Nat;
assume i in dom d;
then per cases by A12;
suppose
(ex l being Nat st 1 <= l & l <= s & i=l*(Euler t)) & d.i=1;
hence d.i<10;
end;
suppose
(not ex l being Nat st 1 <= l & l <= s & i=l*(Euler t)) & d.i=0;
hence d.i<10;
end;
end;
then A20: digits(o,10)=d by NUMBER11:5,A12,A19;
rng d c= {0,1}
proof
let o be object;
assume o in rng d;
then consider k being object such that
A21: k in dom d & o=d.k by FUNCT_1:def 3;
reconsider k as Nat by A21;
per cases;
suppose ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
then d.k=1 by A21,A12;
hence thesis by A21,TARSKI:def 2;
end;
suppose not ex l being Nat st 1 <= l & l <= s & k=l*(Euler t);
then d.k=0 by A21,A12;
hence thesis by A21,TARSKI:def 2;
end;
end;
then A22: Sum d = 1*card(d"{1}) by AFINSQ_2:68;
deffunc G(Nat)=($1+1)*Euler t;
consider f being XFinSequence such that
A23: len f = s &
for k being Nat st k in s holds f.k=G(k) from AFINSQ_1:sch 2;
A24: rng f = d"{1}
proof
thus rng f c= d"{1}
proof
let o be object;
assume o in rng f;
then consider u being object such that
A25: u in dom f & o=f.u by FUNCT_1:def 3;
reconsider u as Nat by A25;
A26: 0+1<=u+1 by XREAL_1:6;
u in Segm s by A25,A23;
then u < s by NAT_1:44;
then A27: u+1 <= s by NAT_1:13;
then (u+1)*Euler t < L() by NAT_1:13,XREAL_1:64;
then A28: (u+1)*Euler t in Segm L() by NAT_1:44;
then d.((u+1)*Euler t)=1 by A26,A27,A12;
then d.((u+1)*Euler t) in {1} by TARSKI:def 1;
then (u+1)*Euler t in d"{1} by A12,A28,FUNCT_1:def 7;
hence o in d"{1} by A23,A25;
end;
let o be object;
assume o in d"{1};
then o in dom d & d.o in {1} by FUNCT_1:def 7;
then consider l being Nat such that
A29: 1 <= l & l <= s & o=l*Euler t by A12;
A30: l-'1+1=l-1+1 by A29,XREAL_1:233;
then l-'1 < s by A29,NAT_1:13;
then A31: l-'1 in Segm s by NAT_1:44;
then o=f.(l-'1) by A29,A23,A30;
hence o in rng f by A23,A31,FUNCT_1:3;
end;
f is one-to-one
proof
let x1,x2 be object;
assume A32: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then reconsider X1=x1,X2=x2 as Nat;
f.X1=(X1+1)*Euler t & f.X2=(X2+1)*Euler t by A32,A23;
then X1+1=X2+1 by XCMPLX_1:5,A8,A32;
hence x1 = x2;
end;
then s,d"{1} are_equipotent by A23,A24,WELLORD2:def 4;
then A33: card s = card(d"{1}) by CARD_1:5;
digits(n,10)=((a+b)-->0)^digits(o,10) by Th55,A18;
hence Sum digits(n,10) = Sum ((a+b)-->0) + Sum digits(o,10)
by AFINSQ_2:55
.= (a+b)*0+s by AFINSQ_2:58,A20,A22,A33
.= s;
10 = 5*2; then
A34: 2|^a divides 10|^a by NEWTON02:15,INT_1:def 3;
a+0<=a+b by XREAL_1:7; then
10|^a divides 10|^(a+b) by NEWTON:89; then
A35: 2|^a divides 10|^(a+b) by A34,INT_2:9;
10 = 5*2; then
A36: 5|^b divides 10|^b by NEWTON02:15,INT_1:def 3;
0+b<=a+b by XREAL_1:7; then
10|^b divides 10|^(a+b) by NEWTON:89; then
5|^b divides 10|^(a+b) by A36,INT_2:9;
then A37: (2|^a)*(5|^b) divides 10|^(a+b) by A35,A4,PEPIN:4;
t divides o
proof
per cases by NAT_1:23;
suppose t=0;
hence thesis by A5,A2;
end;
suppose t=1;
hence thesis by NAT_D:6;
end;
suppose t>=1+1;
then A38: t > 1 by NAT_1:13;
A39: 2,t are_coprime
proof
assume not thesis;
then A40: 2 gcd t <> 1;
2 gcd t divides 2 & 2 gcd t divides t by INT_2:21;
then 2 divides t by A40,INT_2:28;
then consider t2 being Nat such that
A41: t=2*t2 by NAT_D:def 3;
s = (2|^a)*2*(5|^b)*t2 by A5,A41
.= 2|^(a+1)*(5|^b)*t2 by NEWTON:6
.= 2|^(a+1)*((5|^b)*t2);
then 2|^(a+1) divides s;
hence contradiction by A2,NAT_3:def 7;
end;
5,t are_coprime
proof
assume not thesis;
then A42: 5 gcd t <> 1;
5 gcd t divides 5 & 5 gcd t divides t by INT_2:21;
then 5 divides t by A42,PEPIN:59;
then consider t5 being Nat such that
A43: t=5*t5 by NAT_D:def 3;
s = (5|^b)*5*(2|^a)*t5 by A5,A43
.= 5|^(b+1)*(2|^a)*t5 by NEWTON:6
.= 5|^(b+1)*((2|^a)*t5);
then 5|^(b+1) divides s;
hence contradiction by A2,NAT_3:def 7;
end;
then A44: 2*5,t are_coprime by INT_2:26,A39;
now
let i be Nat;
assume A45: i in dom e;
per cases;
suppose ex l being Nat st 1 <= l & l <= s & i=l*(Euler t);
then consider l being Nat such that
A46: 1 <= l & l <= s & i=l*(Euler t);
d.i = 1 by A45,A12,A17,A46;
then e.i = 1*(10|^(l*Euler t)) by A46,A17,A45
.= (10|^(Euler t))|^l by NEWTON:9;
then e.i mod t = ((10|^(Euler t)) mod t)|^l mod t by EULER_2:22
.= (1 |^ l) mod t by A44,A38,EULER_2:18
.= 1 by A38,NAT_D:14;
hence d.i = e.i mod t by A45,A12,A17,A46;
end;
suppose A47: not ex l being Nat st 1 <= l & l <= s & i=l*(Euler t);
then d.i = 0 by A45,A12,A17;
then e.i = 0*(10|^i) by A17,A45;
hence d.i = e.i mod t by A47,A45,A12,A17;
end;
end;
then Sum e mod t = s mod t by A22,A33,NUMERAL2:17,A17
.= 0 by A6;
hence t divides o by A17,A7,PEPIN:6;
end;
end;
hence s divides n by NAT_3:1,A37,A5;
end;
end;
begin :: Problem 101
theorem
for a,b being set holds Replace(<%a%>,0,b) = <%b%>
proof
let a,b be set;
A1: len Replace(<%a%>,0,b) = len <%a%> by FUNCT_7:30
.= 1 by AFINSQ_1:34;
0 in Segm 1 by NAT_1:44;
then 0 in dom <%a%> by AFINSQ_1:33;
then Replace(<%a%>,0,b).0=b by FUNCT_7:31;
hence Replace(<%a%>,0,b) = <%b%> by A1,AFINSQ_1:34;
end;
theorem
for a,b,c being set holds Replace(<%a,b%>,0,c) = <%c,b%>
proof
let a,b,c be set;
A1: len Replace(<%a,b%>,0,c) = len <%a,b%> by FUNCT_7:30
.= 2 by AFINSQ_1:38;
0 in Segm 2 by NAT_1:44;
then 0 in dom <%a,b%> by AFINSQ_1:38;
then
A2: Replace(<%a,b%>,0,c).0=c by FUNCT_7:31;
Replace(<%a,b%>,0,c).1=<%a,b%>.1 by FUNCT_7:32 .= b;
hence Replace(<%a,b%>,0,c) = <%c,b%> by A2,A1,AFINSQ_1:38;
end;
theorem
for a,b,c being set holds Replace(<%a,b%>,1,c) = <%a,c%>
proof
let a,b,c be set;
A1: len Replace(<%a,b%>,1,c) = len <%a,b%> by FUNCT_7:30
.= 2 by AFINSQ_1:38;
1 in Segm 2 by NAT_1:44;
then 1 in dom <%a,b%> by AFINSQ_1:38;
then
A2: Replace(<%a,b%>,1,c).1=c by FUNCT_7:31;
Replace(<%a,b%>,1,c).0=<%a,b%>.0 by FUNCT_7:32 .= a;
hence Replace(<%a,b%>,1,c) = <%a,c%> by A2,A1,AFINSQ_1:38;
end;
theorem Th60:
for a,b,c,d being set holds Replace(<%a,b,c%>,0,d) = <%d,b,c%>
proof
let a,b,c,d be set;
A1: len Replace(<%a,b,c%>,0,d) = len <%a,b,c%> by FUNCT_7:30
.= 3 by AFINSQ_1:39;
0 in Segm 3 by NAT_1:44;
then 0 in dom <%a,b,c%> by AFINSQ_1:39;
then
A2: Replace(<%a,b,c%>,0,d).0=d by FUNCT_7:31;
A3: Replace(<%a,b,c%>,0,d).1=<%a,b,c%>.1 by FUNCT_7:32 .= b;
Replace(<%a,b,c%>,0,d).2=<%a,b,c%>.2 by FUNCT_7:32 .= c;
hence Replace(<%a,b,c%>,0,d) = <%d,b,c%> by A2,A3,A1,AFINSQ_1:39;
end;
theorem
for a,b,c,d being set holds Replace(<%a,b,c%>,1,d) = <%a,d,c%>
proof
let a,b,c,d be set;
A1: len Replace(<%a,b,c%>,1,d) = len <%a,b,c%> by FUNCT_7:30
.= 3 by AFINSQ_1:39;
1 in Segm 3 by NAT_1:44;
then 1 in dom <%a,b,c%> by AFINSQ_1:39;
then
A2: Replace(<%a,b,c%>,1,d).1=d by FUNCT_7:31;
A3: Replace(<%a,b,c%>,1,d).0=<%a,b,c%>.0 by FUNCT_7:32 .= a;
Replace(<%a,b,c%>,1,d).2=<%a,b,c%>.2 by FUNCT_7:32 .= c;
hence Replace(<%a,b,c%>,1,d) = <%a,d,c%> by A2,A3,A1,AFINSQ_1:39;
end;
theorem Th62:
for a,b,c,d being set holds Replace(<%a,b,c%>,2,d) = <%a,b,d%>
proof
let a,b,c,d be set;
A1: len Replace(<%a,b,c%>,2,d) = len <%a,b,c%> by FUNCT_7:30
.= 3 by AFINSQ_1:39;
2 in Segm 3 by NAT_1:44;
then 2 in dom <%a,b,c%> by AFINSQ_1:39;
then
A2: Replace(<%a,b,c%>,2,d).2=d by FUNCT_7:31;
A3: Replace(<%a,b,c%>,2,d).0=<%a,b,c%>.0 by FUNCT_7:32 .= a;
Replace(<%a,b,c%>,2,d).1=<%a,b,c%>.1 by FUNCT_7:32 .= b;
hence Replace(<%a,b,c%>,2,d) = <%a,b,d%> by A2,A3,A1,AFINSQ_1:39;
end;
theorem Th63:
digits(201,10) = <%1,0,2%>
proof
set d=<%1,0,2%>;
set e=<%1*10|^0,0*10|^1,2*10|^2%>;
A1: Sum e = Sum (<%1*10|^0,0*10|^1%>)+Sum(<%2*10|^2%>) by AFINSQ_2:55
.= ((1*10|^0)+(0*10|^1))+Sum(<%2*10|^2%>) by AFINSQ_2:54
.= 1*1 + 0*(10|^1) + 2*(10|^2) by AFINSQ_2:53
.= 1 + 2*(10*10) by POLYEQ_5:1
.= 201;
A2: dom d = 3 by AFINSQ_1:39 .= dom e by AFINSQ_1:39;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence e.i=(d.i)*10|^i;
end;
then A3: value(d,10)=201 by A1,A2,NUMERAL1:def 1;
len(d) - 1 = 3-1 by AFINSQ_1:39;
then A4: d.(len(d)-1) <> 0;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence 0 <= d.i & d.i < 10;
end;
hence thesis by A3,A4,NUMERAL1:def 2;
end;
theorem Th64:
digits(202,10) = <%2,0,2%>
proof
set d=<%2,0,2%>;
set e=<%2*10|^0,0*10|^1,2*10|^2%>;
A1: Sum e = Sum (<%2*10|^0,0*10|^1%>)+Sum(<%2*10|^2%>) by AFINSQ_2:55
.= ((2*10|^0)+(0*10|^1))+Sum(<%2*10|^2%>) by AFINSQ_2:54
.= ((2*10|^0)+(0*10|^1))+(2*10|^2) by AFINSQ_2:53
.= 2*1 + 0*(10|^1) + 2*(10|^2) by NEWTON:4
.= 2 + 2*(10*10) by POLYEQ_5:1
.= 202;
A2: dom d = 3 by AFINSQ_1:39 .= dom e by AFINSQ_1:39;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence e.i=(d.i)*10|^i;
end;
then A3: value(d,10)=202 by A1,A2,NUMERAL1:def 1;
len(d) - 1 = 3-1 by AFINSQ_1:39;
then A4: d.(len(d)-1) <> 0;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence 0 <= d.i & d.i < 10;
end;
hence thesis by A3,A4,NUMERAL1:def 2;
end;
theorem Th65:
digits(203,10) = <%3,0,2%>
proof
set d=<%3,0,2%>;
set e=<%3*10|^0,0*10|^1,2*10|^2%>;
A1: Sum e = Sum (<%3*10|^0,0*10|^1%>)+Sum(<%2*10|^2%>) by AFINSQ_2:55
.= ((3*10|^0)+(0*10|^1))+Sum(<%2*10|^2%>) by AFINSQ_2:54
.= ((3*10|^0)+(0*10|^1))+(2*10|^2) by AFINSQ_2:53
.= 3*1 + 0*(10|^1) + 2*(10|^2) by NEWTON:4
.= 3 + 2*(10*10) by POLYEQ_5:1
.= 203;
A2: dom d = 3 by AFINSQ_1:39 .= dom e by AFINSQ_1:39;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence e.i=(d.i)*10|^i;
end;
then A3: value(d,10)=203 by A1,A2,NUMERAL1:def 1;
len(d) - 1 = 3-1 by AFINSQ_1:39;
then A4: d.(len(d)-1) <> 0;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence 0 <= d.i & d.i < 10;
end;
hence thesis by A3,A4,NUMERAL1:def 2;
end;
theorem Th66:
digits(205,10) = <%5,0,2%>
proof
set d=<%5,0,2%>;
set e=<%5*10|^0,0*10|^1,2*10|^2%>;
A1: Sum e = Sum (<%5*10|^0,0*10|^1%>)+Sum(<%2*10|^2%>) by AFINSQ_2:55
.= ((5*10|^0)+(0*10|^1))+Sum(<%2*10|^2%>) by AFINSQ_2:54
.= ((5*10|^0)+(0*10|^1))+(2*10|^2) by AFINSQ_2:53
.= 5*1 + 0*(10|^1) + 2*(10|^2) by NEWTON:4
.= 5 + 2*(10*10) by POLYEQ_5:1
.= 205;
A2: dom d = 3 by AFINSQ_1:39 .= dom e by AFINSQ_1:39;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence e.i=(d.i)*10|^i;
end;
then A3: value(d,10)=205 by A1,A2,NUMERAL1:def 1;
len(d) - 1 = 3-1 by AFINSQ_1:39;
then A4: d.(len(d)-1) <> 0;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence 0 <= d.i & d.i < 10;
end;
hence thesis by A3,A4,NUMERAL1:def 2;
end;
theorem Th67:
digits(206,10) = <%6,0,2%>
proof
set d=<%6,0,2%>;
set e=<%6*10|^0,0*10|^1,2*10|^2%>;
A1: Sum e = Sum (<%6*10|^0,0*10|^1%>)+Sum(<%2*10|^2%>) by AFINSQ_2:55
.= ((6*10|^0)+(0*10|^1))+Sum(<%2*10|^2%>) by AFINSQ_2:54
.= ((6*10|^0)+(0*10|^1))+(2*10|^2) by AFINSQ_2:53
.= 6*1 + 0*(10|^1) + 2*(10|^2) by NEWTON:4
.= 6 + 2*(10*10) by POLYEQ_5:1
.= 206;
A2: dom d = 3 by AFINSQ_1:39 .= dom e by AFINSQ_1:39;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence e.i=(d.i)*10|^i;
end;
then A3: value(d,10)=206 by A1,A2,NUMERAL1:def 1;
len(d) - 1 = 3-1 by AFINSQ_1:39;
then A4: d.(len(d)-1) <> 0;
now
let i be Nat;
assume i in dom d;
then i in {0,1,2} by CARD_1:51,AFINSQ_1:39;
then i = 0 or i = 1 or i = 2 by ENUMSET1:def 1;
hence 0 <= d.i & d.i < 10;
end;
hence thesis by A3,A4,NUMERAL1:def 2;
end;
theorem
for i,j being Element of NAT st 0 <= j <= 9
holds value(Replace(digits(200,10),i,j),10) is not prime
proof
let i,j be Element of NAT;
assume A1: 0 <= j <= 9;
then A2: j=0 or ... or j=9;
A3: len Replace(digits(200,10),i,j) = len digits(200,10) by FUNCT_7:30;
A4: now
let a being Nat;
assume A5: a in dom Replace(digits(200,10),i,j);
per cases;
suppose a<>i;
then Replace(digits(200,10),i,j).a=digits(200,10).a by FUNCT_7:32;
hence Replace(digits(200,10),i,j).a<10 by A5,A3,NUMERAL1:def 2;
end;
suppose a=i;
then Replace(digits(200,10),i,j).a<=9 by A1,A3,A5,FUNCT_7:31;
hence Replace(digits(200,10),i,j).a<10 by XXREAL_0:2;
end;
end;
per cases;
suppose i in dom digits(200,10);
then i in 3 by AFINSQ_1:39,NUMBER11:360;
then per cases by CARD_1:51,ENUMSET1:def 1;
suppose A6: i=0;
per cases by A2;
suppose j=0;
then Replace(digits(200,10),i,j)=<%0,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by NUMBER11:360,NUMERAL1:def 2,XPRIMES0:200;
end;
suppose j=1;
then Replace(digits(200,10),i,j)=<%1,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by Th63,NUMERAL1:def 2,XPRIMES0:201;
end;
suppose j=2;
then Replace(digits(200,10),i,j)=<%2,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by Th64,NUMERAL1:def 2,XPRIMES0:202;
end;
suppose j=3;
then Replace(digits(200,10),i,j)=<%3,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by Th65,NUMERAL1:def 2,XPRIMES0:203;
end;
suppose j=4;
then Replace(digits(200,10),i,j)=<%4,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by NUMBER11:239,NUMERAL1:def 2,XPRIMES0:204;
end;
suppose j=5;
then Replace(digits(200,10),i,j)=<%5,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by Th66,NUMERAL1:def 2,XPRIMES0:205;
end;
suppose j=6;
then Replace(digits(200,10),i,j)=<%6,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by Th67,NUMERAL1:def 2,XPRIMES0:206;
end;
suppose j=7;
then Replace(digits(200,10),i,j)=<%7,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by NUMBER11:937,NUMERAL1:def 2,XPRIMES0:207;
end;
suppose j=8;
then Replace(digits(200,10),i,j)=<%8,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by NUMBER11:127,NUMERAL1:def 2,XPRIMES0:208;
end;
suppose j=9;
then Replace(digits(200,10),i,j)=<%9,0,2%> by A6,Th60,NUMBER11:360;
hence thesis by NUMBER11:89,NUMERAL1:def 2,XPRIMES0:209;
end;
end;
suppose A7: i=1;
then
i<>len Replace(digits(200,10),i,j)-1 by A3,NUMBER11:360,AFINSQ_1:39;
then Replace(digits(200,10),i,j).(len(Replace(digits(200,10),i,j))-1)
= digits(200,10).(len(digits(200,10))-1) by A3,FUNCT_7:32
.= digits(200,10).(3-1) by NUMBER11:360,AFINSQ_1:39
.= 2 by NUMBER11:360;
then
A8: digits(value(Replace(digits(200,10),i,j),10),10)=
Replace(digits(200,10),i,j) by NUMBER11:5,360,A3,A4;
digits(2,10)=<%2%> by NUMBER11:3;
then len digits(200,10)=3 & len digits(2,10)=1
by NUMBER11:360,AFINSQ_1:34,39;
then
A9: value(Replace(digits(200,10),i,j),10) > 2 by A3,A8,NUMBER11:12;
Replace(digits(200,10),i,j).0=digits(200,10).0 by FUNCT_7:32,A7
.= 0 by NUMBER11:360;
then 2 divides value(Replace(digits(200,10),i,j),10)
by A8,INT_2:12,NUMERAL1:8;
hence thesis by A9;
end;
suppose A10: i=2;
then i=3-1;
then A11: i = len(Replace(digits(200,10),i,j))-1
by A3,NUMBER11:360,AFINSQ_1:39;
i in Segm 3 by A10,NAT_1:44;
then A12: i in dom digits(200,10) by NUMBER11:360,AFINSQ_1:39;
per cases;
suppose j<>0;
then
Replace(digits(200,10),i,j).(len(Replace(digits(200,10),i,j))-1)<>0
by A11,A12,FUNCT_7:31;
then
A13: digits(value(Replace(digits(200,10),i,j),10),10)=
Replace(digits(200,10),i,j) by NUMBER11:5,360,A3,A4;
digits(2,10)=<%2%> by NUMBER11:3;
then len digits(200,10)=3 & len digits(2,10)=1
by NUMBER11:360,AFINSQ_1:34,39;
then
A14: value(Replace(digits(200,10),i,j),10) > 2 by A3,A13,NUMBER11:12;
Replace(digits(200,10),i,j).0=digits(200,10).0 by FUNCT_7:32,A10
.= 0 by NUMBER11:360;
then 2 divides value(Replace(digits(200,10),i,j),10)
by A13,INT_2:12,NUMERAL1:8;
hence thesis by A14;
end;
suppose j=0;
then value(Replace(digits(200,10),i,j),10) =
value(<%0,0,0%>,10) by A10,Th62,NUMBER11:360
.= value(<%0,0%>,10) + value(<%0%>,10)*10|^(len <%0,0%>)
by NUMBER16:1
.= value(<%0,0%>,10) + 0*10|^(len <%0,0%>) by NUMBER11:2
.= value(<%0%>,10) + value(<%0%>,10)*10|^(len(<%0%>))
by NUMBER16:1
.= value(<%0%>,10) + 0*10|^(len(<%0%>)) by NUMBER11:2
.= 0 by NUMBER11:2;
hence thesis;
end;
end;
end;
suppose not i in dom digits(200,10);
then Replace(digits(200,10),i,j) = digits(200,10) by FUNCT_7:def 3;
hence thesis by XPRIMES0:200,NUMERAL1:def 2;
end;
end;
begin :: Problem 115
::$N A consequence of Euler's theorem
theorem Th69:
for a,n,x,y being Nat st a,n are_coprime & a <> 0 & n <> 0 &
x,y are_congruent_mod Euler(n) holds a|^x,a|^y are_congruent_mod n
proof
let a,n,x,y be Nat;
set e = Euler(n);
assume that
A1: a,n are_coprime and
A2: a <> 0 and
A3: n <> 0 and
A4: x,y are_congruent_mod e;
A5: y,x are_congruent_mod e by A4,INT_1:14;
n >= 1+0 by A3,NAT_1:13;
then per cases by XXREAL_0:1;
suppose n = 1;
hence thesis by INT_1:13;
end;
suppose
A6: n > 1;
then
A7: 1 mod n = 1 by NAT_D:24;
A8: (a|^e) mod n = 1 by A1,A2,A6,EULER_2:18;
per cases;
suppose x >= y;
then consider k being Nat such that
A9: x = k * e + y by A3,A4,Th28;
A10: a|^(k*e) = a|^e|^k by NEWTON:9;
A11: a|^y,a|^y are_congruent_mod n by INT_1:11;
a|^e|^k, 1|^k are_congruent_mod n by A3,A7,A8,GR_CY_3:34,NAT_D:64;
then a|^(k*e)*a|^y, 1*a|^y are_congruent_mod n by A10,A11,INT_1:18;
hence a|^x,a|^y are_congruent_mod n by A9,NEWTON:8;
end;
suppose x < y;
then consider k being Nat such that
A12: y = k * e + x by A3,A5,Th28;
A13: a|^(k*e+x) = a|^(k*e) * a|^x by NEWTON:8;
A14: a|^(k*e) = a|^e|^k by NEWTON:9;
A15: a|^x,a|^x are_congruent_mod n by INT_1:11;
a|^e|^k, 1|^k are_congruent_mod n by A3,A7,A8,GR_CY_3:34,NAT_D:64;
then a|^(k*e)*a|^x, 1*a|^x are_congruent_mod n by A14,A15,INT_1:18;
hence a|^x,a|^y are_congruent_mod n by A12,A13,INT_1:14;
end;
end;
end;
theorem Th70:
for a being Nat
for k being Integer st k <> 1
ex n being positive Nat st a < 2|^(2|^n)+k & 2|^(2|^n)+k is composite
proof
let a be Nat;
let k be Integer such that
A1: k <> 1;
k-1 <> 0 by A1;
then consider s being Nat, h being odd Integer such that
A2: k-1 = h*2|^s by Th26;
consider m being positive Nat such that
A3: 2|^(2|^m) > a-k by Th25;
consider L being positive Nat such that
A4: 2|^(2|^L) > -k+2 by Th25;
set l = max(max(s,m),L);
reconsider l as positive Nat;
set p = 2|^(2|^l)+k;
m <= l by XXREAL_0:25,30;
then
A5: 2|^m <= 2|^l by PREPOWER:93;
A6: 2|^(2|^L)+k > -k+2+k by A4,XREAL_1:8;
2|^L <= 2|^l by PREPOWER:93,XXREAL_0:25;
then
A7: 2|^(2|^L)+k <= 2|^(2|^l)+k by XREAL_1:6,PREPOWER:93;
then
A8: p > 2 by A6,XXREAL_0:2;
A9: 2|^(2|^m)+k > a-k+k by A3,XREAL_1:8;
per cases;
suppose
A10: p is composite;
take l;
2|^(2|^m)+k <= 2|^(2|^l)+k by A5,XREAL_1:6,PREPOWER:93;
hence a < 2|^(2|^l)+k by A9,XXREAL_0:2;
thus 2|^(2|^l)+k is composite by A10;
end;
suppose p is non composite;
then reconsider p as Prime by A6,A7,XXREAL_0:2,NUMBER02:def 1;
A11: s <= l by XXREAL_0:25,30;
l < 2|^l by NAT_3:2;
then consider N being Nat such that
A12: 2|^l = s+N by A11,XXREAL_0:2,NAT_1:10;
A13: 2|^(2|^l) + 2|^s*h = 2|^s*2|^N + 2|^s*h by A12,NEWTON:8
.= 2|^s*(2|^N+h);
then 2|^s divides p-1 by A2;
then consider h1 being Nat such that
A14: p-1 = 2|^s*h1 by NAT_D:def 3;
A15: h1 > 0 by A14;
h1 is odd
proof
assume h1 is even;
then consider c,d being Nat such that
d is odd and
A16: c > 0 and
A17: h1 = 2|^c * d by A15,NAT_5:2;
N > 0
proof
assume N <= 0;
then N = 0;
hence contradiction by A11,A12,NAT_3:2;
end;
hence contradiction by A2,A13,A14,A16,A17,XCMPLX_1:5;
end;
then reconsider h1 as odd Nat;
A18: Euler p = p-1 by EULER_1:20;
A19: p > 1 by INT_2:def 4;
2|^(2|^m)+k <= 2|^(2|^l)+k by A5,PREPOWER:93,XREAL_1:6;
then
A20: a < 2|^(2|^l)+k by A9,XXREAL_0:2;
A21: 2|^1,p are_coprime by A8,PEPIN:17,NAT_5:3;
A22: 2|^(2|^l)+k,0 are_congruent_mod p;
per cases;
suppose
A23: h1 = 1;
then reconsider h1 = 1 as odd Nat;
take l+Euler(1);
2|^(s+Euler(1)) = 2|^s*2|^Euler(1) by NEWTON:8;
then 2|^s,2|^(s+Euler(1)) are_congruent_mod p-1
by A14,A23,INT_4:10,INT_1:13;
then 2|^l,2|^(l+Euler(1)) are_congruent_mod p-1 by A11,Th29;
then 2|^(l+Euler(1)),2|^l are_congruent_mod p-1 by INT_1:14;
then 2|^(2|^(l+Euler(1))),2|^(2|^l) are_congruent_mod p
by A18,A21,Th69;
then 2|^(2|^(l+Euler(1)))+k,2|^(2|^l)+k are_congruent_mod p;
then
A24: 2|^(2|^(l+Euler(1)))+k,0 are_congruent_mod p by A22,INT_1:15;
2|^l <= 2|^(l+Euler(1)) by PREPOWER:93,NAT_1:11;
then 2|^(2|^l) <= 2|^(2|^(l+Euler(1))) by PREPOWER:93;
then
A25: 2|^(2|^l)+k <= 2|^(2|^(l+Euler(1)))+k by XREAL_1:6;
hence a < 2|^(2|^(l+Euler(1)))+k by A20,XXREAL_0:2;
now
assume 2|^(2|^(l+Euler(1)))+k is prime;
then p = 2|^(2|^(l+Euler(1)))+k by A19,A24;
then 2|^l = 2|^(l+Euler(1)) by PEPIN:30;
then l+0 = l+Euler(1) by PEPIN:30;
hence contradiction;
end;
hence 2|^(2|^(l+Euler(1)))+k is composite
by A8,A25,XXREAL_0:2,NUMBER02:def 1;
end;
suppose
A26: h1 <> 1;
take l+Euler(h1);
2|^1,h1 are_coprime by NAT_5:3;
then
A27: (2|^Euler(h1)) mod h1 = 1 by A26,EULER_2:18,NAT_1:25;
A28: 2|^(s+Euler(h1)) = 2|^s*2|^Euler(h1) by NEWTON:8;
1 mod h1 = 1 by A26,NAT_D:14,NAT_1:25;
then 2|^Euler(h1)*2|^s,1*2|^s are_congruent_mod h1*2|^s
by A27,NAT_D:64,INT_4:10;
then 2|^s,2|^(s+Euler(h1)) are_congruent_mod p-1 by A14,A28,INT_1:14;
then 2|^l,2|^(l+Euler(h1)) are_congruent_mod p-1 by A11,Th29;
then 2|^(l+Euler(h1)),2|^l are_congruent_mod p-1 by INT_1:14;
then 2|^(2|^(l+Euler(h1))),2|^(2|^l) are_congruent_mod p
by A18,A21,Th69;
then 2|^(2|^(l+Euler(h1)))+k,2|^(2|^l)+k are_congruent_mod p;
then
A29: 2|^(2|^(l+Euler(h1)))+k,0 are_congruent_mod p by A22,INT_1:15;
2|^l <= 2|^(l+Euler(h1)) by PREPOWER:93,NAT_1:11;
then 2|^(2|^l) <= 2|^(2|^(l+Euler(h1))) by PREPOWER:93;
then
A30: 2|^(2|^l)+k <= 2|^(2|^(l+Euler(h1)))+k by XREAL_1:6;
hence a < 2|^(2|^(l+Euler(h1)))+k by A20,XXREAL_0:2;
now
assume 2|^(2|^(l+Euler(h1)))+k is prime;
then p = 2|^(2|^(l+Euler(h1)))+k by A19,A29;
then 2|^l = 2|^(l+Euler(h1)) by PEPIN:30;
then l+0 = l+Euler(h1) by PEPIN:30;
hence contradiction;
end;
hence 2|^(2|^(l+Euler(h1)))+k is composite
by A8,A30,XXREAL_0:2,NUMBER02:def 1;
end;
end;
end;
Lm13:
for k being Integer st k <> 1 holds
{ 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite }
is non empty
proof
let k be Integer;
set X = { 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite };
assume k <> 1;
then consider n being positive Nat such that
1 < 2|^(2|^n)+k and
A1: 2|^(2|^n)+k is composite by Th70;
2|^(2|^n)+k in X by A1;
hence thesis;
end;
theorem Th71:
for k being Integer st k <> 1 holds
{ n where n is positive Nat: 2|^(2|^n)+k is composite },
{ 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite }
are_equipotent
proof
let k be Integer;
set X = { n where n is positive Nat: 2|^(2|^n)+k is composite };
set Y = { 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite };
assume k <> 1;
then
A1: Y is non empty by Lm13;
defpred P[object,object] means
for m st m = $1 holds $2 = 2|^(2|^m)+k;
A2: for x being object st x in X ex y being object st y in Y & P[x,y]
proof
let x be object;
assume x in X;
then consider n being positive Nat such that
A3: x = n & 2|^(2|^n)+k is composite;
take 2|^(2|^n)+k;
thus thesis by A3;
end;
consider f being Function of X,Y such that
A4: for x being object st x in X holds P[x,f.x] from FUNCT_2:sch 1(A2);
take f;
A5: dom f = X by A1,FUNCT_2:def 1;
thus f is one-to-one
proof
let x1,x2 be object;
assume
A6: x1 in dom f;
then consider n1 being positive Nat such that
A7: x1 = n1 and 2|^(2|^n1)+k is composite by A5;
assume
A8: x2 in dom f;
then consider n2 being positive Nat such that
A9: x2 = n2 and 2|^(2|^n2)+k is composite by A5;
assume
A10: f.x1 = f.x2;
A11: f.n1 = 2|^(2|^n1)+k by A4,A6,A7;
f.n2 = 2|^(2|^n2)+k by A4,A8,A9;
then 2|^n1 = 2|^n2 by A7,A9,A10,A11,XCMPLX_1:2,PEPIN:30;
hence thesis by A7,A9,PEPIN:30;
end;
thus dom f = X by A5;
thus rng f c= Y;
let y be object;
assume y in Y;
then consider n being positive Nat such that
A12: y = 2|^(2|^n)+k and
A13: 2|^(2|^n)+k is composite;
A14: n in dom f by A5,A13;
then f.n = y by A4,A12;
hence thesis by A14,FUNCT_1:def 3;
end;
:: Problem 115
theorem Th72:
for k being Integer st k <> 1 holds
{ 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite } is infinite
proof
let k be Integer such that
A1: k <> 1;
set X = { 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite };
A2: X is non empty by A1,Lm13;
A3: X is natural-membered
proof
let x be object;
assume x in X;
then ex n being positive Nat st
x = 2|^(2|^n)+k & 2|^(2|^n)+k is composite;
hence thesis;
end;
for w being Nat st w in X ex b being Nat st b > w & b in X
proof
let w be Nat;
assume w in X;
consider n being positive Nat such that
A4: w < 2|^(2|^n)+k and
A5: 2|^(2|^n)+k is composite by A1,Th70;
reconsider b = 2|^(2|^n)+k as positive Nat by A4;
take b;
thus thesis by A4,A5;
end;
hence thesis by A2,A3,NUMBER04:1;
end;
:: Problem 115
theorem
for k being Integer st k <> 1 holds
{ n where n is positive Nat: 2|^(2|^n)+k is composite } is infinite
proof
let k be Integer;
assume
A1: k <> 1;
then { n where n is positive Nat: 2|^(2|^n)+k is composite },
{ 2|^(2|^n)+k where n is positive Nat: 2|^(2|^n)+k is composite }
are_equipotent by Th71;
hence thesis by A1,Th72,CARD_1:38;
end;
begin :: Problem 117
Lm14:
2|^(2|^(2*s+1)) >= 256
proof
2*s >= 2*1 by NAT_1:14,XREAL_1:64;
then 2*s+1 >= 2+1 by XREAL_1:6;
then 2|^(2*s+1) >= 2|^3 by PREPOWER:93;
hence thesis by Lm6,Lm2,PREPOWER:93;
end;
theorem Th74:
7 divides 2|^(2|^(2*s+1)) + 3
proof
A1: 2*(2|^(2*s)) = 2|^(2*s+1) by NEWTON:6;
3 divides 2|^(2*s) - 1 by Th30;
then 2*3 divides 2* (2|^(2*s) - 1) by INT_4:7;
then consider k being Integer such that
A2: 2|^(2*s+1)-2 = 6*k by A1;
k >= 0 by A2;
then reconsider k as Element of NAT by INT_1:3;
A3: 2|^(2|^(2*s+1)) = 2|^(6*k+2) by A2
.= 2|^(6*k) * 2|^2 by NEWTON:8
.= (2|^6)|^k * 2|^2 by NEWTON:9;
2|^6 = 2*2*2*2*2*2 by NUMBER02:2
.= 7*9+1;
then 2|^6,1 are_congruent_mod 7;
then 2|^6|^k,1|^k are_congruent_mod 7 by GR_CY_3:34;
then 2|^6|^k*4,1*4 are_congruent_mod 7 by INT_4:11;
then 2|^6|^k*4+3,4+3 are_congruent_mod 7;
then 2|^6|^k*4+3,0 are_congruent_mod 7 by Th27;
hence thesis by A3,Lm1;
end;
:: Problem 117 a
theorem
2|^(2|^(2*s+1)) + 3 is composite
proof
set m = 2|^(2|^(2*s+1)) + 3;
A1: m >= 256+3 by Lm14,XREAL_1:6;
hence m >= 2 by XXREAL_0:2;
m <> 7 by A1;
hence thesis by Th74;
end;
Lm15:
2|^(2|^(4*s+1)) >= 2|^32
proof
4*s >= 4*1 by NAT_1:14,XREAL_1:64;
then 4*s+1 >= 4+1 by XREAL_1:6;
then 2|^(4*s+1) >= 2|^5 by PREPOWER:93;
hence thesis by Lm4,PREPOWER:93;
end;
theorem Th76:
11 divides 2|^(2|^(4*s+1)) + 7
proof
A1: 2*(2|^(4*s)) = 2|^(4*s+1) by NEWTON:6;
5 divides 2|^(4*s) - 1 by Th31;
then 2*5 divides 2* (2|^(4*s) - 1) by INT_4:7;
then consider k being Integer such that
A2: 2|^(4*s+1)-2 = 10*k by A1;
k >= 0 by A2;
then reconsider k as Element of NAT by INT_1:3;
A3: 2|^(2|^(4*s+1)) = 2|^(10*k+2) by A2
.= 2|^(10*k) * 2|^2 by NEWTON:8
.= (2|^10)|^k * 2|^2 by NEWTON:9;
2|^10 = 2*2*2*2*2*2*2*2*2*2 by NUMBER02:6
.= 93*11+1;
then 2|^10,1 are_congruent_mod 11;
then 2|^10|^k,1|^k are_congruent_mod 11 by GR_CY_3:34;
then 2|^10|^k*4,1*4 are_congruent_mod 11 by INT_4:11;
then 2|^10|^k*4+7,4+7 are_congruent_mod 11;
then 2|^10|^k*4+7,0 are_congruent_mod 11 by Th27;
hence thesis by A3,Lm1;
end;
:: Problem 117 b
theorem
2|^(2|^(4*s+1)) + 7 is composite
proof
set m = 2|^(2|^(4*s+1)) + 7;
A1: m >= 2|^32+7 by Lm15,XREAL_1:6;
2 <= 2|^32+5+2 by NAT_1:11;
hence m >= 2 by A1,XXREAL_0:2;
m <> 11 by Lm15,Lm1,PEPIN:66;
hence thesis by Th76;
end;
Lm16:
2|^(2|^(6*s+2)) >= 2|^256
proof
6*s >= 6*1 by NAT_1:14,XREAL_1:64;
then 6*s+2 >= 6+2 by XREAL_1:6;
then 2|^(6*s+2) >= 2|^8 by PREPOWER:93;
hence thesis by Lm6,PREPOWER:93;
end;
theorem Th78:
29 divides 2|^(2|^(6*s+2)) + 13
proof
A1: 2|^2*(2|^(6*s)) = 2|^(2+6*s) by NEWTON:8;
7 divides 2|^(6*s) - 1 by Th32;
then 4*7 divides 4* (2|^(6*s) - 1) by INT_4:7;
then consider k being Integer such that
A2: 2|^(6*s+2)-4 = 28*k by A1,Lm1;
k >= 0 by A2,Lm1;
then reconsider k as Element of NAT by INT_1:3;
A3: 2|^(2|^(6*s+2)) = 2|^(28*k+4) by A2
.= 2|^(28*k) * 2|^4 by NEWTON:8
.= (2|^28)|^k * 2|^4 by NEWTON:9;
2|^(14+14) = 2|^14*2|^14 by NEWTON:8
.= 9256395*29+1 by Lm9;
then 2|^28,1 are_congruent_mod 29;
then 2|^28|^k,1|^k are_congruent_mod 29 by GR_CY_3:34;
then 2|^28|^k*16,1*16 are_congruent_mod 29 by INT_4:11;
then 2|^28|^k*16+13,16+13 are_congruent_mod 29;
then 2|^28|^k*16+13,0 are_congruent_mod 29 by Th27;
hence thesis by A3,Lm3;
end;
:: Problem 117 c
theorem
2|^(2|^(6*s+2)) + 13 is composite
proof
set m = 2|^(2|^(6*s+2)) + 13;
A1: m >= 2|^256+13 by Lm16,XREAL_1:6;
2 <= 2|^256+11+2 by NAT_1:11;
hence m >= 2 by A1,XXREAL_0:2;
m <> 29 by Lm16,Lm3,PEPIN:66;
hence thesis by Th78;
end;
Lm17:
2|^(2|^(10*s+1)) >= 2|^2048
proof
10*s >= 10*1 by NAT_1:14,XREAL_1:64;
then 10*s+1 >= 10+1 by XREAL_1:6;
then 2|^(10*s+1) >= 2|^11 by PREPOWER:93;
hence thesis by Lm8,PREPOWER:93;
end;
theorem Th80:
23 divides 2|^(2|^(10*s+1)) + 19
proof
A1: 2*(2|^(10*s)) = 2|^(1+10*s) by NEWTON:6;
11 divides 2|^(10*s) - 1 by Th33;
then 2*11 divides 2* (2|^(10*s) - 1) by INT_4:7;
then consider k being Integer such that
A2: 2|^(10*s+1)-2 = 22*k by A1;
k >= 0 by A2;
then reconsider k as Element of NAT by INT_1:3;
A3: 2|^(2|^(10*s+1)) = 2|^(22*k+2) by A2
.= 2|^(22*k) * 2|^2 by NEWTON:8
.= (2|^22)|^k * 2|^2 by NEWTON:9;
2|^(11+11) = 2|^11*2|^11 by NEWTON:8
.= 182361*23+1 by Lm8;
then 2|^22,1 are_congruent_mod 23;
then 2|^22|^k,1|^k are_congruent_mod 23 by GR_CY_3:34;
then 2|^22|^k*4,1*4 are_congruent_mod 23 by INT_4:11;
then 2|^22|^k*4+19,4+19 are_congruent_mod 23;
then 2|^22|^k*4+19,0 are_congruent_mod 23 by Th27;
hence thesis by A3,Lm1;
end;
:: Problem 117 d
theorem
2|^(2|^(10*s+1)) + 19 is composite
proof
set m = 2|^(2|^(10*s+1)) + 19;
A1: m >= 2|^2048+19 by Lm17,XREAL_1:6;
2 <= 2|^2048+17+2 by NAT_1:11;
hence m >= 2 by A1,XXREAL_0:2;
m <> 23 by Lm17,Lm1,PEPIN:66;
hence thesis by Th80;
end;
theorem Th82:
37 divides 2|^(2|^(6*s+2)) + 21
proof
A1: 2|^2*(2|^(6*s)) = 2|^(2+6*s) by NEWTON:8;
9 divides 2|^(6*s) - 1 by Th34;
then 4*9 divides 4* (2|^(6*s) - 1) by INT_4:7;
then consider k being Integer such that
A2: 2|^(6*s+2)-4 = 36*k by A1,Lm1;
k >= 0 by A2,Lm1;
then reconsider k as Element of NAT by INT_1:3;
A3: 2|^(2|^(6*s+2)) = 2|^(36*k+4) by A2
.= 2|^(36*k) * 2|^4 by NEWTON:8
.= (2|^36)|^k * 2|^4 by NEWTON:9;
2|^(18+18) = 2|^18*2|^18 by NEWTON:8
.= 1857283155*37+1 by Lm10;
then 2|^36,1 are_congruent_mod 37;
then 2|^36|^k,1|^k are_congruent_mod 37 by GR_CY_3:34;
then 2|^36|^k*16,1*16 are_congruent_mod 37 by INT_4:11;
then 2|^36|^k*16+21,16+21 are_congruent_mod 37;
then 2|^36|^k*16+21,0 are_congruent_mod 37 by Th27;
hence thesis by A3,Lm3;
end;
:: Problem 117 e
theorem
2|^(2|^(6*s+2)) + 21 is composite
proof
set m = 2|^(2|^(6*s+2)) + 21;
A1: m >= 2|^256+21 by Lm16,XREAL_1:6;
2 <= 2|^256+19+2 by NAT_1:11;
hence m >= 2 by A1,XXREAL_0:2;
m <> 37 by Lm16,Lm3,PEPIN:66;
hence thesis by Th82;
end;
begin :: Problem 145
theorem Th84:
Fermat(5) = 641 * 6700417 by Lm11,Lm6,Lm12,Lm4; :: = 4294967297
:: Problem 145
theorem
for x,y being positive Nat holds
x*y+x+y = 2|^32 iff x = 640 & y = 6700416 or x = 6700416 & y = 640
proof
let x,y be positive Nat;
A1: x+1 <> 0+1 & y+1 <> 0+1;
thus x*y+x+y = 2|^32 implies x = 640 & y = 6700416 or x = 6700416 & y = 640
proof
assume x*y+x+y = 2|^32;
then Fermat(5) = (x+1)*(y+1) by Lm4;
then x+1 = 641 & y+1 = 6700417 or x+1 = 6700417 & y+1 = 641
by A1,Th84,NUMBER07:59,XPRIMES1:641,XPRIMES3:4;
hence thesis;
end;
thus thesis by Lm11,Lm6,Lm12;
end;
begin :: Problem 157
registration
let a be non positive Integer;
let n be odd Nat;
cluster a|^n -> non positive;
coherence
proof
per cases;
suppose a is zero;
hence thesis;
end;
suppose a is negative;
hence thesis;
end;
end;
end;
theorem Th86:
for a,b,c,d,n being Nat st a,b,c are_mutually_coprime & a*b*c = d|^n
ex k being Nat st a = k|^n
proof
let a,b,c,d,n be Nat such that
A1: a,b,c are_mutually_coprime;
assume a*b*c = d|^n;
then ex k1 being Nat st k1|^n = a*b by A1,NEWTON02:30,INT_2:26;
hence thesis by A1,NEWTON02:30;
end;
:: Problem 157
theorem
(for x,y,z being positive Nat holds x/y + y/z <> z/x)
iff
(for u,v,w being positive Nat holds u|^3 + v|^3 <> w|^3)
proof
thus (for x,y,z being positive Nat holds x/y + y/z <> z/x)
implies
(for u,v,w being positive Nat holds u|^3 + v|^3 <> w|^3)
proof
assume
A1: for x,y,z being positive Nat holds x/y + y/z <> z/x;
given u,v,w being positive Nat such that
A2: u|^3 + v|^3 = w|^3;
set x = u^2*v;
set y = v^2*w;
set z = w^2*u;
A3: u|^3 = u*u*u & v|^3 = v*v*v & w|^3 = w*w*w by POLYEQ_5:2;
x/y + y/z = (u^2*v)/(v*w*v) + (v^2*w)/(w*u*w)
.= (u^2)/(v*w) + (v^2*w)/(w*u*w) by XCMPLX_1:91
.= (u^2)/(v*w) + (v^2)/(w*u) by XCMPLX_1:91
.= (u^2*u)/(v*w*u) + (v^2)/(w*u) by XCMPLX_1:91
.= (u^2*u)/(v*w*u) + (v^2*v)/(w*u*v) by XCMPLX_1:91
.= (w|^3)/(w*u*v) by A2,A3
.= (w^2*w)/(u*v*w) by POLYEQ_5:2
.= (w^2)/(u*v) by XCMPLX_1:91
.= (w^2*u)/(u*v*u) by XCMPLX_1:91
.= z/x;
hence thesis by A1;
end;
assume
A4: for u,v,w being positive Nat holds u|^3 + v|^3 <> w|^3;
given x,y,z being positive Nat such that
A5: x/y + y/z = z/x;
set a = x^2*z;
set b = y^2*x;
x/y + y/z = (x*z+y^2)/(y*z) by XCMPLX_1:116;
then z*(y*z) = x*(x*z+y^2) by A5,XCMPLX_1:95;
then
A6: a*b*(a+b) = (x^2*z)*(y^2*x)*(z^2*y)
.= (x*y*z)*(x*y*z)*(x*y*z);
set d = a gcd b;
consider a1,b1 being Nat such that
A7: a = d*a1 & b = d*b1 and
A8: a1,b1 are_coprime by NUMBER03:18;
reconsider a1,b1 as positive Nat by A7;
A9: d|^3 = d*d*d & (x*y*z)|^3 = (x*y*z)*(x*y*z)*(x*y*z) by POLYEQ_5:2;
A10: a1*b1*(a1+b1)*(d*d*d) = (d*a1)*(d*b1)*(d*(a1+b1))
.= (x*y*z)*(x*y*z)*(x*y*z) by A6,A7;
then d*d*d divides (x*y*z)*(x*y*z)*(x*y*z);
then consider t being Nat such that
A11: x*y*z = d*t by A9,WSIERP_1:26,NAT_D:def 3;
A12: a1*b1*(a1+b1)*(d*d*d) = (d*t)*(d*t)*(d*t) by A10,A11
.= t*t*t*(d*d*d);
A13: t|^3 = t*t*t by POLYEQ_5:2;
A14: 3 = 2*1+1;
A15: 1*a1+b1,a1 are_coprime & 1*b1+a1,b1 are_coprime by A8,NUMBER04:64;
then a1,b1,a1+b1 are_mutually_coprime by A8;
then consider u being Nat such that
A16: u|^3 = a1 by A12,A13,Th86,XCMPLX_1:5;
A17: u is positive by A14,A16;
A18: a1*(a1+b1)*b1 = a1*b1*(a1+b1);
a1+b1,a1,b1 are_mutually_coprime by A8,A15;
then consider v being Nat such that
A19: v|^3 = a1+b1 by A12,A13,A18,Th86,XCMPLX_1:5;
A20: v is positive by A14,A19;
b1,a1,a1+b1 are_mutually_coprime by A8,A15;
then consider w being Nat such that
A21: w|^3 = b1 by A12,A13,Th86,XCMPLX_1:5;
w is positive by A14,A21;
hence thesis by A4,A16,A17,A19,A20,A21;
end;
begin :: Problem 159
registration
let a,b,c be positive Real;
cluster <*a,b,c*> -> positive-yielding;
coherence;
end;
registration
let a,b,c,d be positive Real;
cluster <*a,b,c,d*> -> positive-yielding;
coherence;
end;
Lm18:
now
let x,y,z,t be positive Integer;
A1: (x/y) * (y/z) = (x*y) / (y*z) by XCMPLX_1:76;
(x*y) / (y*z) * (z/t) = (x*y*z) / (y*z*t) by XCMPLX_1:76;
hence (x/y) * (y/z) * (z/t) * (t/x) = (x*y*z*t) / (y*z*t*x) by A1,XCMPLX_1:76
.= 1 by XCMPLX_1:60;
end;
theorem Th88:
for a,b,c,d being Complex holds Product <*a,b,c,d*> = a*b*c*d
proof
let a,b,c,d be Complex;
thus Product <*a,b,c,d*> = Product <*a,b,c*> * d by RVSUM_1:96
.= a*b*c*d by RVSUM_1:100;
end;
theorem
for a being positive Real holds 2-root(a) = sqrt(a)
proof
let a be positive Real;
thus 2-root(a) = 2-Root a by POWER:def 1
.= sqrt(a) by PREPOWER:32;
end;
theorem
for a being positive Real holds GMean <*a*> = a
proof
let a be positive Real;
len <*a*> = 1 by CARD_1:def 7;
hence thesis by POWER:9;
end;
theorem
for a,b being positive Real holds (GMean <*a,b*>)|^2 = a*b
proof
let a,b be positive Real;
set f = <*a,b*>;
A1: Product f = a*b by RVSUM_1:99;
len f = 2 by CARD_1:def 7;
hence thesis by A1;
end;
theorem
for a,b,c being positive Real holds (GMean <*a,b,c*>)|^3 = a*b*c
proof
let a,b,c be positive Real;
set f = <*a,b,c*>;
A1: Product f = a*b*c by RVSUM_1:100;
len f = 3 by CARD_1:def 7;
hence thesis by A1;
end;
theorem Th93:
for a,b,c,d being positive Real holds (GMean <*a,b,c,d*>)|^4 = a*b*c*d
proof
let a,b,c,d be positive Real;
set f = <*a,b,c,d*>;
A1: Product f = a*b*c*d by Th88;
len f = 4 by CARD_1:def 7;
hence thesis by A1;
end;
theorem
for a being Real holds Mean <*a*> = a
proof
let a be Real;
len <*a*> = 1 by CARD_1:def 7;
hence thesis;
end;
theorem
for a,b being Real holds Mean <*a,b*> = (a+b)/2
proof
let a,b be Real;
len <*a,b*> = 2 by CARD_1:def 7;
hence thesis by RVSUM_2:34;
end;
theorem
for a,b,c being Real holds Mean <*a,b,c*> = (a+b+c)/3
proof
let a,b,c be Real;
len <*a,b,c*> = 3 by CARD_1:def 7;
hence thesis by RVSUM_2:35;
end;
theorem Th97:
for a,b,c,d being Real holds Mean <*a,b,c,d*> = (a+b+c+d)/4
proof
let a,b,c,d be Real;
len <*a,b,c,d*> = 4 by CARD_1:def 7;
hence thesis by Th20;
end;
Lm19:
for f being positive real-valued FinSequence st GMean f = Mean f holds
f is constant
proof
let f be positive real-valued FinSequence;
assume
A1: GMean f = Mean f;
assume f is heterogeneous; then
reconsider ff = f as
non empty heterogeneous positive real-valued FinSequence;
ex g being non empty homogeneous positive real-valued FinSequence st
GMean g > GMean ff & Mean g = Mean ff by RVSUM_3:46;
hence thesis by A1,RVSUM_3:14;
end;
theorem Th98:
for w,x,y,z being object st <*w,x,y,z*> is constant holds w = x = y = z
proof
let w,x,y,z be object;
assume
A1: <*w,x,y,z*> is constant;
then
A2: <*w,x,y*> is constant by SPRECT_1:1;
<*w,x,y,z*> = <*w,x*>^<*y,z*> by FINSEQ_4:74;
then <*y,z*> is constant by A1,SPRECT_1:1;
hence thesis by A2,SPRECT_1:2,3;
end;
Lm20:
now
let a,b,c,d be positive Real;
set f = <*a,b,c,d*>;
A1: len f = 4 by FINSEQ_4:76;
A2: Sum f = a+b+c+d by RVSUM_1:142;
(GMean f)|^4 <= (Mean f)|^4 by PREPOWER:9,RVSUM_3:47;
hence a*b*c*d <= ((a+b+c+d)/4)|^4 by A1,A2,Th88;
end;
theorem Th99:
for a,b,c,d being positive Real st a*b*c*d >= ((a+b+c+d)/4)|^4
holds a = b = c = d
proof
let a,b,c,d be positive Real;
set f = <*a,b,c,d*>;
A1: len f = 4 by FINSEQ_4:76;
A2: Sum f = a+b+c+d by RVSUM_1:142;
(GMean f)|^4 <= (Mean f)|^4 by PREPOWER:9,RVSUM_3:47;
then
A3: a*b*c*d <= ((a+b+c+d)/4)|^4 by A1,A2,Th88;
A4: (GMean f)|^4 = a*b*c*d by Th93;
A5: Mean f = (a+b+c+d)/4 by Th97;
assume a*b*c*d >= ((a+b+c+d)/4)|^4;
then a*b*c*d = ((a+b+c+d)/4)|^4 by A3,XXREAL_0:1;
then (Mean f)|^4 = (GMean f)|^4 by A4,A5;
then f is constant by Lm19,WSIERP_1:3;
hence a = b = c = d by Th98;
end;
:: Problem 159 a
theorem
for m being Real st 0 <= m < 4 holds
not ex x,y,z,t being positive Integer st x/y + y/z + z/t + t/x = m
proof
let m be Real;
assume
A1: 0 <= m;
assume m < 4;
then
A2: m/4 < 4/4 by XREAL_1:74;
given x,y,z,t being positive Integer such that
A3: x/y + y/z + z/t + t/x = m;
(x/y) * (y/z) * (z/t) * (t/x) = 1 by Lm18;
then (m/4)|^4 >= 1|^4 by A3,Lm20;
hence contradiction by A1,A2,PREPOWER:10;
end;
:: Problem 159 b
theorem
{ [x,y,z,t] where x,y,z,t is positive Integer: x/y + y/z + z/t + t/x = 4 }
= { [x,y,z,t] where x,y,z,t is positive Integer: x = y = z = t }
proof
set A = {[x,y,z,t] where x,y,z,t is positive Integer: x/y+y/z+z/t+t/x = 4};
set B = {[x,y,z,t] where x,y,z,t is positive Integer: x = y = z = t};
thus A c= B
proof
let q be object;
assume q in A;
then consider x,y,z,t being positive Integer such that
A1: q = [x,y,z,t] and
A2: x/y+y/z+z/t+t/x = 4;
(x/y)*(y/z)*(z/t)*(t/x) = (4/4)|^4 by Lm18;
then x/y = y/z = z/t = t/x by A2,Th99;
then x = y = z = t by A2,XCMPLX_1:58;
hence thesis by A1;
end;
let q be object;
assume q in B;
then consider x,y,z,t being positive Integer such that
A3: q = [x,y,z,t] and
A4: x = y = z = t;
x/y = 1 & y/z = 1 & z/t = 1 & t/x = 1 by A4,XCMPLX_1:60;
then x/y + y/z + z/t + t/x = 1+1+1+1;
hence thesis by A3;
end;
registration
let a,b be Nat;
reduce In([a,b],[:NAT,NAT:]) to [a,b];
reducibility
proof
[In(a,NAT),In(b,NAT)] in [:NAT,NAT:];
hence thesis;
end;
end;
registration
let a,b,c be Nat;
reduce In([a,b,c],[:NAT,NAT,NAT:]) to [a,b,c];
reducibility
proof
[In(a,NAT),In(b,NAT),In(c,NAT)] in [:NAT,NAT,NAT:];
hence thesis;
end;
end;
registration
let a,b,c,d be Nat;
reduce In([a,b,c,d],[:NAT,NAT,NAT,NAT:]) to [a,b,c,d];
reducibility
proof
[In(a,NAT),In(b,NAT),In(c,NAT),In(d,NAT)] in [:NAT,NAT,NAT,NAT:];
hence thesis;
end;
end;
registration
let a be positive Nat;
reduce In(a,NATPLUS) to a;
reducibility
proof
a in NATPLUS by NAT_LAT:def 6;
hence thesis by SUBSET_1:def 8;
end;
end;
registration
let a,b be positive Nat;
reduce In([a,b],[:NATPLUS,NATPLUS:]) to [a,b];
reducibility
proof
[In(a,NATPLUS),In(b,NATPLUS)] in [:NATPLUS,NATPLUS:];
hence thesis;
end;
end;
registration
let a,b,c be positive Nat;
reduce In([a,b,c],[:NATPLUS,NATPLUS,NATPLUS:]) to [a,b,c];
reducibility
proof
[In(a,NATPLUS),In(b,NATPLUS),In(c,NATPLUS)] in [:NATPLUS,NATPLUS,NATPLUS:];
hence thesis;
end;
end;
registration
let a,b,c,d be positive Nat;
reduce In([a,b,c,d],[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:]) to [a,b,c,d];
reducibility
proof
[In(a,NATPLUS),In(b,NATPLUS),In(c,NATPLUS),In(d,NATPLUS)]
in [:NATPLUS,NATPLUS,NATPLUS,NATPLUS:];
hence thesis;
end;
end;
definition
set A = NATPLUS;
set D = [:A,A,A,A:];
func Cart4Id -> Function of NATPLUS, [:NATPLUS,NATPLUS,NATPLUS,NATPLUS:]
means :Def1:
for n being positive Nat holds it.n = [n,n,n,n];
existence
proof
deffunc F(Nat) = In([$1,$1,$1,$1],D);
consider f being Function of A,D such that
A1: for x being Element of A holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let n be positive Nat;
n in A by NAT_LAT:def 6;
hence f.n = F(n) by A1
.= [n,n,n,n];
end;
uniqueness
proof
let f1,f2 be Function of A,D such that
A2: for n being positive Nat holds f1.n = [n,n,n,n] and
A3: for n being positive Nat holds f2.n = [n,n,n,n];
let n be Element of A;
thus f1.n = [n,n,n,n] by A2
.= f2.n by A3;
end;
end;
registration
cluster Cart4Id -> one-to-one;
coherence
proof
set f = Cart4Id;
let x1,x2 be object;
assume x1 in dom f & x2 in dom f;
then reconsider x1,x2 as positive Nat;
f.x1 = [x1,x1,x1,x1] & f.x2 = [x2,x2,x2,x2] by Def1;
hence thesis by XTUPLE_0:5;
end;
end;
theorem Th102:
rng Cart4Id c=
{ [x,y,z,t] where x,y,z,t is positive Integer: x/y + y/z + z/t + t/x = 4 }
proof
set f = Cart4Id;
set A =
{ [x,y,z,t] where x,y,z,t is positive Integer: x/y + y/z + z/t + t/x = 4 };
let q be object;
assume q in rng f;
then consider a being Element of NATPLUS such that
A1: f.a = q by FUNCT_2:113;
A2: f.a = [a,a,a,a] by Def1;
a/a = 1 by XCMPLX_1:60;
then a/a + a/a + a/a + a/a = 4;
hence thesis by A1,A2;
end;
:: Problem 159 c
theorem
{ [x,y,z,t] where x,y,z,t is positive Integer: x/y + y/z + z/t + t/x = 4 }
is infinite
proof
dom Cart4Id = NATPLUS by FUNCT_2:def 1;
hence thesis by Th102,CARD_1:59;
end;
begin :: Problem 161
definition
let R be Relation;
func Permutations(R) -> set equals
the set of all p*R where p is Permutation of dom R;
coherence;
end;
definition
let f be Function;
redefine func Permutations(f) -> set equals :: redefines Permutations (NUMBER17, definition)
the set of all f*p where p is Permutation of dom f;
coherence;
compatibility;
end;
definition
let A be set;
attr A is relational means :Def4:
for a being object st a in A holds a is Relation;
end;
registration
let a,b be object;
cluster { { [a,b] } } -> relational;
coherence;
end;
registration
cluster non empty finite relational for set;
existence
proof
take {{[1,1]}};
thus thesis;
end;
end;
registration
let A be relational set;
cluster -> Relation-like for Element of A;
coherence
proof
let a be Element of A;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A is non empty;
hence thesis by Def4;
end;
end;
end;
registration
cluster functional -> relational for set;
coherence;
end;
registration
let R be finite Relation;
cluster Permutations(R) -> finite;
coherence
proof
deffunc F(Relation) = $1*R;
set A = permutations(dom R);
A1: A is finite;
set X = { F(w) where w is Element of A: w in A };
A2: X is finite from FRAENKEL:sch 21(A1);
Permutations(R) = X
proof
thus Permutations(R) c= X
proof
let a be object;
assume a in Permutations(R);
then consider p being Permutation of dom R such that
A3: a = p*R;
p in A;
hence thesis by A3;
end;
let a be object;
assume a in X;
then consider w being Element of A such that
A4: a = F(w) and
A5: w in A;
ex p being Permutation of dom R st w = p by A5;
hence thesis by A4;
end;
hence thesis by A2;
end;
end;
definition
let A be relational set;
func Permutations(A) -> set equals
{ Permutations(f) where f is Element of A: f in A };
coherence;
end;
registration
let A be finite relational set;
cluster Permutations(A) -> finite;
coherence
proof
deffunc F(Relation) = Permutations($1);
A1: A is finite;
{ F(w) where w is Element of A: w in A } is finite
from FRAENKEL:sch 21(A1);
hence thesis;
end;
end;
definition
let f be complex-valued FinSequence;
attr f is with_sum_of_reciprocals_equal_1 means
Sum(f") = 1;
end;
registration
cluster <*1*> -> with_sum_of_reciprocals_equal_1;
coherence
proof
<*1*>" = <*1"*> by NUMBER15:63;
hence thesis;
end;
end;
registration
cluster with_sum_of_reciprocals_equal_1 for complex-valued FinSequence;
existence
proof
take <*1*>;
thus thesis;
end;
end;
definition
let s be Nat;
func SolutionsOfSumOfReciprocals(s) -> set equals
{ f where f is positive-yielding s-element natural-valued FinSequence:
f is with_sum_of_reciprocals_equal_1 };
coherence;
end;
registration
let s be zero Nat;
cluster SolutionsOfSumOfReciprocals(s) -> empty;
coherence
proof
assume not thesis;
then consider x being object such that
A1: x in SolutionsOfSumOfReciprocals(s) by XBOOLE_0:def 1;
ex f being positive-yielding s-element natural-valued FinSequence
st x = f & f is with_sum_of_reciprocals_equal_1 by A1;
hence thesis;
end;
end;
theorem Th104:
Sum(s|->(s")) = 1
proof
thus Sum(s|->(s")) = s*s" by RVSUM_1:80
.= 1 by XCMPLX_0:def 7;
end;
registration
let s be positive Nat;
cluster s|->s -> with_sum_of_reciprocals_equal_1;
coherence
proof
Sum(s|->(s")) = 1 by Th104;
hence thesis by Th43;
end;
end;
theorem Th105:
s|->s in SolutionsOfSumOfReciprocals(s);
registration
let s be positive Nat;
cluster SolutionsOfSumOfReciprocals(s) -> non empty;
coherence by Th105;
end;
definition
let A,B be FinSequence-membered set;
func A^^B -> set equals
{ p^q where p is (Element of A), q is Element of B: p in A & q in B };
coherence;
end;
registration
let A,B be FinSequence-membered set;
cluster A^^B -> FinSequence-membered;
coherence
proof
let x be object;
assume x in A^^B;
then ex p being (Element of A), q being Element of B st
x = p^q & p in A & q in B;
hence thesis;
end;
end;
theorem Th106:
for A being FinSequence-membered set holds A^^{} c= A
proof
let A be FinSequence-membered set;
let x be object;
assume x in A^^{};
then ex p being (Element of A), q being Element of {} st
x = p^q & p in A & q in {};
hence thesis;
end;
theorem Th107:
for A being FinSequence-membered set holds {}^^A c= A
proof
let A be FinSequence-membered set;
let x be object;
assume x in {}^^A;
then ex p being (Element of {}), q being Element of A st
x = p^q & p in {} & q in A;
hence thesis;
end;
registration
let A,B be finite FinSequence-membered set;
cluster A^^B -> finite;
coherence
proof
per cases;
suppose A is non empty & B is non empty;
then reconsider A,B as non empty finite FinSequence-membered set;
deffunc F((Element of A),Element of B) = $1^$2;
A1: A is finite;
A2: B is finite;
{ F(u,v) where u is (Element of A), v is Element of B:
u in A & v in B } is finite from FRAENKEL:sch 22(A1,A2);
hence thesis;
end;
suppose A is empty;
then A^^B c= B & B^^A c= B by Th106,Th107;
hence thesis;
end;
suppose B is empty;
then A^^B c= A & B^^A c= A by Th106,Th107;
hence thesis;
end;
end;
end;
definition
let D,A be set;
attr A is D-FinSequence-membered means
for f being object st f in A holds f is D-valued FinSequence;
end;
registration
let D be non empty set;
let d be Element of D;
cluster { <*d*> } -> D-FinSequence-membered;
coherence;
end;
registration
let D be non empty set;
cluster D-FinSequence-membered for set;
existence
proof
take { <*the Element of D*> };
thus thesis;
end;
end;
definition
let D be non empty set;
let A be D-FinSequence-membered set;
func decomp(A) -> Relation means :Def10:
for x,y being object holds [x,y] in it iff
x in D & ex f being FinSequence of D st y = f & <*x*>^f in A;
existence
proof
defpred P[object,object] means
$1 in D & ex f being FinSequence of D st $2 = f & <*$1*>^f in A;
consider R being Relation such that
A1: for x,y being object holds [x,y] in R iff x in D & y in D* & P[x,y]
from RELAT_1:sch 1;
take R;
let x,y be object;
thus [x,y] in R implies P[x,y] by A1;
assume that
A2: x in D and
A3: ex f being FinSequence of D st y = f & <*x*>^f in A;
y in D* by A3,FINSEQ_1:def 11;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let P,Q be Relation such that
A4: for x,y being object holds [x,y] in P iff
x in D & ex f being FinSequence of D st y = f & <*x*>^f in A and
A5: for x,y being object holds [x,y] in Q iff
x in D & ex f being FinSequence of D st y = f & <*x*>^f in A;
let x,y be object;
thus [x,y] in P implies [x,y] in Q
proof
assume [x,y] in P;
then x in D & ex f being FinSequence of D st y = f & <*x*>^f in A by A4;
hence thesis by A5;
end;
assume [x,y] in Q;
then x in D & ex f being FinSequence of D st y = f & <*x*>^f in A by A5;
hence thesis by A4;
end;
end;
registration
let D be set;
cluster D-FinSequence-membered -> FinSequence-membered for set;
coherence
proof
let A be set such that
A1: A is D-FinSequence-membered;
let x be object;
thus thesis by A1;
end;
end;
deffunc XX(object) = <*$1*>;
definition
let A be set;
func OneFS(A) -> ManySortedSet of A means :Def11:
for a being object st a in A holds it.a = <*a*>;
existence
proof
ex f being ManySortedSet of A st
for i being object st i in A holds f.i = XX(i) from PBOOLE:sch 4;
hence thesis;
end;
uniqueness
proof
let f,g be ManySortedSet of A such that
A1: for a being object st a in A holds f.a = <*a*> and
A2: for a being object st a in A holds g.a = <*a*>;
dom f = A & dom g = A by PARTFUN1:def 2;
hence dom f = dom g;
let a be object;
assume
A3: a in dom f;
hence f.a = <*a*> by A1
.= g.a by A2,A3;
end;
end;
registration
let A be set;
cluster OneFS(A) -> FinSequence-yielding;
coherence
proof
let a be object;
assume a in dom OneFS(A);
then OneFS(A).a = <*a*> by Def11;
hence thesis;
end;
end;
registration
let f be FinSequence-yielding Function;
cluster rng f -> FinSequence-membered;
coherence
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;
end;
end;
registration
let n;
let f be n-element real-valued FinSequence;
cluster sort_a(f) -> n-element;
coherence
proof
len f = len sort_a f by RFINSEQ2:31;
hence thesis by CARD_1:def 7;
end;
cluster sort_d(f) -> n-element;
coherence
proof
len f = len sort_d f by RFINSEQ2:30;
hence thesis by CARD_1:def 7;
end;
end;
theorem Th108:
for f,g being complex-valued FinSequence, P being Permutation of dom g
st f = g*P & len g >= 1 holds f" = (g")*P
proof
let f,g be complex-valued FinSequence, P be Permutation of dom g;
assume that
A1: f = g*P and
A2: len g >= 1;
A3: rng P = dom g by FUNCT_2:def 3;
A4: dom (g") = dom g by VALUED_1:def 7;
then
A5: rng ((g")*P) = rng (g") by A3,RELAT_1:28;
A6: dom (f") = dom (g*P) by A1,VALUED_1:def 7;
then
A7: dom (f") = dom P by A3,RELAT_1:27;
then
A8: dom (f") = dom ((g")*P) by A3,A4,RELAT_1:27;
A9: dom g = Seg len g by FINSEQ_1:def 3;
then dom P = dom g by A2,FUNCT_2:def 1;
then (g")*P is FinSequence by A7,A8,A9,FINSEQ_1:def 2;
then reconsider k = (g")*P as FinSequence of COMPLEX by A5,FINSEQ_1:def 4;
for i being Nat st i in dom (f") holds (f").i = k.i
proof
let i be Nat;
assume
A10: i in dom (f");
reconsider j = P.i as Nat;
(f").i = (f.i)" by VALUED_1:10
.= (g.(P.i))" by A1,A6,A10,FUNCT_1:12
.= (g").j by VALUED_1:10
.= ((g")*P).i by A8,A10,FUNCT_1:12;
hence thesis;
end;
hence thesis by A8,FINSEQ_1:13;
end;
theorem Th109:
for f,g being complex-valued FinSequence st
f,g are_fiberwise_equipotent holds f",g" are_fiberwise_equipotent
proof
let f,g be complex-valued FinSequence;
assume f,g are_fiberwise_equipotent;
then consider P being Permutation of dom g such that
A1: f = g*P by RFINSEQ:4;
A2: now
per cases;
case len g >= 1;
hence f" = (g")*P by A1,Th108;
end;
case len g < 1;
then g = {} by NAT_1:14;
hence f" = (g")*P by A1;
end;
end;
dom (g") = dom g by VALUED_1:def 7;
hence thesis by A2,RFINSEQ:4;
end;
theorem Th110:
for s being Nat
for f being non-decreasing positive (s+1)-element natural-valued FinSequence
holds f.1 <= (s+1)/Sum(f") & Sum(Del(f,1)") = Sum(f")-1/f.1
proof
let s be Nat;
let f be non-decreasing positive (s+1)-element natural-valued FinSequence;
set u = Sum(f");
set g = Del(f,1);
A1: len f = s+1 by CARD_1:def 7;
defpred Q[FinSequence of NAT] means
for F being non-decreasing positive natural-valued FinSequence
st F = $1 holds Sum($1") <= (len $1) / $1.1;
A2: Q[<*>NAT];
A3: for p being FinSequence of NAT for x being Element of NAT st Q[p]
holds Q[p^<*x*>]
proof
let p be FinSequence of NAT;
let x be Element of NAT such that
A4: Q[p];
let P be non-decreasing positive natural-valued FinSequence
such that
A5: P = p^<*x*>;
p is len p-element;
then
A6: P.1 = p.1 & ... & P.(len p) = p.(len p) by A5,FINSEQ_3:154;
A7: <*x*>" = <*x"*> by NUMBER15:63;
per cases;
suppose len p < 1;
then p = {} by NAT_1:14;
then
A8: P = <*x*> by A5,FINSEQ_1:34;
len <*x*> = 1 by FINSEQ_1:39;
hence thesis by A5,A8,A7;
end;
suppose 1 <= len p;
then
A9: P.1 = p.1 by A6;
A10: len P = len p + 1 by A5,FINSEQ_2:16;
A11: P" = p"^<*x*>" by A5,NUMBER15:60;
A12: Sum(P") = Sum(p") + x" by A7,A11,RVSUM_1:74;
A13: p is non-decreasing by A5,Th37;
p is positive by A5,NUMBER08:37;
then
A14: Sum(p") + x" <= (len p) / p.1 + x" by A4,A13,XREAL_1:6;
A15: 1 <= 1 + len p by NAT_1:11;
then
A16: 1 in dom P by A10,FINSEQ_3:25;
A17: len P in dom P by A10,A15,FINSEQ_3:25;
1 <= len P by A5,A10,XREAL_1:6;
then P.1 <= P.(len P) by A16,A17,VALUED_0:def 15;
then (P.1)" >= (P.(len P))" by A5,XREAL_1:85;
then len p / p.1 + x" <= len p / p.1 + 1 / p.1
by A9,A5,A10,XREAL_1:6;
hence thesis by A9,A10,A12,A5,A14,XXREAL_0:2;
end;
end;
A18: for p being FinSequence of NAT holds Q[p] from FINSEQ_2:sch 2(A2,A3);
reconsider F = f as FinSequence of NAT by FINSEQ_1:103;
Q[F] by A18;
then u*(f.1) <= (s+1)/(f.1)*(f.1) by A1,XREAL_1:64;
then u*(f.1) <= s+1 by XCMPLX_1:87;
then u*(f.1)/u <= (s+1)/u by XREAL_1:64;
hence f.1 <= (s+1)/u by XCMPLX_1:89;
f = <*f.1*>^g by FINSEQ_5:86;
then f" = <*f.1*>"^g" by NUMBER15:60
.= <*(f.1)"*>^g" by NUMBER15:63;
then u = (f.1)" + Sum(g") by RVSUM_2:33;
hence Sum(g") = u-1/f.1;
end;
theorem Th111:
for s being Nat, w being Rational holds
{ f where f is non-decreasing positive s-element natural-valued FinSequence:
Sum(f") = w } is finite
proof
let s be Nat, w be Rational;
deffunc A(Nat,Rational) = { f where f is non-decreasing positive $1-element
natural-valued FinSequence: Sum(f") = $2 };
defpred P[Nat] means for q being Rational holds A($1,q) is finite;
A1: P[0]
proof
let q be Rational;
A(0,q) c= {{}}
proof
let a be object;
assume a in A(0,q);
then ex f being non-decreasing positive 0-element
natural-valued FinSequence st a = f & Sum(f") = q;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
A2: for s being Nat st P[s] holds P[s+1]
proof
let s be Nat such that
A3: P[s];
let u be Rational;
set ONE = {<*f.1*> where
f is positive s+1-element natural-valued FinSequence: f in A(s+1,u)};
ONE is FinSequence-membered
proof
let a be object;
assume a in ONE;
then ex f being positive s+1-element natural-valued FinSequence st
a = <*f.1*> & f in A(s+1,u);
hence thesis;
end;
then reconsider ONE as FinSequence-membered set;
A(s+1,u) is FinSequence-membered
proof
let a be object;
assume a in A(s+1,u);
then ex f being non-decreasing positive s+1-element natural-valued
FinSequence st a = f & Sum(f") = u;
hence thesis;
end;
then reconsider As1u = A(s+1,u) as FinSequence-membered set;
As1u is NAT-FinSequence-membered
proof
let z be object;
assume z in As1u;
then ex f being non-decreasing positive s+1-element natural-valued
FinSequence st z = f & Sum(f") = u;
hence thesis;
end;
then reconsider As1u as NAT-FinSequence-membered set;
set DE = decomp(As1u);
reconsider p1 = rng OneFS(proj1 DE) as FinSequence-membered set;
set p2 = proj2 DE;
p2 is FinSequence-membered
proof
let a be object;
assume a in p2;
then consider x being object such that
A4: [x,a] in DE by XTUPLE_0:def 13;
ex f being FinSequence of NAT st a = f & <*x*>^f in As1u by A4,Def10;
hence thesis;
end;
then reconsider p2 as FinSequence-membered set;
A5: dom OneFS(proj1 DE) = proj1 DE by PARTFUN1:def 2;
A6: A(s+1,u) c= p1^^p2
proof
let z be object;
assume
A7: z in A(s+1,u);
then
consider f being non-decreasing positive s+1-element natural-valued
FinSequence such that
A8: z = f and Sum(f") = u;
set p = f.1;
set q = Del(f,1);
A9: f = <*p*>^q by FINSEQ_5:86;
A10: p in NAT by ORDINAL1:def 12;
q is FinSequence of NAT by FINSEQ_1:103;
then
A11: [p,q] in DE by A7,A8,A9,A10,Def10;
then
A12: p in proj1 DE by XTUPLE_0:def 12;
then (OneFS(proj1 DE)).p = <*p*> by Def11;
then
A13: <*p*> in p1 by A5,A12,FUNCT_1:def 3;
q in p2 by A11,XTUPLE_0:def 13;
hence thesis by A8,A9,A13;
end;
defpred PX[object] means not contradiction;
set XXX =
{XX(i) where i is Element of INT: 0 <= i & i <= [\(s+1)/u/]+1 & PX[i]};
A14: XXX is finite from XXREAL_2:sch 1;
A15: ONE c= XXX
proof
let x be object;
assume x in ONE;
then consider f being positive s+1-element natural-valued FinSequence
such that
A16: x = <*f.1*> and
A17: f in A(s+1,u);
A18: ex f1 being non-decreasing positive s+1-element natural-valued
FinSequence st f = f1 & Sum(f1") = u by A17;
reconsider i = f.1 as Element of INT by INT_1:def 2;
A19: f.1 <= (s+1)/u by A18,Th110;
(s+1)/u-1 < [\(s+1)/u/] by INT_1:def 6;
then (s+1)/u-1+1 < [\(s+1)/u/]+1 by XREAL_1:6;
then i <= [\(s+1)/u/]+1 by A19,XXREAL_0:2;
hence thesis by A16;
end;
A20: p1 c= XXX
proof
let y be object;
assume y in p1;
then consider x being object such that
A21: x in dom OneFS(proj1 DE) and
A22: (OneFS(proj1 DE)).x = y by FUNCT_1:def 3;
consider z being object such that
A23: [x,z] in DE by A21,XTUPLE_0:def 12;
consider f being FinSequence of NAT such that
z = f and
A24: <*x*>^f in As1u by A23,Def10;
consider g being non-decreasing positive s+1-element natural-valued
FinSequence such that
A25: g = <*x*>^f and
A26: Sum(g") = u by A24;
A27: <*x*> is NAT-valued by A25,BAGORD_2:7;
then reconsider x as Element of INT by Th3;
A28: 0 <= x by A27;
g.1 = x by A25;
then
A29: x <= (s+1)/u by A26,Th110;
(s+1)/u-1 < [\(s+1)/u/] by INT_1:def 6;
then (s+1)/u-1+1 < [\(s+1)/u/]+1 by XREAL_1:6;
then x <= [\(s+1)/u/]+1 by A29,XXREAL_0:2;
then XX(x) in XXX by A28;
hence thesis by A21,A22,Def11;
end;
defpred FUN[object,object] means
ex n being Nat st $1 = <*n*> &
$2 = {g where g is non-decreasing positive s-element natural-valued
FinSequence: Sum((<*n*>^g)") = u};
A30: for i being object st i in ONE ex j being object st FUN[i,j]
proof
let i be object;
assume i in ONE;
then consider f being positive s+1-element natural-valued FinSequence
such that
A31: i = <*f.1*> and
f in A(s+1,u);
take {g where g is non-decreasing positive s-element natural-valued
FinSequence: Sum((<*f.1*>^g)") = u};
take n = f.1;
thus i = <*n*> by A31;
thus thesis;
end;
consider FUN being ManySortedSet of ONE such that
A32: for x being object st x in ONE holds FUN[x,FUN.x] from PBOOLE:sch 3(A30);
A33: dom FUN = ONE by PARTFUN1:def 2;
A34: p2 c= union rng FUN
proof
let z be object;
assume z in p2;
then consider x being object such that
A35: [x,z] in DE by XTUPLE_0:def 13;
consider f being FinSequence of NAT such that
A36: z = f and
A37: <*x*>^f in As1u by A35,Def10;
consider g being non-decreasing positive s+1-element natural-valued
FinSequence such that
A38: g = <*x*>^f and
A39: Sum(g") = u by A37;
<*x*> is NAT-valued by A38,BAGORD_2:7;
then reconsider x as Element of INT by Th3;
x = g.1 by A38;
then
A40: <*x*> in ONE by A37,A38;
then consider n being Nat such that
A41: <*x*> = <*n*> and
A42: FUN.<*x*> =
{g where g is non-decreasing positive s-element natural-valued
FinSequence: Sum((<*n*>^g)") = u} by A32;
set Z = {g where g is non-decreasing positive s-element natural-valued
FinSequence: Sum((<*n*>^g)") = u};
reconsider f as natural-valued FinSequence;
A43: len g = s+1 by CARD_1:def 7;
A44: len g = 1+len f by A38,FINSEQ_5:8;
A45: g = <*x*>^f by A38;
then reconsider f as positive s-element natural-valued FinSequence
by A43,A44,CARD_1:def 7,NUMBER08:37;
f is non-decreasing by A45,Th37;
then
A46: f in Z by A38,A39,A41;
Z in rng FUN by A33,A40,A42,FUNCT_1:def 3;
hence thesis by A36,A46,TARSKI:def 4;
end;
FUN is finite-yielding
proof
let x be object;
assume x in ONE;
then FUN[x,FUN.x] by A32;
then consider n being Nat such that
A47: x = <*n*> and
A48: FUN.<*n*> =
{g where g is non-decreasing positive s-element natural-valued
FinSequence: Sum((<*n*>^g)") = u};
A49: A(s,u-n") is finite by A3;
FUN.<*n*> c= A(s,u-n")
proof
let w be object;
assume w in FUN.<*n*>;
then consider g being non-decreasing positive s-element
natural-valued FinSequence such that
A50: w = g and
A51: Sum((<*n*>^g)") = u by A48;
A52: (<*n*>^g)" = <*n*>"^g" by NUMBER15:60;
<*n*>" = <*n"*> by NUMBER15:63;
then Sum(<*n*>"^g") = n" + Sum(g") by RVSUM_1:76;
hence thesis by A50,A51,A52;
end;
hence FUN.x is finite by A47,A49;
end;
hence thesis by A6,A14,A15,A20,A34;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th112:
for s being Nat, w being Rational holds
{ f where f is positive-yielding s-element natural-valued FinSequence:
Sum(f") = w } is finite
proof
let s be Nat;
let w be Rational;
set A = { f where f is positive s-element natural-valued FinSequence:
Sum(f") = w };
set I = { f where f is non-decreasing positive s-element natural-valued
FinSequence: Sum(f") = w };
I is functional
proof
let x be object;
assume x in I;
then ex f being non-decreasing positive s-element natural-valued
FinSequence st x = f & Sum(f") = w;
hence thesis;
end;
then reconsider Ip = I as functional set;
A1: I is finite by Th111;
for X being set st X in Permutations(Ip) holds X is finite
proof
let X be set;
assume X in Permutations(Ip);
then consider E being Element of Ip such that
A2: X = Permutations(E) and
A3: E in Ip;
ex f being non-decreasing positive s-element natural-valued
FinSequence st E = f & Sum(f") = w by A3;
hence thesis by A2;
end;
then
A4: union Permutations(Ip) is finite by A1,FINSET_1:7;
deffunc S(natural-valued FinSequence) = sort_a $1;
A c= union Permutations(Ip)
proof
let a be object;
assume a in A;
then consider f being positive s-element natural-valued FinSequence
such that
A5: a = f and
A6: Sum(f") = w;
A7: f,S(f) are_fiberwise_equipotent by RFINSEQ2:def 6;
then consider P being Permutation of dom S(f) such that
A8: f = S(f)*P by RFINSEQ:4;
Sum((S(f))") = Sum(f") by A7,Th109,RFINSEQ:9;
then
A9: S(f) in Ip by A6;
A10: a in Permutations(S(f)) by A5,A8;
Permutations(S(f)) in Permutations(Ip) by A9;
hence thesis by A10,TARSKI:def 4;
end;
hence thesis by A4;
end;
:: Problem 161
registration
let s be Nat;
cluster SolutionsOfSumOfReciprocals(s) -> finite;
coherence
proof
set A = SolutionsOfSumOfReciprocals(s);
set B = { f where f is positive s-element natural-valued FinSequence:
Sum(f") = 1 };
A = B
proof
thus A c= B
proof
let x be object;
assume x in A;
then ex f being positive s-element natural-valued FinSequence st
x = f & f is with_sum_of_reciprocals_equal_1;
hence thesis;
end;
let x be object;
assume x in B;
then consider f being positive s-element natural-valued FinSequence
such that
A1: x = f and
A2: Sum(f") = 1;
f is with_sum_of_reciprocals_equal_1 by A2;
hence thesis by A1;
end;
hence thesis by Th112;
end;
end;
begin :: Problem 162
registration
cluster <*2,3*> -> increasing;
coherence by Th39;
end;
registration
cluster <*2,3,6*> -> increasing;
coherence by Th40;
end;
registration
cluster <*2,3,7,42*> -> increasing;
coherence by Th41;
end;
registration
cluster <*2,3,8,24*> -> increasing;
coherence by Th41;
end;
definition
let f be complex-valued FinSequence;
func Sierp162FS(f) -> FinSequence equals
<*2*> ^ (2(#)f);
coherence;
func Sierp162FS_2(f) -> FinSequence equals
<*2,3*> ^ (6(#)f);
coherence;
end;
registration
let f be complex-valued FinSequence;
cluster Sierp162FS(f) -> complex-valued;
coherence;
cluster Sierp162FS_2(f) -> complex-valued;
coherence;
end;
registration
let f be real-valued FinSequence;
cluster Sierp162FS(f) -> real-valued;
coherence;
cluster Sierp162FS_2(f) -> real-valued;
coherence;
end;
registration
let f be rational-valued FinSequence;
cluster Sierp162FS(f) -> rational-valued;
coherence;
cluster Sierp162FS_2(f) -> rational-valued;
coherence;
end;
registration
let f be integer-valued FinSequence;
cluster Sierp162FS(f) -> integer-valued;
coherence;
cluster Sierp162FS_2(f) -> integer-valued;
coherence;
end;
registration
let f be natural-valued FinSequence;
cluster Sierp162FS(f) -> natural-valued;
coherence;
cluster Sierp162FS_2(f) -> natural-valued;
coherence;
end;
registration
let s be Nat;
let f be s-element complex-valued FinSequence;
cluster Sierp162FS(f) -> (s+1)-element;
coherence;
cluster Sierp162FS_2(f) -> (s+2)-element;
coherence;
end;
registration
let s be Nat;
cluster increasing s-element for natural-valued FinSequence;
existence
proof
take idseq(s);
thus thesis;
end;
end;
theorem Th113:
for s being Nat holds s >= 2 implies
for f being positive-yielding s-element real-valued FinSequence
st f is with_sum_of_reciprocals_equal_1
for k being Nat st k in dom f holds f.k > 1
proof
let s be Nat such that
A1: s >= 2;
let f be positive-yielding s-element real-valued FinSequence such that
A2: f is with_sum_of_reciprocals_equal_1;
let k be Nat such that
A3: k in dom f;
A4: dom f = dom(f") by VALUED_1:def 7;
len(f") = s by CARD_1:def 7;
then
A5: f".k < 1 by A1,A2,A3,A4,Th42;
f".k = (f.k)" by VALUED_1:10;
then 1" < (f.k)"" by A3,A5,XREAL_1:85,RVSUM_3:def 1;
hence f.k > 1;
end;
Lm21: len <*2*> = 1 by FINSEQ_1:39;
Lm22: len <*2,3*> = 2 by FINSEQ_1:44;
theorem Th114:
for s being Nat holds s >= 2 implies
for f being increasing positive-yielding s-element real-valued FinSequence
st f is with_sum_of_reciprocals_equal_1
holds Sierp162FS(f) is increasing
proof
let s be Nat such that
A1: s >= 2;
let f be increasing positive-yielding s-element real-valued FinSequence
such that
A2: f is with_sum_of_reciprocals_equal_1;
set g = Sierp162FS(f);
let x,y be Nat such that
A3: x in dom g and
A4: y in dom g and
A5: x < y;
set F = 2(#)f;
A6: len g = len <*2*> + len F by FINSEQ_1:22;
A7: y <= len g by A4,FINSEQ_3:25;
x >= 1 by A3,FINSEQ_3:25;
then per cases by XXREAL_0:1;
suppose
A8: x = 1;
reconsider y1 = y-1 as Element of NAT by A5,INT_1:3;
A9: 1 <= y1 by A5,A8,INT_1:52;
A10: y1 <= len g - 1 by A7,XREAL_1:6;
then
A11: g.(1+y1) = F.y1 by A6,A9,Lm21,FINSEQ_1:65
.= 2*(f.y1) by VALUED_1:6;
len(F) = len f by COMPLSP2:3;
then f.y1 > 1 by A1,A2,A6,A9,A10,Lm21,Th113,FINSEQ_3:25;
then 2*f.y1 > 2*1 by XREAL_1:68;
hence g.x < g.y by A8,A11;
end;
suppose
A12: x > 1;
then reconsider x1 = x-1 as Element of NAT by INT_1:3;
1+1 <= x by A12,NAT_1:13;
then
A13: 1+1-1 <= x1 by XREAL_1:6;
x <= len g by A3,FINSEQ_3:25;
then x1 <= len g - 1 by XREAL_1:6;
then
A14: x1 in dom F by A6,A13,Lm21,FINSEQ_3:25;
then
A15: g.(x1+1) = F.x1 by FINSEQ_3:103
.= 2*f.x1 by VALUED_1:6;
reconsider y1 = y-1 as Element of NAT by A5,INT_1:3;
y > 1 by A5,A12,XXREAL_0:2;
then 1+1 <= y by NAT_1:13;
then
A16: 1+1-1 <= y1 by XREAL_1:6;
y1 <= len g - 1 by A7,XREAL_1:6;
then
A17: y1 in dom F by A6,A16,Lm21,FINSEQ_3:25;
then
A18: g.(y1+1) = F.y1 by FINSEQ_3:103
.= 2*f.y1 by VALUED_1:6;
A19: dom F = dom f by VALUED_1:def 5;
x1 < y1 by A5,XREAL_1:6;
hence g.x < g.y by A14,A15,A17,A18,A19,SEQM_3:def 1,XREAL_1:68;
end;
end;
theorem Th115:
for f being increasing positive-yielding s-element natural-valued FinSequence
holds Sierp162FS_2(f) is increasing
proof
let f be increasing positive-yielding s-element natural-valued FinSequence;
set g = Sierp162FS_2(f);
set F = 6(#)f;
A1: f.1 >= 0+1 by NAT_1:13;
F.1 = 6*f.1 by VALUED_1:6;
then F.1 >= 6*1 by A1,XREAL_1:64;
then <*2,3*>.2 < F.1 by XXREAL_0:2;
hence thesis by Lm22,Th38;
end;
theorem Th116:
for f being complex-valued FinSequence st
f is with_sum_of_reciprocals_equal_1
holds Sierp162FS(f) is with_sum_of_reciprocals_equal_1
proof
let f be complex-valued FinSequence such that
A1: f is with_sum_of_reciprocals_equal_1;
set g = Sierp162FS(f);
set F = 2(#)f;
A2: F" = 2"(#)f" by NUMBER15:58;
A3: <*2*>" = <*2"*> by NUMBER15:63;
A4: Sum(2"(#)f") = 2"*Sum(f") by RVSUM_2:38;
g" = <*2*>"^F" by NUMBER15:60;
hence Sum(g") = Sum(<*2*>") + Sum(F") by RVSUM_2:32
.= 1 by A1,A2,A3,A4;
end;
theorem Th117:
for f being complex-valued FinSequence st
f is with_sum_of_reciprocals_equal_1
holds Sierp162FS_2(f) is with_sum_of_reciprocals_equal_1
proof
let f be complex-valued FinSequence such that
A1: f is with_sum_of_reciprocals_equal_1;
set g = Sierp162FS_2(f);
set F = 6(#)f;
A2: F" = 6"(#)f" by NUMBER15:58;
A3: <*2,3*>" = <*2",3"*> by NUMBER15:64;
A4: Sum(6"(#)f") = 6"*Sum(f") by RVSUM_2:38;
A5: Sum <*2",3"*> = 2"+3" by RVSUM_2:34;
g" = <*2,3*>"^F" by NUMBER15:60;
hence Sum(g") = Sum(<*2,3*>") + Sum(F") by RVSUM_2:32
.= 1 by A1,A2,A3,A4,A5;
end;
theorem Th118:
<*2,3,6*> is with_sum_of_reciprocals_equal_1
proof
set f = <*2,3,6*>;
set g = <*1/2,1/3,1/6*>;
f" = g
proof
A1: len(f") = 3 & len g = 3 by CARD_1:def 7;
hence len(f") = len g;
let k be Nat;
assume 1 <= k & k <= len(f");
then k = 1 or ... or k = 3 by A1;
hence g.k = (f.k)"
.= (f").k by VALUED_1:10;
end;
hence Sum (f") = 1/2 + 1/3 + 1/6 by RVSUM_1:78
.= 1;
end;
theorem Th119:
<*2,3,7,42*> is with_sum_of_reciprocals_equal_1
proof
set f = <*2,3,7,42*>;
set g = <*1/2,1/3,1/7,1/42*>;
f" = g
proof
A1: len(f") = 4 & len g = 4 by CARD_1:def 7;
hence len(f") = len g;
let k be Nat;
assume 1 <= k & k <= len(f");
then k = 1 or ... or k = 4 by A1;
hence g.k = (f.k)"
.= (f").k by VALUED_1:10;
end;
hence Sum (f") = 1/2 + 1/3 + 1/7 + 1/42 by Th20
.= 1;
end;
theorem Th120:
<*2,3,8,24*> is with_sum_of_reciprocals_equal_1
proof
set f = <*2,3,8,24*>;
set g = <*1/2,1/3,1/8,1/24*>;
f" = g
proof
A1: len(f") = 4 & len g = 4 by CARD_1:def 7;
hence len(f") = len g;
let k be Nat;
assume 1 <= k & k <= len(f");
then k = 1 or ... or k = 4 by A1;
hence g.k = (f.k)"
.= (f").k by VALUED_1:10;
end;
hence Sum (f") = 1/2 + 1/3 + 1/8 + 1/24 by Th20
.= 1;
end;
:: Problem 162 a
theorem Th121:
for s being Nat st s > 2
ex f being increasing positive-yielding s-element natural-valued FinSequence
st f is with_sum_of_reciprocals_equal_1
proof
let s be Nat;
assume s > 2;
then
A1: s >= 2+1 by NAT_1:13;
defpred P[Nat] means
ex f being increasing positive $1-element natural-valued FinSequence st
f is with_sum_of_reciprocals_equal_1;
A2: P[3] by Th118;
A3: for j being Nat st 3 <= j holds P[j] implies P[j+1]
proof
let j be Nat such that
A4: 3 <= j;
given f being increasing positive j-element natural-valued FinSequence
such that
A5: f is with_sum_of_reciprocals_equal_1;
set g = Sierp162FS(f);
reconsider g as increasing positive (j+1)-element natural-valued
FinSequence by A4,A5,Th114,XXREAL_0:2;
take g;
thus thesis by A5,Th116;
end;
for i being Nat st 3 <= i holds P[i] from NAT_1:sch 8(A2,A3);
hence thesis by A1;
end;
definition
let s be Nat;
func IncreasingSolutionsOfSumOfReciprocals(s) -> set equals
{ f where
f is increasing positive-yielding s-element natural-valued FinSequence:
f is with_sum_of_reciprocals_equal_1 };
coherence;
end;
theorem Th122:
for s being Nat holds
IncreasingSolutionsOfSumOfReciprocals(s) c= SolutionsOfSumOfReciprocals(s)
proof
let s be Nat;
let x be object;
assume x in IncreasingSolutionsOfSumOfReciprocals(s);
then ex f being increasing positive-yielding s-element
natural-valued FinSequence st x = f & f is with_sum_of_reciprocals_equal_1;
hence thesis;
end;
registration
let s be positive Nat;
cluster IncreasingSolutionsOfSumOfReciprocals(s) -> finite;
coherence
proof
IncreasingSolutionsOfSumOfReciprocals(s) c= SolutionsOfSumOfReciprocals(s)
by Th122;
hence thesis;
end;
end;
Lm23:
now
let s;
thus s = 1 or s = 2 or s = 3 or s >= 4
proof
per cases;
suppose s <= 3;
then s = 0 or ... or s = 3;
hence thesis;
end;
suppose s > 3;
then s >= 3+1 by NAT_1:13;
hence thesis;
end;
end;
end;
Lm24:
now
let s;
thus s = 1 or s = 2 or s = 3 or s = 4 or s >= 5
proof
per cases;
suppose s <= 4;
then s = 0 or ... or s = 4;
hence thesis;
end;
suppose s > 4;
then s >= 4+1 by NAT_1:13;
hence thesis;
end;
end;
end;
Lm25:
now
let s;
thus s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7
proof
per cases;
suppose s <= 6;
then s = 0 or ... or s = 6;
hence thesis;
end;
suppose s > 6;
then s >= 6+1 by NAT_1:13;
hence thesis;
end;
end;
end;
theorem Th123:
IncreasingSolutionsOfSumOfReciprocals(3) = {<*2,3,6*>}
proof
set S = IncreasingSolutionsOfSumOfReciprocals(3);
thus S c= {<*2,3,6*>}
proof
let x be object;
assume x in S;
then
consider f being increasing positive 3-element natural-valued FinSequence
such that
A1: x = f and
A2: f is with_sum_of_reciprocals_equal_1;
consider a,b,c being positive Nat such that
A3: f = <*a,b,c*> and
A4: a < b and
A5: b < c by Th48;
f" = <*a",b",c"*> by A3,NUMBER15:65;
then
A6: a"+b"+c" = 1 by A2,RVSUM_2:35;
A7: now
assume
A8: a <> 2;
a >= 0+1 by NAT_1:13;
then per cases by XXREAL_0:1;
suppose a = 1;
then a"+(b"+c") > 1+0 by XREAL_1:8;
hence contradiction by A6;
end;
suppose a > 1;
then a >= 1+1 by NAT_1:13;
then a > 2 by A8,XXREAL_0:1;
then
A9: a >= 2+1 by NAT_1:13;
then
A10: a" <= 3" by XREAL_1:85;
b > 3 by A4,A9,XXREAL_0:2;
then
A11: b >= 3+1 by NAT_1:13;
then b" <= 4" by XREAL_1:85;
then
A12: a"+b" <= 3"+4" by A10,XREAL_1:7;
c > 4 by A5,A11,XXREAL_0:2;
then c >= 4+1 by NAT_1:13;
then c" <= 5" by XREAL_1:85;
then a"+b"+c" <= 3"+4"+5" by A12,XREAL_1:7;
hence contradiction by A6;
end;
end;
A13: now
assume b <> 3;
then per cases by Lm23;
suppose b = 1 or b = 2;
hence contradiction by A4,A7;
end;
suppose
A14: b >= 4;
then b" <= 4" by XREAL_1:85;
then
A15: a"+b" <= 2"+4" by A7,XREAL_1:7;
c > 4 by A5,A14,XXREAL_0:2;
then c >= 4+1 by NAT_1:13;
then c" <= 5" by XREAL_1:85;
then a"+b"+c" <= 2"+4"+5" by A15,XREAL_1:7;
hence contradiction by A6;
end;
end;
now
assume c <> 6;
then per cases by Lm25;
suppose c = 1 or c = 2 or c = 3;
hence contradiction by A5,A13;
end;
suppose c = 4 or c = 5;
hence contradiction by A6,A7,A13;
end;
suppose c >= 7;
then c" <= 7" by XREAL_1:85;
then a"+b"+c" <= 2"+3"+7" by A7,A13,XREAL_1:6;
hence contradiction by A6;
end;
end;
hence thesis by A1,A3,A7,A13,TARSKI:def 1;
end;
let x be object;
assume x in {<*2,3,6*>};
then x = <*2,3,6*> by TARSKI:def 1;
hence thesis by Th118;
end;
theorem Th124:
{<*2,3,7,42*>,<*2,3,8,24*>} c= IncreasingSolutionsOfSumOfReciprocals(4)
proof
let x be object;
assume x in {<*2,3,7,42*>,<*2,3,8,24*>};
then x = <*2,3,7,42*> or x = <*2,3,8,24*> by TARSKI:def 2;
hence thesis by Th119,Th120;
end;
:: Problem 162 b
theorem
for s being positive Nat st s > 2 holds
card IncreasingSolutionsOfSumOfReciprocals(s) <
card IncreasingSolutionsOfSumOfReciprocals(s+1)
proof
let s be positive Nat;
set S = IncreasingSolutionsOfSumOfReciprocals(s);
set S1 = IncreasingSolutionsOfSumOfReciprocals(s+1);
assume s > 2;
then s >= 2+1 by NAT_1:13;
then per cases by XXREAL_0:1;
suppose
A1: s = 3;
then
A2: card S = 1 by Th123,CARD_1:30;
set f = <*2,3,7,42*>;
set g = <*2,3,8,24*>;
len f = 4 by CARD_1:def 7;
then 3 <= len f & f.3 <> g.3;
then
A3: card {f,g} = 2 by CARD_2:57;
card {f,g} <= card S1 by A1,Th124,NAT_1:43;
hence card S1 > card S by A2,A3,XXREAL_0:2;
end;
suppose
A4: s > 3;
then
A5: s-1 > 3-1 by XREAL_1:9;
then reconsider t = s-1 as positive Element of NAT by INT_1:3;
A6: 1 <= t+1 by NAT_1:11;
consider f being increasing positive t-element natural-valued FinSequence
such that
A7: f is with_sum_of_reciprocals_equal_1 by A5,Th121;
A8: len f = t by CARD_1:def 7;
A9: Sierp162FS_2(f).2 = 2*1+1 by NUMBER14:21;
set X = S \/ {f};
defpred P[object,object] means
($1 = f implies $2 = Sierp162FS_2(f)) &
($1 <> f implies
ex h being complex-valued FinSequence st $1 = h & $2 = Sierp162FS(h));
A10: for x being object st x in X ex y being object st y in S1 & P[x,y]
proof
let x be object;
assume x in X;
then per cases by ZFMISC_1:136;
suppose x in S;
then consider X being increasing positive t+1-element natural-valued
FinSequence such that
A11: x = X and
A12: X is with_sum_of_reciprocals_equal_1;
take q = Sierp162FS(X);
A13: q is increasing by A4,A12,Th114,XXREAL_0:2;
A14: q is with_sum_of_reciprocals_equal_1 by A12,Th116;
len X = t+1 by CARD_1:def 7;
hence thesis by A8,A11,A13,A14;
end;
suppose
A15: x = f;
take q = Sierp162FS_2(f);
A16: q is increasing by Th115;
q is with_sum_of_reciprocals_equal_1 by A7,Th117;
hence thesis by A15,A16;
end;
end;
consider F being Function such that
A17: dom F = X and
A18: rng F c= S1 and
A19: for x being object st x in X holds P[x,F.x] from FUNCT_1:sch 6(A10);
F is one-to-one
proof
let x1,x2 be object such that
A20: x1 in dom F and
A21: x2 in dom F and
A22: F.x1 = F.x2;
A23: P[x1,F.x1] by A17,A19,A20;
A24: P[x2,F.x2] by A17,A19,A21;
per cases by A17,A20,ZFMISC_1:136;
suppose x1 in S;
then consider F1 being increasing positive t+1-element natural-valued
FinSequence such that
A25: x1 = F1 and
F1 is with_sum_of_reciprocals_equal_1;
A26: len F1 = t+1 by CARD_1:def 7;
per cases by A17,A21,ZFMISC_1:136;
suppose x2 in S;
then consider F2 being increasing positive t+1-element
natural-valued FinSequence such that
A27: x2 = F2 and
F2 is with_sum_of_reciprocals_equal_1;
len F2 = t+1 by CARD_1:def 7;
then 2(#)F1 = 2(#)F2 by A8,A22,A23,A24,A25,A26,A27,FINSEQ_1:33;
hence thesis by A25,A27,Th49;
end;
suppose
A28: x2 = f;
consider h being complex-valued FinSequence such that
A29: x1 = h and
F.x1 = Sierp162FS(h) by A8,A23,A25,A26;
A30: len h = t+1 by A25,A29,CARD_1:def 7;
dom(2(#)h) = dom h by VALUED_1:def 5;
then Sierp162FS(h).(1+1) = (2(#)h).1 by A6,A30,FINSEQ_3:25,103
.= 2*(h.1) by VALUED_1:6;
hence thesis by A9,A22,A23,A24,A25,A28,A29;
end;
end;
suppose
A31: x1 = f;
per cases by A17,A21,ZFMISC_1:136;
suppose x2 in S;
then consider F2 being increasing positive t+1-element
natural-valued FinSequence such that
A32: x2 = F2 and
F2 is with_sum_of_reciprocals_equal_1;
len F2 = t+1 by CARD_1:def 7;
then consider h being complex-valued FinSequence such that
A33: x2 = h and
F.x2 = Sierp162FS(h) by A8,A24,A32;
A34: len h = t+1 by A32,A33,CARD_1:def 7;
dom(2(#)h) = dom h by VALUED_1:def 5;
then Sierp162FS(h).(1+1) = (2(#)h).1 by A6,A34,FINSEQ_3:25,103
.= 2*(h.1) by VALUED_1:6;
hence thesis by A9,A22,A23,A24,A31,A32,A33;
end;
suppose x2 = f;
hence thesis by A31;
end;
end;
end;
then Segm card(X) c= Segm card(S1) by A17,A18,CARD_1:10;
then
A35: card(X) <= card(S1) by NAT_1:39;
S misses {f}
proof
assume S meets {f};
then consider x being object such that
A36: x in S and
A37: x in {f} by XBOOLE_0:3;
x = f by A37,TARSKI:def 1;
then consider F1 being increasing positive t+1-element natural-valued
FinSequence such that
A38: f = F1 and
F1 is with_sum_of_reciprocals_equal_1 by A36;
len F1 = t+1 by CARD_1:def 7;
hence contradiction by A8,A38;
end;
then card X = card(S) + card {f} by CARD_2:40
.= card(S) + 1 by CARD_1:30;
hence card(S) < card(S1) by A35,NAT_1:13;
end;
end;
begin :: Problem 163
registration
let n be Nat;
cluster Triangle n -> triangular;
coherence by NUMPOLY1:def 2;
end;
registration
let a be triangular Nat;
cluster <*a*> -> triangular-valued;
coherence
proof
let n be object;
A1: dom <*a*> = {1} by FINSEQ_1:def 8,2;
per cases;
suppose n = 1;
hence thesis;
end;
suppose n <> 1;
then not n in dom <*a*> by A1,TARSKI:def 1;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
deffunc T(Nat) = Triangle($1);
registration
cluster triangular-valued for FinSequence;
existence
proof
take <*T(0)*>;
thus thesis;
end;
end;
registration
let f,g be triangular-valued FinSequence;
cluster f^g -> triangular-valued;
coherence
proof
let n be object;
per cases;
suppose
A1: n in dom(f^g);
then reconsider n as Nat;
A2: 1 <= n by A1,FINSEQ_3:25;
A3: n <= len(f^g) by A1,FINSEQ_3:25;
per cases;
suppose n <= len f;
then (f^g).n = f.n by A2,FINSEQ_1:64;
hence thesis by NUMBER06:def 8;
end;
suppose n > len f;
then (f^g).n = g.(n-len f) by A3,FINSEQ_1:24;
hence thesis by NUMBER06:def 8;
end;
end;
suppose not n in dom(f^g);
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let a,b be triangular Nat;
cluster <*a,b*> -> triangular-valued;
coherence;
end;
registration
let a,b,c be triangular Nat;
cluster <*a,b,c*> -> triangular-valued;
coherence;
end;
registration
let a,b,c,d be triangular Nat;
cluster <*a,b,c,d*> -> triangular-valued;
coherence;
end;
registration
let a,b,c,d,e be triangular Nat;
cluster <*a,b,c,d,e*> -> triangular-valued;
coherence;
end;
registration
let a,b,c,d,e,f be triangular Nat;
cluster <*a,b,c,d,e,f*> -> triangular-valued;
coherence;
end;
theorem
<* Triangle 1 *> is with_sum_of_reciprocals_equal_1 by NUMPOLY1:11;
theorem Th127:
<* Triangle 2, Triangle 2, Triangle 2 *> is with_sum_of_reciprocals_equal_1
proof
set d = T(2);
<*d,d,d*>" = <*d",d",d"*> by NUMBER15:65;
hence Sum(<*d,d,d*>") = d"+d"+d" by RVSUM_2:35
.= 1 by NUMPOLY1:12;
end;
theorem Th128:
<* Triangle 2,Triangle 2,Triangle 3,Triangle 3 *>
is with_sum_of_reciprocals_equal_1
proof
set d = T(2);
set t = T(3);
<*d,d,t,t*>" = <*d",d",t",t"*> by Th15;
hence Sum(<*d,d,t,t*>") = d"+d"+t"+t" by Th20
.= 1 by NUMPOLY1:12,13;
end;
theorem Th129:
<* Triangle 3,Triangle 3,Triangle 3,Triangle 3,Triangle 3,Triangle 3*>
is with_sum_of_reciprocals_equal_1
proof
set t = T(3);
<*t,t,t,t,t,t*>" = <*t",t",t",t",t",t"*> by Th17;
hence Sum(<*t,t,t,t,t,t*>") = t"+t"+t"+t"+t"+t" by Th22
.= 1 by NUMPOLY1:13;
end;
definition
let n,a be Nat such that
A1: n >= a+1;
func TriangleShift2(n,a) -> FinSequence of NAT means :Def15:
len it = n-a-1 &
for i being Nat st 1 <= i <= len it holds it.i = Triangle(a+i);
existence
proof
deffunc F(Nat) = In(Triangle(a+$1),NAT);
n-(a+1) in NAT by A1,INT_1:5;
then reconsider s = n-a-1 as Nat;
consider z being FinSequence of NAT such that
A2: len z = s and
A3: for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus len z = n-a-1 by A2;
let i be Nat;
assume 1 <= i <= len z;
then z.i = F(i) by A3,FINSEQ_3:25;
hence thesis;
end;
uniqueness
proof
let f, g be FinSequence of NAT such that
A4: len f = n-a-1 and
A5: for i being Nat st 1 <= i <= len f holds f.i = Triangle(a+i) and
A6: len g = n-a-1 and
A7: for i being Nat st 1 <= i <= len g holds g.i = Triangle(a+i);
thus len f = len g by A4,A6;
let i be Nat such that
A8: 1 <= i <= len f;
thus f.i = Triangle(a+i) by A5,A8
.= g.i by A4,A6,A7,A8;
end;
end;
Lm26: 3 >= 2+1;
registration
cluster TriangleShift2(3,2) -> empty;
coherence
proof
len TriangleShift2(3,2) = 3-2-1 by Lm26,Def15;
hence thesis by FINSEQ_1:20;
end;
end;
theorem
TriangleShift2(4,2) = <*Triangle 3*>
proof
set f = TriangleShift2(4,2);
set g = <*Triangle(3)*>;
A1: len f = 4-2-1 by Lm26,Def15;
hence len f = len g by CARD_1:def 7;
let k;
assume 1 <= k <= len f;
then
A2: k = 1 by A1,XXREAL_0:1;
hence f.k = Triangle(2+k) by A1,Def15
.= g.k by A2;
end;
theorem Th131:
n >= a+1 implies TriangleShift2(n+1,a) = TriangleShift2(n,a)^<*Triangle(n)*>
proof
set f = TriangleShift2(n+1,a);
set g = TriangleShift2(n,a);
set h = <*T(n)*>;
assume
A1: n >= a+1;
then
A2: n+1 >= a+1 by NAT_1:13;
A3: len f = n+1-a-1 by A2,Def15;
A4: len g = n-a-1 by A1,Def15;
A5: len h = 1 by CARD_1:def 7;
A6: len(g^h) = len g + len h by FINSEQ_1:22;
hence len f = len(g^h) by A3,A4,A5;
let k be Nat such that
A7: 1 <= k and
A8: k <= len f;
A9: f.k = T(k+a) by A2,A7,A8,Def15;
per cases;
suppose
A10: k <= len g;
hence f.k = g.k by A1,A7,A9,Def15
.= (g^h).k by A7,A10,FINSEQ_1:64;
end;
suppose
A11: k > len g;
then n-a-1+1 <= k by A4,NAT_1:13;
then k = n-a by A3,A8,XXREAL_0:1;
hence f.k = h.(k - len g) by A4,A9
.= (g^h).k by A3,A4,A5,A6,A8,A11,FINSEQ_1:24;
end;
end;
theorem Th132:
a+1 <= n implies TriangleShift2(n,a) is triangular-valued
proof
set f = TriangleShift2(n,a);
assume
A1: a+1 <= n;
let x be object;
per cases;
suppose
A2: x in dom f;
then reconsider x as Nat;
1 <= x <= len f by A2,FINSEQ_3:25;
then f.x = Triangle(a+x) by A1,Def15;
hence thesis;
end;
suppose not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
registration
let m,n;
cluster m |-> Triangle(n) -> triangular-valued;
coherence
proof
set f = m|->T(n);
let x be object;
per cases;
suppose x in dom f;
hence thesis by FINSEQ_2:57;
end;
suppose not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
theorem Th133:
3 <= n implies Sum ((TriangleShift2(n,2))") = 2/3 - (n+1)/Triangle(n)
proof
defpred P[Nat] means Sum ((TriangleShift2($1,2))") = 2/3 - ($1+1)/T($1);
A1: P[3] by NUMPOLY1:13;
A2: for j being Nat st 3 <= j holds P[j] implies P[j+1]
proof
let j be Nat such that
A3: 3 <= j and
A4: P[j];
A5: T(j+1) = T(j) + (j+1) by NUMPOLY1:10;
A6: T(j) = j*(j+1)/2 by NUMPOLY1:19;
then
A7: (j*(j+1)+2*(j+1))/2 = T(j)+j+1;
A8: (j+1)/T(j) - 1/T(j) = (j+1-1)/T(j)
.= (2*j) / (j*(j+1)) by A6,XCMPLX_1:77
.= 2 / (j+1) by A3,XCMPLX_1:91
.= 2*(j+2) / ((j+2)*(j+1)) by XCMPLX_1:91
.= (j+1+1)/T(j+1) by A5,A7,XCMPLX_1:77;
A9: <*T(j)*>" = <*(T(j))"*> by NUMBER15:63;
TriangleShift2(j+1,2) = TriangleShift2(j,2) ^ <*T(j)*> by Lm26,A3,Th131;
then (TriangleShift2(j+1,2))" = (TriangleShift2(j,2))" ^ <*T(j)*>"
by NUMBER15:60;
hence Sum((TriangleShift2(j+1,2))") = Sum((TriangleShift2(j,2))")+(T(j))"
by A9,RVSUM_2:31
.= 2/3 - (j+1+1)/T(j+1) by A4,A8;
end;
for i being Nat st 3 <= i holds P[i] from NAT_1:sch 8(A1,A2);
hence thesis;
end;
:: Problem 163
theorem
s <> 2 implies
ex f being natural-valued s-element FinSequence st
f is triangular-valued with_sum_of_reciprocals_equal_1
proof
set d = T(2);
set t = T(3);
assume s <> 2;
then per cases by Lm24;
suppose s = 1;
then
reconsider f = <*T(1)*> as natural-valued s-element FinSequence;
take f;
thus f is triangular-valued;
thus f is with_sum_of_reciprocals_equal_1 by NUMPOLY1:11;
end;
suppose s = 3;
then
reconsider f = <*d,d,d*> as natural-valued s-element FinSequence;
take f;
thus f is triangular-valued;
thus f is with_sum_of_reciprocals_equal_1 by Th127;
end;
suppose s = 4;
then
reconsider f = <*d,d,t,t*> as natural-valued s-element FinSequence;
take f;
thus f is triangular-valued;
thus f is with_sum_of_reciprocals_equal_1 by Th128;
end;
suppose
A1: s >= 5;
per cases;
suppose s is odd;
then consider q being Nat such that
A2: s = 2*q+1 by ABIAN:9;
set k = q+1;
A3: now
assume k < 2+1;
then k <= 2 by NAT_1:13;
then 2*k <= 2*2 by XREAL_1:64;
then 2*k-1 <= 4-1 by XREAL_1:9;
hence contradiction by A1,A2,XXREAL_0:2;
end;
set f1 = <*d*>;
set f2 = TriangleShift2(k,2);
set f3 = (k+1)|->T(k);
set f = f1^f2^f3;
A4: len(f1) = 1 by CARD_1:def 7;
A5: len(f2) = k-2-1 by A3,Def15;
A6: len(f1^f2) = len(f1) + len(f2) by FINSEQ_1:22;
len f = len(f1^f2) + len(f3) by FINSEQ_1:22
.= s by A2,A4,A5,A6;
then reconsider f as natural-valued s-element FinSequence
by CARD_1:def 7;
take f;
f2 is triangular-valued by A3,Th132;
hence f is triangular-valued;
A7: f1" = <*d"*> by NUMBER15:63;
A8: Sum(f2") = 2/3 - (k+1)/T(k) by A3,Th133;
A9: f3" = (k+1)|->(T(k)") by Th43;
A10: (f1^f2)" = f1"^f2" by NUMBER15:60;
thus Sum(f") = Sum((f1^f2)"^f3") by NUMBER15:60
.= Sum((f1^f2)") + Sum(f3") by RVSUM_2:32
.= Sum(f1") + Sum(f2") + Sum(f3") by A10,RVSUM_2:32
.= d" + 2/3 - (k+1)/T(k) + (k+1)*(T(k)")
by A7,A8,A9,RVSUM_2:36
.= 1 by NUMPOLY1:12;
end;
suppose s is even;
then consider k being Nat such that
A11: s = 2*k;
now
assume k < 2+1;
then k <= 2 by NAT_1:13;
then 2*k <= 2*2 by XREAL_1:64;
hence contradiction by A1,A11,XXREAL_0:2;
end;
then per cases by XXREAL_0:1;
suppose k = 3;
then reconsider f = <*t,t,t,t,t,t*>
as natural-valued s-element FinSequence by A11;
take f;
thus f is triangular-valued;
thus f is with_sum_of_reciprocals_equal_1 by Th129;
end;
suppose
A12: k > 3;
set f1 = <*t,t*>;
set f2 = TriangleShift2(k,2);
set f3 = (k+1)|->T(k);
set f = f1^f2^f3;
A13: len(f1) = 2 by CARD_1:def 7;
A14: len(f2) = k-2-1 by A12,Lm26,Def15;
A15: len(f1^f2) = len(f1) + len(f2) by FINSEQ_1:22;
len f = len(f1^f2) + len(f3) by FINSEQ_1:22
.= s by A11,A13,A14,A15;
then reconsider f as natural-valued s-element FinSequence
by CARD_1:def 7;
take f;
f2 is triangular-valued by A12,Lm26,Th132;
hence f is triangular-valued;
A16: f1" = <*t",t"*> by NUMBER15:64;
A17: Sum <*t",t"*> = t"+t" by RVSUM_2:34;
A18: Sum(f2") = 2/3 - (k+1)/T(k) by A12,Th133;
A19: f3" = (k+1)|->(T(k)") by Th43;
A20: (f1^f2)" = f1"^f2" by NUMBER15:60;
thus Sum(f") = Sum((f1^f2)"^f3") by NUMBER15:60
.= Sum((f1^f2)") + Sum(f3") by RVSUM_2:32
.= Sum(f1") + Sum(f2") + Sum(f3") by A20,RVSUM_2:32
.= t"+t" + 2/3 - (k+1)/T(k) + (k+1)*(T(k)")
by A16,A17,A18,A19,RVSUM_2:36
.= 1 by NUMPOLY1:13;
end;
end;
end;
end;
begin :: Problem 165
definition
let f be complex-valued FinSequence;
attr f is with_sum_of_squares_of_reciprocals_equal_1 means
Sum (f" ^2) = 1;
end;
Lm27:
now
let s;
thus s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6
proof
per cases;
suppose s <= 5;
then s = 0 or ... or s = 5;
hence thesis;
end;
suppose s > 5;
then s >= 5+1 by NAT_1:13;
hence thesis;
end;
end;
end;
theorem Th135:
<*1*> is with_sum_of_squares_of_reciprocals_equal_1
proof
set f = <*1*>;
f" = <*1"*> by NUMBER15:63;
hence Sum (f" ^2) = Sum <*1^2*> by RVSUM_1:55
.= 1;
end;
theorem Th136:
<*2,2,2,2*> is with_sum_of_squares_of_reciprocals_equal_1
proof
set f = <*2,2,2,2*>;
f" = <*2",2",2",2"*> by Th15;
then f" ^2 = <*2"^2,2"^2,2"^2,2"^2*> by Th10;
hence Sum (f" ^2) = 1/4+1/4+1/4+1/4 by RVSUM_1:142
.= 1;
end;
theorem Th137:
<*2,2,2,3,3,6*> is with_sum_of_squares_of_reciprocals_equal_1
proof
set f = <*2,2,2,3,3,6*>;
f" = <*2",2",2",3",3",6"*> by Th17;
then f" ^2 = <*2"^2,2"^2,2"^2,3"^2,3"^2,6"^2*> by Th12;
hence Sum (f" ^2) = 1/4+1/4+1/4+1/9+1/9+1/36 by Th22
.= 1;
end;
theorem Th138:
<*2,2,2,4,4,4,4*> is with_sum_of_squares_of_reciprocals_equal_1
proof
set f = <*2,2,2,4,4,4,4*>;
f" = <*2",2",2",4",4",4",4"*> by Th18;
then f" ^2 = <*2"^2,2"^2,2"^2,4"^2,4"^2,4"^2,4"^2*> by Th13;
hence Sum (f" ^2) = 1/4+1/4+1/4+1/16+1/16+1/16+1/16 by Th23
.= 1;
end;
theorem Th139:
<*2,2,2,3,3,7,14,21*> is with_sum_of_squares_of_reciprocals_equal_1
proof
set f = <*2,2,2,3,3,7,14,21*>;
f" = <*2",2",2",3",3",7",14",21"*> by Th19;
then f" ^2 = <*2"^2,2"^2,2"^2,3"^2,3"^2,7"^2,14"^2,21"^2*> by Th14;
hence Sum (f" ^2) = 1/4+1/4+1/4+1/9+1/9+1/49+1/196+1/441 by Th24
.= 1;
end;
theorem Th140:
for f being s-element natural-valued FinSequence
st f is with_sum_of_squares_of_reciprocals_equal_1
holds f|(s-1) ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>
is with_sum_of_squares_of_reciprocals_equal_1
proof
let f be s-element natural-valued FinSequence such that
A1: f is with_sum_of_squares_of_reciprocals_equal_1;
set g = f|(s-1) ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>;
<* 2*f.s,2*f.s,2*f.s,2*f.s *>" = <*(2*f.s)",(2*f.s)",(2*f.s)",(2*f.s)"*>
by Th15;
then
<* 2*f.s,2*f.s,2*f.s,2*f.s *>"^2
= <*(2*f.s)"^2,(2*f.s)"^2,(2*f.s)"^2,(2*f.s)"^2*> by Th10;
then
A2: Sum(<* 2*f.s,2*f.s,2*f.s,2*f.s *>"^2)
= (2*f.s)"^2+(2*f.s)"^2+(2*f.s)"^2+(2*f.s)"^2 by Th20;
A3: (2*f.s)"^2 = ((2*f.s)*(2*f.s))" by XCMPLX_1:204
.= (4*(f.s*f.s))"
.= 4"*(f.s*f.s)" by XCMPLX_1:204;
A4: (f|(s-1))"^2 = (f"|(s-1))^2 by NUMBER15:61
.= f"^2|(s-1) by NUMBER15:62;
A5: Sum(f"^2|(s-1)) = Sum(f"^2) - (f"^2).s by Th4;
A6: (f"^2).s = (f".s)^2 by VALUED_1:11
.= (f.s)"^2 by VALUED_1:10;
g" = (f|(s-1))" ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>" by NUMBER15:60;
then g"^2 = (f|(s-1))"^2 ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>"^2 by NUMBER15:59;
hence
Sum (g" ^2) = 1-(f.s)"^2+4*4"*(f.s*f.s)" by A1,A2,A3,A4,A5,A6,RVSUM_2:32
.= 1-(f.s)"^2+4*(2"*(f.s)")^2 by XCMPLX_1:204
.= 1;
end;
registration
let s be positive Nat;
let a,b,c,d be positive Real;
let f be s-element positive real-valued FinSequence;
cluster <* a*f.s,b*f.s,c*f.s,d*f.s *> -> positive-yielding;
coherence
proof
A1: len f = s by CARD_1:def 7;
0+1 <= s by NAT_1:13;
then s in dom f by A1,FINSEQ_3:25;
then f.s is positive by RVSUM_3:def 1;
hence thesis;
end;
end;
Lm28:
for f being s-element positive natural-valued FinSequence
st f is with_sum_of_squares_of_reciprocals_equal_1
ex g being s+3-element positive natural-valued FinSequence
st g is with_sum_of_squares_of_reciprocals_equal_1
proof
let f be s-element positive natural-valued FinSequence;
set g = f|(s-1) ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>;
assume
A1: f is with_sum_of_squares_of_reciprocals_equal_1;
reconsider g as s+3-element positive natural-valued FinSequence;
take g;
thus thesis by A1,Th140;
end;
theorem
for f being s-element positive natural-valued FinSequence
st f is with_sum_of_squares_of_reciprocals_equal_1
ex g being s+3*n-element positive natural-valued FinSequence
st g is with_sum_of_squares_of_reciprocals_equal_1
proof
let f be s-element positive natural-valued FinSequence;
set g = f|(s-1) ^ <* 2*f.s,2*f.s,2*f.s,2*f.s *>;
assume
A1: f is with_sum_of_squares_of_reciprocals_equal_1;
defpred P[Nat] means
ex g being s+3*$1-element positive natural-valued FinSequence
st g is with_sum_of_squares_of_reciprocals_equal_1;
A2: P[0] by A1;
A3: for k st P[k] holds P[k+1]
proof
let k;
assume ex g being s+3*k-element positive natural-valued FinSequence st
g is with_sum_of_squares_of_reciprocals_equal_1;
then ex h being s+3*k+3-element positive natural-valued FinSequence
st h is with_sum_of_squares_of_reciprocals_equal_1 by Lm28;
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
Lm29:
now
let s;
assume s > 1;
then s >= 1+1 by NAT_1:13;
then s" <= 1/2 by XREAL_1:85;
then s"^2 <= (1/2)^2 by XREAL_1:66;
hence s"^2 <= 1/4;
end;
Lm30:
now
let s;
assume s > 2;
then s >= 2+1 by NAT_1:13;
then s" <= 1/3 by XREAL_1:85;
then s"^2 <= (1/3)^2 by XREAL_1:66;
hence s"^2 <= 1/9;
end;
scheme STEP2a { N() -> Nat, P[Nat] } :
for k being Nat st k >= N() holds P[k]
provided
A1: P[N()] and
A2: P[N()+1] and
A3: for k being Nat st k >= N() & P[k] & P[k+1] holds P[k+2]
proof
let k such that
A4: k >= N();
defpred Q[Nat] means $1 >= N() implies P[$1] & P[$1+1];
A5: for m being Nat st Q[m] holds Q[m+1]
proof
let m;
A6: m+2 = (m+1)+1;
assume
A7: Q[m];
assume m+1 >= N();
then per cases by XXREAL_0:1;
suppose m+1 = N();
hence thesis by A1,A2;
end;
suppose m+1 > N();
hence thesis by A3,A6,A7,NAT_1:13;
end;
end;
A8: Q[0] by A1,A2;
for k being Nat holds Q[k] from NAT_1:sch 2(A8,A5);
hence thesis by A4;
end;
scheme STEP2 { P[Nat] } : for k being Nat holds P[k]
provided
A1: for k being Nat holds P[2*k] & P[2*k+1]
proof
let k;
consider a such that
A2: k = 2*a+(0 qua Nat) or ... or k = 2*a+(2-1) by NUMBER02:22;
consider m such that
0 <= m and
A3: m <= 0+1 and
A4: k = 2*a+m by A2;
m = 0 or ... or m = 1 by A3;
hence thesis by A1,A4;
end;
scheme STEP3 { P[Nat] } : for k being Nat holds P[k]
provided
A1: for k being Nat holds P[3*k] & P[3*k+1] & P[3*k+2]
proof
let k;
consider a such that
A2: k = 3*a+(0 qua Nat) or ... or k = 3*a+(3-1) by NUMBER02:22;
consider m such that
0 <= m and
A3: m <= 0+2 and
A4: k = 3*a+m by A2;
m = 0 or ... or m = 2 by A3;
hence thesis by A1,A4;
end;
scheme STEP4 { P[Nat] } : for k being Nat holds P[k]
provided
A1: for k being Nat holds P[4*k] & P[4*k+1] & P[4*k+2] & P[4*k+3]
proof
let k;
consider a such that
A2: k = 4*a+(0 qua Nat) or ... or k = 4*a+(4-1) by NUMBER02:22;
consider m such that
0 <= m and
A3: m <= 0+3 and
A4: k = 4*a+m by A2;
m = 0 or ... or m = 3 by A3;
hence thesis by A1,A4;
end;
:: Problem 165
theorem
(ex f being s-element positive natural-valued FinSequence st
f is with_sum_of_squares_of_reciprocals_equal_1)
iff s = 1 or s = 4 or s >= 6
proof
defpred S[Nat] means
ex f being $1-element positive natural-valued FinSequence st
f is with_sum_of_squares_of_reciprocals_equal_1;
thus S[s] implies s = 1 or s = 4 or s >= 6
proof
given f being s-element positive natural-valued FinSequence such that
A1: f is with_sum_of_squares_of_reciprocals_equal_1;
A2: f is FinSequence of NAT by FINSEQ_1:103;
per cases by Lm27;
suppose s = 1 or s = 4 or s >= 6;
hence thesis;
end;
suppose s = 2;
then consider a,b being Element of NAT such that
A3: f = <*a,b*> by A2,FINSEQ_2:100;
reconsider a,b as positive Nat by A3;
<*a,b*>" = <*a",b"*> by NUMBER15:64;
then <*a,b*>"^2 = <*a"^2,b"^2*> by Th8;
then
A4: Sum (<*a,b*>" ^2) = a"^2 + b"^2 by RVSUM_2:34;
a >= 1 & b >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose a = 1 or b = 1;
hence thesis by A1,A3,A4,XREAL_1:6;
end;
suppose a > 1 & b > 1;
then a"^2 <= 1/4 & b"^2 <= 1/4 by Lm29;
then a"^2+b"^2 <= 1/4+1/4 by XREAL_1:7;
hence thesis by A1,A3,A4;
end;
end;
suppose s = 3;
then consider a,b,c being Element of NAT such that
A5: f = <*a,b,c*> by A2,FINSEQ_2:103;
reconsider a,b,c as positive Nat by A5;
<*a,b,c*>" = <*a",b",c"*> by NUMBER15:65;
then <*a,b,c*>"^2 = <*a"^2,b"^2,c"^2*> by Th9;
then
A6: Sum (<*a,b,c*>" ^2) = a"^2 + b"^2 + c"^2 by RVSUM_2:35;
a >= 1 & b >= 1 & c >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose a = 1 or b = 1 or c = 1;
then a"^2+b"^2+c"^2 > 1+0 or a"^2+c"^2+b"^2 > 1+0
or b"^2+c"^2+a"^2 > 1+0 by XREAL_1:8;
hence thesis by A1,A5,A6;
end;
suppose a > 1 & b > 1 & c > 1;
then
A7: a"^2 <= 1/4 & b"^2 <= 1/4 & c"^2 <= 1/4 by Lm29;
then a"^2+b"^2 <= (1/2)^2+(1/2)^2 by XREAL_1:7;
then a"^2+b"^2+c"^2 <= (1/2)^2+(1/2)^2+(1/2)^2 by A7,XREAL_1:7;
hence thesis by A1,A5,A6;
end;
end;
suppose s = 5;
then consider a,b,c,d,e being Element of NAT such that
A8: f = <*a,b,c,d,e*> by A2,Th6;
reconsider a,b,c,d,e as positive Nat by A8;
<*a,b,c,d,e*>" = <*a",b",c",d",e"*> by Th16;
then <*a,b,c,d,e*>"^2 = <*a"^2,b"^2,c"^2,d"^2,e"^2*> by Th11;
then
A9: Sum (<*a,b,c,d,e*>" ^2) = a"^2 + b"^2 + c"^2 + d"^2 + e"^2 by Th21;
A10: a"^2 + b"^2 + c"^2 + d"^2 + e"^2 = a"^2 + b"^2 + c"^2 + e"^2 + d"^2;
A11: a"^2 + b"^2 + c"^2 + d"^2 + e"^2 = b"^2 + c"^2 + d"^2 + e"^2 + a"^2;
A12: a"^2 + b"^2 + c"^2 + d"^2 + e"^2 = a"^2 + b"^2 + d"^2 + e"^2 + c"^2;
a >= 1 & b >= 1 & c >= 1 & d >= 1 & e >= 1 by NAT_1:14;
then per cases by XXREAL_0:1;
suppose a = 1;
then b"^2+c"^2+d"^2+e"^2+a"^2 > 1+0 by XREAL_1:8;
hence thesis by A1,A8,A9;
end;
suppose b = 1;
then a"^2+c"^2+d"^2+e"^2+b"^2 > 1+0 by XREAL_1:8;
hence thesis by A1,A8,A9;
end;
suppose c = 1;
then a"^2+b"^2+d"^2+e"^2+c"^2 > 1+0 by XREAL_1:8;
hence thesis by A1,A8,A9;
end;
suppose d = 1;
then a"^2+b"^2+c"^2+e"^2+d"^2 > 1+0 by XREAL_1:8;
hence thesis by A1,A8,A9;
end;
suppose e = 1;
hence thesis by A1,A8,A9,XREAL_1:8;
end;
suppose that
A13: a > 1 and
A14: b > 1 and
A15: c > 1 and
A16: d > 1 and
A17: e > 1;
A18: b >= 1+1 by A14,NAT_1:13;
A19: c >= 1+1 by A15,NAT_1:13;
A20: d >= 1+1 by A16,NAT_1:13;
A21: e >= 1+1 by A17,NAT_1:13;
A22: a"^2 <= 1/4 by A13,Lm29;
A23: b"^2 <= 1/4 by A14,Lm29;
A24: c"^2 <= 1/4 by A15,Lm29;
A25: d"^2 <= 1/4 by A16,Lm29;
A26: e"^2 <= 1/4 by A17,Lm29;
a >= 1+1 by A13,NAT_1:13;
then per cases by A18,A19,A20,A21,XXREAL_0:1;
suppose a = 2 & b = 2 & c = 2 & d = 2 & e = 2;
hence thesis by A1,A8,A9;
end;
suppose a > 2;
then
A27: a"^2 <= 1/9 by Lm30;
per cases by A18,XXREAL_0:1;
suppose
A28: b = 2;
per cases by A19,XXREAL_0:1;
suppose
A29: c = 2;
per cases by A20,XXREAL_0:1;
suppose
A30: d = 2;
per cases by A21,XXREAL_0:1;
suppose e = 2;
hence thesis by A1,A8,A9,A11,A28,A29,A30,XREAL_1:6;
end;
suppose e > 2;
then e"^2 <= 1/9 by Lm30;
then
A31: a"^2+e"^2 <= 1/9+1/9 by A27,XREAL_1:7;
b"^2+c"^2 <= 1/4+1/4 by A23,A24,XREAL_1:7;
then b"^2+c"^2+d"^2 <= 2/4+1/4 by A25,XREAL_1:7;
then a"^2+e"^2+(b"^2+c"^2+d"^2) <= 2/9+3/4
by A31,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose d > 2;
then d"^2 <= 1/9 by Lm30;
then
A32: a"^2+d"^2 <= 1/9+1/9 by A27,XREAL_1:7;
b"^2+c"^2 <= 1/4+1/4 by A23,A24,XREAL_1:7;
then b"^2+c"^2+e"^2 <= 2/4+1/4 by A26,XREAL_1:7;
then a"^2+d"^2+(b"^2+c"^2+e"^2) <= 2/9+3/4 by A32,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose c > 2;
then c"^2 <= 1/9 by Lm30;
then
A33: a"^2+c"^2 <= 1/9+1/9 by A27,XREAL_1:7;
b"^2+d"^2 <= 1/4+1/4 by A23,A25,XREAL_1:7;
then b"^2+d"^2+e"^2 <= 2/4+1/4 by A26,XREAL_1:7;
then a"^2+c"^2+(b"^2+d"^2+e"^2) <= 2/9+3/4 by A33,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose b > 2;
then b"^2 <= 1/9 by Lm30;
then
A34: a"^2+b"^2 <= 1/9+1/9 by A27,XREAL_1:7;
c"^2+d"^2 <= 1/4+1/4 by A24,A25,XREAL_1:7;
then c"^2+d"^2+e"^2 <= 1/4+1/4+1/4 by A26,XREAL_1:7;
then a"^2+b"^2+(c"^2+d"^2+e"^2) <= 2/9+3/4 by A34,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose that
A35: a = 2 and
A36: b > 2;
A37: b"^2 <= 1/9 by A36,Lm30;
per cases by A19,XXREAL_0:1;
suppose
A38: c = 2;
per cases by A20,XXREAL_0:1;
suppose
A39: d = 2;
per cases by A21,XXREAL_0:1;
suppose e = 2;
then a"^2+c"^2+d"^2+e"^2+b"^2 > 1+0 by A35,A38,A39,XREAL_1:6;
hence thesis by A1,A8,A9;
end;
suppose e > 2;
then e"^2 <= 1/9 by Lm30;
then
A40: b"^2+e"^2 <= 1/9+1/9 by A37,XREAL_1:7;
a"^2+c"^2 <= 1/4+1/4 by A22,A24,XREAL_1:7;
then a"^2+c"^2+d"^2 <= 2/4+1/4 by A25,XREAL_1:7;
then b"^2+e"^2+(a"^2+c"^2+d"^2) <= 2/9+3/4 by A40,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose d > 2;
then d"^2 <= 1/9 by Lm30;
then
A41: b"^2+d"^2 <= 1/9+1/9 by A37,XREAL_1:7;
a"^2+c"^2 <= 1/4+1/4 by A22,A24,XREAL_1:7;
then a"^2+c"^2+e"^2 <= 2/4+1/4 by A26,XREAL_1:7;
then b"^2+d"^2+(a"^2+c"^2+e"^2) <= 2/9+3/4 by A41,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose c > 2;
then c"^2 <= 1/9 by Lm30;
then
A42: b"^2+c"^2 <= 1/9+1/9 by A37,XREAL_1:7;
a"^2+d"^2 <= 1/4+1/4 by A22,A25,XREAL_1:7;
then a"^2+d"^2+e"^2 <= 2/4+1/4 by A26,XREAL_1:7;
then b"^2+c"^2+(a"^2+d"^2+e"^2) <= 2/9+3/4 by A42,XREAL_1:7;
hence thesis by A1,A8,A9;
end;
end;
suppose that
A43: a = 2 & b = 2 and
A44: c > 2;
A45: c"^2 <= 1/9 by A44,Lm30;
per cases by A20,A21,XXREAL_0:1;
suppose d = 2 & e = 2;
hence thesis by A1,A8,A9,A12,A43,XREAL_1:6;
end;
suppose that
A46: d = 2 and
A47: e > 2;
e"^2 <= 1/9 by A47,Lm30;
then c"^2+e"^2 <= 1/9+1/9 by A45,XREAL_1:7;
then a"^2+b"^2+d"^2+(c"^2+e"^2) <= 3/4+2/9 by A43,A46,XREAL_1:6;
hence thesis by A1,A8,A9;
end;
suppose d > 2;
then d"^2 <= 1/9 by Lm30;
then d"^2+e"^2 <= 1/9+1/4 by A26,XREAL_1:7;
then c"^2+(d"^2+e"^2) <= 1/9+13/36 by A45,XREAL_1:7;
then a"^2+b"^2+(c"^2+(d"^2+e"^2)) <= 2/4+17/36 by A43,XREAL_1:6;
hence thesis by A1,A8,A9;
end;
end;
suppose a = 2 & b = 2 & c = 2 & d > 2 & e = 2;
hence thesis by A1,A8,A9,A10,XREAL_1:6;
end;
suppose that
A48: a = 2 & b = 2 & c = 2 and
A49: d > 2 & e > 2;
d"^2 <= 1/9 & e"^2 <= 1/9 by A49,Lm30;
then d"^2+e"^2 <= 1/9+1/9 by XREAL_1:7;
then a"^2+b"^2+c"^2+(d"^2+e"^2) <= 3/4+2/9 by A48,XREAL_1:6;
hence thesis by A1,A8,A9;
end;
suppose a = 2 & b = 2 & c = 2 & d = 2 & e > 2;
hence thesis by A1,A8,A9,XREAL_1:6;
end;
end;
end;
end;
assume s = 1 or s = 4 or s >= 6;
then per cases;
suppose s = 1;
then
reconsider f = <*1*> as s-element positive natural-valued FinSequence;
take f;
thus thesis by Th135;
end;
suppose s = 4;
then reconsider f = <*2,2,2,2*>
as s-element positive natural-valued FinSequence;
take f;
thus thesis by Th136;
end;
suppose
A50: s >= 6;
defpred P[Nat] means $1 >= 6 implies S[$1];
A51: for k holds P[3*k] & P[3*k+1] & P[3*k+2]
proof
let k;
thus P[3*k]
proof
assume
A52: 3*k >= 6;
then 3*k >= 3*2;
then
A53: k >= 2 by XREAL_1:68;
defpred Q[Nat] means $1 >= 2 implies P[3*$1];
A54: Q[0];
A55: for m st Q[m] holds Q[m+1]
proof
let m;
assume that
A56: Q[m] and
A57: m+1 >= 2;
m >= 2-1 by A57,XREAL_1:20;
then per cases by NAT_1:23;
suppose m = 1;
hence P[3*(m+1)] by Th137;
end;
suppose
A58: m >= 2;
then 3*m >= 3*2 by XREAL_1:64;
then S[3*m+3] by A56,A58,Lm28;
hence P[3*(m+1)];
end;
end;
for m holds Q[m] from NAT_1:sch 2(A54,A55);
hence S[3*k] by A52,A53;
end;
thus P[3*k+1]
proof
assume
A59: 3*k+1 >= 6;
A60: now
assume k < 1+1;
then k <= 1 by NAT_1:13;
then 3*k <= 3*1 by XREAL_1:64;
then 3*k+1 <= 3+1 by XREAL_1:6;
hence contradiction by A59,XXREAL_0:2;
end;
defpred Q[Nat] means $1 >= 2 implies P[3*$1+1];
A61: Q[0];
A62: for m st Q[m] holds Q[m+1]
proof
let m;
assume that
A63: Q[m] and
A64: m+1 >= 2;
m >= 2-1 by A64,XREAL_1:20;
then per cases by NAT_1:23;
suppose m = 1;
hence P[3*(m+1)+1] by Th138;
end;
suppose
A65: m >= 2;
then 3*m+1 >= 3*2 by XREAL_1:64,145;
then S[3*m+1+3] by A63,A65,Lm28;
hence P[3*(m+1)+1];
end;
end;
for m holds Q[m] from NAT_1:sch 2(A61,A62);
hence S[3*k+1] by A59,A60;
end;
thus P[3*k+2]
proof
assume
A66: 3*k+2 >= 6;
A67: now
assume k < 1+1;
then k <= 1 by NAT_1:13;
then 3*k <= 3*1 by XREAL_1:64;
then 3*k+2 <= 3+2 by XREAL_1:6;
hence contradiction by A66,XXREAL_0:2;
end;
defpred Q[Nat] means $1 >= 2 implies P[3*$1+2];
A68: Q[0];
A69: for m st Q[m] holds Q[m+1]
proof
let m;
assume that
A70: Q[m] and
A71: m+1 >= 2;
m >= 2-1 by A71,XREAL_1:20;
then per cases by NAT_1:23;
suppose m = 1;
hence P[3*(m+1)+2] by Th139;
end;
suppose
A72: m >= 2;
then
A73: 3*m >= 3*2 by XREAL_1:64;
3*m+2 > 3*m+0 by XREAL_1:6;
then 3*m+2 >= 3*2 by A73,XXREAL_0:2;
then S[3*m+2+3] by A70,A72,Lm28;
hence P[3*(m+1)+2];
end;
end;
for m holds Q[m] from NAT_1:sch 2(A68,A69);
hence S[3*k+2] by A66,A67;
end;
end;
for k holds P[k] from STEP3(A51);
hence thesis by A50;
end;
end;
begin :: Problem 169
definition
let s be Nat;
let f be (s+1)-element complex-valued FinSequence;
attr f is a_solution_of_Sierp169 means
Sum (((f|s)(#)(f|s)(#)(f|s))") = 1 / ((f.(s+1))|^3);
end;
registration
let a,b,c,d be object;
cluster <*a,b,c,d*> -> 3+1-element;
coherence;
end;
theorem Th143:
<*12,15,20,10*> is a_solution_of_Sierp169
proof
set f = <*12,15,20,10*>;
set s = 3;
set g = f|s;
(g(#)g)" = g"(#)g" by Th50;
then
A1: (g(#)g(#)g)" = g"(#)g"(#)g" by Th50;
A2: g" = <*12",15",20"*> by NUMBER15:65;
A3: <*12",15",20"*>(#)<*12",15",20"*> = <*12"*12",15"*15",20"*20"*>
by FINSEQ_9:46;
A4: <*12"*12",15"*15",20"*20"*>(#)<*12",15",20"*>
= <*12"*12"*12",15"*15"*15",20"*20"*20"*> by FINSEQ_9:46;
f.(s+1)|^3 = f.(s+1)*f.(s+1)*f.(s+1) by POLYEQ_5:2;
hence 1 / ((f.(s+1))|^3) = 12"*12"*12"+15"*15"*15"+20"*20"*20"
.= Sum ((g(#)g(#)g)") by A1,A2,A3,A4,RVSUM_2:35;
end;
registration
let a,b,c,d,e be object;
cluster <*a,b,c,d,e*> -> 4+1-element;
coherence;
end;
theorem Th144:
<*455,780,1092,5460,420*> is a_solution_of_Sierp169
proof
set f = <*455,780,1092,5460,420*>;
set s = 4;
set g = f|s;
A1: f = <*455,780,1092,5460*>^<*420*> by FINSEQ_4:75;
(g(#)g)" = g"(#)g" by Th50;
then
A2: (g(#)g(#)g)" = g"(#)g"(#)g" by Th50;
A3: g" = <*455",780",1092",5460"*> by A1,Th15;
A4: <*455",780",1092",5460"*>(#)<*455",780",1092",5460"*>
= <*455"*455",780"*780",1092"*1092",5460"*5460"*>
by FINSEQ_9:47;
A5: <*455"*455",780"*780",1092"*1092",5460"*5460"*>(#)<*455",780",1092",5460"*>
= <*455"*455"*455",780"*780"*780",1092"*1092"*1092",5460"*5460"*5460"*>
by FINSEQ_9:47;
f.(s+1)|^3 = f.(s+1)*f.(s+1)*f.(s+1) by POLYEQ_5:2;
hence 1 / ((f.(s+1))|^3)
= 455"*455"*455"+780"*780"*780"+1092"*1092"*1092"+5460"*5460"*5460"
.= Sum ((g(#)g(#)g)") by A2,A3,A4,A5,Th20;
end;
registration
let s be positive Nat;
let n be Nat;
let c be Complex;
let f be s+n-element complex-valued FinSequence;
let g be 4-element FinSequence;
cluster (c(#)f|(s-1)) ^ g -> s+2+1-element;
coherence
proof
len f = s+n by CARD_1:def 7;
then len(f|(s-1)) = s-1 by FINSEQ_1:59,XREAL_1:6;
hence thesis;
end;
end;
theorem Th145:
for f being s+1-element complex-valued FinSequence
st f is a_solution_of_Sierp169 holds
(10(#)f|(s-1)) ^ <* 12*f.s,15*f.s,20*f.s,10*f.(s+1) *>
is a_solution_of_Sierp169
proof
let f be s+1-element complex-valued FinSequence such that
A1: f is a_solution_of_Sierp169;
set x = f.s, y = f.(s+1);
set a = 12*x, b = 15*x, c = 20*x, d = 10*y;
set F = <*a,b,c*>;
set G = <*a,b,c,d*>;
set J = <*d*>;
set S1 = f|(s-1);
set Z = 10(#)S1;
set g = Z^G;
set f1 = Z^F;
set h = g|(s+2);
A2: g = Z^F^J by FINSEQ_1:32;
A3: len f = s+1 by CARD_1:def 7;
A4: len S1 = len Z by COMPLSP2:3;
s-1 <= s by XREAL_1:147;
then s-1 <= s+1 by XREAL_1:145;
then
A5: len Z = s-1 by A3,A4,FINSEQ_1:59;
len F = 3 by CARD_1:def 7;
then
A6: s+2 = len Z + len F by A5
.= len(Z^F) by FINSEQ_1:22;
then
A7: h" = Z"^F" by A2,NUMBER15:60;
(h(#)h)" = h"(#)h" by Th50;
then
A8: (h(#)h(#)h)" = h"(#)h"(#)h" by Th50;
A9: (g.(s+3))|^3 = g.(s+3)*g.(s+3)*g.(s+3) by POLYEQ_5:2;
len(Z") = len(Z");
then
A10: (Z"^F")(#)(Z"^F")(#)(Z"^F") = ((Z"(#)Z")^(F"(#)F")) (#) (Z"^F")
by EULRPART:8;
consider k such that
A11: s = k + 1 by NAT_1:6;
A12: f|s|k = f|k by A11,FINSEQ_1:82,NAT_1:11;
A13: (f|s).s = x by FINSEQ_3:112;
<*x*>(#)<*x*> = <*x*x*> by RVSUM_2:26;
then
A14: <*x*>(#)<*x*>(#)<*x*> = <*x*x*x*> by RVSUM_2:26;
len S1 = len S1;
then
A15: (S1^<*x*>)(#)(S1^<*x*>)(#)(S1^<*x*>)
= (S1(#)S1(#)S1)^(<*x*>(#)<*x*>(#)<*x*>) by Th52;
A16: <*x*x*x*>" = <*(x*x*x)"*> by NUMBER15:63;
len(f|s) = s by CARD_1:def 7;
then f|s = S1^<*x*> by A11,A12,A13,RFINSEQ:7;
then ((f|s)(#)(f|s)(#)(f|s))" = (S1(#)S1(#)S1)"^<*x*x*x*>"
by A14,A15,NUMBER15:60;
then
A17: Sum((S1(#)S1(#)S1)") + Sum <*(x*x*x)"*> = 1 / (y|^3) by A1,A16,RVSUM_2:32;
A18: Z" = 10"(#)S1" by NUMBER15:58;
(S1(#)S1)" = S1"(#)S1" by Th50;
then
A19: (S1(#)S1(#)S1)" = S1"(#)S1"(#)S1" by Th50;
(10"(#)S1")(#)(10"(#)S1") = ((10")*(10"))(#)(S1"(#)S1") by Th51;
then
A20: (10"(#)S1")(#)(10"(#)S1")(#)(10"(#)S1")
= (10"*10"*10")(#)(S1"(#)S1"(#)S1") by Th51;
A21: y|^3 = y*y*y by POLYEQ_5:2;
A22: F" = <*a",b",c"*> by NUMBER15:65;
then F"(#)F" = <*a"*a",b"*b",c"*c"*> by FINSEQ_9:46;
then F"(#)F"(#)F" = <*a"*a"*a",b"*b"*b",c"*c"*c"*> by A22,FINSEQ_9:46;
then
A23: Sum(F"(#)F"(#)F") = a"*a"*a"+b"*b"*b"+c"*c"*c" by RVSUM_2:35;
now
let c1,c2,c3;
thus (c1*c2*c3)" = (c1*c2)"*c3" by XCMPLX_1:204
.= c1"*c2"*c3" by XCMPLX_1:204;
end;
then
A24: a"*a"*a" = (a*a*a)" & b"*b"*b" = (b*b*b)" & c"*c"*c" = (c*c*c)";
A25: (x*x*x)"*(12*12*12)" = (x*x*x*(12*12*12))" by XCMPLX_1:204
.= (a*a*a)";
A26: (x*x*x)"*(15*15*15)" = (x*x*x*(15*15*15))" by XCMPLX_1:204
.= (b*b*b)";
A27: (x*x*x)"*(20*20*20)" = (x*x*x*(20*20*20))" by XCMPLX_1:204
.= (c*c*c)";
dom((Z"(#)Z")) = dom(Z") /\ dom(Z") by VALUED_1:def 4
.= dom(Z");
then len((Z"(#)Z")) = len(Z") by FINSEQ_3:29;
then
(h(#)h(#)h)" = (Z"(#)Z"(#)Z") ^ (F"(#)F"(#)F") by A7,A8,A10,EULRPART:8;
hence Sum((h(#)h(#)h)") = Sum (Z"(#)Z"(#)Z") + Sum (F"(#)F"(#)F")
by RVSUM_2:32
.= Sum (Z"(#)Z"(#)Z") + a"*a"*a"+b"*b"*b"+c"*c"*c" by A23
.= (1000")*(1/(y*y*y)-(x*x*x)") + a"*a"*a"+b"*b"*b"+c"*c"*c"
by A17,A18,A19,A20,A21,RVSUM_2:38
.= (1/1000)*(1/(y*y*y)) by A24,A25,A26,A27
.= 1/(1000*(y*y*y)) by XCMPLX_1:102
.= 1 / ((g.(s+2+1))|^3) by A2,A6,A9;
end;
registration
let s be positive Nat;
let a,b,c,d be positive Real;
let f be s+1-element positive real-valued FinSequence;
cluster <* a*f.s,b*f.s,c*f.s,d*f.(s+1) *> -> positive-yielding;
coherence
proof
A1: len f = s+1 by CARD_1:def 7;
A2: 0+1 <= s by NAT_1:13;
s <= s+1 by XREAL_1:145;
then s in dom f by A1,A2,FINSEQ_3:25;
then
A3: f.s is positive by RVSUM_3:def 1;
1 <= s+1 by NAT_1:11;
then s+1 in dom f by A1,FINSEQ_3:25;
then f.(s+1) is positive by RVSUM_3:def 1;
hence thesis by A3;
end;
end;
Lm31:
for f being s+1-element positive natural-valued FinSequence
st f is a_solution_of_Sierp169
ex g being s+2+1-element positive natural-valued FinSequence
st g is a_solution_of_Sierp169
proof
let f be s+1-element positive natural-valued FinSequence;
set g = (10(#)f|(s-1)) ^ <* 12*f.s,15*f.s,20*f.s,10*f.(s+1) *>;
assume
A1: f is a_solution_of_Sierp169;
reconsider g as s+2+1-element positive natural-valued FinSequence;
take g;
thus thesis by A1,Th145;
end;
theorem Th146:
for f being s+1-element complex-valued FinSequence
st f is a_solution_of_Sierp169 holds n(#)f is a_solution_of_Sierp169
proof
let f be s+1-element complex-valued FinSequence such that
A1: f is a_solution_of_Sierp169;
set g = n(#)f;
A2: f.(s+1)|^3 = f.(s+1)*f.(s+1)*f.(s+1) &
g.(s+1)|^3 = g.(s+1)*g.(s+1)*g.(s+1) by POLYEQ_5:2;
A3: g.(s+1) = n*f.(s+1) by VALUED_1:6;
A4: g|s = n(#)(f|s) by NUMBER15:56;
then (g|s)(#)(g|s) = (n*n)(#)((f|s)(#)(f|s)) by Th51;
then
A5: (g|s)(#)(g|s)(#)(g|s) = (n*n*n)(#)((f|s)(#)(f|s)(#)(f|s))
by A4,Th51;
((n*n*n)(#)((f|s)(#)(f|s)(#)(f|s)))" = (n*n*n)"(#)((f|s)(#)(f|s)(#)(f|s))"
by NUMBER15:58;
hence Sum (((g|s)(#)(g|s)(#)(g|s))")
= 1 / (n*n*n) * (1 / ((f.(s+1))|^3)) by A1,A5,RVSUM_2:38
.= 1 / (n*n*n * (f.(s+1))|^3) by XCMPLX_1:102
.= 1 / ((g.(s+1))|^3) by A2,A3;
end;
definition
let s be positive Nat such that
A1: s >= 3;
mode Solution_of_Sierp169 of s ->
(s+1)-element positive-yielding natural-valued FinSequence means :Def18:
it is a_solution_of_Sierp169;
existence
proof
defpred S[Nat] means
ex f being $1+1-element positive natural-valued FinSequence st
f is a_solution_of_Sierp169;
defpred P[Nat] means $1 >= 3 implies S[$1];
A2: for k being Nat holds P[2*k] & P[2*k+1]
proof
let k;
thus P[2*k]
proof
assume
A3: 2*k >= 3;
defpred Q[Nat] means 2*$1 >= 3 implies P[2*$1];
A4: Q[0];
A5: for m st Q[m] holds Q[m+1]
proof
let m such that
A6: Q[m];
assume 2*(m+1) >= 3;
assume 2*(m+1) >= 3;
then per cases by XXREAL_0:1;
suppose 2*(m+1) = 3;
hence S[2*(m+1)] by Th143;
end;
suppose 2*(m+1) > 3;
then 2*m+2-2 > 3-2 by XREAL_1:8;
then
A7: 2*m >= 1+1 by NAT_1:13;
then reconsider m as positive Nat;
per cases by A7,XXREAL_0:1;
suppose 2*m = 2*1;
hence thesis by Th144;
end;
suppose 2*m > 2;
then 2*m >= 2+1 by NAT_1:13;
then
ex f being 2*m+2+1-element positive natural-valued FinSequence
st f is a_solution_of_Sierp169 by A6,Lm31;
hence thesis;
end;
end;
end;
for m holds Q[m] from NAT_1:sch 2(A4,A5);
hence thesis by A3;
end;
thus P[2*k+1]
proof
assume
A8: 2*k+1 >= 3;
defpred Q[Nat] means 2*$1+1 >= 3 implies P[2*$1+1];
A9: Q[0];
A10: for m st Q[m] holds Q[m+1]
proof
let m such that
A11: Q[m];
assume 2*(m+1)+1 >= 3;
then per cases by XXREAL_0:1;
suppose 2*(m+1)+1 = 3;
hence thesis by Th143;
end;
suppose
A12: 2*(m+1)+1 > 3;
A13: now
assume m < 1;
then m = 0 by NAT_1:14;
hence contradiction by A12;
end;
then reconsider m as positive Nat;
per cases by A13,XXREAL_0:1;
suppose m = 1;
hence thesis by Th143,Th144,Lm31;
end;
suppose m > 1;
then 2*m > 2*1 by XREAL_1:68;
then 2*m+1 > 2+1 by XREAL_1:6;
then
ex f being 2*m+1+2+1-element positive natural-valued
FinSequence st f is a_solution_of_Sierp169 by A11,Lm31;
hence thesis;
end;
end;
end;
for m holds Q[m] from NAT_1:sch 2(A9,A10);
hence thesis by A8;
end;
end;
for k be Nat holds P[k] from STEP2(A2);
hence thesis by A1;
end;
end;
theorem Th147:
s >= 3 implies
for f being Solution_of_Sierp169 of s holds
rng Solutions_of_Sierp168(f) c=
the set of all g where g is Solution_of_Sierp169 of s
proof
assume
A1: s >= 3;
let f be Solution_of_Sierp169 of s;
set F = Solutions_of_Sierp168(f);
set A = the set of all g where g is Solution_of_Sierp169 of s;
let y be object;
assume y in rng F;
then consider x being object such that
A2: x in dom F and
A3: F.x = y by FUNCT_1:def 3;
reconsider x as Element of NATPLUS by A2;
f is a_solution_of_Sierp169 by A1,Def18;
then
A4: x(#)f is a_solution_of_Sierp169 by Th146;
F.x = x(#)f by NUMBER15:def 15;
then y is Solution_of_Sierp169 of s by A1,A3,A4,Def18;
hence y in A;
end;
:: Problem 169
theorem
for s being positive Nat st s >= 3 holds
the set of all f where f is Solution_of_Sierp169 of s is infinite
proof
let s be positive Nat such that
A1: s >= 3;
set F = Solutions_of_Sierp168(the Solution_of_Sierp169 of s);
A2: dom F = NATPLUS by PARTFUN1:def 2;
rng F c= the set of all f where f is Solution_of_Sierp169 of s
by A1,Th147;
hence thesis by A2,CARD_1:59;
end;