Step | Hyp | Ref
| Expression |
1 | | snex 4908 |
. . . . 5
|
2 | 1 | a1i 11 |
. . . 4
|
3 | | sge0sn.2 |
. . . . 5
|
4 | 3 | adantr 481 |
. . . 4
|
5 | | id 22 |
. . . . . . 7
|
6 | 5 | eqcomd 2628 |
. . . . . 6
|
7 | 6 | adantl 482 |
. . . . 5
|
8 | | ffun 6048 |
. . . . . . . 8
|
9 | 3, 8 | syl 17 |
. . . . . . 7
|
10 | 9 | adantr 481 |
. . . . . 6
|
11 | | sge0sn.1 |
. . . . . . . . 9
|
12 | | snidg 4206 |
. . . . . . . . 9
|
13 | 11, 12 | syl 17 |
. . . . . . . 8
|
14 | | fdm 6051 |
. . . . . . . . . 10
|
15 | 3, 14 | syl 17 |
. . . . . . . . 9
|
16 | 15 | eqcomd 2628 |
. . . . . . . 8
|
17 | 13, 16 | eleqtrd 2703 |
. . . . . . 7
|
18 | 17 | adantr 481 |
. . . . . 6
|
19 | | fvelrn 6352 |
. . . . . 6
|
20 | 10, 18, 19 | syl2anc 693 |
. . . . 5
|
21 | 7, 20 | eqeltrd 2701 |
. . . 4
|
22 | 2, 4, 21 | sge0pnfval 40590 |
. . 3
Σ^ |
23 | | simpr 477 |
. . 3
|
24 | 22, 23 | eqtr4d 2659 |
. 2
Σ^ |
25 | 1 | a1i 11 |
. . . 4
|
26 | 3 | adantr 481 |
. . . . 5
|
27 | | elsni 4194 |
. . . . . . . . 9
|
28 | 27 | eqcomd 2628 |
. . . . . . . 8
|
29 | 28 | con3i 150 |
. . . . . . 7
|
30 | 29 | adantl 482 |
. . . . . 6
|
31 | 11, 3 | rnsnf 39370 |
. . . . . . . 8
|
32 | 31 | eqcomd 2628 |
. . . . . . 7
|
33 | 32 | adantr 481 |
. . . . . 6
|
34 | 30, 33 | neleqtrd 2722 |
. . . . 5
|
35 | 26, 34 | fge0iccico 40587 |
. . . 4
|
36 | 25, 35 | sge0reval 40589 |
. . 3
Σ^
|
37 | | sum0 14452 |
. . . . . . . 8
|
38 | 37 | eqcomi 2631 |
. . . . . . 7
|
39 | 38 | a1i 11 |
. . . . . 6
|
40 | | nfcvd 2765 |
. . . . . . . 8
|
41 | | nfv 1843 |
. . . . . . . 8
|
42 | | fveq2 6191 |
. . . . . . . . 9
|
43 | 42 | adantl 482 |
. . . . . . . 8
|
44 | 11 | adantr 481 |
. . . . . . . 8
|
45 | | rge0ssre 12280 |
. . . . . . . . . 10
|
46 | | ax-resscn 9993 |
. . . . . . . . . 10
|
47 | 45, 46 | sstri 3612 |
. . . . . . . . 9
|
48 | 44, 12 | syl 17 |
. . . . . . . . . 10
|
49 | 35, 48 | ffvelrnd 6360 |
. . . . . . . . 9
|
50 | 47, 49 | sseldi 3601 |
. . . . . . . 8
|
51 | 40, 41, 43, 44, 50 | sumsnd 39185 |
. . . . . . 7
|
52 | 51 | eqcomd 2628 |
. . . . . 6
|
53 | 39, 52 | preq12d 4276 |
. . . . 5
|
54 | 53 | supeq1d 8352 |
. . . 4
|
55 | | xrltso 11974 |
. . . . . . . 8
|
56 | 55 | a1i 11 |
. . . . . . 7
|
57 | | 0xr 10086 |
. . . . . . . 8
|
58 | 57 | a1i 11 |
. . . . . . 7
|
59 | | iccssxr 12256 |
. . . . . . . 8
|
60 | 3, 13 | ffvelrnd 6360 |
. . . . . . . 8
|
61 | 59, 60 | sseldi 3601 |
. . . . . . 7
|
62 | | suppr 8377 |
. . . . . . 7
|
63 | 56, 58, 61, 62 | syl3anc 1326 |
. . . . . 6
|
64 | | pnfxr 10092 |
. . . . . . . . . . 11
|
65 | 64 | a1i 11 |
. . . . . . . . . 10
|
66 | 58, 65, 60 | 3jca 1242 |
. . . . . . . . 9
|
67 | | iccgelb 12230 |
. . . . . . . . 9
|
68 | 66, 67 | syl 17 |
. . . . . . . 8
|
69 | 58, 61 | xrlenltd 10104 |
. . . . . . . 8
|
70 | 68, 69 | mpbid 222 |
. . . . . . 7
|
71 | 70 | iffalsed 4097 |
. . . . . 6
|
72 | 63, 71 | eqtr2d 2657 |
. . . . 5
|
73 | 72 | adantr 481 |
. . . 4
|
74 | | pwsn 4428 |
. . . . . . . . . . . 12
|
75 | 74 | ineq1i 3810 |
. . . . . . . . . . 11
|
76 | | 0fin 8188 |
. . . . . . . . . . . . 13
|
77 | | snfi 8038 |
. . . . . . . . . . . . 13
|
78 | | prssi 4353 |
. . . . . . . . . . . . 13
|
79 | 76, 77, 78 | mp2an 708 |
. . . . . . . . . . . 12
|
80 | | df-ss 3588 |
. . . . . . . . . . . . 13
|
81 | 80 | biimpi 206 |
. . . . . . . . . . . 12
|
82 | 79, 81 | ax-mp 5 |
. . . . . . . . . . 11
|
83 | 75, 82 | eqtri 2644 |
. . . . . . . . . 10
|
84 | | mpteq1 4737 |
. . . . . . . . . 10
|
85 | 83, 84 | ax-mp 5 |
. . . . . . . . 9
|
86 | | 0ex 4790 |
. . . . . . . . . . . . 13
|
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
|
88 | 1 | a1i 11 |
. . . . . . . . . . . 12
|
89 | | sumex 14418 |
. . . . . . . . . . . . 13
|
90 | 89 | a1i 11 |
. . . . . . . . . . . 12
|
91 | | sumex 14418 |
. . . . . . . . . . . . 13
|
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
|
93 | | sumeq1 14419 |
. . . . . . . . . . . . 13
|
94 | 93 | adantl 482 |
. . . . . . . . . . . 12
|
95 | | sumeq1 14419 |
. . . . . . . . . . . . 13
|
96 | 95 | adantl 482 |
. . . . . . . . . . . 12
|
97 | 87, 88, 90, 92, 94, 96 | fmptpr 6438 |
. . . . . . . . . . 11
|
98 | 97 | trud 1493 |
. . . . . . . . . 10
|
99 | 98 | eqcomi 2631 |
. . . . . . . . 9
|
100 | 85, 99 | eqtri 2644 |
. . . . . . . 8
|
101 | 100 | rneqi 5352 |
. . . . . . 7
|
102 | | rnpropg 5615 |
. . . . . . . 8
|
103 | 86, 1, 102 | mp2an 708 |
. . . . . . 7
|
104 | 101, 103 | eqtri 2644 |
. . . . . 6
|
105 | 104 | supeq1i 8353 |
. . . . 5
|
106 | 105 | a1i 11 |
. . . 4
|
107 | 54, 73, 106 | 3eqtr4d 2666 |
. . 3
|
108 | 36, 107 | eqtr4d 2659 |
. 2
Σ^ |
109 | 24, 108 | pm2.61dan 832 |
1
Σ^ |