Proof of Theorem qqhval2lem
Step | Hyp | Ref
| Expression |
1 | | drngring 19774 |
. . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
2 | | qqhval2.2 |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑅) |
3 | 2 | zrhrhm 20478 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝑅 ∈ DivRing → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
5 | 4 | ad2antrr 726 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
6 | | simpr1 1196 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℤ) |
7 | | simpr2 1197 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℤ) |
8 | 6, 7 | gcdcld 16067 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈
ℕ0) |
9 | 8 | nn0zd 12280 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℤ) |
10 | | simpr3 1198 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ≠ 0) |
11 | | gcdeq0 16076 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 ↔ (𝑋 = 0 ∧ 𝑌 = 0))) |
12 | 11 | simplbda 503 |
. . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) = 0) → 𝑌 = 0) |
13 | 12 | ex 416 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 → 𝑌 = 0)) |
14 | 13 | necon3d 2961 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 ≠ 0 → (𝑋 gcd 𝑌) ≠ 0)) |
15 | 14 | imp 410 |
. . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑌 ≠ 0) → (𝑋 gcd 𝑌) ≠ 0) |
16 | 6, 7, 10, 15 | syl21anc 838 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ≠ 0) |
17 | | gcddvds 16062 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) |
18 | 6, 7, 17 | syl2anc 587 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) |
19 | 18 | simpld 498 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑋) |
20 | | dvdsval2 15818 |
. . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ↔ (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ)) |
21 | 20 | biimpa 480 |
. . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑋) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
22 | 9, 16, 6, 19, 21 | syl31anc 1375 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
23 | 18 | simprd 499 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑌) |
24 | | dvdsval2 15818 |
. . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑌 ↔ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ)) |
25 | 24 | biimpa 480 |
. . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑌) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
26 | 9, 16, 7, 23, 25 | syl31anc 1375 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
27 | | zringbas 20441 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
28 | | qqhval2.0 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
29 | 27, 28 | rhmf 19746 |
. . . . . 6
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶𝐵) |
30 | 5, 29 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿:ℤ⟶𝐵) |
31 | 30, 26 | ffvelrnd 6905 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵) |
32 | 30 | ffnd 6546 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿 Fn ℤ) |
33 | 7 | zcnd 12283 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℂ) |
34 | 9 | zcnd 12283 |
. . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℂ) |
35 | 33, 34, 10, 16 | divne0d 11624 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) |
36 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑌 / (𝑋 gcd 𝑌)) ∈ V |
37 | 36 | elsn 4556 |
. . . . . . . 8
⊢ ((𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) = 0) |
38 | 37 | necon3bbii 2988 |
. . . . . . 7
⊢ (¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) |
39 | 35, 38 | sylibr 237 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0}) |
40 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑅 ∈ Ring) |
41 | | simplr 769 |
. . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) →
(chr‘𝑅) =
0) |
42 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
43 | 28, 2, 42 | zrhker 31639 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((chr‘𝑅) = 0 ↔
(◡𝐿 “ {(0g‘𝑅)}) = {0})) |
44 | 43 | biimpa 480 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) |
45 | 40, 41, 44 | syl2anc 587 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (◡𝐿 “ {(0g‘𝑅)}) = {0}) |
46 | 39, 45 | neleqtrrd 2860 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) |
47 | | elpreima 6878 |
. . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}))) |
48 | 47 | baibd 543 |
. . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)})) |
49 | 48 | biimprd 251 |
. . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} → (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}))) |
50 | 49 | con3dimp 412 |
. . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}) |
51 | | fvex 6730 |
. . . . . . . 8
⊢ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ V |
52 | 51 | elsn 4556 |
. . . . . . 7
⊢ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (0g‘𝑅)) |
53 | 52 | necon3bbii 2988 |
. . . . . 6
⊢ (¬
(𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
54 | 50, 53 | sylib 221 |
. . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
55 | 32, 26, 46, 54 | syl21anc 838 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) |
56 | | eqid 2737 |
. . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
57 | 28, 56, 42 | drngunit 19772 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵 ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)))) |
58 | 57 | ad2antrr 726 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵 ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)))) |
59 | 31, 55, 58 | mpbir2and 713 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅)) |
60 | 30, 9 | ffvelrnd 6905 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵) |
61 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑋 gcd 𝑌) ∈ V |
62 | 61 | elsn 4556 |
. . . . . . . 8
⊢ ((𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) = 0) |
63 | 62 | necon3bbii 2988 |
. . . . . . 7
⊢ (¬
(𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) ≠ 0) |
64 | 16, 63 | sylibr 237 |
. . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ {0}) |
65 | 64, 45 | neleqtrrd 2860 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) |
66 | | elpreima 6878 |
. . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}))) |
67 | 66 | baibd 543 |
. . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)})) |
68 | 67 | biimprd 251 |
. . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} → (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}))) |
69 | 68 | con3dimp 412 |
. . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}) |
70 | | fvex 6730 |
. . . . . . . 8
⊢ (𝐿‘(𝑋 gcd 𝑌)) ∈ V |
71 | 70 | elsn 4556 |
. . . . . . 7
⊢ ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) = (0g‘𝑅)) |
72 | 71 | necon3bbii 2988 |
. . . . . 6
⊢ (¬
(𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
73 | 69, 72 | sylib 221 |
. . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
74 | 32, 9, 65, 73 | syl21anc 838 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) |
75 | 28, 56, 42 | drngunit 19772 |
. . . . 5
⊢ (𝑅 ∈ DivRing → ((𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵 ∧ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)))) |
76 | 75 | ad2antrr 726 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅) ↔ ((𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵 ∧ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)))) |
77 | 60, 74, 76 | mpbir2and 713 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅)) |
78 | | qqhval2.1 |
. . . 4
⊢ / =
(/r‘𝑅) |
79 | | zringmulr 20444 |
. . . 4
⊢ ·
= (.r‘ℤring) |
80 | 56, 27, 78, 79 | rhmdvd 31239 |
. . 3
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ ((𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ∧ (𝐿‘(𝑋 gcd 𝑌)) ∈ (Unit‘𝑅))) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))))) |
81 | 5, 22, 26, 9, 59, 77, 80 | syl132anc 1390 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))))) |
82 | | divnumden 16304 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) |
83 | 6, 82 | sylan 583 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) |
84 | 83 | simpld 498 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌))) |
85 | 84 | eqcomd 2743 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) = (numer‘(𝑋 / 𝑌))) |
86 | 85 | fveq2d 6721 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘(numer‘(𝑋 / 𝑌)))) |
87 | 83 | simprd 499 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌))) |
88 | 87 | eqcomd 2743 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) = (denom‘(𝑋 / 𝑌))) |
89 | 88 | fveq2d 6721 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘(denom‘(𝑋 / 𝑌)))) |
90 | 86, 89 | oveq12d 7231 |
. . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
91 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) |
92 | 91 | zcnd 12283 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℂ) |
93 | 92 | mulm1d 11284 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = -(𝑋 / (𝑋 gcd 𝑌))) |
94 | | neg1cn 11944 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
95 | 94 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℂ) |
96 | 95, 92 | mulcomd 10854 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) |
97 | 93, 96 | eqtr3d 2779 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑋 / (𝑋 gcd 𝑌)) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) |
98 | 97 | fveq2d 6721 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1))) |
99 | 26 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) |
100 | 99 | zcnd 12283 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℂ) |
101 | 100 | mulm1d 11284 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = -(𝑌 / (𝑋 gcd 𝑌))) |
102 | 95, 100 | mulcomd 10854 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) |
103 | 101, 102 | eqtr3d 2779 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑌 / (𝑋 gcd 𝑌)) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) |
104 | 103 | fveq2d 6721 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1))) |
105 | 98, 104 | oveq12d 7231 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
106 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑋 ∈
ℤ) |
107 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑌 ∈
ℤ) |
108 | | simpr 488 |
. . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -𝑌 ∈
ℕ) |
109 | | divnumden2 30852 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) |
110 | 106, 107,
108, 109 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) |
111 | 110 | simpld 498 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌))) |
112 | 111 | fveq2d 6721 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(numer‘(𝑋 / 𝑌))) = (𝐿‘-(𝑋 / (𝑋 gcd 𝑌)))) |
113 | 110 | simprd 499 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌))) |
114 | 113 | fveq2d 6721 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(denom‘(𝑋 / 𝑌))) = (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) |
115 | 112, 114 | oveq12d 7231 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))))) |
116 | 5 | adantr 484 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
117 | | 1zzd 12208 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 1 ∈
ℤ) |
118 | 117 | znegcld 12284 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℤ) |
119 | 59 | adantr 484 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅)) |
120 | | neg1z 12213 |
. . . . . . . 8
⊢ -1 ∈
ℤ |
121 | | ax-1cn 10787 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
122 | 121 | absnegi 14964 |
. . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) |
123 | | abs1 14861 |
. . . . . . . . 9
⊢
(abs‘1) = 1 |
124 | 122, 123 | eqtri 2765 |
. . . . . . . 8
⊢
(abs‘-1) = 1 |
125 | | zringunit 20453 |
. . . . . . . 8
⊢ (-1
∈ (Unit‘ℤring) ↔ (-1 ∈ ℤ ∧
(abs‘-1) = 1)) |
126 | 120, 124,
125 | mpbir2an 711 |
. . . . . . 7
⊢ -1 ∈
(Unit‘ℤring) |
127 | 126 | a1i 11 |
. . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ (Unit‘ℤring)) |
128 | | elrhmunit 31238 |
. . . . . 6
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ -1 ∈
(Unit‘ℤring)) → (𝐿‘-1) ∈ (Unit‘𝑅)) |
129 | 116, 127,
128 | syl2anc 587 |
. . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-1) ∈
(Unit‘𝑅)) |
130 | 56, 27, 78, 79 | rhmdvd 31239 |
. . . . 5
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ ((𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ -1 ∈ ℤ)
∧ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅) ∧ (𝐿‘-1) ∈ (Unit‘𝑅))) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
131 | 116, 91, 99, 118, 119, 129, 130 | syl132anc 1390 |
. . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) |
132 | 105, 115,
131 | 3eqtr4rd 2788 |
. . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
133 | | simp3 1140 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ≠ 0) |
134 | 133 | neneqd 2945 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ¬ 𝑌 = 0) |
135 | | simp2 1139 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ∈
ℤ) |
136 | | elz 12178 |
. . . . . . . 8
⊢ (𝑌 ∈ ℤ ↔ (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
137 | 135, 136 | sylib 221 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
138 | 137 | simprd 499 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) |
139 | | 3orass 1092 |
. . . . . 6
⊢ ((𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ) ↔ (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
140 | 138, 139 | sylib 221 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
141 | | orel1 889 |
. . . . 5
⊢ (¬
𝑌 = 0 → ((𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) |
142 | 134, 140,
141 | sylc 65 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) |
143 | 142 | adantl 485 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) |
144 | 90, 132, 143 | mpjaodan 959 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) |
145 | 6 | zcnd 12283 |
. . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℂ) |
146 | 145, 34, 16 | divcan1d 11609 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑋) |
147 | 146 | fveq2d 6721 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑋)) |
148 | 33, 34, 16 | divcan1d 11609 |
. . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑌) |
149 | 148 | fveq2d 6721 |
. . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑌)) |
150 | 147, 149 | oveq12d 7231 |
. 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) |
151 | 81, 144, 150 | 3eqtr3d 2785 |
1
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) |