:: deftheorem Def5 defines Proth NAT_6:def 5 :
for p being natural number holds
( p is Proth iff ex k being natural odd number ex n being natural positive number st
( 2 |^ n > k & p = (k * (2 |^ n)) + 1 ) );