Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . 9
    |
2 | | ioossre 11721 |
. . . . . . . . 9
    |
3 | 1, 2 | eqsstri 3448 |
. . . . . . . 8
 |
4 | | dvfsumlem1.2 |
. . . . . . . 8
   |
5 | 3, 4 | sseldi 3416 |
. . . . . . 7
   |
6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
   |
7 | 6, 1 | syl6eleq 2559 |
. . . . . . . . . 10
      |
8 | | dvfsum.t |
. . . . . . . . . . . 12
   |
9 | 8 | rexrd 9708 |
. . . . . . . . . . 11
   |
10 | | elioopnf 11753 |
. . . . . . . . . . 11

         |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
          |
12 | 7, 11 | mpbid 215 |
. . . . . . . . 9
     |
13 | 12 | simpld 466 |
. . . . . . . 8
   |
14 | | reflcl 12065 |
. . . . . . . 8
       |
15 | 13, 14 | syl 17 |
. . . . . . 7
       |
16 | 5, 15 | resubcld 10068 |
. . . . . 6
         |
17 | 13 | rexrd 9708 |
. . . . . . . 8
   |
18 | 5 | rexrd 9708 |
. . . . . . . 8
   |
19 | | dvfsumlem1.4 |
. . . . . . . 8

  |
20 | | ubicc2 11775 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    |
21 | 17, 18, 19, 20 | syl3anc 1292 |
. . . . . . 7
   ![[,] [,]](_icc.gif)    |
22 | | pnfxr 11435 |
. . . . . . . . . . . . 13
 |
23 | 22 | a1i 11 |
. . . . . . . . . . . 12
   |
24 | 12 | simprd 470 |
. . . . . . . . . . . 12
   |
25 | | ltpnf 11445 |
. . . . . . . . . . . . 13
   |
26 | 5, 25 | syl 17 |
. . . . . . . . . . . 12
   |
27 | | iccssioo 11728 |
. . . . . . . . . . . 12
         ![[,] [,]](_icc.gif) 
     |
28 | 9, 23, 24, 26, 27 | syl22anc 1293 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
     |
29 | 28, 1 | syl6sseqr 3465 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif) 
  |
30 | 29 | sselda 3418 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
  |
31 | 3 | a1i 11 |
. . . . . . . . . . . . 13

  |
32 | | dvfsum.a |
. . . . . . . . . . . . 13
 
   |
33 | | dvfsum.b1 |
. . . . . . . . . . . . 13
 
   |
34 | | dvfsum.b3 |
. . . . . . . . . . . . 13
         |
35 | 31, 32, 33, 34 | dvmptrecl 23055 |
. . . . . . . . . . . 12
 
   |
36 | | eqid 2471 |
. . . . . . . . . . . 12
     |
37 | 35, 36 | fmptd 6061 |
. . . . . . . . . . 11
         |
38 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
39 | | nfcsb1v 3365 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)  |
40 | | csbeq1a 3358 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)   |
41 | 38, 39, 40 | cbvmpt 4487 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)   |
42 | 41 | fmpt 6058 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)         |
43 | 37, 42 | sylibr 217 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
  |
44 | 43 | r19.21bi 2776 |
. . . . . . . . 9
 
   ![]_ ]_](_urbrack.gif)   |
45 | 30, 44 | syldan 478 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   |
46 | 45 | ralrimiva 2809 |
. . . . . . 7
    ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  |
47 | | csbeq1 3352 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
48 | 47 | eleq1d 2533 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
49 | 48 | rspcv 3132 |
. . . . . . 7
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
50 | 21, 46, 49 | sylc 61 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)
  |
51 | 16, 50 | remulcld 9689 |
. . . . 5
          ![]_ ]_](_urbrack.gif)    |
52 | | eqid 2471 |
. . . . . . . . . . 11
     |
53 | 32, 52 | fmptd 6061 |
. . . . . . . . . 10
         |
54 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
55 | | nfcsb1v 3365 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
56 | | csbeq1a 3358 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
57 | 54, 55, 56 | cbvmpt 4487 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)   |
58 | 57 | fmpt 6058 |
. . . . . . . . . 10
 
  ![]_ ]_](_urbrack.gif)         |
59 | 53, 58 | sylibr 217 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)
  |
60 | 59 | r19.21bi 2776 |
. . . . . . . 8
 
   ![]_ ]_](_urbrack.gif)   |
61 | 30, 60 | syldan 478 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   |
62 | 61 | ralrimiva 2809 |
. . . . . 6
    ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  |
63 | | csbeq1 3352 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
64 | 63 | eleq1d 2533 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
65 | 64 | rspcv 3132 |
. . . . . 6
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
66 | 21, 62, 65 | sylc 61 |
. . . . 5
   ![]_ ]_](_urbrack.gif)
  |
67 | 51, 66 | resubcld 10068 |
. . . 4
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
68 | 13, 15 | resubcld 10068 |
. . . . . 6
         |
69 | | lbicc2 11774 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)    |
70 | 17, 18, 19, 69 | syl3anc 1292 |
. . . . . . 7
   ![[,] [,]](_icc.gif)    |
71 | | csbeq1 3352 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
72 | 71 | eleq1d 2533 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
73 | 72 | rspcv 3132 |
. . . . . . 7
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
74 | 70, 46, 73 | sylc 61 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)
  |
75 | 68, 74 | remulcld 9689 |
. . . . 5
          ![]_ ]_](_urbrack.gif)    |
76 | | csbeq1 3352 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
77 | 76 | eleq1d 2533 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
78 | 77 | rspcv 3132 |
. . . . . 6
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
79 | 70, 62, 78 | sylc 61 |
. . . . 5
   ![]_ ]_](_urbrack.gif)
  |
80 | 75, 79 | resubcld 10068 |
. . . 4
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
81 | | fzfid 12224 |
. . . . 5
           |
82 | | dvfsum.b2 |
. . . . . . 7
 
   |
83 | 82 | ralrimiva 2809 |
. . . . . 6
 
  |
84 | | elfzuz 11822 |
. . . . . . 7
        
      |
85 | | dvfsum.z |
. . . . . . 7
     |
86 | 84, 85 | syl6eleqr 2560 |
. . . . . 6
        
  |
87 | | dvfsum.c |
. . . . . . . 8
   |
88 | 87 | eleq1d 2533 |
. . . . . . 7
 
   |
89 | 88 | rspccva 3135 |
. . . . . 6
  
   |
90 | 83, 86, 89 | syl2an 485 |
. . . . 5
 
        
  |
91 | 81, 90 | fsumrecl 13877 |
. . . 4
             |
92 | 68, 50 | remulcld 9689 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)    |
93 | 92, 79 | resubcld 10068 |
. . . . 5
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
94 | 5, 13 | resubcld 10068 |
. . . . . . . . 9
     |
95 | 50, 94 | remulcld 9689 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif) 
    |
96 | 50 | recnd 9687 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)
  |
97 | 5 | recnd 9687 |
. . . . . . . . . 10
   |
98 | 13 | recnd 9687 |
. . . . . . . . . 10
   |
99 | 96, 97, 98 | subdid 10095 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
100 | | eqid 2471 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
101 | 100 | mulcn 21977 |
. . . . . . . . . . 11
    ℂfld   ℂfld   ℂfld  |
102 | 28, 2 | syl6ss 3430 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif) 
  |
103 | | ax-resscn 9614 |
. . . . . . . . . . . . 13
 |
104 | 102, 103 | syl6ss 3430 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
105 | 103 | a1i 11 |
. . . . . . . . . . . 12

  |
106 | | cncfmptc 22021 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
  ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)       |
107 | 50, 104, 105, 106 | syl3anc 1292 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)       |
108 | | cncfmptid 22022 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
109 | 102, 103,
108 | sylancl 675 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
110 | | remulcl 9642 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
111 | 100, 101,
107, 109, 103, 110 | cncfmpt2ss 22025 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)      ![[,] [,]](_icc.gif)       |
112 | | reelprrecn 9649 |
. . . . . . . . . . . . 13
    |
113 | 112 | a1i 11 |
. . . . . . . . . . . 12
      |
114 | | ioossicc 11745 |
. . . . . . . . . . . . . . 15
      ![[,] [,]](_icc.gif)   |
115 | 114, 102 | syl5ss 3429 |
. . . . . . . . . . . . . 14
    
  |
116 | 115 | sselda 3418 |
. . . . . . . . . . . . 13
 
    
  |
117 | 116 | recnd 9687 |
. . . . . . . . . . . 12
 
    
  |
118 | | 1cnd 9677 |
. . . . . . . . . . . 12
 
    
  |
119 | | simpr 468 |
. . . . . . . . . . . . . 14
 

  |
120 | 119 | recnd 9687 |
. . . . . . . . . . . . 13
 

  |
121 | | 1cnd 9677 |
. . . . . . . . . . . . 13
 

  |
122 | 113 | dvmptid 22990 |
. . . . . . . . . . . . 13
         |
123 | 100 | tgioo2 21899 |
. . . . . . . . . . . . 13
       ℂfld
↾t   |
124 | | iooretop 21864 |
. . . . . . . . . . . . . 14
         |
125 | 124 | a1i 11 |
. . . . . . . . . . . . 13
           |
126 | 113, 120,
121, 122, 115, 123, 100, 125 | dvmptres 22996 |
. . . . . . . . . . . 12
                 |
127 | 113, 117,
118, 126, 96 | dvmptcmul 22997 |
. . . . . . . . . . 11
          ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)     |
128 | 96 | mulid1d 9678 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
129 | 128 | mpteq2dv 4483 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
130 | 127, 129 | eqtrd 2505 |
. . . . . . . . . 10
          ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)    |
131 | 29 | resmptd 5162 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)    |
132 | 32 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
   |
133 | 132, 52 | fmptd 6061 |
. . . . . . . . . . . . . . . 16
         |
134 | 34 | dmeqd 5042 |
. . . . . . . . . . . . . . . . 17
  
      |
135 | 33 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . 18
 
  |
136 | | dmmptg 5339 |
. . . . . . . . . . . . . . . . . 18
 
    |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . 17
     |
138 | 134, 137 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
  
    |
139 | | dvcn 22954 |
. . . . . . . . . . . . . . . 16
                       |
140 | 105, 133,
31, 138, 139 | syl31anc 1295 |
. . . . . . . . . . . . . . 15
         |
141 | | cncffvrn 22008 |
. . . . . . . . . . . . . . 15
 
                       |
142 | 103, 140,
141 | sylancr 676 |
. . . . . . . . . . . . . 14
                 |
143 | 53, 142 | mpbird 240 |
. . . . . . . . . . . . 13
         |
144 | 57, 143 | syl5eqelr 2554 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)        |
145 | | rescncf 22007 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)      ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        |
146 | 29, 144, 145 | sylc 61 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
147 | 131, 146 | eqeltrrd 2550 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)       |
148 | 60 | recnd 9687 |
. . . . . . . . . . 11
 
   ![]_ ]_](_urbrack.gif)   |
149 | 57 | oveq2i 6319 |
. . . . . . . . . . . 12
        ![]_ ]_](_urbrack.gif)    |
150 | 34, 149, 41 | 3eqtr3g 2528 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
151 | 114, 29 | syl5ss 3429 |
. . . . . . . . . . 11
    
  |
152 | 113, 148,
44, 150, 151, 123, 100, 125 | dvmptres 22996 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
153 | 114 | sseli 3414 |
. . . . . . . . . . 11
       ![[,] [,]](_icc.gif)    |
154 | | simpl 464 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
155 | 4 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
156 | | dvfsum.d |
. . . . . . . . . . . . . 14
   |
157 | 156 | adantr 472 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
158 | 13 | adantr 472 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
159 | | elicc2 11724 |
. . . . . . . . . . . . . . . 16
 
    ![[,] [,]](_icc.gif)  
    |
160 | 13, 5, 159 | syl2anc 673 |
. . . . . . . . . . . . . . 15
    ![[,] [,]](_icc.gif)  
    |
161 | 160 | biimpa 492 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)  

   |
162 | 161 | simp1d 1042 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
163 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14

  |
164 | 163 | adantr 472 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
165 | 161 | simp2d 1043 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  |
166 | 157, 158,
162, 164, 165 | letrd 9809 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
167 | 161 | simp3d 1044 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
168 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13

  |
169 | 168 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
  |
170 | | simp2r 1057 |
. . . . . . . . . . . . 13
 

   
  |
171 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
 
   |
172 | 171 | anbi2d 718 |
. . . . . . . . . . . . . . . 16
  
      |
173 | | breq2 4399 |
. . . . . . . . . . . . . . . . 17
 
   |
174 | | breq1 4398 |
. . . . . . . . . . . . . . . . 17
 
   |
175 | 173, 174 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . 16
  

     |
176 | 172, 175 | 3anbi23d 1368 |
. . . . . . . . . . . . . . 15
  

 
  

 
     |
177 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
178 | 177, 87 | csbie 3375 |
. . . . . . . . . . . . . . . . 17
  ![]_ ]_](_urbrack.gif)  |
179 | | csbeq1 3352 |
. . . . . . . . . . . . . . . . 17
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
180 | 178, 179 | syl5eqr 2519 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
181 | 180 | breq1d 4405 |
. . . . . . . . . . . . . . 15
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
182 | 176, 181 | imbi12d 327 |
. . . . . . . . . . . . . 14
    


    ![]_ ]_](_urbrack.gif) 
       
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
183 | | nfv 1769 |
. . . . . . . . . . . . . . . 16
  

 
   |
184 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
185 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
  |
186 | 184, 185,
39 | nfbr 4440 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)  |
187 | 183, 186 | nfim 2023 |
. . . . . . . . . . . . . . 15
    


    ![]_ ]_](_urbrack.gif)   |
188 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
 
   |
189 | 188 | anbi1d 719 |
. . . . . . . . . . . . . . . . 17
  
      |
190 | | breq2 4399 |
. . . . . . . . . . . . . . . . . 18
 
   |
191 | | breq1 4398 |
. . . . . . . . . . . . . . . . . 18
 
   |
192 | 190, 191 | 3anbi12d 1366 |
. . . . . . . . . . . . . . . . 17
  


    |
193 | 189, 192 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . 16
  

 
  

 
     |
194 | 40 | breq2d 4407 |
. . . . . . . . . . . . . . . 16
 
  ![]_ ]_](_urbrack.gif)    |
195 | 193, 194 | imbi12d 327 |
. . . . . . . . . . . . . . 15
    


  
         ![]_ ]_](_urbrack.gif)     |
196 | | dvfsum.l |
. . . . . . . . . . . . . . 15
 

      |
197 | 187, 195,
196 | chvar 2119 |
. . . . . . . . . . . . . 14
 

      ![]_ ]_](_urbrack.gif)   |
198 | 182, 197 | vtoclg 3093 |
. . . . . . . . . . . . 13
  

 
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
199 | 170, 198 | mpcom 36 |
. . . . . . . . . . . 12
 

    
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
200 | 154, 30, 155, 166, 167, 169, 199 | syl123anc 1309 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
201 | 153, 200 | sylan2 482 |
. . . . . . . . . 10
 
    
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
202 | | oveq2 6316 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
203 | | oveq2 6316 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
204 | 13, 5, 111, 130, 147, 152, 201, 70, 21, 19, 202, 76, 203, 63 | dvle 23038 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
   
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
205 | 99, 204 | eqbrtrd 4416 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif) 
 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
206 | 95, 66, 79, 205 | lesubd 10238 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
     |
207 | 92 | recnd 9687 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)    |
208 | 51 | recnd 9687 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)    |
209 | 66 | recnd 9687 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)
  |
210 | 207, 208,
209 | subsubd 10033 |
. . . . . . . 8
           ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
211 | 208, 207 | negsubdi2d 10021 |
. . . . . . . . . . 11
            ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     |
212 | 15 | recnd 9687 |
. . . . . . . . . . . . . . 15
       |
213 | 97, 98, 212 | nnncan2d 10040 |
. . . . . . . . . . . . . 14
                   |
214 | 213 | oveq1d 6323 |
. . . . . . . . . . . . 13
         
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
215 | 16 | recnd 9687 |
. . . . . . . . . . . . . 14
         |
216 | 68 | recnd 9687 |
. . . . . . . . . . . . . 14
         |
217 | 215, 216,
96 | subdird 10096 |
. . . . . . . . . . . . 13
         
        ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     |
218 | 94 | recnd 9687 |
. . . . . . . . . . . . . 14
     |
219 | 218, 96 | mulcomd 9682 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
220 | 214, 217,
219 | 3eqtr3d 2513 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif) 
    |
221 | 220 | negeqd 9889 |
. . . . . . . . . . 11
            ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)

    |
222 | 211, 221 | eqtr3d 2507 |
. . . . . . . . . 10
           ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif) 
    |
223 | 222 | oveq1d 6323 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)

    ![]_ ]_](_urbrack.gif)    |
224 | 95 | recnd 9687 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif) 
    |
225 | 224, 209 | negsubdid 10020 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)

    ![]_ ]_](_urbrack.gif)    |
226 | 223, 225 | eqtr4d 2508 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
227 | 224, 209 | negsubdi2d 10021 |
. . . . . . . 8
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
     |
228 | 210, 226,
227 | 3eqtrd 2509 |
. . . . . . 7
           ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)

     |
229 | 206, 228 | breqtrrd 4422 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)     |
230 | 79, 92, 67, 229 | lesubd 10238 |
. . . . 5
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
231 | | flle 12068 |
. . . . . . . . 9
       |
232 | 13, 231 | syl 17 |
. . . . . . . 8
    
  |
233 | 13, 15 | subge0d 10224 |
. . . . . . . 8
  
    
       |
234 | 232, 233 | mpbird 240 |
. . . . . . 7

        |
235 | 200 | ralrimiva 2809 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
236 | 71 | breq2d 4407 |
. . . . . . . . 9
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
237 | 236 | rspcv 3132 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
 ![]_ ]_](_urbrack.gif)    |
238 | 70, 235, 237 | sylc 61 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
239 | 50, 74, 68, 234, 238 | lemul2ad 10569 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    |
240 | 92, 75, 79, 239 | lesub1dd 10250 |
. . . . 5
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
241 | 67, 93, 80, 230, 240 | letrd 9809 |
. . . 4
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
          ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
242 | 67, 80, 91, 241 | leadd1dd 10248 |
. . 3
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
                     ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
            |
243 | | dvfsum.m |
. . . 4
   |
244 | | dvfsum.md |
. . . 4

    |
245 | | dvfsum.u |
. . . 4
   |
246 | | dvfsum.h |
. . . 4
                         |
247 | | dvfsumlem1.6 |
. . . 4

        |
248 | 1, 85, 243, 156, 244, 8, 32, 33, 82, 34, 87, 245, 196, 246, 6, 4, 163, 19, 168, 247 | dvfsumlem1 23057 |
. . 3
                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |
249 | 13 | leidd 10201 |
. . . 4

  |
250 | 17, 18, 245, 19, 168 | xrletrd 11482 |
. . . 4

  |
251 | | fllep1 12070 |
. . . . 5
         |
252 | 13, 251 | syl 17 |
. . . 4

        |
253 | 1, 85, 243, 156, 244, 8, 32, 33, 82, 34, 87, 245, 196, 246, 6, 6, 163, 249, 250, 252 | dvfsumlem1 23057 |
. . 3
                ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |
254 | 242, 248,
253 | 3brtr4d 4426 |
. 2
    
      |
255 | 80, 74 | resubcld 10068 |
. . . . 5
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
256 | 67, 50 | resubcld 10068 |
. . . . 5
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
257 | | peano2rem 9961 |
. . . . . . . . . . 11
                 |
258 | 68, 257 | syl 17 |
. . . . . . . . . 10
           |
259 | 258, 74 | remulcld 9689 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)    |
260 | 259, 79 | resubcld 10068 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
261 | | peano2rem 9961 |
. . . . . . . . . . 11
                 |
262 | 16, 261 | syl 17 |
. . . . . . . . . 10
           |
263 | 262, 74 | remulcld 9689 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)    |
264 | 263, 66 | resubcld 10068 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
265 | 262, 50 | remulcld 9689 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)    |
266 | 265, 66 | resubcld 10068 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
267 | 259 | recnd 9687 |
. . . . . . . . . . . . . 14
            ![]_ ]_](_urbrack.gif)    |
268 | 263 | recnd 9687 |
. . . . . . . . . . . . . 14
            ![]_ ]_](_urbrack.gif)    |
269 | 267, 268 | subcld 10005 |
. . . . . . . . . . . . 13
             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)     |
270 | 269, 209 | addcomd 9853 |
. . . . . . . . . . . 12
              ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)      |
271 | 267, 268,
209 | subsubd 10033 |
. . . . . . . . . . . 12
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
272 | 209, 268,
267 | subsub2d 10034 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)      |
273 | 270, 271,
272 | 3eqtr4d 2515 |
. . . . . . . . . . 11
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)      |
274 | | 1cnd 9677 |
. . . . . . . . . . . . . . . 16
   |
275 | 215, 216,
274 | nnncan2d 10040 |
. . . . . . . . . . . . . . 15
                          
        |
276 | 275, 213 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                       |
277 | 276 | oveq1d 6323 |
. . . . . . . . . . . . 13
                      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
278 | 262 | recnd 9687 |
. . . . . . . . . . . . . 14
           |
279 | 258 | recnd 9687 |
. . . . . . . . . . . . . 14
           |
280 | 74 | recnd 9687 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)
  |
281 | 278, 279,
280 | subdird 10096 |
. . . . . . . . . . . . 13
                      ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)     |
282 | 218, 280 | mulcomd 9682 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
283 | 277, 281,
282 | 3eqtr3d 2513 |
. . . . . . . . . . . 12
             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif) 
    |
284 | 283 | oveq2d 6324 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)

     |
285 | 273, 284 | eqtrd 2505 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
     |
286 | 74, 94 | remulcld 9689 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif) 
    |
287 | | cncfmptc 22021 |
. . . . . . . . . . . . . . 15
    ![]_ ]_](_urbrack.gif)
  ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)       |
288 | 74, 104, 105, 287 | syl3anc 1292 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)       |
289 | | remulcl 9642 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
290 | 100, 101,
288, 109, 103, 289 | cncfmpt2ss 22025 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)      ![[,] [,]](_icc.gif)       |
291 | 113, 117,
118, 126, 280 | dvmptcmul 22997 |
. . . . . . . . . . . . . 14
          ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)     |
292 | 280 | mulid1d 9678 |
. . . . . . . . . . . . . . 15
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
293 | 292 | mpteq2dv 4483 |
. . . . . . . . . . . . . 14
         ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
294 | 291, 293 | eqtrd 2505 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)    |
295 | 6 | adantr 472 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)  
  |
296 | 162 | rexrd 9708 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)  
  |
297 | 18 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)  
  |
298 | 245 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)  
  |
299 | 296, 297,
298, 167, 169 | xrletrd 11482 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)  
  |
300 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
301 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . 19
 
   |
302 | 301 | anbi2d 718 |
. . . . . . . . . . . . . . . . . 18
  
      |
303 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . 19
 
   |
304 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . 19
 
   |
305 | 303, 304 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . . . 18
  


    |
306 | 302, 305 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . . 17
  

 
  

 
     |
307 | | csbeq1 3352 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
308 | 178, 307 | syl5eqr 2519 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
309 | 308 | breq1d 4405 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
310 | 306, 309 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
    


    ![]_ ]_](_urbrack.gif) 
       
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
311 | | simp2l 1056 |
. . . . . . . . . . . . . . . . 17
 

   
  |
312 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . 19
  

 
   |
313 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . . . 20
  
 ![]_ ]_](_urbrack.gif)  |
314 | 184, 185,
313 | nfbr 4440 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)  |
315 | 312, 314 | nfim 2023 |
. . . . . . . . . . . . . . . . . 18
    


    ![]_ ]_](_urbrack.gif)   |
316 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
317 | 316 | anbi1d 719 |
. . . . . . . . . . . . . . . . . . . 20
  
      |
318 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
319 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
320 | 318, 319 | 3anbi12d 1366 |
. . . . . . . . . . . . . . . . . . . 20
  


    |
321 | 317, 320 | 3anbi23d 1368 |
. . . . . . . . . . . . . . . . . . 19
  

 
  

 
     |
322 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   |
323 | 322 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . 19
 
  ![]_ ]_](_urbrack.gif)    |
324 | 321, 323 | imbi12d 327 |
. . . . . . . . . . . . . . . . . 18
    


  
         ![]_ ]_](_urbrack.gif)     |
325 | 315, 324,
196 | vtoclg1f 3092 |
. . . . . . . . . . . . . . . . 17
  

 
    ![]_ ]_](_urbrack.gif)    |
326 | 311, 325 | mpcom 36 |
. . . . . . . . . . . . . . . 16
 

      ![]_ ]_](_urbrack.gif)   |
327 | 300, 310,
326 | vtocl 3086 |
. . . . . . . . . . . . . . 15
 

    
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
328 | 154, 295,
30, 164, 165, 299, 327 | syl123anc 1309 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
329 | 153, 328 | sylan2 482 |
. . . . . . . . . . . . 13
 
    
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
330 | | oveq2 6316 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
331 | | oveq2 6316 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
332 | 13, 5, 147, 152, 290, 294, 329, 70, 21, 19, 76, 330, 63, 331 | dvle 23038 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
333 | 280, 97, 98 | subdid 10095 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif) 
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
334 | 332, 333 | breqtrrd 4422 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)      |
335 | 66, 79, 286, 334 | subled 10237 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)  
 ![]_ ]_](_urbrack.gif)

     ![]_ ]_](_urbrack.gif)   |
336 | 285, 335 | eqbrtrd 4416 |
. . . . . . . . 9
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)   |
337 | 259, 264,
79, 336 | subled 10237 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
338 | 262 | renegcld 10067 |
. . . . . . . . . . . 12
            |
339 | | 1red 9676 |
. . . . . . . . . . . . . . . 16
   |
340 | 5, 15, 339 | lesubadd2d 10233 |
. . . . . . . . . . . . . . 15
       
         |
341 | 247, 340 | mpbird 240 |
. . . . . . . . . . . . . 14
         |
342 | 16, 339 | suble0d 10225 |
. . . . . . . . . . . . . 14
                   |
343 | 341, 342 | mpbird 240 |
. . . . . . . . . . . . 13
           |
344 | 262 | le0neg1d 10206 |
. . . . . . . . . . . . 13
                      |
345 | 343, 344 | mpbid 215 |
. . . . . . . . . . . 12

           |
346 | 50, 74, 338, 345, 238 | lemul2ad 10569 |
. . . . . . . . . . 11
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    |
347 | 278, 96 | mulneg1d 10092 |
. . . . . . . . . . 11
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    |
348 | 278, 280 | mulneg1d 10092 |
. . . . . . . . . . 11
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    |
349 | 346, 347,
348 | 3brtr3d 4425 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    |
350 | 263, 265 | lenegd 10213 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif) 
            ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)     |
351 | 349, 350 | mpbird 240 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif) 
           ![]_ ]_](_urbrack.gif)    |
352 | 263, 265,
66, 351 | lesub1dd 10250 |
. . . . . . . 8
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
353 | 260, 264,
266, 337, 352 | letrd 9809 |
. . . . . . 7
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
354 | 216, 274,
280 | subdird 10096 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
355 | 280 | mulid2d 9679 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
356 | 355 | oveq2d 6324 |
. . . . . . . . 9
           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
357 | 354, 356 | eqtrd 2505 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
358 | 357 | oveq1d 6323 |
. . . . . . 7
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
359 | 215, 274,
96 | subdird 10096 |
. . . . . . . . 9
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
360 | 96 | mulid2d 9679 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
361 | 360 | oveq2d 6324 |
. . . . . . . . 9
           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
362 | 359, 361 | eqtrd 2505 |
. . . . . . . 8
            ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
363 | 362 | oveq1d 6323 |
. . . . . . 7
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
364 | 353, 358,
363 | 3brtr3d 4425 |
. . . . . 6
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
365 | 75 | recnd 9687 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)    |
366 | 79 | recnd 9687 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)
  |
367 | 365, 366,
280 | sub32d 10037 |
. . . . . 6
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
368 | 208, 209,
96 | sub32d 10037 |
. . . . . 6
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
369 | 364, 367,
368 | 3brtr4d 4426 |
. . . . 5
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif) 
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
370 | 255, 256,
91, 369 | leadd1dd 10248 |
. . . 4
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |
371 | 80 | recnd 9687 |
. . . . 5
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
372 | 91 | recnd 9687 |
. . . . 5
             |
373 | 371, 372,
280 | addsubd 10026 |
. . . 4
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |
374 | 67 | recnd 9687 |
. . . . 5
           ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
375 | 374, 372,
96 | addsubd 10026 |
. . . 4
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               |
376 | 370, 373,
375 | 3brtr4d 4426 |
. . 3
             ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)    |
377 | 253 | oveq1d 6323 |
. . 3
        ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)    |
378 | 248 | oveq1d 6323 |
. . 3
        ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)    |
379 | 376, 377,
378 | 3brtr4d 4426 |
. 2
        ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)    |
380 | 254, 379 | jca 541 |
1
                 ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)     |