let n be non zero Nat; :: thesis: for k, t being Nat st k >= 1 & n = ((2 |^ k) * t) + (2 |^ (k -' 1)) holds
k divides card (NatDivisors n)
let k, t be Nat; :: thesis: ( k >= 1 & n = ((2 |^ k) * t) + (2 |^ (k -' 1)) implies k divides card (NatDivisors n) )
assume k >= 1 ; :: thesis: ( not n = ((2 |^ k) * t) + (2 |^ (k -' 1)) or k divides card (NatDivisors n) )

per cases then ( k = 1 or k > 1 ) by XXREAL_0:1;

suppose k = 1 ; :: thesis: ( not n = ((2 |^ k) * t) + (2 |^ (k -' 1)) or k divides card (NatDivisors n) )

then k divides card (NatDivisors n) by NAT_D:6;
hence ( not n = ((2 |^ k) * t) + (2 |^ (k -' 1)) or k divides card (NatDivisors n) ) ; :: thesis: verum

end;

suppose SY: k > 1 ; :: thesis: ( not n = ((2 |^ k) * t) + (2 |^ (k -' 1)) or k divides card (NatDivisors n) )

then A0: (k -' 1) + 1 = k by XREAL_1:235;
assume n = ((2 |^ k) * t) + (2 |^ (k -' 1)) ; :: thesis: k divides card (NatDivisors n)
then A3: n = (((2 |^ (k -' 1)) * 2) * t) + (2 |^ (k -' 1)) by A0, NEWTON:6
.= (2 |^ (k -' 1)) * ((2 * t) + 1) ;
A2: 2 |^ (k -' 1),(2 * t) + 1 are_coprime by NAT_5:3;
PP: #divs n = card (NatDivisors n) by ThDivs;
P0: #divs (2 |^ (k -' 1)) = k by A0, Cosik1;
#divs n = (#divs ((2 * t) + 1)) * (#divs (2 |^ (k -' 1))) by A2, A3, DivsMulti;
hence k divides card (NatDivisors n) by PP, P0; :: thesis: verum

end;

end;