:: Diophantine Sets -- Preliminaries
:: by Karol P\kak
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


registration
let c1, c2 be Complex;
cluster <%c1,c2%> -> complex-valued ;
coherence
<%c1,c2%> is complex-valued
proof end;
end;

definition
let cF be XFinSequence;
func Product cF -> Element of COMPLEX equals :: HILB10_4:def 1
multcomplex "**" cF;
coherence
multcomplex "**" cF is Element of COMPLEX ;
end;

:: deftheorem defines Product HILB10_4:def 1 :
for cF being XFinSequence holds Product cF = multcomplex "**" cF;

theorem Th1: :: HILB10_4:1
for cF being complex-valued XFinSequence st cF is real-valued holds
Product cF = multreal "**" cF
proof end;

theorem :: HILB10_4:2
for cF being complex-valued XFinSequence st cF is INT -valued holds
Product cF = multint "**" cF
proof end;

theorem Th3: :: HILB10_4:3
for cF being complex-valued XFinSequence st cF is natural-valued holds
Product cF = multnat "**" cF
proof end;

registration
let F be real-valued XFinSequence;
cluster Product F -> real ;
coherence
Product F is real
proof end;
end;

registration
let F be natural-valued XFinSequence;
cluster Product F -> natural ;
coherence
Product F is natural
proof end;
end;

theorem Th4: :: HILB10_4:4
for cF being complex-valued XFinSequence st cF = {} holds
Product cF = 1
proof end;

theorem Th5: :: HILB10_4:5
for c being Complex holds Product <%c%> = c
proof end;

theorem :: HILB10_4:6
for c1, c2 being Complex holds Product <%c1,c2%> = c1 * c2
proof end;

theorem Th7: :: HILB10_4:7
for cF1, cF2 being complex-valued XFinSequence holds Product (cF1 ^ cF2) = (Product cF1) * (Product cF2)
proof end;

theorem Th8: :: HILB10_4:8
for cF1, cF2 being complex-valued XFinSequence
for c being Complex holds c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2)
proof end;

theorem Th9: :: HILB10_4:9
for c1, c2 being Complex holds c1 + <%c2%> = <%(c1 + c2)%>
proof end;

theorem Th10: :: HILB10_4:10
for f1, f2 being XFinSequence
for n being Nat st n <= len f1 holds
(f1 ^ f2) /^ n = (f1 /^ n) ^ f2
proof end;

registration
let n be Nat;
cluster Relation-like omega -defined Sequence-like Function-like natural-valued V55() n -element V213() for set ;
existence
ex b1 being XFinSequence st
( b1 is n -element & b1 is natural-valued )
proof end;
end;

registration
cluster Relation-like omega -defined Sequence-like Function-like natural-valued V55() V213() positive-yielding for set ;
existence
ex b1 being XFinSequence st
( b1 is natural-valued & b1 is positive-yielding )
proof end;
end;

registration
let R be positive-yielding Relation;
let X be set ;
cluster R | X -> positive-yielding ;
coherence
R | X is positive-yielding
proof end;
end;

registration
let X be real-valued positive-yielding XFinSequence;
cluster Product X -> positive ;
coherence
Product X is positive
proof end;
end;

theorem :: HILB10_4:11
for i being Nat
for X being natural-valued positive-yielding XFinSequence st i in dom X holds
X . i <= Product X
proof end;

registration
let X be natural-valued XFinSequence;
let n be positive Nat;
cluster n + X -> positive-yielding ;
coherence
n + X is positive-yielding
proof end;
end;

theorem :: HILB10_4:12
for X1, X2 being natural-valued XFinSequence st len X1 = len X2 & ( for n being Nat st n in dom X1 holds
X1 . n <= X2 . n ) holds
Product X1 <= Product X2
proof end;

theorem Th13: :: HILB10_4:13
for n, k being Nat st k <= n holds
n choose k <= n |^ k
proof end;

theorem Th14: :: HILB10_4:14
for i, n, k, u being Nat st u > n |^ k & n >= k & k > i holds
(n choose i) * (u |^ i) < (u |^ k) / n
proof end;

theorem Th15: :: HILB10_4:15
for n, k, u being Nat st u > n |^ k & n >= k holds
[\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k
proof end;

theorem Th16: :: HILB10_4:16
for x, y, z being Nat holds
( ( x >= z & y = x choose z ) iff ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z ) )
proof end;

Lm1: for n, k being Nat st k < n holds
( 1 - (k / n) = (n - k) / n & 1 / (1 - (k / n)) = n / (n - k) )
proof end;

Lm2: for n, k being Nat st k < n holds
(n |^ k) / (n choose k) <= ((k !) * 1) / ((1 - (k / n)) |^ k)
proof end;

Lm3: for n, k being Nat st 0 < 2 * k & 2 * k < n holds
1 / (1 - (k / n)) <= 1 + ((2 * k) / n)
proof end;

Lm4: for n, k being Nat st k < n holds
k ! <= (n |^ k) / (n choose k)
proof end;

Lm5: for k being Nat
for r being Real st 0 < r & r < 1 / 2 holds
(1 + r) |^ k < 1 + (r * (2 |^ k))
proof end;

theorem Th17: :: HILB10_4:17
for n, k being Nat st k > 0 & n > (2 * k) |^ (k + 1) holds
k ! = [\((n |^ k) / (n choose k))/]
proof end;

theorem Th18: :: HILB10_4:18
for x, y being Nat holds
( y = x ! iff ex n, y1, y2, y3 being Nat st
( y1 = (2 * x) |^ (x + 1) & y2 = n |^ x & y3 = n choose x & n > y1 & y = [\(y2 / y3)/] ) )
proof end;

theorem Th19: :: HILB10_4:19
for x1, w, u being Nat st x1 * w,1 are_congruent_mod u holds
for x being Nat holds Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u
proof end;

theorem Th20: :: HILB10_4:20
for x, y, x1 being Nat st x1 >= 1 holds
( y = Product (1 + (x1 * (idseq x))) iff ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) )
proof end;

theorem Th21: :: HILB10_4:21
for n being Nat
for c1, c2 being Complex holds c1 + (n |-> c2) = n |-> (c1 + c2)
proof end;

theorem :: HILB10_4:22
for x, y, x1 being Nat st x1 = 0 holds
( y = Product (1 + (x1 * (idseq x))) iff y = 1 )
proof end;

theorem Th23: :: HILB10_4:23
for n, k being Nat st n >= k holds
Product ((n + 1) + (- (idseq k))) = (k !) * (n choose k)
proof end;

theorem :: HILB10_4:24
for y, x1, x2 being Nat holds
( y = Product ((x2 + 1) + (- (idseq x1))) & x2 > x1 iff ( y = (x1 !) * (x2 choose x1) & x2 > x1 ) ) by Th23;

theorem Th25: :: HILB10_4:25
for n, a, b being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = ((a * (p . i2)) + b) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:26
for n being Nat
for a being Integer
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = (a * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:27
for n being Nat
for A being diophantine Subset of (n -xtuples_of NAT)
for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is b1 -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
proof end;

theorem Th28: :: HILB10_4:28
for n being Nat
for a, b being Integer
for c being Nat
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)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th29: :: HILB10_4:29
for n being Nat
for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is b1 -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th30: :: HILB10_4:30
for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th31: :: HILB10_4:31
for n being Nat
for i1, i2 being Element of n st n <> 0 holds
{ p where p is b1 -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th32: :: HILB10_4:32
for n being Nat
for i1, i2 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:33
for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th34: :: HILB10_4:34
for n being Nat
for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is b1 -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th35: :: HILB10_4:35
for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:36
for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th37: :: HILB10_4:37
for n being Nat
for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is b1 -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:38
for n being Nat
for i1, i2, i3 being Element of n holds { p where p is b1 -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_4:39
for i, n1, n2, n being Nat
for i1 being Element of n holds { p where p is b4 -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
proof end;