:: Formalization of the {MRDP } Theorem in the {M}izar System
:: by Karol P\kak
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

registration

let n be Nat;

cluster idseq n -> INT -valued ;

coherence
idseq n is INT -valued ;
let x be natural-valued n -element XFinSequence;
let p be INT -valued Polynomial of n,F_Real;

cluster eval (p,(@ x)) -> integer ;

coherence
eval (p,(@ x)) is integer

proof end;

end;

theorem Th1: :: HILB10_5:1

for n, k being Nat
for p being INT -valued Polynomial of n,F_Real
for x, y being b₁ -element XFinSequence of NAT st k <> 0 & ( for i being Nat st i in n holds
k divides (x . i) - (y . i) ) holds
k divides (eval (p,(@ x))) - (eval (p,(@ y)))

proof end;

registration

let f be INT -valued Function;

cluster - f -> INT -valued ;

coherence
- f is INT -valued ;

end;

scheme :: HILB10_5:sch 1
SCH1{ P₁[ object , object ], F₁() -> XFinSequence-yielding XFinSequence } :

{ ((F₁() . i) . j) where i, j is Nat : P₁[i,j] } is finite

proof end;

theorem Th2: :: HILB10_5:2

for n, m being Nat st m >= n & n > 0 holds
1 + ((m !) * (idseq n)) is CR_Sequence

proof end;

Lm1: for K, n being Nat ex Z being Nat st
( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) )

proof end;

theorem Th12: :: HILB10_5:3

for p being Prime
for f being FinSequence of NAT st f is positive-yielding & p divides Product f holds
ex i being Nat st
( i in dom f & p divides f . i )

proof end;

definition

let n be set ;
let p be Series of n,F_Real;

func |.p.| -> Series of n,F_Real means :Def1: :: HILB10_5:def 1
for b being bag of n holds it . b = |.(p . b).|;

existence
ex b₁ being Series of n,F_Real st
for b being bag of n holds b₁ . b = |.(p . b).|

proof end;

uniqueness
for b₁, b₂ being Series of n,F_Real st ( for b being bag of n holds b₁ . b = |.(p . b).| ) & ( for b being bag of n holds b₂ . b = |.(p . b).| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines |. HILB10_5:def 1 :
for n being set
for p, b₃ being Series of n,F_Real holds
( b₃ = |.p.| iff for b being bag of n holds b₃ . b = |.(p . b).| );

theorem Th3: :: HILB10_5:4

for n being set
for p being Series of n,F_Real holds Support p = Support |.p.|

proof end;

registration

let n be Ordinal;
let p be Polynomial of n,F_Real;

cluster |.p.| -> finite-Support ;

coherence
|.p.| is finite-Support

proof end;

end;

registration

let n be set ;
let S be non empty ZeroStr ;
let p be finite-Support Series of n,S;

cluster Support p -> finite ;

coherence
Support p is finite by POLYNOM1:def 5;

end;

definition

let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;

func sum_of_coefficients p -> Element of L equals :: HILB10_5:def 2
Sum (p * (SgmX ((BagOrder n),(Support p))));

coherence
Sum (p * (SgmX ((BagOrder n),(Support p)))) is Element of L ;

end;

:: deftheorem defines sum_of_coefficients HILB10_5:def 2 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds sum_of_coefficients p = Sum (p * (SgmX ((BagOrder n),(Support p))));

definition

let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;

func degree p -> Nat means :Def3: :: HILB10_5:def 3
( ex s being bag of n st
( s in Support p & it = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= it ) ) if p <> 0_ (n,L)
otherwise it = 0 ;

existence
( ( p <> 0_ (n,L) implies ex b₁ being Nat st
( ex s being bag of n st
( s in Support p & b₁ = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b₁ ) ) ) & ( not p <> 0_ (n,L) implies ex b₁ being Nat st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Nat holds
( ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & b₁ = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b₁ ) & ex s being bag of n st
( s in Support p & b₂ = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b₂ ) implies b₁ = b₂ ) & ( not p <> 0_ (n,L) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Nat holds verum ;

end;

:: deftheorem Def3 defines degree HILB10_5:def 3 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b₄ being Nat holds
( ( p <> 0_ (n,L) implies ( b₄ = degree p iff ( ex s being bag of n st
( s in Support p & b₄ = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b₄ ) ) ) ) & ( not p <> 0_ (n,L) implies ( b₄ = degree p iff b₄ = 0 ) ) );

theorem Th4: :: HILB10_5:5

for n being Ordinal
for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))

proof end;

theorem :: HILB10_5:6

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds
( degree p = 0 iff Support p c= {(EmptyBag n)} )

proof end;

theorem Th6: :: HILB10_5:7

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p holds
degree p >= degree b

proof end;

theorem Th7: :: HILB10_5:8

for n being Ordinal
for p being Polynomial of n,F_Real st |.p.| = 0_ (n,F_Real) holds
p = 0_ (n,F_Real)

proof end;

registration

let n be set ;

reduce |.(0_ (n,F_Real)).| to 0_ (n,F_Real);

reducibility
|.(0_ (n,F_Real)).| = 0_ (n,F_Real)

proof end;

end;

theorem :: HILB10_5:9

for n being Ordinal
for p being Polynomial of n,F_Real holds degree p = degree |.p.|

proof end;

theorem Th9: :: HILB10_5:10

for n being Ordinal
for b being bag of n
for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b)

proof end;

theorem Th10: :: HILB10_5:11

for n being Ordinal
for p being Polynomial of n,F_Real
for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))

proof end;

registration

let n be Ordinal;
let p be INT -valued Polynomial of n,F_Real;

cluster |.p.| -> natural-valued ;

coherence
|.p.| is natural-valued

proof end;

end;

registration

let n be Ordinal;

cluster Relation-like Bags n -defined the carrier of F_Real -valued non empty Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued finite-Support for Element of K16(K17((Bags n), the carrier of F_Real));

existence
ex b₁ being Polynomial of n,F_Real st b₁ is natural-valued

proof end;

end;

registration

let O be Ordinal;
let p be natural-valued Polynomial of O,F_Real;

cluster sum_of_coefficients p -> natural ;

coherence
sum_of_coefficients p is natural

proof end;

end;

:: as diophantine sets

scheme :: HILB10_5:sch 2
SubsetDioph{ F₁() -> Nat, P₁[ Nat, Nat, Nat, Nat], F₂() -> set } :

for i2, i3, i4 being Element of F₁() holds { p where p is F₁() -element XFinSequence of NAT : for i being Nat st i in F₂() holds
P₁[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F₁() -xtuples_of NAT)

provided

A1: for i1, i2, i3, i4 being Element of F₁() holds { p where p is F₁() -element XFinSequence of NAT : P₁[p . i1,p . i2,p . i3,p . i4] } is diophantine Subset of (F₁() -xtuples_of NAT) and
A2: F₂() c= Segm F₁()

proof end;

theorem Th11: :: HILB10_5:12

for k, n1, n2, i, j, l, m, n being Nat
for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds
{ p where p is b₈ -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th13: :: HILB10_5:13

for n, k being Nat
for P being INT -valued Polynomial of k,F_Real
for a being Integer
for perm being Permutation of n
for i1 being Element of n st k <= n holds
{ p where p is b₁ -element XFinSequence of NAT : for q being b₂ -element XFinSequence of NAT st q = (p * perm) | k holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th14: :: HILB10_5:14

for k being Nat
for P being INT -valued Polynomial of (k + 1),F_Real
for a being Integer
for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i2 holds
{ p where p is b₄ -element XFinSequence of NAT : for q being b₁ + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th15: :: HILB10_5:15

for k being Nat
for P being INT -valued Polynomial of (k + 1),F_Real
for n being Nat
for i1, i2 being Element of n st k + 1 <= n & k in i1 holds
{ p where p is b₃ -element XFinSequence of NAT : for q being b₁ + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds
eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th16: :: HILB10_5:16

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real
for X being b₁ -element XFinSequence of NAT
for x being Element of NAT holds
( ( for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) iff ex Y being b₂ -element XFinSequence of NAT ex Z, e, K being Element of NAT st
( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) & ( for i being Nat st i in k holds
Y . i > e ) & e > x & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

proof end;

theorem Th17: :: HILB10_5:17

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real
for X being b₁ -element XFinSequence of NAT
for x being Element of NAT holds
( ( for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ) iff ex Y being b₂ -element XFinSequence of NAT ex Z, K being Element of NAT st
( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) & ( for i being Nat st i in k holds
Y . i > x + 1 ) & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds
Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

proof end;

theorem :: HILB10_5:18

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b₁ -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th19: :: HILB10_5:19

for n, k being Nat
for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b₁ -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being b₂ -element XFinSequence of NAT st
( ( for i being Nat st i in k holds
y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

:: Davis Normal Form

definition

let n be Nat;
let A be Subset of (n -xtuples_of NAT);

attr A is recursively_enumerable means :: HILB10_5:def 4
ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st
for X being n -element XFinSequence of NAT holds
( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being b₁ -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) );

end;

:: deftheorem defines recursively_enumerable HILB10_5:def 4 :
for n being Nat
for A being Subset of (n -xtuples_of NAT) holds
( A is recursively_enumerable iff ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st
for X being b₁ -element XFinSequence of NAT holds
( X in A iff ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being b₃ -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) );

theorem :: HILB10_5:20

for n being Nat
for A being Subset of (n -xtuples_of NAT) st A is diophantine holds
A is recursively_enumerable

proof end;

:: Yuri Matiyasevich, Julia Robinson, Martin Davis, Hilary Putnam Theorem

theorem :: HILB10_5:21

for n being Nat
for A being Subset of (n -xtuples_of NAT) st A is recursively_enumerable holds
A is diophantine

proof end;