let IT be Real; :: 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 A1: 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 A1, PREPOWER:74
.= a #Z b by A1, PREPOWER:99 ;
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 A2: 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 that
A3: b > 0 and
A4: b is Integer ; :: thesis: ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) )
b in NAT by A3, A4, INT_1:3;
then reconsider b = b as Nat ;
a #Z b = a |^ b by PREPOWER:36
.= 0 by A2, A3, NAT_1:14, NEWTON:11 ;
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