let a be Nat; :: thesis: for n being prime Nat holds
( n divides a iff n divides a |^ n )
let n be prime Nat; :: thesis: ( n divides a iff n divides a |^ n )
a divides a |^ n by NAT_3:3;
hence ( n divides a iff n divides a |^ n ) by NAT_D:4, NAT_3:5; :: thesis: verum