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

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
then A4: p > 1 by INT_2:def 5;
reconsider n' = n, m' = m as non zero natural number by A2, A1;
A5: p |-count (n' gcd m') = min (p |-count n'),(p |-count m') by A3, Lm1;
min (p |-count n),(p |-count m) = 0

proof

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

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

not p divides m

proof

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

end;

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

end;

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

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

end;

end;

end;

hence p |-count h = p |-count 1 by A4, A5, 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