let n be even Nat; :: thesis: ( card (PrimeDivisors n) = 1 implies ex k being Nat st n = 2 |^ k )
assume A0: card (PrimeDivisors n) = 1 ; :: thesis: ex k being Nat st n = 2 |^ k
n <> 0

proof

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

end;

then consider j, i being Nat such that
c1: ( i is odd & j > 0 & n = (2 |^ j) * i ) by NAT_5:2;
A9: 2 is Prime by XPRIMES1:2;
2 divides n by ABIAN:def 1;
then A8: 2 in PrimeDivisors n by A9;
consider x being object such that
A2: PrimeDivisors n = {x} by A0, CARD_2:42;
x in PrimeDivisors n by A2, TARSKI:def 1;
then consider k being Prime such that
A3: ( x = k & k divides n ) ;

per cases ( k divides 2 |^ j or k divides i ) by c1, A3, NAT_6:7;

suppose k divides 2 |^ j ; :: thesis: ex k being Nat st n = 2 |^ k

then k = 2 by A9, NAT_3:6;
then S1: PrimeDivisors n = {2} by A2, A3;
S2: i divides n by c1;
EE: ( i = 1 implies ex k being Nat st n = 2 |^ k )

proof

assume i = 1 ; :: thesis: ex k being Nat st n = 2 |^ k
hence ex k being Nat st n = 2 |^ k by c1; :: thesis: verum

end;

per cases ( i is Prime or ( i is not Prime & i <> 1 ) or ( i is not Prime & i = 1 ) ) ;

suppose i is Prime ; :: thesis: ex k being Nat st n = 2 |^ k

then i in PrimeDivisors n by S2;
then i = 2 * 1 by S1, TARSKI:def 1;
hence ex k being Nat st n = 2 |^ k by c1; :: thesis: verum

end;

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

then consider p being Prime such that
D2: ( p divides i & p <> i ) by MOEBIUS1:4;
p divides n by D2, S2, NAT_D:4;
then p in { k where k is Prime : k divides n } ;
then 2 divides i by S1, D2, TARSKI:def 1;
hence ex k being Nat st n = 2 |^ k by c1; :: thesis: verum

end;

suppose ( i is not Prime & i = 1 ) ; :: thesis: ex k being Nat st n = 2 |^ k

hence ex k being Nat st n = 2 |^ k by EE; :: thesis: verum

end;

end;

end;

suppose S1: k divides i ; :: thesis: ex k being Nat st n = 2 |^ k

E3: i divides n by c1;
E4: ( i is odd & k is Prime ) by c1;
E2: i <> 1

proof

assume i = 1 ; :: thesis: contradiction
then k = 1 by S1, WSIERP_1:15;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

i is not Prime

proof

assume i is Prime ; :: thesis: contradiction
then i in PrimeDivisors n by E3;
then i = k by A2, A3, TARSKI:def 1;
then E5: k is odd by E4;
set l = k |-count n;
( k |-count n >= 1 & n = k |^ (k |-count n) ) by A3, A2, OnlyOddPrimeX;
hence contradiction by E5; :: thesis: verum

end;

then consider p being Prime such that
D2: ( p divides i & p <> i ) by E2, MOEBIUS1:4;
d4: p is odd by D2, E4;
d3: k = 2 * 1 by A2, A8, A3, TARSKI:def 1;
p divides n by D2, E3, NAT_D:4;
then p in { k where k is Prime : k divides n } ;
hence ex k being Nat st n = 2 |^ k by A2, A3, d3, d4, TARSKI:def 1; :: thesis: verum

end;

end;