theorem :: PEPIN:29

for n being Nat holds 2 |^ (n + 1) = (2 |^ n) + (2 |^ n)