Step | Hyp | Ref
| Expression |
1 | | sge0iunmptlemre.sxr |
. 2
Σ^
|
2 | | sge0iunmptlemre.ssxr |
. 2
Σ^ Σ^ |
3 | | elpwinss 39216 |
. . . . . . . . . 10
|
4 | 3 | resmptd 5452 |
. . . . . . . . 9
|
5 | 4 | fveq2d 6195 |
. . . . . . . 8
Σ^
Σ^ |
6 | 5 | adantl 482 |
. . . . . . 7
Σ^
Σ^ |
7 | | elinel2 3800 |
. . . . . . . . 9
|
8 | 7 | adantl 482 |
. . . . . . . 8
|
9 | 3 | sselda 3603 |
. . . . . . . . . . 11
|
10 | | eliun 4524 |
. . . . . . . . . . 11
|
11 | 9, 10 | sylib 208 |
. . . . . . . . . 10
|
12 | 11 | adantll 750 |
. . . . . . . . 9
|
13 | | nfv 1843 |
. . . . . . . . . . . 12
|
14 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
15 | | nfiu1 4550 |
. . . . . . . . . . . . . . 15
|
16 | 15 | nfpw 4172 |
. . . . . . . . . . . . . 14
|
17 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
18 | 16, 17 | nfin 3820 |
. . . . . . . . . . . . 13
|
19 | 14, 18 | nfel 2777 |
. . . . . . . . . . . 12
|
20 | 13, 19 | nfan 1828 |
. . . . . . . . . . 11
|
21 | | nfv 1843 |
. . . . . . . . . . 11
|
22 | 20, 21 | nfan 1828 |
. . . . . . . . . 10
|
23 | | nfv 1843 |
. . . . . . . . . 10
|
24 | | simp3 1063 |
. . . . . . . . . . . . . . 15
|
25 | | sge0iunmptlemre.c |
. . . . . . . . . . . . . . 15
|
26 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
|
28 | 24, 25, 27 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
29 | 28 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
30 | 25 | 3expa 1265 |
. . . . . . . . . . . . . . . . 17
|
31 | 30, 26 | fmptd 6385 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
|
33 | | sge0iunmptlemre.b |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
35 | | sge0iunmptlemre.re |
. . . . . . . . . . . . . . . . 17
Σ^ |
36 | 35 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
Σ^ |
37 | 34, 32, 36 | sge0rern 40605 |
. . . . . . . . . . . . . . 15
|
38 | 32, 37 | fge0iccico 40587 |
. . . . . . . . . . . . . 14
|
39 | 38, 24 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
40 | 29, 39 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
41 | 40 | 3exp 1264 |
. . . . . . . . . . 11
|
42 | 41 | ad2antrr 762 |
. . . . . . . . . 10
|
43 | 22, 23, 42 | rexlimd 3026 |
. . . . . . . . 9
|
44 | 12, 43 | mpd 15 |
. . . . . . . 8
|
45 | 8, 44 | sge0fsummpt 40607 |
. . . . . . 7
Σ^
|
46 | | sseqin2 3817 |
. . . . . . . . . . . . . 14
|
47 | 46 | biimpi 206 |
. . . . . . . . . . . . 13
|
48 | 47 | eqcomd 2628 |
. . . . . . . . . . . 12
|
49 | | iunin1 4585 |
. . . . . . . . . . . . 13
|
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
|
51 | 48, 50 | eqtr4d 2659 |
. . . . . . . . . . 11
|
52 | 3, 51 | syl 17 |
. . . . . . . . . 10
|
53 | 52 | sumeq1d 14431 |
. . . . . . . . 9
|
54 | 53 | adantl 482 |
. . . . . . . 8
|
55 | | simpl 473 |
. . . . . . . . 9
|
56 | 33 | adantlr 751 |
. . . . . . . . . 10
|
57 | | sge0iunmptlemre.dj |
. . . . . . . . . . 11
Disj
|
58 | 57 | adantr 481 |
. . . . . . . . . 10
Disj
|
59 | | rge0ssre 12280 |
. . . . . . . . . . . . 13
|
60 | | ax-resscn 9993 |
. . . . . . . . . . . . 13
|
61 | 59, 60 | sstri 3612 |
. . . . . . . . . . . 12
|
62 | 61, 40 | sseldi 3601 |
. . . . . . . . . . 11
|
63 | 62 | 3adant1r 1319 |
. . . . . . . . . 10
|
64 | | simpr 477 |
. . . . . . . . . 10
|
65 | 56, 58, 63, 64 | fsumiunss 39807 |
. . . . . . . . 9
|
66 | 55, 8, 65 | syl2anc 693 |
. . . . . . . 8
|
67 | 54, 66 | eqtrd 2656 |
. . . . . . 7
|
68 | 6, 45, 67 | 3eqtrd 2660 |
. . . . . 6
Σ^
|
69 | 56, 58, 64 | disjinfi 39380 |
. . . . . . . . . 10
|
70 | | id 22 |
. . . . . . . . . . . . 13
|
71 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
|
73 | | ssfi 8180 |
. . . . . . . . . . . . 13
|
74 | 70, 72, 73 | syl2anc 693 |
. . . . . . . . . . . 12
|
75 | 74 | ad2antlr 763 |
. . . . . . . . . . 11
|
76 | | simpll 790 |
. . . . . . . . . . . . 13
|
77 | | elrabi 3359 |
. . . . . . . . . . . . . 14
|
78 | 77 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
79 | | elinel1 3799 |
. . . . . . . . . . . . . 14
|
80 | 79 | adantl 482 |
. . . . . . . . . . . . 13
|
81 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
82 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
83 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
84 | 82, 83 | nfel 2777 |
. . . . . . . . . . . . . . . 16
|
85 | 13, 81, 84 | nf3an 1831 |
. . . . . . . . . . . . . . 15
|
86 | 85, 23 | nfim 1825 |
. . . . . . . . . . . . . 14
|
87 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
88 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
90 | 87, 89 | 3anbi23d 1402 |
. . . . . . . . . . . . . . 15
|
91 | 90 | imbi1d 331 |
. . . . . . . . . . . . . 14
|
92 | 86, 91, 40 | chvar 2262 |
. . . . . . . . . . . . 13
|
93 | 76, 78, 80, 92 | syl3anc 1326 |
. . . . . . . . . . . 12
|
94 | 93 | adantllr 755 |
. . . . . . . . . . 11
|
95 | 75, 94 | fsumge0cl 39805 |
. . . . . . . . . 10
|
96 | 69, 95 | sge0fsummpt 40607 |
. . . . . . . . 9
Σ^
|
97 | | inss2 3834 |
. . . . . . . . . . . . . . . . 17
|
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
99 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
|
100 | 70, 98, 99 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
101 | 100 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
102 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
103 | | rabid 3116 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 103 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | simpld 475 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
|
107 | | elinel1 3799 |
. . . . . . . . . . . . . . . . 17
|
108 | 107 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
109 | 102, 106,
108, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
110 | 109 | adantllr 755 |
. . . . . . . . . . . . . 14
|
111 | 101, 110 | sge0fsummpt 40607 |
. . . . . . . . . . . . 13
Σ^ |
112 | 111 | mpteq2dva 4744 |
. . . . . . . . . . . 12
Σ^ |
113 | | nfrab1 3122 |
. . . . . . . . . . . . . 14
|
114 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
115 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
116 | 83, 14 | nfin 3820 |
. . . . . . . . . . . . . . 15
|
117 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
118 | 116, 117 | nfsum 14421 |
. . . . . . . . . . . . . 14
|
119 | 88 | ineq1d 3813 |
. . . . . . . . . . . . . . 15
|
120 | 119 | sumeq1d 14431 |
. . . . . . . . . . . . . 14
|
121 | 113, 114,
115, 118, 120 | cbvmptf 4748 |
. . . . . . . . . . . . 13
|
122 | 121 | a1i 11 |
. . . . . . . . . . . 12
|
123 | 112, 122 | eqtr2d 2657 |
. . . . . . . . . . 11
Σ^ |
124 | 123 | fveq2d 6195 |
. . . . . . . . . 10
Σ^ Σ^ Σ^ |
125 | 124 | eqcomd 2628 |
. . . . . . . . 9
Σ^ Σ^ Σ^ |
126 | 120, 114,
113, 115, 118 | cbvsum 14425 |
. . . . . . . . . 10
|
127 | 126 | a1i 11 |
. . . . . . . . 9
|
128 | 96, 125, 127 | 3eqtr4d 2666 |
. . . . . . . 8
Σ^ Σ^
|
129 | 55, 8, 128 | syl2anc 693 |
. . . . . . 7
Σ^
Σ^
|
130 | 129 | eqcomd 2628 |
. . . . . 6
Σ^ Σ^ |
131 | 68, 130 | eqtrd 2656 |
. . . . 5
Σ^
Σ^
Σ^ |
132 | | sge0iunmptlemre.a |
. . . . . . . . 9
|
133 | 77 | ssriv 3607 |
. . . . . . . . . 10
|
134 | 133 | a1i 11 |
. . . . . . . . 9
|
135 | 132, 134 | ssexd 4805 |
. . . . . . . 8
|
136 | | vex 3203 |
. . . . . . . . . . . . 13
|
137 | 136 | inex2 4800 |
. . . . . . . . . . . 12
|
138 | 137 | a1i 11 |
. . . . . . . . . . 11
|
139 | | icossicc 12260 |
. . . . . . . . . . . . 13
|
140 | | simpll 790 |
. . . . . . . . . . . . . 14
|
141 | | simplr 792 |
. . . . . . . . . . . . . 14
|
142 | 79 | adantl 482 |
. . . . . . . . . . . . . 14
|
143 | 140, 141,
142, 92 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
144 | 139, 143 | sseldi 3601 |
. . . . . . . . . . . 12
|
145 | | eqid 2622 |
. . . . . . . . . . . 12
|
146 | 144, 145 | fmptd 6385 |
. . . . . . . . . . 11
|
147 | 138, 146 | sge0cl 40598 |
. . . . . . . . . 10
Σ^ |
148 | 77, 147 | sylan2 491 |
. . . . . . . . 9
Σ^
|
149 | | nfcv 2764 |
. . . . . . . . . 10
Σ^ |
150 | | nfcv 2764 |
. . . . . . . . . . 11
Σ^ |
151 | 116, 117 | nfmpt 4746 |
. . . . . . . . . . 11
|
152 | 150, 151 | nffv 6198 |
. . . . . . . . . 10
Σ^
|
153 | 119 | mpteq1d 4738 |
. . . . . . . . . . 11
|
154 | 153 | fveq2d 6195 |
. . . . . . . . . 10
Σ^ Σ^ |
155 | 113, 114,
149, 152, 154 | cbvmptf 4748 |
. . . . . . . . 9
Σ^ Σ^ |
156 | 148, 155 | fmptd 6385 |
. . . . . . . 8
Σ^ |
157 | 135, 156 | sge0xrcl 40602 |
. . . . . . 7
Σ^ Σ^ |
158 | 157 | adantr 481 |
. . . . . 6
Σ^
Σ^ |
159 | | eqid 2622 |
. . . . . . . . 9
Σ^
Σ^
|
160 | 147, 159 | fmptd 6385 |
. . . . . . . 8
Σ^
|
161 | 132, 160 | sge0xrcl 40602 |
. . . . . . 7
Σ^ Σ^
|
162 | 161 | adantr 481 |
. . . . . 6
Σ^ Σ^ |
163 | 55, 2 | syl 17 |
. . . . . 6
Σ^ Σ^ |
164 | 155 | fveq2i 6194 |
. . . . . . . . 9
Σ^ Σ^ Σ^ Σ^ |
165 | 164 | a1i 11 |
. . . . . . . 8
Σ^ Σ^ Σ^ Σ^ |
166 | 132, 147,
134 | sge0lessmpt 40616 |
. . . . . . . 8
Σ^ Σ^ Σ^ Σ^
|
167 | 165, 166 | eqbrtrd 4675 |
. . . . . . 7
Σ^ Σ^ Σ^ Σ^
|
168 | 167 | adantr 481 |
. . . . . 6
Σ^
Σ^
Σ^ Σ^
|
169 | 149, 152,
154 | cbvmpt 4749 |
. . . . . . . . . . 11
Σ^ Σ^
|
170 | 169 | eqcomi 2631 |
. . . . . . . . . 10
Σ^
Σ^ |
171 | 170 | fveq2i 6194 |
. . . . . . . . 9
Σ^ Σ^
Σ^ Σ^ |
172 | 171 | a1i 11 |
. . . . . . . 8
Σ^ Σ^
Σ^ Σ^ |
173 | 136 | inex2 4800 |
. . . . . . . . . . 11
|
174 | 173 | a1i 11 |
. . . . . . . . . 10
|
175 | 107, 30 | sylan2 491 |
. . . . . . . . . . 11
|
176 | | eqid 2622 |
. . . . . . . . . . 11
|
177 | 175, 176 | fmptd 6385 |
. . . . . . . . . 10
|
178 | 174, 177 | sge0cl 40598 |
. . . . . . . . 9
Σ^ |
179 | 33, 31 | sge0cl 40598 |
. . . . . . . . 9
Σ^ |
180 | | inss1 3833 |
. . . . . . . . . . 11
|
181 | 180 | a1i 11 |
. . . . . . . . . 10
|
182 | 33, 30, 181 | sge0lessmpt 40616 |
. . . . . . . . 9
Σ^ Σ^ |
183 | 13, 132, 178, 179, 182 | sge0lempt 40627 |
. . . . . . . 8
Σ^ Σ^
Σ^ Σ^ |
184 | 172, 183 | eqbrtrd 4675 |
. . . . . . 7
Σ^ Σ^
Σ^ Σ^ |
185 | 184 | adantr 481 |
. . . . . 6
Σ^ Σ^ Σ^ Σ^ |
186 | 158, 162,
163, 168, 185 | xrletrd 11993 |
. . . . 5
Σ^
Σ^
Σ^ Σ^ |
187 | 131, 186 | eqbrtrd 4675 |
. . . 4
Σ^
Σ^ Σ^ |
188 | 187 | ralrimiva 2966 |
. . 3
Σ^ Σ^ Σ^ |
189 | | sge0iunmptlemre.iue |
. . . 4
|
190 | | sge0iunmptlemre.f |
. . . 4
|
191 | 189, 190,
2 | sge0lefi 40615 |
. . 3
Σ^
Σ^ Σ^ Σ^ Σ^ Σ^ |
192 | 188, 191 | mpbird 247 |
. 2
Σ^
Σ^ Σ^ |
193 | | elpwinss 39216 |
. . . . . . . . 9
|
194 | 193 | resmptd 5452 |
. . . . . . . 8
Σ^ Σ^ |
195 | 194 | fveq2d 6195 |
. . . . . . 7
Σ^ Σ^ Σ^ Σ^ |
196 | 195 | adantl 482 |
. . . . . 6
Σ^ Σ^ Σ^ Σ^ |
197 | | elinel2 3800 |
. . . . . . . 8
|
198 | 197 | adantl 482 |
. . . . . . 7
|
199 | | 0xr 10086 |
. . . . . . . . 9
|
200 | 199 | a1i 11 |
. . . . . . . 8
|
201 | | pnfxr 10092 |
. . . . . . . . 9
|
202 | 201 | a1i 11 |
. . . . . . . 8
|
203 | | simpll 790 |
. . . . . . . . . 10
|
204 | 193 | sselda 3603 |
. . . . . . . . . . 11
|
205 | 204 | adantll 750 |
. . . . . . . . . 10
|
206 | 203, 205,
33 | syl2anc 693 |
. . . . . . . . 9
|
207 | 203, 205,
31 | syl2anc 693 |
. . . . . . . . 9
|
208 | 206, 207 | sge0xrcl 40602 |
. . . . . . . 8
Σ^ |
209 | 206, 207 | sge0ge0 40601 |
. . . . . . . 8
Σ^ |
210 | 203, 205,
35 | syl2anc 693 |
. . . . . . . . 9
Σ^ |
211 | | ltpnf 11954 |
. . . . . . . . 9
Σ^ Σ^ |
212 | 210, 211 | syl 17 |
. . . . . . . 8
Σ^ |
213 | 200, 202,
208, 209, 212 | elicod 12224 |
. . . . . . 7
Σ^ |
214 | 198, 213 | sge0fsummpt 40607 |
. . . . . 6
Σ^ Σ^ Σ^ |
215 | 196, 214 | eqtrd 2656 |
. . . . 5
Σ^ Σ^
Σ^ |
216 | | nfv 1843 |
. . . . . 6
|
217 | 189 | adantr 481 |
. . . . . 6
|
218 | 190 | mptex2 6384 |
. . . . . . 7
|
219 | 218 | adantlr 751 |
. . . . . 6
|
220 | 198, 210 | fsumrecl 14465 |
. . . . . . 7
Σ^ |
221 | 220 | rexrd 10089 |
. . . . . 6
Σ^ |
222 | | nfv 1843 |
. . . . . . . 8
|
223 | | iunss1 4532 |
. . . . . . . . . . . 12
|
224 | 193, 223 | syl 17 |
. . . . . . . . . . 11
|
225 | 224 | adantl 482 |
. . . . . . . . . 10
|
226 | 217, 225 | ssexd 4805 |
. . . . . . . . 9
|
227 | 226 | adantr 481 |
. . . . . . . 8
|
228 | | simpll 790 |
. . . . . . . . . 10
|
229 | 225 | sselda 3603 |
. . . . . . . . . 10
|
230 | 228, 229,
218 | syl2anc 693 |
. . . . . . . . 9
|
231 | 230 | adantlr 751 |
. . . . . . . 8
|
232 | | simpr 477 |
. . . . . . . 8
|
233 | 193 | adantl 482 |
. . . . . . . . . . . 12
|
234 | 57 | adantr 481 |
. . . . . . . . . . . 12
Disj |
235 | | disjss1 4626 |
. . . . . . . . . . . 12
Disj Disj |
236 | 233, 234,
235 | sylc 65 |
. . . . . . . . . . 11
Disj |
237 | 203 | 3adant3 1081 |
. . . . . . . . . . . 12
|
238 | 205 | 3adant3 1081 |
. . . . . . . . . . . 12
|
239 | | simp3 1063 |
. . . . . . . . . . . 12
|
240 | 237, 238,
239, 25 | syl3anc 1326 |
. . . . . . . . . . 11
|
241 | 198, 206,
236, 240, 210 | sge0iunmptlemfi 40630 |
. . . . . . . . . 10
Σ^
Σ^ Σ^ |
242 | 214, 220 | eqeltrd 2701 |
. . . . . . . . . 10
Σ^ Σ^ |
243 | 241, 242 | eqeltrd 2701 |
. . . . . . . . 9
Σ^
|
244 | 243 | adantr 481 |
. . . . . . . 8
Σ^
|
245 | 222, 227,
231, 232, 244 | sge0ltfirpmpt 40625 |
. . . . . . 7
Σ^
Σ^ |
246 | | nfv 1843 |
. . . . . . . 8
|
247 | | nfre1 3005 |
. . . . . . . 8
Σ^ Σ^ |
248 | | sspwb 4917 |
. . . . . . . . . . . . . . . . . 18
|
249 | 248 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
|
250 | 223, 249 | syl 17 |
. . . . . . . . . . . . . . . 16
|
251 | 193, 250 | syl 17 |
. . . . . . . . . . . . . . 15
|
252 | 251 | adantr 481 |
. . . . . . . . . . . . . 14
|
253 | | elinel1 3799 |
. . . . . . . . . . . . . . 15
|
254 | 253 | adantl 482 |
. . . . . . . . . . . . . 14
|
255 | 252, 254 | sseldd 3604 |
. . . . . . . . . . . . 13
|
256 | | elinel2 3800 |
. . . . . . . . . . . . . 14
|
257 | 256 | adantl 482 |
. . . . . . . . . . . . 13
|
258 | 255, 257 | elind 3798 |
. . . . . . . . . . . 12
|
259 | 258 | ad4ant24 1298 |
. . . . . . . . . . 11
|
260 | 259 | 3adant3 1081 |
. . . . . . . . . 10
Σ^
Σ^ |
261 | 221 | ad2antrr 762 |
. . . . . . . . . . . 12
Σ^ |
262 | 261 | 3adant3 1081 |
. . . . . . . . . . 11
Σ^
Σ^ Σ^ |
263 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
264 | 226 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
265 | 230 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
266 | 243 | adantr 481 |
. . . . . . . . . . . . . . . 16
Σ^
|
267 | 253 | elpwid 4170 |
. . . . . . . . . . . . . . . . 17
|
268 | 267 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
269 | 263, 264,
265, 266, 268 | sge0ssrempt 40622 |
. . . . . . . . . . . . . . 15
Σ^ |
270 | 269 | rexrd 10089 |
. . . . . . . . . . . . . 14
Σ^ |
271 | 270 | adantlr 751 |
. . . . . . . . . . . . 13
Σ^ |
272 | | rpxr 11840 |
. . . . . . . . . . . . . 14
|
273 | 272 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
274 | 271, 273 | xaddcld 12131 |
. . . . . . . . . . . 12
Σ^ |
275 | 274 | 3adant3 1081 |
. . . . . . . . . . 11
Σ^
Σ^ Σ^ |
276 | | simp3 1063 |
. . . . . . . . . . . 12
Σ^
Σ^ Σ^
Σ^ |
277 | 241, 214 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
Σ^ Σ^
|
278 | 277 | adantr 481 |
. . . . . . . . . . . . . 14
Σ^ Σ^
|
279 | 278 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Σ^
Σ^ Σ^ Σ^
|
280 | 269 | adantlr 751 |
. . . . . . . . . . . . . . 15
Σ^ |
281 | | rpre 11839 |
. . . . . . . . . . . . . . . 16
|
282 | 281 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
|
283 | | rexadd 12063 |
. . . . . . . . . . . . . . 15
Σ^ Σ^ Σ^ |
284 | 280, 282,
283 | syl2anc 693 |
. . . . . . . . . . . . . 14
Σ^ Σ^ |
285 | 284 | 3adant3 1081 |
. . . . . . . . . . . . 13
Σ^
Σ^ Σ^ Σ^ |
286 | 279, 285 | breq12d 4666 |
. . . . . . . . . . . 12
Σ^
Σ^ Σ^ Σ^
Σ^
Σ^ |
287 | 276, 286 | mpbird 247 |
. . . . . . . . . . 11
Σ^
Σ^ Σ^ Σ^ |
288 | 262, 275,
287 | xrltled 39486 |
. . . . . . . . . 10
Σ^
Σ^ Σ^ Σ^ |
289 | | rspe 3003 |
. . . . . . . . . 10
Σ^ Σ^ Σ^ Σ^ |
290 | 260, 288,
289 | syl2anc 693 |
. . . . . . . . 9
Σ^
Σ^
Σ^ Σ^ |
291 | 290 | 3exp 1264 |
. . . . . . . 8
Σ^
Σ^
Σ^ Σ^ |
292 | 246, 247,
291 | rexlimd 3026 |
. . . . . . 7
Σ^
Σ^
Σ^ Σ^ |
293 | 245, 292 | mpd 15 |
. . . . . 6
Σ^ Σ^ |
294 | 216, 217,
219, 221, 293 | sge0gerpmpt 40619 |
. . . . 5
Σ^ Σ^
|
295 | 215, 294 | eqbrtrd 4675 |
. . . 4
Σ^ Σ^ Σ^
|
296 | 295 | ralrimiva 2966 |
. . 3
Σ^ Σ^ Σ^
|
297 | | eqid 2622 |
. . . . 5
Σ^ Σ^ |
298 | 179, 297 | fmptd 6385 |
. . . 4
Σ^ |
299 | 132, 298,
1 | sge0lefi 40615 |
. . 3
Σ^ Σ^
Σ^
Σ^ Σ^ Σ^
|
300 | 296, 299 | mpbird 247 |
. 2
Σ^ Σ^
Σ^
|
301 | 1, 2, 192, 300 | xrletrid 11986 |
1
Σ^
Σ^ Σ^ |