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 ⊢A∈ℕ∧B∈ℕ→AAgcdB∈Odd∨BAgcdB∈Odd

Proof

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