Step | Hyp | Ref
| Expression |
1 | | omeiunltfirp.z |
. . . . . 6
     |
2 | | fvex 5889 |
. . . . . 6
     |
3 | 1, 2 | eqeltri 2545 |
. . . . 5
 |
4 | 3 | a1i 11 |
. . . 4
 
Σ^               |
5 | | omeiunltfirp.o |
. . . . . . . 8

OutMeas |
6 | 5 | adantr 472 |
. . . . . . 7
 
 OutMeas |
7 | | omeiunltfirp.x |
. . . . . . 7

 |
8 | | omeiunltfirp.e |
. . . . . . . . 9
        |
9 | 8 | ffvelrnda 6037 |
. . . . . . . 8
 
        |
10 | | fvex 5889 |
. . . . . . . . 9
     |
11 | 10 | elpw 3948 |
. . . . . . . 8
     
      |
12 | 9, 11 | sylib 201 |
. . . . . . 7
 
       |
13 | 6, 7, 12 | omecl 38443 |
. . . . . 6
 
              |
14 | | eqid 2471 |
. . . . . 6
                     |
15 | 13, 14 | fmptd 6061 |
. . . . 5
                    |
16 | 15 | adantr 472 |
. . . 4
 
Σ^                                |
17 | | simpr 468 |
. . . 4
 
Σ^             Σ^              |
18 | | omeiunltfirp.re |
. . . . 5
    
       |
19 | 18 | adantr 472 |
. . . 4
 
Σ^                        |
20 | 4, 16, 17, 19 | sge0pnffigt 38352 |
. . 3
 
Σ^                           Σ^                |
21 | | simpl 464 |
. . . . . . 7
                Σ^               
      |
22 | | simpr 468 |
. . . . . . . . 9
        
     Σ^                  
     Σ^                |
23 | | elpwinss 37446 |
. . . . . . . . . . . 12
      |
24 | 23 | resmptd 5162 |
. . . . . . . . . . 11
                            |
25 | 24 | fveq2d 5883 |
. . . . . . . . . 10
    Σ^              Σ^              |
26 | 25 | adantr 472 |
. . . . . . . . 9
        
     Σ^               Σ^              Σ^              |
27 | 22, 26 | breqtrd 4420 |
. . . . . . . 8
        
     Σ^                  
     Σ^              |
28 | 27 | adantll 728 |
. . . . . . 7
                Σ^                  
     Σ^              |
29 | 18 | rexrd 9708 |
. . . . . . . . 9
    
       |
30 | 29 | ad2antrr 740 |
. . . . . . . 8
                Σ^                        |
31 | | simpr 468 |
. . . . . . . . . 10
 
         |
32 | 5 | ad2antrr 740 |
. . . . . . . . . . . 12
        OutMeas |
33 | 8 | ad2antrr 740 |
. . . . . . . . . . . . . 14
               |
34 | 23 | adantr 472 |
. . . . . . . . . . . . . . . 16
    

  |
35 | | simpr 468 |
. . . . . . . . . . . . . . . 16
    

  |
36 | 34, 35 | sseldd 3419 |
. . . . . . . . . . . . . . 15
    

  |
37 | 36 | adantll 728 |
. . . . . . . . . . . . . 14
          |
38 | 33, 37 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
               |
39 | 38, 11 | sylib 201 |
. . . . . . . . . . . 12
              |
40 | 32, 7, 39 | omecl 38443 |
. . . . . . . . . . 11
                     |
41 | | eqid 2471 |
. . . . . . . . . . 11
                     |
42 | 40, 41 | fmptd 6061 |
. . . . . . . . . 10
 
                       |
43 | 31, 42 | sge0xrcl 38341 |
. . . . . . . . 9
 
    Σ^              |
44 | 43 | adantr 472 |
. . . . . . . 8
                Σ^             Σ^              |
45 | | elinel2 3611 |
. . . . . . . . . . . . 13
      |
46 | 45 | adantl 473 |
. . . . . . . . . . . 12
 
      |
47 | | rge0ssre 11766 |
. . . . . . . . . . . . 13
    |
48 | | 0xr 9705 |
. . . . . . . . . . . . . . 15
 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . 14
          |
50 | | pnfxr 11435 |
. . . . . . . . . . . . . . 15
 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
          |
52 | 32, 7, 39 | omexrcl 38447 |
. . . . . . . . . . . . . 14
                  |
53 | | iccgelb 11716 |
. . . . . . . . . . . . . . 15
                        |
54 | 49, 51, 40, 53 | syl3anc 1292 |
. . . . . . . . . . . . . 14
                  |
55 | 12 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . 18
        |
56 | | iunss 4310 |
. . . . . . . . . . . . . . . . . 18
 
           |
57 | 55, 56 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
        |
58 | 57 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
        
      |
59 | 32, 7, 58 | omexrcl 38447 |
. . . . . . . . . . . . . . 15
                   |
60 | | ssiun2 4312 |
. . . . . . . . . . . . . . . . 17
            |
61 | 37, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
                   |
62 | 32, 7, 58, 61 | omessle 38438 |
. . . . . . . . . . . . . . 15
                   
       |
63 | 18 | ltpnfd 11446 |
. . . . . . . . . . . . . . . 16
    
       |
64 | 63 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
                   |
65 | 52, 59, 51, 62, 64 | xrlelttrd 11480 |
. . . . . . . . . . . . . 14
                  |
66 | 49, 51, 52, 54, 65 | elicod 11710 |
. . . . . . . . . . . . 13
                     |
67 | 47, 66 | sseldi 3416 |
. . . . . . . . . . . 12
                  |
68 | 46, 67 | fsumrecl 13877 |
. . . . . . . . . . 11
 
    
          |
69 | | omeiunltfirp.y |
. . . . . . . . . . . . 13
   |
70 | 69 | rpred 11364 |
. . . . . . . . . . . 12
   |
71 | 70 | adantr 472 |
. . . . . . . . . . 11
 
      |
72 | 68, 71 | readdcld 9688 |
. . . . . . . . . 10
 
                 |
73 | 72 | rexrd 9708 |
. . . . . . . . 9
 
                 |
74 | 73 | adantr 472 |
. . . . . . . 8
                Σ^              
           |
75 | | simpr 468 |
. . . . . . . 8
                Σ^                      Σ^              |
76 | 66, 41 | fmptd 6061 |
. . . . . . . . . . . 12
 
                       |
77 | 46, 76 | sge0fsum 38343 |
. . . . . . . . . . 11
 
    Σ^            
                |
78 | | eqidd 2472 |
. . . . . . . . . . . . 13
                              |
79 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
80 | 79 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                   |
81 | 80 | adantl 473 |
. . . . . . . . . . . . 13
   
                        |
82 | | simpr 468 |
. . . . . . . . . . . . 13
          |
83 | | fvex 5889 |
. . . . . . . . . . . . . 14
         |
84 | 83 | a1i 11 |
. . . . . . . . . . . . 13
                  |
85 | 78, 81, 82, 84 | fvmptd 5969 |
. . . . . . . . . . . 12
                                |
86 | 85 | sumeq2dv 13846 |
. . . . . . . . . . 11
 
    
                         |
87 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
88 | 87 | fveq2d 5883 |
. . . . . . . . . . . . 13
                   |
89 | 88 | cbvsumv 13839 |
. . . . . . . . . . . 12

                  |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
 
    
                   |
91 | 77, 86, 90 | 3eqtrd 2509 |
. . . . . . . . . 10
 
    Σ^                       |
92 | 69 | adantr 472 |
. . . . . . . . . . 11
 
      |
93 | 68, 92 | ltaddrpd 11394 |
. . . . . . . . . 10
 
    
                     |
94 | 91, 93 | eqbrtrd 4416 |
. . . . . . . . 9
 
    Σ^                         |
95 | 94 | adantr 472 |
. . . . . . . 8
                Σ^             Σ^                         |
96 | 30, 44, 74, 75, 95 | xrlttrd 11479 |
. . . . . . 7
                Σ^                                   |
97 | 21, 28, 96 | syl2anc 673 |
. . . . . 6
                Σ^                  
                  |
98 | 97 | ex 441 |
. . . . 5
 
        
     Σ^                                     |
99 | 98 | adantlr 729 |
. . . 4
   Σ^                     
     Σ^                                     |
100 | 99 | reximdva 2858 |
. . 3
 
Σ^              
 
     
     Σ^                                          |
101 | 20, 100 | mpd 15 |
. 2
 
Σ^                                        |
102 | | simpl 464 |
. . 3
 
Σ^               |
103 | | simpr 468 |
. . . 4
 
Σ^            
Σ^              |
104 | 3 | a1i 11 |
. . . . . 6
   |
105 | 104, 15 | sge0repnf 38342 |
. . . . 5
  Σ^           
Σ^               |
106 | 105 | adantr 472 |
. . . 4
 
Σ^              Σ^           
Σ^               |
107 | 103, 106 | mpbird 240 |
. . 3
 
Σ^             Σ^              |
108 | | nfv 1769 |
. . . . . 6
   |
109 | | nfcv 2612 |
. . . . . . . 8
 Σ^ |
110 | | nfmpt1 4485 |
. . . . . . . 8
             |
111 | 109, 110 | nffv 5886 |
. . . . . . 7
  Σ^             |
112 | | nfcv 2612 |
. . . . . . 7
   |
113 | 111, 112 | nfel 2624 |
. . . . . 6
  Σ^             |
114 | 108, 113 | nfan 2031 |
. . . . 5
  
Σ^              |
115 | 3 | a1i 11 |
. . . . 5
 
Σ^               |
116 | 13 | adantlr 729 |
. . . . 5
   Σ^             
             |
117 | 69 | adantr 472 |
. . . . 5
 
Σ^               |
118 | | simpr 468 |
. . . . 5
 
Σ^             Σ^              |
119 | 114, 115,
116, 117, 118 | sge0ltfirpmpt 38364 |
. . . 4
 
Σ^                  Σ^             Σ^               |
120 | 18 | ad3antrrr 744 |
. . . . . . 7
    Σ^ 
               Σ^             Σ^                 
       |
121 | 118 | ad2antrr 740 |
. . . . . . 7
    Σ^ 
               Σ^             Σ^              Σ^              |
122 | 72 | ad4ant13 1258 |
. . . . . . 7
    Σ^ 
               Σ^             Σ^                           |
123 | | nfcv 2612 |
. . . . . . . . 9
   |
124 | 108, 123,
5, 7, 1, 8 | omeiunle 38457 |
. . . . . . . 8
    
     Σ^              |
125 | 124 | ad3antrrr 744 |
. . . . . . 7
    Σ^ 
               Σ^             Σ^                 
     Σ^              |
126 | | simpr 468 |
. . . . . . . 8
    Σ^ 
               Σ^             Σ^              Σ^             Σ^               |
127 | | simpll 768 |
. . . . . . . . . . 11
   Σ^                   |
128 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
129 | 128 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
                   |
130 | 129 | cbvmptv 4488 |
. . . . . . . . . . . . . . 15
                     |
131 | 130 | fveq2i 5882 |
. . . . . . . . . . . . . 14
Σ^            Σ^             |
132 | 131 | eleq1i 2540 |
. . . . . . . . . . . . 13
 Σ^            Σ^              |
133 | 132 | biimpi 199 |
. . . . . . . . . . . 12
 Σ^            Σ^              |
134 | 133 | ad2antlr 741 |
. . . . . . . . . . 11
   Σ^                 Σ^              |
135 | | simpr 468 |
. . . . . . . . . . 11
   Σ^                      |
136 | 45 | adantl 473 |
. . . . . . . . . . . 12
   Σ^                   |
137 | 66 | adantllr 733 |
. . . . . . . . . . . 12
    Σ^ 
                             |
138 | 136, 137 | sge0fsummpt 38346 |
. . . . . . . . . . 11
   Σ^                 Σ^                       |
139 | 127, 134,
135, 138 | syl21anc 1291 |
. . . . . . . . . 10
   Σ^                 Σ^                       |
140 | 139 | oveq1d 6323 |
. . . . . . . . 9
   Σ^                  Σ^              
           |
141 | 140 | adantr 472 |
. . . . . . . 8
    Σ^ 
               Σ^             Σ^               Σ^              
           |
142 | 126, 141 | breqtrd 4420 |
. . . . . . 7
    Σ^ 
               Σ^             Σ^              Σ^                         |
143 | 120, 121,
122, 125, 142 | lelttrd 9810 |
. . . . . 6
    Σ^ 
               Σ^             Σ^                 
                  |
144 | 143 | ex 441 |
. . . . 5
   Σ^                  Σ^             Σ^                                    |
145 | 144 | reximdva 2858 |
. . . 4
 
Σ^              
 
  Σ^             Σ^                                         |
146 | 119, 145 | mpd 15 |
. . 3
 
Σ^                                        |
147 | 102, 107,
146 | syl2anc 673 |
. 2
 
Σ^                                        |
148 | 101, 147 | pm2.61dan 808 |
1
                            |