let n, p be Nat; :: thesis: ( p is prime implies NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } )

assume A1: p is prime ; :: thesis: NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }

for x being object holds

( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

assume A1: p is prime ; :: thesis: NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }

for x being object holds

( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

proof

hence
NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in NatDivisors (p |^ n) iff x in { (p |^ k) where k is Element of NAT : k <= n } )

then A3: ex t being Element of NAT st

( x = p |^ t & t <= n ) ;

then reconsider x9 = x as Nat ;

x9 divides p |^ n by A3, NEWTON:89;

hence x in NatDivisors (p |^ n) by A1, A3, MOEBIUS1:39; :: thesis: verum

end;hereby :: thesis: ( x in { (p |^ k) where k is Element of NAT : k <= n } implies x in NatDivisors (p |^ n) )

assume
x in { (p |^ k) where k is Element of NAT : k <= n }
; :: thesis: x in NatDivisors (p |^ n)assume A2:
x in NatDivisors (p |^ n)
; :: thesis: x in { (p |^ k) where k is Element of NAT : k <= n }

then reconsider x9 = x as Nat ;

x9 divides p |^ n by A2, MOEBIUS1:39;

then ex t being Element of NAT st

( x9 = p |^ t & t <= n ) by A1, PEPIN:34;

hence x in { (p |^ k) where k is Element of NAT : k <= n } ; :: thesis: verum

end;then reconsider x9 = x as Nat ;

x9 divides p |^ n by A2, MOEBIUS1:39;

then ex t being Element of NAT st

( x9 = p |^ t & t <= n ) by A1, PEPIN:34;

hence x in { (p |^ k) where k is Element of NAT : k <= n } ; :: thesis: verum

then A3: ex t being Element of NAT st

( x = p |^ t & t <= n ) ;

then reconsider x9 = x as Nat ;

x9 divides p |^ n by A3, NEWTON:89;

hence x in NatDivisors (p |^ n) by A1, A3, MOEBIUS1:39; :: thesis: verum