:: by Karol P\kak

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

:: deftheorem defines Product HILB10_4:def 1 :

for cF being XFinSequence holds Product cF = multcomplex "**" cF;

for cF being XFinSequence holds Product cF = multcomplex "**" cF;

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)

for c being Complex holds c + (cF1 ^ cF2) = (c + cF1) ^ (c + cF2)

proof end;

registration

let n be Nat;

ex b_{1} being XFinSequence st

( b_{1} is n -element & b_{1} is natural-valued )

end;
cluster Relation-like omega -defined Sequence-like Function-like natural-valued V55() n -element V213() for set ;

existence ex b

( b

proof end;

registration

ex b_{1} being XFinSequence st

( b_{1} is natural-valued & b_{1} is positive-yielding )
end;

cluster Relation-like omega -defined Sequence-like Function-like natural-valued V55() V213() positive-yielding for set ;

existence ex b

( b

proof end;

registration
end;

registration
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

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;

coherence

n + X is positive-yielding

end;
let n be positive Nat;

coherence

n + X is positive-yielding

proof 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

X1 . n <= X2 . n ) holds

Product X1 <= Product X2

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

(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

[\(((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 ) )

( ( 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 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)/] ) )

( 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

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

( 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 :: HILB10_4:24

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_{1} -element XFinSequence of NAT : p . i1 = ((a * (p . i2)) + b) * (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;

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

for a being Integer

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

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_{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, nk being Nat st k + nk = n holds

{ (p /^ nk) where p is b

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_{1} -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)

for a, b being Integer

for c being Nat

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

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

for i1, i2, i3 being Element of n st n <> 0 holds

{ p where p is b

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_{1} -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (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;

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_{1} -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)

for i1, i2 being Element of n st n <> 0 holds

{ p where p is b

proof end;

theorem Th32: :: HILB10_4:32

for n being Nat

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

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

proof end;

theorem :: HILB10_4:33

for n being Nat

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = 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;

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_{1} -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)

for i1, i2, i3 being Element of n st n <> 0 holds

{ p where p is b

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_{1} -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 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_4:36

for n being Nat

for i1, i2, i3 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } 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 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_{1} -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)

for i1, i2, i3 being Element of n st n <> 0 holds

{ p where p is b

proof end;

theorem :: HILB10_4:38

for n being Nat

for i1, i2, i3 being Element of n holds { p where p is b_{1} -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)

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

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_{4} -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)

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

proof end;