Proof of Theorem qqhval2lem
Step | Hyp | Ref
| Expression |
1 | | drngring 18577 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
2 | | qqhval2.2 |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑅) |
3 | 2 | zrhrhm 19679 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
5 | 4 | ad2antrr 758 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
6 | | simpr1 1060 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℤ) |
7 | | simpr2 1061 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℤ) |
8 | 6, 7 | gcdcld 15068 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈
ℕ0) |
9 | 8 | nn0zd 11356 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℤ) |
10 | | simpr3 1062 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ≠ 0) |
11 | | gcdeq0 15076 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 ↔ (𝑋 = 0 ∧ 𝑌 = 0))) |
12 | 11 | simplbda 652 |
. . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) = 0) → 𝑌 = 0) |
13 | 12 | ex 449 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 → 𝑌 = 0)) |
14 | 13 | necon3d 2803 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 ≠ 0 → (𝑋 gcd 𝑌) ≠ 0)) |
15 | 14 | imp 444 |
. . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑌 ≠ 0) → (𝑋 gcd 𝑌) ≠ 0) |
16 | 6, 7, 10, 15 | syl21anc 1317 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ≠ 0) |
17 | | gcddvds 15063 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) |
18 | 6, 7, 17 | syl2anc 691 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) |
19 | 18 | simpld 474 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑋) |
20 | | dvdsval2 14824 |
. . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ↔ (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ)) |
21 | 20 | biimpa 500 |
. . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑋) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
22 | 9, 16, 6, 19, 21 | syl31anc 1321 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
23 | 18 | simprd 478 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑌) |
24 | | dvdsval2 14824 |
. . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑌 ↔ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ)) |
25 | 24 | biimpa 500 |
. . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑌) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
26 | 9, 16, 7, 23, 25 | syl31anc 1321 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
27 | | zringbas 19643 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
28 | | qqhval2.0 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
29 | 27, 28 | rhmf 18549 |
. . . . . 6
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶𝐵) |
30 | 5, 29 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿:ℤ⟶𝐵) |
31 | 30, 26 | ffvelrnd 6268 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵) |
32 | | ffn 5958 |
. . . . . 6
⊢ (𝐿:ℤ⟶𝐵 → 𝐿 Fn ℤ) |
33 | 30, 32 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿 Fn ℤ) |
34 | 7 | zcnd 11359 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℂ) |
35 | 9 | zcnd 11359 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℂ) |
36 | 34, 35, 10, 16 | divne0d 10696 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) |
37 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑌 / (𝑋 gcd 𝑌)) ∈ V |
38 | 37 | elsn 4140 |
. . . . . . . 8
⊢ ((𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) = 0) |
39 | 38 | necon3bbii 2829 |
. . . . . . 7
⊢ (¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) |
40 | 36, 39 | sylibr 223 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0}) |
41 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑅 ∈ Ring) |
42 | | simplr 788 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) →
(chr‘𝑅) =
0) |
43 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
44 | 28, 2, 43 | zrhker 29349 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((chr‘𝑅) = 0 ↔
(◡𝐿 “ {(0g‘𝑅)}) = {0})) |
45 | 44 | biimpa 500 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) |
46 | 41, 42, 45 | syl2anc 691 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (◡𝐿 “ {(0g‘𝑅)}) = {0}) |
47 | 40, 46 | neleqtrrd 2710 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) |
48 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}))) |
49 | 48 | baibd 946 |
. . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)})) |
50 | 49 | biimprd 237 |
. . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} → (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}))) |
51 | 50 | con3dimp 456 |
. . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}) |
52 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ V |
53 | 52 | elsn 4140 |
. . . . . . 7
⊢ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (0g‘𝑅)) |
54 | 53 | necon3bbii 2829 |
. . . . . 6
⊢ (¬
(𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
55 | 51, 54 | sylib 207 |
. . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
56 | 33, 26, 47, 55 | syl21anc 1317 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
57 | | eqid 2610 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
58 | 28, 57, 43 | drngunit 18575 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵 ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)))) |
59 | 58 | ad2antrr 758 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵 ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)))) |
60 | 31, 56, 59 | mpbir2and 959 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅)) |
61 | 30, 9 | ffvelrnd 6268 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵) |
62 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑋 gcd 𝑌) ∈ V |
63 | 62 | elsn 4140 |
. . . . . . . 8
⊢ ((𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) = 0) |
64 | 63 | necon3bbii 2829 |
. . . . . . 7
⊢ (¬
(𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) ≠ 0) |
65 | 16, 64 | sylibr 223 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ {0}) |
66 | 65, 46 | neleqtrrd 2710 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) |
67 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}))) |
68 | 67 | baibd 946 |
. . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)})) |
69 | 68 | biimprd 237 |
. . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} → (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}))) |
70 | 69 | con3dimp 456 |
. . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}) |
71 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐿‘(𝑋 gcd 𝑌)) ∈ V |
72 | 71 | elsn 4140 |
. . . . . . 7
⊢ ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) = (0g‘𝑅)) |
73 | 72 | necon3bbii 2829 |
. . . . . 6
⊢ (¬
(𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
74 | 70, 73 | sylib 207 |
. . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
75 | 33, 9, 66, 74 | syl21anc 1317 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
76 | 28, 57, 43 | drngunit 18575 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵 ∧ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)))) |
77 | 76 | ad2antrr 758 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵 ∧ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)))) |
78 | 61, 75, 77 | mpbir2and 959 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅)) |
79 | | qqhval2.1 |
. . . 4
⊢ / =
(/r‘𝑅) |
80 | | zringmulr 19646 |
. . . 4
⊢ ·
= (.r‘ℤring) |
81 | 57, 27, 79, 80 | rhmdvd 29152 |
. . 3
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ ((𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ∧ (𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅))) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))))) |
82 | 5, 22, 26, 9, 60, 78, 81 | syl132anc 1336 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))))) |
83 | | divnumden 15294 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) |
84 | 6, 83 | sylan 487 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) |
85 | 84 | simpld 474 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌))) |
86 | 85 | eqcomd 2616 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) = (numer‘(𝑋 / 𝑌))) |
87 | 86 | fveq2d 6107 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘(numer‘(𝑋 / 𝑌)))) |
88 | 84 | simprd 478 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌))) |
89 | 88 | eqcomd 2616 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) = (denom‘(𝑋 / 𝑌))) |
90 | 89 | fveq2d 6107 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘(denom‘(𝑋 / 𝑌)))) |
91 | 87, 90 | oveq12d 6567 |
. . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
92 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
93 | 92 | zcnd 11359 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℂ) |
94 | 93 | mulm1d 10361 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = -(𝑋 / (𝑋 gcd 𝑌))) |
95 | | neg1cn 11001 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
96 | 95 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℂ) |
97 | 96, 93 | mulcomd 9940 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) |
98 | 94, 97 | eqtr3d 2646 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑋 / (𝑋 gcd 𝑌)) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) |
99 | 98 | fveq2d 6107 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1))) |
100 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
101 | 100 | zcnd 11359 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℂ) |
102 | 101 | mulm1d 10361 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = -(𝑌 / (𝑋 gcd 𝑌))) |
103 | 96, 101 | mulcomd 9940 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) |
104 | 102, 103 | eqtr3d 2646 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑌 / (𝑋 gcd 𝑌)) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) |
105 | 104 | fveq2d 6107 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1))) |
106 | 99, 105 | oveq12d 6567 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
107 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑋 ∈
ℤ) |
108 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑌 ∈
ℤ) |
109 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -𝑌 ∈
ℕ) |
110 | | divnumden2 28951 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) |
111 | 107, 108,
109, 110 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) |
112 | 111 | simpld 474 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌))) |
113 | 112 | fveq2d 6107 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(numer‘(𝑋 / 𝑌))) = (𝐿‘-(𝑋 / (𝑋 gcd 𝑌)))) |
114 | 111 | simprd 478 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌))) |
115 | 114 | fveq2d 6107 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(denom‘(𝑋 / 𝑌))) = (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) |
116 | 113, 115 | oveq12d 6567 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))))) |
117 | 5 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
118 | | 1zzd 11285 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 1 ∈
ℤ) |
119 | 118 | znegcld 11360 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℤ) |
120 | 60 | adantr 480 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅)) |
121 | | neg1z 11290 |
. . . . . . . 8
⊢ -1 ∈
ℤ |
122 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
123 | 122 | absnegi 13987 |
. . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) |
124 | | abs1 13885 |
. . . . . . . . 9
⊢
(abs‘1) = 1 |
125 | 123, 124 | eqtri 2632 |
. . . . . . . 8
⊢
(abs‘-1) = 1 |
126 | | zringunit 19655 |
. . . . . . . 8
⊢ (-1
∈ (Unit‘ℤring) ↔ (-1 ∈ ℤ ∧
(abs‘-1) = 1)) |
127 | 121, 125,
126 | mpbir2an 957 |
. . . . . . 7
⊢ -1 ∈
(Unit‘ℤring) |
128 | 127 | a1i 11 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ (Unit‘ℤring)) |
129 | | elrhmunit 29151 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ -1 ∈
(Unit‘ℤring)) → (𝐿‘-1) ∈ (Unit‘𝑅)) |
130 | 117, 128,
129 | syl2anc 691 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-1) ∈
(Unit‘𝑅)) |
131 | 57, 27, 79, 80 | rhmdvd 29152 |
. . . . 5
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ ((𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ -1 ∈ ℤ)
∧ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ∧ (𝐿‘-1) ∈ (Unit‘𝑅))) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
132 | 117, 92, 100, 119, 120, 130, 131 | syl132anc 1336 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
133 | 106, 116,
132 | 3eqtr4rd 2655 |
. . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
134 | | simp3 1056 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ≠ 0) |
135 | 134 | neneqd 2787 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ¬ 𝑌 = 0) |
136 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ∈
ℤ) |
137 | | elz 11256 |
. . . . . . . 8
⊢ (𝑌 ∈ ℤ ↔ (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
138 | 136, 137 | sylib 207 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
139 | 138 | simprd 478 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) |
140 | | 3orass 1034 |
. . . . . 6
⊢ ((𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ) ↔ (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
141 | 139, 140 | sylib 207 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
142 | | orel1 396 |
. . . . 5
⊢ (¬
𝑌 = 0 → ((𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
143 | 135, 141,
142 | sylc 63 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) |
144 | 143 | adantl 481 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) |
145 | 91, 133, 144 | mpjaodan 823 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
146 | 6 | zcnd 11359 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℂ) |
147 | 146, 35, 16 | divcan1d 10681 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑋) |
148 | 147 | fveq2d 6107 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑋)) |
149 | 34, 35, 16 | divcan1d 10681 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑌) |
150 | 149 | fveq2d 6107 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑌)) |
151 | 148, 150 | oveq12d 6567 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) |
152 | 82, 145, 151 | 3eqtr3d 2652 |
1
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) |