# Metamath Proof Explorer

## Theorem divgcdodd

Description: Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014)

Ref Expression
Assertion divgcdodd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )

### Proof

Step Hyp Ref Expression
1 n2dvds1 ¬ 2 ∥ 1
2 2z 2 ∈ ℤ
3 nnz ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
4 nnz ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
5 gcddvds ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
6 3 4 5 syl2an ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
7 6 simpld ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
8 gcdnncl ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
9 8 nnzd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
10 8 nnne0d ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ≠ 0 )
11 3 adantr ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
12 dvdsval2 ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
13 9 10 11 12 syl3anc ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
14 7 13 mpbid ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
15 6 simprd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
16 4 adantl ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
17 dvdsval2 ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
18 9 10 16 17 syl3anc ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
19 15 18 mpbid ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
20 dvdsgcdb ( ( 2 ∈ ℤ ∧ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) → ( ( 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 2 ∥ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) )
21 2 14 19 20 mp3an2i ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 2 ∥ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) )
22 gcddiv ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
23 11 16 8 6 22 syl31anc ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
24 8 nncnd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
25 24 10 dividd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) / ( 𝐴 gcd 𝐵 ) ) = 1 )
26 23 25 eqtr3d ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) = 1 )
27 26 breq2d ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 2 ∥ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ 2 ∥ 1 ) )
28 27 biimpd ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 2 ∥ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) gcd ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → 2 ∥ 1 ) )
29 21 28 sylbid ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∧ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) → 2 ∥ 1 ) )
30 29 expdimp ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ( 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) → 2 ∥ 1 ) )
31 1 30 mtoi ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) → ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) )
32 31 ex ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) → ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
33 imor ( ( 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) → ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
34 32 33 sylib ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )