Proof of Theorem hoidmv1lelem1
Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem1.s |
. . . . . 6
|
2 | | hoidmv1lelem1.a |
. . . . . . 7
|
3 | | hoidmv1lelem1.b |
. . . . . . 7
|
4 | | hoidmv1lelem1.u |
. . . . . . . . 9
Σ^ |
5 | | ssrab2 3687 |
. . . . . . . . 9
Σ^ |
6 | 4, 5 | eqsstri 3635 |
. . . . . . . 8
|
7 | 6 | a1i 11 |
. . . . . . 7
|
8 | 2 | rexrd 10089 |
. . . . . . . . . . . 12
|
9 | 3 | rexrd 10089 |
. . . . . . . . . . . 12
|
10 | | hoidmv1lelem1.l |
. . . . . . . . . . . . 13
|
11 | 2, 3, 10 | ltled 10185 |
. . . . . . . . . . . 12
|
12 | | lbicc2 12288 |
. . . . . . . . . . . 12
|
13 | 8, 9, 11, 12 | syl3anc 1326 |
. . . . . . . . . . 11
|
14 | 2 | recnd 10068 |
. . . . . . . . . . . . 13
|
15 | 14 | subidd 10380 |
. . . . . . . . . . . 12
|
16 | | nfv 1843 |
. . . . . . . . . . . . 13
|
17 | | nnex 11026 |
. . . . . . . . . . . . . 14
|
18 | 17 | a1i 11 |
. . . . . . . . . . . . 13
|
19 | | volf 23297 |
. . . . . . . . . . . . . . 15
|
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
|
21 | | hoidmv1lelem1.c |
. . . . . . . . . . . . . . . 16
|
22 | 21 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
23 | | hoidmv1lelem1.d |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
|
25 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
26 | 24, 25 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
28 | | icombl 23332 |
. . . . . . . . . . . . . . 15
|
29 | 22, 27, 28 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
30 | 20, 29 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
31 | 16, 18, 30 | sge0ge0mpt 40655 |
. . . . . . . . . . . 12
Σ^ |
32 | 15, 31 | eqbrtrd 4675 |
. . . . . . . . . . 11
Σ^ |
33 | 13, 32 | jca 554 |
. . . . . . . . . 10
Σ^ |
34 | | oveq1 6657 |
. . . . . . . . . . . 12
|
35 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
|
36 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
37 | 35, 36 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
40 | 39 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . 12
Σ^ Σ^ |
42 | 34, 41 | breq12d 4666 |
. . . . . . . . . . 11
Σ^
Σ^ |
43 | 42 | elrab 3363 |
. . . . . . . . . 10
Σ^ Σ^ |
44 | 33, 43 | sylibr 224 |
. . . . . . . . 9
Σ^ |
45 | 44, 4 | syl6eleqr 2712 |
. . . . . . . 8
|
46 | | ne0i 3921 |
. . . . . . . 8
|
47 | 45, 46 | syl 17 |
. . . . . . 7
|
48 | 2, 3, 7, 47 | supicc 12320 |
. . . . . 6
|
49 | 1, 48 | syl5eqel 2705 |
. . . . 5
|
50 | 1 | a1i 11 |
. . . . . . 7
|
51 | | nfv 1843 |
. . . . . . . . 9
|
52 | 2, 3 | iccssred 39727 |
. . . . . . . . . . . . 13
|
53 | 7, 52 | sstrd 3613 |
. . . . . . . . . . . 12
|
54 | 53 | sselda 3603 |
. . . . . . . . . . 11
|
55 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
56 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
57 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
58 | 22 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
59 | 24 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | 59, 60 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
63 | | icombl 23332 |
. . . . . . . . . . . . . . . . . 18
|
64 | 58, 62, 63 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
65 | 57, 64 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
66 | 55, 56, 65 | sge0xrclmpt 40645 |
. . . . . . . . . . . . . . 15
Σ^ |
67 | | pnfxr 10092 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . 15
|
69 | | hoidmv1lelem1.r |
. . . . . . . . . . . . . . . . . 18
Σ^ |
70 | 69 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
Σ^ |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . 16
Σ^ |
72 | 24 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | | icombl 23332 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 22, 72, 73 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 20, 74 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
|
76 | 75 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
77 | 74 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
|
78 | 22 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 78 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 72 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 22 | leidd 10594 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 81 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
83 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 59, 60, 83 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
85 | | icossico 12243 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 79, 80, 82, 84, 85 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
|
87 | | volss 23301 |
. . . . . . . . . . . . . . . . . 18
|
88 | 64, 77, 86, 87 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
89 | 55, 56, 65, 76, 88 | sge0lempt 40627 |
. . . . . . . . . . . . . . . 16
Σ^ Σ^ |
90 | 69 | ltpnfd 11955 |
. . . . . . . . . . . . . . . . 17
Σ^ |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
Σ^ |
92 | 66, 71, 68, 89, 91 | xrlelttrd 11991 |
. . . . . . . . . . . . . . 15
Σ^ |
93 | 66, 68, 92 | xrltned 39573 |
. . . . . . . . . . . . . 14
Σ^ |
94 | 93 | neneqd 2799 |
. . . . . . . . . . . . 13
Σ^ |
95 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
96 | 65, 95 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
97 | 56, 96 | sge0repnf 40603 |
. . . . . . . . . . . . 13
Σ^
Σ^ |
98 | 94, 97 | mpbird 247 |
. . . . . . . . . . . 12
Σ^ |
99 | 2 | adantr 481 |
. . . . . . . . . . . 12
|
100 | 98, 99 | readdcld 10069 |
. . . . . . . . . . 11
Σ^ |
101 | 52, 49 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 24, 102 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | 103 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
105 | | icombl 23332 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 22, 104, 105 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
107 | 20, 106 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
108 | 16, 18, 107 | sge0xrclmpt 40645 |
. . . . . . . . . . . . . . . 16
Σ^ |
109 | 67 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
110 | | min1 12020 |
. . . . . . . . . . . . . . . . . . . . 21
|
111 | 24, 102, 110 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | | icossico 12243 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 78, 72, 81, 111, 112 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | volss 23301 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 106, 74, 113, 114 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
116 | 16, 18, 107, 75, 115 | sge0lempt 40627 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
117 | 108, 70, 109, 116, 90 | xrlelttrd 11991 |
. . . . . . . . . . . . . . . 16
Σ^ |
118 | 108, 109,
117 | xrltned 39573 |
. . . . . . . . . . . . . . 15
Σ^ |
119 | 118 | neneqd 2799 |
. . . . . . . . . . . . . 14
Σ^ |
120 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
121 | 107, 120 | fmptd 6385 |
. . . . . . . . . . . . . . 15
|
122 | 18, 121 | sge0repnf 40603 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
123 | 119, 122 | mpbird 247 |
. . . . . . . . . . . . 13
Σ^ |
124 | 123, 2 | readdcld 10069 |
. . . . . . . . . . . 12
Σ^ |
125 | 124 | adantr 481 |
. . . . . . . . . . 11
Σ^ |
126 | 4 | eleq2i 2693 |
. . . . . . . . . . . . . . . 16
Σ^ |
127 | 126 | biimpi 206 |
. . . . . . . . . . . . . . 15
Σ^ |
128 | 127 | adantl 482 |
. . . . . . . . . . . . . 14
Σ^ |
129 | | rabid 3116 |
. . . . . . . . . . . . . 14
Σ^ Σ^ |
130 | 128, 129 | sylib 208 |
. . . . . . . . . . . . 13
Σ^ |
131 | 130 | simprd 479 |
. . . . . . . . . . . 12
Σ^ |
132 | 54, 99, 98 | lesubaddd 10624 |
. . . . . . . . . . . 12
Σ^
Σ^ |
133 | 131, 132 | mpbid 222 |
. . . . . . . . . . 11
Σ^ |
134 | 123 | adantr 481 |
. . . . . . . . . . . 12
Σ^ |
135 | 107 | adantlr 751 |
. . . . . . . . . . . . 13
|
136 | 106 | adantlr 751 |
. . . . . . . . . . . . . 14
|
137 | 104 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
138 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
139 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . 18
|
140 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
|
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
142 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
143 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 101 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
145 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
146 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
147 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
148 | 2, 3 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
149 | | iccsupr 12266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
150 | 148, 7, 45, 149 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
151 | 150 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
152 | 151 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
153 | 128, 126 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
154 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
155 | 146, 147,
152, 153, 154 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . 22
|
156 | 155, 1 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . . 21
|
157 | 156 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
158 | 142, 143,
144, 145, 157 | letrd 10194 |
. . . . . . . . . . . . . . . . . . 19
|
159 | 158 | iftrued 4094 |
. . . . . . . . . . . . . . . . . 18
|
160 | 139, 141,
159 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
|
161 | 138, 160 | eqled 10140 |
. . . . . . . . . . . . . . . 16
|
162 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
163 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
165 | 162, 163 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . 21
|
166 | 164, 165 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
|
167 | 162, 163,
166 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
169 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
|
170 | 169 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
171 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . 20
|
172 | 171 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
173 | 170, 172 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
|
174 | 168, 173 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
175 | 156 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
|
176 | 169 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
|
177 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . 20
|
178 | 177 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
179 | 176, 178 | breq12d 4666 |
. . . . . . . . . . . . . . . . . 18
|
180 | 175, 179 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
181 | 174, 180 | pm2.61dan 832 |
. . . . . . . . . . . . . . . 16
|
182 | 161, 181 | pm2.61dan 832 |
. . . . . . . . . . . . . . 15
|
183 | | icossico 12243 |
. . . . . . . . . . . . . . 15
|
184 | 79, 137, 82, 182, 183 | syl22anc 1327 |
. . . . . . . . . . . . . 14
|
185 | | volss 23301 |
. . . . . . . . . . . . . 14
|
186 | 64, 136, 184, 185 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
187 | 55, 56, 65, 135, 186 | sge0lempt 40627 |
. . . . . . . . . . . 12
Σ^ Σ^ |
188 | 98, 134, 99, 187 | leadd1dd 10641 |
. . . . . . . . . . 11
Σ^ Σ^ |
189 | 54, 100, 125, 133, 188 | letrd 10194 |
. . . . . . . . . 10
Σ^ |
190 | 189 | ex 450 |
. . . . . . . . 9
Σ^ |
191 | 51, 190 | ralrimi 2957 |
. . . . . . . 8
Σ^ |
192 | | suprleub 10989 |
. . . . . . . . 9
Σ^
Σ^
Σ^ |
193 | 53, 47, 151, 124, 192 | syl31anc 1329 |
. . . . . . . 8
Σ^
Σ^ |
194 | 191, 193 | mpbird 247 |
. . . . . . 7
Σ^ |
195 | 50, 194 | eqbrtrd 4675 |
. . . . . 6
Σ^ |
196 | 101, 2, 123 | lesubaddd 10624 |
. . . . . 6
Σ^
Σ^ |
197 | 195, 196 | mpbird 247 |
. . . . 5
Σ^ |
198 | 49, 197 | jca 554 |
. . . 4
Σ^ |
199 | | oveq1 6657 |
. . . . . 6
|
200 | | breq2 4657 |
. . . . . . . . . . 11
|
201 | | id 22 |
. . . . . . . . . . 11
|
202 | 200, 201 | ifbieq2d 4111 |
. . . . . . . . . 10
|
203 | 202 | oveq2d 6666 |
. . . . . . . . 9
|
204 | 203 | fveq2d 6195 |
. . . . . . . 8
|
205 | 204 | mpteq2dv 4745 |
. . . . . . 7
|
206 | 205 | fveq2d 6195 |
. . . . . 6
Σ^ Σ^ |
207 | 199, 206 | breq12d 4666 |
. . . . 5
Σ^
Σ^ |
208 | 207 | elrab 3363 |
. . . 4
Σ^ Σ^ |
209 | 198, 208 | sylibr 224 |
. . 3
Σ^ |
210 | 209, 4 | syl6eleqr 2712 |
. 2
|
211 | 210, 45, 151 | 3jca 1242 |
1
|