:: 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 b₁ being XFinSequence st
( b₁ is n -element & b₁ 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 b₁ being XFinSequence st
( b₁ is natural-valued & b₁ 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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₄ -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)

proof end;