:: 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 b1 + b2 -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 b1 -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 b1 -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 b1 -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{ F1() -> Nat, P1[ XFinSequence of NAT ], P2[ XFinSequence of NAT ] } :
{ p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } is diophantine Subset of (F1() -xtuples_of NAT)
provided
A1: { p where p is F1() -element XFinSequence of NAT : P1[p] } is diophantine Subset of (F1() -xtuples_of NAT) and
A2: { p where p is F1() -element XFinSequence of NAT : P2[p] } is diophantine Subset of (F1() -xtuples_of NAT)
proof end;

scheme :: HILB10_3:sch 2
Eq{ F1() -> Nat, P1[ object ], P2[ object ] } :
{ p where p is F1() -element XFinSequence of NAT : P1[p] } = { q where q is F1() -element XFinSequence of NAT : P2[q] }
provided
A1: for p being F1() -element XFinSequence of NAT holds
( P1[p] iff P2[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 b1 -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 b1 -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 b1 -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{ F1() -> Nat, P1[ XFinSequence], P2[ XFinSequence] } :
{ p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } is diophantine Subset of (F1() -xtuples_of NAT)
provided
A1: { p where p is F1() -element XFinSequence of NAT : P1[p] } is diophantine Subset of (F1() -xtuples_of NAT) and
A2: { p where p is F1() -element XFinSequence of NAT : P2[p] } is diophantine Subset of (F1() -xtuples_of NAT)
proof end;

scheme :: HILB10_3:sch 4
Substitution{ P1[ Nat, Nat, natural object , Nat, Nat, Nat], F1( Nat, Nat, Nat) -> natural object } :
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : P1[p . i1,p . i2,F1((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 b1 -element XFinSequence of NAT : P1[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 b1 -element XFinSequence of NAT : F1((p . i1),(p . i2),(p . i3)) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
proof end;

scheme :: HILB10_3:sch 5
SubstitutionInt{ P1[ Nat, Nat, Integer], F1( Nat, Nat, Nat) -> Integer } :
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : P1[p . i1,p . i2,F1((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 b1 -element XFinSequence of NAT : P1[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 b1 -element XFinSequence of NAT : F1((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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -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 b1 -element XFinSequence of NAT : p . i2 = (p . i1) |^ (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
proof end;