consider nA being Nat, pA being INT -valued Polynomial of (n + nA),F_Real such that
A1:
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
A2:
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 A3:
rng qA c= (rng pA) \/ {(0. F_Real)}
and A4:
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 A3, 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 A5:
rng qB c= (rng pB) \/ {(0. F_Real)}
and A6:
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 A5, 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 *' qA) + (qB *' 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 A7:
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 )
then
y in A
by XBOOLE_0:def 4;
then consider xA being
n -element XFinSequence of
NAT ,
yA being
nA -element XFinSequence of
NAT such that A8:
(
y = xA &
eval (
pA,
(@ (xA ^ yA)))
= 0 )
by A1;
y in B
by A7, XBOOLE_0:def 4;
then consider xB being
n -element XFinSequence of
NAT ,
yB being
nB -element XFinSequence of
NAT such that A9:
(
y = xB &
eval (
pB,
(@ (xB ^ yB)))
= 0 )
by A2;
reconsider X =
@ ((xA ^ yA) ^ yB) as
Function of
(n + N),
F_Real ;
A10:
len (xA ^ yA) = n + nA
by CARD_1:def 7;
then
((xA ^ yA) ^ yB) | (n + nA) = xA ^ yA
by AFINSQ_1:57;
then A11:
eval (
qA,
X)
= 0
by A8, A4;
A12:
X = xA ^ (yA ^ yB)
by AFINSQ_1:27;
A13:
len xA = n
by CARD_1:def 7;
then A14:
(
(@ (@ (xA ^ yB))) | n = xA &
X | n = xA )
by A12, AFINSQ_1:57;
(
(@ X) /^ (n + nA) = yB &
(@ (@ (xA ^ yB))) /^ n = yB )
by A10, A13, AFINSQ_2:12;
then A15:
eval (
qB,
X)
= 0
by A8, A9, A14, A6;
reconsider Y =
@ (@ (yA ^ yB)) as
N -element XFinSequence of
NAT ;
A16:
eval (
(qA *' qA),
(@ (xA ^ Y))) =
(eval (qA,(@ (xA ^ Y)))) * (eval (qA,(@ (xA ^ Y))))
by POLYNOM2:25
.=
0 * 0
by A11, A12
;
A17:
eval (
(qB *' qB),
(@ (xA ^ Y))) =
(eval (qB,(@ (xA ^ Y)))) * (eval (qB,(@ (xA ^ Y))))
by POLYNOM2:25
.=
0 * 0
by A15, A12
;
eval (
Q,
(@ (xA ^ Y))) =
(eval ((qA *' qA),(@ (xA ^ Y)))) + (eval ((qB *' qB),(@ (xA ^ Y))))
by POLYNOM2:23
.=
0
by A16, A17
;
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 A8;
verum
end;
given xA being
n -element XFinSequence of
NAT ,
y1 being
N -element XFinSequence of
NAT such that A18:
(
xA = y &
eval (
Q,
(@ (xA ^ y1)))
= 0 )
;
y in A /\ B
reconsider yA =
y1 | nA,
yB =
y1 /^ nA as
XFinSequence of
NAT ;
A19:
(
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 A19, 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 ;
A21:
len (xA ^ yA) = n + nA
by CARD_1:def 7;
then
((xA ^ yA) ^ yB) | (n + nA) = xA ^ yA
by AFINSQ_1:57;
then A22:
eval (
pA,
(@ (xA ^ yA)))
= eval (
qA,
X)
by A4;
A23:
X = xA ^ (yA ^ yB)
by AFINSQ_1:27;
A24:
len xA = n
by CARD_1:def 7;
then A25:
(
(@ (@ (xA ^ yB))) | n = xA &
X | n = xA )
by A23, AFINSQ_1:57;
(
(@ X) /^ (n + nA) = yB &
(@ (@ (xA ^ yB))) /^ n = yB )
by A21, A24, AFINSQ_2:12;
then A26:
eval (
pB,
(@ (xA ^ yB)))
= eval (
qB,
X)
by A25, A6;
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;
reconsider eAA =
eA * eA,
eBB =
eB * eB as
Element of
NAT by INT_1:3, XREAL_1:63;
A27:
eval (
(qA *' qA),
(@ (xA ^ y1))) =
(eval (qA,(@ (xA ^ y1)))) * (eval (qA,(@ (xA ^ y1))))
by POLYNOM2:25
.=
eAA
;
A28:
eval (
(qB *' qB),
(@ (xA ^ y1))) =
(eval (qB,(@ (xA ^ y1)))) * (eval (qB,(@ (xA ^ y1))))
by POLYNOM2:25
.=
eBB
;
eval (
Q,
(@ (xA ^ y1))) =
(eval ((qA *' qA),(@ (xA ^ y1)))) + (eval ((qB *' qB),(@ (xA ^ y1))))
by POLYNOM2:23
.=
eAA + eBB
by A27, A28
;
then
(
eAA = 0 &
eBB = 0 )
by A18;
then A29:
(
eA = 0 &
eB = 0 )
by XCMPLX_1:6;
then A30:
xA in A
by A1, A22, A23;
xA in B
by A2, A29, A26, A23;
hence
y in A /\ B
by A18, A30, XBOOLE_0:def 4;
verum
end;
hence
for b1 being Subset of (n -xtuples_of NAT) st b1 = A /\ B holds
b1 is diophantine
; verum