Proof of Theorem divgcdodd
Step | Hyp | Ref
| Expression |
1 | | n2dvds1 14942 |
. . . 4
⊢ ¬ 2
∥ 1 |
2 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
3 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
4 | | gcddvds 15063 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
5 | 2, 3, 4 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
6 | 5 | simpld 474 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
7 | 2, 3 | anim12i 588 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ)) |
8 | | nnne0 10930 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) |
9 | 8 | neneqd 2787 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → ¬
𝐴 = 0) |
10 | 9 | intnanrd 954 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
12 | | gcdn0cl 15062 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
13 | 7, 11, 12 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
14 | 13 | nnzd 11357 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ) |
15 | 13 | nnne0d 10942 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
16 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
17 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
18 | 14, 15, 16, 17 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
19 | 6, 18 | mpbid 221 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
20 | 5 | simprd 478 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
21 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
22 | | dvdsval2 14824 |
. . . . . . . . 9
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
23 | 14, 15, 21, 22 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
24 | 20, 23 | mpbid 221 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ) |
25 | | 2z 11286 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
26 | | dvdsgcdb 15100 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ (𝐴 /
(𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ) → ((2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∧ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) ↔ 2 ∥ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))) |
27 | 25, 26 | mp3an1 1403 |
. . . . . . 7
⊢ (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℤ) → ((2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∧ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) ↔ 2 ∥ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))) |
28 | 19, 24, 27 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((2
∥ (𝐴 / (𝐴 gcd 𝐵)) ∧ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) ↔ 2 ∥ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))) |
29 | | gcddiv 15106 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
30 | 16, 21, 13, 5, 29 | syl31anc 1321 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
31 | 13 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ) |
32 | 31, 15 | dividd 10678 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1) |
33 | 30, 32 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
34 | 33 | breq2d 4595 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (2
∥ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) ↔ 2 ∥ 1)) |
35 | 34 | biimpd 218 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (2
∥ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) → 2 ∥ 1)) |
36 | 28, 35 | sylbid 229 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((2
∥ (𝐴 / (𝐴 gcd 𝐵)) ∧ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) → 2 ∥ 1)) |
37 | 36 | expdimp 452 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))) → (2 ∥ (𝐵 / (𝐴 gcd 𝐵)) → 2 ∥ 1)) |
38 | 1, 37 | mtoi 189 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 2 ∥
(𝐴 / (𝐴 gcd 𝐵))) → ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) |
39 | 38 | ex 449 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (2
∥ (𝐴 / (𝐴 gcd 𝐵)) → ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)))) |
40 | | imor 427 |
. 2
⊢ ((2
∥ (𝐴 / (𝐴 gcd 𝐵)) → ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))) ↔ (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)))) |
41 | 39, 40 | sylib 207 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2
∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)))) |