:: Basic Diophantine Relations
:: 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;

cluster a * p -> INT -valued ;

coherence
a * p is INT -valued

proof end;

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

proof end;

theorem Th2: :: HILB10_3:2

for n, k being Nat
for i1 being Element of n holds i1 is Element of n + k

proof end;

theorem Th3: :: HILB10_3:3

for n, m, k being Nat st k < m holds
n + k in n + m

proof end;

theorem Th4: :: HILB10_3:4

for n, k being Nat
for i1 being Element of n
for p being b₁ + b₂ -element XFinSequence st n <> 0 & k <> 0 holds
(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₁ -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

proof end;

scheme :: HILB10_3:sch 1
UnionDiophantine{ F₁() -> Nat, P₁[ XFinSequence of NAT ], P₂[ XFinSequence of NAT ] } :

{ p where p is F₁() -element XFinSequence of NAT : ( P₁[p] or P₂[p] ) } is diophantine Subset of (F₁() -xtuples_of NAT)

provided

A1: { p where p is F₁() -element XFinSequence of NAT : P₁[p] } is diophantine Subset of (F₁() -xtuples_of NAT) and
A2: { p where p is F₁() -element XFinSequence of NAT : P₂[p] } is diophantine Subset of (F₁() -xtuples_of NAT)

proof end;

scheme :: HILB10_3:sch 2
Eq{ F₁() -> Nat, P₁[ object ], P₂[ object ] } :

{ p where p is F₁() -element XFinSequence of NAT : P₁[p] } = { q where q is F₁() -element XFinSequence of NAT : P₂[q] }

provided

A1: for p being F₁() -element XFinSequence of NAT holds
( P₁[p] iff P₂[p] )

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₁ -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -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)

proof end;

scheme :: HILB10_3:sch 3
IntersectionDiophantine{ F₁() -> Nat, P₁[ XFinSequence], P₂[ XFinSequence] } :

{ p where p is F₁() -element XFinSequence of NAT : ( P₁[p] & P₂[p] ) } is diophantine Subset of (F₁() -xtuples_of NAT)

provided

A1: { p where p is F₁() -element XFinSequence of NAT : P₁[p] } is diophantine Subset of (F₁() -xtuples_of NAT) and
A2: { p where p is F₁() -element XFinSequence of NAT : P₂[p] } is diophantine Subset of (F₁() -xtuples_of NAT)

proof end;

scheme :: HILB10_3:sch 4
Substitution{ P₁[ Nat, Nat, natural object , Nat, Nat, Nat], F₁( Nat, Nat, Nat) -> natural object } :

for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : P₁[p . i1,p . i2,F₁((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)

provided

A1: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : P₁[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₁ -element XFinSequence of NAT : F₁((p . i1),(p . i2),(p . i3)) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)

proof end;

scheme :: HILB10_3:sch 5
SubstitutionInt{ P₁[ Nat, Nat, Integer], F₁( Nat, Nat, Nat) -> Integer } :

for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : P₁[p . i1,p . i2,F₁((p . i3),(p . i4),(p . i5))] } is diophantine Subset of (n -xtuples_of NAT)

provided

A1: for n being Nat
for i1, i2, i3 being Element of n
for a being Integer holds { p where p is b₁ -element XFinSequence of NAT : P₁[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₁ -element XFinSequence of NAT : F₁((p . i1),(p . i2),(p . i3)) = a * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : p . i1 = (a * (p . i2)) + b } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) < (b * (p . i2)) + (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT)

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₁ -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)

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₁ -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)

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₁ -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of (n -xtuples_of NAT)

proof end;

theorem :: HILB10_3:24

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

proof end;