Step | Hyp | Ref
| Expression |
1 | | caucvgpr.cau |
. . . . . . 7
                                             |
2 | | caucvgprlemnbj.b |
. . . . . . . 8
   |
3 | | caucvgprlemnbj.j |
. . . . . . . 8
   |
4 | | breq1 4007 |
. . . . . . . . . 10
 
   |
5 | | fveq2 5516 |
. . . . . . . . . . . 12
           |
6 | | opeq1 3779 |
. . . . . . . . . . . . . . 15
   
     |
7 | 6 | eceq1d 6571 |
. . . . . . . . . . . . . 14
            |
8 | 7 | fveq2d 5520 |
. . . . . . . . . . . . 13
                   |
9 | 8 | oveq2d 5891 |
. . . . . . . . . . . 12
                               |
10 | 5, 9 | breq12d 4017 |
. . . . . . . . . . 11
                   
                     |
11 | 5, 8 | oveq12d 5893 |
. . . . . . . . . . . 12
                               |
12 | 11 | breq2d 4016 |
. . . . . . . . . . 11
                   
                     |
13 | 10, 12 | anbi12d 473 |
. . . . . . . . . 10
                    
                  
                  
                      |
14 | 4, 13 | imbi12d 234 |
. . . . . . . . 9
                     
                   

                  
                       |
15 | | breq2 4008 |
. . . . . . . . . 10
 
   |
16 | | fveq2 5516 |
. . . . . . . . . . . . 13
           |
17 | 16 | oveq1d 5890 |
. . . . . . . . . . . 12
                               |
18 | 17 | breq2d 4016 |
. . . . . . . . . . 11
                   
                     |
19 | 16 | breq1d 4014 |
. . . . . . . . . . 11
                   
                     |
20 | 18, 19 | anbi12d 473 |
. . . . . . . . . 10
                    
                  
                  
                      |
21 | 15, 20 | imbi12d 234 |
. . . . . . . . 9
                     
                   

                  
                       |
22 | 14, 21 | rspc2v 2855 |
. . . . . . . 8
 
    
                  
                                       
                       |
23 | 2, 3, 22 | syl2anc 411 |
. . . . . . 7
    
                  
                                       
                       |
24 | 1, 23 | mpd 13 |
. . . . . 6
                    
                      |
25 | 24 | imp 124 |
. . . . 5
 

                  
                     |
26 | 25 | simprd 114 |
. . . 4
 

                    |
27 | | caucvgpr.f |
. . . . . . . 8
       |
28 | 27, 2 | ffvelcdmd 5653 |
. . . . . . 7
       |
29 | | nnnq 7421 |
. . . . . . . 8
        |
30 | | recclnq 7391 |
. . . . . . . 8
             
  |
31 | 2, 29, 30 | 3syl 17 |
. . . . . . 7
           |
32 | | addclnq 7374 |
. . . . . . 7
             
                 |
33 | 28, 31, 32 | syl2anc 411 |
. . . . . 6
                 |
34 | | nnnq 7421 |
. . . . . . 7
        |
35 | | recclnq 7391 |
. . . . . . 7
             
  |
36 | 3, 34, 35 | 3syl 17 |
. . . . . 6
           |
37 | | ltaddnq 7406 |
. . . . . 6
                       
                                         |
38 | 33, 36, 37 | syl2anc 411 |
. . . . 5
                                         |
39 | 38 | adantr 276 |
. . . 4
 

                                        |
40 | | ltsonq 7397 |
. . . . 5
 |
41 | | ltrelnq 7364 |
. . . . 5
   |
42 | 40, 41 | sotri 5025 |
. . . 4
                                                          
                              |
43 | 26, 39, 42 | syl2anc 411 |
. . 3
 

                              |
44 | | ltaddnq 7406 |
. . . . . . 7
             
                     |
45 | 28, 31, 44 | syl2anc 411 |
. . . . . 6
                     |
46 | 45 | adantr 276 |
. . . . 5
 
                     |
47 | | fveq2 5516 |
. . . . . . 7
           |
48 | 47 | breq1d 4014 |
. . . . . 6
                   
                     |
49 | 48 | adantl 277 |
. . . . 5
 
                   
                     |
50 | 46, 49 | mpbid 147 |
. . . 4
 
                     |
51 | 38 | adantr 276 |
. . . 4
 
                                         |
52 | 50, 51, 42 | syl2anc 411 |
. . 3
 
                               |
53 | | breq1 4007 |
. . . . . . . . . 10
 
   |
54 | | fveq2 5516 |
. . . . . . . . . . . 12
           |
55 | | opeq1 3779 |
. . . . . . . . . . . . . . 15
   
     |
56 | 55 | eceq1d 6571 |
. . . . . . . . . . . . . 14
            |
57 | 56 | fveq2d 5520 |
. . . . . . . . . . . . 13
                   |
58 | 57 | oveq2d 5891 |
. . . . . . . . . . . 12
                               |
59 | 54, 58 | breq12d 4017 |
. . . . . . . . . . 11
                   
                     |
60 | 54, 57 | oveq12d 5893 |
. . . . . . . . . . . 12
                               |
61 | 60 | breq2d 4016 |
. . . . . . . . . . 11
                   
                     |
62 | 59, 61 | anbi12d 473 |
. . . . . . . . . 10
                    
                  
                  
                      |
63 | 53, 62 | imbi12d 234 |
. . . . . . . . 9
                     
                   

                  
                       |
64 | | breq2 4008 |
. . . . . . . . . 10
 
   |
65 | | fveq2 5516 |
. . . . . . . . . . . . 13
           |
66 | 65 | oveq1d 5890 |
. . . . . . . . . . . 12
                               |
67 | 66 | breq2d 4016 |
. . . . . . . . . . 11
                   
                     |
68 | 65 | breq1d 4014 |
. . . . . . . . . . 11
                   
                     |
69 | 67, 68 | anbi12d 473 |
. . . . . . . . . 10
                    
                  
                  
                      |
70 | 64, 69 | imbi12d 234 |
. . . . . . . . 9
                     
                   

                  
                       |
71 | 63, 70 | rspc2v 2855 |
. . . . . . . 8
 
    
                  
                                       
                       |
72 | 3, 2, 71 | syl2anc 411 |
. . . . . . 7
    
                  
                                       
                       |
73 | 1, 72 | mpd 13 |
. . . . . 6
                    
                      |
74 | 73 | imp 124 |
. . . . 5
 

                  
                     |
75 | 74 | simpld 112 |
. . . 4
 

                    |
76 | | ltanqg 7399 |
. . . . . . . 8
 
 
       |
77 | 76 | adantl 277 |
. . . . . . 7
 

  
       |
78 | | addcomnqg 7380 |
. . . . . . . 8
 
       |
79 | 78 | adantl 277 |
. . . . . . 7
 
         |
80 | 77, 28, 33, 36, 79 | caovord2d 6044 |
. . . . . 6
                                                             |
81 | 45, 80 | mpbid 147 |
. . . . 5
                                         |
82 | 81 | adantr 276 |
. . . 4
 

                                        |
83 | 40, 41 | sotri 5025 |
. . . 4
                                                          
                              |
84 | 75, 82, 83 | syl2anc 411 |
. . 3
 

                              |
85 | | pitri3or 7321 |
. . . 4
 
 
   |
86 | 2, 3, 85 | syl2anc 411 |
. . 3
 
   |
87 | 43, 52, 84, 86 | mpjao3dan 1307 |
. 2
                               |
88 | 27, 3 | ffvelcdmd 5653 |
. . . 4
       |
89 | | addclnq 7374 |
. . . . 5
                       
                           |
90 | 33, 36, 89 | syl2anc 411 |
. . . 4
                           |
91 | | so2nr 4322 |
. . . . 5
                                                            
                               |
92 | 40, 91 | mpan 424 |
. . . 4
                                                           
                               |
93 | 88, 90, 92 | syl2anc 411 |
. . 3
                                                             |
94 | | imnan 690 |
. . 3
                             
                            
                                                            |
95 | 93, 94 | sylibr 134 |
. 2
                             
                               |
96 | 87, 95 | mpd 13 |
1
                               |