let a, b, e be Nat; :: thesis: ( e > 0 & a |^ e divides b |^ e implies a divides b )
assume that
A1: e > 0 and
A2: a |^ e divides b |^ e ; :: thesis: a divides b
consider f being Nat such that
A3: (a |^ e) * f = b |^ e by A2, NAT_D:def 3;
A4: now :: thesis: ( a <> 0 & b <> 0 implies a divides b )
assume that
A5: a <> 0 and
b <> 0 ; :: thesis: a divides b
a |^ e <> 0 by A5, CARD_4:3;
then f = (b |^ e) / (a |^ e) by A3, XCMPLX_1:89
.= (b / a) |^ e by PREPOWER:8 ;
then consider d being Nat such that
A6: f = d |^ e by Th25;
b |^ e = (a * d) |^ e by A3, A6, NEWTON:7;
then b = a * d by A1, Th3;
hence a divides b ; :: thesis: verum
end;
A7: now :: thesis: ( a = 0 implies a divides b )
assume A8: a = 0 ; :: thesis: a divides b
then 0 divides b |^ e by A1, A2, NAT_1:14, NEWTON:11;
then ex f being Nat st 0 * f = b |^ e by NAT_D:def 3;
hence a divides b by A8, CARD_4:3; :: thesis: verum
end;
now :: thesis: ( b = 0 implies a divides b )
assume b = 0 ; :: thesis: a divides b
then a * 0 = b ;
hence a divides b ; :: thesis: verum
end;
hence a divides b by A7, A4; :: thesis: verum