Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . 4
    |
2 | | ioossre 11693 |
. . . 4
    |
3 | 1, 2 | eqsstri 3461 |
. . 3
 |
4 | | dvfsumlem1.2 |
. . 3
   |
5 | 3, 4 | sseldi 3429 |
. 2
   |
6 | | dvfsumlem1.1 |
. . . 4
   |
7 | 3, 6 | sseldi 3429 |
. . 3
   |
8 | | reflcl 12029 |
. . 3
       |
9 | | peano2re 9803 |
. . 3
             |
10 | 7, 8, 9 | 3syl 18 |
. 2
         |
11 | | dvfsum.z |
. . 3
     |
12 | | dvfsum.m |
. . . 4
   |
13 | 12 | adantr 467 |
. . 3
 
      
  |
14 | | dvfsum.d |
. . . 4
   |
15 | 14 | adantr 467 |
. . 3
 
      
  |
16 | | dvfsum.md |
. . . 4

    |
17 | 16 | adantr 467 |
. . 3
 
      
    |
18 | | dvfsum.t |
. . . 4
   |
19 | 18 | adantr 467 |
. . 3
 
      
  |
20 | | dvfsum.a |
. . . 4
 
   |
21 | 20 | adantlr 720 |
. . 3
             |
22 | | dvfsum.b1 |
. . . 4
 
   |
23 | 22 | adantlr 720 |
. . 3
             |
24 | | dvfsum.b2 |
. . . 4
 
   |
25 | 24 | adantlr 720 |
. . 3
             |
26 | | dvfsum.b3 |
. . . 4
         |
27 | 26 | adantr 467 |
. . 3
 
      
        |
28 | | dvfsum.c |
. . 3
   |
29 | | dvfsum.u |
. . . 4
   |
30 | 29 | adantr 467 |
. . 3
 
      
  |
31 | | dvfsum.l |
. . . 4
 

      |
32 | 31 | 3adant1r 1260 |
. . 3
          
 
    |
33 | | dvfsum.h |
. . 3
                         |
34 | 6 | adantr 467 |
. . 3
 
      
  |
35 | 4 | adantr 467 |
. . 3
 
      
  |
36 | | dvfsumlem1.3 |
. . . 4

  |
37 | 36 | adantr 467 |
. . 3
 
      
  |
38 | | dvfsumlem1.4 |
. . . 4

  |
39 | 38 | adantr 467 |
. . 3
 
      
  |
40 | | dvfsumlem1.5 |
. . . 4

  |
41 | 40 | adantr 467 |
. . 3
 
      
  |
42 | | simpr 463 |
. . 3
 
      
        |
43 | 1, 11, 13, 15, 17, 19, 21, 23, 25, 27, 28, 30, 32, 33, 34, 35, 37, 39, 41, 42 | dvfsumlem2 22972 |
. 2
 
      
        
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)     |
44 | 3 | a1i 11 |
. . . . . . . . . . 11

  |
45 | 44 | sselda 3431 |
. . . . . . . . . 10
 
   |
46 | | reflcl 12029 |
. . . . . . . . . . 11
       |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
 
       |
48 | 45, 47 | resubcld 10044 |
. . . . . . . . 9
 
         |
49 | 44, 20, 22, 26 | dvmptrecl 22969 |
. . . . . . . . 9
 
   |
50 | 48, 49 | remulcld 9668 |
. . . . . . . 8
 
           |
51 | | fzfid 12183 |
. . . . . . . . . 10
 
           |
52 | 24 | ralrimiva 2801 |
. . . . . . . . . . . 12
 
  |
53 | 52 | adantr 467 |
. . . . . . . . . . 11
 
 
  |
54 | | elfzuz 11793 |
. . . . . . . . . . . 12
        
      |
55 | 54, 11 | syl6eleqr 2539 |
. . . . . . . . . . 11
        
  |
56 | 28 | eleq1d 2512 |
. . . . . . . . . . . 12
 
   |
57 | 56 | rspccva 3148 |
. . . . . . . . . . 11
  
   |
58 | 53, 55, 57 | syl2an 480 |
. . . . . . . . . 10
            
  |
59 | 51, 58 | fsumrecl 13793 |
. . . . . . . . 9
 
             |
60 | 59, 20 | resubcld 10044 |
. . . . . . . 8
 
               |
61 | 50, 60 | readdcld 9667 |
. . . . . . 7
 
                         |
62 | 61, 33 | fmptd 6044 |
. . . . . 6
       |
63 | 62 | adantr 467 |
. . . . 5
 
      
      |
64 | 4 | adantr 467 |
. . . . 5
 
      
  |
65 | 63, 64 | ffvelrnd 6021 |
. . . 4
 
      
      |
66 | 5 | adantr 467 |
. . . . . . . 8
 
      
  |
67 | | reflcl 12029 |
. . . . . . . 8
       |
68 | 66, 67 | syl 17 |
. . . . . . 7
 
      
      |
69 | 18 | adantr 467 |
. . . . . . . 8
 
      
  |
70 | 7 | adantr 467 |
. . . . . . . . 9
 
      
  |
71 | 70, 8, 9 | 3syl 18 |
. . . . . . . 8
 
      
        |
72 | 6, 1 | syl6eleq 2538 |
. . . . . . . . . . . 12
      |
73 | 18 | rexrd 9687 |
. . . . . . . . . . . . 13
   |
74 | | elioopnf 11725 |
. . . . . . . . . . . . 13

         |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
          |
76 | 72, 75 | mpbid 214 |
. . . . . . . . . . 11
     |
77 | 76 | simprd 465 |
. . . . . . . . . 10
   |
78 | | fllep1 12034 |
. . . . . . . . . . 11
         |
79 | 7, 78 | syl 17 |
. . . . . . . . . 10

        |
80 | 18, 7, 10, 77, 79 | ltletrd 9792 |
. . . . . . . . 9
         |
81 | 80 | adantr 467 |
. . . . . . . 8
 
      
        |
82 | | simpr 463 |
. . . . . . . . 9
 
      
        |
83 | 70 | flcld 12031 |
. . . . . . . . . . 11
 
      
      |
84 | 83 | peano2zd 11040 |
. . . . . . . . . 10
 
      
        |
85 | | flge 12038 |
. . . . . . . . . 10
                     
       |
86 | 66, 84, 85 | syl2anc 666 |
. . . . . . . . 9
 
      
      
             |
87 | 82, 86 | mpbid 214 |
. . . . . . . 8
 
      
            |
88 | 69, 71, 68, 81, 87 | ltletrd 9792 |
. . . . . . 7
 
      
      |
89 | 73 | adantr 467 |
. . . . . . . 8
 
      
  |
90 | | elioopnf 11725 |
. . . . . . . 8

                     |
91 | 89, 90 | syl 17 |
. . . . . . 7
 
      
                     |
92 | 68, 88, 91 | mpbir2and 932 |
. . . . . 6
 
      
         |
93 | 92, 1 | syl6eleqr 2539 |
. . . . 5
 
      
      |
94 | 63, 93 | ffvelrnd 6021 |
. . . 4
 
      
          |
95 | 6 | adantr 467 |
. . . . 5
 
      
  |
96 | 63, 95 | ffvelrnd 6021 |
. . . 4
 
      
      |
97 | 12 | adantr 467 |
. . . . . 6
 
      
  |
98 | 14 | adantr 467 |
. . . . . 6
 
      
  |
99 | 16 | adantr 467 |
. . . . . 6
 
      
    |
100 | 20 | adantlr 720 |
. . . . . 6
         
   |
101 | 22 | adantlr 720 |
. . . . . 6
         
   |
102 | 24 | adantlr 720 |
. . . . . 6
         
   |
103 | 26 | adantr 467 |
. . . . . 6
 
      
        |
104 | 29 | adantr 467 |
. . . . . 6
 
      
  |
105 | 31 | 3adant1r 1260 |
. . . . . 6
          


    |
106 | 36 | adantr 467 |
. . . . . . . 8
 
      
  |
107 | 70, 78 | syl 17 |
. . . . . . . 8
 
      
        |
108 | 98, 70, 71, 106, 107 | letrd 9789 |
. . . . . . 7
 
      
        |
109 | 98, 71, 68, 108, 87 | letrd 9789 |
. . . . . 6
 
      
      |
110 | | flle 12032 |
. . . . . . 7
       |
111 | 66, 110 | syl 17 |
. . . . . 6
 
      
      |
112 | 40 | adantr 467 |
. . . . . 6
 
      
  |
113 | | fllep1 12034 |
. . . . . . . 8
         |
114 | 66, 113 | syl 17 |
. . . . . . 7
 
      
        |
115 | | flidm 12042 |
. . . . . . . . 9
               |
116 | 66, 115 | syl 17 |
. . . . . . . 8
 
      
              |
117 | 116 | oveq1d 6303 |
. . . . . . 7
 
      
                  |
118 | 114, 117 | breqtrrd 4428 |
. . . . . 6
 
      
            |
119 | 1, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 93, 64, 109, 111, 112, 118 | dvfsumlem2 22972 |
. . . . 5
 
      
                            ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)     |
120 | 119 | simpld 461 |
. . . 4
 
      
              |
121 | | elioopnf 11725 |
. . . . . . . . . 10

                           |
122 | 73, 121 | syl 17 |
. . . . . . . . 9
                            |
123 | 10, 80, 122 | mpbir2and 932 |
. . . . . . . 8
            |
124 | 123, 1 | syl6eleqr 2539 |
. . . . . . 7
         |
125 | 124 | adantr 467 |
. . . . . 6
 
      
        |
126 | 63, 125 | ffvelrnd 6021 |
. . . . 5
 
      
            |
127 | 66 | flcld 12031 |
. . . . . . 7
 
      
      |
128 | | eluz2 11162 |
. . . . . . 7
                                       |
129 | 84, 127, 87, 128 | syl3anbrc 1191 |
. . . . . 6
 
      
                |
130 | 63 | adantr 467 |
. . . . . . 7
         
                     |
131 | | elfzelz 11797 |
. . . . . . . . . . 11
                 |
132 | 131 | adantl 468 |
. . . . . . . . . 10
         
                 |
133 | 132 | zred 11037 |
. . . . . . . . 9
         
                 |
134 | 69 | adantr 467 |
. . . . . . . . . 10
         
                 |
135 | 71 | adantr 467 |
. . . . . . . . . 10
         
                       |
136 | 80 | ad2antrr 731 |
. . . . . . . . . 10
         
                       |
137 | | elfzle1 11799 |
. . . . . . . . . . 11
                       |
138 | 137 | adantl 468 |
. . . . . . . . . 10
         
                       |
139 | 134, 135,
133, 136, 138 | ltletrd 9792 |
. . . . . . . . 9
         
                 |
140 | 73 | ad2antrr 731 |
. . . . . . . . . 10
         
                 |
141 | | elioopnf 11725 |
. . . . . . . . . 10

         |
142 | 140, 141 | syl 17 |
. . . . . . . . 9
         
                        |
143 | 133, 139,
142 | mpbir2and 932 |
. . . . . . . 8
         
                    |
144 | 143, 1 | syl6eleqr 2539 |
. . . . . . 7
         
                 |
145 | 130, 144 | ffvelrnd 6021 |
. . . . . 6
         
                     |
146 | 97 | adantr 467 |
. . . . . . . 8
         
                   |
147 | 98 | adantr 467 |
. . . . . . . 8
         
                   |
148 | 16 | ad2antrr 731 |
. . . . . . . 8
         
                 
   |
149 | 69 | adantr 467 |
. . . . . . . 8
         
                   |
150 | 100 | adantlr 720 |
. . . . . . . 8
         

                    |
151 | 101 | adantlr 720 |
. . . . . . . 8
         

                    |
152 | 102 | adantlr 720 |
. . . . . . . 8
         

                    |
153 | 103 | adantr 467 |
. . . . . . . 8
         
                  
      |
154 | 104 | adantr 467 |
. . . . . . . 8
         
                   |
155 | 105 | 3adant1r 1260 |
. . . . . . . 8
         

                        |
156 | | elfzelz 11797 |
. . . . . . . . . . . 12
                   |
157 | 156 | adantl 468 |
. . . . . . . . . . 11
         
                   |
158 | 157 | zred 11037 |
. . . . . . . . . 10
         
                   |
159 | 71 | adantr 467 |
. . . . . . . . . . 11
         
                         |
160 | 80 | ad2antrr 731 |
. . . . . . . . . . 11
         
                         |
161 | | elfzle1 11799 |
. . . . . . . . . . . 12
                         |
162 | 161 | adantl 468 |
. . . . . . . . . . 11
         
                         |
163 | 149, 159,
158, 160, 162 | ltletrd 9792 |
. . . . . . . . . 10
         
                   |
164 | 149 | rexrd 9687 |
. . . . . . . . . . 11
         
                   |
165 | 164, 141 | syl 17 |
. . . . . . . . . 10
         
                          |
166 | 158, 163,
165 | mpbir2and 932 |
. . . . . . . . 9
         
                      |
167 | 166, 1 | syl6eleqr 2539 |
. . . . . . . 8
         
                   |
168 | | peano2re 9803 |
. . . . . . . . . . 11
     |
169 | 158, 168 | syl 17 |
. . . . . . . . . 10
         
                     |
170 | 158 | lep1d 10535 |
. . . . . . . . . . 11
         
                     |
171 | 149, 158,
169, 163, 170 | ltletrd 9792 |
. . . . . . . . . 10
         
                     |
172 | | elioopnf 11725 |
. . . . . . . . . . 11

               |
173 | 164, 172 | syl 17 |
. . . . . . . . . 10
         
                                |
174 | 169, 171,
173 | mpbir2and 932 |
. . . . . . . . 9
         
                        |
175 | 174, 1 | syl6eleqr 2539 |
. . . . . . . 8
         
                     |
176 | 108 | adantr 467 |
. . . . . . . . 9
         
                         |
177 | 147, 159,
158, 176, 162 | letrd 9789 |
. . . . . . . 8
         
                   |
178 | 169 | rexrd 9687 |
. . . . . . . . 9
         
                     |
179 | 68 | rexrd 9687 |
. . . . . . . . . 10
 
      
      |
180 | 179 | adantr 467 |
. . . . . . . . 9
         
                       |
181 | | elfzle2 11800 |
. . . . . . . . . . 11
                         |
182 | 181 | adantl 468 |
. . . . . . . . . 10
         
                         |
183 | | 1red 9655 |
. . . . . . . . . . 11
         
                   |
184 | 66 | adantr 467 |
. . . . . . . . . . . 12
         
                   |
185 | 184, 67 | syl 17 |
. . . . . . . . . . 11
         
                       |
186 | | leaddsub 10087 |
. . . . . . . . . . 11
 
       
   
         |
187 | 158, 183,
185, 186 | syl3anc 1267 |
. . . . . . . . . 10
         
                       
         |
188 | 182, 187 | mpbird 236 |
. . . . . . . . 9
         
                         |
189 | 66 | rexrd 9687 |
. . . . . . . . . . 11
 
      
  |
190 | 179, 189,
104, 111, 112 | xrletrd 11456 |
. . . . . . . . . 10
 
      
      |
191 | 190 | adantr 467 |
. . . . . . . . 9
         
                       |
192 | 178, 180,
154, 188, 191 | xrletrd 11456 |
. . . . . . . 8
         
                     |
193 | | flid 12041 |
. . . . . . . . . . . 12
       |
194 | 157, 193 | syl 17 |
. . . . . . . . . . 11
         
                       |
195 | 194 | eqcomd 2456 |
. . . . . . . . . 10
         
                       |
196 | 195 | oveq1d 6303 |
. . . . . . . . 9
         
                           |
197 | | eqle 9733 |
. . . . . . . . 9
    
                  |
198 | 169, 196,
197 | syl2anc 666 |
. . . . . . . 8
         
                           |
199 | 1, 11, 146, 147, 148, 149, 150, 151, 152, 153, 28, 154, 155, 33, 167, 175, 177, 170, 192, 198 | dvfsumlem2 22972 |
. . . . . . 7
         
                           
       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)     |
200 | 199 | simpld 461 |
. . . . . 6
         
                    
        |
201 | 129, 145,
200 | monoord2 12241 |
. . . . 5
 
      
                    |
202 | 71 | rexrd 9687 |
. . . . . . . 8
 
      
        |
203 | 202, 179,
104, 87, 190 | xrletrd 11456 |
. . . . . . 7
 
      
        |
204 | 71 | leidd 10177 |
. . . . . . 7
 
      
              |
205 | 1, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 95, 125, 106, 107, 203, 204 | dvfsumlem2 22972 |
. . . . . 6
 
      
              
       ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)     |
206 | 205 | simpld 461 |
. . . . 5
 
      
                |
207 | 94, 126, 96, 201, 206 | letrd 9789 |
. . . 4
 
      
              |
208 | 65, 94, 96, 120, 207 | letrd 9789 |
. . 3
 
      
          |
209 | 49 | ralrimiva 2801 |
. . . . . . . . 9
 
  |
210 | 209 | adantr 467 |
. . . . . . . 8
 
      

  |
211 | | nfcsb1v 3378 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)  |
212 | 211 | nfel1 2605 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)
 |
213 | | csbeq1a 3371 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
214 | 213 | eleq1d 2512 |
. . . . . . . . 9
 
  ![]_ ]_](_urbrack.gif)    |
215 | 212, 214 | rspc 3143 |
. . . . . . . 8
  
  ![]_ ]_](_urbrack.gif)
   |
216 | 210, 215 | mpan9 472 |
. . . . . . 7
         
   ![]_ ]_](_urbrack.gif)
  |
217 | 216 | ralrimiva 2801 |
. . . . . 6
 
      

  ![]_ ]_](_urbrack.gif)   |
218 | | csbeq1 3365 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
219 | 218 | eleq1d 2512 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
220 | 219 | rspcv 3145 |
. . . . . 6
  
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
221 | 95, 217, 220 | sylc 62 |
. . . . 5
 
      
  ![]_ ]_](_urbrack.gif)   |
222 | 96, 221 | resubcld 10044 |
. . . 4
 
      
       ![]_ ]_](_urbrack.gif)    |
223 | | csbeq1 3365 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
224 | 223 | eleq1d 2512 |
. . . . . . 7
      
 ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)
   |
225 | 224 | rspcv 3145 |
. . . . . 6
      
  ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)
   |
226 | 93, 217, 225 | sylc 62 |
. . . . 5
 
      
      ![]_ ]_](_urbrack.gif)   |
227 | 94, 226 | resubcld 10044 |
. . . 4
 
      
               ![]_ ]_](_urbrack.gif)    |
228 | | csbeq1 3365 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
229 | 228 | eleq1d 2512 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
230 | 229 | rspcv 3145 |
. . . . . 6
  
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
231 | 64, 217, 230 | sylc 62 |
. . . . 5
 
      
  ![]_ ]_](_urbrack.gif)   |
232 | 65, 231 | resubcld 10044 |
. . . 4
 
      
       ![]_ ]_](_urbrack.gif)    |
233 | | csbeq1 3365 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
234 | 233 | eleq1d 2512 |
. . . . . . . 8
        
 ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif)
   |
235 | 234 | rspcv 3145 |
. . . . . . 7
        
  ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif)
   |
236 | 125, 217,
235 | sylc 62 |
. . . . . 6
 
      
        ![]_ ]_](_urbrack.gif)   |
237 | 126, 236 | resubcld 10044 |
. . . . 5
 
      
                   ![]_ ]_](_urbrack.gif)    |
238 | 205 | simprd 465 |
. . . . 5
 
      
       ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)    |
239 | | vex 3047 |
. . . . . . . . 9
 |
240 | | fveq2 5863 |
. . . . . . . . . . 11
           |
241 | | csbeq1 3365 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
242 | 240, 241 | oveq12d 6306 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
243 | | eqid 2450 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    |
244 | | ovex 6316 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)   |
245 | 242, 243,
244 | fvmpt3i 5951 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    |
246 | 239, 245 | ax-mp 5 |
. . . . . . . 8
         ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)   |
247 | 144, 216 | syldan 473 |
. . . . . . . . 9
         
                 ![]_ ]_](_urbrack.gif)
  |
248 | 145, 247 | resubcld 10044 |
. . . . . . . 8
         
                      ![]_ ]_](_urbrack.gif)    |
249 | 246, 248 | syl5eqel 2532 |
. . . . . . 7
         
                        ![]_ ]_](_urbrack.gif)        |
250 | 199 | simprd 465 |
. . . . . . . 8
         
                        ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    |
251 | | ovex 6316 |
. . . . . . . . 9
   |
252 | | fveq2 5863 |
. . . . . . . . . . 11
          
    |
253 | | csbeq1 3365 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
254 | 252, 253 | oveq12d 6306 |
. . . . . . . . . 10
          ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    |
255 | 254, 243,
244 | fvmpt3i 5951 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)    |
256 | 251, 255 | ax-mp 5 |
. . . . . . . 8
         ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)   |
257 | 250, 246,
256 | 3brtr4g 4434 |
. . . . . . 7
         
                          ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)     
    |
258 | 129, 249,
257 | monoord 12240 |
. . . . . 6
 
      
         ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)            |
259 | | ovex 6316 |
. . . . . . 7
       |
260 | | fveq2 5863 |
. . . . . . . . 9
                       |
261 | | csbeq1 3365 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
262 | 260, 261 | oveq12d 6306 |
. . . . . . . 8
              ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)    |
263 | 262, 243,
244 | fvmpt3i 5951 |
. . . . . . 7
                ![]_ ]_](_urbrack.gif)                               ![]_ ]_](_urbrack.gif)    |
264 | 259, 263 | ax-mp 5 |
. . . . . 6
         ![]_ ]_](_urbrack.gif)                               ![]_ ]_](_urbrack.gif)   |
265 | | fvex 5873 |
. . . . . . 7
     |
266 | | fveq2 5863 |
. . . . . . . . 9
                   |
267 | | csbeq1 3365 |
. . . . . . . . 9
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
268 | 266, 267 | oveq12d 6306 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)    |
269 | 268, 243,
244 | fvmpt3i 5951 |
. . . . . . 7
              ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)    |
270 | 265, 269 | ax-mp 5 |
. . . . . 6
         ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)   |
271 | 258, 264,
270 | 3brtr3g 4433 |
. . . . 5
 
      
                   ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)    |
272 | 222, 237,
227, 238, 271 | letrd 9789 |
. . . 4
 
      
       ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)    |
273 | 119 | simprd 465 |
. . . 4
 
      
               ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
274 | 222, 227,
232, 272, 273 | letrd 9789 |
. . 3
 
      
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
275 | 208, 274 | jca 535 |
. 2
 
      
        
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)     |
276 | 5, 10, 43, 275 | lecasei 9737 |
1
                 ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)     |