Step | Hyp | Ref
| Expression |
1 | | sge0le.x |
. . . . . 6
|
2 | | sge0le.F |
. . . . . 6
|
3 | 1, 2 | sge0xrcl 40602 |
. . . . 5
Σ^ |
4 | | pnfge 11964 |
. . . . 5
Σ^ Σ^
|
5 | 3, 4 | syl 17 |
. . . 4
Σ^ |
6 | 5 | adantr 481 |
. . 3
Σ^ Σ^ |
7 | | id 22 |
. . . . 5
Σ^ Σ^ |
8 | 7 | eqcomd 2628 |
. . . 4
Σ^ Σ^ |
9 | 8 | adantl 482 |
. . 3
Σ^
Σ^ |
10 | 6, 9 | breqtrd 4679 |
. 2
Σ^ Σ^ Σ^ |
11 | | elinel2 3800 |
. . . . . . . 8
|
12 | 11 | adantl 482 |
. . . . . . 7
Σ^ |
13 | 2 | adantr 481 |
. . . . . . . . . 10
Σ^ |
14 | 1 | adantr 481 |
. . . . . . . . . . . . 13
|
15 | | sge0le.g |
. . . . . . . . . . . . . 14
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . 13
|
17 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
18 | 2 | ffnd 6046 |
. . . . . . . . . . . . . . . . 17
|
19 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . 17
|
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
|
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . 15
|
22 | 17, 21 | mpbid 222 |
. . . . . . . . . . . . . 14
|
23 | | iccssxr 12256 |
. . . . . . . . . . . . . . . . . . . . . 22
|
24 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
|
25 | 23, 24 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
|
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | | sge0le.le |
. . . . . . . . . . . . . . . . . . . . . 22
|
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 29, 31 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 26, 32 | xrgepnfd 39547 |
. . . . . . . . . . . . . . . . . . 19
|
34 | 33 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
35 | 15 | ffnd 6046 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 36, 37, 38 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
41 | 34, 40 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | ex 450 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
44 | 43 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
|
45 | 22, 44 | mpd 15 |
. . . . . . . . . . . . 13
|
46 | 14, 16, 45 | sge0pnfval 40590 |
. . . . . . . . . . . 12
Σ^ |
47 | 46 | adantlr 751 |
. . . . . . . . . . 11
Σ^
Σ^ |
48 | | simplr 792 |
. . . . . . . . . . 11
Σ^
Σ^ |
49 | 47, 48 | pm2.65da 600 |
. . . . . . . . . 10
Σ^ |
50 | 13, 49 | fge0iccico 40587 |
. . . . . . . . 9
Σ^ |
51 | 50 | adantr 481 |
. . . . . . . 8
Σ^ |
52 | | elpwinss 39216 |
. . . . . . . . 9
|
53 | 52 | adantl 482 |
. . . . . . . 8
Σ^ |
54 | 51, 53 | fssresd 6071 |
. . . . . . 7
Σ^ |
55 | 12, 54 | sge0fsum 40604 |
. . . . . 6
Σ^ Σ^ |
56 | | rge0ssre 12280 |
. . . . . . . 8
|
57 | 54 | ffvelrnda 6359 |
. . . . . . . 8
Σ^ |
58 | 56, 57 | sseldi 3601 |
. . . . . . 7
Σ^ |
59 | 12, 58 | fsumrecl 14465 |
. . . . . 6
Σ^
|
60 | 55, 59 | eqeltrd 2701 |
. . . . 5
Σ^ Σ^ |
61 | 15 | adantr 481 |
. . . . . . . . . 10
Σ^ |
62 | 1 | adantr 481 |
. . . . . . . . . . 11
Σ^ |
63 | | simpr 477 |
. . . . . . . . . . . 12
Σ^ Σ^ |
64 | 62, 61 | sge0repnf 40603 |
. . . . . . . . . . . 12
Σ^ Σ^ Σ^ |
65 | 63, 64 | mpbird 247 |
. . . . . . . . . . 11
Σ^ Σ^ |
66 | 62, 61, 65 | sge0rern 40605 |
. . . . . . . . . 10
Σ^ |
67 | 61, 66 | fge0iccico 40587 |
. . . . . . . . 9
Σ^ |
68 | 67 | adantr 481 |
. . . . . . . 8
Σ^ |
69 | 68, 53 | fssresd 6071 |
. . . . . . 7
Σ^ |
70 | 12, 69 | sge0fsum 40604 |
. . . . . 6
Σ^ Σ^ |
71 | 69 | ffvelrnda 6359 |
. . . . . . . 8
Σ^ |
72 | 56, 71 | sseldi 3601 |
. . . . . . 7
Σ^ |
73 | 12, 72 | fsumrecl 14465 |
. . . . . 6
Σ^
|
74 | 70, 73 | eqeltrd 2701 |
. . . . 5
Σ^ Σ^ |
75 | 65 | adantr 481 |
. . . . 5
Σ^ Σ^ |
76 | | simplll 798 |
. . . . . . . . 9
Σ^ |
77 | 53 | sselda 3603 |
. . . . . . . . 9
Σ^ |
78 | 76, 77, 30 | syl2anc 693 |
. . . . . . . 8
Σ^ |
79 | | fvres 6207 |
. . . . . . . . . 10
|
80 | 79 | adantl 482 |
. . . . . . . . 9
Σ^ |
81 | | fvres 6207 |
. . . . . . . . . 10
|
82 | 81 | adantl 482 |
. . . . . . . . 9
Σ^ |
83 | 80, 82 | breq12d 4666 |
. . . . . . . 8
Σ^
|
84 | 78, 83 | mpbird 247 |
. . . . . . 7
Σ^ |
85 | 12, 58, 72, 84 | fsumle 14531 |
. . . . . 6
Σ^
|
86 | 55, 70 | breq12d 4666 |
. . . . . 6
Σ^ Σ^ Σ^
|
87 | 85, 86 | mpbird 247 |
. . . . 5
Σ^ Σ^ Σ^ |
88 | 1 | adantr 481 |
. . . . . . 7
|
89 | 15 | adantr 481 |
. . . . . . 7
|
90 | 88, 89 | sge0less 40609 |
. . . . . 6
Σ^ Σ^ |
91 | 90 | adantlr 751 |
. . . . 5
Σ^ Σ^ Σ^ |
92 | 60, 74, 75, 87, 91 | letrd 10194 |
. . . 4
Σ^ Σ^ Σ^ |
93 | 92 | ralrimiva 2966 |
. . 3
Σ^ Σ^ Σ^ |
94 | 62, 61 | sge0xrcl 40602 |
. . . 4
Σ^ Σ^ |
95 | 62, 13, 94 | sge0lefi 40615 |
. . 3
Σ^ Σ^ Σ^ Σ^ Σ^ |
96 | 93, 95 | mpbird 247 |
. 2
Σ^ Σ^ Σ^ |
97 | 10, 96 | pm2.61dan 832 |
1
Σ^ Σ^ |