:: by Marcin Acewicz and Karol P\kak

::

:: Received June 29, 2018

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

registration

let X be set ;

let p be INT -valued Series of X,F_Real;

let a be integer Element of F_Real;

coherence

a * p is INT -valued

end;
let p be INT -valued Series of X,F_Real;

let a be integer Element of F_Real;

coherence

a * p is INT -valued

proof end;

theorem Th1: :: HILB10_3:1

for O being non empty Ordinal

for i being Element of O

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

for i being Element of O

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of O,L holds eval ((1_1 (i,L)),x) = x . i

proof end;

theorem Th4: :: HILB10_3:4

for n, k being Nat

for i1 being Element of n

for p being b_{1} + b_{2} -element XFinSequence st n <> 0 & k <> 0 holds

(p | n) . i1 = p . i1

for i1 being Element of n

for p being b

(p | n) . i1 = p . i1

proof end;

theorem Th5: :: HILB10_3:5

for n being Nat

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

for k being Nat st k <= n holds

{ (p | k) where p is b_{1} -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)

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

for k being Nat st k <= n holds

{ (p | k) where p is b

proof end;

theorem Th6: :: HILB10_3:6

for n being Nat

for a, b, c being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th7: :: HILB10_3:7

for n being Nat

for a, b, c being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

scheme :: HILB10_3:sch 1

UnionDiophantine{ F_{1}() -> Nat, P_{1}[ XFinSequence of NAT ], P_{2}[ XFinSequence of NAT ] } :

UnionDiophantine{ F

{ p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } is diophantine Subset of (F_{1}() -xtuples_of NAT)

provided
A1:
{ p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
and

A2: { p where p is F_{1}() -element XFinSequence of NAT : P_{2}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

A2: { p where p is F

proof end;

scheme :: HILB10_3:sch 2

Eq{ F_{1}() -> Nat, P_{1}[ object ], P_{2}[ object ] } :

Eq{ F

{ p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } = { q where q is F_{1}() -element XFinSequence of NAT : P_{2}[q] }

provided
proof end;

theorem Th8: :: HILB10_3:8

for n being Nat

for a, b, c being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th9: :: HILB10_3:9

for n being Nat

for a, b being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

for a, b being Integer

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

proof end;

theorem Th10: :: HILB10_3:10

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

scheme :: HILB10_3:sch 3

IntersectionDiophantine{ F_{1}() -> Nat, P_{1}[ XFinSequence], P_{2}[ XFinSequence] } :

IntersectionDiophantine{ F

{ p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] & P_{2}[p] ) } is diophantine Subset of (F_{1}() -xtuples_of NAT)

provided
A1:
{ p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)
and

A2: { p where p is F_{1}() -element XFinSequence of NAT : P_{2}[p] } is diophantine Subset of (F_{1}() -xtuples_of NAT)

A2: { p where p is F

proof end;

scheme :: HILB10_3:sch 4

Substitution{ P_{1}[ Nat, Nat, natural object , Nat, Nat, Nat], F_{1}( Nat, Nat, Nat) -> natural object } :

Substitution{ P

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 : P_{1}[p . i1,p . i2,F_{1}((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)

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

A1:
for n being Nat

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

A2: for n being Nat

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

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

A2: for n being Nat

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

proof end;

scheme :: HILB10_3:sch 5

SubstitutionInt{ P_{1}[ Nat, Nat, Integer], F_{1}( Nat, Nat, Nat) -> Integer } :

SubstitutionInt{ P

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 : P_{1}[p . i1,p . i2,F_{1}((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT)

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

A1:
for n being Nat

for i1, i2, i3 being Element of n

for a being Integer holds { p where p is b_{1} -element XFinSequence of NAT : P_{1}[p . i1,p . i2,a * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
and

A2: for n being Nat

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

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

for i1, i2, i3 being Element of n

for a being Integer holds { p where p is b

A2: for n being Nat

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

for a being Integer holds { p where p is b

proof end;

theorem Th11: :: HILB10_3:11

for n being Nat

for a, b, c, d being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c, d being Integer

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

proof end;

theorem Th12: :: HILB10_3:12

for n being Nat

for a being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT)

for a being Integer

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

proof end;

theorem Th13: :: HILB10_3:13

for n being Nat

for a, b being Integer

for i1 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT)

for a, b being Integer

for i1 being Element of n holds { p where p is b

proof end;

theorem Th14: :: HILB10_3:14

for n being Nat

for a being Integer

for i1 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

for a being Integer

for i1 being Element of n holds { p where p is b

proof end;

theorem :: HILB10_3:15

for n being Nat

for a, b being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i1 = (a * (p . i2)) + b } is diophantine Subset of (n -xtuples_of NAT)

for a, b being Integer

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

proof end;

theorem :: HILB10_3:16

for n being Nat

for a, b, c being Integer

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th17: :: HILB10_3:17

for n being Nat

for a, b being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

for a, b being Integer

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

proof end;

theorem Th18: :: HILB10_3:18

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) < (b * (p . i2)) + (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th19: :: HILB10_3:19

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th20: :: HILB10_3:20

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

Lm1: for x, y being Integer

for D being Nat holds

( (x ^2) - (D * (y ^2)) = 1 iff [x,y] is Pell's_solution of D )

proof end;

theorem Th21: :: HILB10_3:21

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th22: :: HILB10_3:22

for n being Nat

for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)

for a, b, c being Integer

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

proof end;

theorem Th23: :: HILB10_3:23

for n being Nat

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)

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

proof end;

theorem :: HILB10_3:24

for n being Nat

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

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

proof end;