Proof of Theorem divnumden
Step | Hyp | Ref
| Expression |
1 | | simpl 107 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
2 | | nnz 8665 |
. . . . 5
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
3 | 2 | adantl 271 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
4 | | nnne0 8344 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
5 | 4 | neneqd 2270 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → ¬
𝐵 = 0) |
6 | 5 | adantl 271 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
𝐵 = 0) |
7 | 6 | intnand 874 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
8 | | gcdn0cl 10734 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
9 | 1, 3, 7, 8 | syl21anc 1169 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
10 | | gcddvds 10735 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
11 | 2, 10 | sylan2 280 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
12 | | gcddiv 10788 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
13 | 1, 3, 9, 11, 12 | syl31anc 1173 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
14 | 9 | nncnd 8330 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ) |
15 | 9 | nnap0d 8361 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) # 0) |
16 | 14, 15 | dividapd 8151 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1) |
17 | 13, 16 | eqtr3d 2117 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
18 | | zcn 8651 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
19 | 18 | adantr 270 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
20 | | nncn 8324 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
21 | 20 | adantl 271 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
22 | | simpr 108 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℕ) |
23 | 22 | nnap0d 8361 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 # 0) |
24 | | divcanap7 8086 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵))) = (𝐴 / 𝐵)) |
25 | 24 | eqcomd 2088 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
26 | 19, 21, 23, 14, 15, 25 | syl122anc 1179 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
27 | | znq 9004 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
28 | 11 | simpld 110 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
29 | | gcdcl 10738 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
30 | 29 | nn0zd 8762 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ) |
31 | 2, 30 | sylan2 280 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ) |
32 | 9 | nnne0d 8360 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
33 | | dvdsval2 10579 |
. . . . 5
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
34 | 31, 32, 1, 33 | syl3anc 1170 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
35 | 28, 34 | mpbid 145 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
36 | 11 | simprd 112 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
37 | | nndivdvds 10582 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
38 | 22, 9, 37 | syl2anc 403 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
39 | 36, 38 | mpbid 145 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
40 | | qnumdenbi 10950 |
. . 3
⊢ (((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) → ((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
41 | 27, 35, 39, 40 | syl3anc 1170 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
42 | 17, 26, 41 | mpbi2and 885 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵)))) |