Proof of Theorem divnumden
Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℤ) |
2 | | nnz 8925 |
. . . . 5
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
3 | 2 | adantl 273 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℤ) |
4 | | nnne0 8606 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
5 | 4 | neneqd 2288 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → ¬
𝐵 = 0) |
6 | 5 | adantl 273 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
𝐵 = 0) |
7 | 6 | intnand 884 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ¬
(𝐴 = 0 ∧ 𝐵 = 0)) |
8 | | gcdn0cl 11446 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴 gcd 𝐵) ∈ ℕ) |
9 | 1, 3, 7, 8 | syl21anc 1183 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
10 | | gcddvds 11447 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
11 | 2, 10 | sylan2 282 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
12 | | gcddiv 11500 |
. . . 4
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) ∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
13 | 1, 3, 9, 11, 12 | syl31anc 1187 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵)))) |
14 | 9 | nncnd 8592 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℂ) |
15 | 9 | nnap0d 8624 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) # 0) |
16 | 14, 15 | dividapd 8407 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) / (𝐴 gcd 𝐵)) = 1) |
17 | 13, 16 | eqtr3d 2134 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1) |
18 | | zcn 8911 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
19 | 18 | adantr 272 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐴 ∈
ℂ) |
20 | | nncn 8586 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
21 | 20 | adantl 273 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
22 | | simpr 109 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℕ) |
23 | 22 | nnap0d 8624 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → 𝐵 # 0) |
24 | | divcanap7 8342 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵))) = (𝐴 / 𝐵)) |
25 | 24 | eqcomd 2105 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ ((𝐴 gcd 𝐵) ∈ ℂ ∧ (𝐴 gcd 𝐵) # 0)) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
26 | 19, 21, 23, 14, 15, 25 | syl122anc 1193 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) |
27 | | znq 9266 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / 𝐵) ∈ ℚ) |
28 | 11 | simpld 111 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐴) |
29 | | gcdcl 11450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈
ℕ0) |
30 | 29 | nn0zd 9023 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 gcd 𝐵) ∈ ℤ) |
31 | 2, 30 | sylan2 282 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℤ) |
32 | 9 | nnne0d 8623 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ≠ 0) |
33 | | dvdsval2 11291 |
. . . . 5
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ (𝐴 gcd 𝐵) ≠ 0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
34 | 31, 32, 1, 33 | syl3anc 1184 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ)) |
35 | 28, 34 | mpbid 146 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
36 | 11 | simprd 113 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∥ 𝐵) |
37 | | nndivdvds 11294 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
38 | 22, 9, 37 | syl2anc 406 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)) |
39 | 36, 38 | mpbid 146 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) |
40 | | qnumdenbi 11662 |
. . 3
⊢ (((𝐴 / 𝐵) ∈ ℚ ∧ (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ) → ((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
41 | 27, 35, 39, 40 | syl3anc 1184 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (𝐴 / 𝐵) = ((𝐴 / (𝐴 gcd 𝐵)) / (𝐵 / (𝐴 gcd 𝐵)))) ↔ ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))) |
42 | 17, 26, 41 | mpbi2and 895 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) →
((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵)))) |