Step | Hyp | Ref
| Expression |
1 | | iccssxr 11714 |
. . . . . . 7
    |
2 | | meadjun.m |
. . . . . . . . 9
 Meas |
3 | | meadjun.x |
. . . . . . . . 9
 |
4 | 2, 3 | meaf 38285 |
. . . . . . . 8
          |
5 | | meadjun.b |
. . . . . . . 8
   |
6 | 4, 5 | ffvelrnd 6021 |
. . . . . . 7
          |
7 | 1, 6 | sseldi 3429 |
. . . . . 6
       |
8 | | xaddid2 11530 |
. . . . . 6
    
               |
9 | 7, 8 | syl 17 |
. . . . 5
                |
10 | 9 | eqcomd 2456 |
. . . 4
                |
11 | 10 | adantr 467 |
. . 3
 

               |
12 | | uneq1 3580 |
. . . . . 6

  
   |
13 | | 0un 37380 |
. . . . . . 7
   |
14 | 13 | a1i 11 |
. . . . . 6

    |
15 | 12, 14 | eqtrd 2484 |
. . . . 5

    |
16 | 15 | fveq2d 5867 |
. . . 4

            |
17 | 16 | adantl 468 |
. . 3
 

            |
18 | | fveq2 5863 |
. . . . . 6

          |
19 | 18 | adantl 468 |
. . . . 5
 

          |
20 | 2 | mea0 38286 |
. . . . . 6
       |
21 | 20 | adantr 467 |
. . . . 5
 

      |
22 | 19, 21 | eqtrd 2484 |
. . . 4
 

      |
23 | 22 | oveq1d 6303 |
. . 3
 

                        |
24 | 11, 17, 23 | 3eqtr4d 2494 |
. 2
 

                     |
25 | | simpl 459 |
. . 3
 
   |
26 | | meadjun.dj |
. . . . . 6
     |
27 | 26 | ad2antrr 731 |
. . . . 5
  

     |
28 | | inidm 3640 |
. . . . . . . . . . 11
   |
29 | 28 | eqcomi 2459 |
. . . . . . . . . 10
   |
30 | | ineq2 3627 |
. . . . . . . . . 10
       |
31 | 29, 30 | syl5req 2497 |
. . . . . . . . 9
     |
32 | 31 | adantl 468 |
. . . . . . . 8
       |
33 | | neqne 37368 |
. . . . . . . . 9
   |
34 | 33 | adantr 467 |
. . . . . . . 8
     |
35 | 32, 34 | eqnetrd 2690 |
. . . . . . 7
       |
36 | 35 | neneqd 2628 |
. . . . . 6
  
    |
37 | 36 | adantll 719 |
. . . . 5
  

     |
38 | 27, 37 | pm2.65da 579 |
. . . 4
 

  |
39 | 38 | neqned 2630 |
. . 3
 
   |
40 | | meadjun.a |
. . . . . . . 8
   |
41 | | uniprg 4211 |
. . . . . . . 8
 
    

   |
42 | 40, 5, 41 | syl2anc 666 |
. . . . . . 7
    

   |
43 | 42 | eqcomd 2456 |
. . . . . 6
     
   |
44 | 43 | fveq2d 5867 |
. . . . 5
    
            |
45 | 44 | adantr 467 |
. . . 4
 

           
    |
46 | 40, 5 | prssd 37378 |
. . . . . 6
      |
47 | | prfi 7843 |
. . . . . . . 8
    |
48 | | isfinite 8154 |
. . . . . . . . . 10
         |
49 | 48 | biimpi 198 |
. . . . . . . . 9
   
     |
50 | | sdomdom 7594 |
. . . . . . . . 9
   
     |
51 | 49, 50 | syl 17 |
. . . . . . . 8
   
     |
52 | 47, 51 | ax-mp 5 |
. . . . . . 7
    |
53 | 52 | a1i 11 |
. . . . . 6
      |
54 | | disjxsn 4395 |
. . . . . . . . . 10
Disj     |
55 | 54 | a1i 11 |
. . . . . . . . 9
 Disj      |
56 | | preq1 4050 |
. . . . . . . . . . 11
     
   |
57 | | dfsn2 3980 |
. . . . . . . . . . . . 13
 
    |
58 | 57 | eqcomi 2459 |
. . . . . . . . . . . 12
      |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
        |
60 | 56, 59 | eqtrd 2484 |
. . . . . . . . . 10
        |
61 | 60 | disjeq1d 4380 |
. . . . . . . . 9
 Disj    
Disj       |
62 | 55, 61 | mpbird 236 |
. . . . . . . 8
 Disj       |
63 | 62 | adantl 468 |
. . . . . . 7
 
 Disj       |
64 | | simpl 459 |
. . . . . . . 8
 
   |
65 | | neqne 37368 |
. . . . . . . . 9
   |
66 | 65 | adantl 468 |
. . . . . . . 8
 
   |
67 | 26 | adantr 467 |
. . . . . . . . 9
 

    |
68 | 40 | adantr 467 |
. . . . . . . . . 10
 

  |
69 | 5 | adantr 467 |
. . . . . . . . . 10
 

  |
70 | | simpr 463 |
. . . . . . . . . 10
 

  |
71 | | id 22 |
. . . . . . . . . . 11
   |
72 | | id 22 |
. . . . . . . . . . 11
   |
73 | 71, 72 | disjprg 4397 |
. . . . . . . . . 10
 
 Disj    
     |
74 | 68, 69, 70, 73 | syl3anc 1267 |
. . . . . . . . 9
 

Disj    
     |
75 | 67, 74 | mpbird 236 |
. . . . . . . 8
 

Disj  
    |
76 | 64, 66, 75 | syl2anc 666 |
. . . . . . 7
 
 Disj       |
77 | 63, 76 | pm2.61dan 799 |
. . . . . 6
 Disj
      |
78 | 2, 3, 46, 53, 77 | meadjuni 38289 |
. . . . 5
         Σ^         |
79 | 78 | adantr 467 |
. . . 4
 

        Σ^         |
80 | 4, 40 | ffvelrnd 6021 |
. . . . . . 7
          |
81 | 80 | adantr 467 |
. . . . . 6
 

         |
82 | 6 | adantr 467 |
. . . . . 6
 

         |
83 | | fveq2 5863 |
. . . . . 6
           |
84 | | fveq2 5863 |
. . . . . 6
           |
85 | 68, 69, 81, 82, 83, 84, 70 | sge0pr 38230 |
. . . . 5
 

Σ^   
                      |
86 | 4, 46 | fssresd 5748 |
. . . . . . . . 9
                  |
87 | 86 | feqmptd 5916 |
. . . . . . . 8
        
             |
88 | | fvres 5877 |
. . . . . . . . . 10
   
 
             |
89 | 88 | mpteq2ia 4484 |
. . . . . . . . 9
   
 
          
       |
90 | 89 | a1i 11 |
. . . . . . . 8
   
              
       |
91 | 87, 90 | eqtrd 2484 |
. . . . . . 7
        
        |
92 | 91 | fveq2d 5867 |
. . . . . 6
 Σ^       Σ^   
         |
93 | 92 | adantr 467 |
. . . . 5
 

Σ^       Σ^   
         |
94 | | eqidd 2451 |
. . . . 5
 

                            |
95 | 85, 93, 94 | 3eqtr4d 2494 |
. . . 4
 

Σ^                      |
96 | 45, 79, 95 | 3eqtrd 2488 |
. . 3
 

                     |
97 | 25, 39, 96 | syl2anc 666 |
. 2
 
                      |
98 | 24, 97 | pm2.61dan 799 |
1
    
                 |