let n be Nat; for A being Subset of (n -xtuples_of NAT) st A is recursively_enumerable holds
A is diophantine
let A be Subset of (n -xtuples_of NAT); ( A is recursively_enumerable implies A is diophantine )
assume
A is recursively_enumerable
; A is diophantine
then consider m being Nat, P being INT -valued Polynomial of ((2 + n) + m),F_Real such that
A1:
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 m -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 ) )
;
set X = { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } ;
A2:
A c= { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in A or a in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } )
assume A3:
a in A
;
a in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }
reconsider a =
a as
n -element XFinSequence of
NAT by A3, HILB10_2:def 5;
consider x being
Element of
NAT such that A4:
for
z being
Element of
NAT st
z <= x holds
ex
Y being
m -element XFinSequence of
NAT st
( ( for
i being
object st
i in dom Y holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ a) ^ Y)))
= 0 )
by A3, A1;
now for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )let z be
Element of
NAT ;
( z <= x implies ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) )assume A5:
z <= x
;
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )consider Y being
m -element XFinSequence of
NAT such that A6:
( ( for
i being
object st
i in dom Y holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ a) ^ Y)))
= 0 )
by A4, A5;
take Y =
Y;
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )
len Y = m
by CARD_1:def 7;
hence
( ( for
i being
Nat st
i in m holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ a) ^ Y)))
= 0 )
by A6;
verum end;
hence
a in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }
;
verum
end;
{ X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } c= A
proof
let b be
object ;
TARSKI:def 3 ( not b in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } or b in A )
assume A7:
b in { X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) }
;
b in A
consider X being
n -element XFinSequence of
NAT such that A8:
(
b = X & ex
x being
Element of
NAT st
for
z being
Element of
NAT st
z <= x holds
ex
Y being
m -element XFinSequence of
NAT st
( ( for
i being
Nat st
i in m holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ X) ^ Y)))
= 0 ) )
by A7;
consider x being
Element of
NAT such that A9:
for
z being
Element of
NAT st
z <= x holds
ex
Y being
m -element XFinSequence of
NAT st
( ( for
i being
Nat st
i in m holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ X) ^ Y)))
= 0 )
by A8;
now for z being Element of NAT st z <= x holds
ex Y being m -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 )let z be
Element of
NAT ;
( z <= x implies ex Y being m -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 ) )assume A10:
z <= x
;
ex Y being m -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 )consider Y being
m -element XFinSequence of
NAT such that A11:
( ( for
i being
Nat st
i in m holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ X) ^ Y)))
= 0 )
by A9, A10;
take Y =
Y;
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
m = len Y
by CARD_1:def 7;
hence
( ( for
i being
object st
i in dom Y holds
Y . i <= x ) &
eval (
P,
(@ ((<%z,x%> ^ X) ^ Y)))
= 0 )
by A11;
verum end;
hence
b in A
by A1, A8;
verum
end;
then
{ X where X is n -element XFinSequence of NAT : ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } = A
by A2, XBOOLE_0:def 10;
hence
A is diophantine
by Th19; verum