let n, k, m be natural number ; :: thesis: ( n = 2 |^ k & not m is even implies n,m are_relative_prime )
assume A1: n = 2 |^ k ; :: thesis: ( m is even or n,m are_relative_prime )
assume A2: not m is even ; :: thesis: n,m are_relative_prime
then reconsider h = n gcd m as non zero natural number by INT_2:5;
for p being Element of NAT st p is prime holds
p |-count h = p |-count 1

proof

reconsider n9 = n, m9 = m as non zero natural number by A1, A2;
let p be Element of NAT ; :: thesis: ( p is prime implies p |-count h = p |-count 1 )
assume A3: p is prime ; :: thesis: p |-count h = p |-count 1
A4: min (p |-count n),(p |-count m) = 0

proof

per cases ( p = 2 or p <> 2 ) ;

suppose A5: p = 2 ; :: thesis: min (p |-count n),(p |-count m) = 0

not p divides m

proof

assume p divides m ; :: thesis: contradiction
then consider m9 being natural number such that
A6: m = p * m9 by NAT_D:def 3;
thus contradiction by A2, A5, A6; :: thesis: verum
reconsider m9 = m9 as Element of NAT by ORDINAL1:def 13;

end;

then p |-count m = 0 by A5, NAT_3:27;
hence min (p |-count n),(p |-count m) = 0 by XXREAL_0:def 9; :: thesis: verum

end;

suppose A7: p <> 2 ; :: thesis: min (p |-count n),(p |-count m) = 0

p <> 1 by A3, INT_2:def 5;
then A8: p |-count 2 = 0 by A7, INT_2:44, NAT_3:24;
p |-count n = k * (p |-count 2) by A1, A3, NAT_3:32
.= k * 0 by A8 ;
hence min (p |-count n),(p |-count m) = 0 by XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

( p > 1 & p |-count (n9 gcd m9) = min (p |-count n9),(p |-count m9) ) by A3, Lm1, INT_2:def 5;
hence p |-count h = p |-count 1 by A4, NAT_3:21; :: thesis: verum

end;

then n gcd m = 1 by NAT_4:21;
hence n,m are_relative_prime by INT_2:def 4; :: thesis: verum