:: Elementary Number Theory Problems. {P}art {XV } -- Diophantine Equations
:: by Karol P\kak and Artur Korni{\l}owicz
::
:: Received November 8, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

Lm1: 2 |^ 2 = 2 * 2
by NEWTON:81;

Lm2: 3 |^ 2 = 3 * 3
by NEWTON:81;

Lm3: 1 mod 4 = 1
by NAT_D:24;

registration

let p be Prime;

reduce In (p,SetPrimes) to p;

reducibility
In (p,SetPrimes) = p

proof end;

end;

registration

let a, b, c, d be Integer;

reduce In ([a,b,c,d],[:INT,INT,INT,INT:]) to [a,b,c,d];

reducibility
In ([a,b,c,d],[:INT,INT,INT,INT:]) = [a,b,c,d]

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite n -element FinSequence-like FinSubsequence-like natural-valued finite-support positive-yielding for set ;

existence
ex b₁ being FinSequence st
( b₁ is positive-yielding & b₁ is natural-valued & b₁ is n -element )

proof end;

end;

registration

cluster Relation-like non-empty natural-valued -> positive-yielding for set ;

coherence
for b₁ being Relation st b₁ is non-empty & b₁ is natural-valued holds
b₁ is positive-yielding

proof end;

end;

registration

let D be set ;
let f be D -valued XFinSequence;

cluster XFS2FS f -> D -valued ;

coherence
XFS2FS f is D -valued ;

end;

theorem Th1: :: NUMBER15:1

for n being Nat
for f being XFinSequence st n in dom (XFS2FS f) holds
n - 1 in dom f

proof end;

registration

let f be ext-real-valued increasing XFinSequence;

cluster XFS2FS f -> increasing ;

coherence
XFS2FS f is increasing

proof end;

end;

registration

let f be ext-real-valued decreasing XFinSequence;

cluster XFS2FS f -> decreasing ;

coherence
XFS2FS f is decreasing

proof end;

end;

registration

let f be ext-real-valued non-increasing XFinSequence;

cluster XFS2FS f -> non-increasing ;

coherence
XFS2FS f is non-increasing

proof end;

end;

registration

let f be ext-real-valued non-decreasing XFinSequence;

cluster XFS2FS f -> non-decreasing ;

coherence
XFS2FS f is non-decreasing

proof end;

end;

registration

let r be positive Real;
let f be real-valued positive-yielding Function;

cluster r (#) f -> positive-yielding ;

coherence
r (#) f is positive-yielding ;

end;

registration

let r be positive Real;
let f be real-valued increasing Function;

cluster r (#) f -> increasing ;

coherence
r (#) f is increasing

proof end;

end;

registration

let r be negative Real;
let f be real-valued increasing Function;

cluster r (#) f -> decreasing ;

coherence
r (#) f is decreasing

proof end;

end;

registration

let r be positive Real;
let f be real-valued decreasing Function;

cluster r (#) f -> decreasing ;

coherence
r (#) f is decreasing

proof end;

end;

registration

let r be negative Real;
let f be real-valued decreasing Function;

cluster r (#) f -> increasing ;

coherence
r (#) f is increasing

proof end;

end;

registration

let r be positive Real;
let f be real-valued non-increasing Function;

cluster r (#) f -> non-increasing ;

coherence
r (#) f is non-increasing

proof end;

end;

registration

let r be negative Real;
let f be real-valued non-increasing Function;

cluster r (#) f -> non-decreasing ;

coherence
r (#) f is non-decreasing

proof end;

end;

registration

let r be positive Real;
let f be real-valued non-decreasing Function;

cluster r (#) f -> non-decreasing ;

coherence
r (#) f is non-decreasing

proof end;

end;

registration

let r be negative Real;
let f be real-valued non-decreasing Function;

cluster r (#) f -> non-increasing ;

coherence
r (#) f is non-increasing

proof end;

end;

theorem Th2: :: NUMBER15:2

for f being finite-support Function holds rng f c= (rng (f | (support f))) \/ {0}

proof end;

registration

let f be finite-support Function;

cluster proj2 f -> finite ;

coherence
rng f is finite

proof end;

end;

theorem Th3: :: NUMBER15:3

for f being complex-valued FinSequence
for g being FinSequence of F_Complex st f = g holds
Product f = Product g

proof end;

theorem Th4: :: NUMBER15:4

for a being Complex
for p, q being complex-valued FinSequence st len p = len q & ex i being Nat st
( i in dom p & q . i = a * (p . i) & ( for j being Nat st j in dom p & i <> j holds
q . j = p . j ) ) holds
Product q = a * (Product p)

proof end;

theorem Th5: :: NUMBER15:5

for m, n being Nat holds
( ( not n mod 4 = 0 & not n mod 4 = 2 ) or (n * m) mod 4 = 0 or (n * m) mod 4 = 2 )

proof end;

theorem Th6: :: NUMBER15:6

for m, n being Nat holds
( not (n * m) mod 4 = 1 or n mod 4 = 1 or n mod 4 = 3 )

proof end;

theorem Th7: :: NUMBER15:7

for m, n being Nat holds
( not (n * m) mod 4 = 3 or ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) )

proof end;

theorem Th8: :: NUMBER15:8

for m, n being Nat st ( ( n mod 4 = 1 & m mod 4 = 1 ) or ( n mod 4 = 3 & m mod 4 = 3 ) ) holds
(n * m) mod 4 = 1

proof end;

theorem Th9: :: NUMBER15:9

for m, n being Nat st ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) holds
(n * m) mod 4 = 3

proof end;

Lm4: for k, n being Nat st n <> 1 & n divides 2 |^ k & not n mod 4 = 0 holds
n mod 4 = 2

proof end;

theorem Th10: :: NUMBER15:10

for k, n being Nat
for p being Prime st p is prime & p mod 4 = 1 & n divides p |^ k holds
n mod 4 = 1

proof end;

theorem Th11: :: NUMBER15:11

for n being Nat
for p being Prime st p mod 4 = 3 holds
( (p |^ (2 * n)) mod 4 = 1 & (p |^ ((2 * n) + 1)) mod 4 = 3 )

proof end;

definition

let n, m, r be Integer;

func divisors (n,m,r) -> Subset of NAT equals :: NUMBER15:def 1
{ k where k is Nat : ( k mod m = r & k divides n ) } ;

coherence
{ k where k is Nat : ( k mod m = r & k divides n ) } is Subset of NAT

proof end;

end;

:: deftheorem defines divisors NUMBER15:def 1 :
for n, m, r being Integer holds divisors (n,m,r) = { k where k is Nat : ( k mod m = r & k divides n ) } ;

theorem Th12: :: NUMBER15:12

for k being Nat
for n, m, r being Integer holds
( k in divisors (n,m,r) iff ( k mod m = r & k divides n ) )

proof end;

registration

let n be positive Nat;
let m, r be Integer;

cluster divisors (n,m,r) -> finite ;

coherence
divisors (n,m,r) is finite

proof end;

end;

theorem Th13: :: NUMBER15:13

for k being Nat
for n, m, r, p being Integer holds
( k in (divisors (n,m,r)) \/ (divisors (n,m,p)) iff ( ( k mod m = r or k mod m = p ) & k divides n ) )

proof end;

theorem Th14: :: NUMBER15:14

for k being Nat
for i, n, m, r being Integer st k <> i holds
divisors (n,m,k) misses divisors (n,m,i)

proof end;

theorem Th15: :: NUMBER15:15

for n being Nat holds
( divisors ((2 |^ n),4,3) = {} & divisors ((2 |^ n),4,1) = {1} )

proof end;

Lm5: for X being finite set
for X1 being set
for p being Prime
for i being Nat st X = { k where k is Nat : k divides p |^ i } & X1 = { k where k is Nat : k divides p |^ (i + 1) } holds
( not p |^ (i + 1) in X & X \/ {(p |^ (i + 1))} = X1 )

proof end;

theorem Th16: :: NUMBER15:16

for p being Prime
for n being Nat holds card { k where k is Nat : k divides p |^ n } = n + 1

proof end;

theorem Th17: :: NUMBER15:17

for p being Prime
for n being Nat st p mod 4 = 1 holds
( card (divisors ((p |^ n),4,1)) = n + 1 & card (divisors ((p |^ n),4,3)) = 0 )

proof end;

theorem Th18: :: NUMBER15:18

for p being Prime
for m, n being Nat st p mod 4 = 3 holds
( (divisors ((p |^ n),4,1)) \/ (divisors ((p |^ n),4,3)) = { k where k is Nat : k divides p |^ n } & ( n = 2 * m implies ( card (divisors ((p |^ n),4,1)) = m + 1 & card (divisors ((p |^ n),4,3)) = m ) ) & ( n = (2 * m) + 1 implies ( card (divisors ((p |^ n),4,1)) = m + 1 & card (divisors ((p |^ n),4,3)) = m + 1 ) ) )

proof end;

theorem Th19: :: NUMBER15:19

for p being Prime holds
( not p is prime or p = 2 or p mod 4 = 1 or p mod 4 = 3 )

proof end;

Lm6: for n being Nat
for p being Prime holds card (divisors ((p |^ n),4,1)) >= card (divisors ((p |^ n),4,3))

proof end;

theorem Th20: :: NUMBER15:20

for n being Nat st n > 1 holds
ex p being Prime st
( p divides n & ( for q being Prime st q divides n holds
q <= p ) )

proof end;

theorem Th21: :: NUMBER15:21

for n being Nat
for p being Prime st n is positive & p is prime & p divides n holds
ex k, m being positive Nat st
( 0 < k & n = m * (p |^ k) & m,p are_coprime )

proof end;

theorem :: NUMBER15:22

for n being non zero Nat holds card (divisors (n,4,3)) <= card (divisors (n,4,1))

proof end;

Lm7: for n being Nat ex k being Nat st 3 |^ (2 * n) = (4 * k) + 1

proof end;

theorem Th23: :: NUMBER15:23

for m being Nat st m is even holds
(3 |^ m) mod 4 = 1

proof end;

Lm8: for n being Nat ex k being Nat st 3 |^ ((2 * n) + 1) = (4 * k) + 3

proof end;

theorem Th24: :: NUMBER15:24

for m being Nat st m is odd holds
(3 |^ m) mod 4 = 3

proof end;

theorem Th25: :: NUMBER15:25

for n being Nat holds divisors ((3 |^ ((2 * n) + 1)),4,1) = { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) }

proof end;

theorem Th26: :: NUMBER15:26

for n being Nat holds divisors ((3 |^ ((2 * n) + 1)),4,3) = { (3 |^ m) where m is Nat : ( m is odd & m <= (2 * n) + 1 ) }

proof end;

theorem Th27: :: NUMBER15:27

for n being Nat holds card { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } = n + 1

proof end;

theorem Th28: :: NUMBER15:28

for n being Nat holds card { (3 |^ m) where m is Nat : ( m is odd & m <= (2 * n) + 1 ) } = n + 1

proof end;

theorem Th29: :: NUMBER15:29

for n being Nat holds card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = n + 1

proof end;

theorem Th30: :: NUMBER15:30

for n being Nat holds card (divisors ((3 |^ ((2 * n) + 1)),4,3)) = n + 1

proof end;

Lm9: for n being non zero Nat holds { k where k is Nat : k divides n } is finite

proof end;

theorem Th31: :: NUMBER15:31

for n being Nat holds card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3))

proof end;

theorem :: NUMBER15:32

{ n where n is Nat : card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3)) } is infinite

proof end;

theorem :: NUMBER15:33

{ n where n is Nat : card (divisors (n,4,1)) = card (divisors (n,4,3)) } is infinite

proof end;

theorem Th34: :: NUMBER15:34

for k, n being Nat st k divides 5 |^ n holds
k mod 4 = 1

proof end;

theorem :: NUMBER15:35

for n, k being Nat holds
( not k mod 4 = 3 or not k divides 5 |^ n ) by Th34;

theorem Th36: :: NUMBER15:36

for n being Nat holds { k where k is Nat : k divides 5 |^ n } = divisors ((5 |^ n),4,1)

proof end;

theorem Th37: :: NUMBER15:37

for n being Nat holds card { k where k is Nat : k divides 5 |^ n } = n + 1

proof end;

theorem Th38: :: NUMBER15:38

for n being Nat holds divisors ((5 |^ n),4,3) = {}

proof end;

theorem :: NUMBER15:39

{ n where n is Nat : card (divisors ((5 |^ n),4,1)) > card (divisors ((5 |^ n),4,3)) } is infinite

proof end;

theorem :: NUMBER15:40

{ n where n is positive Nat : card (divisors (n,4,1)) > card (divisors (n,4,3)) } is infinite

proof end;

definition

let X be set ;

attr X is positive-membered means :Def2: :: NUMBER15:def 2
for x being ExtReal st x in X holds
x > 0 ;

end;

:: deftheorem Def2 defines positive-membered NUMBER15:def 2 :
for X being set holds
( X is positive-membered iff for x being ExtReal st x in X holds
x > 0 );

registration

let n be non zero Nat;

cluster {n} -> positive-membered ;

coherence
{n} is positive-membered ;
let m be non zero Nat;

cluster {m,n} -> positive-membered ;

coherence
{m,n} is positive-membered ;

end;

registration

cluster NAT \ {0} -> positive-membered ;

coherence
NAT \ {0} is positive-membered ;

end;

registration

cluster non empty finite positive-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is finite & b₁ is positive-membered )

proof end;

end;

registration

cluster infinite positive-membered for set ;

existence
ex b₁ being set st
( b₁ is infinite & b₁ is positive-membered )

proof end;

end;

theorem :: NUMBER15:41

for A being positive-membered set
for B being set st B c= A holds
B is positive-membered by Def2;

registration

let A be positive-membered set ;

cluster -> positive-membered for Element of bool A;

coherence
for b₁ being Subset of A holds b₁ is positive-membered by Def2;

end;

registration

let X be positive-membered set ;

cluster Relation-like X -valued -> positive-yielding for set ;

coherence
for b₁ being Relation st b₁ is X -valued holds
b₁ is positive-yielding

proof end;

end;

registration

let n be Nat;

cluster Seg n -> positive-membered ;

coherence
Seg n is positive-membered by FINSEQ_1:1;

end;

registration

let X be positive-membered set ;

cluster id X -> positive-yielding ;

coherence
id X is positive-yielding ;

end;

registration

let n be Nat;

cluster idseq n -> positive-yielding ;

coherence
idseq n is positive-yielding ;

end;

registration

let n be Nat;

cluster idseq n -> increasing ;

coherence
idseq n is increasing

proof end;

end;

registration

cluster SetPrimes -> positive-membered ;

coherence
SetPrimes is positive-membered

proof end;

end;

definition

let s be Nat;

func PrimeNumbersS s -> sequence of SetPrimes means :Def3: :: NUMBER15:def 3
for n being Nat holds it . n = primenumber n;

existence
ex b₁ being sequence of SetPrimes st
for n being Nat holds b₁ . n = primenumber n

proof end;

uniqueness
for b₁, b₂ being sequence of SetPrimes st ( for n being Nat holds b₁ . n = primenumber n ) & ( for n being Nat holds b₂ . n = primenumber n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines PrimeNumbersS NUMBER15:def 3 :
for s being Nat
for b₂ being sequence of SetPrimes holds
( b₂ = PrimeNumbersS s iff for n being Nat holds b₂ . n = primenumber n );

registration

let s be Nat;

cluster PrimeNumbersS s -> increasing ;

coherence
PrimeNumbersS s is increasing

proof end;

end;

registration

let s be Nat;

cluster PrimeNumbersS s -> onto ;

coherence
PrimeNumbersS s is onto

proof end;

end;

registration

let s be Nat;

cluster (PrimeNumbersS s) | s -> increasing ;

coherence
(PrimeNumbersS s) | s is increasing ;

end;

definition

let s be Nat;

func PrimeNumbersFS s -> FinSequence of SetPrimes equals :: NUMBER15:def 4
XFS2FS ((PrimeNumbersS s) | s);

coherence
XFS2FS ((PrimeNumbersS s) | s) is FinSequence of SetPrimes

proof end;

end;

:: deftheorem defines PrimeNumbersFS NUMBER15:def 4 :
for s being Nat holds PrimeNumbersFS s = XFS2FS ((PrimeNumbersS s) | s);

theorem Th42: :: NUMBER15:42

for s being Nat holds len (PrimeNumbersFS s) = s

proof end;

theorem Th43: :: NUMBER15:43

for n, s being Nat st n < s holds
(PrimeNumbersFS s) . (n + 1) = primenumber n

proof end;

theorem Th44: :: NUMBER15:44

for n being non zero Nat
for s being Nat st n <= s holds
(PrimeNumbersFS s) . n = primenumber (n - 1)

proof end;

registration

let s be Nat;

cluster PrimeNumbersFS s -> increasing ;

coherence
PrimeNumbersFS s is increasing ;

end;

registration

let s be Nat;

cluster PrimeNumbersFS s -> positive-yielding ;

coherence
PrimeNumbersFS s is positive-yielding ;

end;

registration

let s be non zero Nat;

cluster PrimeNumbersFS s -> non empty ;

coherence
not PrimeNumbersFS s is empty

proof end;

end;

registration

let s be non zero Nat;

cluster PrimeNumbersFS s -> Chinese_Remainder ;

coherence
PrimeNumbersFS s is Chinese_Remainder

proof end;

end;

theorem Th45: :: NUMBER15:45

for k, s being Nat st k < s holds
(Product (PrimeNumbersFS s)) / (primenumber k) is Nat

proof end;

definition

let s be Nat;

func sequenceA s -> FinSequence of NAT means :Def5: :: NUMBER15:def 5
( len it = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
it . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) );

existence
ex b₁ being FinSequence of NAT st
( len b₁ = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
b₁ . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
b₁ . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) & len b₂ = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
b₂ . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines sequenceA NUMBER15:def 5 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceA s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
for e being Nat st e = (Product (PrimeNumbersFS s)) / (primenumber (k - 1)) holds
b₂ . k = (CRT (0,e,(- 1),(primenumber (k - 1)))) + (Product (PrimeNumbersFS s)) ) ) );

registration

let s be Nat;

cluster sequenceA s -> s -element ;

coherence
sequenceA s is s -element by Def5;

end;

registration

let s be Nat;

cluster sequenceA s -> positive-yielding ;

coherence
sequenceA s is positive-yielding

proof end;

end;

theorem Th46: :: NUMBER15:46

for k, s being non zero Nat st k <= s holds
primenumber (k - 1) divides ((sequenceA s) . k) + 1

proof end;

theorem Th47: :: NUMBER15:47

for s being Nat
for k, n being non zero Nat st k <> n & n <= s & k <= s holds
primenumber (k - 1) divides (sequenceA s) . n

proof end;

definition

let f, g be real-valued Function;
deffunc H₁( object ) -> object = (f . $1) to_power (g . $1);
set X = (dom f) /\ (dom g);

func f to_power g -> Function means :Def6: :: NUMBER15:def 6
( dom it = (dom f) /\ (dom g) & ( for x being object st x in dom it holds
it . x = (f . x) to_power (g . x) ) );

existence
ex b₁ being Function st
( dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in dom b₁ holds
b₁ . x = (f . x) to_power (g . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) /\ (dom g) & ( for x being object st x in dom b₁ holds
b₁ . x = (f . x) to_power (g . x) ) & dom b₂ = (dom f) /\ (dom g) & ( for x being object st x in dom b₂ holds
b₂ . x = (f . x) to_power (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines to_power NUMBER15:def 6 :
for f, g being real-valued Function
for b₃ being Function holds
( b₃ = f to_power g iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being object st x in dom b₃ holds
b₃ . x = (f . x) to_power (g . x) ) ) );

registration

let f, g be real-valued FinSequence;

cluster f to_power g -> FinSequence-like ;

coherence
f to_power g is FinSequence-like

proof end;

end;

registration

let n be Nat;
let f, g be n -element real-valued FinSequence;

cluster f to_power g -> n -element ;

coherence
f to_power g is n -element

proof end;

end;

registration

let f, g be real-valued Function;

cluster f to_power g -> REAL -valued ;

coherence
f to_power g is REAL -valued

proof end;

end;

registration

let f be rational-valued Function;
let g be integer-valued Function;

cluster f to_power g -> RAT -valued ;

coherence
f to_power g is RAT -valued

proof end;

end;

registration

let f be integer-valued Function;
let g be natural-valued Function;

cluster f to_power g -> INT -valued ;

coherence
f to_power g is INT -valued

proof end;

end;

registration

let f, g be natural-valued Function;

cluster f to_power g -> NAT -valued ;

coherence
f to_power g is NAT -valued

proof end;

end;

registration

let f, g be real-valued positive-yielding Function;

cluster f to_power g -> positive-yielding ;

coherence
f to_power g is positive-yielding

proof end;

end;

definition

let s be Nat;

func numberQ s -> Nat equals :: NUMBER15:def 7
Product ((idseq s) to_power (sequenceA s));

coherence
Product ((idseq s) to_power (sequenceA s)) is Nat by TARSKI:1;

end;

:: deftheorem defines numberQ NUMBER15:def 7 :
for s being Nat holds numberQ s = Product ((idseq s) to_power (sequenceA s));

registration

let s be Nat;

cluster numberQ s -> positive ;

coherence
numberQ s is positive ;

end;

definition

let s be Nat;

func Problem58Solution s -> FinSequence of NAT equals :: NUMBER15:def 8
(numberQ s) (#) (idseq s);

coherence
(numberQ s) (#) (idseq s) is FinSequence of NAT by FINSEQ_1:103;

end;

:: deftheorem defines Problem58Solution NUMBER15:def 8 :
for s being Nat holds Problem58Solution s = (numberQ s) (#) (idseq s);

registration

let s be Nat;

cluster Problem58Solution s -> s -element ;

coherence
Problem58Solution s is s -element ;

end;

theorem Th48: :: NUMBER15:48

for k, s being Nat st 1 <= k & k <= s holds
(Problem58Solution s) . k = k * (numberQ s)

proof end;

registration

let s be Nat;

cluster Problem58Solution s -> increasing positive-yielding ;

coherence
( Problem58Solution s is increasing & Problem58Solution s is positive-yielding ) ;

end;

definition

let s be Nat;
set A = sequenceA s;
deffunc H₁( non zero Nat) -> set = (((sequenceA s) . $1) + 1) / (primenumber ($1 - 1));

func sequenceAk1Pk s -> FinSequence of NAT means :Def9: :: NUMBER15:def 9
( len it = s & ( for k being non zero Nat st k <= s holds
it . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) );

existence
ex b₁ being FinSequence of NAT st
( len b₁ = s & ( for k being non zero Nat st k <= s holds
b₁ . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = s & ( for k being non zero Nat st k <= s holds
b₁ . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) & len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines sequenceAk1Pk NUMBER15:def 9 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceAk1Pk s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (((sequenceA s) . k) + 1) / (primenumber (k - 1)) ) ) );

registration

let s be Nat;

cluster sequenceAk1Pk s -> s -element ;

coherence
sequenceAk1Pk s is s -element by Def9;

end;

definition

let s be Nat;
let k be non zero Nat;
assume A1: k <= s ;
set A = sequenceA s;
set p = primenumber (k - 1);
deffunc H₁( non zero Nat) -> set = ((sequenceA s) . $1) / (primenumber (k - 1));

func sequenceAnPk (s,k) -> FinSequence of NAT means :Def10: :: NUMBER15:def 10
( len it = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies it . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies it . n = 0 ) ) ) );

existence
ex b₁ being FinSequence of NAT st
( len b₁ = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies b₁ . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies b₁ . n = 0 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies b₁ . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies b₁ . n = 0 ) ) ) & len b₂ = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies b₂ . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies b₂ . n = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines sequenceAnPk NUMBER15:def 10 :
for s being Nat
for k being non zero Nat st k <= s holds
for b₃ being FinSequence of NAT holds
( b₃ = sequenceAnPk (s,k) iff ( len b₃ = s & ( for n being non zero Nat st n <= s holds
( ( n <> k implies b₃ . n = ((sequenceA s) . n) / (primenumber (k - 1)) ) & ( n = k implies b₃ . n = 0 ) ) ) ) );

definition

let s be Nat;
deffunc H₁( non zero Nat) -> set = ($1 |^ ((sequenceAk1Pk s) . $1)) * (Product ((idseq s) to_power (sequenceAnPk (s,$1))));

func sequenceQk s -> FinSequence of NAT means :Def11: :: NUMBER15:def 11
( len it = s & ( for k being non zero Nat st k <= s holds
it . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) );

existence
ex b₁ being FinSequence of NAT st
( len b₁ = s & ( for k being non zero Nat st k <= s holds
b₁ . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = s & ( for k being non zero Nat st k <= s holds
b₁ . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) & len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines sequenceQk NUMBER15:def 11 :
for s being Nat
for b₂ being FinSequence of NAT holds
( b₂ = sequenceQk s iff ( len b₂ = s & ( for k being non zero Nat st k <= s holds
b₂ . k = (k |^ ((sequenceAk1Pk s) . k)) * (Product ((idseq s) to_power (sequenceAnPk (s,k)))) ) ) );

registration

let s be Nat;

cluster sequenceQk s -> s -element ;

coherence
sequenceQk s is s -element by Def11;

end;

theorem Th49: :: NUMBER15:49

for s being Nat
for k, w being non zero Nat st k <= s & w <= s & w <> k holds
((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w

proof end;

theorem Th50: :: NUMBER15:50

for s being Nat
for k being non zero Nat st k <= s holds
(Problem58Solution s) . k = ((sequenceQk s) . k) |^ (primenumber (k - 1))

proof end;

registration

cluster Relation-like omega -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued increasing Cardinal-yielding finite-support fAP-like positive-yielding for FinSequence of NAT ;

existence
ex b₁ being FinSequence of NAT st
( b₁ is fAP-like & b₁ is increasing & b₁ is positive-yielding )

proof end;

end;

registration

let s be Nat;

cluster Problem58Solution s -> fAP-like ;

coherence
Problem58Solution s is fAP-like

proof end;

end;

theorem :: NUMBER15:51

for s being Nat ex f being increasing fAP-like positive-yielding FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power ) )

proof end;

theorem :: NUMBER15:52

for x, y, z, t being positive Nat st x <= y & y <= z & z <= t holds
( (((1 / x) + (1 / y)) + (1 / z)) + (1 / t) = 1 iff ( ( x = 2 & y = 3 & z = 7 & t = 42 ) or ( x = 2 & y = 3 & z = 8 & t = 24 ) or ( x = 2 & y = 3 & z = 9 & t = 18 ) or ( x = 2 & y = 3 & z = 10 & t = 15 ) or ( x = 2 & y = 3 & z = 12 & t = 12 ) or ( x = 2 & y = 4 & z = 5 & t = 20 ) or ( x = 2 & y = 4 & z = 6 & t = 12 ) or ( x = 2 & y = 4 & z = 8 & t = 8 ) or ( x = 2 & y = 5 & z = 5 & t = 10 ) or ( x = 2 & y = 6 & z = 6 & t = 6 ) or ( x = 3 & y = 3 & z = 4 & t = 12 ) or ( x = 3 & y = 3 & z = 6 & t = 6 ) or ( x = 3 & y = 4 & z = 4 & t = 6 ) or ( x = 4 & y = 4 & z = 4 & t = 4 ) ) )

proof end;

Lm10: for r being Integer st r >= 2 holds
1 / (r ^2) <= 1 / 4

proof end;

Lm11: for r being Integer st r > 2 holds
1 / (r ^2) <= 1 / 9

proof end;

theorem :: NUMBER15:53

for x, y, z, t being positive Integer holds
( (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 iff ( x = 2 & y = 2 & z = 2 & t = 2 ) )

proof end;

theorem Th54: :: NUMBER15:54

for f being complex-valued FinSequence holds len (f ^2) = len f

proof end;

theorem Th55: :: NUMBER15:55

for f being complex-valued FinSequence holds len (f ") = len f

proof end;

theorem Th56: :: NUMBER15:56

for n being Nat
for c being Complex
for f being complex-valued FinSequence holds (c (#) f) | n = c (#) (f | n)

proof end;

theorem Th57: :: NUMBER15:57

for f being complex-valued Function holds (f ") ^2 = (f ^2) "

proof end;

theorem Th58: :: NUMBER15:58

for c being Complex
for f being complex-valued Function holds (c (#) f) " = (c ") (#) (f ")

proof end;

theorem Th59: :: NUMBER15:59

for f, g being complex-valued FinSequence holds (f ^ g) ^2 = (f ^2) ^ (g ^2)

proof end;

theorem Th60: :: NUMBER15:60

for f, g being complex-valued FinSequence holds (f ^ g) " = (f ") ^ (g ")

proof end;

theorem Th61: :: NUMBER15:61

for n being Nat
for f being complex-valued FinSequence holds (f | n) " = (f ") | n

proof end;

theorem Th62: :: NUMBER15:62

for n being Nat
for f being complex-valued FinSequence holds (f | n) ^2 = (f ^2) | n

proof end;

theorem Th63: :: NUMBER15:63

for c being Complex holds <*c*> " = <*(c ")*>

proof end;

theorem Th64: :: NUMBER15:64

for c1, c2 being Complex holds <*c1,c2*> " = <*(c1 "),(c2 ")*>

proof end;

theorem :: NUMBER15:65

for c1, c2, c3 being Complex holds <*c1,c2,c3*> " = <*(c1 "),(c2 "),(c3 ")*>

proof end;

definition

let s be Nat;
let f be s + 1 -element complex-valued FinSequence;

attr f is a_solution_of_Sierp168 means :: NUMBER15:def 12
Sum (((f | s) ") ^2) = 1 / ((f . (s + 1)) ^2);

end;

:: deftheorem defines a_solution_of_Sierp168 NUMBER15:def 12 :
for s being Nat
for f being b₁ + 1 -element complex-valued FinSequence holds
( f is a_solution_of_Sierp168 iff Sum (((f | s) ") ^2) = 1 / ((f . (s + 1)) ^2) );

registration

let a be object ;

cluster <*a*> -> 0 + 1 -element ;

coherence
<*a*> is 0 + 1 -element ;

end;

registration

let a, b be object ;

cluster <*a,b*> -> 1 + 1 -element ;

coherence
<*a,b*> is 1 + 1 -element ;

end;

registration

let a, b, c be object ;

cluster <*a,b,c*> -> 2 + 1 -element ;

coherence
<*a,b,c*> is 2 + 1 -element ;

end;

theorem :: NUMBER15:66

<*0*> is a_solution_of_Sierp168 ;

theorem Th67: :: NUMBER15:67

<*1,1*> is a_solution_of_Sierp168

proof end;

theorem :: NUMBER15:68

<*15,20,12*> is a_solution_of_Sierp168

proof end;

theorem Th69: :: NUMBER15:69

for s, n being Nat
for f being b₁ + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp168 holds
n (#) f is a_solution_of_Sierp168

proof end;

definition

let s be positive Nat;
let f be s + 1 -element complex-valued FinSequence;

func SierpProblem168FS f -> FinSequence equals :: NUMBER15:def 13
(12 (#) (f | (s - 1))) ^ <*(15 * (f . s)),(20 * (f . s)),(12 * (f . (s + 1)))*>;

coherence
(12 (#) (f | (s - 1))) ^ <*(15 * (f . s)),(20 * (f . s)),(12 * (f . (s + 1)))*> is FinSequence ;

end;

:: deftheorem defines SierpProblem168FS NUMBER15:def 13 :
for s being positive Nat
for f being b₁ + 1 -element complex-valued FinSequence holds SierpProblem168FS f = (12 (#) (f | (s - 1))) ^ <*(15 * (f . s)),(20 * (f . s)),(12 * (f . (s + 1)))*>;

registration

let s be positive Nat;
let f be s + 1 -element complex-valued FinSequence;

cluster SierpProblem168FS f -> (s + 1) + 1 -element ;

coherence
SierpProblem168FS f is (s + 1) + 1 -element

proof end;

end;

registration

let s be positive Nat;
let f be s + 1 -element complex-valued FinSequence;

cluster SierpProblem168FS f -> complex-valued ;

coherence
SierpProblem168FS f is complex-valued ;

end;

registration

let s be positive Nat;
let f be s + 1 -element real-valued FinSequence;

cluster SierpProblem168FS f -> real-valued ;

coherence
SierpProblem168FS f is real-valued ;

end;

registration

let s be positive Nat;
let f be s + 1 -element integer-valued FinSequence;

cluster SierpProblem168FS f -> integer-valued ;

coherence
SierpProblem168FS f is integer-valued ;

end;

registration

let s be positive Nat;
let f be s + 1 -element natural-valued FinSequence;

cluster SierpProblem168FS f -> natural-valued ;

coherence
SierpProblem168FS f is natural-valued ;

end;

registration

let c be non zero Complex;

cluster <*c*> -> non-empty ;

coherence
<*c*> is non-empty

proof end;

let f be non-empty complex-valued FinSequence;

cluster c (#) f -> non-empty ;

coherence
c (#) f is non-empty

proof end;

end;

registration

let s be positive Nat;
let f be non-empty s + 1 -element real-valued FinSequence;

cluster SierpProblem168FS f -> non-empty ;

coherence
SierpProblem168FS f is non-empty

proof end;

end;

theorem Th70: :: NUMBER15:70

for s being positive Nat ex f being non-empty b₁ + 1 -element natural-valued FinSequence st f is a_solution_of_Sierp168

proof end;

definition

let s be positive Nat;

mode Solution_of_Sierp168 of s -> s + 1 -element natural-valued positive-yielding FinSequence means :Def14: :: NUMBER15:def 14
it is a_solution_of_Sierp168 ;

existence
ex b₁ being s + 1 -element natural-valued positive-yielding FinSequence st b₁ is a_solution_of_Sierp168 by Th70;

end;

:: deftheorem Def14 defines Solution_of_Sierp168 NUMBER15:def 14 :
for s being positive Nat
for b₂ being b₁ + 1 -element natural-valued positive-yielding FinSequence holds
( b₂ is Solution_of_Sierp168 of s iff b₂ is a_solution_of_Sierp168 );

registration

let s be positive Nat;

cluster -> a_solution_of_Sierp168 for Solution_of_Sierp168 of s;

coherence
for b₁ being Solution_of_Sierp168 of s holds b₁ is a_solution_of_Sierp168 by Def14;

end;

registration

let s, n be positive Nat;
let f be Solution_of_Sierp168 of s;

cluster n (#) f -> a_solution_of_Sierp168 ;

coherence
n (#) f is a_solution_of_Sierp168 by Th69;

end;

theorem :: NUMBER15:71

for s, n being positive Nat
for f being Solution_of_Sierp168 of s holds n (#) f is Solution_of_Sierp168 of s by Def14;

definition

let s be positive Nat;
let f be s + 1 -element natural-valued positive-yielding FinSequence;

func Solutions_of_Sierp168 f -> ManySortedSet of NATPLUS means :Def15: :: NUMBER15:def 15
for n being non zero Nat holds it . n = n (#) f;

existence
ex b₁ being ManySortedSet of NATPLUS st
for n being non zero Nat holds b₁ . n = n (#) f

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of NATPLUS st ( for n being non zero Nat holds b₁ . n = n (#) f ) & ( for n being non zero Nat holds b₂ . n = n (#) f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Solutions_of_Sierp168 NUMBER15:def 15 :
for s being positive Nat
for f being b₁ + 1 -element natural-valued positive-yielding FinSequence
for b₃ being ManySortedSet of NATPLUS holds
( b₃ = Solutions_of_Sierp168 f iff for n being non zero Nat holds b₃ . n = n (#) f );

registration

let s be positive Nat;
let f be s + 1 -element natural-valued positive-yielding FinSequence;

cluster Solutions_of_Sierp168 f -> one-to-one ;

coherence
Solutions_of_Sierp168 f is one-to-one

proof end;

end;

theorem Th72: :: NUMBER15:72

for s being positive Nat
for f being Solution_of_Sierp168 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp168 of s : verum }

proof end;

theorem :: NUMBER15:73

for S being positive Nat holds { f where f is Solution_of_Sierp168 of S : verum } is infinite

proof end;

theorem Th74: :: NUMBER15:74

for n being positive Integer holds
( ( n <= 7 or n in {9,10,12,15} ) iff for x, y being positive Integer holds not (3 * x) + (5 * y) = n )

proof end;

theorem :: NUMBER15:75

for m, n being positive Integer st n > 40 * m holds
for A being finite set st A = { [x,y] where x, y is positive Integer : (3 * x) + (5 * y) = n } holds
card A > m

proof end;

Lm12: for x, y, z, t being Nat holds
( not (x ^2) + (2 * (y ^2)) = z ^2 or not (2 * (x ^2)) + (y ^2) = t ^2 or not x,y are_coprime )

proof end;

theorem Th76: :: NUMBER15:76

for m being Nat
for i being Integer st m <> 0 holds
i div (i gcd m),m div (i gcd m) are_coprime by RING_3:14;

theorem :: NUMBER15:77

for x, y, z, t being positive Nat holds
( not (x ^2) + (2 * (y ^2)) = z ^2 or not (2 * (x ^2)) + (y ^2) = t ^2 )

proof end;

theorem Th78: :: NUMBER15:78

for n being Nat holds
( not n is even or n mod 4 = 0 or n mod 4 = 2 )

proof end;

theorem :: NUMBER15:79

for n being Nat holds
( not n is even or n, 0 are_congruent_mod 4 or n,2 are_congruent_mod 4 )

proof end;

theorem Th80: :: NUMBER15:80

for n being Nat holds
( not n is odd or n mod 4 = 1 or n mod 4 = 3 )

proof end;

theorem Th81: :: NUMBER15:81

for n being Nat holds
( not n is odd or n,1 are_congruent_mod 4 or n,3 are_congruent_mod 4 )

proof end;

theorem Th82: :: NUMBER15:82

for i being Integer st i is even holds
(i |^ 3) mod 8 = 0

proof end;

theorem :: NUMBER15:83

for k being non zero Nat
for x, y being positive Nat holds not ((x |^ 2) + (2 |^ (2 * k))) + 1 = y |^ 3

proof end;

theorem :: NUMBER15:84

for x, y, z, t being positive Nat st x <= y & x <= z & z <= t holds
( ( x + y = z * t & z + t = x * y ) iff ( ( x = 1 & y = 5 & z = 2 & t = 3 ) or ( x = 2 & y = 2 & z = 2 & t = 2 ) ) )

proof end;

deffunc H₁( Nat) -> object = - 1;

deffunc H₂( Nat) -> Nat = $1;

deffunc H₃( Nat) -> set = 1 - H₂($1);

deffunc H₄( Nat) -> object = - 1;

deffunc H₅( Nat) -> object = [H₁($1),H₂($1),H₃($1),H₄($1)];

definition

func exampleSierpinski196 -> Function of NAT,[:INT,INT,INT,INT:] means :Def16: :: NUMBER15:def 16
for n being Nat holds it . n = [(- 1),n,(1 - n),(- 1)];

existence
ex b₁ being Function of NAT,[:INT,INT,INT,INT:] st
for n being Nat holds b₁ . n = [(- 1),n,(1 - n),(- 1)]

proof end;

uniqueness
for b₁, b₂ being Function of NAT,[:INT,INT,INT,INT:] st ( for n being Nat holds b₁ . n = [(- 1),n,(1 - n),(- 1)] ) & ( for n being Nat holds b₂ . n = [(- 1),n,(1 - n),(- 1)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines exampleSierpinski196 NUMBER15:def 16 :
for b₁ being Function of NAT,[:INT,INT,INT,INT:] holds
( b₁ = exampleSierpinski196 iff for n being Nat holds b₁ . n = [(- 1),n,(1 - n),(- 1)] );

set f = exampleSierpinski196 ;

registration

cluster exampleSierpinski196 -> one-to-one ;

coherence
exampleSierpinski196 is one-to-one

proof end;

end;

theorem Th85: :: NUMBER15:85

rng exampleSierpinski196 c= { [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) }

proof end;

theorem :: NUMBER15:86

{ [x,y,z,t] where x, y, z, t is Integer : ( x + y = z * t & z + t = x * y ) } is infinite

proof end;

registration

let r be non negative Real;

cluster [/r\] -> natural ;

coherence
[/r\] is natural by INT_1:53;

end;

registration

let f be non empty real-valued positive-yielding FinSequence;

cluster Sum f -> positive ;

coherence
Sum f is positive by PRSUBSET:4;

end;

registration

let a, b be positive Real;
let n be Nat;

cluster (a,b) Subnomial n -> positive-yielding ;

coherence
(a,b) Subnomial n is positive-yielding

proof end;

end;

registration

let r be non positive Real;

cluster <*r*> -> non positive-yielding ;

coherence
not <*r*> is positive-yielding

proof end;

end;

theorem Th87: :: NUMBER15:87

for a being Real
for n, x, y being positive Nat st a > 0 & 2 <= n & (x |^ n) - (y |^ n) = a holds
( x < (n - 1) -Root a & y < (n - 1) -Root a )

proof end;

theorem :: NUMBER15:88

for a being Real
for k, x, y being positive Nat st a > 0 & (x |^ (2 * k)) - (y |^ (2 * k)) = a holds
( x < k -Root a & y < k -Root a )

proof end;

theorem :: NUMBER15:89

for a, x, y being Complex holds
( (x |^ 1) - (y |^ 1) = a iff x = a + y ) ;

scheme :: NUMBER15:sch 1
FinitePairs{ F₁() -> Nat, F₂() -> Nat, P₁[ object , object ] } :

{ [m,n] where m, n is Nat : ( m < F₁() & n < F₂() & P₁[m,n] ) } is finite

proof end;

:: Method - finite number of checking

theorem :: NUMBER15:90

for a, n being positive Nat st 2 <= n holds
{ [x,y] where x, y is positive Nat : (x |^ n) - (y |^ n) = a } is finite

proof end;