let p be natural number ; :: thesis: ( p is Proth implies ( not p is trivial & p is odd ) )
assume A1: p is Proth ; :: thesis: ( not p is trivial & p is odd )
then consider k being natural odd number , n being natural positive number such that
A2: ( 2 |^ n > k & p = (k * (2 |^ n)) + 1 ) ;
thus not p is trivial by A1, NAT_2:def 1; :: thesis: p is odd
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
2 * (2 |^ n1) = 2 |^ (1 + n1) by NEWTON:6
.= 2 |^ n ;
hence p is odd by A2; :: thesis: verum