Proof of Theorem divnumden
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
2 | | nnz 12342 |
. . . . 5
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
3 | 2 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
4 | | nnne0 12007 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
5 | 4 | neneqd 2948 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → ¬
𝐵 = 0) |
6 | 5 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
𝐵 = 0) |
7 | 6 | intnand 489 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
8 | | gcdn0cl 16209 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
9 | 1, 3, 7, 8 | syl21anc 835 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
10 | | gcddvds 16210 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
11 | 2, 10 | sylan2 593 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
12 | | gcddiv 16259 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
13 | 1, 3, 9, 11, 12 | syl31anc 1372 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
14 | 9 | nncnd 11989 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ) |
15 | 9 | nnne0d 12023 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
16 | 14, 15 | dividd 11749 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1) |
17 | 13, 16 | eqtr3d 2780 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
18 | | zcn 12324 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
19 | 18 | adantr 481 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
20 | | nncn 11981 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
21 | 20 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
22 | 4 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ≠ 0) |
23 | | divcan7 11684 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) ≠ 0)) → ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵))) = (𝐴 / 𝐵)) |
24 | 23 | eqcomd 2744 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) ≠ 0)) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
25 | 19, 21, 22, 14, 15, 24 | syl122anc 1378 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
26 | | znq 12692 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
27 | 11 | simpld 495 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
28 | | gcdcl 16213 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
29 | 28 | nn0zd 12424 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ) |
30 | 2, 29 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ) |
31 | | dvdsval2 15966 |
. . . . 5
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
32 | 30, 15, 1, 31 | syl3anc 1370 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
33 | 27, 32 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
34 | 11 | simprd 496 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
35 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℕ) |
36 | | nndivdvds 15972 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
37 | 35, 9, 36 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
38 | 34, 37 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
39 | | qnumdenbi 16448 |
. . 3
⊢ (((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) → ((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
40 | 26, 33, 38, 39 | syl3anc 1370 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
41 | 17, 25, 40 | mpbi2and 709 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵)))) |