Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. 2
|
2 | | simpl 473 |
. 2
|
3 | | fveq2 6191 |
. . . . 5
|
4 | | csbeq1 3536 |
. . . . . . 7
|
5 | 4 | oveq1d 6665 |
. . . . . 6
|
6 | 5 | mpteq2dv 4745 |
. . . . 5
|
7 | 3, 6 | eqeq12d 2637 |
. . . 4
|
8 | 7 | imbi2d 330 |
. . 3
|
9 | | fveq2 6191 |
. . . . 5
|
10 | | csbeq1 3536 |
. . . . . . 7
|
11 | 10 | oveq1d 6665 |
. . . . . 6
|
12 | 11 | mpteq2dv 4745 |
. . . . 5
|
13 | 9, 12 | eqeq12d 2637 |
. . . 4
|
14 | 13 | imbi2d 330 |
. . 3
|
15 | | fveq2 6191 |
. . . . 5
|
16 | | csbeq1 3536 |
. . . . . . 7
|
17 | 16 | oveq1d 6665 |
. . . . . 6
|
18 | 17 | mpteq2dv 4745 |
. . . . 5
|
19 | 15, 18 | eqeq12d 2637 |
. . . 4
|
20 | 19 | imbi2d 330 |
. . 3
|
21 | | fveq2 6191 |
. . . . 5
|
22 | | csbeq1a 3542 |
. . . . . . . . 9
|
23 | 22 | equcoms 1947 |
. . . . . . . 8
|
24 | 23 | eqcomd 2628 |
. . . . . . 7
|
25 | 24 | oveq1d 6665 |
. . . . . 6
|
26 | 25 | mpteq2dv 4745 |
. . . . 5
|
27 | 21, 26 | eqeq12d 2637 |
. . . 4
|
28 | 27 | imbi2d 330 |
. . 3
|
29 | | dvnmptdivc.s |
. . . . . . 7
|
30 | | recnprss 23668 |
. . . . . . 7
|
31 | 29, 30 | syl 17 |
. . . . . 6
|
32 | | cnex 10017 |
. . . . . . . 8
|
33 | 32 | a1i 11 |
. . . . . . 7
|
34 | | dvnmptdivc.a |
. . . . . . . . 9
|
35 | | dvnmptdivc.c |
. . . . . . . . . 10
|
36 | 35 | adantr 481 |
. . . . . . . . 9
|
37 | | dvnmptdivc.cne0 |
. . . . . . . . . 10
|
38 | 37 | adantr 481 |
. . . . . . . . 9
|
39 | 34, 36, 38 | divcld 10801 |
. . . . . . . 8
|
40 | | eqid 2622 |
. . . . . . . 8
|
41 | 39, 40 | fmptd 6385 |
. . . . . . 7
|
42 | | dvnmptdivc.x |
. . . . . . 7
|
43 | | elpm2r 7875 |
. . . . . . 7
|
44 | 33, 29, 41, 42, 43 | syl22anc 1327 |
. . . . . 6
|
45 | | dvn0 23687 |
. . . . . 6
|
46 | 31, 44, 45 | syl2anc 693 |
. . . . 5
|
47 | | id 22 |
. . . . . . . . . . . 12
|
48 | | dvnmptdivc.8 |
. . . . . . . . . . . . . 14
|
49 | | nn0uz 11722 |
. . . . . . . . . . . . . 14
|
50 | 48, 49 | syl6eleq 2711 |
. . . . . . . . . . . . 13
|
51 | | eluzfz1 12348 |
. . . . . . . . . . . . 13
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
|
53 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
54 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
55 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
56 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . 16
|
57 | 55, 56 | nfmpt 4746 |
. . . . . . . . . . . . . . 15
|
58 | 54, 57 | nfeq 2776 |
. . . . . . . . . . . . . 14
|
59 | 53, 58 | nfim 1825 |
. . . . . . . . . . . . 13
|
60 | | c0ex 10034 |
. . . . . . . . . . . . 13
|
61 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
62 | 61 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
63 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
64 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | mpteq2dv 4745 |
. . . . . . . . . . . . . . 15
|
66 | 63, 65 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
|
67 | 62, 66 | imbi12d 334 |
. . . . . . . . . . . . 13
|
68 | | dvnmptdivc.dvn |
. . . . . . . . . . . . 13
|
69 | 59, 60, 67, 68 | vtoclf 3258 |
. . . . . . . . . . . 12
|
70 | 47, 52, 69 | syl2anc 693 |
. . . . . . . . . . 11
|
71 | 70 | fveq1d 6193 |
. . . . . . . . . 10
|
72 | 71 | adantr 481 |
. . . . . . . . 9
|
73 | | simpr 477 |
. . . . . . . . . 10
|
74 | | simpl 473 |
. . . . . . . . . . 11
|
75 | 52 | adantr 481 |
. . . . . . . . . . 11
|
76 | | 0re 10040 |
. . . . . . . . . . . 12
|
77 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
78 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
79 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
80 | 56, 79 | nfel 2777 |
. . . . . . . . . . . . . 14
|
81 | 78, 80 | nfim 1825 |
. . . . . . . . . . . . 13
|
82 | 61 | 3anbi3d 1405 |
. . . . . . . . . . . . . 14
|
83 | 64 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
84 | 82, 83 | imbi12d 334 |
. . . . . . . . . . . . 13
|
85 | | dvnmptdivc.b |
. . . . . . . . . . . . 13
|
86 | 77, 81, 84, 85 | vtoclgf 3264 |
. . . . . . . . . . . 12
|
87 | 76, 86 | ax-mp 5 |
. . . . . . . . . . 11
|
88 | 74, 73, 75, 87 | syl3anc 1326 |
. . . . . . . . . 10
|
89 | | eqid 2622 |
. . . . . . . . . . 11
|
90 | 89 | fvmpt2 6291 |
. . . . . . . . . 10
|
91 | 73, 88, 90 | syl2anc 693 |
. . . . . . . . 9
|
92 | 72, 91 | eqtr2d 2657 |
. . . . . . . 8
|
93 | | eqid 2622 |
. . . . . . . . . . . . 13
|
94 | 34, 93 | fmptd 6385 |
. . . . . . . . . . . 12
|
95 | | elpm2r 7875 |
. . . . . . . . . . . 12
|
96 | 33, 29, 94, 42, 95 | syl22anc 1327 |
. . . . . . . . . . 11
|
97 | | dvn0 23687 |
. . . . . . . . . . 11
|
98 | 31, 96, 97 | syl2anc 693 |
. . . . . . . . . 10
|
99 | 98 | fveq1d 6193 |
. . . . . . . . 9
|
100 | 99 | adantr 481 |
. . . . . . . 8
|
101 | 93 | fvmpt2 6291 |
. . . . . . . . 9
|
102 | 73, 34, 101 | syl2anc 693 |
. . . . . . . 8
|
103 | 92, 100, 102 | 3eqtrrd 2661 |
. . . . . . 7
|
104 | 103 | oveq1d 6665 |
. . . . . 6
|
105 | 104 | mpteq2dva 4744 |
. . . . 5
|
106 | 46, 105 | eqtrd 2656 |
. . . 4
|
107 | 106 | a1i 11 |
. . 3
|
108 | | simp3 1063 |
. . . . 5
..^ |
109 | | simp1 1061 |
. . . . 5
..^ ..^ |
110 | | simpr 477 |
. . . . . . 7
|
111 | | simpl 473 |
. . . . . . 7
|
112 | 110, 111 | mpd 15 |
. . . . . 6
|
113 | 112 | 3adant1 1079 |
. . . . 5
..^ |
114 | 31 | ad2antrr 762 |
. . . . . . 7
..^ |
115 | 44 | ad2antrr 762 |
. . . . . . 7
..^ |
116 | | elfzofz 12485 |
. . . . . . . 8
..^
|
117 | | elfznn0 12433 |
. . . . . . . . 9
|
118 | 117 | ad2antlr 763 |
. . . . . . . 8
|
119 | 116, 118 | sylanl2 683 |
. . . . . . 7
..^ |
120 | | dvnp1 23688 |
. . . . . . 7
|
121 | 114, 115,
119, 120 | syl3anc 1326 |
. . . . . 6
..^ |
122 | | oveq2 6658 |
. . . . . . 7
|
123 | 122 | adantl 482 |
. . . . . 6
..^
|
124 | 31 | adantr 481 |
. . . . . . . . . . 11
..^ |
125 | 44 | adantr 481 |
. . . . . . . . . . 11
..^ |
126 | | simpr 477 |
. . . . . . . . . . . . 13
|
127 | 126, 117 | syl 17 |
. . . . . . . . . . . 12
|
128 | 116, 127 | sylan2 491 |
. . . . . . . . . . 11
..^ |
129 | 124, 125,
128, 120 | syl3anc 1326 |
. . . . . . . . . 10
..^ |
130 | 129 | adantr 481 |
. . . . . . . . 9
..^ |
131 | 29 | adantr 481 |
. . . . . . . . . . 11
..^
|
132 | | simplr 792 |
. . . . . . . . . . . . 13
|
133 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
134 | | simpr 477 |
. . . . . . . . . . . . . 14
|
135 | 133, 134,
132 | 3jca 1242 |
. . . . . . . . . . . . 13
|
136 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
137 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
138 | 136 | nfcsb1 3548 |
. . . . . . . . . . . . . . . 16
|
139 | 138, 79 | nfel 2777 |
. . . . . . . . . . . . . . 15
|
140 | 137, 139 | nfim 1825 |
. . . . . . . . . . . . . 14
|
141 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
142 | 141 | 3anbi3d 1405 |
. . . . . . . . . . . . . . 15
|
143 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . 16
|
144 | 143 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
|
145 | 142, 144 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
146 | 136, 140,
145, 85 | vtoclgf 3264 |
. . . . . . . . . . . . 13
|
147 | 132, 135,
146 | sylc 65 |
. . . . . . . . . . . 12
|
148 | 116, 147 | sylanl2 683 |
. . . . . . . . . . 11
..^ |
149 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
..^
|
150 | 149 | ad2antlr 763 |
. . . . . . . . . . . 12
..^ |
151 | 116, 133 | sylanl2 683 |
. . . . . . . . . . . . 13
..^ |
152 | | simpr 477 |
. . . . . . . . . . . . 13
..^ |
153 | 151, 152,
150 | 3jca 1242 |
. . . . . . . . . . . 12
..^ |
154 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
155 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
156 | 154 | nfcsb1 3548 |
. . . . . . . . . . . . . . 15
|
157 | 156, 79 | nfel 2777 |
. . . . . . . . . . . . . 14
|
158 | 155, 157 | nfim 1825 |
. . . . . . . . . . . . 13
|
159 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
160 | 159 | 3anbi3d 1405 |
. . . . . . . . . . . . . 14
|
161 | | csbeq1a 3542 |
. . . . . . . . . . . . . . 15
|
162 | 161 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
163 | 160, 162 | imbi12d 334 |
. . . . . . . . . . . . 13
|
164 | 154, 158,
163, 85 | vtoclgf 3264 |
. . . . . . . . . . . 12
|
165 | 150, 153,
164 | sylc 65 |
. . . . . . . . . . 11
..^ |
166 | | simpl 473 |
. . . . . . . . . . . . . . 15
..^ |
167 | 116 | adantl 482 |
. . . . . . . . . . . . . . 15
..^ |
168 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
169 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
170 | 55, 138 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . 18
|
171 | 169, 170 | nfeq 2776 |
. . . . . . . . . . . . . . . . 17
|
172 | 168, 171 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
173 | 141 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
|
174 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
175 | 143 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
|
176 | 174, 175 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
177 | 173, 176 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
178 | 172, 177,
68 | chvar 2262 |
. . . . . . . . . . . . . . 15
|
179 | 166, 167,
178 | syl2anc 693 |
. . . . . . . . . . . . . 14
..^ |
180 | 179 | eqcomd 2628 |
. . . . . . . . . . . . 13
..^ |
181 | 180 | oveq2d 6666 |
. . . . . . . . . . . 12
..^
|
182 | 166, 96 | syl 17 |
. . . . . . . . . . . . . 14
..^ |
183 | | dvnp1 23688 |
. . . . . . . . . . . . . 14
|
184 | 124, 182,
128, 183 | syl3anc 1326 |
. . . . . . . . . . . . 13
..^ |
185 | 184 | eqcomd 2628 |
. . . . . . . . . . . 12
..^ |
186 | 149 | adantl 482 |
. . . . . . . . . . . . 13
..^ |
187 | 166, 186 | jca 554 |
. . . . . . . . . . . . 13
..^ |
188 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
189 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
190 | 55, 156 | nfmpt 4746 |
. . . . . . . . . . . . . . . 16
|
191 | 189, 190 | nfeq 2776 |
. . . . . . . . . . . . . . 15
|
192 | 188, 191 | nfim 1825 |
. . . . . . . . . . . . . 14
|
193 | 159 | anbi2d 740 |
. . . . . . . . . . . . . . 15
|
194 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
195 | 161 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
|
196 | 194, 195 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
|
197 | 193, 196 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
198 | 154, 192,
197, 68 | vtoclgf 3264 |
. . . . . . . . . . . . 13
|
199 | 186, 187,
198 | sylc 65 |
. . . . . . . . . . . 12
..^ |
200 | 181, 185,
199 | 3eqtrd 2660 |
. . . . . . . . . . 11
..^
|
201 | 35 | adantr 481 |
. . . . . . . . . . 11
..^ |
202 | 37 | adantr 481 |
. . . . . . . . . . 11
..^ |
203 | 131, 148,
165, 200, 201, 202 | dvmptdivc 23728 |
. . . . . . . . . 10
..^
|
204 | 203 | adantr 481 |
. . . . . . . . 9
..^
|
205 | 130, 123,
204 | 3eqtrd 2660 |
. . . . . . . 8
..^ |
206 | 205 | eqcomd 2628 |
. . . . . . 7
..^ |
207 | 206, 121,
123 | 3eqtrrd 2661 |
. . . . . 6
..^
|
208 | 121, 123,
207 | 3eqtrd 2660 |
. . . . 5
..^ |
209 | 108, 109,
113, 208 | syl21anc 1325 |
. . . 4
..^ |
210 | 209 | 3exp 1264 |
. . 3
..^
|
211 | 8, 14, 20, 28, 107, 210 | fzind2 12586 |
. 2
|
212 | 1, 2, 211 | sylc 65 |
1
|