let k be Nat; :: thesis: not (4 * k) + 2 is perfect_power
a5: 2 * ((2 * k) + 1) is even ;
assume (4 * k) + 2 is perfect_power ; :: thesis: contradiction
then A2: 4 divides (4 * k) + 2 by a5, FourPerfectPower;
4 divides 4 * k ;
then 4 divides ((4 * k) + 2) - (4 * k) by A2, PREPOWER:94;
hence contradiction by INT_2:28; :: thesis: verum