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

Proof

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