Proof of Theorem qqhval2lem
Step | Hyp | Ref
| Expression |
1 | | drngring 18754 |
. . . . 5
|
2 | | qqhval2.2 |
. . . . . 6
RHom |
3 | 2 | zrhrhm 19860 |
. . . . 5
ℤring RingHom |
4 | 1, 3 | syl 17 |
. . . 4
ℤring RingHom |
5 | 4 | ad2antrr 762 |
. . 3
chr
ℤring
RingHom |
6 | | simpr1 1067 |
. . . . . 6
chr
|
7 | | simpr2 1068 |
. . . . . 6
chr
|
8 | 6, 7 | gcdcld 15230 |
. . . . 5
chr
|
9 | 8 | nn0zd 11480 |
. . . 4
chr
|
10 | | simpr3 1069 |
. . . . 5
chr
|
11 | | gcdeq0 15238 |
. . . . . . . . 9
|
12 | 11 | simplbda 654 |
. . . . . . . 8
|
13 | 12 | ex 450 |
. . . . . . 7
|
14 | 13 | necon3d 2815 |
. . . . . 6
|
15 | 14 | imp 445 |
. . . . 5
|
16 | 6, 7, 10, 15 | syl21anc 1325 |
. . . 4
chr
|
17 | | gcddvds 15225 |
. . . . . 6
|
18 | 6, 7, 17 | syl2anc 693 |
. . . . 5
chr
|
19 | 18 | simpld 475 |
. . . 4
chr
|
20 | | dvdsval2 14986 |
. . . . 5
|
21 | 20 | biimpa 501 |
. . . 4
|
22 | 9, 16, 6, 19, 21 | syl31anc 1329 |
. . 3
chr
|
23 | 18 | simprd 479 |
. . . 4
chr
|
24 | | dvdsval2 14986 |
. . . . 5
|
25 | 24 | biimpa 501 |
. . . 4
|
26 | 9, 16, 7, 23, 25 | syl31anc 1329 |
. . 3
chr
|
27 | | zringbas 19824 |
. . . . . . 7
ℤring |
28 | | qqhval2.0 |
. . . . . . 7
|
29 | 27, 28 | rhmf 18726 |
. . . . . 6
ℤring RingHom |
30 | 5, 29 | syl 17 |
. . . . 5
chr
|
31 | 30, 26 | ffvelrnd 6360 |
. . . 4
chr
|
32 | | ffn 6045 |
. . . . . 6
|
33 | 30, 32 | syl 17 |
. . . . 5
chr
|
34 | 7 | zcnd 11483 |
. . . . . . . 8
chr
|
35 | 9 | zcnd 11483 |
. . . . . . . 8
chr
|
36 | 34, 35, 10, 16 | divne0d 10817 |
. . . . . . 7
chr
|
37 | | ovex 6678 |
. . . . . . . . 9
|
38 | 37 | elsn 4192 |
. . . . . . . 8
|
39 | 38 | necon3bbii 2841 |
. . . . . . 7
|
40 | 36, 39 | sylibr 224 |
. . . . . 6
chr
|
41 | 1 | ad2antrr 762 |
. . . . . . 7
chr
|
42 | | simplr 792 |
. . . . . . 7
chr
chr |
43 | | eqid 2622 |
. . . . . . . . 9
|
44 | 28, 2, 43 | zrhker 30021 |
. . . . . . . 8
chr |
45 | 44 | biimpa 501 |
. . . . . . 7
chr
|
46 | 41, 42, 45 | syl2anc 693 |
. . . . . 6
chr
|
47 | 40, 46 | neleqtrrd 2723 |
. . . . 5
chr
|
48 | | elpreima 6337 |
. . . . . . . . 9
|
49 | 48 | baibd 948 |
. . . . . . . 8
|
50 | 49 | biimprd 238 |
. . . . . . 7
|
51 | 50 | con3dimp 457 |
. . . . . 6
|
52 | | fvex 6201 |
. . . . . . . 8
|
53 | 52 | elsn 4192 |
. . . . . . 7
|
54 | 53 | necon3bbii 2841 |
. . . . . 6
|
55 | 51, 54 | sylib 208 |
. . . . 5
|
56 | 33, 26, 47, 55 | syl21anc 1325 |
. . . 4
chr
|
57 | | eqid 2622 |
. . . . . 6
Unit Unit |
58 | 28, 57, 43 | drngunit 18752 |
. . . . 5
Unit |
59 | 58 | ad2antrr 762 |
. . . 4
chr
Unit
|
60 | 31, 56, 59 | mpbir2and 957 |
. . 3
chr
Unit |
61 | 30, 9 | ffvelrnd 6360 |
. . . 4
chr
|
62 | | ovex 6678 |
. . . . . . . . 9
|
63 | 62 | elsn 4192 |
. . . . . . . 8
|
64 | 63 | necon3bbii 2841 |
. . . . . . 7
|
65 | 16, 64 | sylibr 224 |
. . . . . 6
chr
|
66 | 65, 46 | neleqtrrd 2723 |
. . . . 5
chr
|
67 | | elpreima 6337 |
. . . . . . . . 9
|
68 | 67 | baibd 948 |
. . . . . . . 8
|
69 | 68 | biimprd 238 |
. . . . . . 7
|
70 | 69 | con3dimp 457 |
. . . . . 6
|
71 | | fvex 6201 |
. . . . . . . 8
|
72 | 71 | elsn 4192 |
. . . . . . 7
|
73 | 72 | necon3bbii 2841 |
. . . . . 6
|
74 | 70, 73 | sylib 208 |
. . . . 5
|
75 | 33, 9, 66, 74 | syl21anc 1325 |
. . . 4
chr
|
76 | 28, 57, 43 | drngunit 18752 |
. . . . 5
Unit
|
77 | 76 | ad2antrr 762 |
. . . 4
chr
Unit
|
78 | 61, 75, 77 | mpbir2and 957 |
. . 3
chr
Unit |
79 | | qqhval2.1 |
. . . 4
/r |
80 | | zringmulr 19827 |
. . . 4
ℤring |
81 | 57, 27, 79, 80 | rhmdvd 29821 |
. . 3
ℤring
RingHom Unit Unit
|
82 | 5, 22, 26, 9, 60, 78, 81 | syl132anc 1344 |
. 2
chr
|
83 | | divnumden 15456 |
. . . . . . . 8
numer denom |
84 | 6, 83 | sylan 488 |
. . . . . . 7
chr
numer denom |
85 | 84 | simpld 475 |
. . . . . 6
chr
numer |
86 | 85 | eqcomd 2628 |
. . . . 5
chr
numer |
87 | 86 | fveq2d 6195 |
. . . 4
chr
numer |
88 | 84 | simprd 479 |
. . . . . 6
chr
denom |
89 | 88 | eqcomd 2628 |
. . . . 5
chr
denom |
90 | 89 | fveq2d 6195 |
. . . 4
chr
denom |
91 | 87, 90 | oveq12d 6668 |
. . 3
chr
numer denom
|
92 | 22 | adantr 481 |
. . . . . . . . 9
chr |
93 | 92 | zcnd 11483 |
. . . . . . . 8
chr |
94 | 93 | mulm1d 10482 |
. . . . . . 7
chr |
95 | | neg1cn 11124 |
. . . . . . . . 9
|
96 | 95 | a1i 11 |
. . . . . . . 8
chr |
97 | 96, 93 | mulcomd 10061 |
. . . . . . 7
chr |
98 | 94, 97 | eqtr3d 2658 |
. . . . . 6
chr |
99 | 98 | fveq2d 6195 |
. . . . 5
chr |
100 | 26 | adantr 481 |
. . . . . . . . 9
chr |
101 | 100 | zcnd 11483 |
. . . . . . . 8
chr |
102 | 101 | mulm1d 10482 |
. . . . . . 7
chr |
103 | 96, 101 | mulcomd 10061 |
. . . . . . 7
chr |
104 | 102, 103 | eqtr3d 2658 |
. . . . . 6
chr |
105 | 104 | fveq2d 6195 |
. . . . 5
chr |
106 | 99, 105 | oveq12d 6668 |
. . . 4
chr |
107 | 6 | adantr 481 |
. . . . . . . 8
chr |
108 | 7 | adantr 481 |
. . . . . . . 8
chr |
109 | | simpr 477 |
. . . . . . . 8
chr |
110 | | divnumden2 29564 |
. . . . . . . 8
numer denom
|
111 | 107, 108,
109, 110 | syl3anc 1326 |
. . . . . . 7
chr numer
denom |
112 | 111 | simpld 475 |
. . . . . 6
chr numer |
113 | 112 | fveq2d 6195 |
. . . . 5
chr numer |
114 | 111 | simprd 479 |
. . . . . 6
chr denom |
115 | 114 | fveq2d 6195 |
. . . . 5
chr denom |
116 | 113, 115 | oveq12d 6668 |
. . . 4
chr numer
denom |
117 | 5 | adantr 481 |
. . . . 5
chr ℤring RingHom |
118 | | 1zzd 11408 |
. . . . . 6
chr |
119 | 118 | znegcld 11484 |
. . . . 5
chr |
120 | 60 | adantr 481 |
. . . . 5
chr
Unit |
121 | | neg1z 11413 |
. . . . . . . 8
|
122 | | ax-1cn 9994 |
. . . . . . . . . 10
|
123 | 122 | absnegi 14139 |
. . . . . . . . 9
|
124 | | abs1 14037 |
. . . . . . . . 9
|
125 | 123, 124 | eqtri 2644 |
. . . . . . . 8
|
126 | | zringunit 19836 |
. . . . . . . 8
Unitℤring |
127 | 121, 125,
126 | mpbir2an 955 |
. . . . . . 7
Unitℤring |
128 | 127 | a1i 11 |
. . . . . 6
chr Unitℤring |
129 | | elrhmunit 29820 |
. . . . . 6
ℤring
RingHom Unitℤring
Unit |
130 | 117, 128,
129 | syl2anc 693 |
. . . . 5
chr Unit |
131 | 57, 27, 79, 80 | rhmdvd 29821 |
. . . . 5
ℤring
RingHom Unit Unit |
132 | 117, 92, 100, 119, 120, 130, 131 | syl132anc 1344 |
. . . 4
chr |
133 | 106, 116,
132 | 3eqtr4rd 2667 |
. . 3
chr numer
denom |
134 | | simp3 1063 |
. . . . . 6
|
135 | 134 | neneqd 2799 |
. . . . 5
|
136 | | simp2 1062 |
. . . . . . . 8
|
137 | | elz 11379 |
. . . . . . . 8
|
138 | 136, 137 | sylib 208 |
. . . . . . 7
|
139 | 138 | simprd 479 |
. . . . . 6
|
140 | | 3orass 1040 |
. . . . . 6
|
141 | 139, 140 | sylib 208 |
. . . . 5
|
142 | | orel1 397 |
. . . . 5
|
143 | 135, 141,
142 | sylc 65 |
. . . 4
|
144 | 143 | adantl 482 |
. . 3
chr
|
145 | 91, 133, 144 | mpjaodan 827 |
. 2
chr
numer denom
|
146 | 6 | zcnd 11483 |
. . . . 5
chr
|
147 | 146, 35, 16 | divcan1d 10802 |
. . . 4
chr
|
148 | 147 | fveq2d 6195 |
. . 3
chr
|
149 | 34, 35, 16 | divcan1d 10802 |
. . . 4
chr
|
150 | 149 | fveq2d 6195 |
. . 3
chr
|
151 | 148, 150 | oveq12d 6668 |
. 2
chr
|
152 | 82, 145, 151 | 3eqtr3d 2664 |
1
chr
numer denom |