Metamath Proof Explorer

Theorem divgcdoddALTV

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

Ref Expression
Assertion divgcdoddALTV ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ∨ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ) )

Proof

Step Hyp Ref Expression
1 divgcdodd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
2 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
3 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
4 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
5 2 3 4 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
6 5 simpld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
7 2 3 anim12i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
8 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
9 8 neneqd ⊢ ( 𝐴 ∈ ℕ → ¬ 𝐴 = 0 )
10 9 intnanrd ⊢ ( 𝐴 ∈ ℕ → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
11 10 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
12 gcdn0cl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
13 7 11 12 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
14 13 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
15 13 nnne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ≠ 0 )
16 2 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
17 dvdsval2 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
18 14 15 16 17 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ↔ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
19 6 18 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
20 19 biantrurd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ↔ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ) )
21 5 simprd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
22 3 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
23 dvdsval2 ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
24 14 15 22 23 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ↔ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ) )
25 21 24 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ )
26 25 biantrurd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ↔ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) )
27 20 26 orbi12d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∨ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ↔ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∨ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) ) )
28 1 27 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∨ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) )
29 isodd3 ⊢ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ↔ ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) )
30 isodd3 ⊢ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ↔ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) )
31 29 30 orbi12i ⊢ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ∨ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ) ↔ ( ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ) ∨ ( ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ ℤ ∧ ¬ 2 ∥ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ) ) )
32 28 31 sylibr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ∨ ( 𝐵 / ( 𝐴 gcd 𝐵 ) ) ∈ Odd ) )