let x, y, z be Nat; ( 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 ) ) ) ) ) )
thus
( not y = x |^ z or ( 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 = 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 ) ) ) ) ) implies y = x |^ z )proof
assume A1:
y = x |^ z
;
( ( 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 ) ) ) ) )
per cases
( z = 0 or z > 0 )
;
suppose
z = 0
;
( ( 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 ) ) ) ) )hence
( (
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 ) ) ) ) )
by A1, NEWTON:4;
verum end; suppose A2:
z > 0
;
( ( 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 ) ) ) ) )per cases
( x = 0 or x = 1 or x > 1 )
by NAT_1:53;
suppose
(
x = 0 or
x = 1 )
;
( ( 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 ) ) ) ) )hence
( (
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 ) ) ) ) )
by A1, A2, NAT_1:14, NEWTON:11;
verum end; suppose A3:
x > 1
;
( ( 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 ) ) ) ) )then reconsider x1 =
x as non
trivial Nat by NAT_2:28;
ex
y1,
y2,
y3,
K being
Nat st
(
y1 = Py (
x1,
(z + 1)) &
K > (2 * z) * y1 &
y2 = Py (
K,
(z + 1)) &
y3 = Py (
(K * x1),
(z + 1)) & ( (
0 <= y - (y3 / y2) &
y - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - y &
(y3 / y2) - y < 1
/ 2 ) ) )
proof
set y1 =
Py (
x1,
(z + 1));
set K =
((2 * z) * (Py (x1,(z + 1)))) + 1;
set y2 =
Py (
(((2 * z) * (Py (x1,(z + 1)))) + 1),
(z + 1));
set y3 =
Py (
((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),
(z + 1));
reconsider K =
((2 * z) * (Py (x1,(z + 1)))) + 1 as non
trivial Nat by A2;
take
Py (
x1,
(z + 1))
;
ex y2, y3, K being Nat st
( Py (x1,(z + 1)) = Py (x1,(z + 1)) & K > (2 * z) * (Py (x1,(z + 1))) & y2 = Py (K,(z + 1)) & y3 = Py ((K * x1),(z + 1)) & ( ( 0 <= y - (y3 / y2) & y - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - y & (y3 / y2) - y < 1 / 2 ) ) )
take
Py (
(((2 * z) * (Py (x1,(z + 1)))) + 1),
(z + 1))
;
ex y3, K being Nat st
( Py (x1,(z + 1)) = Py (x1,(z + 1)) & K > (2 * z) * (Py (x1,(z + 1))) & Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)) = Py (K,(z + 1)) & y3 = Py ((K * x1),(z + 1)) & ( ( 0 <= y - (y3 / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) & y - (y3 / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) < 1 / 2 ) or ( 0 <= (y3 / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y & (y3 / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y < 1 / 2 ) ) )
take
Py (
((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),
(z + 1))
;
ex K being Nat st
( Py (x1,(z + 1)) = Py (x1,(z + 1)) & K > (2 * z) * (Py (x1,(z + 1))) & Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)) = Py (K,(z + 1)) & Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1)) = Py ((K * x1),(z + 1)) & ( ( 0 <= y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) & y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) < 1 / 2 ) or ( 0 <= ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y & ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y < 1 / 2 ) ) )
take
K
;
( Py (x1,(z + 1)) = Py (x1,(z + 1)) & K > (2 * z) * (Py (x1,(z + 1))) & Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)) = Py (K,(z + 1)) & Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1)) = Py ((K * x1),(z + 1)) & ( ( 0 <= y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) & y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) < 1 / 2 ) or ( 0 <= ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y & ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y < 1 / 2 ) ) )
x1 + (x1 - 1) > x1 + 0
by XREAL_1:6;
then A4:
(x1 + (x1 - 1)) to_power z > x1 to_power z
by A2, POWER:37;
((2 * x1) - 1) |^ z <= Py (
x1,
(z + 1))
by Th20;
then
Py (
x1,
(z + 1))
>= x1 |^ z
by A4, XXREAL_0:2;
then
K > (2 * z) * (x1 |^ z)
by NAT_1:13, XREAL_1:64;
then A5:
(
y - (1 / 2) < (Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1))) &
(Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1))) < y + (1 / 2) )
by A1, Th22;
(
y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) >= 0 or
- (y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1))))) >= - 0 )
;
hence
(
Py (
x1,
(z + 1))
= Py (
x1,
(z + 1)) &
K > (2 * z) * (Py (x1,(z + 1))) &
Py (
(((2 * z) * (Py (x1,(z + 1)))) + 1),
(z + 1))
= Py (
K,
(z + 1)) &
Py (
((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),
(z + 1))
= Py (
(K * x1),
(z + 1)) & ( (
0 <= y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) &
y - ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) < 1
/ 2 ) or (
0 <= ((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y &
((Py (((((2 * z) * (Py (x1,(z + 1)))) + 1) * x1),(z + 1))) / (Py ((((2 * z) * (Py (x1,(z + 1)))) + 1),(z + 1)))) - y < 1
/ 2 ) ) )
by NAT_1:13, XREAL_1:19, XREAL_1:11, A5;
verum
end; hence
( (
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 ) ) ) ) )
by A3, A2;
verum end; end; end; end;
end;
assume A6:
( ( 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
per cases
( ( 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 ) ) ) ) )
by A6;
suppose A7:
(
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 |^ zreconsider x1 =
x as non
trivial Nat by A7, NAT_2:28;
consider y1,
y2,
y3,
K being
Nat such that A8:
y1 = Py (
x1,
(z + 1))
and A9:
K > (2 * z) * y1
and A10:
y2 = Py (
K,
(z + 1))
and A11:
y3 = Py (
(K * x1),
(z + 1))
and A12:
( (
0 <= y - (y3 / y2) &
y - (y3 / y2) < 1
/ 2 ) or (
0 <= (y3 / y2) - y &
(y3 / y2) - y < 1
/ 2 ) )
by A7;
(2 * z) * y1 >= 1
by NAT_1:14, A8, A7;
then reconsider K =
K as non
trivial Nat by NAT_2:28, A9;
x1 + (x1 - 1) > x1 + 0
by XREAL_1:6;
then A13:
(x1 + (x1 - 1)) to_power z > x1 to_power z
by A7, POWER:37;
((2 * x1) - 1) |^ z <= y1
by A8, Th20;
then
y1 >= x1 |^ z
by A13, XXREAL_0:2;
then
y1 * (2 * z) >= (x1 |^ z) * (2 * z)
by XREAL_1:64;
then
K > (2 * z) * (x1 |^ z)
by A9, XXREAL_0:2;
then A14:
(
(x1 |^ z) - (1 / 2) < y3 / y2 &
y3 / y2 < (x1 |^ z) + (1 / 2) )
by Th22, A10, A11;
end; end;