Step | Hyp | Ref
| Expression |
1 | | binomcxplem.s |
. . . 4
               |
2 | | binomcxplem.p |
. . . . 5
            |
3 | | binomcxplem.d |
. . . . . . 7
          |
4 | | nfcv 2592 |
. . . . . . . 8
    |
5 | | nfcv 2592 |
. . . . . . . . 9
   |
6 | | nfcv 2592 |
. . . . . . . . 9
   |
7 | | binomcxplem.r |
. . . . . . . . . 10
             |
8 | | nfcv 2592 |
. . . . . . . . . . . . . 14
  |
9 | | nfmpt1 4492 |
. . . . . . . . . . . . . . . 16
                 |
10 | 1, 9 | nfcxfr 2590 |
. . . . . . . . . . . . . . 15
   |
11 | | nfcv 2592 |
. . . . . . . . . . . . . . 15
   |
12 | 10, 11 | nffv 5872 |
. . . . . . . . . . . . . 14
       |
13 | 5, 8, 12 | nfseq 12223 |
. . . . . . . . . . . . 13
         |
14 | 13 | nfel1 2606 |
. . . . . . . . . . . 12
         |
15 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
16 | 14, 15 | nfrab 2972 |
. . . . . . . . . . 11
           |
17 | | nfcv 2592 |
. . . . . . . . . . 11
   |
18 | | nfcv 2592 |
. . . . . . . . . . 11
  |
19 | 16, 17, 18 | nfsup 7965 |
. . . . . . . . . 10
               |
20 | 7, 19 | nfcxfr 2590 |
. . . . . . . . 9
   |
21 | 5, 6, 20 | nfov 6316 |
. . . . . . . 8
       |
22 | 4, 21 | nfima 5176 |
. . . . . . 7
            |
23 | 3, 22 | nfcxfr 2590 |
. . . . . 6
   |
24 | | nfcv 2592 |
. . . . . 6
   |
25 | | nfcv 2592 |
. . . . . 6
            |
26 | | nfcv 2592 |
. . . . . . 7
   |
27 | | nfcv 2592 |
. . . . . . . . 9
   |
28 | 10, 27 | nffv 5872 |
. . . . . . . 8
       |
29 | | nfcv 2592 |
. . . . . . . 8
   |
30 | 28, 29 | nffv 5872 |
. . . . . . 7
           |
31 | 26, 30 | nfsum 13757 |
. . . . . 6
            |
32 | | simpl 459 |
. . . . . . . . . 10
 
   |
33 | 32 | fveq2d 5869 |
. . . . . . . . 9
 
           |
34 | 33 | fveq1d 5867 |
. . . . . . . 8
 
                   |
35 | 34 | sumeq2dv 13769 |
. . . . . . 7
          
          |
36 | | nfcv 2592 |
. . . . . . . 8
           |
37 | | nfcv 2592 |
. . . . . . . . . . . 12
   |
38 | | nfmpt1 4492 |
. . . . . . . . . . . 12
               |
39 | 37, 38 | nfmpt 4491 |
. . . . . . . . . . 11
                 |
40 | 1, 39 | nfcxfr 2590 |
. . . . . . . . . 10
   |
41 | | nfcv 2592 |
. . . . . . . . . 10
   |
42 | 40, 41 | nffv 5872 |
. . . . . . . . 9
       |
43 | | nfcv 2592 |
. . . . . . . . 9
   |
44 | 42, 43 | nffv 5872 |
. . . . . . . 8
           |
45 | | fveq2 5865 |
. . . . . . . 8
                   |
46 | 36, 44, 45 | cbvsumi 13763 |
. . . . . . 7
         
         |
47 | 35, 46 | syl6eq 2501 |
. . . . . 6
          
          |
48 | 23, 24, 25, 31, 47 | cbvmptf 4493 |
. . . . 5
            
          |
49 | 2, 48 | eqtri 2473 |
. . . 4
 
          |
50 | | ovex 6318 |
. . . . . 6
 C𝑐  |
51 | 50 | a1i 11 |
. . . . 5
 

 C𝑐   |
52 | | binomcxplem.f |
. . . . . 6
  C𝑐   |
53 | 52 | a1i 11 |
. . . . 5
 
 C𝑐    |
54 | 52 | a1i 11 |
. . . . . . 7
 

  C𝑐    |
55 | | simpr 463 |
. . . . . . . 8
       |
56 | 55 | oveq2d 6306 |
. . . . . . 7
      C𝑐  C𝑐   |
57 | | simpr 463 |
. . . . . . 7
 

  |
58 | | binomcxp.c |
. . . . . . . . 9
   |
59 | 58 | adantr 467 |
. . . . . . . 8
 

  |
60 | 59, 57 | bcccl 36688 |
. . . . . . 7
 

 C𝑐   |
61 | 54, 56, 57, 60 | fvmptd 5954 |
. . . . . 6
 

     C𝑐   |
62 | 61, 60 | eqeltrd 2529 |
. . . . 5
 

      |
63 | 51, 53, 62 | fmpt2d 6053 |
. . . 4
       |
64 | | nfcv 2592 |
. . . . . . 7
   |
65 | | nfcv 2592 |
. . . . . . 7
   |
66 | | nfv 1761 |
. . . . . . 7
         |
67 | | nfcv 2592 |
. . . . . . . . 9
   |
68 | | nfcv 2592 |
. . . . . . . . 9
  |
69 | | nfcv 2592 |
. . . . . . . . . . 11
                 |
70 | 1, 69 | nfcxfr 2590 |
. . . . . . . . . 10
   |
71 | | nfcv 2592 |
. . . . . . . . . 10
   |
72 | 70, 71 | nffv 5872 |
. . . . . . . . 9
       |
73 | 67, 68, 72 | nfseq 12223 |
. . . . . . . 8
         |
74 | 73 | nfel1 2606 |
. . . . . . 7
         |
75 | | fveq2 5865 |
. . . . . . . . 9
           |
76 | 75 | seqeq3d 12221 |
. . . . . . . 8
                 |
77 | 76 | eleq1d 2513 |
. . . . . . 7
                 |
78 | 64, 65, 66, 74, 77 | cbvrab 3043 |
. . . . . 6
                 |
79 | 78 | supeq1i 7961 |
. . . . 5
                         |
80 | 7, 79 | eqtri 2473 |
. . . 4
             |
81 | 1 | fveq1i 5866 |
. . . . . . . . . . . 12
                       |
82 | | seqeq3 12218 |
. . . . . . . . . . . 12
       
                          
                  |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . . . 11
                             |
84 | 83 | eleq1i 2520 |
. . . . . . . . . 10
                             |
85 | 84 | a1i 11 |
. . . . . . . . 9
                               |
86 | 85 | rabbiia 3033 |
. . . . . . . 8
                               |
87 | 86 | supeq1i 7961 |
. . . . . . 7
                                       |
88 | 7, 79, 87 | 3eqtrri 2478 |
. . . . . 6
       
                   |
89 | 88 | eleq1i 2520 |
. . . . 5
                          
  |
90 | 88 | oveq2i 6301 |
. . . . . 6
                                       |
91 | 90 | oveq1i 6300 |
. . . . 5
             
                             |
92 | | eqid 2451 |
. . . . 5
             |
93 | 89, 91, 92 | ifbieq12i 3907 |
. . . 4
                                          
                                                |
94 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . 18
           |
95 | 94 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
                       |
96 | 95 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . 16
                           |
97 | 96 | cbvmptv 4495 |
. . . . . . . . . . . . . . 15
 
             
             |
98 | 97 | fveq1i 5866 |
. . . . . . . . . . . . . 14
                    
                |
99 | | seqeq3 12218 |
. . . . . . . . . . . . . 14
                                                                                 |
100 | 98, 99 | ax-mp 5 |
. . . . . . . . . . . . 13
                         
                 |
101 | 100 | eleq1i 2520 |
. . . . . . . . . . . 12
                    
                      |
102 | 101 | a1i 11 |
. . . . . . . . . . 11
                     
                       |
103 | 102 | rabbiia 3033 |
. . . . . . . . . 10
                           
                 |
104 | 103 | supeq1i 7961 |
. . . . . . . . 9
       
                                             |
105 | 104 | eleq1i 2520 |
. . . . . . . 8
                          
       
                    |
106 | 104 | oveq2i 6301 |
. . . . . . . . 9
                                            
                    |
107 | 106 | oveq1i 6300 |
. . . . . . . 8
             
                                 
                     |
108 | 105, 107,
92 | ifbieq12i 3907 |
. . . . . . 7
                                          
                                                                      
                             |
109 | 108 | oveq2i 6301 |
. . . . . 6
                                               
                                                                            
                              |
110 | 109 | oveq1i 6300 |
. . . . 5
                                                
                                                                              
                               |
111 | 110 | oveq2i 6301 |
. . . 4
                                                        
                                                                                       
                                |
112 | 1, 49, 63, 80, 3, 93, 111 | pserdv2 23385 |
. . 3
                      |
113 | | cnvimass 5188 |
. . . . . . . 8
        
 |
114 | 3, 113 | eqsstri 3462 |
. . . . . . 7
 |
115 | | absf 13400 |
. . . . . . . 8
     |
116 | 115 | fdmi 5734 |
. . . . . . 7
 |
117 | 114, 116 | sseqtri 3464 |
. . . . . 6
 |
118 | 117 | sseli 3428 |
. . . . 5
   |
119 | | binomcxplem.e |
. . . . . . . . . 10
                   |
120 | 119 | a1i 11 |
. . . . . . . . 9
 

                    |
121 | | simplr 762 |
. . . . . . . . . . . 12
   



  |
122 | 121 | oveq1d 6305 |
. . . . . . . . . . 11
   



              |
123 | 122 | oveq2d 6306 |
. . . . . . . . . 10
   



                              |
124 | 123 | mpteq2dva 4489 |
. . . . . . . . 9
                                       |
125 | | simpr 463 |
. . . . . . . . 9
 

  |
126 | | nnex 10615 |
. . . . . . . . . . 11
 |
127 | 126 | mptex 6136 |
. . . . . . . . . 10
                 |
128 | 127 | a1i 11 |
. . . . . . . . 9
 

                  |
129 | 120, 124,
125, 128 | fvmptd 5954 |
. . . . . . . 8
 

                      |
130 | 129 | adantr 467 |
. . . . . . 7
                           |
131 | | simpr 463 |
. . . . . . . . 9
   

 
  |
132 | 131 | fveq2d 5869 |
. . . . . . . . 9
   

 
          |
133 | 131, 132 | oveq12d 6308 |
. . . . . . . 8
   

 
              |
134 | 131 | oveq1d 6305 |
. . . . . . . . 9
   

 
      |
135 | 134 | oveq2d 6306 |
. . . . . . . 8
   

 
              |
136 | 133, 135 | oveq12d 6308 |
. . . . . . 7
   

 
                              |
137 | | simpr 463 |
. . . . . . 7
       |
138 | | ovex 6318 |
. . . . . . . 8
               |
139 | 138 | a1i 11 |
. . . . . . 7
                     |
140 | 130, 136,
137, 139 | fvmptd 5954 |
. . . . . 6
                             |
141 | 140 | sumeq2dv 13769 |
. . . . 5
 

                          |
142 | 118, 141 | sylan2 477 |
. . . 4
 
                           |
143 | 142 | mpteq2dva 4489 |
. . 3
  
                            |
144 | 112, 143 | eqtr4d 2488 |
. 2
                |
145 | | nfcv 2592 |
. . . 4
   |
146 | | nfmpt1 4492 |
. . . . . . 7
                     |
147 | 119, 146 | nfcxfr 2590 |
. . . . . 6
   |
148 | 147, 27 | nffv 5872 |
. . . . 5
       |
149 | | nfcv 2592 |
. . . . 5
   |
150 | 148, 149 | nffv 5872 |
. . . 4
           |
151 | 145, 150 | nfsum 13757 |
. . 3
            |
152 | | nfcv 2592 |
. . 3
            |
153 | | simpl 459 |
. . . . . . 7
 
   |
154 | 153 | fveq2d 5869 |
. . . . . 6
 
           |
155 | 154 | fveq1d 5867 |
. . . . 5
 
                   |
156 | 155 | sumeq2dv 13769 |
. . . 4
                     |
157 | | nfmpt1 4492 |
. . . . . . . . 9
                   |
158 | 37, 157 | nfmpt 4491 |
. . . . . . . 8
                     |
159 | 119, 158 | nfcxfr 2590 |
. . . . . . 7
   |
160 | | nfcv 2592 |
. . . . . . 7
   |
161 | 159, 160 | nffv 5872 |
. . . . . 6
       |
162 | | nfcv 2592 |
. . . . . 6
   |
163 | 161, 162 | nffv 5872 |
. . . . 5
           |
164 | | nfcv 2592 |
. . . . 5
           |
165 | | fveq2 5865 |
. . . . 5
                   |
166 | 163, 164,
165 | cbvsumi 13763 |
. . . 4
         
         |
167 | 156, 166 | syl6eq 2501 |
. . 3
          
          |
168 | 24, 23, 151, 152, 167 | cbvmptf 4493 |
. 2
                       |
169 | 144, 168 | syl6eq 2501 |
1
                |