let k, n, m be Nat; :: thesis: ( n = 2 |^ k & m is odd implies n,m are_coprime )
assume A1: n = 2 |^ k ; :: thesis: ( not m is odd or n,m are_coprime )
assume A2: m is odd ; :: thesis: n,m are_coprime
then reconsider h = n gcd m as non zero Nat 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 Nat 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 Nat such that
A6: m = p * m9 by NAT_D:def 3;
thus contradiction by A2, A5, A6; :: thesis: verum

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 4;
then A8: p |-count 2 = 0 by A7, INT_2:28, 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 4;
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_coprime by INT_2:def 3; :: thesis: verum