Step | Hyp | Ref
| Expression |
1 | | caucvgsr.f |
. . . 4
       |
2 | | caucvgsr.cau |
. . . 4
                            
          
                            
           
      |
3 | | caucvgsrlembnd.bnd |
. . . 4
        |
4 | | caucvgsrlembnd.offset |
. . . 4
             |
5 | 1, 2, 3, 4 | caucvgsrlemofff 7796 |
. . 3
       |
6 | 1, 2, 3, 4 | caucvgsrlemoffcau 7797 |
. . 3
                            
          
                            
           
      |
7 | 1, 2, 3, 4 | caucvgsrlemoffgt1 7798 |
. . 3
        |
8 | 5, 6, 7 | caucvgsrlemgt1 7794 |
. 2
      
      
           |
9 | | simprl 529 |
. . . . 5
 
                          |
10 | 3 | caucvgsrlemasr 7789 |
. . . . . 6
   |
11 | 10 | adantr 276 |
. . . . 5
 
                          |
12 | | addclsr 7752 |
. . . . 5
 
     |
13 | 9, 11, 12 | syl2anc 411 |
. . . 4
 
                            |
14 | | m1r 7751 |
. . . 4
 |
15 | | addclsr 7752 |
. . . 4
        
  |
16 | 13, 14, 15 | sylancl 413 |
. . 3
 
                              |
17 | | ltasrg 7769 |
. . . . . . . . . . . . . . . 16
 
 
       |
18 | 17 | adantl 277 |
. . . . . . . . . . . . . . 15
     
  
  
       |
19 | 5 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
   

        |
20 | | simpr 110 |
. . . . . . . . . . . . . . . 16
   

    |
21 | 19, 20 | ffvelcdmd 5653 |
. . . . . . . . . . . . . . 15
   

        |
22 | | simpllr 534 |
. . . . . . . . . . . . . . . 16
   

    |
23 | | simplr 528 |
. . . . . . . . . . . . . . . 16
   

    |
24 | | addclsr 7752 |
. . . . . . . . . . . . . . . 16
 
     |
25 | 22, 23, 24 | syl2anc 411 |
. . . . . . . . . . . . . . 15
   

      |
26 | 10 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
   

    |
27 | | addcomsrg 7754 |
. . . . . . . . . . . . . . . 16
 
       |
28 | 27 | adantl 277 |
. . . . . . . . . . . . . . 15
     
  
        |
29 | 18, 21, 25, 26, 28 | caovord2d 6044 |
. . . . . . . . . . . . . 14
   

                      |
30 | 1, 2, 3, 4 | caucvgsrlemoffval 7795 |
. . . . . . . . . . . . . . . . 17
 

              |
31 | 30 | adantlr 477 |
. . . . . . . . . . . . . . . 16
                   |
32 | 31 | adantlr 477 |
. . . . . . . . . . . . . . 15
   

                |
33 | 32 | breq1d 4014 |
. . . . . . . . . . . . . 14
   

                          |
34 | 29, 33 | bitrd 188 |
. . . . . . . . . . . . 13
   

                      |
35 | | addasssrg 7755 |
. . . . . . . . . . . . . . . 16
 
           |
36 | 35 | adantl 277 |
. . . . . . . . . . . . . . 15
     
  
            |
37 | 22, 23, 26, 28, 36 | caov32d 6055 |
. . . . . . . . . . . . . 14
   

            |
38 | 37 | breq2d 4016 |
. . . . . . . . . . . . 13
   

                          |
39 | 1 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
           |
40 | 39 | ffvelcdmda 5652 |
. . . . . . . . . . . . . . . 16
   

        |
41 | | 1sr 7750 |
. . . . . . . . . . . . . . . 16
 |
42 | | addclsr 7752 |
. . . . . . . . . . . . . . . 16
            
  |
43 | 40, 41, 42 | sylancl 413 |
. . . . . . . . . . . . . . 15
   

          |
44 | 22, 26, 12 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
   

      |
45 | | addclsr 7752 |
. . . . . . . . . . . . . . . 16
   
       |
46 | 44, 23, 45 | syl2anc 411 |
. . . . . . . . . . . . . . 15
   

        |
47 | 14 | a1i 9 |
. . . . . . . . . . . . . . 15
   

 
  |
48 | 18, 43, 46, 47, 28 | caovord2d 6044 |
. . . . . . . . . . . . . 14
   

                              |
49 | 41 | a1i 9 |
. . . . . . . . . . . . . . . . 17
   

 
  |
50 | | addasssrg 7755 |
. . . . . . . . . . . . . . . . 17
                         |
51 | 40, 49, 47, 50 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
   

                    |
52 | | addcomsrg 7754 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
53 | 41, 14, 52 | mp2an 426 |
. . . . . . . . . . . . . . . . . . 19
     |
54 | | m1p1sr 7759 |
. . . . . . . . . . . . . . . . . . 19
   |
55 | 53, 54 | eqtri 2198 |
. . . . . . . . . . . . . . . . . 18
   |
56 | 55 | oveq2i 5886 |
. . . . . . . . . . . . . . . . 17
               |
57 | | 0idsr 7766 |
. . . . . . . . . . . . . . . . . 18
                 |
58 | 40, 57 | syl 14 |
. . . . . . . . . . . . . . . . 17
   

              |
59 | 56, 58 | eqtrid 2222 |
. . . . . . . . . . . . . . . 16
   

                |
60 | 51, 59 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
   

                |
61 | 44, 23, 47, 28, 36 | caov32d 6055 |
. . . . . . . . . . . . . . 15
   

                |
62 | 60, 61 | breq12d 4017 |
. . . . . . . . . . . . . 14
   

                              |
63 | 48, 62 | bitrd 188 |
. . . . . . . . . . . . 13
   

                          |
64 | 34, 38, 63 | 3bitrd 214 |
. . . . . . . . . . . 12
   

                      |
65 | 64 | biimpd 144 |
. . . . . . . . . . 11
   

        
             |
66 | | addclsr 7752 |
. . . . . . . . . . . . . . . 16
     
         |
67 | 21, 23, 66 | syl2anc 411 |
. . . . . . . . . . . . . . 15
   

          |
68 | 18, 22, 67, 26, 28 | caovord2d 6044 |
. . . . . . . . . . . . . 14
   

                      |
69 | 21, 23, 26, 28, 36 | caov32d 6055 |
. . . . . . . . . . . . . . . 16
   

                    |
70 | 32 | oveq1d 5890 |
. . . . . . . . . . . . . . . 16
   

                    |
71 | 69, 70 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
   

                    |
72 | 71 | breq2d 4016 |
. . . . . . . . . . . . . 14
   

                          |
73 | 68, 72 | bitrd 188 |
. . . . . . . . . . . . 13
   

                      |
74 | | addclsr 7752 |
. . . . . . . . . . . . . . 15
       
           |
75 | 43, 23, 74 | syl2anc 411 |
. . . . . . . . . . . . . 14
   

            |
76 | 18, 44, 75, 47, 28 | caovord2d 6044 |
. . . . . . . . . . . . 13
   

                              |
77 | 40, 49, 23, 28, 36 | caov32d 6055 |
. . . . . . . . . . . . . . . . . 18
   

                    |
78 | 77 | oveq1d 5890 |
. . . . . . . . . . . . . . . . 17
   

           
            |
79 | | addclsr 7752 |
. . . . . . . . . . . . . . . . . . 19
     
         |
80 | 40, 23, 79 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
   

          |
81 | | addasssrg 7755 |
. . . . . . . . . . . . . . . . . 18
                               |
82 | 80, 49, 47, 81 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
   

                        |
83 | 78, 82 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
   

           
            |
84 | 55 | oveq2i 5886 |
. . . . . . . . . . . . . . . 16
                   |
85 | 83, 84 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
   

           
          |
86 | | 0idsr 7766 |
. . . . . . . . . . . . . . . 16
                       |
87 | 80, 86 | syl 14 |
. . . . . . . . . . . . . . 15
   

                  |
88 | 85, 87 | eqtrd 2210 |
. . . . . . . . . . . . . 14
   

           
        |
89 | 88 | breq2d 4016 |
. . . . . . . . . . . . 13
   

                              |
90 | 73, 76, 89 | 3bitrd 214 |
. . . . . . . . . . . 12
   

                      |
91 | 90 | biimpd 144 |
. . . . . . . . . . 11
   

        
             |
92 | 65, 91 | anim12d 335 |
. . . . . . . . . 10
   

         
      
          
              |
93 | 92 | imim2d 54 |
. . . . . . . . 9
   

   
      
                                   |
94 | 93 | ralimdva 2544 |
. . . . . . . 8
      
                 
          
               |
95 | | breq2 4008 |
. . . . . . . . . 10
 
   |
96 | | fveq2 5516 |
. . . . . . . . . . . 12
           |
97 | 96 | breq1d 4014 |
. . . . . . . . . . 11
           
             |
98 | 96 | oveq1d 5890 |
. . . . . . . . . . . 12
               |
99 | 98 | breq2d 4016 |
. . . . . . . . . . 11
           
             |
100 | 97, 99 | anbi12d 473 |
. . . . . . . . . 10
                       
          
              |
101 | 95, 100 | imbi12d 234 |
. . . . . . . . 9
                                                     |
102 | 101 | cbvralv 2704 |
. . . . . . . 8
 
                       
 
          
              |
103 | 94, 102 | imbitrdi 161 |
. . . . . . 7
      
                 
          
               |
104 | 103 | reximdv 2578 |
. . . . . 6
      
                 
                            |
105 | 104 | imim2d 54 |
. . . . 5
                                                         |
106 | 105 | ralimdva 2544 |
. . . 4
 

 
   
      
         


                             |
107 | 106 | impr 379 |
. . 3
 
                                                       |
108 | | oveq1 5882 |
. . . . . . . . . 10
               |
109 | 108 | breq2d 4016 |
. . . . . . . . 9
           
             |
110 | | breq1 4007 |
. . . . . . . . 9
           
             |
111 | 109, 110 | anbi12d 473 |
. . . . . . . 8
                              
              |
112 | 111 | imbi2d 230 |
. . . . . . 7
                     

          
               |
113 | 112 | rexralbidv 2503 |
. . . . . 6
      
                
  
          
               |
114 | 113 | imbi2d 230 |
. . . . 5
                                                         |
115 | 114 | ralbidv 2477 |
. . . 4
      


                  


                             |
116 | 115 | rspcev 2842 |
. . 3
     

   
          
             
                        |
117 | 16, 107, 116 | syl2anc 411 |
. 2
 
                                                |
118 | 8, 117 | rexlimddv 2599 |
1
      
      
           |