Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem1.s |
. . . . . 6
|
2 | 1 | a1i 11 |
. . . . 5
|
3 | | hoidmvlelem1.a |
. . . . . . 7
|
4 | | hoidmvlelem1.z |
. . . . . . . . . 10
|
5 | | snidg 4206 |
. . . . . . . . . 10
|
6 | 4, 5 | syl 17 |
. . . . . . . . 9
|
7 | | elun2 3781 |
. . . . . . . . 9
|
8 | 6, 7 | syl 17 |
. . . . . . . 8
|
9 | | hoidmvlelem1.w |
. . . . . . . 8
|
10 | 8, 9 | syl6eleqr 2712 |
. . . . . . 7
|
11 | 3, 10 | ffvelrnd 6360 |
. . . . . 6
|
12 | | hoidmvlelem1.b |
. . . . . . 7
|
13 | 12, 10 | ffvelrnd 6360 |
. . . . . 6
|
14 | | hoidmvlelem1.u |
. . . . . . . 8
Σ^ |
15 | | ssrab2 3687 |
. . . . . . . 8
Σ^ |
16 | 14, 15 | eqsstri 3635 |
. . . . . . 7
|
17 | 16 | a1i 11 |
. . . . . 6
|
18 | 11 | leidd 10594 |
. . . . . . . . . . 11
|
19 | | hoidmvlelem1.ab |
. . . . . . . . . . . 12
|
20 | 11, 13, 19 | ltled 10185 |
. . . . . . . . . . 11
|
21 | 11, 13, 11, 18, 20 | eliccd 39726 |
. . . . . . . . . 10
|
22 | 11 | recnd 10068 |
. . . . . . . . . . . . . 14
|
23 | 22 | subidd 10380 |
. . . . . . . . . . . . 13
|
24 | 23 | oveq2d 6666 |
. . . . . . . . . . . 12
|
25 | | rge0ssre 12280 |
. . . . . . . . . . . . . . 15
|
26 | | hoidmvlelem1.g |
. . . . . . . . . . . . . . . 16
|
27 | | hoidmvlelem1.l |
. . . . . . . . . . . . . . . . 17
|
28 | | hoidmvlelem1.x |
. . . . . . . . . . . . . . . . . 18
|
29 | | hoidmvlelem1.y |
. . . . . . . . . . . . . . . . . 18
|
30 | 28, 29 | ssfid 8183 |
. . . . . . . . . . . . . . . . 17
|
31 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 31, 9 | sseqtr4i 3638 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
34 | 3, 33 | fssresd 6071 |
. . . . . . . . . . . . . . . . 17
|
35 | 12, 33 | fssresd 6071 |
. . . . . . . . . . . . . . . . 17
|
36 | 27, 30, 34, 35 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . 16
|
37 | 26, 36 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
|
38 | 25, 37 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
39 | 38 | recnd 10068 |
. . . . . . . . . . . . 13
|
40 | 39 | mul01d 10235 |
. . . . . . . . . . . 12
|
41 | 24, 40 | eqtrd 2656 |
. . . . . . . . . . 11
|
42 | | 1red 10055 |
. . . . . . . . . . . . 13
|
43 | | hoidmvlelem1.e |
. . . . . . . . . . . . . 14
|
44 | 43 | rpred 11872 |
. . . . . . . . . . . . 13
|
45 | 42, 44 | readdcld 10069 |
. . . . . . . . . . . 12
|
46 | | 0red 10041 |
. . . . . . . . . . . . 13
|
47 | | 0lt1 10550 |
. . . . . . . . . . . . . . 15
|
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
|
49 | 42, 43 | ltaddrpd 11905 |
. . . . . . . . . . . . . 14
|
50 | 46, 42, 45, 48, 49 | lttrd 10198 |
. . . . . . . . . . . . 13
|
51 | 46, 45, 50 | ltled 10185 |
. . . . . . . . . . . 12
|
52 | | nnex 11026 |
. . . . . . . . . . . . . . 15
|
53 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
|
54 | | icossicc 12260 |
. . . . . . . . . . . . . . . 16
|
55 | | snfi 8038 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | | unfi 8227 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 30, 56, 57 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 9, 58 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
61 | | hoidmvlelem1.c |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
63 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
|
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
65 | | hoidmvlelem1.h |
. . . . . . . . . . . . . . . . . . 19
|
66 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
68 | 67 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 68, 67 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | 66, 67, 69 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . . . 22
|
71 | 70 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . . . 21
|
72 | 71 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 72 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 65, 73 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
75 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
76 | | hoidmvlelem1.d |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 76 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
|
78 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
80 | 74, 75, 60, 79 | hsphoif 40790 |
. . . . . . . . . . . . . . . . 17
|
81 | 27, 60, 64, 80 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . 16
|
82 | 54, 81 | sseldi 3601 |
. . . . . . . . . . . . . . 15
|
83 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
84 | 82, 83 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
85 | 53, 84 | sge0cl 40598 |
. . . . . . . . . . . . 13
Σ^ |
86 | 53, 84 | sge0xrcl 40602 |
. . . . . . . . . . . . . 14
Σ^ |
87 | | pnfxr 10092 |
. . . . . . . . . . . . . . 15
|
88 | 87 | a1i 11 |
. . . . . . . . . . . . . 14
|
89 | | hoidmvlelem1.r |
. . . . . . . . . . . . . . . 16
Σ^ |
90 | 89 | rexrd 10089 |
. . . . . . . . . . . . . . 15
Σ^ |
91 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
92 | 27, 60, 64, 79 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . . 17
|
93 | 54, 92 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
|
94 | 4 | eldifbd 3587 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 10, 94 | eldifd 3585 |
. . . . . . . . . . . . . . . . . 18
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
97 | 27, 60, 96, 9, 75, 74, 64, 79 | hsphoidmvle 40800 |
. . . . . . . . . . . . . . . 16
|
98 | 91, 53, 82, 93, 97 | sge0lempt 40627 |
. . . . . . . . . . . . . . 15
Σ^ Σ^ |
99 | 89 | ltpnfd 11955 |
. . . . . . . . . . . . . . 15
Σ^ |
100 | 86, 90, 88, 98, 99 | xrlelttrd 11991 |
. . . . . . . . . . . . . 14
Σ^ |
101 | 86, 88, 100 | xrltned 39573 |
. . . . . . . . . . . . 13
Σ^ |
102 | | ge0xrre 39758 |
. . . . . . . . . . . . 13
Σ^ Σ^ Σ^ |
103 | 85, 101, 102 | syl2anc 693 |
. . . . . . . . . . . 12
Σ^ |
104 | 53, 84 | sge0ge0 40601 |
. . . . . . . . . . . 12
Σ^ |
105 | | mulge0 10546 |
. . . . . . . . . . . 12
Σ^
Σ^ Σ^ |
106 | 45, 51, 103, 104, 105 | syl22anc 1327 |
. . . . . . . . . . 11
Σ^ |
107 | 41, 106 | eqbrtrd 4675 |
. . . . . . . . . 10
Σ^ |
108 | 21, 107 | jca 554 |
. . . . . . . . 9
Σ^ |
109 | | oveq1 6657 |
. . . . . . . . . . . 12
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . 11
|
111 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
112 | 111 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
|
113 | 112 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
114 | 113 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
|
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . 12
Σ^ Σ^ |
116 | 115 | oveq2d 6666 |
. . . . . . . . . . 11
Σ^ Σ^ |
117 | 110, 116 | breq12d 4666 |
. . . . . . . . . 10
Σ^
Σ^ |
118 | 117 | elrab 3363 |
. . . . . . . . 9
Σ^ Σ^ |
119 | 108, 118 | sylibr 224 |
. . . . . . . 8
Σ^ |
120 | 119, 14 | syl6eleqr 2712 |
. . . . . . 7
|
121 | | ne0i 3921 |
. . . . . . 7
|
122 | 120, 121 | syl 17 |
. . . . . 6
|
123 | 11, 13, 17, 122 | supicc 12320 |
. . . . 5
|
124 | 2, 123 | eqeltrd 2701 |
. . . 4
|
125 | 2 | oveq1d 6665 |
. . . . . . 7
|
126 | 125 | oveq2d 6666 |
. . . . . 6
|
127 | 11, 13 | iccssred 39727 |
. . . . . . . . 9
|
128 | 17, 127 | sstrd 3613 |
. . . . . . . 8
|
129 | 11, 13 | jca 554 |
. . . . . . . . . 10
|
130 | | iccsupr 12266 |
. . . . . . . . . 10
|
131 | 129, 17, 120, 130 | syl3anc 1326 |
. . . . . . . . 9
|
132 | 131 | simp3d 1075 |
. . . . . . . 8
|
133 | | eqid 2622 |
. . . . . . . 8
|
134 | 128, 122,
132, 11, 133 | supsubc 39569 |
. . . . . . 7
|
135 | 134 | oveq2d 6666 |
. . . . . 6
|
136 | 46 | rexrd 10089 |
. . . . . . . 8
|
137 | | icogelb 12225 |
. . . . . . . 8
|
138 | 136, 88, 37, 137 | syl3anc 1326 |
. . . . . . 7
|
139 | | vex 3203 |
. . . . . . . . . . . 12
|
140 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
141 | 140 | rexbidv 3052 |
. . . . . . . . . . . 12
|
142 | 139, 141 | elab 3350 |
. . . . . . . . . . 11
|
143 | 142 | biimpi 206 |
. . . . . . . . . 10
|
144 | 143 | adantl 482 |
. . . . . . . . 9
|
145 | | nfv 1843 |
. . . . . . . . . . 11
|
146 | | nfcv 2764 |
. . . . . . . . . . . 12
|
147 | | nfre1 3005 |
. . . . . . . . . . . . 13
|
148 | 147 | nfab 2769 |
. . . . . . . . . . . 12
|
149 | 146, 148 | nfel 2777 |
. . . . . . . . . . 11
|
150 | 145, 149 | nfan 1828 |
. . . . . . . . . 10
|
151 | | nfv 1843 |
. . . . . . . . . 10
|
152 | 11 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
|
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
154 | 13 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
|
155 | 154 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
156 | 17 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
157 | | iccgelb 12230 |
. . . . . . . . . . . . . . . 16
|
158 | 153, 155,
156, 157 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
159 | 128 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
160 | 11 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
161 | 159, 160 | subge0d 10617 |
. . . . . . . . . . . . . . 15
|
162 | 158, 161 | mpbird 247 |
. . . . . . . . . . . . . 14
|
163 | 162 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
164 | | id 22 |
. . . . . . . . . . . . . . 15
|
165 | 164 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
166 | 165 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
|
167 | 163, 166 | breqtrd 4679 |
. . . . . . . . . . . 12
|
168 | 167 | 3exp 1264 |
. . . . . . . . . . 11
|
169 | 168 | adantr 481 |
. . . . . . . . . 10
|
170 | 150, 151,
169 | rexlimd 3026 |
. . . . . . . . 9
|
171 | 144, 170 | mpd 15 |
. . . . . . . 8
|
172 | 171 | ralrimiva 2966 |
. . . . . . 7
|
173 | | simp3 1063 |
. . . . . . . . . . . 12
|
174 | 159, 160 | resubcld 10458 |
. . . . . . . . . . . . 13
|
175 | 174 | 3adant3 1081 |
. . . . . . . . . . . 12
|
176 | 173, 175 | eqeltrd 2701 |
. . . . . . . . . . 11
|
177 | 176 | 3exp 1264 |
. . . . . . . . . 10
|
178 | 177 | rexlimdv 3030 |
. . . . . . . . 9
|
179 | 178 | alrimiv 1855 |
. . . . . . . 8
|
180 | | abss 3671 |
. . . . . . . 8
|
181 | 179, 180 | sylibr 224 |
. . . . . . 7
|
182 | 23 | eqcomd 2628 |
. . . . . . . . . 10
|
183 | | oveq1 6657 |
. . . . . . . . . . . 12
|
184 | 183 | eqeq2d 2632 |
. . . . . . . . . . 11
|
185 | 184 | rspcev 3309 |
. . . . . . . . . 10
|
186 | 120, 182,
185 | syl2anc 693 |
. . . . . . . . 9
|
187 | | c0ex 10034 |
. . . . . . . . . 10
|
188 | | eqeq1 2626 |
. . . . . . . . . . 11
|
189 | 188 | rexbidv 3052 |
. . . . . . . . . 10
|
190 | 187, 189 | elab 3350 |
. . . . . . . . 9
|
191 | 186, 190 | sylibr 224 |
. . . . . . . 8
|
192 | | ne0i 3921 |
. . . . . . . 8
|
193 | 191, 192 | syl 17 |
. . . . . . 7
|
194 | 13, 11 | resubcld 10458 |
. . . . . . . 8
|
195 | | vex 3203 |
. . . . . . . . . . . . 13
|
196 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
|
197 | 196 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
198 | 195, 197 | elab 3350 |
. . . . . . . . . . . 12
|
199 | 198 | biimpi 206 |
. . . . . . . . . . 11
|
200 | 199 | adantl 482 |
. . . . . . . . . 10
|
201 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
202 | 201, 148 | nfel 2777 |
. . . . . . . . . . . 12
|
203 | 145, 202 | nfan 1828 |
. . . . . . . . . . 11
|
204 | | nfv 1843 |
. . . . . . . . . . 11
|
205 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
206 | 160 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
207 | 13 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
208 | 156 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
209 | 21 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
210 | 206, 207,
208, 209 | iccsuble 39745 |
. . . . . . . . . . . . . 14
|
211 | 205, 210 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
212 | 211 | 3exp 1264 |
. . . . . . . . . . . 12
|
213 | 212 | adantr 481 |
. . . . . . . . . . 11
|
214 | 203, 204,
213 | rexlimd 3026 |
. . . . . . . . . 10
|
215 | 200, 214 | mpd 15 |
. . . . . . . . 9
|
216 | 215 | ralrimiva 2966 |
. . . . . . . 8
|
217 | | breq2 4657 |
. . . . . . . . . 10
|
218 | 217 | ralbidv 2986 |
. . . . . . . . 9
|
219 | 218 | rspcev 3309 |
. . . . . . . 8
|
220 | 194, 216,
219 | syl2anc 693 |
. . . . . . 7
|
221 | | eqid 2622 |
. . . . . . . 8
|
222 | | biid 251 |
. . . . . . . 8
|
223 | 221, 222 | supmul1 10992 |
. . . . . . 7
|
224 | 38, 138, 172, 181, 193, 220, 223 | syl33anc 1341 |
. . . . . 6
|
225 | 126, 135,
224 | 3eqtrd 2660 |
. . . . 5
|
226 | | vex 3203 |
. . . . . . . . . . . 12
|
227 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
228 | 227 | rexbidv 3052 |
. . . . . . . . . . . 12
|
229 | 226, 228 | elab 3350 |
. . . . . . . . . . 11
|
230 | 229 | biimpi 206 |
. . . . . . . . . 10
|
231 | | nfv 1843 |
. . . . . . . . . . . 12
|
232 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
233 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
|
234 | 233 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
235 | 232, 234 | elab 3350 |
. . . . . . . . . . . . . . . 16
|
236 | 235 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
237 | 236 | adantr 481 |
. . . . . . . . . . . . . 14
|
238 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
239 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
240 | 239 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
241 | 238, 240 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
242 | 241 | ex 450 |
. . . . . . . . . . . . . . . 16
|
243 | 242 | reximdv 3016 |
. . . . . . . . . . . . . . 15
|
244 | 243 | adantl 482 |
. . . . . . . . . . . . . 14
|
245 | 237, 244 | mpd 15 |
. . . . . . . . . . . . 13
|
246 | 245 | ex 450 |
. . . . . . . . . . . 12
|
247 | 231, 246 | rexlimi 3024 |
. . . . . . . . . . 11
|
248 | 247 | a1i 11 |
. . . . . . . . . 10
|
249 | 230, 248 | mpd 15 |
. . . . . . . . 9
|
250 | 249 | adantl 482 |
. . . . . . . 8
|
251 | | simp3 1063 |
. . . . . . . . . . . 12
|
252 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
|
253 | 252, 174 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
254 | 45 | adantr 481 |
. . . . . . . . . . . . . . 15
|
255 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
256 | 60 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
257 | 64 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
258 | 159 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
259 | 79 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
260 | 74, 258, 256, 259 | hsphoif 40790 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | 27, 256, 257, 260 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . . . . 19
|
262 | 54, 261 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
263 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
264 | 262, 263 | fmptd 6385 |
. . . . . . . . . . . . . . . . 17
|
265 | 255, 264 | sge0cl 40598 |
. . . . . . . . . . . . . . . 16
Σ^ |
266 | 255, 264 | sge0xrcl 40602 |
. . . . . . . . . . . . . . . . 17
Σ^ |
267 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
268 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Σ^ |
269 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
270 | 93 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
271 | 96 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
272 | 27, 256, 271, 9, 258, 74, 257, 259 | hsphoidmvle 40800 |
. . . . . . . . . . . . . . . . . . 19
|
273 | 269, 255,
262, 270, 272 | sge0lempt 40627 |
. . . . . . . . . . . . . . . . . 18
Σ^ Σ^ |
274 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Σ^ |
275 | 266, 268,
267, 273, 274 | xrlelttrd 11991 |
. . . . . . . . . . . . . . . . 17
Σ^ |
276 | 266, 267,
275 | xrltned 39573 |
. . . . . . . . . . . . . . . 16
Σ^ |
277 | | ge0xrre 39758 |
. . . . . . . . . . . . . . . 16
Σ^ Σ^ Σ^ |
278 | 265, 276,
277 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Σ^ |
279 | 254, 278 | remulcld 10070 |
. . . . . . . . . . . . . 14
Σ^ |
280 | 127, 124 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
281 | 27, 30, 95, 9, 61, 76, 89, 65, 280 | sge0hsphoire 40803 |
. . . . . . . . . . . . . . . 16
Σ^ |
282 | 45, 281 | remulcld 10070 |
. . . . . . . . . . . . . . 15
Σ^ |
283 | 282 | adantr 481 |
. . . . . . . . . . . . . 14
Σ^ |
284 | 14 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . 18
Σ^ |
285 | 284 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
Σ^ |
286 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
287 | 286 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
288 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
289 | 288 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
290 | 289 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
|
291 | 290 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . 21
|
292 | 291 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
Σ^ Σ^ |
293 | 292 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
Σ^ Σ^ |
294 | 287, 293 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
Σ^
Σ^ |
295 | 294 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
Σ^
Σ^ |
296 | 285, 295 | sylib 208 |
. . . . . . . . . . . . . . . 16
Σ^ |
297 | 296 | simprd 479 |
. . . . . . . . . . . . . . 15
Σ^ |
298 | 297 | adantl 482 |
. . . . . . . . . . . . . 14
Σ^ |
299 | 281 | adantr 481 |
. . . . . . . . . . . . . . 15
Σ^ |
300 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
|
301 | 280 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
302 | 74, 301, 60, 79 | hsphoif 40790 |
. . . . . . . . . . . . . . . . . . 19
|
303 | 27, 60, 64, 302 | hoidmvcl 40796 |
. . . . . . . . . . . . . . . . . 18
|
304 | 54, 303 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
305 | 304 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
306 | 301 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
307 | 128 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
308 | 122 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
309 | 132 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
310 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
311 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . 20
|
312 | 307, 308,
309, 310, 311 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . 19
|
313 | 312, 1 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . 18
|
314 | 313 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
315 | 27, 256, 271, 9, 258, 306, 314, 74, 257, 259 | hsphoidmvle2 40799 |
. . . . . . . . . . . . . . . 16
|
316 | 269, 255,
262, 305, 315 | sge0lempt 40627 |
. . . . . . . . . . . . . . 15
Σ^ Σ^ |
317 | 278, 299,
254, 300, 316 | lemul2ad 10964 |
. . . . . . . . . . . . . 14
Σ^ Σ^ |
318 | 253, 279,
283, 298, 317 | letrd 10194 |
. . . . . . . . . . . . 13
Σ^ |
319 | 318 | 3adant3 1081 |
. . . . . . . . . . . 12
Σ^ |
320 | 251, 319 | eqbrtrd 4675 |
. . . . . . . . . . 11
Σ^ |
321 | 320 | 3exp 1264 |
. . . . . . . . . 10
Σ^ |
322 | 321 | rexlimdv 3030 |
. . . . . . . . 9
Σ^ |
323 | 322 | adantr 481 |
. . . . . . . 8
Σ^ |
324 | 250, 323 | mpd 15 |
. . . . . . 7
Σ^ |
325 | 324 | ralrimiva 2966 |
. . . . . 6
Σ^ |
326 | 230 | adantl 482 |
. . . . . . . . . 10
|
327 | | nfv 1843 |
. . . . . . . . . . . 12
|
328 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
329 | | nfre1 3005 |
. . . . . . . . . . . . . 14
|
330 | 329 | nfab 2769 |
. . . . . . . . . . . . 13
|
331 | 328, 330 | nfel 2777 |
. . . . . . . . . . . 12
|
332 | 327, 331 | nfan 1828 |
. . . . . . . . . . 11
|
333 | | nfv 1843 |
. . . . . . . . . . 11
|
334 | 236 | adantl 482 |
. . . . . . . . . . . . . 14
|
335 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
336 | 252 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
|
337 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . 22
|
338 | 174 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
|
339 | 337, 338 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
|
340 | 336, 339 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
|
341 | 340 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
342 | 335, 341 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
343 | 342 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
344 | 343 | 3exp 1264 |
. . . . . . . . . . . . . . . 16
|
345 | 344 | rexlimdv 3030 |
. . . . . . . . . . . . . . 15
|
346 | 345 | adantr 481 |
. . . . . . . . . . . . . 14
|
347 | 334, 346 | mpd 15 |
. . . . . . . . . . . . 13
|
348 | 347 | ex 450 |
. . . . . . . . . . . 12
|
349 | 348 | adantr 481 |
. . . . . . . . . . 11
|
350 | 332, 333,
349 | rexlimd 3026 |
. . . . . . . . . 10
|
351 | 326, 350 | mpd 15 |
. . . . . . . . 9
|
352 | 351 | ralrimiva 2966 |
. . . . . . . 8
|
353 | | dfss3 3592 |
. . . . . . . 8
|
354 | 352, 353 | sylibr 224 |
. . . . . . 7
|
355 | 40 | eqcomd 2628 |
. . . . . . . . . 10
|
356 | | oveq2 6658 |
. . . . . . . . . . . 12
|
357 | 356 | eqeq2d 2632 |
. . . . . . . . . . 11
|
358 | 357 | rspcev 3309 |
. . . . . . . . . 10
|
359 | 191, 355,
358 | syl2anc 693 |
. . . . . . . . 9
|
360 | | eqeq1 2626 |
. . . . . . . . . . 11
|
361 | 360 | rexbidv 3052 |
. . . . . . . . . 10
|
362 | 187, 361 | elab 3350 |
. . . . . . . . 9
|
363 | 359, 362 | sylibr 224 |
. . . . . . . 8
|
364 | | ne0i 3921 |
. . . . . . . 8
|
365 | 363, 364 | syl 17 |
. . . . . . 7
|
366 | 38, 194 | remulcld 10070 |
. . . . . . . 8
|
367 | 194 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
368 | 138 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
369 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
370 | | iccleub 12229 |
. . . . . . . . . . . . . . . . . 18
|
371 | 153, 155,
156, 370 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
372 | 159, 369,
160, 371 | lesub1dd 10643 |
. . . . . . . . . . . . . . . 16
|
373 | 174, 367,
252, 368, 372 | lemul2ad 10964 |
. . . . . . . . . . . . . . 15
|
374 | 373 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
375 | 251, 374 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
376 | 375 | 3exp 1264 |
. . . . . . . . . . . 12
|
377 | 376 | rexlimdv 3030 |
. . . . . . . . . . 11
|
378 | 377 | adantr 481 |
. . . . . . . . . 10
|
379 | 250, 378 | mpd 15 |
. . . . . . . . 9
|
380 | 379 | ralrimiva 2966 |
. . . . . . . 8
|
381 | | breq2 4657 |
. . . . . . . . . 10
|
382 | 381 | ralbidv 2986 |
. . . . . . . . 9
|
383 | 382 | rspcev 3309 |
. . . . . . . 8
|
384 | 366, 380,
383 | syl2anc 693 |
. . . . . . 7
|
385 | | suprleub 10989 |
. . . . . . 7
Σ^
Σ^
Σ^ |
386 | 354, 365,
384, 282, 385 | syl31anc 1329 |
. . . . . 6
Σ^
Σ^ |
387 | 325, 386 | mpbird 247 |
. . . . 5
Σ^ |
388 | 225, 387 | eqbrtrd 4675 |
. . . 4
Σ^ |
389 | 124, 388 | jca 554 |
. . 3
Σ^ |
390 | | oveq1 6657 |
. . . . . 6
|
391 | 390 | oveq2d 6666 |
. . . . 5
|
392 | | fveq2 6191 |
. . . . . . . . . 10
|
393 | 392 | fveq1d 6193 |
. . . . . . . . 9
|
394 | 393 | oveq2d 6666 |
. . . . . . . 8
|
395 | 394 | mpteq2dv 4745 |
. . . . . . 7
|
396 | 395 | fveq2d 6195 |
. . . . . 6
Σ^ Σ^ |
397 | 396 | oveq2d 6666 |
. . . . 5
Σ^ Σ^ |
398 | 391, 397 | breq12d 4666 |
. . . 4
Σ^
Σ^ |
399 | 398 | elrab 3363 |
. . 3
Σ^
Σ^ |
400 | 389, 399 | sylibr 224 |
. 2
Σ^ |
401 | 400, 14 | syl6eleqr 2712 |
1
|