let n be Nat; :: thesis: for a, b being Integer

for c being Nat

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let a, b be Integer; :: thesis: for c being Nat

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let c be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

deffunc H_{1}( Nat, Nat, Nat) -> set = (c * $3) + (((a * c) * $1) * $3);

A1: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
_{1}[ Nat, Nat, Integer] means (b * $1) + 0 < $3;

A6: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:7;

A7: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{1}(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A6, A1);

defpred S_{2}[ Nat, Nat, Integer] means b * $1 >= $3 + 0;

A8: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : S_{2}[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:8;

deffunc H_{2}( Nat, Nat, Nat) -> set = ((a * c) * $1) * $3;

A9: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : H_{2}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:9;

A10: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : S_{2}[p . i1,p . i2,H_{2}(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A8, A9);

defpred S_{3}[ XFinSequence of NAT ] means S_{1}[$1 . i2,$1 . i2,H_{1}($1 . i1,$1 . i1,$1 . i3)];

defpred S_{4}[ XFinSequence of NAT ] means S_{2}[$1 . i2,$1 . i2,H_{2}($1 . i1,$1 . i1,$1 . i3)];

defpred S_{5}[ XFinSequence of NAT ] means ( S_{3}[$1] & S_{4}[$1] );

defpred S_{6}[ XFinSequence of NAT ] means c * ($1 . i3) <> (0 * ($1 . i3)) + 0;

defpred S_{7}[ XFinSequence of NAT ] means ( S_{5}[$1] & S_{6}[$1] );

defpred S_{8}[ XFinSequence of NAT ] means ( a * ($1 . i1) = [\((b * ($1 . i2)) / (c * ($1 . i3)))/] & c * ($1 . i3) <> 0 );

A11: { p where p is n -element XFinSequence of NAT : S_{3}[p] } is diophantine Subset of (n -xtuples_of NAT)
by A7;

A12: { p where p is n -element XFinSequence of NAT : S_{4}[p] } is diophantine Subset of (n -xtuples_of NAT)
by A10;

{ p where p is n -element XFinSequence of NAT : ( S_{3}[p] & S_{4}[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 3(A11, A12);

then A13: { p where p is n -element XFinSequence of NAT : S_{5}[p] } is diophantine Subset of (n -xtuples_of NAT)
;

A14: { p where p is n -element XFinSequence of NAT : S_{6}[p] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:16;

A15: { p where p is n -element XFinSequence of NAT : ( S_{5}[p] & S_{6}[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 3(A13, A14);

A16: for p being n -element XFinSequence of NAT holds

( S_{8}[p] iff S_{7}[p] )
_{8}[p] } = { q where q is n -element XFinSequence of NAT : S_{7}[q] }
from HILB10_3:sch 2(A16);

hence { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT) by A15; :: thesis: verum

for c being Nat

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let a, b be Integer; :: thesis: for c being Nat

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let c be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)

deffunc H

A1: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b

proof

defpred S
let n be Nat; :: thesis: for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is n -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)

let i1, i2, i3, i4 be Element of n; :: thesis: for d being Integer holds { p where p is n -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)

let d be Integer; :: thesis: { p where p is n -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)

defpred S_{1}[ Nat, Nat, Integer] means d * $1 = ((c * $2) + $3) + 0;

A2: for n being Nat

for i1, i2, i3 being Element of n

for f being Integer holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,f * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:11;

deffunc H_{2}( Nat, Nat, Nat) -> set = ((a * c) * $1) * $3;

A3: for n being Nat

for i1, i2, i3, i4 being Element of n

for f being Integer holds { p where p is b_{1} -element XFinSequence of NAT : H_{2}(p . i1,p . i2,p . i3) = f * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:9;

A4: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{2}(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A2, A3);

defpred S_{2}[ XFinSequence of NAT ] means H_{1}($1 . i1,$1 . i2,$1 . i3) = d * ($1 . i4);

defpred S_{3}[ XFinSequence of NAT ] means S_{1}[$1 . i4,$1 . i3,H_{2}($1 . i1,$1 . i2,$1 . i3)];

A5: for p being n -element XFinSequence of NAT holds

( S_{2}[p] iff S_{3}[p] )
;

{ p where p is n -element XFinSequence of NAT : S_{2}[p] } = { q where q is n -element XFinSequence of NAT : S_{3}[q] }
from HILB10_3:sch 2(A5);

hence { p where p is n -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by A4; :: thesis: verum

end;for d being Integer holds { p where p is n -element XFinSequence of NAT : H

let i1, i2, i3, i4 be Element of n; :: thesis: for d being Integer holds { p where p is n -element XFinSequence of NAT : H

let d be Integer; :: thesis: { p where p is n -element XFinSequence of NAT : H

defpred S

A2: for n being Nat

for i1, i2, i3 being Element of n

for f being Integer holds { p where p is b

deffunc H

A3: for n being Nat

for i1, i2, i3, i4 being Element of n

for f being Integer holds { p where p is b

A4: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

defpred S

defpred S

A5: for p being n -element XFinSequence of NAT holds

( S

{ p where p is n -element XFinSequence of NAT : S

hence { p where p is n -element XFinSequence of NAT : H

A6: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b

A7: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

defpred S

A8: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b

deffunc H

A9: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b

A10: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

defpred S

defpred S

defpred S

defpred S

defpred S

defpred S

A11: { p where p is n -element XFinSequence of NAT : S

A12: { p where p is n -element XFinSequence of NAT : S

{ p where p is n -element XFinSequence of NAT : ( S

then A13: { p where p is n -element XFinSequence of NAT : S

A14: { p where p is n -element XFinSequence of NAT : S

A15: { p where p is n -element XFinSequence of NAT : ( S

A16: for p being n -element XFinSequence of NAT holds

( S

proof

{ p where p is n -element XFinSequence of NAT : S
let p be n -element XFinSequence of NAT ; :: thesis: ( S_{8}[p] iff S_{7}[p] )

thus ( S_{8}[p] implies S_{7}[p] )
:: thesis: ( S_{7}[p] implies S_{8}[p] )_{7}[p]
; :: thesis: S_{8}[p]

then A21: (a * (p . i1)) * (c * (p . i3)) > (b * (p . i2)) - (c * (p . i3)) by XREAL_1:19;

((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75

.= 1 * (b * (p . i2)) by A20, XCMPLX_1:60 ;

then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;

then A22: a * (p . i1) > ((b * (p . i2)) / (c * (p . i3))) - 1 by A21, XREAL_1:64;

(a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by A20;

then a * (p . i1) <= (b * (p . i2)) / (c * (p . i3)) by A20, XREAL_1:77;

hence S_{8}[p]
by A20, A22, INT_1:def 6; :: thesis: verum

end;thus ( S

proof

assume A20:
S
assume A17:
S_{8}[p]
; :: thesis: S_{7}[p]

then A18: (a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by XREAL_1:83, INT_1:def 6;

((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75

.= 1 * (b * (p . i2)) by A17, XCMPLX_1:60 ;

then A19: (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;

((b * (p . i2)) / (c * (p . i3))) - 1 < a * (p . i1) by A17, INT_1:def 6;

then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) < (a * (p . i1)) * (c * (p . i3)) by A17, XREAL_1:68;

hence S_{7}[p]
by A18, A19, XREAL_1:19; :: thesis: verum

end;then A18: (a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by XREAL_1:83, INT_1:def 6;

((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75

.= 1 * (b * (p . i2)) by A17, XCMPLX_1:60 ;

then A19: (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;

((b * (p . i2)) / (c * (p . i3))) - 1 < a * (p . i1) by A17, INT_1:def 6;

then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) < (a * (p . i1)) * (c * (p . i3)) by A17, XREAL_1:68;

hence S

then A21: (a * (p . i1)) * (c * (p . i3)) > (b * (p . i2)) - (c * (p . i3)) by XREAL_1:19;

((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75

.= 1 * (b * (p . i2)) by A20, XCMPLX_1:60 ;

then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;

then A22: a * (p . i1) > ((b * (p . i2)) / (c * (p . i3))) - 1 by A21, XREAL_1:64;

(a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by A20;

then a * (p . i1) <= (b * (p . i2)) / (c * (p . i3)) by A20, XREAL_1:77;

hence S

hence { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT) by A15; :: thesis: verum