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