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

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

( 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;

definition

let a, n be Nat;

assume A1: not a is trivial ;

ex b_{1} being Nat st

for b being non trivial Nat st b = a holds

ex y being Nat st b_{1} + (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_{1}, b_{2} being Nat st ( for b being non trivial Nat st b = a holds

ex y being Nat st b_{1} + (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_{2} + (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_{1} = b_{2}

end;
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 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;

ex b

for b being non trivial Nat st b = a holds

ex y being Nat st b

proof end;

uniqueness for b

ex y being Nat st b

ex y being Nat st b

b

proof end;

:: deftheorem Def1 defines Px HILB10_1:def 1 :

for a, n being Nat st not a is trivial holds

for b_{3} being Nat holds

( b_{3} = Px (a,n) iff for b being non trivial Nat st b = a holds

ex y being Nat st b_{3} + (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 a, n being Nat st not a is trivial holds

for b

( b

ex y being Nat st b

definition

let a, n be Nat;

assume A1: not a is trivial ;

ex b_{1} being Nat st

for b being non trivial Nat st b = a holds

(Px (b,n)) + (b_{1} * (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_{1}, b_{2} being Nat st ( for b being non trivial Nat st b = a holds

(Px (b,n)) + (b_{1} * (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_{2} * (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_{1} = b_{2}

end;
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 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;

ex b

for b being non trivial Nat st b = a holds

(Px (b,n)) + (b

proof end;

uniqueness for b

(Px (b,n)) + (b

(Px (b,n)) + (b

b

proof end;

:: deftheorem Def2 defines Py HILB10_1:def 2 :

for a, n being Nat st not a is trivial holds

for b_{3} being Nat holds

( b_{3} = Py (a,n) iff for b being non trivial Nat st b = a holds

(Px (b,n)) + (b_{3} * (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 a, n being Nat st not a is trivial holds

for b

( b

(Px (b,n)) + (b

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

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

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

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 )

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

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;

Lm4: for k being Nat

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

k = 0

proof end;

registration
end;

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

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)

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 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

( 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;