:: The {M}atiyasevich Theorem -- Preliminaries
:: by Karol P\kak
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

Lm1: for n being Nat holds [\(((2 * n) + 1) / 2)/] = n

proof end;

Lm2: for n being Nat holds [/(((2 * n) + 1) / 2)\] = n + 1

proof end;

theorem Th1: :: HILB10_1:1

for n being Nat
for F being FinSequence of NAT st ( for k being Nat st 1 < k & k <= len F holds
(F . k) mod n = 0 ) holds
(Sum F) mod n = (F . 1) mod n

proof end;

theorem Th2: :: HILB10_1:2

for f being complex-valued FinSequence ex e, o being complex-valued FinSequence st
( len e = [\((len f) / 2)/] & len o = [/((len f) / 2)\] & Sum f = (Sum e) + (Sum o) & ( for n being Nat holds
( e . n = f . (2 * n) & o . n = f . ((2 * n) - 1) ) ) )

proof end;

registration

let a be non trivial Nat;

cluster (a ^2) -' 1 -> non square ;

coherence
not (a ^2) -' 1 is square

proof end;

end;

definition

let a, n be Nat;
assume A1: not a is trivial ;

func Px (a,n) -> Nat means :Def1: :: HILB10_1:def 1
for b being non trivial Nat st b = a holds
ex y being Nat st it + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n;

existence
ex b₁ being Nat st
for b being non trivial Nat st b = a holds
ex y being Nat st b₁ + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n

proof end;

uniqueness
for b₁, b₂ being Nat st ( for b being non trivial Nat st b = a holds
ex y being Nat st b₁ + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n ) & ( for b being non trivial Nat st b = a holds
ex y being Nat st b₂ + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Px HILB10_1:def 1 :
for a, n being Nat st not a is trivial holds
for b₃ being Nat holds
( b₃ = Px (a,n) iff for b being non trivial Nat st b = a holds
ex y being Nat st b₃ + (y * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n );

definition

let a, n be Nat;
assume A1: not a is trivial ;

func Py (a,n) -> Nat means :Def2: :: HILB10_1:def 2
for b being non trivial Nat st b = a holds
(Px (b,n)) + (it * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n;

existence
ex b₁ being Nat st
for b being non trivial Nat st b = a holds
(Px (b,n)) + (b₁ * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n

proof end;

uniqueness
for b₁, b₂ being Nat st ( for b being non trivial Nat st b = a holds
(Px (b,n)) + (b₁ * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n ) & ( for b being non trivial Nat st b = a holds
(Px (b,n)) + (b₂ * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Py HILB10_1:def 2 :
for a, n being Nat st not a is trivial holds
for b₃ being Nat holds
( b₃ = Py (a,n) iff for b being non trivial Nat st b = a holds
(Px (b,n)) + (b₃ * (sqrt ((b ^2) -' 1))) = (((min_Pell's_solution_of ((b ^2) -' 1)) `1) + (((min_Pell's_solution_of ((b ^2) -' 1)) `2) * (sqrt ((b ^2) -' 1)))) |^ n );

theorem Th6: :: HILB10_1:3

for a being non trivial Nat holds
( Px (a,0) = 1 & Py (a,0) = 0 )

proof end;

Lm3: 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 Th7: :: HILB10_1:4

for n1, n2 being Nat
for a being non trivial Nat st [n1,n2] is Pell's_solution of (a ^2) -' 1 holds
ex n being Nat st
( n1 = Px (a,n) & n2 = Py (a,n) )

proof end;

theorem Th8: :: HILB10_1:5

for a being non trivial Nat holds [a,1] = min_Pell's_solution_of ((a ^2) -' 1)

proof end;

theorem Th9: :: HILB10_1:6

for n being Nat
for a being non trivial Nat holds
( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) )

proof end;

theorem Th10: :: HILB10_1:7

for n being Nat
for a being non trivial Nat holds ((Px (a,n)) ^2) - (((a ^2) -' 1) * ((Py (a,n)) ^2)) = 1

proof end;

theorem Th11: :: HILB10_1:8

for n being Nat
for a being non trivial Nat holds
( (Px (a,n)) + ((Py (a,n)) * (sqrt ((a ^2) -' 1))) = (a + (sqrt ((a ^2) -' 1))) |^ n & (Px (a,n)) + ((- (Py (a,n))) * (sqrt ((a ^2) -' 1))) = (a - (sqrt ((a ^2) -' 1))) |^ n )

proof end;

theorem Th12: :: HILB10_1:9

for n being Nat
for a being non trivial Nat ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )

proof end;

theorem Th13: :: HILB10_1:10

for n, k being Nat
for a being non trivial Nat st k <= n holds
Px (a,k) <= Px (a,n)

proof end;

registration

let a be non trivial Nat;
let k be Nat;

cluster Px (a,k) -> positive ;

coherence
Px (a,k) is positive

proof end;

end;

theorem Th14: :: HILB10_1:11

for n, k being Nat
for a being non trivial Nat st k < n holds
Py (a,k) < Py (a,n)

proof end;

theorem Th15: :: HILB10_1:12

for n, k being Nat
for a being non trivial Nat st Py (a,k) = Py (a,n) holds
k = n

proof end;

theorem Th16: :: HILB10_1:13

for n being Nat
for a being non trivial Nat holds Py (a,n) >= n

proof end;

Lm4: for k being Nat
for a being non trivial Nat st Py (a,k) = 0 holds
k = 0

proof end;

registration

let a be non trivial Nat;
let k be non zero Nat;

cluster Py (a,k) -> non zero ;

coherence
not Py (a,k) is zero by Lm4;

end;

registration

let a be non trivial Nat;
let x be positive Nat;

cluster a * x -> non trivial ;

coherence
not a * x is trivial

proof end;

end;

theorem Th17: :: HILB10_1:14

for n, k being Nat
for a being non trivial Nat st a <> 2 & k <= n holds
2 * (Py (a,k)) < Px (a,n)

proof end;

theorem Th18: :: HILB10_1:15

for n, k being Nat
for a being non trivial Nat st a = 2 & k <= n holds
(sqrt 3) * (Py (a,k)) < Px (a,n)

proof end;

theorem Th19: :: HILB10_1:16

for n, k being Nat
for a being non trivial Nat st a = 2 & k < n holds
(3 + (2 * (sqrt 3))) * (Py (a,k)) < Px (a,n)

proof end;

theorem Th20: :: HILB10_1:17

for n being Nat
for a being non trivial Nat holds
( (((2 * a) - 1) |^ n) * (a - 1) <= Px (a,(n + 1)) & Px (a,(n + 1)) <= a * ((2 * a) |^ n) & ((2 * a) - 1) |^ n <= Py (a,(n + 1)) & Py (a,(n + 1)) <= (2 * a) |^ n )

proof end;

theorem Th21: :: HILB10_1:18

for n being Nat
for a being non trivial Nat
for x being positive Nat holds
( (x |^ n) * ((1 - (1 / ((2 * a) * x))) |^ n) <= (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) <= (x |^ n) * (1 / ((1 - (1 / (2 * a))) |^ n)) )

proof end;

Lm5: for n being Nat
for r being Real st 0 <= 1 - r & 1 - r <= 1 holds
(1 - r) |^ n >= 1 - (n * r)

proof end;

theorem Th22: :: HILB10_1:19

for n being Nat
for a being non trivial Nat
for x being positive Nat st a > (2 * n) * (x |^ n) holds
( (x |^ n) - (1 / 2) < (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) & (Py ((a * x),(n + 1))) / (Py (a,(n + 1))) < (x |^ n) + (1 / 2) )

proof end;

theorem Th23: :: HILB10_1:20

for x being Integer
for a being non trivial Nat st x >= 0 holds
(sgn x) * (Py (a,|.x.|)) = Py (a,|.x.|)

proof end;

theorem Th24: :: HILB10_1:21

for x being Integer
for a being non trivial Nat st x <= 0 holds
(sgn x) * (Py (a,|.x.|)) = - (Py (a,|.x.|))

proof end;

theorem Th25: :: HILB10_1:22

for x, y being Integer
for a being non trivial Nat holds
( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )

proof end;

theorem Th26: :: HILB10_1:23

for n being Nat
for a being non trivial Nat holds Px (a,n), Py (a,n) are_coprime

proof end;

theorem Th27: :: HILB10_1:24

for n being Nat
for a being non trivial Nat holds Py (a,n),n are_congruent_mod a - 1

proof end;

theorem Th28: :: HILB10_1:25

for n being Nat
for a, b being non trivial Nat holds
( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b )

proof end;

theorem Th29: :: HILB10_1:26

for n, k being Nat
for a, b being non trivial Nat st a,b are_congruent_mod k holds
Py (a,n), Py (b,n) are_congruent_mod k

proof end;

Lm6: for x being Integer
for a being non trivial Nat holds ((sgn x) * (sgn x)) * (Py (a,|.x.|)) = Py (a,|.x.|)

proof end;

theorem Th30: :: HILB10_1:27

for x, y being Integer
for a being non trivial Nat holds (sgn ((2 * x) + y)) * (Py (a,|.((2 * x) + y).|)), - ((sgn y) * (Py (a,|.y.|))) are_congruent_mod Px (a,|.x.|)

proof end;

Lm7: for a being non trivial Nat
for i, j being Integer holds (sgn ((4 * i) + j)) * (Py (a,|.((4 * i) + j).|)),(sgn j) * (Py (a,|.j.|)) are_congruent_mod Px (a,|.i.|)

proof end;

theorem Th31: :: HILB10_1:28

for n being Nat
for x, y being Integer
for a being non trivial Nat holds (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|)

proof end;

theorem Th32: :: HILB10_1:29

for x, y being Integer
for a being non trivial Nat holds (sgn (x + y)) * (Py (a,|.(x + y).|)),(sgn (x - y)) * (Py (a,|.(x - y).|)) are_congruent_mod Px (a,|.x.|)

proof end;

Lm8: for r1, r2 being Real st |.r1.| < r2 holds
( - r2 < r1 & r1 < r2 )

proof end;

theorem Th33: :: HILB10_1:30

for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
x = y

proof end;

Lm9: for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 < n2 & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
n1 = (2 * n) - n2

proof end;

theorem Th34: :: HILB10_1:31

for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 <= 2 * n & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n

proof end;

Lm10: for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 <= 2 * n & 2 * n < n2 & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n

proof end;

Lm11: for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st 2 * n < n1 & n1 <= 4 * n & 2 * n < n2 & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n

proof end;

theorem Th35: :: HILB10_1:32

for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n

proof end;

theorem Th36: :: HILB10_1:33

for n, n1, n2 being Nat
for a being non trivial Nat st Py (a,n1), Py (a,n2) are_congruent_mod Px (a,n) & n > 0 & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n

proof end;

theorem Th37: :: HILB10_1:34

for n, k being Nat
for a being non trivial Nat holds Py (a,n) divides Py (a,(n * k))

proof end;

theorem Th38: :: HILB10_1:35

for n, k being Nat
for a being non trivial Nat holds Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2

proof end;

theorem Th39: :: HILB10_1:36

for n, k being Nat
for a being non trivial Nat st k > 0 & Py (a,k) divides Py (a,n) holds
k divides n

proof end;

theorem Th40: :: HILB10_1:37

for n, k being Nat
for a being non trivial Nat st (Py (a,k)) ^2 divides Py (a,n) holds
Py (a,k) divides n

proof end;

theorem :: HILB10_1:38

for y, z, a being Nat holds
( ( y = Py (a,z) & a > 1 ) iff ex x, x1, y1, A, x2, y2 being Nat st
( a > 1 & [x,y] is Pell's_solution of (a ^2) -' 1 & [x1,y1] is Pell's_solution of (a ^2) -' 1 & y1 >= y & A > y & y >= z & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,y are_congruent_mod x1 & A,a are_congruent_mod x1 & y2,z are_congruent_mod 2 * y & A,1 are_congruent_mod 2 * y & y1, 0 are_congruent_mod y ^2 ) )

proof end;

theorem :: HILB10_1:39

for x, y, z being Nat holds
( y = x |^ z iff ( ( y = 1 & z = 0 ) or ( x = 0 & y = 0 & z > 0 ) or ( x = 1 & y = 1 & z > 0 ) or ( x > 1 & z > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py (x,(z + 1)) & K > (2 * z) * y1 & y2 = Py (K,(z + 1)) & y3 = Py ((K * x),(z + 1)) & ( ( 0 <= y - (y3 / y2) & y - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - y & (y3 / y2) - y < 1 / 2 ) ) ) ) ) )

proof end;