let n be even Nat; :: thesis: ( card (PrimeDivisors n) = 1 implies ex k being Nat st
( k >= 1 & n = 2 |^ k ) )
assume card (PrimeDivisors n) = 1 ; :: thesis: ex k being Nat st
( k >= 1 & n = 2 |^ k )
then consider x being object such that
A2: PrimeDivisors n = {x} by CARD_2:42;
x in PrimeDivisors n by A2, TARSKI:def 1;
then consider p being Prime such that
A3: ( x = p & p divides n ) ;
Z1: PrimeDivisors n = {p} by A2, A3;
set k = p |-count n;
set a = p |^ (p |-count n);
n <> 0

proof

assume n = 0 ; :: thesis: contradiction
hence contradiction by Z1, PrimeSet0; :: thesis: verum

end;

then reconsider nn = n as non zero Nat ;
consider s, t being Nat such that
C1: ( t is odd & s > 0 & nn = (2 |^ s) * t ) by NAT_5:2;
II: 2 is Prime by XPRIMES1:2;
C2: 2 divides 2 |^ s by C1, NAT_3:3;
2 |^ s divides nn by C1;
then 2 divides nn by C2, NAT_D:4;
then 2 in PrimeDivisors n by II;
then G1: x = 2 by A2, TARSKI:def 1;
D4: t divides nn by C1;

per cases ( t = 1 or t <> 1 ) ;

suppose E1: t = 1 ; :: thesis: ex k being Nat st
( k >= 1 & n = 2 |^ k )

IK: s >= 0 + 1 by C1, NAT_1:13;
( t = 1 implies ex k being Nat st
( k >= 1 & n = 2 |^ k ) )

proof

assume t = 1 ; :: thesis: ex k being Nat st
( k >= 1 & n = 2 |^ k )
hence ex k being Nat st
( k >= 1 & n = 2 |^ k ) by IK, C1; :: thesis: verum

end;

hence ex k being Nat st
( k >= 1 & n = 2 |^ k ) by E1; :: thesis: verum

end;

suppose t <> 1 ; :: thesis: ex k being Nat st
( k >= 1 & n = 2 |^ k )

then consider q being Prime such that
D2: q divides t by MOEBIUS1:5;
consider m being Nat such that
D3: t = q * m by D2, NAT_D:def 3;
q divides nn by D2, D4, NAT_D:4;
then q in {2} by A2, G1;
then q = 2 * 1 by TARSKI:def 1;
hence ex k being Nat st
( k >= 1 & n = 2 |^ k ) by C1, D3; :: thesis: verum

end;

end;