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

hence n,m are_coprime by INT_2:def 3; :: thesis: verum

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

then
n gcd m = 1
by NAT_4:21;
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

hence p |-count h = p |-count 1 by A4, NAT_3:21; :: thesis: verum

end;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
end;

( p > 1 & p |-count (n9 gcd m9) = min ((p |-count n9),(p |-count m9)) )
by A3, Lm1, INT_2:def 4;per cases
( p = 2 or p <> 2 )
;

end;

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

not p divides m

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

end;proof

then
p |-count m = 0
by A5, NAT_3:27;
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 consider m9 being Nat such that

A6: m = p * m9 by NAT_D:def 3;

thus contradiction by A2, A5, A6; :: thesis: verum

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

hence p |-count h = p |-count 1 by A4, NAT_3:21; :: thesis: verum

hence n,m are_coprime by INT_2:def 3; :: thesis: verum