Proof of Theorem divgcdoddALTV
| Step | Hyp | Ref
| Expression |
| 1 | | divgcdodd 16747 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2
∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)))) |
| 2 | | nnz 12634 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
| 3 | | nnz 12634 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
| 4 | | gcddvds 16540 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 5 | 2, 3, 4 | syl2an 596 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
| 6 | 5 | simpld 494 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
| 7 | 2, 3 | anim12i 613 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ)) |
| 8 | | nnne0 12300 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) |
| 9 | 8 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → ¬
𝐴 = 0) |
| 10 | 9 | intnanrd 489 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
| 11 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
| 12 | | gcdn0cl 16539 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 13 | 7, 11, 12 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
| 14 | 13 | nnzd 12640 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ) |
| 15 | 13 | nnne0d 12316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
| 16 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
| 17 | | dvdsval2 16293 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 18 | 14, 15, 16, 17 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 19 | 6, 18 | mpbid 232 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
| 20 | 19 | biantrurd 532 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2
∥ (𝐴 / (𝐴 gcd 𝐵)) ↔ ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))))) |
| 21 | 5 | simprd 495 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
| 22 | 3 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
| 23 | | dvdsval2 16293 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 24 | 14, 15, 22, 23 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
| 25 | 21, 24 | mpbid 232 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ) |
| 26 | 25 | biantrurd 532 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2
∥ (𝐵 / (𝐴 gcd 𝐵)) ↔ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐵 / (𝐴 gcd 𝐵))))) |
| 27 | 20, 26 | orbi12d 919 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((¬
2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) ↔ (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))) ∨ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐵 / (𝐴 gcd 𝐵)))))) |
| 28 | 1, 27 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))) ∨ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐵 / (𝐴 gcd 𝐵))))) |
| 29 | | isodd3 47639 |
. . 3
⊢ ((𝐴 / (𝐴 gcd 𝐵)) ∈ Odd ↔ ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐴 / (𝐴 gcd 𝐵)))) |
| 30 | | isodd3 47639 |
. . 3
⊢ ((𝐵 / (𝐴 gcd 𝐵)) ∈ Odd ↔ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐵 / (𝐴 gcd 𝐵)))) |
| 31 | 29, 30 | orbi12i 915 |
. 2
⊢ (((𝐴 / (𝐴 gcd 𝐵)) ∈ Odd ∨ (𝐵 / (𝐴 gcd 𝐵)) ∈ Odd ) ↔ (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))) ∨ ((𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ ¬ 2 ∥
(𝐵 / (𝐴 gcd 𝐵))))) |
| 32 | 28, 31 | sylibr 234 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) ∈ Odd ∨ (𝐵 / (𝐴 gcd 𝐵)) ∈ Odd )) |