Metamath Proof Explorer

Theorem qqhval2lem

Description: Lemma for qqhval2 . (Contributed by Thierry Arnoux, 29-Oct-2017)

Ref Expression
Hypotheses qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion qqhval2lem ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) = ( ( 𝐿 ‘ 𝑋 ) / ( 𝐿 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 qqhval2.0 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 qqhval2.1 ⊢ / = ( /r ‘ 𝑅 )
3 qqhval2.2 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
4 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
5 3 zrhrhm ⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
6 4 5 syl ⊢ ( 𝑅 ∈ DivRing → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
7 6 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
8 simpr1 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑋 ∈ ℤ )
9 simpr2 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ∈ ℤ )
10 8 9 gcdcld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ∈ ℕ0 )
11 10 nn0zd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ∈ ℤ )
12 simpr3 ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ≠ 0 )
13 gcdeq0 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∧ 𝑌 = 0 ) ) )
14 13 simplbda ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑋 gcd 𝑌 ) = 0 ) → 𝑌 = 0 )
15 14 ex ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) = 0 → 𝑌 = 0 ) )
16 15 necon3d ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑌 ≠ 0 → ( 𝑋 gcd 𝑌 ) ≠ 0 ) )
17 16 imp ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑌 ≠ 0 ) → ( 𝑋 gcd 𝑌 ) ≠ 0 )
18 8 9 12 17 syl21anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ≠ 0 )
19 gcddvds ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) ∥ 𝑋 ∧ ( 𝑋 gcd 𝑌 ) ∥ 𝑌 ) )
20 8 9 19 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝑋 gcd 𝑌 ) ∥ 𝑋 ∧ ( 𝑋 gcd 𝑌 ) ∥ 𝑌 ) )
21 20 simpld ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ∥ 𝑋 )
22 dvdsval2 ⊢ ( ( ( 𝑋 gcd 𝑌 ) ∈ ℤ ∧ ( 𝑋 gcd 𝑌 ) ≠ 0 ∧ 𝑋 ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) ∥ 𝑋 ↔ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) )
23 22 biimpa ⊢ ( ( ( ( 𝑋 gcd 𝑌 ) ∈ ℤ ∧ ( 𝑋 gcd 𝑌 ) ≠ 0 ∧ 𝑋 ∈ ℤ ) ∧ ( 𝑋 gcd 𝑌 ) ∥ 𝑋 ) → ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
24 11 18 8 21 23 syl31anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
25 20 simprd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ∥ 𝑌 )
26 dvdsval2 ⊢ ( ( ( 𝑋 gcd 𝑌 ) ∈ ℤ ∧ ( 𝑋 gcd 𝑌 ) ≠ 0 ∧ 𝑌 ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) ∥ 𝑌 ↔ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) )
27 26 biimpa ⊢ ( ( ( ( 𝑋 gcd 𝑌 ) ∈ ℤ ∧ ( 𝑋 gcd 𝑌 ) ≠ 0 ∧ 𝑌 ∈ ℤ ) ∧ ( 𝑋 gcd 𝑌 ) ∥ 𝑌 ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
28 11 18 9 25 27 syl31anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
29 zringbas ⊢ ℤ = ( Base ‘ ℤring )
30 29 1 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
31 7 30 syl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝐿 : ℤ ⟶ 𝐵 )
32 31 28 ffvelrnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ 𝐵 )
33 31 ffnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝐿 Fn ℤ )
34 9 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑌 ∈ ℂ )
35 11 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 gcd 𝑌 ) ∈ ℂ )
36 34 35 12 18 divne0d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ≠ 0 )
37 ovex ⊢ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ V
38 37 elsn ⊢ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ { 0 } ↔ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) = 0 )
39 38 necon3bbii ⊢ ( ¬ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ { 0 } ↔ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ≠ 0 )
40 36 39 sylibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ¬ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ { 0 } )
41 4 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑅 ∈ Ring )
42 simplr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( chr ‘ 𝑅 ) = 0 )
43 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
44 1 3 43 zrhker ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } ) )
45 44 biimpa ⊢ ( ( 𝑅 ∈ Ring ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } )
46 41 42 45 syl2anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) = { 0 } )
47 40 46 neleqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ¬ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) )
48 elpreima ⊢ ( 𝐿 Fn ℤ → ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ∧ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } ) ) )
49 48 baibd ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) → ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } ) )
50 49 biimprd ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) )
51 50 con3dimp ⊢ ( ( ( 𝐿 Fn ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) ∧ ¬ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) → ¬ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } )
52 fvex ⊢ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ V
53 52 elsn ⊢ ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) = ( 0g ‘ 𝑅 ) )
54 53 necon3bbii ⊢ ( ¬ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
55 51 54 sylib ⊢ ( ( ( 𝐿 Fn ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ) ∧ ¬ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
56 33 28 47 55 syl21anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ≠ ( 0g ‘ 𝑅 ) )
57 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
58 1 57 43 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
59 58 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
60 32 56 59 mpbir2and ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
61 31 11 ffvelrnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ 𝐵 )
62 ovex ⊢ ( 𝑋 gcd 𝑌 ) ∈ V
63 62 elsn ⊢ ( ( 𝑋 gcd 𝑌 ) ∈ { 0 } ↔ ( 𝑋 gcd 𝑌 ) = 0 )
64 63 necon3bbii ⊢ ( ¬ ( 𝑋 gcd 𝑌 ) ∈ { 0 } ↔ ( 𝑋 gcd 𝑌 ) ≠ 0 )
65 18 64 sylibr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ¬ ( 𝑋 gcd 𝑌 ) ∈ { 0 } )
66 65 46 neleqtrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ¬ ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) )
67 elpreima ⊢ ( 𝐿 Fn ℤ → ( ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( ( 𝑋 gcd 𝑌 ) ∈ ℤ ∧ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } ) ) )
68 67 baibd ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝑋 gcd 𝑌 ) ∈ ℤ ) → ( ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } ) )
69 68 biimprd ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝑋 gcd 𝑌 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } → ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) )
70 69 con3dimp ⊢ ( ( ( 𝐿 Fn ℤ ∧ ( 𝑋 gcd 𝑌 ) ∈ ℤ ) ∧ ¬ ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) → ¬ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } )
71 fvex ⊢ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ V
72 71 elsn ⊢ ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) = ( 0g ‘ 𝑅 ) )
73 72 necon3bbii ⊢ ( ¬ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ { ( 0g ‘ 𝑅 ) } ↔ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ≠ ( 0g ‘ 𝑅 ) )
74 70 73 sylib ⊢ ( ( ( 𝐿 Fn ℤ ∧ ( 𝑋 gcd 𝑌 ) ∈ ℤ ) ∧ ¬ ( 𝑋 gcd 𝑌 ) ∈ ( ◡ 𝐿 “ { ( 0g ‘ 𝑅 ) } ) ) → ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ≠ ( 0g ‘ 𝑅 ) )
75 33 11 66 74 syl21anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ≠ ( 0g ‘ 𝑅 ) )
76 1 57 43 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
77 76 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ 𝐵 ∧ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
78 61 75 77 mpbir2and ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ ( Unit ‘ 𝑅 ) )
79 zringmulr ⊢ · = ( .r ‘ ℤring )
80 57 29 2 79 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ∧ ( 𝑋 gcd 𝑌 ) ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ ( 𝑋 gcd 𝑌 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) ) )
81 7 24 28 11 60 78 80 syl132anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) ) )
82 divnumden ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℕ ) → ( ( numer ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∧ ( denom ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) )
83 8 82 sylan ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( ( numer ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∧ ( denom ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) )
84 83 simpld ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( numer ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) )
85 84 eqcomd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) = ( numer ‘ ( 𝑋 / 𝑌 ) ) )
86 85 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) )
87 83 simprd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( denom ‘ ( 𝑋 / 𝑌 ) ) = ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) )
88 87 eqcomd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) = ( denom ‘ ( 𝑋 / 𝑌 ) ) )
89 88 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) )
90 86 89 oveq12d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ 𝑌 ∈ ℕ ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) )
91 24 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
92 91 zcnd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℂ )
93 92 mulm1d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( - 1 · ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) = - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) )
94 neg1cn ⊢ - 1 ∈ ℂ
95 94 a1i ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - 1 ∈ ℂ )
96 95 92 mulcomd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( - 1 · ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) = ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) )
97 93 96 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) = ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) )
98 97 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) )
99 28 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ )
100 99 zcnd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℂ )
101 100 mulm1d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( - 1 · ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) = - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) )
102 95 100 mulcomd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( - 1 · ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) = ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) )
103 101 102 eqtr3d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) = ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) )
104 103 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) )
105 98 104 oveq12d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( ( 𝐿 ‘ - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) ) )
106 8 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → 𝑋 ∈ ℤ )
107 9 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → 𝑌 ∈ ℤ )
108 simpr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - 𝑌 ∈ ℕ )
109 divnumden2 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ - 𝑌 ∈ ℕ ) → ( ( numer ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∧ ( denom ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) )
110 106 107 108 109 syl3anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( ( numer ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∧ ( denom ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) )
111 110 simpld ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( numer ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) )
112 111 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) = ( 𝐿 ‘ - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) )
113 110 simprd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( denom ‘ ( 𝑋 / 𝑌 ) ) = - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) )
114 113 fveq2d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) = ( 𝐿 ‘ - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) )
115 112 114 oveq12d ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) = ( ( 𝐿 ‘ - ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ - ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) )
116 7 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
117 1zzd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → 1 ∈ ℤ )
118 117 znegcld ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - 1 ∈ ℤ )
119 60 adantr ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
120 neg1z ⊢ - 1 ∈ ℤ
121 ax-1cn ⊢ 1 ∈ ℂ
122 121 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
123 abs1 ⊢ ( abs ‘ 1 ) = 1
124 122 123 eqtri ⊢ ( abs ‘ - 1 ) = 1
125 zringunit ⊢ ( - 1 ∈ ( Unit ‘ ℤring ) ↔ ( - 1 ∈ ℤ ∧ ( abs ‘ - 1 ) = 1 ) )
126 120 124 125 mpbir2an ⊢ - 1 ∈ ( Unit ‘ ℤring )
127 126 a1i ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → - 1 ∈ ( Unit ‘ ℤring ) )
128 elrhmunit ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ - 1 ∈ ( Unit ‘ ℤring ) ) → ( 𝐿 ‘ - 1 ) ∈ ( Unit ‘ 𝑅 ) )
129 116 127 128 syl2anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( 𝐿 ‘ - 1 ) ∈ ( Unit ‘ 𝑅 ) )
130 57 29 2 79 rhmdvd ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) ∧ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ∧ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) ∧ ( ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ∈ ( Unit ‘ 𝑅 ) ∧ ( 𝐿 ‘ - 1 ) ∈ ( Unit ‘ 𝑅 ) ) ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) ) )
131 116 91 99 118 119 129 130 syl132anc ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · - 1 ) ) ) )
132 105 115 131 3eqtr4rd ⊢ ( ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) ∧ - 𝑌 ∈ ℕ ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) )
133 simp3 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → 𝑌 ≠ 0 )
134 133 neneqd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → ¬ 𝑌 = 0 )
135 simp2 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → 𝑌 ∈ ℤ )
136 elz ⊢ ( 𝑌 ∈ ℤ ↔ ( 𝑌 ∈ ℝ ∧ ( 𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) )
137 135 136 sylib ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → ( 𝑌 ∈ ℝ ∧ ( 𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) )
138 137 simprd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → ( 𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) )
139 3orass ⊢ ( ( 𝑌 = 0 ∨ 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ↔ ( 𝑌 = 0 ∨ ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) )
140 138 139 sylib ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → ( 𝑌 = 0 ∨ ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) )
141 orel1 ⊢ ( ¬ 𝑌 = 0 → ( ( 𝑌 = 0 ∨ ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) → ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) ) )
142 134 140 141 sylc ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) → ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) )
143 142 adantl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝑌 ∈ ℕ ∨ - 𝑌 ∈ ℕ ) )
144 90 132 143 mpjaodan ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) )
145 8 zcnd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → 𝑋 ∈ ℂ )
146 145 35 18 divcan1d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) = 𝑋 )
147 146 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ 𝑋 ) )
148 34 35 18 divcan1d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) = 𝑌 )
149 148 fveq2d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) = ( 𝐿 ‘ 𝑌 ) )
150 147 149 oveq12d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( ( 𝑋 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) / ( 𝐿 ‘ ( ( 𝑌 / ( 𝑋 gcd 𝑌 ) ) · ( 𝑋 gcd 𝑌 ) ) ) ) = ( ( 𝐿 ‘ 𝑋 ) / ( 𝐿 ‘ 𝑌 ) ) )
151 81 144 150 3eqtr3d ⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝑌 ≠ 0 ) ) → ( ( 𝐿 ‘ ( numer ‘ ( 𝑋 / 𝑌 ) ) ) / ( 𝐿 ‘ ( denom ‘ ( 𝑋 / 𝑌 ) ) ) ) = ( ( 𝐿 ‘ 𝑋 ) / ( 𝐿 ‘ 𝑌 ) ) )