let p be Prime; :: thesis: for a being Element of NAT
for x being set st a <> 0 & x = p |^ (p |-count a) holds
ex b being Element of NAT st
( b = x & 1 <= b & b <= a )
let a be Element of NAT ; :: thesis: for x being set st a <> 0 & x = p |^ (p |-count a) holds
ex b being Element of NAT st
( b = x & 1 <= b & b <= a )
let x be set ; :: thesis: ( a <> 0 & x = p |^ (p |-count a) implies ex b being Element of NAT st
( b = x & 1 <= b & b <= a ) )
assume A1: a <> 0 ; :: thesis: ( not x = p |^ (p |-count a) or ex b being Element of NAT st
( b = x & 1 <= b & b <= a ) )
assume A2: x = p |^ (p |-count a) ; :: thesis: ex b being Element of NAT st
( b = x & 1 <= b & b <= a )
then reconsider b = x as Element of NAT by ORDINAL1:def 13;
take b ; :: thesis: ( b = x & 1 <= b & b <= a )
thus b = x ; :: thesis: ( 1 <= b & b <= a )
p >= 1 by INT_2:def 5;
hence 1 <= b by A2, PREPOWER:19; :: thesis: b <= a
p <> 1 by INT_2:def 5;
then b divides a by A1, A2, NAT_3:def 7;
hence b <= a by A1, NAT_D:7; :: thesis: verum