:: Prime Representing Polynomial
:: by Karol P\kak
::
:: Received November 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


theorem Th1: :: HILB10_6:1
for n being Nat
for i being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i > 1 } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th2: :: HILB10_6:2
for n being Nat
for i, j being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i = (((p . j) -' 1) !) + 1 } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem Th3: :: HILB10_6:3
for n being Nat
for i being Element of n holds { p where p is b1 -element XFinSequence of NAT : ( ((((p . i) -' 1) !) + 1) mod (p . i) = 0 & p . i > 1 ) } is diophantine Subset of (n -xtuples_of NAT)
proof end;

theorem :: HILB10_6:4
for n being Nat
for i being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i is prime } 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 Th5: :: HILB10_6:5
for n, e being Nat st 2 <= e & ex i being Nat st (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 holds
(e - 1) + (e |^ (e -' 2)) <= n
proof end;

theorem Th6: :: HILB10_6:6
for e, t being Nat st 2 <= e & 0 < t holds
ex n, i being Nat st
( t divides n + 1 & (((e ^2) * (e * (e + 2))) * ((n + 1) ^2)) + 1 = i ^2 )
proof end;

theorem Th7: :: HILB10_6:7
for n, k being Nat st n >= k holds
n choose k >= (((n + 1) - k) |^ k) / (k !)
proof end;

theorem Th8: :: HILB10_6:8
for n, k being Nat st n >= k holds
n choose k <= (n |^ k) / (k !)
proof end;

theorem Th9: :: HILB10_6:9
for i, j, n being Nat st i <= j & 2 * j <= n + 1 holds
n choose i <= n choose j
proof end;

Lm2: for n, k being Nat st n > 0 holds
k + (n |^ k) <= (1 + n) |^ k
proof end;

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

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

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

theorem Th10: :: HILB10_6:10
for n, k being Nat st k <= n holds
n ! <= (k !) * (n |^ (n -' k))
proof end;

theorem Th11: :: HILB10_6:11
for n, k, p being Nat st 0 < k & (2 * k) |^ k <= n & n |^ k < p holds
( ((p + 1) |^ n) mod (p |^ (k + 1)) > 0 & k ! < (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) & (((n + 1) |^ k) * (p |^ k)) / (((p + 1) |^ n) mod (p |^ (k + 1))) < (k !) + 1 )
proof end;

theorem Th12: :: HILB10_6:12
for n being Nat
for a being non trivial Nat holds
( Px (a,(n + 2)) = ((2 * a) * (Px (a,(n + 1)))) - (Px (a,n)) & Py (a,(n + 2)) = ((2 * a) * (Py (a,(n + 1)))) - (Py (a,n)) )
proof end;

theorem Th13: :: HILB10_6:13
for n, p being Nat
for a being non trivial Nat holds Px (a,n),(p |^ n) + ((Py (a,n)) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
proof end;

theorem Th14: :: HILB10_6:14
for n, p being Nat
for a being non trivial Nat st 0 < p |^ n & p |^ n < a holds
(p |^ n) + ((Py (a,n)) * (a - p)) <= Px (a,n)
proof end;

theorem Th15: :: HILB10_6:15
for n being Nat
for a, b being non trivial Nat st a <= b holds
( Px (a,n) <= Px (b,n) & Py (a,n) <= Py (b,n) )
proof end;

theorem Th16: :: HILB10_6:16
for n, k being Nat
for a, b being non trivial Nat st a,b are_congruent_mod k holds
Px (a,n), Px (b,n) are_congruent_mod k
proof end;

theorem Th17: :: HILB10_6:17
for a being non trivial Nat
for x, y being Integer holds Px (a,|.((2 * x) + y).|), - (Px (a,|.y.|)) are_congruent_mod Px (a,|.x.|)
proof end;

theorem Th18: :: HILB10_6:18
for a being non trivial Nat
for x, y being Integer holds Px (a,|.((4 * x) + y).|), Px (a,|.y.|) are_congruent_mod Px (a,|.x.|)
proof end;

Lm6: for i, j, n being Nat st i <= j & j < n & i,j are_congruent_mod n holds
i = j
proof end;

Lm7: for i, j, n being Nat st i < n & j < n & i,j are_congruent_mod n holds
i = j
proof end;

theorem Th19: :: HILB10_6:19
for n, k being Nat
for a being non trivial Nat st k < n holds
Px (a,k) < Px (a,n)
proof end;

theorem Th20: :: HILB10_6:20
for n, k being Nat
for a being non trivial Nat st Px (a,k) = Px (a,n) holds
k = n
proof end;

Lm8: for i, j, n being Nat
for a being non trivial Nat st Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & i < n & j < n holds
i = j
proof end;

Lm9: for i, n being Nat
for a being non trivial Nat st i < n & ( not a = 2 or not n = 1 ) holds
Px (a,i) < (Px (a,n)) / 2
proof end;

Lm10: for i, j, n being Nat
for a being non trivial Nat st Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & n < i & i <= 2 * n & n < j & j <= 2 * n holds
i = j
proof end;

theorem Th21: :: HILB10_6:21
for i, j, n being Nat
for a being non trivial Nat st i <= j & j <= 2 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not ( i = 0 & j = 2 & a = 2 & n = 1 ) holds
i = j
proof end;

theorem Th22: :: HILB10_6:22
for i, j, n being Nat
for a being non trivial Nat st 0 < i & i <= n & 0 <= j & j < 4 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j = i holds
j + i = 4 * n
proof end;

theorem Th23: :: HILB10_6:23
for n being Nat
for a being non trivial Nat
for x, y being Integer holds Px (a,|.(((4 * x) * n) + y).|), Px (a,|.y.|) are_congruent_mod Px (a,|.x.|)
proof end;

theorem Th24: :: HILB10_6:24
for i, j, n being Nat
for a being non trivial Nat st 0 < i & i <= n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j,i are_congruent_mod 4 * n holds
j, - i are_congruent_mod 4 * n
proof end;

theorem Th25: :: HILB10_6:25
for n being Nat
for a being non trivial Nat holds Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))
proof end;

theorem Th26: :: HILB10_6:26
for a being non trivial Nat
for y, n, b, c, d, r, s, t, u, v, x being Nat st 1 <= n & [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [s,t] is Pell's_solution of (b ^2) -' 1 & v = (4 * r) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y holds
( not b is trivial & u ^2 > a & y = Py (a,n) )
proof end;

theorem Th27: :: HILB10_6:27
for a being non trivial Nat
for y, n being Nat st 1 <= n & y = Py (a,n) holds
ex b, c, d, r, s, t, u, v, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & [u,v] is Pell's_solution of (a ^2) -' 1 & [s,t] is Pell's_solution of (b ^2) -' 1 & v = (4 * r) * (y ^2) & b = a + ((u ^2) * ((u ^2) - a)) & s = x + (c * u) & t = n + ((4 * d) * y) & n <= y )
proof end;

theorem Th28: :: HILB10_6:28
for a being non trivial Nat
for y, n being Nat st 1 <= n holds
( y = Py (a,n) iff ex c, d, r, u, x being Nat st
( [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & n <= y ) )
proof end;

theorem Th29: :: HILB10_6:29
for f, k being positive Nat holds
( f = k ! iff ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) )
proof end;

theorem Th30: :: HILB10_6:30
for k being positive Nat holds
( k + 1 is prime iff ex a, b, c, d, e, f, g, h, i, j, l, m, n, o, p, q, r, s, t, u, w, v, x, y, z being Nat st
( q = ((w * z) + h) + j & z = ((((g * k) + g) + k) * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 & e = ((p + q) + z) + (2 * n) & (((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 & [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & [m,l] is Pell's_solution of (a ^2) -' 1 & l = k + (i * (a - 1)) & (n + l) + v = y & m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) ) )
proof end;

:: WP: Prime Representing Polynomial
theorem :: HILB10_6:31
for k being positive Nat holds
( k + 1 is prime iff ex a, b, c, d, e, f, g, h, i, j, l, m, n, o, p, q, r, s, t, u, w, v, x, y, z being Nat st 0 = (((((((((((((((((w * z) + h) + j) - q) ^2) + (((((((g * k) + g) + k) * (h + j)) + h) - z) ^2)) + (((((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1) - (f ^2)) ^2)) + (((((p + q) + z) + (2 * n)) - e) ^2)) + ((((((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1) - (o ^2)) ^2)) + ((((x ^2) - (((a ^2) -' 1) * (y ^2))) - 1) ^2)) + (((((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1) - (u ^2)) ^2)) + (((((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1) - ((x + (c * u)) ^2)) ^2)) + ((((m ^2) - (((a ^2) -' 1) * (l ^2))) - 1) ^2)) + (((k + (i * (a - 1))) - l) ^2)) + ((((n + l) + v) - y) ^2)) + ((((p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1))) - m) ^2)) + ((((q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1))) - x) ^2)) + ((((z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1))) - (p * m)) ^2) )
proof end;