let k be Nat; :: thesis: ( k >= 1 implies PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1)) )
assume A1: k >= 1 ; :: thesis: PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))
then 2 |^ k >= 2 by PREPOWER:12;
then (2 |^ k) - 2 >= 2 - 2 by XREAL_1:13;
then (2 |^ k) - 2 >= 0 ;
then PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = (PrimeDivisors (2 |^ k)) \/ (PrimeDivisors ((2 |^ k) - 2)) by DivisorsMulti
.= {2} \/ (PrimeDivisors ((2 |^ k) - 2)) by A1, DivK, XPRIMES1:2
.= {2} \/ (PrimeDivisors ((2 |^ ((k -' 1) + 1)) - 2)) by XREAL_1:235, A1
.= {2} \/ (PrimeDivisors (((2 |^ (k -' 1)) * 2) - 2)) by NEWTON:6
.= {2} \/ (PrimeDivisors (2 * ((2 |^ (k -' 1)) - 1)))
.= {2} \/ ((PrimeDivisors 2) \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))) by DivisorsMulti
.= {2} \/ ({2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))) by LemmaOne, XPRIMES1:2
.= ({2} \/ {2}) \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1)) by XBOOLE_1:4
.= {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1)) ;
hence PrimeDivisors ((2 |^ k) * ((2 |^ k) - 2)) = {2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1)) ; :: thesis: verum