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 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 A2: b is Integer ; :: thesis: ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) )
reconsider b = b as Integer by A2;
A3: a #R b = a #Q b by A1, PREPOWER:88
.= a #Z b by A1, PREPOWER:113 ;
thus ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) by A3; :: thesis: verum

end;

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

proof

assume A5: 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
A6: b > 0 and
A7: b is Integer ; :: thesis: ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) )
A8: b in NAT by A6, A7, INT_1:16;
reconsider b = b as Nat by A8;
A9: a #Z b = a |^ b by PREPOWER:46
.= 0 by A5, A6, NAT_1:14, NEWTON:16 ;
thus ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) by A9; :: thesis: verum

end;

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