let k, m, n be Nat; ( k >= 1 & m = (2 |^ k) - 2 & n = (2 |^ k) * ((2 |^ k) - 2) implies ( PrimeDivisors m = PrimeDivisors n & PrimeDivisors (m + 1) = PrimeDivisors (n + 1) ) )
assume A1:
( k >= 1 & m = (2 |^ k) - 2 & n = (2 |^ k) * ((2 |^ k) - 2) )
; ( PrimeDivisors m = PrimeDivisors n & PrimeDivisors (m + 1) = PrimeDivisors (n + 1) )
A2: PrimeDivisors (n + 1) =
PrimeDivisors ((2 |^ k) - 1)
by P136c, A1
.=
PrimeDivisors (m + 1)
by A1
;
PrimeDivisors m =
{2} \/ (PrimeDivisors ((2 |^ (k -' 1)) - 1))
by A1, P136b
.=
PrimeDivisors n
by P136a, A1
;
hence
( PrimeDivisors m = PrimeDivisors n & PrimeDivisors (m + 1) = PrimeDivisors (n + 1) )
by A2; verum