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

registration
let n be Nat;
coherence ;
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 b1 -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;
coherence
- f is INT -valued
;
end;

scheme :: HILB10_5:sch 1
SCH1{ P1[ object , object ], F1() -> XFinSequence-yielding XFinSequence } :
{ ((F1() . i) . j) where i, j is Nat : P1[i,j] } is finite
proof end;

theorem Th2: :: HILB10_5:2
for n, m being Nat st m >= n & n > 0 holds
1 + ((m !) * ()) is CR_Sequence
proof end;

Lm1: for K, n being Nat ex Z being Nat st
( Product (1 + (K * ())) = 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 b1 being Series of n,F_Real st
for b being bag of n holds b1 . b = |.(p . b).|
proof end;
uniqueness
for b1, b2 being Series of n,F_Real st ( for b being bag of n holds b1 . b = |.(p . b).| ) & ( for b being bag of n holds b2 . b = |.(p . b).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines |. HILB10_5:def 1 :
for n being set
for p, b3 being Series of n,F_Real holds
( b3 = |.p.| iff for b being bag of n holds b3 . 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;
coherence
proof end;
end;

registration
let n be set ;
let S be non empty ZeroStr ;
let p be finite-Support Series of n,S;
coherence by POLYNOM1:def 5;
end;

definition
let n be Ordinal;
let p be Polynomial of n,L;
func sum_of_coefficients p -> Element of L equals :: HILB10_5:def 2
Sum (p * (SgmX ((),())));
coherence
Sum (p * (SgmX ((),()))) is Element of L
;
end;

:: deftheorem defines sum_of_coefficients HILB10_5:def 2 :
for n being Ordinal
for p being Polynomial of n,L holds sum_of_coefficients p = Sum (p * (SgmX ((),())));

definition
let n be Ordinal;
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 b1 being Nat st
( ex s being bag of n st
( s in Support p & b1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b1 ) ) ) & ( not p <> 0_ (n,L) implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( p <> 0_ (n,L) & ex s being bag of n st
( s in Support p & b1 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b1 ) & ex s being bag of n st
( s in Support p & b2 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b2 ) implies b1 = b2 ) & ( not p <> 0_ (n,L) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum
;
end;

:: deftheorem Def3 defines degree HILB10_5:def 3 :
for n being Ordinal
for p being Polynomial of n,L
for b4 being Nat holds
( ( p <> 0_ (n,L) implies ( b4 = degree p iff ( ex s being bag of n st
( s in Support p & b4 = degree s ) & ( for s1 being bag of n st s1 in Support p holds
degree s1 <= b4 ) ) ) ) & ( not p <> 0_ (n,L) implies ( b4 = degree p iff b4 = 0 ) ) );

theorem Th4: :: HILB10_5:5
for n being Ordinal
for b being bag of n holds degree b = Sum (b * (SgmX ((),())))
proof end;

theorem :: HILB10_5:6
for n being Ordinal
for p being Polynomial of n,L holds
( degree p = 0 iff Support p c= {()} )
proof end;

theorem Th6: :: HILB10_5:7
for n being Ordinal
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 |^ ()
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)).| <= * (r |^ ())
proof end;

registration
let n be Ordinal;
let p be INT -valued Polynomial of n,F_Real;
coherence
proof end;
end;

registration
let n be Ordinal;
existence
ex b1 being Polynomial of n,F_Real st b1 is natural-valued
proof end;
end;

registration
let O be Ordinal;
let p be natural-valued Polynomial of O,F_Real;
coherence
proof end;
end;

:: as diophantine sets
scheme :: HILB10_5:sch 2
SubsetDioph{ F1() -> Nat, P1[ Nat, Nat, Nat, Nat], F2() -> set } :
for i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : for i being Nat st i in F2() holds
P1[p . i,p . i2,p . i3,p . i4]
}
is diophantine Subset of (F1() -xtuples_of NAT)
provided
A1: for i1, i2, i3, i4 being Element of F1() holds { p where p is F1() -element XFinSequence of NAT : P1[p . i1,p . i2,p . i3,p . i4] } is diophantine Subset of (F1() -xtuples_of NAT) and
A2: F2() c= Segm F1()
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 b8 -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 ()
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 b1 -element XFinSequence of NAT : for q being b2 -element XFinSequence of NAT st q = (p * perm) | k holds
a * (p . i1) = eval (P,(@ q))
}
is diophantine Subset of ()
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 b4 -element XFinSequence of NAT : for q being b1 + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q))
}
is diophantine Subset of ()
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 b3 -element XFinSequence of NAT : for q being b1 + 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 ()
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 b1 -element XFinSequence of NAT
for x being Element of NAT holds
( ( for z being Element of NAT st z <= x holds
ex y being b2 -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) iff ex Y being b2 -element XFinSequence of NAT ex Z, e, K being Element of NAT st
( K > x & K >= * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ ()) & ( 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) + (- ())), 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 b1 -element XFinSequence of NAT
for x being Element of NAT holds
( ( for z being Element of NAT st z <= x holds
ex y being b2 -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 b2 -element XFinSequence of NAT ex Z, K being Element of NAT st
( K > x & K >= * ((((x ^2) + 1) * (Product (1 + X))) |^ ()) & ( 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 b1 -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being b2 -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0
}
is diophantine Subset of ()
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 b1 -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex y being b2 -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 ()
proof end;

:: Davis Normal Form
definition
let n be Nat;
let A be Subset of ();
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 b1 -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 () 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 b1 -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 b3 -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 () 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 () st A is recursively_enumerable holds
A is diophantine
proof end;