Metamath Proof Explorer

Theorem qqhval2lem

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

Ref Expression
Hypotheses qqhval2.0 
|- B = ( Base ` R )
qqhval2.1 
|- ./ = ( /r ` R )
qqhval2.2 
|- L = ( ZRHom ` R )
Assertion qqhval2lem 
|- ( ( ( R e. DivRing /\ ( chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( numer ` ( X / Y ) ) ) ./ ( L ` ( denom ` ( X / Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )

Proof

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