Step | Hyp | Ref
| Expression |
1 | | opeq1 3776 |
. . . . . . . . 9
   
     |
2 | 1 | eceq1d 6565 |
. . . . . . . 8
            |
3 | 2 | fveq2d 5515 |
. . . . . . 7
                   |
4 | 3 | oveq2d 5885 |
. . . . . 6
                       |
5 | | fveq2 5511 |
. . . . . . 7
           |
6 | 5 | oveq1d 5884 |
. . . . . 6
               |
7 | 4, 6 | breq12d 4013 |
. . . . 5
                 
                   |
8 | 7 | cbvrexv 2704 |
. . . 4
                 
                   |
9 | 8 | a1i 9 |
. . 3
  
               
                    |
10 | 9 | rabbiia 2722 |
. 2
 
                                     |
11 | | oveq1 5876 |
. . . . . . 7
                       |
12 | 11 | breq1d 4010 |
. . . . . 6
                 
                   |
13 | 12 | rexbidv 2478 |
. . . . 5
  
               
                    |
14 | 13 | elrab 2893 |
. . . 4
                   
                     |
15 | | caucvgpr.f |
. . . . . . . . . . . . . . 15
       |
16 | 15 | ad4antr 494 |
. . . . . . . . . . . . . 14
     
                         |
17 | | caucvgpr.cau |
. . . . . . . . . . . . . . 15
                                             |
18 | 17 | ad4antr 494 |
. . . . . . . . . . . . . 14
     
                                        
                      |
19 | | simpr 110 |
. . . . . . . . . . . . . 14
     
                     |
20 | | simpllr 534 |
. . . . . . . . . . . . . 14
     
                     |
21 | 16, 18, 19, 20 | caucvgprlemnbj 7654 |
. . . . . . . . . . . . 13
     
                                                 |
22 | 15 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
   

                        |
23 | 22 | ffvelcdmda 5647 |
. . . . . . . . . . . . . . . . 17
     
                         |
24 | | nnnq 7409 |
. . . . . . . . . . . . . . . . . 18
        |
25 | | recclnq 7379 |
. . . . . . . . . . . . . . . . . 18
             
  |
26 | 19, 24, 25 | 3syl 17 |
. . . . . . . . . . . . . . . . 17
     
                             |
27 | | addclnq 7362 |
. . . . . . . . . . . . . . . . 17
             
                 |
28 | 23, 26, 27 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
     
                                   |
29 | | nnnq 7409 |
. . . . . . . . . . . . . . . . 17
        |
30 | | recclnq 7379 |
. . . . . . . . . . . . . . . . 17
             
  |
31 | 20, 29, 30 | 3syl 17 |
. . . . . . . . . . . . . . . 16
     
                             |
32 | | caucvgprlemladd.s |
. . . . . . . . . . . . . . . . 17
   |
33 | 32 | ad4antr 494 |
. . . . . . . . . . . . . . . 16
     
                     |
34 | | addassnqg 7369 |
. . . . . . . . . . . . . . . 16
                       
                                                       |
35 | 28, 31, 33, 34 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
     
                                                                         |
36 | 35 | breq1d 4010 |
. . . . . . . . . . . . . 14
     
                                                                                       |
37 | | ltanqg 7387 |
. . . . . . . . . . . . . . . 16
 
 
       |
38 | 37 | adantl 277 |
. . . . . . . . . . . . . . 15
     

                 
 
 
        |
39 | | addclnq 7362 |
. . . . . . . . . . . . . . . 16
                       
                           |
40 | 28, 31, 39 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     
                                             |
41 | 16, 20 | ffvelcdmd 5648 |
. . . . . . . . . . . . . . 15
     
                         |
42 | | addcomnqg 7368 |
. . . . . . . . . . . . . . . 16
 
       |
43 | 42 | adantl 277 |
. . . . . . . . . . . . . . 15
     

                 
   
      |
44 | 38, 40, 41, 33, 43 | caovord2d 6038 |
. . . . . . . . . . . . . 14
     
                                                                                   |
45 | | addcomnqg 7368 |
. . . . . . . . . . . . . . . . 17
         
                       |
46 | 33, 31, 45 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
     
                                         |
47 | 46 | oveq2d 5885 |
. . . . . . . . . . . . . . 15
     
                                                                         |
48 | 47 | breq1d 4010 |
. . . . . . . . . . . . . 14
     
                                                                                       |
49 | 36, 44, 48 | 3bitr4rd 221 |
. . . . . . . . . . . . 13
     
                                                                                   |
50 | 21, 49 | mtbird 673 |
. . . . . . . . . . . 12
     
                                                     |
51 | 50 | nrexdv 2570 |
. . . . . . . . . . 11
   

                                            
        |
52 | 51 | intnand 931 |
. . . . . . . . . 10
   

                                                             |
53 | 17 | ad3antrrr 492 |
. . . . . . . . . . . . 13
   

                                       
                      |
54 | | caucvgpr.bnd |
. . . . . . . . . . . . . . 15
        |
55 | | fveq2 5511 |
. . . . . . . . . . . . . . . . 17
           |
56 | 55 | breq2d 4012 |
. . . . . . . . . . . . . . . 16
     
       |
57 | 56 | cbvralv 2703 |
. . . . . . . . . . . . . . 15
 
           |
58 | 54, 57 | sylib 122 |
. . . . . . . . . . . . . 14
        |
59 | 58 | ad3antrrr 492 |
. . . . . . . . . . . . 13
   

                         |
60 | | caucvgpr.lim |
. . . . . . . . . . . . . 14
                   
                  |
61 | | opeq1 3776 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
62 | 61 | eceq1d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
            |
63 | 62 | fveq2d 5515 |
. . . . . . . . . . . . . . . . . . . 20
                   |
64 | 63 | oveq2d 5885 |
. . . . . . . . . . . . . . . . . . 19
                       |
65 | 64, 55 | breq12d 4013 |
. . . . . . . . . . . . . . . . . 18
               
                 |
66 | 65 | cbvrexv 2704 |
. . . . . . . . . . . . . . . . 17
               
                 |
67 | 66 | a1i 9 |
. . . . . . . . . . . . . . . 16
  
             
                  |
68 | 67 | rabbiia 2722 |
. . . . . . . . . . . . . . 15
 
                                 |
69 | 55, 63 | oveq12d 5887 |
. . . . . . . . . . . . . . . . . . 19
                               |
70 | 69 | breq1d 4010 |
. . . . . . . . . . . . . . . . . 18
               
                 |
71 | 70 | cbvrexv 2704 |
. . . . . . . . . . . . . . . . 17
               
                 |
72 | 71 | a1i 9 |
. . . . . . . . . . . . . . . 16
  
             
                  |
73 | 72 | rabbiia 2722 |
. . . . . . . . . . . . . . 15
                
 
                |
74 | 68, 73 | opeq12i 3781 |
. . . . . . . . . . . . . 14
  
                
                                    
                  |
75 | 60, 74 | eqtri 2198 |
. . . . . . . . . . . . 13
                   
                  |
76 | 32 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
   

                    |
77 | 29, 30 | syl 14 |
. . . . . . . . . . . . . . 15
           |
78 | 77 | ad2antlr 489 |
. . . . . . . . . . . . . 14
   

                            |
79 | | addclnq 7362 |
. . . . . . . . . . . . . 14
         
             |
80 | 76, 78, 79 | syl2anc 411 |
. . . . . . . . . . . . 13
   

                              |
81 | 22, 53, 59, 75, 80 | caucvgprlemladdfu 7664 |
. . . . . . . . . . . 12
   

                                                  
                               |
82 | 81 | sseld 3154 |
. . . . . . . . . . 11
   

                                                         
       
                              |
83 | | breq2 4004 |
. . . . . . . . . . . . 13
                                                           
         |
84 | 83 | rexbidv 2478 |
. . . . . . . . . . . 12
        
                                                    
         |
85 | 84 | elrab 2893 |
. . . . . . . . . . 11
                                   
      
                                    |
86 | 82, 85 | syl6ib 161 |
. . . . . . . . . 10
   

                                                         
       
                         
          |
87 | 52, 86 | mtod 663 |
. . . . . . . . 9
   

                                                           |
88 | 15, 17, 54, 60 | caucvgprlemcl 7663 |
. . . . . . . . . . . 12
   |
89 | 88 | ad3antrrr 492 |
. . . . . . . . . . 11
   

                    |
90 | | nqprlu 7534 |
. . . . . . . . . . . 12
                                        |
91 | 80, 90 | syl 14 |
. . . . . . . . . . 11
   

                                               |
92 | | addclpr 7524 |
. . . . . . . . . . 11
                                                             |
93 | 89, 91, 92 | syl2anc 411 |
. . . . . . . . . 10
   

                    
                            |
94 | | prop 7462 |
. . . . . . . . . . 11
                                    
                                                                |
95 | | prloc 7478 |
. . . . . . . . . . 11
        
                                                                                               
                                      
                              |
96 | 94, 95 | sylan 283 |
. . . . . . . . . 10
                                                                                                       
                              |
97 | 93, 96 | sylancom 420 |
. . . . . . . . 9
   

                                                                         
                              |
98 | 87, 97 | ecased 1349 |
. . . . . . . 8
   

                                                               |
99 | | simpllr 534 |
. . . . . . . . 9
   

                    |
100 | 89, 76, 99, 78 | caucvgprlemcanl 7631 |
. . . . . . . 8
   

                                                                   
          |
101 | 98, 100 | mpbid 147 |
. . . . . . 7
   

                       
         |
102 | 101 | ex 115 |
. . . . . 6
                           
          |
103 | 102 | rexlimdva 2594 |
. . . . 5
 

                       
          |
104 | 103 | expimpd 363 |
. . . 4
  
                       
          |
105 | 14, 104 | biimtrid 152 |
. . 3
   
                      
          |
106 | 105 | ssrdv 3161 |
. 2
                         
         |
107 | 10, 106 | eqsstrid 3201 |
1
                         
         |