consider nA being Nat, pA being INT -valued Polynomial of (n + nA),F_Real such that
A31:
for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being nA -element XFinSequence of NAT st
( s = x & eval (pA,(@ (x ^ y))) = 0 ) )
by Def6;
consider nB being Nat, pB being INT -valued Polynomial of (n + nB),F_Real such that
A32:
for s being object holds
( s in B iff ex x being n -element XFinSequence of NAT ex y being nB -element XFinSequence of NAT st
( s = x & eval (pB,(@ (x ^ y))) = 0 ) )
by Def6;
A \/ B is diophantine
proof
take N =
nA + nB;
HILB10_2:def 6 ex p being INT -valued Polynomial of (n + N),F_Real st
for s being object holds
( s in A \/ B iff ex x being n -element XFinSequence of NAT ex y being N -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) )
consider qA being
Polynomial of
((n + nA) + nB),
F_Real such that A33:
rng qA c= (rng pA) \/ {(0. F_Real)}
and A34:
for
x being
Function of
(n + nA),
F_Real for
y being
Function of
((n + nA) + nB),
F_Real st
y | (n + nA) = x holds
eval (
pA,
x)
= eval (
qA,
y)
by Th27;
rng qA c= INT
by A33, INT_1:def 2;
then reconsider qA =
qA as
INT -valued Polynomial of
(n + N),
F_Real by RELAT_1:def 19;
consider qB being
Polynomial of
((n + nA) + nB),
F_Real such that A35:
rng qB c= (rng pB) \/ {(0. F_Real)}
and A36:
for
XY being
Function of
(n + nB),
F_Real for
XanyY being
Function of
((n + nA) + nB),
F_Real st
XY | n = XanyY | n &
(@ XY) /^ n = (@ XanyY) /^ (n + nA) holds
eval (
pB,
XY)
= eval (
qB,
XanyY)
by Th28;
rng qB c= INT
by A35, INT_1:def 2;
then reconsider qB =
qB as
INT -valued Polynomial of
(n + N),
F_Real by RELAT_1:def 19;
take Q =
qA *' qB;
for s being object holds
( s in A \/ B iff ex x being n -element XFinSequence of NAT ex y being N -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) )
let y be
object ;
( y in A \/ B iff ex x being n -element XFinSequence of NAT ex y being N -element XFinSequence of NAT st
( y = x & eval (Q,(@ (x ^ y))) = 0 ) )
thus
(
y in A \/ B implies ex
x being
n -element XFinSequence of
NAT ex
y1 being
N -element XFinSequence of
NAT st
(
y = x &
eval (
Q,
(@ (x ^ y1)))
= 0 ) )
( ex x being n -element XFinSequence of NAT ex y being N -element XFinSequence of NAT st
( y = x & eval (Q,(@ (x ^ y))) = 0 ) implies y in A \/ B )proof
assume
y in A \/ B
;
ex x being n -element XFinSequence of NAT ex y1 being N -element XFinSequence of NAT st
( y = x & eval (Q,(@ (x ^ y1))) = 0 )
per cases then
( y in A or y in B )
by XBOOLE_0:def 3;
suppose
y in A
;
ex x being n -element XFinSequence of NAT ex y1 being N -element XFinSequence of NAT st
( y = x & eval (Q,(@ (x ^ y1))) = 0 )then consider xA being
n -element XFinSequence of
NAT ,
yA being
nA -element XFinSequence of
NAT such that A38:
(
y = xA &
eval (
pA,
(@ (xA ^ yA)))
= 0 )
by A31;
set yB = the
nB -element XFinSequence of
NAT ;
reconsider X =
@ ((xA ^ yA) ^ the nB -element XFinSequence of NAT ) as
Function of
(n + N),
F_Real ;
len (xA ^ yA) = n + nA
by CARD_1:def 7;
then
((xA ^ yA) ^ the nB -element XFinSequence of NAT ) | (n + nA) = xA ^ yA
by AFINSQ_1:57;
then A39:
eval (
qA,
X)
= 0
by A38, A34;
reconsider Y =
@ (@ (yA ^ the nB -element XFinSequence of NAT )) as
N -element XFinSequence of
NAT ;
eval (
Q,
(@ (xA ^ Y))) =
(eval (qA,(@ (xA ^ Y)))) * (eval (qB,(@ (xA ^ Y))))
by POLYNOM2:25
.=
0 * (eval (qB,(@ (xA ^ Y))))
by A39, AFINSQ_1:27
;
hence
ex
x being
n -element XFinSequence of
NAT ex
y1 being
N -element XFinSequence of
NAT st
(
y = x &
eval (
Q,
(@ (x ^ y1)))
= 0 )
by A38;
verum end; suppose
y in B
;
ex x being n -element XFinSequence of NAT ex y1 being N -element XFinSequence of NAT st
( y = x & eval (Q,(@ (x ^ y1))) = 0 )then consider xA being
n -element XFinSequence of
NAT ,
yB being
nB -element XFinSequence of
NAT such that A40:
(
y = xA &
eval (
pB,
(@ (xA ^ yB)))
= 0 )
by A32;
set yA = the
nA -element XFinSequence of
NAT ;
reconsider X =
@ ((xA ^ the nA -element XFinSequence of NAT ) ^ yB) as
Function of
(n + N),
F_Real ;
A41:
len (xA ^ the nA -element XFinSequence of NAT ) = n + nA
by CARD_1:def 7;
A42:
X = xA ^ ( the nA -element XFinSequence of NAT ^ yB)
by AFINSQ_1:27;
A43:
len xA = n
by CARD_1:def 7;
then A44:
(
(@ (@ (xA ^ yB))) | n = xA &
X | n = xA )
by A42, AFINSQ_1:57;
A45:
(
(@ X) /^ (n + nA) = yB &
(@ (@ (xA ^ yB))) /^ n = yB )
by A41, A43, AFINSQ_2:12;
reconsider Y =
@ (@ ( the nA -element XFinSequence of NAT ^ yB)) as
N -element XFinSequence of
NAT ;
eval (
Q,
(@ (xA ^ Y))) =
(eval (qA,(@ (xA ^ Y)))) * (eval (qB,(@ (xA ^ Y))))
by POLYNOM2:25
.=
(eval (qA,(@ (xA ^ Y)))) * 0
by A45, A40, A44, A36, A42
;
hence
ex
x being
n -element XFinSequence of
NAT ex
y1 being
N -element XFinSequence of
NAT st
(
y = x &
eval (
Q,
(@ (x ^ y1)))
= 0 )
by A40;
verum end;
end;
given xA being
n -element XFinSequence of
NAT ,
y1 being
N -element XFinSequence of
NAT such that A46:
(
xA = y &
eval (
Q,
(@ (xA ^ y1)))
= 0 )
;
y in A \/ B
reconsider yA =
y1 | nA,
yB =
y1 /^ nA as
XFinSequence of
NAT ;
A47:
(
nA <= nA + nB &
len y1 = nA + nB )
by NAT_1:11, CARD_1:def 7;
then
len yA = nA
by AFINSQ_1:54;
then reconsider yA =
yA as
nA -element XFinSequence of
NAT by CARD_1:def 7;
len yB =
(nA + nB) -' nA
by A47, AFINSQ_2:def 2
.=
nB
by NAT_D:34
;
then reconsider yB =
yB as
nB -element XFinSequence of
NAT by CARD_1:def 7;
reconsider X =
@ ((xA ^ yA) ^ yB) as
Function of
(n + N),
F_Real ;
A49:
len (xA ^ yA) = n + nA
by CARD_1:def 7;
then
((xA ^ yA) ^ yB) | (n + nA) = xA ^ yA
by AFINSQ_1:57;
then A50:
eval (
pA,
(@ (xA ^ yA)))
= eval (
qA,
X)
by A34;
A51:
X = xA ^ (yA ^ yB)
by AFINSQ_1:27;
A52:
len xA = n
by CARD_1:def 7;
then A53:
(
(@ (@ (xA ^ yB))) | n = xA &
X | n = xA )
by A51, AFINSQ_1:57;
(
(@ X) /^ (n + nA) = yB &
(@ (@ (xA ^ yB))) /^ n = yB )
by A49, A52, AFINSQ_2:12;
then A54:
eval (
pB,
(@ (xA ^ yB)))
= eval (
qB,
X)
by A53, A36;
reconsider eA =
eval (
qA,
(@ (xA ^ y1))) as
Integer by INT_1:def 2;
reconsider eB =
eval (
qB,
(@ (xA ^ y1))) as
Integer by INT_1:def 2;
eval (
Q,
(@ (xA ^ y1))) =
(eval (qA,(@ (xA ^ y1)))) * (eval (qB,(@ (xA ^ y1))))
by POLYNOM2:25
.=
eA * eB
;
then
(
eA = 0 or
eB = 0 )
by A46, XCMPLX_1:6;
then
(
xA in A or
xA in B )
by A31, A32, A54, A50, A51;
hence
y in A \/ B
by A46, XBOOLE_0:def 3;
verum
end;
hence
for b1 being Subset of (n -xtuples_of NAT) st b1 = A \/ B holds
b1 is diophantine
; verum