Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . 3
|
2 | | sge0xaddlem2.a |
. . 3
|
3 | | 0xr 10086 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | | pnfxr 10092 |
. . . . 5
|
6 | 5 | a1i 11 |
. . . 4
|
7 | | rge0ssre 12280 |
. . . . . . 7
|
8 | | sge0xaddlem2.b |
. . . . . . 7
|
9 | 7, 8 | sseldi 3601 |
. . . . . 6
|
10 | | sge0xaddlem2.c |
. . . . . . 7
|
11 | 7, 10 | sseldi 3601 |
. . . . . 6
|
12 | 9, 11 | readdcld 10069 |
. . . . 5
|
13 | 12 | rexrd 10089 |
. . . 4
|
14 | | icossicc 12260 |
. . . . . . 7
|
15 | 14, 8 | sseldi 3601 |
. . . . . 6
|
16 | | xrge0ge0 39563 |
. . . . . 6
|
17 | 15, 16 | syl 17 |
. . . . 5
|
18 | 14, 10 | sseldi 3601 |
. . . . . 6
|
19 | | xrge0ge0 39563 |
. . . . . 6
|
20 | 18, 19 | syl 17 |
. . . . 5
|
21 | 9, 11, 17, 20 | addge0d 10603 |
. . . 4
|
22 | 12 | ltpnfd 11955 |
. . . 4
|
23 | 4, 6, 13, 21, 22 | elicod 12224 |
. . 3
|
24 | 1, 2, 23 | sge0revalmpt 40595 |
. 2
Σ^
|
25 | | rexadd 12063 |
. . . . 5
|
26 | 9, 11, 25 | syl2anc 693 |
. . . 4
|
27 | 26 | mpteq2dva 4744 |
. . 3
|
28 | 27 | fveq2d 6195 |
. 2
Σ^ Σ^ |
29 | | sge0xaddlem2.sb |
. . . 4
Σ^ |
30 | | sge0xaddlem2.sc |
. . . 4
Σ^ |
31 | | rexadd 12063 |
. . . 4
Σ^ Σ^ Σ^ Σ^ Σ^ Σ^ |
32 | 29, 30, 31 | syl2anc 693 |
. . 3
Σ^ Σ^ Σ^ Σ^ |
33 | 1, 2, 8 | sge0revalmpt 40595 |
. . . 4
Σ^ |
34 | 1, 2, 10 | sge0revalmpt 40595 |
. . . 4
Σ^ |
35 | 33, 34 | oveq12d 6668 |
. . 3
Σ^ Σ^ |
36 | 33 | eqcomd 2628 |
. . . . . . 7
Σ^ |
37 | 36, 29 | eqeltrd 2701 |
. . . . . 6
|
38 | 34, 30 | eqeltrrd 2702 |
. . . . . 6
|
39 | 37, 38 | readdcld 10069 |
. . . . 5
|
40 | 39 | rexrd 10089 |
. . . 4
|
41 | | elinel2 3800 |
. . . . . . . . . 10
|
42 | 41 | adantl 482 |
. . . . . . . . 9
|
43 | | simpll 790 |
. . . . . . . . . . 11
|
44 | | elpwinss 39216 |
. . . . . . . . . . . . . 14
|
45 | 44 | adantr 481 |
. . . . . . . . . . . . 13
|
46 | | simpr 477 |
. . . . . . . . . . . . 13
|
47 | 45, 46 | sseldd 3604 |
. . . . . . . . . . . 12
|
48 | 47 | adantll 750 |
. . . . . . . . . . 11
|
49 | 43, 48, 9 | syl2anc 693 |
. . . . . . . . . 10
|
50 | 43, 48, 11 | syl2anc 693 |
. . . . . . . . . 10
|
51 | 49, 50 | readdcld 10069 |
. . . . . . . . 9
|
52 | 42, 51 | fsumrecl 14465 |
. . . . . . . 8
|
53 | 52 | rexrd 10089 |
. . . . . . 7
|
54 | 53 | ralrimiva 2966 |
. . . . . 6
|
55 | | eqid 2622 |
. . . . . . 7
|
56 | 55 | rnmptss 6392 |
. . . . . 6
|
57 | 54, 56 | syl 17 |
. . . . 5
|
58 | | supxrcl 12145 |
. . . . 5
|
59 | 57, 58 | syl 17 |
. . . 4
|
60 | 35 | eqcomd 2628 |
. . . . . . 7
Σ^ Σ^ |
61 | 60 | adantr 481 |
. . . . . 6
Σ^ Σ^ |
62 | | nfv 1843 |
. . . . . . . 8
|
63 | 2 | adantr 481 |
. . . . . . . 8
|
64 | 15 | adantlr 751 |
. . . . . . . 8
|
65 | | rphalfcl 11858 |
. . . . . . . . 9
|
66 | 65 | adantl 482 |
. . . . . . . 8
|
67 | 29 | adantr 481 |
. . . . . . . 8
Σ^ |
68 | 62, 63, 64, 66, 67 | sge0ltfirpmpt2 40643 |
. . . . . . 7
Σ^
|
69 | 18 | adantlr 751 |
. . . . . . . . . . . 12
|
70 | 30 | adantr 481 |
. . . . . . . . . . . 12
Σ^ |
71 | 62, 63, 69, 66, 70 | sge0ltfirpmpt2 40643 |
. . . . . . . . . . 11
Σ^ |
72 | 71 | 3ad2ant1 1082 |
. . . . . . . . . 10
Σ^
Σ^ |
73 | 63 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
Σ^
|
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
75 | | simpl1l 1112 |
. . . . . . . . . . . . . . . 16
Σ^
|
76 | 75 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
77 | | simpr 477 |
. . . . . . . . . . . . . . 15
Σ^
Σ^ |
78 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
79 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
80 | 79 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
81 | 78, 80 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
82 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
|
84 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
86 | 83, 85 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
87 | 81, 86, 8 | chvar 2262 |
. . . . . . . . . . . . . . 15
|
88 | 76, 77, 87 | syl2anc 693 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
89 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
90 | 89 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
|
91 | 78, 90 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
92 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
94 | 83, 93 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
95 | 91, 94, 10 | chvar 2262 |
. . . . . . . . . . . . . . 15
|
96 | 76, 77, 95 | syl2anc 693 |
. . . . . . . . . . . . . 14
Σ^
Σ^ |
97 | | simp11r 1173 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
98 | | simp12 1092 |
. . . . . . . . . . . . . . 15
Σ^
Σ^
|
99 | | elpwinss 39216 |
. . . . . . . . . . . . . . 15
|
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
101 | | elinel2 3800 |
. . . . . . . . . . . . . . . 16
|
102 | 101 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
Σ^
|
103 | 102 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
104 | | simp2 1062 |
. . . . . . . . . . . . . . 15
Σ^
Σ^
|
105 | | elpwinss 39216 |
. . . . . . . . . . . . . . 15
|
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
107 | | elinel2 3800 |
. . . . . . . . . . . . . . 15
|
108 | 107 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
109 | | simp13 1093 |
. . . . . . . . . . . . . . 15
Σ^
Σ^
Σ^
|
110 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
111 | 110, 79, 84 | cbvmpt 4749 |
. . . . . . . . . . . . . . . . . 18
|
112 | 111 | fveq2i 6194 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
113 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
114 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 84, 113, 114, 110, 79 | cbvsum 14425 |
. . . . . . . . . . . . . . . . . 18
|
116 | 115 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
117 | 112, 116 | breq12i 4662 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^
|
118 | 117 | biimpi 206 |
. . . . . . . . . . . . . . 15
Σ^ Σ^
|
119 | 109, 118 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
Σ^
|
120 | | simp3 1063 |
. . . . . . . . . . . . . . 15
Σ^
Σ^
Σ^ |
121 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
122 | 121, 89, 92 | cbvmpt 4749 |
. . . . . . . . . . . . . . . . . 18
|
123 | 122 | fveq2i 6194 |
. . . . . . . . . . . . . . . . 17
Σ^ Σ^ |
124 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
125 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
126 | 92, 124, 125, 121, 89 | cbvsum 14425 |
. . . . . . . . . . . . . . . . . 18
|
127 | 126 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
128 | 123, 127 | breq12i 4662 |
. . . . . . . . . . . . . . . 16
Σ^
Σ^
|
129 | 128 | biimpi 206 |
. . . . . . . . . . . . . . 15
Σ^ Σ^
|
130 | 120, 129 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
Σ^
|
131 | | simp11l 1172 |
. . . . . . . . . . . . . . 15
Σ^
Σ^
|
132 | 84, 92 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
133 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
134 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
135 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
136 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
137 | 79, 136, 89 | nfov 6676 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
138 | 132, 133,
134, 135, 137 | cbvsum 14425 |
. . . . . . . . . . . . . . . . . . . . . 22
|
139 | 138 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . . . . . 21
|
140 | 139 | rneqi 5352 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 140 | supeq1i 8353 |
. . . . . . . . . . . . . . . . . . 19
|
142 | 141 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
|
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
144 | 143, 24 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
Σ^ |
145 | | ge0xaddcl 12286 |
. . . . . . . . . . . . . . . . . . 19
|
146 | 15, 18, 145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
147 | 26, 146 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
|
148 | 1, 2, 147 | sge0clmpt 40642 |
. . . . . . . . . . . . . . . 16
Σ^ |
149 | 144, 148 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
150 | 131, 149 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
|
151 | 112, 29 | syl5eqelr 2706 |
. . . . . . . . . . . . . . 15
Σ^ |
152 | 131, 151 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
Σ^ |
153 | 123, 30 | syl5eqelr 2706 |
. . . . . . . . . . . . . . 15
Σ^ |
154 | 131, 153 | syl 17 |
. . . . . . . . . . . . . 14
Σ^
Σ^
Σ^ |
155 | 74, 88, 96, 97, 100, 103, 106, 108, 119, 130, 150, 152, 154 | sge0xaddlem1 40650 |
. . . . . . . . . . . . 13
Σ^
Σ^
Σ^ Σ^
|
156 | 112, 123 | oveq12i 6662 |
. . . . . . . . . . . . . 14
Σ^ Σ^ Σ^ Σ^ |
157 | 141 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
158 | 156, 157 | breq12i 4662 |
. . . . . . . . . . . . 13
Σ^ Σ^
Σ^ Σ^
|
159 | 155, 158 | sylibr 224 |
. . . . . . . . . . . 12
Σ^
Σ^
Σ^ Σ^
|
160 | 159 | 3exp 1264 |
. . . . . . . . . . 11
Σ^
Σ^ Σ^ Σ^
|
161 | 160 | rexlimdv 3030 |
. . . . . . . . . 10
Σ^
Σ^ Σ^ Σ^
|
162 | 72, 161 | mpd 15 |
. . . . . . . . 9
Σ^
Σ^ Σ^
|
163 | 162 | 3exp 1264 |
. . . . . . . 8
Σ^ Σ^ Σ^
|
164 | 163 | rexlimdv 3030 |
. . . . . . 7
Σ^ Σ^ Σ^
|
165 | 68, 164 | mpd 15 |
. . . . . 6
Σ^ Σ^
|
166 | 61, 165 | eqbrtrd 4675 |
. . . . 5
|
167 | 40, 59, 166 | xrlexaddrp 39568 |
. . . 4
|
168 | 24 | eqcomd 2628 |
. . . . 5
Σ^ |
169 | 43, 48, 23 | syl2anc 693 |
. . . . . . . . . 10
|
170 | 42, 169 | sge0fsummpt 40607 |
. . . . . . . . 9
Σ^
|
171 | 49 | recnd 10068 |
. . . . . . . . . 10
|
172 | 50 | recnd 10068 |
. . . . . . . . . 10
|
173 | 42, 171, 172 | fsumadd 14470 |
. . . . . . . . 9
|
174 | 170, 173 | eqtrd 2656 |
. . . . . . . 8
Σ^
|
175 | 42, 49 | fsumrecl 14465 |
. . . . . . . . 9
|
176 | 42, 50 | fsumrecl 14465 |
. . . . . . . . 9
|
177 | 37 | adantr 481 |
. . . . . . . . 9
|
178 | 38 | adantr 481 |
. . . . . . . . 9
|
179 | | elinel2 3800 |
. . . . . . . . . . . . . . . 16
|
180 | 179 | adantl 482 |
. . . . . . . . . . . . . . 15
|
181 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
182 | | elpwinss 39216 |
. . . . . . . . . . . . . . . . . . 19
|
183 | 182 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
184 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
185 | 183, 184 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
|
186 | 185 | adantll 750 |
. . . . . . . . . . . . . . . 16
|
187 | 181, 186,
9 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
188 | 180, 187 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
|
189 | 188 | rexrd 10089 |
. . . . . . . . . . . . 13
|
190 | 189 | ralrimiva 2966 |
. . . . . . . . . . . 12
|
191 | | eqid 2622 |
. . . . . . . . . . . . 13
|
192 | 191 | rnmptss 6392 |
. . . . . . . . . . . 12
|
193 | 190, 192 | syl 17 |
. . . . . . . . . . 11
|
194 | 193 | adantr 481 |
. . . . . . . . . 10
|
195 | | simpr 477 |
. . . . . . . . . . . 12
|
196 | | eqidd 2623 |
. . . . . . . . . . . 12
|
197 | | sumeq1 14419 |
. . . . . . . . . . . . . 14
|
198 | 197 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
199 | 198 | rspcev 3309 |
. . . . . . . . . . . 12
|
200 | 195, 196,
199 | syl2anc 693 |
. . . . . . . . . . 11
|
201 | 175 | elexd 3214 |
. . . . . . . . . . 11
|
202 | 191, 200,
201 | elrnmptd 39366 |
. . . . . . . . . 10
|
203 | | supxrub 12154 |
. . . . . . . . . 10
|
204 | 194, 202,
203 | syl2anc 693 |
. . . . . . . . 9
|
205 | | nfv 1843 |
. . . . . . . . . . . 12
|
206 | | eqid 2622 |
. . . . . . . . . . . 12
|
207 | | elinel2 3800 |
. . . . . . . . . . . . . . 15
|
208 | 207 | adantl 482 |
. . . . . . . . . . . . . 14
|
209 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
210 | | elpwinss 39216 |
. . . . . . . . . . . . . . . . . 18
|
211 | 210 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
212 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
213 | 211, 212 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
|
214 | 213 | adantll 750 |
. . . . . . . . . . . . . . 15
|
215 | 209, 214,
11 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
216 | 208, 215 | fsumrecl 14465 |
. . . . . . . . . . . . 13
|
217 | 216 | rexrd 10089 |
. . . . . . . . . . . 12
|
218 | 205, 206,
217 | rnmptssd 39385 |
. . . . . . . . . . 11
|
219 | 218 | adantr 481 |
. . . . . . . . . 10
|
220 | | eqidd 2623 |
. . . . . . . . . . . 12
|
221 | | sumeq1 14419 |
. . . . . . . . . . . . . 14
|
222 | 221 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
223 | 222 | rspcev 3309 |
. . . . . . . . . . . 12
|
224 | 195, 220,
223 | syl2anc 693 |
. . . . . . . . . . 11
|
225 | 176 | elexd 3214 |
. . . . . . . . . . 11
|
226 | 206, 224,
225 | elrnmptd 39366 |
. . . . . . . . . 10
|
227 | | supxrub 12154 |
. . . . . . . . . 10
|
228 | 219, 226,
227 | syl2anc 693 |
. . . . . . . . 9
|
229 | 175, 176,
177, 178, 204, 228 | le2addd 10646 |
. . . . . . . 8
|
230 | 174, 229 | eqbrtrd 4675 |
. . . . . . 7
Σ^
|
231 | 230 | ralrimiva 2966 |
. . . . . 6
Σ^ |
232 | 1, 2, 147, 40 | sge0lefimpt 40640 |
. . . . . 6
Σ^
Σ^ |
233 | 231, 232 | mpbird 247 |
. . . . 5
Σ^ |
234 | 168, 233 | eqbrtrd 4675 |
. . . 4
|
235 | 40, 59, 167, 234 | xrletrid 11986 |
. . 3
|
236 | 32, 35, 235 | 3eqtrd 2660 |
. 2
Σ^ Σ^
|
237 | 24, 28, 236 | 3eqtr4d 2666 |
1
Σ^ Σ^ Σ^ |