Step | Hyp | Ref
| Expression |
1 | | ltsonq 7399 |
. . . 4
 |
2 | | ltrelnq 7366 |
. . . 4
   |
3 | 1, 2 | son2lpi 5027 |
. . 3
           |
4 | | simprl 529 |
. . . . . . 7
                                                   |
5 | | caucvgpr.cau |
. . . . . . . . . . . 12
                                             |
6 | | breq1 4008 |
. . . . . . . . . . . . . 14
 
   |
7 | | fveq2 5517 |
. . . . . . . . . . . . . . . 16
           |
8 | | opeq1 3780 |
. . . . . . . . . . . . . . . . . . 19
   
     |
9 | 8 | eceq1d 6573 |
. . . . . . . . . . . . . . . . . 18
            |
10 | 9 | fveq2d 5521 |
. . . . . . . . . . . . . . . . 17
                   |
11 | 10 | oveq2d 5893 |
. . . . . . . . . . . . . . . 16
                               |
12 | 7, 11 | breq12d 4018 |
. . . . . . . . . . . . . . 15
                   
                     |
13 | 7, 10 | oveq12d 5895 |
. . . . . . . . . . . . . . . 16
                               |
14 | 13 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
15 | 12, 14 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
16 | 6, 15 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
17 | | breq2 4009 |
. . . . . . . . . . . . . 14
 
   |
18 | | fveq2 5517 |
. . . . . . . . . . . . . . . . 17
           |
19 | 18 | oveq1d 5892 |
. . . . . . . . . . . . . . . 16
                               |
20 | 19 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
21 | 18 | breq1d 4015 |
. . . . . . . . . . . . . . 15
                   
                     |
22 | 20, 21 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
23 | 17, 22 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
24 | 16, 23 | cbvral2v 2718 |
. . . . . . . . . . . 12
 
                    
                   
  
                  
                      |
25 | 5, 24 | sylib 122 |
. . . . . . . . . . 11
                                             |
26 | | caucvgprlemnkj.k |
. . . . . . . . . . . 12
   |
27 | | caucvgprlemnkj.j |
. . . . . . . . . . . 12
   |
28 | | breq1 4008 |
. . . . . . . . . . . . . 14
 
   |
29 | | fveq2 5517 |
. . . . . . . . . . . . . . . 16
           |
30 | | opeq1 3780 |
. . . . . . . . . . . . . . . . . . 19
   
     |
31 | 30 | eceq1d 6573 |
. . . . . . . . . . . . . . . . . 18
            |
32 | 31 | fveq2d 5521 |
. . . . . . . . . . . . . . . . 17
                   |
33 | 32 | oveq2d 5893 |
. . . . . . . . . . . . . . . 16
                               |
34 | 29, 33 | breq12d 4018 |
. . . . . . . . . . . . . . 15
                   
                     |
35 | 29, 32 | oveq12d 5895 |
. . . . . . . . . . . . . . . 16
                               |
36 | 35 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
37 | 34, 36 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
38 | 28, 37 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
39 | | breq2 4009 |
. . . . . . . . . . . . . 14
 
   |
40 | | fveq2 5517 |
. . . . . . . . . . . . . . . . 17
           |
41 | 40 | oveq1d 5892 |
. . . . . . . . . . . . . . . 16
                               |
42 | 41 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
43 | 40 | breq1d 4015 |
. . . . . . . . . . . . . . 15
                   
                     |
44 | 42, 43 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
45 | 39, 44 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
46 | 38, 45 | rspc2v 2856 |
. . . . . . . . . . . 12
 
                       
                                       
                       |
47 | 26, 27, 46 | syl2anc 411 |
. . . . . . . . . . 11
                       
                                       
                       |
48 | 25, 47 | mpd 13 |
. . . . . . . . . 10
                    
                      |
49 | 48 | imp 124 |
. . . . . . . . 9
 

                  
                     |
50 | 49 | simpld 112 |
. . . . . . . 8
 

                    |
51 | 50 | adantr 276 |
. . . . . . 7
                                                       |
52 | 1, 2 | sotri 5026 |
. . . . . . 7
                                                             |
53 | 4, 51, 52 | syl2anc 411 |
. . . . . 6
                                                             |
54 | | ltanqg 7401 |
. . . . . . . 8
 
 
       |
55 | 54 | adantl 277 |
. . . . . . 7
                                    
  
       |
56 | | caucvgprlemnkj.s |
. . . . . . . 8
   |
57 | 56 | ad2antrr 488 |
. . . . . . 7
                                     |
58 | | caucvgpr.f |
. . . . . . . . 9
       |
59 | 58, 27 | ffvelcdmd 5654 |
. . . . . . . 8
       |
60 | 59 | ad2antrr 488 |
. . . . . . 7
                                         |
61 | | nnnq 7423 |
. . . . . . . . 9
        |
62 | | recclnq 7393 |
. . . . . . . . 9
             
  |
63 | 26, 61, 62 | 3syl 17 |
. . . . . . . 8
           |
64 | 63 | ad2antrr 488 |
. . . . . . 7
                                             |
65 | | addcomnqg 7382 |
. . . . . . . 8
 
       |
66 | 65 | adantl 277 |
. . . . . . 7
                                    
        |
67 | 55, 57, 60, 64, 66 | caovord2d 6046 |
. . . . . 6
                                                                   |
68 | 53, 67 | mpbird 167 |
. . . . 5
                                         |
69 | | nnnq 7423 |
. . . . . . . . 9
        |
70 | | recclnq 7393 |
. . . . . . . . 9
             
  |
71 | 27, 69, 70 | 3syl 17 |
. . . . . . . 8
           |
72 | 71 | ad2antrr 488 |
. . . . . . 7
                                             |
73 | | ltaddnq 7408 |
. . . . . . 7
             
                     |
74 | 60, 72, 73 | syl2anc 411 |
. . . . . 6
                                                       |
75 | | simprr 531 |
. . . . . 6
                                                   |
76 | 1, 2 | sotri 5026 |
. . . . . 6
                                         |
77 | 74, 75, 76 | syl2anc 411 |
. . . . 5
                                         |
78 | 68, 77 | jca 306 |
. . . 4
                                               |
79 | 78 | ex 115 |
. . 3
 

                                            |
80 | 3, 79 | mtoi 664 |
. 2
 

                                |
81 | 1, 2 | son2lpi 5027 |
. . 3
                                           |
82 | | opeq1 3780 |
. . . . . . . . . . . 12
         |
83 | 82 | eceq1d 6573 |
. . . . . . . . . . 11
            |
84 | 83 | fveq2d 5521 |
. . . . . . . . . 10
                   |
85 | 84 | oveq2d 5893 |
. . . . . . . . 9
                       |
86 | | fveq2 5517 |
. . . . . . . . 9
           |
87 | 85, 86 | breq12d 4018 |
. . . . . . . 8
               
                 |
88 | 87 | anbi1d 465 |
. . . . . . 7
                               
              
                  |
89 | 88 | adantl 277 |
. . . . . 6
 
                               
              
                  |
90 | 54 | adantl 277 |
. . . . . . . . 9
 

  
       |
91 | | addclnq 7376 |
. . . . . . . . . 10
         
             |
92 | 56, 71, 91 | syl2anc 411 |
. . . . . . . . 9
             |
93 | 65 | adantl 277 |
. . . . . . . . 9
 
         |
94 | 90, 92, 59, 71, 93 | caovord2d 6046 |
. . . . . . . 8
                                                     |
95 | 94 | adantr 276 |
. . . . . . 7
 
               
                                     |
96 | 95 | anbi1d 465 |
. . . . . 6
 
                               
                                                     |
97 | 89, 96 | bitrd 188 |
. . . . 5
 
                               
                                                     |
98 | 1, 2 | sotri 5026 |
. . . . 5
                                                                         |
99 | 97, 98 | biimtrdi 163 |
. . . 4
 
                                                       |
100 | | ltaddnq 7408 |
. . . . . . 7
         

            |
101 | 56, 71, 100 | syl2anc 411 |
. . . . . 6

            |
102 | | ltaddnq 7408 |
. . . . . . 7
                   
                                 |
103 | 92, 71, 102 | syl2anc 411 |
. . . . . 6
                                 |
104 | 1, 2 | sotri 5026 |
. . . . . 6
 
          
                             
                      |
105 | 101, 103,
104 | syl2anc 411 |
. . . . 5

                      |
106 | 105 | adantr 276 |
. . . 4
 
                       |
107 | 99, 106 | jctird 317 |
. . 3
 
                                                    
                        |
108 | 81, 107 | mtoi 664 |
. 2
 
                                 |
109 | 1, 2 | son2lpi 5027 |
. . 3
                               |
110 | 56 | ad2antrr 488 |
. . . . . . 7
                                     |
111 | 63 | ad2antrr 488 |
. . . . . . 7
                                             |
112 | | ltaddnq 7408 |
. . . . . . 7
         

            |
113 | 110, 111,
112 | syl2anc 411 |
. . . . . 6
                                               |
114 | | simprl 529 |
. . . . . . 7
                                                   |
115 | | breq1 4008 |
. . . . . . . . . . . . . 14
 
   |
116 | | fveq2 5517 |
. . . . . . . . . . . . . . . 16
           |
117 | | opeq1 3780 |
. . . . . . . . . . . . . . . . . . 19
   
     |
118 | 117 | eceq1d 6573 |
. . . . . . . . . . . . . . . . . 18
            |
119 | 118 | fveq2d 5521 |
. . . . . . . . . . . . . . . . 17
                   |
120 | 119 | oveq2d 5893 |
. . . . . . . . . . . . . . . 16
                               |
121 | 116, 120 | breq12d 4018 |
. . . . . . . . . . . . . . 15
                   
                     |
122 | 116, 119 | oveq12d 5895 |
. . . . . . . . . . . . . . . 16
                               |
123 | 122 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
124 | 121, 123 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
125 | 115, 124 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
126 | | breq2 4009 |
. . . . . . . . . . . . . 14
 
   |
127 | | fveq2 5517 |
. . . . . . . . . . . . . . . . 17
           |
128 | 127 | oveq1d 5892 |
. . . . . . . . . . . . . . . 16
                               |
129 | 128 | breq2d 4017 |
. . . . . . . . . . . . . . 15
                   
                     |
130 | 127 | breq1d 4015 |
. . . . . . . . . . . . . . 15
                   
                     |
131 | 129, 130 | anbi12d 473 |
. . . . . . . . . . . . . 14
                    
                  
                  
                      |
132 | 126, 131 | imbi12d 234 |
. . . . . . . . . . . . 13
                     
                   

                  
                       |
133 | 125, 132 | rspc2v 2856 |
. . . . . . . . . . . 12
 
                       
                                       
                       |
134 | 27, 26, 133 | syl2anc 411 |
. . . . . . . . . . 11
                       
                                       
                       |
135 | 25, 134 | mpd 13 |
. . . . . . . . . 10
                    
                      |
136 | 135 | imp 124 |
. . . . . . . . 9
 

                  
                     |
137 | 136 | simprd 114 |
. . . . . . . 8
 

                    |
138 | 137 | adantr 276 |
. . . . . . 7
                                                       |
139 | 1, 2 | sotri 5026 |
. . . . . . 7
                                                             |
140 | 114, 138,
139 | syl2anc 411 |
. . . . . 6
                                                             |
141 | 1, 2 | sotri 5026 |
. . . . . 6
 
          
                                        |
142 | 113, 140,
141 | syl2anc 411 |
. . . . 5
                                                   |
143 | | simprr 531 |
. . . . 5
                                                   |
144 | 142, 143 | jca 306 |
. . . 4
                                                 
                 |
145 | 144 | ex 115 |
. . 3
 

                                             
                  |
146 | 109, 145 | mtoi 664 |
. 2
 

                                |
147 | | pitri3or 7323 |
. . 3
 
 
   |
148 | 26, 27, 147 | syl2anc 411 |
. 2
 
   |
149 | 80, 108, 146, 148 | mpjao3dan 1307 |
1
               
                 |