let n be Nat; for a, b being Integer
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let a, b be Integer; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
set F = F_Real ;
reconsider ar = a, br = b as integer Element of F_Real by XREAL_0:def 1;
set D = { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } ;
{ p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } c= n -xtuples_of NAT
then reconsider D = { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } as Subset of (n -xtuples_of NAT) ;
per cases
( n = 0 or n <> 0 )
;
suppose A1:
n <> 0
;
{ p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)set Q =
(ar * (1_1 (i1,F_Real))) - (br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real))));
reconsider Q =
(ar * (1_1 (i1,F_Real))) - (br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real)))) as
INT -valued Polynomial of
(n + 0),
F_Real ;
for
s being
object holds
(
s in D iff ex
x being
n -element XFinSequence of
NAT ex
y being
0 -element XFinSequence of
NAT st
(
s = x &
eval (
Q,
(@ (x ^ y)))
= 0 ) )
proof
let s be
object ;
( s in D iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) )
thus
(
s in D implies ex
x being
n -element XFinSequence of
NAT ex
y being
0 -element XFinSequence of
NAT st
(
s = x &
eval (
Q,
(@ (x ^ y)))
= 0 ) )
( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) implies s in D )proof
assume
s in D
;
ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 )
then consider p being
n -element XFinSequence of
NAT such that A2:
(
s = p &
a * (p . i1) = (b * (p . i2)) * (p . i3) )
;
reconsider Z =
<%> NAT as
0 -element XFinSequence of
NAT ;
take
p
;
ex y being 0 -element XFinSequence of NAT st
( s = p & eval (Q,(@ (p ^ y))) = 0 )
take
Z
;
( s = p & eval (Q,(@ (p ^ Z))) = 0 )
set pZ =
p ^ Z;
A3:
(
eval (
(1_1 (i1,F_Real)),
(@ p))
= p . i1 &
eval (
(1_1 (i2,F_Real)),
(@ p))
= p . i2 &
eval (
(1_1 (i3,F_Real)),
(@ p))
= p . i3 )
by A1, Th1;
A4:
eval (
(ar * (1_1 (i1,F_Real))),
(@ p)) =
ar * (eval ((1_1 (i1,F_Real)),(@ p)))
by POLYNOM7:29
.=
a * (p . i1)
by A1, Th1
;
A5:
eval (
(br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real)))),
(@ p)) =
br * (eval (((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real))),(@ p)))
by POLYNOM7:29
.=
br * ((eval ((1_1 (i2,F_Real)),(@ p))) * (eval ((1_1 (i3,F_Real)),(@ p))))
by POLYNOM2:25
.=
b * ((p . i2) * (p . i3))
by A3
;
eval (
Q,
(@ (p ^ Z))) =
(eval ((ar * (1_1 (i1,F_Real))),(@ p))) - (eval ((br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real)))),(@ p)))
by POLYNOM2:24
.=
0
by A2, A4, A5
;
hence
(
s = p &
eval (
Q,
(@ (p ^ Z)))
= 0 )
by A2;
verum
end;
given p being
n -element XFinSequence of
NAT ,
Z being
0 -element XFinSequence of
NAT such that A6:
(
s = p &
eval (
Q,
(@ (p ^ Z)))
= 0 )
;
s in D
A7:
(
eval (
(1_1 (i1,F_Real)),
(@ p))
= p . i1 &
eval (
(1_1 (i2,F_Real)),
(@ p))
= p . i2 &
eval (
(1_1 (i3,F_Real)),
(@ p))
= p . i3 )
by A1, Th1;
A8:
eval (
(br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real)))),
(@ p)) =
br * (eval (((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real))),(@ p)))
by POLYNOM7:29
.=
br * ((eval ((1_1 (i2,F_Real)),(@ p))) * (eval ((1_1 (i3,F_Real)),(@ p))))
by POLYNOM2:25
.=
b * ((p . i2) * (p . i3))
by A7
;
A9:
eval (
(ar * (1_1 (i1,F_Real))),
(@ p)) =
ar * (eval ((1_1 (i1,F_Real)),(@ p)))
by POLYNOM7:29
.=
a * (p . i1)
by A1, Th1
;
set P =
p ^ Z;
eval (
Q,
(@ (p ^ Z))) =
(eval ((ar * (1_1 (i1,F_Real))),(@ p))) - (eval ((br * ((1_1 (i2,F_Real)) *' (1_1 (i3,F_Real)))),(@ p)))
by POLYNOM2:24
.=
(a * (p . i1)) - (b * ((p . i2) * (p . i3)))
by A8, A9
;
then
a * (p . i1) = (b * (p . i2)) * (p . i3)
by A6;
hence
s in D
by A6;
verum
end; then
D is
diophantine
;
hence
{ p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is
diophantine Subset of
(n -xtuples_of NAT)
;
verum end; end;