:: 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


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;

registration
let A be finite set ;
cluster Segm A -> finite ;
coherence
Segm A is finite ;
end;

theorem Th1: :: NUMBER17:1
for a, b, c, d being object holds dom <*a,b,c,d*> = {1,2,3,4}
proof end;

theorem Th2: :: NUMBER17:2
for a, b, c, d, e being object holds dom <*a,b,c,d,e*> = {1,2,3,4,5}
proof end;

theorem Th3: :: NUMBER17:3
for a being object
for A being set st <*a*> is A -valued holds
a in A
proof end;

registration
let s be positive Nat;
let f be s -element FinSequence;
cluster f | (s - 1) -> s - 1 -element ;
coherence
f | (s - 1) is s - 1 -element
proof end;
end;

registration
let f be non empty real-valued positive-yielding FinSequence;
cluster f . 1 -> positive ;
coherence
f . 1 is positive
proof end;
end;

theorem Th4: :: NUMBER17:4
for s being positive Nat
for f being b1 -element complex-valued FinSequence holds Sum (f | (s - 1)) = (Sum f) - (f . s)
proof end;

theorem Th5: :: NUMBER17:5
for D being non empty set holds 5 -tuples_on D = { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum }
proof end;

theorem Th6: :: NUMBER17:6
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 end;

theorem Th7: :: NUMBER17:7
for c being Complex holds <*c*> ^2 = <*(c ^2)*>
proof end;

theorem Th8: :: NUMBER17:8
for c1, c2 being Complex holds <*c1,c2*> ^2 = <*(c1 ^2),(c2 ^2)*>
proof end;

theorem Th9: :: NUMBER17:9
for c1, c2, c3 being Complex holds <*c1,c2,c3*> ^2 = <*(c1 ^2),(c2 ^2),(c3 ^2)*>
proof end;

theorem Th10: :: NUMBER17:10
for c1, c2, c3, c4 being Complex holds <*c1,c2,c3,c4*> ^2 = <*(c1 ^2),(c2 ^2),(c3 ^2),(c4 ^2)*>
proof end;

theorem Th11: :: NUMBER17:11
for c1, c2, c3, c4, c5 being Complex holds <*c1,c2,c3,c4,c5*> ^2 = <*(c1 ^2),(c2 ^2),(c3 ^2),(c4 ^2),(c5 ^2)*>
proof end;

theorem Th12: :: NUMBER17:12
for c1, c2, c3, c4, c5, c6 being Complex holds <*c1,c2,c3,c4,c5,c6*> ^2 = <*(c1 ^2),(c2 ^2),(c3 ^2),(c4 ^2),(c5 ^2),(c6 ^2)*>
proof end;

theorem Th13: :: NUMBER17:13
for c1, c2, c3, c4, c5, c6, c7 being Complex holds <*c1,c2,c3,c4,c5,c6,c7*> ^2 = <*(c1 ^2),(c2 ^2),(c3 ^2),(c4 ^2),(c5 ^2),(c6 ^2),(c7 ^2)*>
proof end;

theorem Th14: :: NUMBER17:14
for c1, c2, c3, c4, c5, c6, c7, c8 being Complex holds <*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 end;

theorem Th15: :: NUMBER17:15
for c1, c2, c3, c4 being Complex holds <*c1,c2,c3,c4*> " = <*(c1 "),(c2 "),(c3 "),(c4 ")*>
proof end;

theorem Th16: :: NUMBER17:16
for c1, c2, c3, c4, c5 being Complex holds <*c1,c2,c3,c4,c5*> " = <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 ")*>
proof end;

theorem Th17: :: NUMBER17:17
for c1, c2, c3, c4, c5, c6 being Complex holds <*c1,c2,c3,c4,c5,c6*> " = <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 "),(c6 ")*>
proof end;

theorem Th18: :: NUMBER17:18
for c1, c2, c3, c4, c5, c6, c7 being Complex holds <*c1,c2,c3,c4,c5,c6,c7*> " = <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 "),(c6 "),(c7 ")*>
proof end;

theorem Th19: :: NUMBER17:19
for c1, c2, c3, c4, c5, c6, c7, c8 being Complex holds <*c1,c2,c3,c4,c5,c6,c7,c8*> " = <*(c1 "),(c2 "),(c3 "),(c4 "),(c5 "),(c6 "),(c7 "),(c8 ")*>
proof end;

theorem Th20: :: NUMBER17:20
for c1, c2, c3, c4 being Complex holds Sum <*c1,c2,c3,c4*> = ((c1 + c2) + c3) + c4
proof end;

theorem Th21: :: NUMBER17:21
for c1, c2, c3, c4, c5 being Complex holds Sum <*c1,c2,c3,c4,c5*> = (((c1 + c2) + c3) + c4) + c5
proof end;

theorem Th22: :: NUMBER17:22
for c1, c2, c3, c4, c5, c6 being Complex holds Sum <*c1,c2,c3,c4,c5,c6*> = ((((c1 + c2) + c3) + c4) + c5) + c6
proof end;

theorem Th23: :: NUMBER17:23
for c1, c2, c3, c4, c5, c6, c7 being Complex holds Sum <*c1,c2,c3,c4,c5,c6,c7*> = (((((c1 + c2) + c3) + c4) + c5) + c6) + c7
proof end;

theorem Th24: :: NUMBER17:24
for c1, c2, c3, c4, c5, c6, c7, c8 being Complex holds Sum <*c1,c2,c3,c4,c5,c6,c7,c8*> = ((((((c1 + c2) + c3) + c4) + c5) + c6) + c7) + c8
proof end;

theorem Th25: :: NUMBER17:25
for m being Nat
for r being Real st m > 1 holds
ex n being positive Nat st m |^ (m |^ n) > r
proof end;

theorem Th26: :: NUMBER17:26
for n being non zero Integer ex k being Nat ex j being odd Integer st n = j * (2 |^ k)
proof end;

theorem Th27: :: NUMBER17:27
for i, j being Integer st i,j are_congruent_mod j holds
i, 0 are_congruent_mod j
proof end;

theorem Th28: :: NUMBER17:28
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 end;

theorem Th29: :: NUMBER17:29
for a, k, m, n being Nat
for i being Integer st m <= n & i |^ m,i |^ (m + k) are_congruent_mod a holds
i |^ n,i |^ (n + k) are_congruent_mod a
proof end;

theorem Th30: :: NUMBER17:30
for n being Nat holds 3 divides (2 |^ (2 * n)) - 1
proof end;

theorem Th31: :: NUMBER17:31
for n being Nat holds 5 divides (2 |^ (4 * n)) - 1
proof end;

theorem Th32: :: NUMBER17:32
for n being Nat holds 7 divides (2 |^ (6 * n)) - 1
proof end;

theorem Th33: :: NUMBER17:33
for n being Nat holds 11 divides (2 |^ (10 * n)) - 1
proof end;

theorem Th34: :: NUMBER17:34
for n being Nat holds 9 divides (2 |^ (6 * n)) - 1
proof end;

registration
let F be rational-valued FinSequence;
A1: F is FinSequence of RAT by FINSEQ_1:102;
cluster Sum F -> rational ;
coherence
Sum F is rational
proof end;
cluster Product F -> rational ;
coherence
Product F is rational
proof end;
end;

registration
let n be Nat;
let f be n + 1 -element FinSequence;
cluster Del (f,1) -> n -element ;
coherence
Del (f,1) is n -element
proof end;
end;

registration
let D be set ;
let f be D -valued FinSequence;
let n be Nat;
cluster Del (f,n) -> D -valued ;
coherence
Del (f,n) is D -valued
proof end;
end;

registration
let f be real-valued increasing FinSequence;
let n be Nat;
cluster Del (f,n) -> increasing ;
coherence
Del (f,n) is increasing
proof end;
end;

registration
let f be real-valued decreasing FinSequence;
let n be Nat;
cluster Del (f,n) -> decreasing ;
coherence
Del (f,n) is decreasing
proof end;
end;

registration
let f be real-valued non-increasing FinSequence;
let n be Nat;
cluster Del (f,n) -> non-increasing ;
coherence
Del (f,n) is non-increasing
proof end;
end;

registration
let f be real-valued non-decreasing FinSequence;
let n be Nat;
cluster Del (f,n) -> non-decreasing ;
coherence
Del (f,n) is non-decreasing
proof end;
end;

registration
let m, n be Nat;
let f be n -element positive-yielding FinSequence;
cluster Del (f,m) -> positive-yielding ;
coherence
Del (f,m) is positive-yielding
proof end;
end;

theorem :: NUMBER17:35
for f, g being ext-real-valued FinSequence st f ^ g is decreasing holds
( f is decreasing & g is decreasing )
proof end;

theorem :: NUMBER17:36
for f, g being ext-real-valued FinSequence st f ^ g is non-increasing holds
( f is non-increasing & g is non-increasing )
proof end;

theorem Th37: :: NUMBER17:37
for f, g being ext-real-valued FinSequence st f ^ g is non-decreasing holds
( f is non-decreasing & g is non-decreasing )
proof end;

theorem Th38: :: NUMBER17:38
for p, q being real-valued increasing FinSequence st p . (len p) < q . 1 holds
p ^ q is increasing
proof end;

theorem Th39: :: NUMBER17:39
for r1, r2 being Real st r1 < r2 holds
<*r1,r2*> is increasing
proof end;

theorem Th40: :: NUMBER17:40
for r1, r2, r3 being Real st r1 < r2 & r2 < r3 holds
<*r1,r2,r3*> is increasing
proof end;

theorem Th41: :: NUMBER17:41
for r1, r2, r3, r4 being Real st r1 < r2 & r2 < r3 & r3 < r4 holds
<*r1,r2,r3,r4*> is increasing
proof end;

registration
let n be Nat;
cluster Relation-like NAT -defined NAT -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued increasing finite-support positive-yielding nonnegative-yielding for set ;
existence
ex b1 being natural-valued FinSequence st
( b1 is increasing & b1 is positive-yielding & b1 is n -element )
proof end;
end;

theorem Th42: :: NUMBER17:42
for f being real-valued positive-yielding FinSequence st len f >= 2 holds
for k being Nat st k in dom f holds
f . k < Sum f
proof end;

theorem Th43: :: NUMBER17:43
for n being Nat
for c being Complex holds n |-> (c ") = (n |-> c) "
proof end;

registration
let a be non positive Real;
let b be Real;
cluster <*a,b*> -> non positive-yielding ;
coherence
not <*a,b*> is positive-yielding
proof end;
end;

registration
let a be Real;
let b be non positive Real;
cluster <*a,b*> -> non positive-yielding ;
coherence
not <*a,b*> is positive-yielding
proof end;
end;

registration
let a be non positive Real;
let b, c be Real;
cluster <*a,b,c*> -> non positive-yielding ;
coherence
not <*a,b,c*> is positive-yielding
proof end;
end;

registration
let b be non positive Real;
let a, c be Real;
cluster <*a,b,c*> -> non positive-yielding ;
coherence
not <*a,b,c*> is positive-yielding
proof end;
end;

registration
let c be non positive Real;
let a, b be Real;
cluster <*a,b,c*> -> non positive-yielding ;
coherence
not <*a,b,c*> is positive-yielding
proof end;
end;

registration
let a be non positive Real;
let b, c, d be Real;
cluster <*a,b,c,d*> -> non positive-yielding ;
coherence
not <*a,b,c,d*> is positive-yielding
proof end;
end;

registration
let b be non positive Real;
let a, c, d be Real;
cluster <*a,b,c,d*> -> non positive-yielding ;
coherence
not <*a,b,c,d*> is positive-yielding
proof end;
end;

registration
let c be non positive Real;
let a, b, d be Real;
cluster <*a,b,c,d*> -> non positive-yielding ;
coherence
not <*a,b,c,d*> is positive-yielding
proof end;
end;

registration
let d be non positive Real;
let a, b, c be Real;
cluster <*a,b,c,d*> -> non positive-yielding ;
coherence
not <*a,b,c,d*> is positive-yielding
proof 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
not <*a,b,c,d,e*> is positive-yielding
proof 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
not <*a,b,c,d,e*> is positive-yielding
proof 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
not <*a,b,c,d,e*> is positive-yielding
proof 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
not <*a,b,c,d,e*> is positive-yielding
proof 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
not <*a,b,c,d,e*> is positive-yielding
proof end;
end;

theorem :: NUMBER17:44
for f being 1 -element natural-valued positive FinSequence ex a being positive Nat st f = <*a*>
proof end;

theorem Th45: :: NUMBER17:45
for f being 2 -element natural-valued positive FinSequence ex a, b being positive Nat st f = <*a,b*>
proof end;

theorem :: NUMBER17:46
for f being 2 -element natural-valued increasing positive FinSequence ex a, b being positive Nat st
( f = <*a,b*> & a < b )
proof end;

theorem Th47: :: NUMBER17:47
for f being 3 -element natural-valued positive FinSequence ex a, b, c being positive Nat st f = <*a,b,c*>
proof end;

theorem Th48: :: NUMBER17:48
for f being 3 -element natural-valued increasing positive FinSequence ex a, b, c being positive Nat st
( f = <*a,b,c*> & a < b & b < c )
proof end;

theorem Th49: :: NUMBER17:49
for c being Complex
for f, g being complex-valued Function st c (#) f = c (#) g & c <> 0 holds
f = g
proof end;

theorem Th50: :: NUMBER17:50
for f, g being complex-valued Function holds (f (#) g) " = (f ") (#) (g ")
proof end;

theorem Th51: :: NUMBER17:51
for c1, c2 being Complex
for f, g being complex-valued Function holds (c1 (#) f) (#) (c2 (#) g) = (c1 * c2) (#) (f (#) g)
proof end;

theorem Th52: :: NUMBER17:52
for f1, f2, g1, g2, h1, h2 being complex-valued FinSequence st len f1 = len g1 & len g1 = len h1 holds
((f1 ^ f2) (#) (g1 ^ g2)) (#) (h1 ^ h2) = ((f1 (#) g1) (#) h1) ^ ((f2 (#) g2) (#) h2)
proof end;

theorem Th53: :: NUMBER17:53
for n being Nat
for e being object holds (Segm (n + 1)) --> e = <%e%> ^ ((Segm n) --> e)
proof end;

theorem Th54: :: NUMBER17:54
for n, b being Nat st n > 0 & b > 1 holds
digits ((n * b),b) = <%0%> ^ (digits (n,b))
proof end;

theorem Th55: :: NUMBER17:55
for n, b being Nat st n > 0 & b > 1 holds
for i being Nat holds digits ((n * (b |^ i)),b) = (i --> 0) ^ (digits (n,b))
proof end;

theorem :: NUMBER17:56
for s being Nat ex n being Nat st
( Sum (digits (n,10)) = s & s divides n )
proof end;

theorem :: NUMBER17:57
for a, b being set holds Replace (<%a%>,0,b) = <%b%>
proof end;

theorem :: NUMBER17:58
for a, b, c being set holds Replace (<%a,b%>,0,c) = <%c,b%>
proof end;

theorem :: NUMBER17:59
for a, b, c being set holds Replace (<%a,b%>,1,c) = <%a,c%>
proof end;

theorem Th60: :: NUMBER17:60
for a, b, c, d being set holds Replace (<%a,b,c%>,0,d) = <%d,b,c%>
proof end;

theorem :: NUMBER17:61
for a, b, c, d being set holds Replace (<%a,b,c%>,1,d) = <%a,d,c%>
proof end;

theorem Th62: :: NUMBER17:62
for a, b, c, d being set holds Replace (<%a,b,c%>,2,d) = <%a,b,d%>
proof end;

theorem Th63: :: NUMBER17:63
digits (201,10) = <%1,0,2%>
proof end;

theorem Th64: :: NUMBER17:64
digits (202,10) = <%2,0,2%>
proof end;

theorem Th65: :: NUMBER17:65
digits (203,10) = <%3,0,2%>
proof end;

theorem Th66: :: NUMBER17:66
digits (205,10) = <%5,0,2%>
proof end;

theorem Th67: :: NUMBER17:67
digits (206,10) = <%6,0,2%>
proof end;

theorem :: NUMBER17:68
for i, j being Element of NAT st 0 <= j & j <= 9 holds
not value ((Replace ((digits (200,10)),i,j)),10) is prime
proof end;

:: WP: A consequence of Euler's theorem
theorem Th69: :: NUMBER17:69
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 end;

theorem Th70: :: NUMBER17:70
for a being Nat
for k being Integer st k <> 1 holds
ex n being positive Nat st
( a < (2 |^ (2 |^ n)) + k & (2 |^ (2 |^ n)) + k is composite )
proof end;

Lm13: for k being Integer st k <> 1 holds
not { ((2 |^ (2 |^ n)) + k) where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is empty
proof end;

theorem Th71: :: NUMBER17:71
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 end;

:: Problem 115
theorem Th72: :: NUMBER17:72
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 end;

:: Problem 115
theorem :: NUMBER17:73
for k being Integer st k <> 1 holds
{ n where n is positive Nat : (2 |^ (2 |^ n)) + k is composite } is infinite
proof end;

Lm14: for s being positive Nat holds 2 |^ (2 |^ ((2 * s) + 1)) >= 256
proof end;

theorem Th74: :: NUMBER17:74
for s being positive Nat holds 7 divides (2 |^ (2 |^ ((2 * s) + 1))) + 3
proof end;

:: Problem 117 a
theorem :: NUMBER17:75
for s being positive Nat holds (2 |^ (2 |^ ((2 * s) + 1))) + 3 is composite
proof end;

Lm15: for s being positive Nat holds 2 |^ (2 |^ ((4 * s) + 1)) >= 2 |^ 32
proof end;

theorem Th76: :: NUMBER17:76
for s being positive Nat holds 11 divides (2 |^ (2 |^ ((4 * s) + 1))) + 7
proof end;

:: Problem 117 b
theorem :: NUMBER17:77
for s being positive Nat holds (2 |^ (2 |^ ((4 * s) + 1))) + 7 is composite
proof end;

Lm16: for s being positive Nat holds 2 |^ (2 |^ ((6 * s) + 2)) >= 2 |^ 256
proof end;

theorem Th78: :: NUMBER17:78
for s being positive Nat holds 29 divides (2 |^ (2 |^ ((6 * s) + 2))) + 13
proof end;

:: Problem 117 c
theorem :: NUMBER17:79
for s being positive Nat holds (2 |^ (2 |^ ((6 * s) + 2))) + 13 is composite
proof end;

Lm17: for s being positive Nat holds 2 |^ (2 |^ ((10 * s) + 1)) >= 2 |^ 2048
proof end;

theorem Th80: :: NUMBER17:80
for s being positive Nat holds 23 divides (2 |^ (2 |^ ((10 * s) + 1))) + 19
proof end;

:: Problem 117 d
theorem :: NUMBER17:81
for s being positive Nat holds (2 |^ (2 |^ ((10 * s) + 1))) + 19 is composite
proof end;

theorem Th82: :: NUMBER17:82
for s being positive Nat holds 37 divides (2 |^ (2 |^ ((6 * s) + 2))) + 21
proof end;

:: Problem 117 e
theorem :: NUMBER17:83
for s being positive Nat holds (2 |^ (2 |^ ((6 * s) + 2))) + 21 is composite
proof end;

theorem Th84: :: NUMBER17:84
Fermat 5 = 641 * 6700417 by Lm11, Lm6, Lm12, Lm4;

:: Problem 145
theorem :: NUMBER17:85
for x, y being positive Nat holds
( ((x * y) + x) + y = 2 |^ 32 iff ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) )
proof end;

registration
let a be non positive Integer;
let n be odd Nat;
cluster a |^ n -> non positive ;
coherence
not a |^ n is positive
proof end;
end;

theorem Th86: :: NUMBER17:86
for a, b, c, d, n being Nat st a,b,c are_mutually_coprime & (a * b) * c = d |^ n holds
ex k being Nat st a = k |^ n
proof end;

:: Problem 157
theorem :: NUMBER17:87
( ( 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 end;

registration
let a, b, c be positive Real;
cluster <*a,b,c*> -> positive-yielding ;
coherence
<*a,b,c*> is positive-yielding ;
end;

registration
let a, b, c, d be positive Real;
cluster <*a,b,c,d*> -> positive-yielding ;
coherence
<*a,b,c,d*> is positive-yielding ;
end;

Lm18: now :: thesis: for x, y, z, t being positive Integer holds (((x / y) * (y / z)) * (z / t)) * (t / x) = 1
let x, y, z, t be positive Integer; :: thesis: (((x / y) * (y / z)) * (z / t)) * (t / x) = 1
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 ;
:: thesis: verum
end;

theorem Th88: :: NUMBER17:88
for a, b, c, d being Complex holds Product <*a,b,c,d*> = ((a * b) * c) * d
proof end;

theorem :: NUMBER17:89
for a being positive Real holds 2 -root a = sqrt a
proof end;

theorem :: NUMBER17:90
for a being positive Real holds GMean <*a*> = a
proof end;

theorem :: NUMBER17:91
for a, b being positive Real holds (GMean <*a,b*>) |^ 2 = a * b
proof end;

theorem :: NUMBER17:92
for a, b, c being positive Real holds (GMean <*a,b,c*>) |^ 3 = (a * b) * c
proof end;

theorem Th93: :: NUMBER17:93
for a, b, c, d being positive Real holds (GMean <*a,b,c,d*>) |^ 4 = ((a * b) * c) * d
proof end;

theorem :: NUMBER17:94
for a being Real holds Mean <*a*> = a
proof end;

theorem :: NUMBER17:95
for a, b being Real holds Mean <*a,b*> = (a + b) / 2
proof end;

theorem :: NUMBER17:96
for a, b, c being Real holds Mean <*a,b,c*> = ((a + b) + c) / 3
proof end;

theorem Th97: :: NUMBER17:97
for a, b, c, d being Real holds Mean <*a,b,c,d*> = (((a + b) + c) + d) / 4
proof end;

Lm19: for f being real-valued positive FinSequence st GMean f = Mean f holds
f is constant
proof end;

theorem Th98: :: NUMBER17:98
for w, x, y, z being object st <*w,x,y,z*> is constant holds
( w = x & x = y & y = z )
proof end;

Lm20: now :: thesis: for a, b, c, d being positive Real holds ((a * b) * c) * d <= ((((a + b) + c) + d) / 4) |^ 4
let a, b, c, d be positive Real; :: thesis: ((a * b) * c) * d <= ((((a + b) + c) + d) / 4) |^ 4
set f = <*a,b,c,d*>;
A1: len <*a,b,c,d*> = 4 by FINSEQ_4:76;
A2: Sum <*a,b,c,d*> = ((a + b) + c) + d by RVSUM_1:142;
(GMean <*a,b,c,d*>) |^ 4 <= (Mean <*a,b,c,d*>) |^ 4 by PREPOWER:9, RVSUM_3:47;
hence ((a * b) * c) * d <= ((((a + b) + c) + d) / 4) |^ 4 by A1, A2, Th88; :: thesis: verum
end;

theorem Th99: :: NUMBER17:99
for a, b, c, d being positive Real st ((a * b) * c) * d >= ((((a + b) + c) + d) / 4) |^ 4 holds
( a = b & b = c & c = d )
proof end;

:: Problem 159 a
theorem :: NUMBER17:100
for m being Real st 0 <= m & m < 4 holds
for x, y, z, t being positive Integer holds not (((x / y) + (y / z)) + (z / t)) + (t / x) = m
proof end;

:: Problem 159 b
theorem :: NUMBER17:101
{ [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 & y = z & z = t ) }
proof end;

registration
let a, b be Nat;
reduce In ([a,b],[:NAT,NAT:]) to [a,b];
reducibility
In ([a,b],[:NAT,NAT:]) = [a,b]
proof end;
end;

registration
let a, b, c be Nat;
reduce In ([a,b,c],[:NAT,NAT,NAT:]) to [a,b,c];
reducibility
In ([a,b,c],[:NAT,NAT,NAT:]) = [a,b,c]
proof 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
In ([a,b,c,d],[:NAT,NAT,NAT,NAT:]) = [a,b,c,d]
proof end;
end;

registration
let a be positive Nat;
reduce In (a,NATPLUS) to a;
reducibility
In (a,NATPLUS) = a
proof end;
end;

registration
let a, b be positive Nat;
reduce In ([a,b],[:NATPLUS,NATPLUS:]) to [a,b];
reducibility
In ([a,b],[:NATPLUS,NATPLUS:]) = [a,b]
proof end;
end;

registration
let a, b, c be positive Nat;
reduce In ([a,b,c],[:NATPLUS,NATPLUS,NATPLUS:]) to [a,b,c];
reducibility
In ([a,b,c],[:NATPLUS,NATPLUS,NATPLUS:]) = [a,b,c]
proof 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
In ([a,b,c,d],[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:]) = [a,b,c,d]
proof end;
end;

definition
set A = NATPLUS ;
set D = [:NATPLUS,NATPLUS,NATPLUS,NATPLUS:];
func Cart4Id -> Function of NATPLUS,[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:] means :Def1: :: NUMBER17:def 1
 for n being positive Nat holds it . n = [n,n,n,n];
existence
ex b1 being Function of NATPLUS,[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:] st
for n being positive Nat holds b1 . n = [n,n,n,n]
proof end;
uniqueness
for b1, b2 being Function of NATPLUS,[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:] st ( for n being positive Nat holds b1 . n = [n,n,n,n] ) & ( for n being positive Nat holds b2 . n = [n,n,n,n] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Cart4Id NUMBER17:def 1 :
for b1 being Function of NATPLUS,[:NATPLUS,NATPLUS,NATPLUS,NATPLUS:] holds
( b1 = Cart4Id iff for n being positive Nat holds b1 . n = [n,n,n,n] );

registration
cluster Cart4Id -> one-to-one ;
coherence
Cart4Id is one-to-one
proof end;
end;

theorem Th102: :: NUMBER17:102
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 end;

:: Problem 159 c
theorem :: NUMBER17:103
{ [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } is infinite
proof end;

definition
let R be Relation;
func Permutations R -> set equals :: NUMBER17:def 2
 { (p * R) where p is Permutation of (dom R) : verum } ;
coherence
{ (p * R) where p is Permutation of (dom R) : verum } is set ;
end;

:: deftheorem defines Permutations NUMBER17:def 2 :
for R being Relation holds Permutations R = { (p * R) where p is Permutation of (dom R) : verum } ;

definition
let f be Function;
:: original: Permutations
redefine func Permutations f -> set equals :: NUMBER17:def 3
 { (f * p) where p is Permutation of (dom f) : verum } ;
coherence
Permutations f is set ;
compatibility
for b1 being set holds
( b1 = Permutations f iff b1 = { (f * p) where p is Permutation of (dom f) : verum } ) ;
end;

:: deftheorem defines Permutations NUMBER17:def 3 :
for f being Function holds Permutations f = { (f * p) where p is Permutation of (dom f) : verum } ;

definition
let A be set ;
attr A is relational means :Def4: :: NUMBER17:def 4
 for a being object st a in A holds
a is Relation;
end;

:: deftheorem Def4 defines relational NUMBER17:def 4 :
for A being set holds
( A is relational iff for a being object st a in A holds
a is Relation );

registration
let a, b be object ;
cluster {{[a,b]}} -> relational ;
coherence
{{[a,b]}} is relational ;
end;

registration
cluster non empty finite relational for set ;
existence
ex b1 being set st
( not b1 is empty & b1 is finite & b1 is relational )
proof end;
end;

registration
let A be relational set ;
cluster -> Relation-like for Element of A;
coherence
for b1 being Element of A holds b1 is Relation-like
proof end;
end;

registration
cluster functional -> relational for set ;
coherence
for b1 being set st b1 is functional holds
b1 is relational ;
end;

registration
let R be finite Relation;
cluster Permutations R -> finite ;
coherence
Permutations R is finite
proof end;
end;

definition
let A be relational set ;
func Permutations A -> set equals :: NUMBER17:def 5
 { (Permutations f) where f is Element of A : f in A } ;
coherence
{ (Permutations f) where f is Element of A : f in A } is set ;
end;

:: deftheorem defines Permutations NUMBER17:def 5 :
for A being relational set holds Permutations A = { (Permutations f) where f is Element of A : f in A } ;

registration
let A be finite relational set ;
cluster Permutations A -> finite ;
coherence
Permutations A is finite
proof end;
end;

definition
let f be complex-valued FinSequence;
attr f is with_sum_of_reciprocals_equal_1 means :: NUMBER17:def 6
 Sum (f ") = 1;
end;

:: deftheorem defines with_sum_of_reciprocals_equal_1 NUMBER17:def 6 :
for f being complex-valued FinSequence holds
( f is with_sum_of_reciprocals_equal_1 iff Sum (f ") = 1 );

registration
cluster <*1*> -> with_sum_of_reciprocals_equal_1 ;
coherence
<*1*> is with_sum_of_reciprocals_equal_1
proof end;
end;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support with_sum_of_reciprocals_equal_1 for set ;
existence
ex b1 being complex-valued FinSequence st b1 is with_sum_of_reciprocals_equal_1
proof end;
end;

definition
let s be Nat;
func SolutionsOfSumOfReciprocals s -> set equals :: NUMBER17:def 7
 { f where f is s -element natural-valued positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;
coherence
{ f where f is s -element natural-valued positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } is set ;
end;

:: deftheorem defines SolutionsOfSumOfReciprocals NUMBER17:def 7 :
for s being Nat holds SolutionsOfSumOfReciprocals s = { f where f is b1 -element natural-valued positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;

registration
let s be zero Nat;
cluster SolutionsOfSumOfReciprocals s -> empty ;
coherence
SolutionsOfSumOfReciprocals s is empty
proof end;
end;

theorem Th104: :: NUMBER17:104
for s being positive Nat holds Sum (s |-> (s ")) = 1
proof end;

registration
let s be positive Nat;
cluster s |-> s -> with_sum_of_reciprocals_equal_1 ;
coherence
s |-> s is with_sum_of_reciprocals_equal_1
proof end;
end;

theorem Th105: :: NUMBER17:105
for s being positive Nat holds s |-> s in SolutionsOfSumOfReciprocals s ;

registration
let s be positive Nat;
cluster SolutionsOfSumOfReciprocals s -> non empty ;
coherence
not SolutionsOfSumOfReciprocals s is empty by Th105;
end;

definition
let A, B be FinSequence-membered set ;
func A ^^ B -> set equals :: NUMBER17:def 8
 { (p ^ q) where p is Element of A, q is Element of B : ( p in A & q in B ) } ;
coherence
{ (p ^ q) where p is Element of A, q is Element of B : ( p in A & q in B ) } is set ;
end;

:: deftheorem defines ^^ NUMBER17:def 8 :
for A, B being FinSequence-membered set holds A ^^ B = { (p ^ q) where p is Element of A, q is Element of B : ( p in A & q in B ) } ;

registration
let A, B be FinSequence-membered set ;
cluster A ^^ B -> FinSequence-membered ;
coherence
A ^^ B is FinSequence-membered
proof end;
end;

theorem Th106: :: NUMBER17:106
for A being FinSequence-membered set holds A ^^ {} c= A
proof end;

theorem Th107: :: NUMBER17:107
for A being FinSequence-membered set holds {} ^^ A c= A
proof end;

registration
let A, B be finite FinSequence-membered set ;
cluster A ^^ B -> finite ;
coherence
A ^^ B is finite
proof end;
end;

definition
let D, A be set ;
attr A is D -FinSequence-membered means :: NUMBER17:def 9
 for f being object st f in A holds
f is D -valued FinSequence;
end;

:: deftheorem defines -FinSequence-membered NUMBER17:def 9 :
for D, A being set holds
( A is D -FinSequence-membered iff for f being object st f in A holds
f is b1 -valued FinSequence );

registration
let D be non empty set ;
let d be Element of D;
cluster {<*d*>} -> D -FinSequence-membered ;
coherence
{<*d*>} is D -FinSequence-membered ;
end;

registration
let D be non empty set ;
cluster D -FinSequence-membered for set ;
existence
ex b1 being set st b1 is D -FinSequence-membered
proof end;
end;

definition
let D be non empty set ;
let A be D -FinSequence-membered set ;
func decomp A -> Relation means :Def10: :: NUMBER17:def 10
 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
ex b1 being Relation st
for x, y being object holds
( [x,y] in b1 iff ( x in D & ex f being FinSequence of D st
( y = f & <*x*> ^ f in A ) ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being object holds
( [x,y] in b1 iff ( x in D & ex f being FinSequence of D st
( y = f & <*x*> ^ f in A ) ) ) ) & ( for x, y being object holds
( [x,y] in b2 iff ( x in D & ex f being FinSequence of D st
( y = f & <*x*> ^ f in A ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines decomp NUMBER17:def 10 :
for D being non empty set
for A being b1 -FinSequence-membered set
for b3 being Relation holds
( b3 = decomp A iff for x, y being object holds
( [x,y] in b3 iff ( x in D & ex f being FinSequence of D st
( y = f & <*x*> ^ f in A ) ) ) );

registration
let D be set ;
cluster D -FinSequence-membered -> FinSequence-membered for set ;
coherence
for b1 being set st b1 is D -FinSequence-membered holds
b1 is FinSequence-membered
proof end;
end;

deffunc H1( object ) -> set = <*$1*>;

definition
let A be set ;
func OneFS A -> ManySortedSet of A means :Def11: :: NUMBER17:def 11
 for a being object st a in A holds
it . a = <*a*>;
existence
ex b1 being ManySortedSet of A st
for a being object st a in A holds
b1 . a = <*a*>
proof end;
uniqueness
for b1, b2 being ManySortedSet of A st ( for a being object st a in A holds
b1 . a = <*a*> ) & ( for a being object st a in A holds
b2 . a = <*a*> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines OneFS NUMBER17:def 11 :
for A being set
for b2 being ManySortedSet of A holds
( b2 = OneFS A iff for a being object st a in A holds
b2 . a = <*a*> );

registration
let A be set ;
cluster OneFS A -> FinSequence-yielding ;
coherence
OneFS A is FinSequence-yielding
proof end;
end;

registration
let f be FinSequence-yielding Function;
cluster proj2 f -> FinSequence-membered ;
coherence
rng f is FinSequence-membered
proof end;
end;

registration
let n be Nat;
let f be n -element real-valued FinSequence;
cluster sort_a f -> n -element ;
coherence
sort_a f is n -element
proof end;
cluster sort_d f -> n -element ;
coherence
sort_d f is n -element
proof end;
end;

theorem Th108: :: NUMBER17:108
for f, g being complex-valued FinSequence
for P being Permutation of (dom g) st f = g * P & len g >= 1 holds
f " = (g ") * P
proof end;

theorem Th109: :: NUMBER17:109
for f, g being complex-valued FinSequence st f,g are_fiberwise_equipotent holds
f " ,g " are_fiberwise_equipotent
proof end;

theorem Th110: :: NUMBER17:110
for s being Nat
for f being b1 + 1 -element natural-valued non-decreasing positive FinSequence holds
( f . 1 <= (s + 1) / (Sum (f ")) & Sum ((Del (f,1)) ") = (Sum (f ")) - (1 / (f . 1)) )
proof end;

theorem Th111: :: NUMBER17:111
for s being Nat
for w being Rational holds { f where f is b1 -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } is finite
proof end;

theorem Th112: :: NUMBER17:112
for s being Nat
for w being Rational holds { f where f is b1 -element natural-valued positive-yielding FinSequence : Sum (f ") = w } is finite
proof end;

:: Problem 161
registration
let s be Nat;
cluster SolutionsOfSumOfReciprocals s -> finite ;
coherence
SolutionsOfSumOfReciprocals s is finite
proof end;
end;

registration
cluster <*2,3*> -> increasing ;
coherence
<*2,3*> is increasing by Th39;
end;

registration
cluster <*2,3,6*> -> increasing ;
coherence
<*2,3,6*> is increasing by Th40;
end;

registration
cluster <*2,3,7,42*> -> increasing ;
coherence
<*2,3,7,42*> is increasing by Th41;
end;

registration
cluster <*2,3,8,24*> -> increasing ;
coherence
<*2,3,8,24*> is increasing by Th41;
end;

definition
let f be complex-valued FinSequence;
func Sierp162FS f -> FinSequence equals :: NUMBER17:def 12
<*2*> ^ (2 (#) f);
coherence
<*2*> ^ (2 (#) f) is FinSequence ;
func Sierp162FS_2 f -> FinSequence equals :: NUMBER17:def 13
<*2,3*> ^ (6 (#) f);
coherence
<*2,3*> ^ (6 (#) f) is FinSequence ;
end;

:: deftheorem defines Sierp162FS NUMBER17:def 12 :
for f being complex-valued FinSequence holds Sierp162FS f = <*2*> ^ (2 (#) f);

:: deftheorem defines Sierp162FS_2 NUMBER17:def 13 :
for f being complex-valued FinSequence holds Sierp162FS_2 f = <*2,3*> ^ (6 (#) f);

registration
let f be complex-valued FinSequence;
cluster Sierp162FS f -> complex-valued ;
coherence
Sierp162FS f is complex-valued ;
cluster Sierp162FS_2 f -> complex-valued ;
coherence
Sierp162FS_2 f is complex-valued ;
end;

registration
let f be real-valued FinSequence;
cluster Sierp162FS f -> real-valued ;
coherence
Sierp162FS f is real-valued ;
cluster Sierp162FS_2 f -> real-valued ;
coherence
Sierp162FS_2 f is real-valued ;
end;

registration
let f be rational-valued FinSequence;
cluster Sierp162FS f -> rational-valued ;
coherence
Sierp162FS f is rational-valued ;
cluster Sierp162FS_2 f -> rational-valued ;
coherence
Sierp162FS_2 f is rational-valued ;
end;

registration
let f be integer-valued FinSequence;
cluster Sierp162FS f -> integer-valued ;
coherence
Sierp162FS f is integer-valued ;
cluster Sierp162FS_2 f -> integer-valued ;
coherence
Sierp162FS_2 f is integer-valued ;
end;

registration
let f be natural-valued FinSequence;
cluster Sierp162FS f -> natural-valued ;
coherence
Sierp162FS f is natural-valued ;
cluster Sierp162FS_2 f -> natural-valued ;
coherence
Sierp162FS_2 f is natural-valued ;
end;

registration
let s be Nat;
let f be s -element complex-valued FinSequence;
cluster Sierp162FS f -> s + 1 -element ;
coherence
Sierp162FS f is s + 1 -element ;
cluster Sierp162FS_2 f -> s + 2 -element ;
coherence
Sierp162FS_2 f is s + 2 -element ;
end;

registration
let s be Nat;
cluster Relation-like NAT -defined NAT -valued Function-like finite s -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued increasing finite-support nonnegative-yielding for set ;
existence
ex b1 being natural-valued FinSequence st
( b1 is increasing & b1 is s -element )
proof end;
end;

theorem Th113: :: NUMBER17:113
for s being Nat st s >= 2 holds
for f being b1 -element real-valued positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
for k being Nat st k in dom f holds
f . k > 1
proof end;

Lm21: len <*2*> = 1
by FINSEQ_1:39;

Lm22: len <*2,3*> = 2
by FINSEQ_1:44;

theorem Th114: :: NUMBER17:114
for s being Nat st s >= 2 holds
for f being b1 -element real-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
Sierp162FS f is increasing
proof end;

theorem Th115: :: NUMBER17:115
for s being positive Nat
for f being b1 -element natural-valued increasing positive-yielding FinSequence holds Sierp162FS_2 f is increasing
proof end;

theorem Th116: :: NUMBER17:116
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 end;

theorem Th117: :: NUMBER17:117
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 end;

theorem Th118: :: NUMBER17:118
<*2,3,6*> is with_sum_of_reciprocals_equal_1
proof end;

theorem Th119: :: NUMBER17:119
<*2,3,7,42*> is with_sum_of_reciprocals_equal_1
proof end;

theorem Th120: :: NUMBER17:120
<*2,3,8,24*> is with_sum_of_reciprocals_equal_1
proof end;

:: Problem 162 a
theorem Th121: :: NUMBER17:121
for s being Nat st s > 2 holds
ex f being b1 -element natural-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1
proof end;

definition
let s be Nat;
func IncreasingSolutionsOfSumOfReciprocals s -> set equals :: NUMBER17:def 14
 { f where f is s -element natural-valued increasing positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;
coherence
{ f where f is s -element natural-valued increasing positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } is set ;
end;

:: deftheorem defines IncreasingSolutionsOfSumOfReciprocals NUMBER17:def 14 :
for s being Nat holds IncreasingSolutionsOfSumOfReciprocals s = { f where f is b1 -element natural-valued increasing positive-yielding FinSequence : f is with_sum_of_reciprocals_equal_1 } ;

theorem Th122: :: NUMBER17:122
for s being Nat holds IncreasingSolutionsOfSumOfReciprocals s c= SolutionsOfSumOfReciprocals s
proof end;

registration
let s be positive Nat;
cluster IncreasingSolutionsOfSumOfReciprocals s -> finite ;
coherence
IncreasingSolutionsOfSumOfReciprocals s is finite
proof end;
end;

Lm23: now :: thesis: for s being positive Nat holds
( s = 1 or s = 2 or s = 3 or s >= 4 )
let s be positive Nat; :: thesis: ( s = 1 or s = 2 or s = 3 or s >= 4 )
thus ( s = 1 or s = 2 or s = 3 or s >= 4 ) :: thesis: verum
proof
per cases ( s <= 3 or s > 3 ) ;
suppose s <= 3 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s >= 4 )
then not not s = 0 & ... & not s = 3 ;
hence ( s = 1 or s = 2 or s = 3 or s >= 4 ) ; :: thesis: verum
end;
suppose s > 3 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s >= 4 )
then s >= 3 + 1 by NAT_1:13;
hence ( s = 1 or s = 2 or s = 3 or s >= 4 ) ; :: thesis: verum
end;
end;
end;
end;

Lm24: now :: thesis: for s being positive Nat holds
( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 )
let s be positive Nat; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 )
thus ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 ) :: thesis: verum
proof
per cases ( s <= 4 or s > 4 ) ;
suppose s <= 4 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 )
then not not s = 0 & ... & not s = 4 ;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 ) ; :: thesis: verum
end;
suppose s > 4 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 )
then s >= 4 + 1 by NAT_1:13;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s >= 5 ) ; :: thesis: verum
end;
end;
end;
end;

Lm25: now :: thesis: for s being positive Nat holds
( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 )
let s be positive Nat; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 )
thus ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 ) :: thesis: verum
proof
per cases ( s <= 6 or s > 6 ) ;
suppose s <= 6 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 )
then not not s = 0 & ... & not s = 6 ;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 ) ; :: thesis: verum
end;
suppose s > 6 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 )
then s >= 6 + 1 by NAT_1:13;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s >= 7 ) ; :: thesis: verum
end;
end;
end;
end;

theorem Th123: :: NUMBER17:123
IncreasingSolutionsOfSumOfReciprocals 3 = {<*2,3,6*>}
proof end;

theorem Th124: :: NUMBER17:124
{<*2,3,7,42*>,<*2,3,8,24*>} c= IncreasingSolutionsOfSumOfReciprocals 4
proof end;

:: Problem 162 b
theorem :: NUMBER17:125
for s being positive Nat st s > 2 holds
card (IncreasingSolutionsOfSumOfReciprocals s) < card (IncreasingSolutionsOfSumOfReciprocals (s + 1))
proof end;

registration
let n be Nat;
cluster Triangle n -> triangular ;
coherence
Triangle n is triangular by NUMPOLY1:def 2;
end;

registration
let a be triangular Nat;
cluster <*a*> -> triangular-valued ;
coherence
<*a*> is triangular-valued
proof end;
end;

deffunc H2( Nat) -> set = Triangle $1;

registration
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like triangular-valued finite-support for set ;
existence
ex b1 being FinSequence st b1 is triangular-valued
proof end;
end;

registration
let f, g be triangular-valued FinSequence;
cluster f ^ g -> triangular-valued ;
coherence
f ^ g is triangular-valued
proof end;
end;

registration
let a, b be triangular Nat;
cluster <*a,b*> -> triangular-valued ;
coherence
<*a,b*> is triangular-valued ;
end;

registration
let a, b, c be triangular Nat;
cluster <*a,b,c*> -> triangular-valued ;
coherence
<*a,b,c*> is triangular-valued ;
end;

registration
let a, b, c, d be triangular Nat;
cluster <*a,b,c,d*> -> triangular-valued ;
coherence
<*a,b,c,d*> is triangular-valued ;
end;

registration
let a, b, c, d, e be triangular Nat;
cluster <*a,b,c,d,e*> -> triangular-valued ;
coherence
<*a,b,c,d,e*> is triangular-valued ;
end;

registration
let a, b, c, d, e, f be triangular Nat;
cluster <*a,b,c,d,e,f*> -> triangular-valued ;
coherence
<*a,b,c,d,e,f*> is triangular-valued ;
end;

theorem :: NUMBER17:126
<*(Triangle 1)*> is with_sum_of_reciprocals_equal_1 by NUMPOLY1:11;

theorem Th127: :: NUMBER17:127
<*(Triangle 2),(Triangle 2),(Triangle 2)*> is with_sum_of_reciprocals_equal_1
proof end;

theorem Th128: :: NUMBER17:128
<*(Triangle 2),(Triangle 2),(Triangle 3),(Triangle 3)*> is with_sum_of_reciprocals_equal_1
proof end;

theorem Th129: :: NUMBER17:129
<*(Triangle 3),(Triangle 3),(Triangle 3),(Triangle 3),(Triangle 3),(Triangle 3)*> is with_sum_of_reciprocals_equal_1
proof end;

definition
let n, a be Nat;
assume A1: n >= a + 1 ;
func TriangleShift2 (n,a) -> FinSequence of NAT means :Def15: :: NUMBER17:def 15
( len it = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len it holds
it . i = Triangle (a + i) ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len b1 holds
b1 . i = Triangle (a + i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len b1 holds
b1 . i = Triangle (a + i) ) & len b2 = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len b2 holds
b2 . i = Triangle (a + i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines TriangleShift2 NUMBER17:def 15 :
for n, a being Nat st n >= a + 1 holds
for b3 being FinSequence of NAT holds
( b3 = TriangleShift2 (n,a) iff ( len b3 = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len b3 holds
b3 . i = Triangle (a + i) ) ) );

Lm26: 3 >= 2 + 1
;

registration
cluster TriangleShift2 (3,2) -> empty ;
coherence
TriangleShift2 (3,2) is empty
proof end;
end;

theorem :: NUMBER17:130
TriangleShift2 (4,2) = <*(Triangle 3)*>
proof end;

theorem Th131: :: NUMBER17:131
for a, n being Nat st n >= a + 1 holds
TriangleShift2 ((n + 1),a) = (TriangleShift2 (n,a)) ^ <*(Triangle n)*>
proof end;

theorem Th132: :: NUMBER17:132
for a, n being Nat st a + 1 <= n holds
TriangleShift2 (n,a) is triangular-valued
proof end;

registration
let m, n be Nat;
cluster m |-> (Triangle n) -> triangular-valued ;
coherence
m |-> (Triangle n) is triangular-valued
proof end;
end;

theorem Th133: :: NUMBER17:133
for n being Nat st 3 <= n holds
Sum ((TriangleShift2 (n,2)) ") = (2 / 3) - ((n + 1) / (Triangle n))
proof end;

:: Problem 163
theorem :: NUMBER17:134
for s being positive Nat st s <> 2 holds
ex f being b1 -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
proof end;

definition
let f be complex-valued FinSequence;
attr f is with_sum_of_squares_of_reciprocals_equal_1 means :: NUMBER17:def 16
 Sum ((f ") ^2) = 1;
end;

:: deftheorem defines with_sum_of_squares_of_reciprocals_equal_1 NUMBER17:def 16 :
for f being complex-valued FinSequence holds
( f is with_sum_of_squares_of_reciprocals_equal_1 iff Sum ((f ") ^2) = 1 );

Lm27: now :: thesis: for s being positive Nat holds
( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 )
let s be positive Nat; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 )
thus ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 ) :: thesis: verum
proof
per cases ( s <= 5 or s > 5 ) ;
suppose s <= 5 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 )
then not not s = 0 & ... & not s = 5 ;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 ) ; :: thesis: verum
end;
suppose s > 5 ; :: thesis: ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 )
then s >= 5 + 1 by NAT_1:13;
hence ( s = 1 or s = 2 or s = 3 or s = 4 or s = 5 or s >= 6 ) ; :: thesis: verum
end;
end;
end;
end;

theorem Th135: :: NUMBER17:135
<*1*> is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem Th136: :: NUMBER17:136
<*2,2,2,2*> is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem Th137: :: NUMBER17:137
<*2,2,2,3,3,6*> is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem Th138: :: NUMBER17:138
<*2,2,2,4,4,4,4*> is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem Th139: :: NUMBER17:139
<*2,2,2,3,3,7,14,21*> is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem Th140: :: NUMBER17:140
for s being positive Nat
for f being b1 -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 end;

registration
let s be positive Nat;
let a, b, c, d be positive Real;
let f be s -element real-valued positive FinSequence;
cluster <*(a * (f . s)),(b * (f . s)),(c * (f . s)),(d * (f . s))*> -> positive-yielding ;
coherence
<*(a * (f . s)),(b * (f . s)),(c * (f . s)),(d * (f . s))*> is positive-yielding
proof end;
end;

Lm28: for s being positive Nat
for f being b1 -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 holds
ex g being b1 + 3 -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
proof end;

theorem :: NUMBER17:141
for n being Nat
for s being positive Nat
for f being b2 -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 holds
ex g being b2 + (3 * b1) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
proof end;

Lm29: now :: thesis: for s being positive Nat st s > 1 holds
(s ") ^2 <= 1 / 4
let s be positive Nat; :: thesis: ( s > 1 implies (s ") ^2 <= 1 / 4 )
assume s > 1 ; :: thesis: (s ") ^2 <= 1 / 4
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 ; :: thesis: verum
end;

Lm30: now :: thesis: for s being positive Nat st s > 2 holds
(s ") ^2 <= 1 / 9
let s be positive Nat; :: thesis: ( s > 2 implies (s ") ^2 <= 1 / 9 )
assume s > 2 ; :: thesis: (s ") ^2 <= 1 / 9
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 ; :: thesis: verum
end;

scheme :: NUMBER17:sch 1
STEP2a{ F1() -> Nat, P1[ Nat] } :
for k being Nat st k >= F1() holds
P1[k]
provided
A1: P1[F1()] and
A2: P1[F1() + 1] and
A3: for k being Nat st k >= F1() & P1[k] & P1[k + 1] holds
P1[k + 2]
proof end;

scheme :: NUMBER17:sch 2
STEP2{ P1[ Nat] } :
for k being Nat holds P1[k]
provided
A1: for k being Nat holds
( P1[2 * k] & P1[(2 * k) + 1] )
proof end;

scheme :: NUMBER17:sch 3
STEP3{ P1[ Nat] } :
for k being Nat holds P1[k]
provided
A1: for k being Nat holds
( P1[3 * k] & P1[(3 * k) + 1] & P1[(3 * k) + 2] )
proof end;

scheme :: NUMBER17:sch 4
STEP4{ P1[ Nat] } :
for k being Nat holds P1[k]
provided
A1: for k being Nat holds
( P1[4 * k] & P1[(4 * k) + 1] & P1[(4 * k) + 2] & P1[(4 * k) + 3] )
proof end;

:: Problem 165
theorem :: NUMBER17:142
for s being positive Nat holds
( ( s = 1 or s = 4 or s >= 6 ) iff ex f being b1 -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 )
proof end;

definition
let s be Nat;
let f be s + 1 -element complex-valued FinSequence;
attr f is a_solution_of_Sierp169 means :: NUMBER17:def 17
 Sum ((((f | s) (#) (f | s)) (#) (f | s)) ") = 1 / ((f . (s + 1)) |^ 3);
end;

:: deftheorem defines a_solution_of_Sierp169 NUMBER17:def 17 :
for s being Nat
for f being b1 + 1 -element complex-valued FinSequence holds
( f is a_solution_of_Sierp169 iff Sum ((((f | s) (#) (f | s)) (#) (f | s)) ") = 1 / ((f . (s + 1)) |^ 3) );

registration
let a, b, c, d be object ;
cluster <*a,b,c,d*> -> 3 + 1 -element ;
coherence
<*a,b,c,d*> is 3 + 1 -element ;
end;

theorem Th143: :: NUMBER17:143
<*12,15,20,10*> is a_solution_of_Sierp169
proof end;

registration
let a, b, c, d, e be object ;
cluster <*a,b,c,d,e*> -> 4 + 1 -element ;
coherence
<*a,b,c,d,e*> is 4 + 1 -element ;
end;

theorem Th144: :: NUMBER17:144
<*455,780,1092,5460,420*> is a_solution_of_Sierp169
proof 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
(c (#) (f | (s - 1))) ^ g is (s + 2) + 1 -element
proof end;
end;

theorem Th145: :: NUMBER17:145
for s being positive Nat
for f being b1 + 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 end;

registration
let s be positive Nat;
let a, b, c, d be positive Real;
let f be s + 1 -element real-valued positive FinSequence;
cluster <*(a * (f . s)),(b * (f . s)),(c * (f . s)),(d * (f . (s + 1)))*> -> positive-yielding ;
coherence
<*(a * (f . s)),(b * (f . s)),(c * (f . s)),(d * (f . (s + 1)))*> is positive-yielding
proof end;
end;

Lm31: for s being positive Nat
for f being b1 + 1 -element natural-valued positive FinSequence st f is a_solution_of_Sierp169 holds
ex g being (b1 + 2) + 1 -element natural-valued positive FinSequence st g is a_solution_of_Sierp169
proof end;

theorem Th146: :: NUMBER17:146
for n being Nat
for s being positive Nat
for f being b2 + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp169 holds
n (#) f is a_solution_of_Sierp169
proof end;

definition
let s be positive Nat;
assume A1: s >= 3 ;
mode Solution_of_Sierp169 of s -> s + 1 -element natural-valued positive-yielding FinSequence means :Def18: :: NUMBER17:def 18
it is a_solution_of_Sierp169 ;
existence
ex b1 being s + 1 -element natural-valued positive-yielding FinSequence st b1 is a_solution_of_Sierp169
proof end;
end;

:: deftheorem Def18 defines Solution_of_Sierp169 NUMBER17:def 18 :
for s being positive Nat st s >= 3 holds
for b2 being b1 + 1 -element natural-valued positive-yielding FinSequence holds
( b2 is Solution_of_Sierp169 of s iff b2 is a_solution_of_Sierp169 );

theorem Th147: :: NUMBER17:147
for s being positive Nat st s >= 3 holds
for f being Solution_of_Sierp169 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp169 of s : verum }
proof end;

:: Problem 169
theorem :: NUMBER17:148
for s being positive Nat st s >= 3 holds
{ f where f is Solution_of_Sierp169 of s : verum } is infinite
proof end;