let IT be real number ; :: thesis: ( ( a > 0 & a = 0 & b > 0 implies ( IT = a #R b iff IT = 0 ) ) & ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) )
thus ( a > 0 & a = 0 & b > 0 implies ( IT = a #R b iff IT = 0 ) ) ; :: thesis: ( ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) )
thus ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) :: thesis: ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )

proof

assume Z1: a > 0 ; :: thesis: ( not b is Integer or ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
assume b is Integer ; :: thesis: ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) )
then reconsider b = b as Integer ;
a #R b = a #Q b by Z1, PREPOWER:88
.= a #Z b by Z1, PREPOWER:113 ;
hence ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ; :: thesis: verum

end;

( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )

proof

assume Z1: a = 0 ; :: thesis: ( not b > 0 or not b is Integer or ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
assume Z2: ( b > 0 & b is Integer ) ; :: thesis: ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) )
then b in NAT by INT_1:16;
then reconsider b = b as Nat ;
a #Z b = a |^ b by PREPOWER:46
.= 0 by Z1, Z2, NAT_1:14, NEWTON:16 ;
hence ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ; :: thesis: verum

end;

hence ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) ; :: thesis: verum