let n be Nat; :: thesis: for m being non zero Nat holds
( n / m is Nat iff m divides n )
let m be non zero Nat; :: thesis: ( n / m is Nat iff m divides n )
thus ( n / m is Nat implies m divides n ) by WSIERP_1:17; :: thesis: ( m divides n implies n / m is Nat )
H: n * 1 = n * (m / m) by XCMPLX_1:60;
assume m divides n ; :: thesis: n / m is Nat
then consider x being Nat such that
A1: m * x = n by NAT_D:def 3;
m * (n / m) = m * x by A1, H;
hence n / m is Nat by XCMPLX_1:5; :: thesis: verum