:: by Karol P\kak

::

:: Received May 27, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

registration

let n be Nat;

coherence

idseq n is INT -valued ;

let x be natural-valued n -element XFinSequence;

let p be INT -valued Polynomial of n,F_Real;

coherence

eval (p,(@ x)) is integer

end;
coherence

idseq n is INT -valued ;

let x be natural-valued n -element XFinSequence;

let p be INT -valued Polynomial of n,F_Real;

coherence

eval (p,(@ x)) is integer

proof end;

theorem Th1: :: HILB10_5:1

for n, k being Nat

for p being INT -valued Polynomial of n,F_Real

for x, y being b_{1} -element XFinSequence of NAT st k <> 0 & ( for i being Nat st i in n holds

k divides (x . i) - (y . i) ) holds

k divides (eval (p,(@ x))) - (eval (p,(@ y)))

for p being INT -valued Polynomial of n,F_Real

for x, y being b

k divides (x . i) - (y . i) ) holds

k divides (eval (p,(@ x))) - (eval (p,(@ y)))

proof end;

registration
end;

scheme :: HILB10_5:sch 1

SCH1{ P_{1}[ object , object ], F_{1}() -> XFinSequence-yielding XFinSequence } :

SCH1{ P

proof end;

Lm1: for K, n being Nat ex Z being Nat st

( Product (1 + (K * (idseq n))) = 1 + (K * Z) & ( n > 0 implies Z > 0 ) )

proof end;

theorem Th12: :: HILB10_5:3

for p being Prime

for f being FinSequence of NAT st f is positive-yielding & p divides Product f holds

ex i being Nat st

( i in dom f & p divides f . i )

for f being FinSequence of NAT st f is positive-yielding & p divides Product f holds

ex i being Nat st

( i in dom f & p divides f . i )

proof end;

definition

let n be set ;

let p be Series of n,F_Real;

ex b_{1} being Series of n,F_Real st

for b being bag of n holds b_{1} . b = |.(p . b).|

for b_{1}, b_{2} being Series of n,F_Real st ( for b being bag of n holds b_{1} . b = |.(p . b).| ) & ( for b being bag of n holds b_{2} . b = |.(p . b).| ) holds

b_{1} = b_{2}

end;
let p be Series of n,F_Real;

func |.p.| -> Series of n,F_Real means :Def1: :: HILB10_5:def 1

for b being bag of n holds it . b = |.(p . b).|;

existence for b being bag of n holds it . b = |.(p . b).|;

ex b

for b being bag of n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines |. HILB10_5:def 1 :

for n being set

for p, b_{3} being Series of n,F_Real holds

( b_{3} = |.p.| iff for b being bag of n holds b_{3} . b = |.(p . b).| );

for n being set

for p, b

( b

registration
end;

registration

let n be set ;

let S be non empty ZeroStr ;

let p be finite-Support Series of n,S;

coherence

Support p is finite by POLYNOM1:def 5;

end;
let S be non empty ZeroStr ;

let p be finite-Support Series of n,S;

coherence

Support p is finite by POLYNOM1:def 5;

definition

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

Sum (p * (SgmX ((BagOrder n),(Support p)))) is Element of L ;

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

func sum_of_coefficients p -> Element of L equals :: HILB10_5:def 2

Sum (p * (SgmX ((BagOrder n),(Support p))));

coherence Sum (p * (SgmX ((BagOrder n),(Support p))));

Sum (p * (SgmX ((BagOrder n),(Support p)))) is Element of L ;

:: deftheorem defines sum_of_coefficients HILB10_5:def 2 :

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds sum_of_coefficients p = Sum (p * (SgmX ((BagOrder n),(Support p))));

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds sum_of_coefficients p = Sum (p * (SgmX ((BagOrder n),(Support p))));

definition

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

( ( p <> 0_ (n,L) implies ex b_{1} being Nat st

( ex s being bag of n st

( s in Support p & b_{1} = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= b_{1} ) ) ) & ( not p <> 0_ (n,L) implies ex b_{1} being Nat st b_{1} = 0 ) )

for b_{1}, b_{2} being Nat holds

( ( p <> 0_ (n,L) & ex s being bag of n st

( s in Support p & b_{1} = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= b_{1} ) & ex s being bag of n st

( s in Support p & b_{2} = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= b_{2} ) implies b_{1} = b_{2} ) & ( not p <> 0_ (n,L) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Nat holds verum
;

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p be Polynomial of n,L;

func degree p -> Nat means :Def3: :: HILB10_5:def 3

( ex s being bag of n st

( s in Support p & it = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= it ) ) if p <> 0_ (n,L)

otherwise it = 0 ;

existence ( ex s being bag of n st

( s in Support p & it = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= it ) ) if p <> 0_ (n,L)

otherwise it = 0 ;

( ( p <> 0_ (n,L) implies ex b

( ex s being bag of n st

( s in Support p & b

degree s1 <= b

proof end;

uniqueness for b

( ( p <> 0_ (n,L) & ex s being bag of n st

( s in Support p & b

degree s1 <= b

( s in Support p & b

degree s1 <= b

proof end;

consistency for b

:: deftheorem Def3 defines degree HILB10_5:def 3 :

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b_{4} being Nat holds

( ( p <> 0_ (n,L) implies ( b_{4} = degree p iff ( ex s being bag of n st

( s in Support p & b_{4} = degree s ) & ( for s1 being bag of n st s1 in Support p holds

degree s1 <= b_{4} ) ) ) ) & ( not p <> 0_ (n,L) implies ( b_{4} = degree p iff b_{4} = 0 ) ) );

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b

( ( p <> 0_ (n,L) implies ( b

( s in Support p & b

degree s1 <= b

theorem Th4: :: HILB10_5:5

for n being Ordinal

for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))

for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))

proof end;

theorem :: HILB10_5:6

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( degree p = 0 iff Support p c= {(EmptyBag n)} )

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L holds

( degree p = 0 iff Support p c= {(EmptyBag n)} )

proof end;

theorem Th6: :: HILB10_5:7

for n being Ordinal

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for b being bag of n st b in Support p holds

degree p >= degree b

proof end;

theorem Th7: :: HILB10_5:8

for n being Ordinal

for p being Polynomial of n,F_Real st |.p.| = 0_ (n,F_Real) holds

p = 0_ (n,F_Real)

for p being Polynomial of n,F_Real st |.p.| = 0_ (n,F_Real) holds

p = 0_ (n,F_Real)

proof end;

theorem Th9: :: HILB10_5:10

for n being Ordinal

for b being bag of n

for r being Real st r >= 1 holds

for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds

|.(x . i).| <= r ) holds

|.(eval (b,x)).| <= r |^ (degree b)

for b being bag of n

for r being Real st r >= 1 holds

for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds

|.(x . i).| <= r ) holds

|.(eval (b,x)).| <= r |^ (degree b)

proof end;

theorem Th10: :: HILB10_5:11

for n being Ordinal

for p being Polynomial of n,F_Real

for r being Real st r >= 1 holds

for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds

|.(x . i).| <= r ) holds

|.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))

for p being Polynomial of n,F_Real

for r being Real st r >= 1 holds

for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds

|.(x . i).| <= r ) holds

|.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))

proof end;

registration

let n be Ordinal;

let p be INT -valued Polynomial of n,F_Real;

coherence

|.p.| is natural-valued

end;
let p be INT -valued Polynomial of n,F_Real;

coherence

|.p.| is natural-valued

proof end;

registration

let n be Ordinal;

ex b_{1} being Polynomial of n,F_Real st b_{1} is natural-valued

end;
cluster Relation-like Bags n -defined the carrier of F_Real -valued non empty Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued finite-Support for Element of K16(K17((Bags n), the carrier of F_Real));

existence ex b

proof end;

registration

let O be Ordinal;

let p be natural-valued Polynomial of O,F_Real;

coherence

sum_of_coefficients p is natural

end;
let p be natural-valued Polynomial of O,F_Real;

coherence

sum_of_coefficients p is natural

proof end;

:: as diophantine sets

scheme :: HILB10_5:sch 2

SubsetDioph{ F_{1}() -> Nat, P_{1}[ Nat, Nat, Nat, Nat], F_{2}() -> set } :

SubsetDioph{ F

for i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : for i being Nat st i in F_{2}() holds

P_{1}[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

providedP

A1:
for i1, i2, i3, i4 being Element of F_{1}() holds { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p . i1,p . i2,p . i3,p . i4] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
and

A2: F_{2}() c= Segm F_{1}()

A2: F

proof end;

theorem Th11: :: HILB10_5:12

for k, n1, n2, i, j, l, m, n being Nat

for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds

{ p where p is b_{8} -element XFinSequence of NAT : p . i1 >= k * ((((((p . i2) ^2) + 1) * (Product (1 + ((p /^ n1) | n2)))) * ((l * (p . i3)) + m)) |^ ((i * (p . i4)) + j)) } is diophantine Subset of (n -xtuples_of NAT)

for i1, i2, i3, i4 being Element of n st n1 + n2 <= n holds

{ p where p is b

proof end;

theorem Th13: :: HILB10_5:13

for n, k being Nat

for P being INT -valued Polynomial of k,F_Real

for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is b_{1} -element XFinSequence of NAT : for q being b_{2} -element XFinSequence of NAT st q = (p * perm) | k holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

for P being INT -valued Polynomial of k,F_Real

for a being Integer

for perm being Permutation of n

for i1 being Element of n st k <= n holds

{ p where p is b

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th14: :: HILB10_5:14

for k being Nat

for P being INT -valued Polynomial of (k + 1),F_Real

for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b_{4} -element XFinSequence of NAT : for q being b_{1} + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

for P being INT -valued Polynomial of (k + 1),F_Real

for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th15: :: HILB10_5:15

for k being Nat

for P being INT -valued Polynomial of (k + 1),F_Real

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b_{3} -element XFinSequence of NAT : for q being b_{1} + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

for P being INT -valued Polynomial of (k + 1),F_Real

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem Th16: :: HILB10_5:16

for n, k being Nat

for p being INT -valued Polynomial of ((2 + n) + k),F_Real

for X being b_{1} -element XFinSequence of NAT

for x being Element of NAT holds

( ( for z being Element of NAT st z <= x holds

ex y being b_{2} -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) iff ex Y being b_{2} -element XFinSequence of NAT ex Z, e, K being Element of NAT st

( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) & ( for i being Nat st i in k holds

Y . i > e ) & e > x & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds

Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

for p being INT -valued Polynomial of ((2 + n) + k),F_Real

for X being b

for x being Element of NAT holds

( ( for z being Element of NAT st z <= x holds

ex y being b

( K > x & K >= (sum_of_coefficients |.p.|) * (((((x ^2) + 1) * (Product (1 + X))) * e) |^ (degree p)) & ( for i being Nat st i in k holds

Y . i > e ) & e > x & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds

Product (((Y . i) + 1) + (- (idseq e))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

proof end;

theorem Th17: :: HILB10_5:17

for n, k being Nat

for p being INT -valued Polynomial of ((2 + n) + k),F_Real

for X being b_{1} -element XFinSequence of NAT

for x being Element of NAT holds

( ( for z being Element of NAT st z <= x holds

ex y being b_{2} -element XFinSequence of NAT st

( ( for i being Nat st i in k holds

y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ) iff ex Y being b_{2} -element XFinSequence of NAT ex Z, K being Element of NAT st

( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) & ( for i being Nat st i in k holds

Y . i > x + 1 ) & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds

Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

for p being INT -valued Polynomial of ((2 + n) + k),F_Real

for X being b

for x being Element of NAT holds

( ( for z being Element of NAT st z <= x holds

ex y being b

( ( for i being Nat st i in k holds

y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) ) iff ex Y being b

( K > x & K >= (sum_of_coefficients |.p.|) * ((((x ^2) + 1) * (Product (1 + X))) |^ (degree p)) & ( for i being Nat st i in k holds

Y . i > x + 1 ) & 1 + ((Z + 1) * (K !)) = Product (1 + ((K !) * (idseq (x + 1)))) & eval (p,(@ ((<%Z,x%> ^ X) ^ Y))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) & ( for i being Nat st i in k holds

Product (((Y . i) + 1) + (- (idseq (x + 1)))), 0 are_congruent_mod 1 + ((Z + 1) * (K !)) ) ) )

proof end;

theorem :: HILB10_5:18

for n, k being Nat

for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b_{1} -element XFinSequence of NAT : ex x being Element of NAT st

for z being Element of NAT st z <= x holds

ex y being b_{2} -element XFinSequence of NAT st eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 } is diophantine Subset of (n -xtuples_of NAT)

for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b

for z being Element of NAT st z <= x holds

ex y being b

proof end;

theorem Th19: :: HILB10_5:19

for n, k being Nat

for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b_{1} -element XFinSequence of NAT : ex x being Element of NAT st

for z being Element of NAT st z <= x holds

ex y being b_{2} -element XFinSequence of NAT st

( ( for i being Nat st i in k holds

y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } is diophantine Subset of (n -xtuples_of NAT)

for p being INT -valued Polynomial of ((2 + n) + k),F_Real holds { X where X is b

for z being Element of NAT st z <= x holds

ex y being b

( ( for i being Nat st i in k holds

y . i <= x ) & eval (p,(@ ((<%z,x%> ^ X) ^ y))) = 0 ) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

definition

let n be Nat;

let A be Subset of (n -xtuples_of NAT);

end;
let A be Subset of (n -xtuples_of NAT);

attr A is recursively_enumerable means :: HILB10_5:def 4

ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st

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 b_{1} -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 ) );

ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st

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 b

( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) );

:: deftheorem defines recursively_enumerable HILB10_5:def 4 :

for n being Nat

for A being Subset of (n -xtuples_of NAT) holds

( A is recursively_enumerable iff ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st

for X being b_{1} -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 b_{3} -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 ) ) );

for n being Nat

for A being Subset of (n -xtuples_of NAT) holds

( A is recursively_enumerable iff ex m being Nat ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st

for X being b

( X in A iff ex x being Element of NAT st

for z being Element of NAT st z <= x holds

ex Y being b

( ( for i being object st i in dom Y holds

Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) );

theorem :: HILB10_5:20

for n being Nat

for A being Subset of (n -xtuples_of NAT) st A is diophantine holds

A is recursively_enumerable

for A being Subset of (n -xtuples_of NAT) st A is diophantine holds

A is recursively_enumerable

proof end;

theorem :: HILB10_5:21

for n being Nat

for A being Subset of (n -xtuples_of NAT) st A is recursively_enumerable holds

A is diophantine

for A being Subset of (n -xtuples_of NAT) st A is recursively_enumerable holds

A is diophantine

proof end;