Proof of Theorem qqhval2lem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | drngring 20737 | . . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | 
| 2 |  | qqhval2.2 | . . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑅) | 
| 3 | 2 | zrhrhm 21523 | . . . . 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 1194 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℤ) | 
| 7 |  | simpr2 1195 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℤ) | 
| 8 | 6, 7 | gcdcld 16546 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈
ℕ0) | 
| 9 | 8 | nn0zd 12641 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℤ) | 
| 10 |  | simpr3 1196 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ≠ 0) | 
| 11 |  | gcdeq0 16555 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 ↔ (𝑋 = 0 ∧ 𝑌 = 0))) | 
| 12 | 11 | simplbda 499 | . . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) = 0) → 𝑌 = 0) | 
| 13 | 12 | ex 412 | . . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) = 0 → 𝑌 = 0)) | 
| 14 | 13 | necon3d 2960 | . . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 ≠ 0 → (𝑋 gcd 𝑌) ≠ 0)) | 
| 15 | 14 | imp 406 | . . . . 5
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑌 ≠ 0) → (𝑋 gcd 𝑌) ≠ 0) | 
| 16 | 6, 7, 10, 15 | syl21anc 837 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ≠ 0) | 
| 17 |  | gcddvds 16541 | . . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) | 
| 18 | 6, 7, 17 | syl2anc 584 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 gcd 𝑌) ∥ 𝑋 ∧ (𝑋 gcd 𝑌) ∥ 𝑌)) | 
| 19 | 18 | simpld 494 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑋) | 
| 20 |  | dvdsval2 16294 | . . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑋 ↔ (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ)) | 
| 21 | 20 | biimpa 476 | . . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑋 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑋) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 22 | 9, 16, 6, 19, 21 | syl31anc 1374 | . . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 23 | 18 | simprd 495 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∥ 𝑌) | 
| 24 |  | dvdsval2 16294 | . . . . 5
⊢ (((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) → ((𝑋 gcd 𝑌) ∥ 𝑌 ↔ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ)) | 
| 25 | 24 | biimpa 476 | . . . 4
⊢ ((((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝑋 gcd 𝑌) ≠ 0 ∧ 𝑌 ∈ ℤ) ∧ (𝑋 gcd 𝑌) ∥ 𝑌) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 26 | 9, 16, 7, 23, 25 | syl31anc 1374 | . . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 27 |  | zringbas 21465 | . . . . . . 7
⊢ ℤ =
(Base‘ℤring) | 
| 28 |  | qqhval2.0 | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 29 | 27, 28 | rhmf 20486 | . . . . . 6
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶𝐵) | 
| 30 | 5, 29 | syl 17 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿:ℤ⟶𝐵) | 
| 31 | 30, 26 | ffvelcdmd 7104 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ 𝐵) | 
| 32 | 30 | ffnd 6736 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝐿 Fn ℤ) | 
| 33 | 7 | zcnd 12725 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑌 ∈
ℂ) | 
| 34 | 9 | zcnd 12725 | . . . . . . . 8
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑋 gcd 𝑌) ∈ ℂ) | 
| 35 | 33, 34, 10, 16 | divne0d 12060 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) | 
| 36 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑌 / (𝑋 gcd 𝑌)) ∈ V | 
| 37 | 36 | elsn 4640 | . . . . . . . 8
⊢ ((𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) = 0) | 
| 38 | 37 | necon3bbii 2987 | . . . . . . 7
⊢ (¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0} ↔ (𝑌 / (𝑋 gcd 𝑌)) ≠ 0) | 
| 39 | 35, 38 | sylibr 234 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ {0}) | 
| 40 | 1 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑅 ∈ Ring) | 
| 41 |  | simplr 768 | . . . . . . 7
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) →
(chr‘𝑅) =
0) | 
| 42 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 43 | 28, 2, 42 | zrhker 33977 | . . . . . . . 8
⊢ (𝑅 ∈ Ring →
((chr‘𝑅) = 0 ↔
(◡𝐿 “ {(0g‘𝑅)}) = {0})) | 
| 44 | 43 | biimpa 476 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(chr‘𝑅) = 0) →
(◡𝐿 “ {(0g‘𝑅)}) = {0}) | 
| 45 | 40, 41, 44 | syl2anc 584 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (◡𝐿 “ {(0g‘𝑅)}) = {0}) | 
| 46 | 39, 45 | neleqtrrd 2863 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) | 
| 47 |  | elpreima 7077 | . . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ ∧ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}))) | 
| 48 | 47 | baibd 539 | . . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)})) | 
| 49 | 48 | biimprd 248 | . . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) → ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} → (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)}))) | 
| 50 | 49 | con3dimp 408 | . . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)}) | 
| 51 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ V | 
| 52 | 51 | elsn 4640 | . . . . . . 7
⊢ ((𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (0g‘𝑅)) | 
| 53 | 52 | necon3bbii 2987 | . . . . . 6
⊢ (¬
(𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) | 
| 54 | 50, 53 | sylib 218 | . . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) ∧ ¬ (𝑌 / (𝑋 gcd 𝑌)) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) | 
| 55 | 32, 26, 46, 54 | syl21anc 837 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ≠ (0g‘𝑅)) | 
| 56 |  | eqid 2736 | . . . . . 6
⊢
(Unit‘𝑅) =
(Unit‘𝑅) | 
| 57 | 28, 56, 42 | drngunit 20735 | . . . . 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 | ffvelcdmd 7104 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ∈ 𝐵) | 
| 61 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑋 gcd 𝑌) ∈ V | 
| 62 | 61 | elsn 4640 | . . . . . . . 8
⊢ ((𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) = 0) | 
| 63 | 62 | necon3bbii 2987 | . . . . . . 7
⊢ (¬
(𝑋 gcd 𝑌) ∈ {0} ↔ (𝑋 gcd 𝑌) ≠ 0) | 
| 64 | 16, 63 | sylibr 234 | . . . . . 6
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ {0}) | 
| 65 | 64, 45 | neleqtrrd 2863 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ¬
(𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) | 
| 66 |  | elpreima 7077 | . . . . . . . . 9
⊢ (𝐿 Fn ℤ → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ ((𝑋 gcd 𝑌) ∈ ℤ ∧ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}))) | 
| 67 | 66 | baibd 539 | . . . . . . . 8
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}) ↔ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)})) | 
| 68 | 67 | biimprd 248 | . . . . . . 7
⊢ ((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) → ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} → (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)}))) | 
| 69 | 68 | con3dimp 408 | . . . . . 6
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → ¬ (𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)}) | 
| 70 |  | fvex 6918 | . . . . . . . 8
⊢ (𝐿‘(𝑋 gcd 𝑌)) ∈ V | 
| 71 | 70 | elsn 4640 | . . . . . . 7
⊢ ((𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) = (0g‘𝑅)) | 
| 72 | 71 | necon3bbii 2987 | . . . . . 6
⊢ (¬
(𝐿‘(𝑋 gcd 𝑌)) ∈ {(0g‘𝑅)} ↔ (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) | 
| 73 | 69, 72 | sylib 218 | . . . . 5
⊢ (((𝐿 Fn ℤ ∧ (𝑋 gcd 𝑌) ∈ ℤ) ∧ ¬ (𝑋 gcd 𝑌) ∈ (◡𝐿 “ {(0g‘𝑅)})) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) | 
| 74 | 32, 9, 65, 73 | syl21anc 837 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘(𝑋 gcd 𝑌)) ≠ (0g‘𝑅)) | 
| 75 | 28, 56, 42 | drngunit 20735 | . . . . 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 21469 | . . . 4
⊢  ·
= (.r‘ℤring) | 
| 80 | 56, 27, 78, 79 | rhmdvd 33349 | . . 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 1389 | . 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))))) | 
| 82 |  | divnumden 16786 | . . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) | 
| 83 | 6, 82 | sylan 580 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌)))) | 
| 84 | 83 | simpld 494 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = (𝑋 / (𝑋 gcd 𝑌))) | 
| 85 | 84 | eqcomd 2742 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) = (numer‘(𝑋 / 𝑌))) | 
| 86 | 85 | fveq2d 6909 | . . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘(numer‘(𝑋 / 𝑌)))) | 
| 87 | 83 | simprd 495 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = (𝑌 / (𝑋 gcd 𝑌))) | 
| 88 | 87 | eqcomd 2742 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) = (denom‘(𝑋 / 𝑌))) | 
| 89 | 88 | fveq2d 6909 | . . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘(denom‘(𝑋 / 𝑌)))) | 
| 90 | 86, 89 | oveq12d 7450 | . . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ 𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) | 
| 91 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 92 | 91 | zcnd 12725 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑋 / (𝑋 gcd 𝑌)) ∈ ℂ) | 
| 93 | 92 | mulm1d 11716 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = -(𝑋 / (𝑋 gcd 𝑌))) | 
| 94 |  | neg1cn 12381 | . . . . . . . . 9
⊢ -1 ∈
ℂ | 
| 95 | 94 | a1i 11 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℂ) | 
| 96 | 95, 92 | mulcomd 11283 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑋 / (𝑋 gcd 𝑌))) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) | 
| 97 | 93, 96 | eqtr3d 2778 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑋 / (𝑋 gcd 𝑌)) = ((𝑋 / (𝑋 gcd 𝑌)) · -1)) | 
| 98 | 97 | fveq2d 6909 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1))) | 
| 99 | 26 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℤ) | 
| 100 | 99 | zcnd 12725 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝑌 / (𝑋 gcd 𝑌)) ∈ ℂ) | 
| 101 | 100 | mulm1d 11716 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = -(𝑌 / (𝑋 gcd 𝑌))) | 
| 102 | 95, 100 | mulcomd 11283 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (-1
· (𝑌 / (𝑋 gcd 𝑌))) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) | 
| 103 | 101, 102 | eqtr3d 2778 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -(𝑌 / (𝑋 gcd 𝑌)) = ((𝑌 / (𝑋 gcd 𝑌)) · -1)) | 
| 104 | 103 | fveq2d 6909 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))) = (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1))) | 
| 105 | 98, 104 | oveq12d 7450 | . . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) | 
| 106 | 6 | adantr 480 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑋 ∈
ℤ) | 
| 107 | 7 | adantr 480 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝑌 ∈
ℤ) | 
| 108 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -𝑌 ∈
ℕ) | 
| 109 |  | divnumden2 32818 | . . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) | 
| 110 | 106, 107,
108, 109 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
((numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌)) ∧ (denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌)))) | 
| 111 | 110 | simpld 494 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(numer‘(𝑋 / 𝑌)) = -(𝑋 / (𝑋 gcd 𝑌))) | 
| 112 | 111 | fveq2d 6909 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(numer‘(𝑋 / 𝑌))) = (𝐿‘-(𝑋 / (𝑋 gcd 𝑌)))) | 
| 113 | 110 | simprd 495 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) →
(denom‘(𝑋 / 𝑌)) = -(𝑌 / (𝑋 gcd 𝑌))) | 
| 114 | 113 | fveq2d 6909 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(denom‘(𝑋 / 𝑌))) = (𝐿‘-(𝑌 / (𝑋 gcd 𝑌)))) | 
| 115 | 112, 114 | oveq12d 7450 | . . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘-(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘-(𝑌 / (𝑋 gcd 𝑌))))) | 
| 116 | 5 | adantr 480 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 𝐿 ∈ (ℤring
RingHom 𝑅)) | 
| 117 |  | 1zzd 12650 | . . . . . 6
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → 1 ∈
ℤ) | 
| 118 | 117 | znegcld 12726 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → -1
∈ ℤ) | 
| 119 | 59 | adantr 480 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘(𝑌 / (𝑋 gcd 𝑌))) ∈ (Unit‘𝑅)) | 
| 120 |  | neg1z 12655 | . . . . . . . 8
⊢ -1 ∈
ℤ | 
| 121 |  | ax-1cn 11214 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 122 | 121 | absnegi 15440 | . . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) | 
| 123 |  | abs1 15337 | . . . . . . . . 9
⊢
(abs‘1) = 1 | 
| 124 | 122, 123 | eqtri 2764 | . . . . . . . 8
⊢
(abs‘-1) = 1 | 
| 125 |  | zringunit 21478 | . . . . . . . 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 20511 | . . . . . 6
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑅) ∧ -1 ∈
(Unit‘ℤring)) → (𝐿‘-1) ∈ (Unit‘𝑅)) | 
| 129 | 116, 127,
128 | syl2anc 584 | . . . . 5
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → (𝐿‘-1) ∈
(Unit‘𝑅)) | 
| 130 | 56, 27, 78, 79 | rhmdvd 33349 | . . . . 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 1389 | . . . 4
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · -1)) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · -1)))) | 
| 132 | 105, 115,
131 | 3eqtr4rd 2787 | . . 3
⊢ ((((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) ∧ -𝑌 ∈ ℕ) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) | 
| 133 |  | simp3 1138 | . . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ≠ 0) | 
| 134 | 133 | neneqd 2944 | . . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → ¬ 𝑌 = 0) | 
| 135 |  | simp2 1137 | . . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → 𝑌 ∈
ℤ) | 
| 136 |  | elz 12617 | . . . . . . . 8
⊢ (𝑌 ∈ ℤ ↔ (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) | 
| 137 | 135, 136 | sylib 218 | . . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℝ ∧ (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) | 
| 138 | 137 | simprd 495 | . . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) | 
| 139 |  | 3orass 1089 | . . . . . 6
⊢ ((𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ) ↔ (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) | 
| 140 | 138, 139 | sylib 218 | . . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) | 
| 141 |  | orel1 888 | . . . . 5
⊢ (¬
𝑌 = 0 → ((𝑌 = 0 ∨ (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈ ℕ))) | 
| 142 | 134, 140,
141 | sylc 65 | . . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) | 
| 143 | 142 | adantl 481 | . . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝑌 ∈ ℕ ∨ -𝑌 ∈
ℕ)) | 
| 144 | 90, 132, 143 | mpjaodan 960 | . 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(𝑋 / (𝑋 gcd 𝑌))) / (𝐿‘(𝑌 / (𝑋 gcd 𝑌)))) = ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌))))) | 
| 145 | 6 | zcnd 12725 | . . . . 5
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → 𝑋 ∈
ℂ) | 
| 146 | 145, 34, 16 | divcan1d 12045 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑋) | 
| 147 | 146 | fveq2d 6909 | . . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑋)) | 
| 148 | 33, 34, 16 | divcan1d 12045 | . . . 4
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)) = 𝑌) | 
| 149 | 148 | fveq2d 6909 | . . 3
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) = (𝐿‘𝑌)) | 
| 150 | 147, 149 | oveq12d 7450 | . 2
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘((𝑋 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌))) / (𝐿‘((𝑌 / (𝑋 gcd 𝑌)) · (𝑋 gcd 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) | 
| 151 | 81, 144, 150 | 3eqtr3d 2784 | 1
⊢ (((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) ∧
(𝑋 ∈ ℤ ∧
𝑌 ∈ ℤ ∧
𝑌 ≠ 0)) → ((𝐿‘(numer‘(𝑋 / 𝑌))) / (𝐿‘(denom‘(𝑋 / 𝑌)))) = ((𝐿‘𝑋) / (𝐿‘𝑌))) |