:: Prime Representing Polynomial with 10 Unknowns -- Introduction. Part II
:: by Karol P\kak
::
:: Received December 27, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

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;

definition

let t be Real;

attr t is theta means :Def1: :: HILB10_8:def 1
( - 1 <= t & t <= 1 );

end;

:: deftheorem Def1 defines theta HILB10_8:def 1 :
for t being Real holds
( t is theta iff ( - 1 <= t & t <= 1 ) );

registration

cluster 0 -> theta ;

coherence
0 is theta ;

cluster complex real ext-real theta for object ;

existence
ex b₁ being Real st b₁ is theta

proof end;

end;

definition

mode _Theta is theta Real;

end;

registration

let t be _Theta;

cluster - t -> theta ;

coherence
- t is theta

proof end;

let u be _Theta;

cluster t * u -> theta ;

coherence
t * u is theta

proof end;

end;

theorem Th1: :: HILB10_8:1

for T being _Theta holds |.T.| <= 1

proof end;

theorem Th2: :: HILB10_8:2

for T being _Theta
for lambda, epsilon1, epsilon2 being Real st lambda = T * epsilon1 & |.epsilon1.| <= |.epsilon2.| holds
ex T1 being _Theta st lambda = T1 * epsilon2

proof end;

theorem Th3: :: HILB10_8:3

for T1, T2 being _Theta
for lambda, epsilon1, epsilon2 being Real st lambda = (1 + (T1 * epsilon1)) * (1 + (T2 * epsilon2)) & 0 <= epsilon1 & epsilon1 <= 1 & 0 <= epsilon2 holds
ex T being _Theta st lambda = 1 + (T * (epsilon1 + (2 * epsilon2)))

proof end;

theorem Th4: :: HILB10_8:4

for T1, T2 being _Theta
for epsilon1, epsilon2 being Real st T1 * epsilon1 <= epsilon2 & epsilon2 <= T2 * epsilon1 holds
ex T being _Theta st epsilon2 = T * epsilon1

proof end;

theorem Th5: :: HILB10_8:5

for T being _Theta
for lambda, epsilon1, epsilon2 being Real st lambda = T * epsilon1 & epsilon1 <= epsilon2 & 0 <= epsilon1 holds
ex T1 being _Theta st lambda = T1 * epsilon2

proof end;

theorem Th6: :: HILB10_8:6

for T1, T2 being _Theta
for epsilon1, epsilon2 being Real st 0 <= epsilon1 & 0 <= epsilon2 holds
ex T being _Theta st (T1 * epsilon1) + (T2 * epsilon2) = T * (epsilon1 + epsilon2)

proof end;

theorem Th7: :: HILB10_8:7

for T1 being _Theta
for epsilon being Real st 0 <= epsilon & epsilon <= 1 / 2 holds
ex T2 being _Theta st 1 / (1 + (T1 * epsilon)) = 1 + ((T2 * 2) * epsilon)

proof end;

theorem Th8: :: HILB10_8:8

for n, m being Nat st m ^2 <= n holds
ex T being _Theta st n choose m = ((n |^ m) / (m !)) * (1 + (T * ((m ^2) / n)))

proof end;

theorem Th9: :: HILB10_8:9

for n being Nat
for T being _Theta
for alpha, epsilon being Real st alpha = (1 + (T * epsilon)) |^ n & 0 <= epsilon & epsilon <= 1 / (2 * n) holds
ex T1 being _Theta st alpha = 1 + (((T1 * 2) * n) * epsilon)

proof end;

theorem Th10: :: HILB10_8:10

for n being Nat
for a being non trivial Nat st n <= a holds
ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))

proof end;

theorem Th11: :: HILB10_8:11

for a being non trivial Nat
for y, n being Nat st y > 0 & n > 0 & (((a ^2) - 1) * (y ^2)) + 1 is square & y,n are_congruent_mod a - 1 & y <= Py (a,(a - 1)) & n <= a - 1 holds
y = Py (a,n)

proof end;

theorem Th12: :: HILB10_8:12

for a being non trivial Nat
for s, n being Nat holds (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1

proof end;

theorem Th13: :: HILB10_8:13

for a being non trivial Nat
for s, n, r being Nat st s > 0 & r > 0 & (((s ^2) * (r ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * r)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 & s * (((s |^ n) ^2) * (s |^ n)) < a & s * ((r ^2) * r) < a holds
r = s |^ n

proof end;

theorem Th14: :: HILB10_8:14

for a, b, c, d being Nat st a <= b & b <= c & 2 * c <= d & c > 0 holds
for f being FinSequence of REAL st len f = (b - a) + 1 & ( for i being Nat st i + 1 in dom f holds
f . (i + 1) = (c choose (a + i)) * (d |^ (c -' (a + i))) ) holds
( 0 < Sum f & Sum f < (2 * (c |^ a)) * (d |^ (c -' a)) )

proof end;

theorem Th15: :: HILB10_8:15

for f, k, m, r, s, t, u being Nat
for W, M, U, S, T, Q being Integer st f > 0 & k > 0 & m > 0 & u > 0 & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 holds
( M * (U + 1) is non trivial Nat & W is Nat & ( for mu being non trivial Nat
for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k ! ) )

proof end;

theorem Th16: :: HILB10_8:16

for f, k being Nat st f = k ! & k > 0 holds
ex m, r, s, t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( m > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )

proof end;

theorem Th17: :: HILB10_8:17

for A being non trivial Nat
for C, B, e being Nat st 0 < B & C = Py (A,B) holds
ex i, j, D, E, F, G, H, I being Nat st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )

proof end;

theorem Th18: :: HILB10_8:18

for A being non trivial Nat
for C, B, e being Nat st 0 < B holds
for i, j being Nat
for D, E, F, G, H, I being Integer st (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 holds
C = Py (A,B)

proof end;

:: Diophantine Representation of Solutions to Pell's Equation
::with 2 Explicite Unknowns $i$, $j$

theorem :: HILB10_8:19

for A being non trivial Nat
for C, B, e being Nat st 0 < B holds
( C = Py (A,B) iff ex i, j being Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (e + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )

proof end;

theorem Th20: :: HILB10_8:20

for A being non trivial Nat
for C being Nat
for B, L being positive Nat holds
( C = Py (A,B) iff ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )

proof end;

theorem :: HILB10_8:21

for k being Nat
for L being positive Nat st k > 0 holds
( k + 1 is prime iff ex f, i, j, m, u being positive Nat ex r, s, t being Nat ex A, B, C, D, E, F, G, H, I, W, U, M, S, T, Q being Integer st
( (D * F) * I is square & F divides H - C & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & k + 1 divides f + 1 & A = M * (U + 1) & B = W + 1 & C = (r + W) + 1 & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 ) )

proof end;

theorem Th22: :: HILB10_8:22

for a, b, A, B being Integer st a,b are_coprime holds
( ( a divides A & b divides B ) iff a * b divides (a * B) + (b * A) )

proof end;

:: Diophantine Representation of Prime Numbers with 8 Explicite Unknowns

theorem :: HILB10_8:23

for k being Nat st k > 0 holds
( k + 1 is prime iff ex f, i, j, m, u being positive Nat ex r, s, t being Nat ex A, B, C, D, E, F, G, H, I, L, W, U, M, S, T, Q being Integer st
( (D * F) * I is square & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & F * L divides (((H - C) * L) + ((F * (f + 1)) * Q)) + ((F * (k + 1)) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)) & A = M * (U + 1) & B = W + 1 & C = (r + W) + 1 & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 & L = (k + 1) * Q & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 ) )

proof end;