Step | Hyp | Ref
| Expression |
1 | | caratheodorylem2.o |
. . 3

OutMeas |
2 | | caratheodorylem2.x |
. . 3

 |
3 | | caratheodorylem2.s |
. . . . . . . . . . 11
CaraGen   |
4 | 3 | caragenss 38325 |
. . . . . . . . . 10
 OutMeas   |
5 | 1, 4 | syl 17 |
. . . . . . . . 9

  |
6 | 5 | adantr 467 |
. . . . . . . 8
 

  |
7 | | caratheodorylem2.e |
. . . . . . . . 9
       |
8 | 7 | ffvelrnda 6022 |
. . . . . . . 8
 

      |
9 | 6, 8 | sseldd 3433 |
. . . . . . 7
 

      |
10 | | elssuni 4227 |
. . . . . . 7
        
   |
11 | 9, 10 | syl 17 |
. . . . . 6
 

       |
12 | 11, 2 | syl6sseqr 3479 |
. . . . 5
 

      |
13 | 12 | ralrimiva 2802 |
. . . 4
        |
14 | | iunss 4319 |
. . . 4
 
           |
15 | 13, 14 | sylibr 216 |
. . 3
        |
16 | 1, 2, 15 | omexrcl 38328 |
. 2
            |
17 | | nnex 10615 |
. . . 4
 |
18 | 17 | a1i 11 |
. . 3
   |
19 | 1 | adantr 467 |
. . . . 5
 

OutMeas |
20 | 19, 2, 12 | omecl 38324 |
. . . 4
 

             |
21 | | eqid 2451 |
. . . 4
                     |
22 | 20, 21 | fmptd 6046 |
. . 3
                    |
23 | 18, 22 | sge0xrcl 38227 |
. 2
 Σ^              |
24 | | nfv 1761 |
. . 3
   |
25 | | nfcv 2592 |
. . 3
   |
26 | | nnuz 11194 |
. . 3
     |
27 | 1, 2, 3 | caragensspw 38330 |
. . . 4

   |
28 | 7, 27 | fssd 5738 |
. . 3
        |
29 | 24, 25, 1, 2, 26, 28 | omeiunle 38338 |
. 2
          Σ^              |
30 | | elpwinss 37387 |
. . . . . . . 8
      |
31 | 30 | resmptd 5156 |
. . . . . . 7
              
             |
32 | 31 | fveq2d 5869 |
. . . . . 6
    Σ^           
  Σ^              |
33 | 32 | adantl 468 |
. . . . 5
 
    Σ^           
  Σ^              |
34 | | 1zzd 10968 |
. . . . . . 7
 
      |
35 | 30 | adantl 468 |
. . . . . . 7
 
      |
36 | | elinel2 3620 |
. . . . . . . 8
      |
37 | 36 | adantl 468 |
. . . . . . 7
 
      |
38 | 34, 26, 35, 37 | uzfissfz 37549 |
. . . . . 6
 
           |
39 | | vex 3048 |
. . . . . . . . . . . . 13
 |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
 
       |
41 | 1 | ad2antrr 732 |
. . . . . . . . . . . . . 14
         OutMeas |
42 | 28 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
                |
43 | | fz1ssnn 11830 |
. . . . . . . . . . . . . . . . . 18
     |
44 | | ssel2 3427 |
. . . . . . . . . . . . . . . . . 18
 
   
       |
45 | 43, 44 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
 
   
   |
46 | 45 | adantll 720 |
. . . . . . . . . . . . . . . 16
           |
47 | 42, 46 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
                |
48 | | elpwi 3960 |
. . . . . . . . . . . . . . 15
         
  |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
               |
50 | 41, 2, 49 | omecl 38324 |
. . . . . . . . . . . . 13
                      |
51 | | eqid 2451 |
. . . . . . . . . . . . 13
                     |
52 | 50, 51 | fmptd 6046 |
. . . . . . . . . . . 12
 
                        |
53 | 40, 52 | sge0xrcl 38227 |
. . . . . . . . . . 11
 
     Σ^              |
54 | 53 | 3adant2 1027 |
. . . . . . . . . 10
 
     Σ^              |
55 | | ovex 6318 |
. . . . . . . . . . . . 13
     |
56 | 55 | a1i 11 |
. . . . . . . . . . . 12
       |
57 | | elfznn 11828 |
. . . . . . . . . . . . . 14
       |
58 | 57, 20 | sylan2 477 |
. . . . . . . . . . . . 13
 
                  |
59 | | eqid 2451 |
. . . . . . . . . . . . 13
                             |
60 | 58, 59 | fmptd 6046 |
. . . . . . . . . . . 12
                            |
61 | 56, 60 | sge0xrcl 38227 |
. . . . . . . . . . 11
 Σ^                  |
62 | 61 | 3ad2ant1 1029 |
. . . . . . . . . 10
 
     Σ^                  |
63 | 16 | 3ad2ant1 1029 |
. . . . . . . . . 10
 
                |
64 | 55 | a1i 11 |
. . . . . . . . . . 11
 
           |
65 | | simpl1 1011 |
. . . . . . . . . . . 12
               |
66 | 57 | adantl 468 |
. . . . . . . . . . . 12
               |
67 | 65, 66, 20 | syl2anc 667 |
. . . . . . . . . . 11
                          |
68 | | simp3 1010 |
. . . . . . . . . . 11
 
           |
69 | 64, 67, 68 | sge0lessmpt 38241 |
. . . . . . . . . 10
 
     Σ^            Σ^                  |
70 | 1 | adantr 467 |
. . . . . . . . . . . . . 14
 

OutMeas |
71 | 7 | adantr 467 |
. . . . . . . . . . . . . 14
 

      |
72 | | caratheodorylem2.5 |
. . . . . . . . . . . . . . 15
 Disj
      |
73 | 72 | adantr 467 |
. . . . . . . . . . . . . 14
 

Disj
      |
74 | | caratheodorylem2.g |
. . . . . . . . . . . . . . 15
             |
75 | | nfiu1 4308 |
. . . . . . . . . . . . . . . 16
  
          |
76 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
  
          |
77 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
78 | 77 | cbviunv 4317 |
. . . . . . . . . . . . . . . . . 18
          
          |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . 17
           
           |
80 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18
           |
81 | 80 | iuneq1d 4303 |
. . . . . . . . . . . . . . . . 17
           
           |
82 | 79, 81 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
           
           |
83 | 75, 76, 82 | cbvmpt 4494 |
. . . . . . . . . . . . . . 15
                         |
84 | 74, 83 | eqtri 2473 |
. . . . . . . . . . . . . 14
             |
85 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
86 | 85, 26 | syl6eleq 2539 |
. . . . . . . . . . . . . . 15
       |
87 | 86 | adantl 468 |
. . . . . . . . . . . . . 14
 

      |
88 | 70, 3, 26, 71, 73, 84, 87 | caratheodorylem1 38347 |
. . . . . . . . . . . . 13
 

        Σ^                  |
89 | 88 | eqcomd 2457 |
. . . . . . . . . . . 12
 

Σ^                          |
90 | 15 | adantr 467 |
. . . . . . . . . . . . 13
 

       |
91 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
     |
92 | 55, 91 | iunex 6773 |
. . . . . . . . . . . . . . . 16
           |
93 | 74 | fvmpt2 5957 |
. . . . . . . . . . . . . . . 16
                             |
94 | 85, 92, 93 | sylancl 668 |
. . . . . . . . . . . . . . 15
                 |
95 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
       |
96 | | iunss1 4290 |
. . . . . . . . . . . . . . . 16
    
                 |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . 15
                  |
98 | 94, 97 | eqsstrd 3466 |
. . . . . . . . . . . . . 14
            |
99 | 98 | adantl 468 |
. . . . . . . . . . . . 13
 

           |
100 | 70, 2, 90, 99 | omessle 38319 |
. . . . . . . . . . . 12
 

                   |
101 | 89, 100 | eqbrtrd 4423 |
. . . . . . . . . . 11
 

Σ^                           |
102 | 101 | 3adant3 1028 |
. . . . . . . . . 10
 
     Σ^                           |
103 | 54, 62, 63, 69, 102 | xrletrd 11459 |
. . . . . . . . 9
 
     Σ^                       |
104 | 103 | 3exp 1207 |
. . . . . . . 8
       Σ^                         |
105 | 104 | adantr 467 |
. . . . . . 7
 
     
    Σ^                         |
106 | 105 | rexlimdv 2877 |
. . . . . 6
 
     
    Σ^                        |
107 | 38, 106 | mpd 15 |
. . . . 5
 
    Σ^                       |
108 | 33, 107 | eqbrtrd 4423 |
. . . 4
 
    Σ^           
 
           |
109 | 108 | ralrimiva 2802 |
. . 3
      Σ^                         |
110 | 18, 22, 16 | sge0lefi 38240 |
. . 3
  Σ^                    
     Σ^                          |
111 | 109, 110 | mpbird 236 |
. 2
 Σ^                       |
112 | 16, 23, 29, 111 | xrletrid 11452 |
1
          Σ^              |