# 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 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(¬2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\vee ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 n2dvds1 ${⊢}¬2\parallel 1$
2 2z ${⊢}2\in ℤ$
3 nnz ${⊢}{A}\in ℕ\to {A}\in ℤ$
4 nnz ${⊢}{B}\in ℕ\to {B}\in ℤ$
5 gcddvds ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)$
6 3 4 5 syl2an ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)$
7 6 simpld ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left({A}\mathrm{gcd}{B}\right)\parallel {A}$
8 gcdnncl ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}\mathrm{gcd}{B}\in ℕ$
9 8 nnzd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}\mathrm{gcd}{B}\in ℤ$
10 8 nnne0d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}\mathrm{gcd}{B}\ne 0$
11 3 adantr ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}\in ℤ$
12 dvdsval2 ${⊢}\left({A}\mathrm{gcd}{B}\in ℤ\wedge {A}\mathrm{gcd}{B}\ne 0\wedge {A}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}↔\frac{{A}}{{A}\mathrm{gcd}{B}}\in ℤ\right)$
13 9 10 11 12 syl3anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}↔\frac{{A}}{{A}\mathrm{gcd}{B}}\in ℤ\right)$
14 7 13 mpbid ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \frac{{A}}{{A}\mathrm{gcd}{B}}\in ℤ$
15 6 simprd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left({A}\mathrm{gcd}{B}\right)\parallel {B}$
16 4 adantl ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {B}\in ℤ$
17 dvdsval2 ${⊢}\left({A}\mathrm{gcd}{B}\in ℤ\wedge {A}\mathrm{gcd}{B}\ne 0\wedge {B}\in ℤ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {B}↔\frac{{B}}{{A}\mathrm{gcd}{B}}\in ℤ\right)$
18 9 10 16 17 syl3anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\left({A}\mathrm{gcd}{B}\right)\parallel {B}↔\frac{{B}}{{A}\mathrm{gcd}{B}}\in ℤ\right)$
19 15 18 mpbid ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \frac{{B}}{{A}\mathrm{gcd}{B}}\in ℤ$
20 dvdsgcdb ${⊢}\left(2\in ℤ\wedge \frac{{A}}{{A}\mathrm{gcd}{B}}\in ℤ\wedge \frac{{B}}{{A}\mathrm{gcd}{B}}\in ℤ\right)\to \left(\left(2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\wedge 2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)↔2\parallel \left(\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)\right)$
21 2 14 19 20 mp3an2i ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\left(2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\wedge 2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)↔2\parallel \left(\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)\right)$
22 gcddiv ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {A}\mathrm{gcd}{B}\in ℕ\right)\wedge \left(\left({A}\mathrm{gcd}{B}\right)\parallel {A}\wedge \left({A}\mathrm{gcd}{B}\right)\parallel {B}\right)\right)\to \frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)$
23 11 16 8 6 22 syl31anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)$
24 8 nncnd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}\mathrm{gcd}{B}\in ℂ$
25 24 10 dividd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \frac{{A}\mathrm{gcd}{B}}{{A}\mathrm{gcd}{B}}=1$
26 23 25 eqtr3d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)=1$
27 26 breq2d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(2\parallel \left(\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)↔2\parallel 1\right)$
28 27 biimpd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(2\parallel \left(\left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\mathrm{gcd}\left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)\to 2\parallel 1\right)$
29 21 28 sylbid ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(\left(2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\wedge 2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)\to 2\parallel 1\right)$
30 29 expdimp ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge 2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\right)\to \left(2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\to 2\parallel 1\right)$
31 1 30 mtoi ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\right)\wedge 2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\right)\to ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)$
32 31 ex ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\to ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)$
33 imor ${⊢}\left(2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\to ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)↔\left(¬2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\vee ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)$
34 32 33 sylib ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to \left(¬2\parallel \left(\frac{{A}}{{A}\mathrm{gcd}{B}}\right)\vee ¬2\parallel \left(\frac{{B}}{{A}\mathrm{gcd}{B}}\right)\right)$