Step | Hyp | Ref
| Expression |
1 | | c1liplem1.k |
. . 3
|
2 | | imassrn 5477 |
. . . . . 6
|
3 | | absf 14077 |
. . . . . . 7
|
4 | | frn 6053 |
. . . . . . 7
|
5 | 3, 4 | ax-mp 5 |
. . . . . 6
|
6 | 2, 5 | sstri 3612 |
. . . . 5
|
7 | 6 | a1i 11 |
. . . 4
|
8 | | dvf 23671 |
. . . . . . . 8
|
9 | | ffun 6048 |
. . . . . . . 8
|
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
|
11 | 10 | a1i 11 |
. . . . . 6
|
12 | | c1liplem1.dv |
. . . . . . . 8
|
13 | | cncff 22696 |
. . . . . . . 8
|
14 | | fdm 6051 |
. . . . . . . 8
|
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
|
16 | | ssdmres 5420 |
. . . . . . 7
|
17 | 15, 16 | sylibr 224 |
. . . . . 6
|
18 | | c1liplem1.a |
. . . . . . . 8
|
19 | 18 | rexrd 10089 |
. . . . . . 7
|
20 | | c1liplem1.b |
. . . . . . . 8
|
21 | 20 | rexrd 10089 |
. . . . . . 7
|
22 | | c1liplem1.le |
. . . . . . 7
|
23 | | lbicc2 12288 |
. . . . . . 7
|
24 | 19, 21, 22, 23 | syl3anc 1326 |
. . . . . 6
|
25 | | funfvima2 6493 |
. . . . . . 7
|
26 | 25 | imp 445 |
. . . . . 6
|
27 | 11, 17, 24, 26 | syl21anc 1325 |
. . . . 5
|
28 | | ffun 6048 |
. . . . . . 7
|
29 | 3, 28 | ax-mp 5 |
. . . . . 6
|
30 | | imassrn 5477 |
. . . . . . . 8
|
31 | | frn 6053 |
. . . . . . . . 9
|
32 | 8, 31 | ax-mp 5 |
. . . . . . . 8
|
33 | 30, 32 | sstri 3612 |
. . . . . . 7
|
34 | 3 | fdmi 6052 |
. . . . . . 7
|
35 | 33, 34 | sseqtr4i 3638 |
. . . . . 6
|
36 | | funfvima2 6493 |
. . . . . 6
|
37 | 29, 35, 36 | mp2an 708 |
. . . . 5
|
38 | | ne0i 3921 |
. . . . 5
|
39 | 27, 37, 38 | 3syl 18 |
. . . 4
|
40 | | ax-resscn 9993 |
. . . . . . . 8
|
41 | | ssid 3624 |
. . . . . . . 8
|
42 | | cncfss 22702 |
. . . . . . . 8
|
43 | 40, 41, 42 | mp2an 708 |
. . . . . . 7
|
44 | 43, 12 | sseldi 3601 |
. . . . . 6
|
45 | | cniccbdd 23230 |
. . . . . 6
|
46 | 18, 20, 44, 45 | syl3anc 1326 |
. . . . 5
|
47 | | fvelima 6248 |
. . . . . . . . . 10
|
48 | 29, 47 | mpan 706 |
. . . . . . . . 9
|
49 | | fvelima 6248 |
. . . . . . . . . . . . . 14
|
50 | 10, 49 | mpan 706 |
. . . . . . . . . . . . 13
|
51 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
54 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
56 | 55 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | rspccva 3308 |
. . . . . . . . . . . . . . . . 17
|
58 | 53, 57 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | adantll 750 |
. . . . . . . . . . . . . . 15
|
60 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | breq1d 4663 |
. . . . . . . . . . . . . . 15
|
62 | 59, 61 | syl5ibcom 235 |
. . . . . . . . . . . . . 14
|
63 | 62 | rexlimdva 3031 |
. . . . . . . . . . . . 13
|
64 | 50, 63 | syl5 34 |
. . . . . . . . . . . 12
|
65 | 64 | imp 445 |
. . . . . . . . . . 11
|
66 | | breq1 4656 |
. . . . . . . . . . 11
|
67 | 65, 66 | syl5ibcom 235 |
. . . . . . . . . 10
|
68 | 67 | rexlimdva 3031 |
. . . . . . . . 9
|
69 | 48, 68 | syl5 34 |
. . . . . . . 8
|
70 | 69 | ralrimiv 2965 |
. . . . . . 7
|
71 | 70 | ex 450 |
. . . . . 6
|
72 | 71 | reximdva 3017 |
. . . . 5
|
73 | 46, 72 | mpd 15 |
. . . 4
|
74 | | suprcl 10983 |
. . . 4
|
75 | 7, 39, 73, 74 | syl3anc 1326 |
. . 3
|
76 | 1, 75 | syl5eqel 2705 |
. 2
|
77 | | simplrr 801 |
. . . . . . . . . . 11
|
78 | | fvres 6207 |
. . . . . . . . . . 11
|
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
|
80 | | c1liplem1.cn |
. . . . . . . . . . . . . 14
|
81 | | cncff 22696 |
. . . . . . . . . . . . . 14
|
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
|
83 | 82 | ad2antrr 762 |
. . . . . . . . . . . 12
|
84 | 83, 77 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
85 | 84 | recnd 10068 |
. . . . . . . . . 10
|
86 | 79, 85 | eqeltrrd 2702 |
. . . . . . . . 9
|
87 | | simplrl 800 |
. . . . . . . . . . 11
|
88 | | fvres 6207 |
. . . . . . . . . . 11
|
89 | 87, 88 | syl 17 |
. . . . . . . . . 10
|
90 | 83, 87 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
91 | 90 | recnd 10068 |
. . . . . . . . . 10
|
92 | 89, 91 | eqeltrrd 2702 |
. . . . . . . . 9
|
93 | 86, 92 | subcld 10392 |
. . . . . . . 8
|
94 | | iccssre 12255 |
. . . . . . . . . . . . 13
|
95 | 18, 20, 94 | syl2anc 693 |
. . . . . . . . . . . 12
|
96 | 95 | ad2antrr 762 |
. . . . . . . . . . 11
|
97 | 96, 77 | sseldd 3604 |
. . . . . . . . . 10
|
98 | 96, 87 | sseldd 3604 |
. . . . . . . . . 10
|
99 | 97, 98 | resubcld 10458 |
. . . . . . . . 9
|
100 | 99 | recnd 10068 |
. . . . . . . 8
|
101 | | simpr 477 |
. . . . . . . . . 10
|
102 | | difrp 11868 |
. . . . . . . . . . 11
|
103 | 98, 97, 102 | syl2anc 693 |
. . . . . . . . . 10
|
104 | 101, 103 | mpbid 222 |
. . . . . . . . 9
|
105 | 104 | rpne0d 11877 |
. . . . . . . 8
|
106 | 93, 100, 105 | absdivd 14194 |
. . . . . . 7
|
107 | 6 | a1i 11 |
. . . . . . . . 9
|
108 | 39 | ad2antrr 762 |
. . . . . . . . 9
|
109 | 73 | ad2antrr 762 |
. . . . . . . . 9
|
110 | 29 | a1i 11 |
. . . . . . . . . 10
|
111 | 93, 100, 105 | divcld 10801 |
. . . . . . . . . . 11
|
112 | 111, 34 | syl6eleqr 2712 |
. . . . . . . . . 10
|
113 | 98 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
114 | 97 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
115 | 98, 97, 101 | ltled 10185 |
. . . . . . . . . . . . . . 15
|
116 | | ubicc2 12289 |
. . . . . . . . . . . . . . 15
|
117 | 113, 114,
115, 116 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
118 | | fvres 6207 |
. . . . . . . . . . . . . 14
|
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . 13
|
120 | | lbicc2 12288 |
. . . . . . . . . . . . . . 15
|
121 | 113, 114,
115, 120 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
122 | | fvres 6207 |
. . . . . . . . . . . . . 14
|
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . 13
|
124 | 119, 123 | oveq12d 6668 |
. . . . . . . . . . . 12
|
125 | 124 | oveq1d 6665 |
. . . . . . . . . . 11
|
126 | | iccss2 12244 |
. . . . . . . . . . . . . . . 16
|
127 | 126 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
128 | 127 | resabs1d 5428 |
. . . . . . . . . . . . . 14
|
129 | 80 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
130 | | rescncf 22700 |
. . . . . . . . . . . . . . 15
|
131 | 127, 129,
130 | sylc 65 |
. . . . . . . . . . . . . 14
|
132 | 128, 131 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
|
133 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
134 | | c1liplem1.f |
. . . . . . . . . . . . . . . . . . 19
|
135 | 134 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
136 | | cnex 10017 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | | reex 10027 |
. . . . . . . . . . . . . . . . . . . 20
|
138 | 136, 137 | elpm2 7889 |
. . . . . . . . . . . . . . . . . . 19
|
139 | 138 | simplbi 476 |
. . . . . . . . . . . . . . . . . 18
|
140 | 135, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
141 | 138 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
|
142 | 135, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
143 | | iccssre 12255 |
. . . . . . . . . . . . . . . . . 18
|
144 | 98, 97, 143 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
145 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
ℂfld ℂfld |
146 | 145 | tgioo2 22606 |
. . . . . . . . . . . . . . . . . 18
ℂfld
↾t |
147 | 145, 146 | dvres 23675 |
. . . . . . . . . . . . . . . . 17
|
148 | 133, 140,
142, 144, 147 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
149 | | iccntr 22624 |
. . . . . . . . . . . . . . . . . 18
|
150 | 98, 97, 149 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
151 | 150 | reseq2d 5396 |
. . . . . . . . . . . . . . . 16
|
152 | 148, 151 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
153 | 152 | dmeqd 5326 |
. . . . . . . . . . . . . 14
|
154 | | ioossicc 12259 |
. . . . . . . . . . . . . . . . 17
|
155 | 154, 127 | syl5ss 3614 |
. . . . . . . . . . . . . . . 16
|
156 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
157 | 155, 156 | sstrd 3613 |
. . . . . . . . . . . . . . 15
|
158 | | ssdmres 5420 |
. . . . . . . . . . . . . . 15
|
159 | 157, 158 | sylib 208 |
. . . . . . . . . . . . . 14
|
160 | 153, 159 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
161 | 98, 97, 101, 132, 160 | mvth 23755 |
. . . . . . . . . . . 12
|
162 | 152 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . 18
|
163 | 162 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
164 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
|
165 | 164 | ad2antll 765 |
. . . . . . . . . . . . . . . . 17
|
166 | 163, 165 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
167 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
168 | 17 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
169 | 155 | sseld 3602 |
. . . . . . . . . . . . . . . . . 18
|
170 | 169 | impr 649 |
. . . . . . . . . . . . . . . . 17
|
171 | | funfvima2 6493 |
. . . . . . . . . . . . . . . . . 18
|
172 | 171 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
173 | 167, 168,
170, 172 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
|
174 | 166, 173 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
175 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
176 | 174, 175 | syl5ibcom 235 |
. . . . . . . . . . . . . 14
|
177 | 176 | expr 643 |
. . . . . . . . . . . . 13
|
178 | 177 | rexlimdv 3030 |
. . . . . . . . . . . 12
|
179 | 161, 178 | mpd 15 |
. . . . . . . . . . 11
|
180 | 125, 179 | eqeltrrd 2702 |
. . . . . . . . . 10
|
181 | | funfvima 6492 |
. . . . . . . . . . 11
|
182 | 181 | imp 445 |
. . . . . . . . . 10
|
183 | 110, 112,
180, 182 | syl21anc 1325 |
. . . . . . . . 9
|
184 | | suprub 10984 |
. . . . . . . . 9
|
185 | 107, 108,
109, 183, 184 | syl31anc 1329 |
. . . . . . . 8
|
186 | 185, 1 | syl6breqr 4695 |
. . . . . . 7
|
187 | 106, 186 | eqbrtrrd 4677 |
. . . . . 6
|
188 | 93 | abscld 14175 |
. . . . . . 7
|
189 | 76 | ad2antrr 762 |
. . . . . . 7
|
190 | 100, 105 | absrpcld 14187 |
. . . . . . 7
|
191 | 188, 189,
190 | ledivmuld 11925 |
. . . . . 6
|
192 | 187, 191 | mpbid 222 |
. . . . 5
|
193 | 190 | rpcnd 11874 |
. . . . . 6
|
194 | 189 | recnd 10068 |
. . . . . 6
|
195 | 193, 194 | mulcomd 10061 |
. . . . 5
|
196 | 192, 195 | breqtrd 4679 |
. . . 4
|
197 | 196 | ex 450 |
. . 3
|
198 | 197 | ralrimivva 2971 |
. 2
|
199 | 76, 198 | jca 554 |
1
|