let x, y, z be Nat; :: thesis: ( 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 ) ) ) ) ) :: thesis: ( ( ( 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 ; :: thesis: ( ( 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 ; :: thesis: ( ( 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; :: thesis: verum

end;

suppose A2: z > 0 ; :: thesis: ( ( 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 ) ; :: thesis: ( ( 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; :: thesis: verum

end;

suppose A3: x > 1 ; :: thesis: ( ( 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)) ; :: thesis: 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)) ; :: thesis: 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)) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: 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 ) ) ) ) ) ; :: thesis: 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 ( y = 1 & z = 0 ) ; :: thesis: y = x |^ z

hence y = x |^ z by NEWTON:4; :: thesis: verum

end;

suppose ( x = 0 & y = 0 & z > 0 ) ; :: thesis: y = x |^ z

hence y = x |^ z by NAT_1:14, NEWTON:11; :: thesis: verum

end;

suppose ( x = 1 & y = 1 & z > 0 ) ; :: thesis: y = x |^ z

hence y = x |^ z ; :: thesis: verum

end;

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 ) ) ) ) ; :: thesis: y = x |^ z

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

per cases ( ( 0 <= y - (y3 / y2) & y - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - y & (y3 / y2) - y < 1 / 2 ) ) by A12;

suppose ( 0 <= y - (y3 / y2) & y - (y3 / y2) < 1 / 2 ) ; :: thesis: y = x |^ z

then A15: ( ((x1 |^ z) - (1 / 2)) + 0 < (y - (y3 / y2)) + (y3 / y2) & (y - (y3 / y2)) + (y3 / y2) < (1 / 2) + ((x1 |^ z) + (1 / 2)) ) by A14, XREAL_1:8;
then y < (x1 |^ z) + 1 ;
then A16: y <= x1 |^ z by INT_1:7;
(x1 |^ z) - 1 < (x1 |^ z) - (1 / 2) by XREAL_1:10;
then (x1 |^ z) - 1 < y by A15, XXREAL_0:2;
then ((x1 |^ z) - 1) + 1 <= y by INT_1:7;
hence y = x |^ z by A16, XXREAL_0:1; :: thesis: verum

end;

suppose ( 0 <= (y3 / y2) - y & (y3 / y2) - y < 1 / 2 ) ; :: thesis: y = x |^ z

then A17: ( ((x1 |^ z) - (1 / 2)) - (1 / 2) < (y3 / y2) - ((y3 / y2) - y) & (y3 / y2) - ((y3 / y2) - y) < ((x1 |^ z) + (1 / 2)) - 0 ) by A14, XREAL_1:14;
then A18: ((x1 |^ z) - 1) + 1 <= y by INT_1:7;
(x1 |^ z) + (1 / 2) < (x1 |^ z) + 1 by XREAL_1:6;
then y < (x1 |^ z) + 1 by A17, XXREAL_0:2;
then y <= x1 |^ z by INT_1:7;
hence y = x |^ z by A18, XXREAL_0:1; :: thesis: verum

end;

end;

end;

end;