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 𝐵 ) ) ) )