Step | Hyp | Ref
| Expression |
1 | | fzodisj 11130 |
. . . . . . . . 9
  ..^      ..^     |
2 | 1 | a1i 11 |
. . . . . . . 8
   ..^      ..^      |
3 | | dchrisumlem2.4 |
. . . . . . . . . . . 12
   |
4 | 3 | peano2nnd 9981 |
. . . . . . . . . . 11
     |
5 | | nnuz 10485 |
. . . . . . . . . . 11
     |
6 | 4, 5 | syl6eleq 2502 |
. . . . . . . . . 10
         |
7 | | dchrisumlem2.5 |
. . . . . . . . . . 11
       |
8 | | eluzp1p1 10475 |
. . . . . . . . . . 11
    
          |
9 | 7, 8 | syl 16 |
. . . . . . . . . 10
      
    |
10 | | elfzuzb 11017 |
. . . . . . . . . 10
        
      
           |
11 | 6, 9, 10 | sylanbrc 646 |
. . . . . . . . 9
           |
12 | | fzosplit 11129 |
. . . . . . . . 9
          ..^     ..^      ..^      |
13 | 11, 12 | syl 16 |
. . . . . . . 8
  ..^     ..^      ..^      |
14 | | fzofi 11276 |
. . . . . . . . 9
 ..^    |
15 | 14 | a1i 11 |
. . . . . . . 8
  ..^     |
16 | | elfzouz 11107 |
. . . . . . . . . 10
  ..^  
      |
17 | 16, 5 | syl6eleqr 2503 |
. . . . . . . . 9
  ..^  
  |
18 | | rpvmasum.g |
. . . . . . . . . . 11
DChr   |
19 | | rpvmasum.z |
. . . . . . . . . . 11
ℤ/nℤ   |
20 | | rpvmasum.d |
. . . . . . . . . . 11
     |
21 | | rpvmasum.l |
. . . . . . . . . . 11
 RHom   |
22 | | dchrisum.b |
. . . . . . . . . . . 12
   |
23 | 22 | adantr 452 |
. . . . . . . . . . 11
 

  |
24 | | nnz 10267 |
. . . . . . . . . . . 12
   |
25 | 24 | adantl 453 |
. . . . . . . . . . 11
 

  |
26 | 18, 19, 20, 21, 23, 25 | dchrzrhcl 20990 |
. . . . . . . . . 10
 

          |
27 | | nnrp 10585 |
. . . . . . . . . . . . 13
   |
28 | | rpvmasum.a |
. . . . . . . . . . . . . . 15
   |
29 | | rpvmasum.1 |
. . . . . . . . . . . . . . 15
     |
30 | | dchrisum.n1 |
. . . . . . . . . . . . . . 15
  |
31 | | dchrisum.2 |
. . . . . . . . . . . . . . 15
   |
32 | | dchrisum.3 |
. . . . . . . . . . . . . . 15
   |
33 | | dchrisum.4 |
. . . . . . . . . . . . . . 15
 

  |
34 | | dchrisum.5 |
. . . . . . . . . . . . . . 15
 
 
     |
35 | | dchrisum.6 |
. . . . . . . . . . . . . . 15
      |
36 | | dchrisum.7 |
. . . . . . . . . . . . . . 15
             |
37 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 21143 |
. . . . . . . . . . . . . 14
     ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)     |
38 | 37 | simpld 446 |
. . . . . . . . . . . . 13
    ![]_ ]_](_urbrack.gif)
   |
39 | 27, 38 | syl5 30 |
. . . . . . . . . . . 12
    ![]_ ]_](_urbrack.gif)
   |
40 | 39 | imp 419 |
. . . . . . . . . . 11
 

  ![]_ ]_](_urbrack.gif)   |
41 | 40 | recnd 9078 |
. . . . . . . . . 10
 

  ![]_ ]_](_urbrack.gif)   |
42 | 26, 41 | mulcld 9072 |
. . . . . . . . 9
 

           ![]_ ]_](_urbrack.gif)    |
43 | 17, 42 | sylan2 461 |
. . . . . . . 8
 
 ..^               ![]_ ]_](_urbrack.gif)    |
44 | 2, 13, 15, 43 | fsumsplit 12496 |
. . . . . . 7
   ..^               ![]_ ]_](_urbrack.gif)     ..^               ![]_ ]_](_urbrack.gif)      ..^               ![]_ ]_](_urbrack.gif)     |
45 | | eluzelz 10460 |
. . . . . . . . 9
    
  |
46 | | fzval3 11143 |
. . . . . . . . 9
      ..^     |
47 | 7, 45, 46 | 3syl 19 |
. . . . . . . 8
      ..^     |
48 | 47 | sumeq1d 12458 |
. . . . . . 7
                  ![]_ ]_](_urbrack.gif)    ..^               ![]_ ]_](_urbrack.gif)    |
49 | 3 | nnzd 10338 |
. . . . . . . . . 10
   |
50 | | fzval3 11143 |
. . . . . . . . . 10
      ..^     |
51 | 49, 50 | syl 16 |
. . . . . . . . 9
      ..^     |
52 | 51 | sumeq1d 12458 |
. . . . . . . 8
                  ![]_ ]_](_urbrack.gif)    ..^               ![]_ ]_](_urbrack.gif)    |
53 | 52 | oveq1d 6063 |
. . . . . . 7
                   ![]_ ]_](_urbrack.gif)      ..^               ![]_ ]_](_urbrack.gif)    
 ..^               ![]_ ]_](_urbrack.gif)      ..^               ![]_ ]_](_urbrack.gif)     |
54 | 44, 48, 53 | 3eqtr4d 2454 |
. . . . . 6
                  ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)  
   ..^               ![]_ ]_](_urbrack.gif)     |
55 | | elfznn 11044 |
. . . . . . . 8
       |
56 | | simpr 448 |
. . . . . . . . 9
 

  |
57 | | nfcv 2548 |
. . . . . . . . . 10
   |
58 | | nfcv 2548 |
. . . . . . . . . . 11
           |
59 | | nfcv 2548 |
. . . . . . . . . . 11
  |
60 | | nfcsb1v 3251 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
61 | 58, 59, 60 | nfov 6071 |
. . . . . . . . . 10
             ![]_ ]_](_urbrack.gif)   |
62 | | fveq2 5695 |
. . . . . . . . . . . 12
           |
63 | 62 | fveq2d 5699 |
. . . . . . . . . . 11
                   |
64 | | csbeq1a 3227 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
65 | 63, 64 | oveq12d 6066 |
. . . . . . . . . 10
                      ![]_ ]_](_urbrack.gif)    |
66 | 57, 61, 65, 36 | fvmptf 5788 |
. . . . . . . . 9
             ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)    |
67 | 56, 42, 66 | syl2anc 643 |
. . . . . . . 8
 

               ![]_ ]_](_urbrack.gif)    |
68 | 55, 67 | sylan2 461 |
. . . . . . 7
 
                    ![]_ ]_](_urbrack.gif)    |
69 | 3, 5 | syl6eleq 2502 |
. . . . . . . 8
       |
70 | | uztrn 10466 |
. . . . . . . 8
          
      |
71 | 7, 69, 70 | syl2anc 643 |
. . . . . . 7
       |
72 | 55, 42 | sylan2 461 |
. . . . . . 7
 
                ![]_ ]_](_urbrack.gif)    |
73 | 68, 71, 72 | fsumser 12487 |
. . . . . 6
                  ![]_ ]_](_urbrack.gif)         |
74 | 54, 73 | eqtr3d 2446 |
. . . . 5
                   ![]_ ]_](_urbrack.gif)      ..^               ![]_ ]_](_urbrack.gif)          |
75 | | elfznn 11044 |
. . . . . . 7
       |
76 | 75, 67 | sylan2 461 |
. . . . . 6
 
                    ![]_ ]_](_urbrack.gif)    |
77 | 75, 42 | sylan2 461 |
. . . . . 6
 
                ![]_ ]_](_urbrack.gif)    |
78 | 76, 69, 77 | fsumser 12487 |
. . . . 5
                  ![]_ ]_](_urbrack.gif)         |
79 | 74, 78 | oveq12d 6066 |
. . . 4
                    ![]_ ]_](_urbrack.gif)  
   ..^               ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)                 |
80 | | fzfid 11275 |
. . . . . 6
       |
81 | 80, 77 | fsumcl 12490 |
. . . . 5
                  ![]_ ]_](_urbrack.gif)    |
82 | | fzofi 11276 |
. . . . . . 7
   ..^    |
83 | 82 | a1i 11 |
. . . . . 6
    ..^     |
84 | | ssun2 3479 |
. . . . . . . . 9
   ..^     ..^      ..^     |
85 | 84, 13 | syl5sseqr 3365 |
. . . . . . . 8
    ..^    ..^     |
86 | 85 | sselda 3316 |
. . . . . . 7
 
   ..^   
 ..^     |
87 | 86, 43 | syldan 457 |
. . . . . 6
 
   ..^   
           ![]_ ]_](_urbrack.gif)    |
88 | 83, 87 | fsumcl 12490 |
. . . . 5
     ..^               ![]_ ]_](_urbrack.gif)    |
89 | 81, 88 | pncan2d 9377 |
. . . 4
                    ![]_ ]_](_urbrack.gif)  
   ..^               ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)       ..^               ![]_ ]_](_urbrack.gif)    |
90 | 79, 89 | eqtr3d 2446 |
. . 3
      
          ..^               ![]_ ]_](_urbrack.gif)    |
91 | 90 | fveq2d 5699 |
. 2
    
               
   ..^               ![]_ ]_](_urbrack.gif)     |
92 | 88 | abscld 12201 |
. . 3
    
   ..^               ![]_ ]_](_urbrack.gif)     |
93 | | 2re 10033 |
. . . . . 6
 |
94 | 93 | a1i 11 |
. . . . 5
   |
95 | | dchrisum.9 |
. . . . 5
   |
96 | 94, 95 | remulcld 9080 |
. . . 4
     |
97 | 40 | ralrimiva 2757 |
. . . . 5
    ![]_ ]_](_urbrack.gif)
  |
98 | | csbeq1 3222 |
. . . . . . 7
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
99 | 98 | eleq1d 2478 |
. . . . . 6
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
100 | 99 | rspcv 3016 |
. . . . 5
    
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
101 | 4, 97, 100 | sylc 58 |
. . . 4
     ![]_ ]_](_urbrack.gif)
  |
102 | 96, 101 | remulcld 9080 |
. . 3
     
  ![]_ ]_](_urbrack.gif)    |
103 | | dchrisumlem2.1 |
. . . . 5
   |
104 | 33 | ralrimiva 2757 |
. . . . 5
    |
105 | | nfcsb1v 3251 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)  |
106 | 105 | nfel1 2558 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)
 |
107 | | csbeq1a 3227 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   |
108 | 107 | eleq1d 2478 |
. . . . . 6
 
  ![]_ ]_](_urbrack.gif)    |
109 | 106, 108 | rspc 3014 |
. . . . 5

 
  ![]_ ]_](_urbrack.gif)    |
110 | 103, 104,
109 | sylc 58 |
. . . 4
   ![]_ ]_](_urbrack.gif)
  |
111 | 96, 110 | remulcld 9080 |
. . 3
      ![]_ ]_](_urbrack.gif)    |
112 | 71, 5 | syl6eleqr 2503 |
. . . . . . . . . . . 12
   |
113 | 112 | peano2nnd 9981 |
. . . . . . . . . . 11
     |
114 | 113 | nnrpd 10611 |
. . . . . . . . . 10
     |
115 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 21143 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)
        
  ![]_ ]_](_urbrack.gif)     |
116 | 115 | simpld 446 |
. . . . . . . . . 10
        ![]_ ]_](_urbrack.gif)
   |
117 | 114, 116 | mpd 15 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)
  |
118 | 117 | recnd 9078 |
. . . . . . . 8
     ![]_ ]_](_urbrack.gif)
  |
119 | | fzofi 11276 |
. . . . . . . . . 10
 ..^    |
120 | 119 | a1i 11 |
. . . . . . . . 9
  ..^     |
121 | | elfzoelz 11103 |
. . . . . . . . . 10
  ..^  
  |
122 | 22 | adantr 452 |
. . . . . . . . . . 11
 

  |
123 | | simpr 448 |
. . . . . . . . . . 11
 

  |
124 | 18, 19, 20, 21, 122, 123 | dchrzrhcl 20990 |
. . . . . . . . . 10
 

          |
125 | 121, 124 | sylan2 461 |
. . . . . . . . 9
 
 ..^              |
126 | 120, 125 | fsumcl 12490 |
. . . . . . . 8
 
 ..^              |
127 | 118, 126 | mulcld 9072 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)   ..^               |
128 | 101 | recnd 9078 |
. . . . . . . 8
     ![]_ ]_](_urbrack.gif)
  |
129 | | fzofi 11276 |
. . . . . . . . . 10
 ..^    |
130 | 129 | a1i 11 |
. . . . . . . . 9
  ..^     |
131 | | elfzoelz 11103 |
. . . . . . . . . 10
  ..^  
  |
132 | 131, 124 | sylan2 461 |
. . . . . . . . 9
 
 ..^              |
133 | 130, 132 | fsumcl 12490 |
. . . . . . . 8
 
 ..^              |
134 | 128, 133 | mulcld 9072 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)   ..^               |
135 | 127, 134 | subcld 9375 |
. . . . . 6
    
  ![]_ ]_](_urbrack.gif)   ..^               
  ![]_ ]_](_urbrack.gif)
  ..^                |
136 | 135 | abscld 12201 |
. . . . 5
          ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                 |
137 | 86, 17 | syl 16 |
. . . . . . . 8
 
   ..^   
  |
138 | | peano2nn 9976 |
. . . . . . . . . . . . 13
     |
139 | 138 | nnrpd 10611 |
. . . . . . . . . . . 12
     |
140 | | nfcsb1v 3251 |
. . . . . . . . . . . . . . 15
      ![]_ ]_](_urbrack.gif)  |
141 | 140 | nfel1 2558 |
. . . . . . . . . . . . . 14
      ![]_ ]_](_urbrack.gif)
 |
142 | | csbeq1a 3227 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)   |
143 | 142 | eleq1d 2478 |
. . . . . . . . . . . . . 14
   
    ![]_ ]_](_urbrack.gif)    |
144 | 141, 143 | rspc 3014 |
. . . . . . . . . . . . 13
  
 
    ![]_ ]_](_urbrack.gif)    |
145 | 144 | impcom 420 |
. . . . . . . . . . . 12
          ![]_ ]_](_urbrack.gif)   |
146 | 104, 139,
145 | syl2an 464 |
. . . . . . . . . . 11
 

    ![]_ ]_](_urbrack.gif)   |
147 | 146, 40 | resubcld 9429 |
. . . . . . . . . 10
 

     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
148 | 147 | recnd 9078 |
. . . . . . . . 9
 

     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
149 | | fzofi 11276 |
. . . . . . . . . . . 12
 ..^    |
150 | 149 | a1i 11 |
. . . . . . . . . . 11
  ..^     |
151 | | elfzoelz 11103 |
. . . . . . . . . . . 12
  ..^  
  |
152 | 151, 124 | sylan2 461 |
. . . . . . . . . . 11
 
 ..^              |
153 | 150, 152 | fsumcl 12490 |
. . . . . . . . . 10
 
 ..^              |
154 | 153 | adantr 452 |
. . . . . . . . 9
 

  ..^              |
155 | 148, 154 | mulcld 9072 |
. . . . . . . 8
 

      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^               |
156 | 137, 155 | syldan 457 |
. . . . . . 7
 
   ..^   
      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  
 ..^               |
157 | 83, 156 | fsumcl 12490 |
. . . . . 6
     ..^          ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ..^               |
158 | 157 | abscld 12201 |
. . . . 5
    
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                |
159 | 136, 158 | readdcld 9079 |
. . . 4
           ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                 |
160 | 26, 41 | mulcomd 9073 |
. . . . . . . . . 10
 

           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)            |
161 | | nnnn0 10192 |
. . . . . . . . . . . . . . . 16
   |
162 | 161 | adantl 453 |
. . . . . . . . . . . . . . 15
 

  |
163 | | nn0uz 10484 |
. . . . . . . . . . . . . . 15
     |
164 | 162, 163 | syl6eleq 2502 |
. . . . . . . . . . . . . 14
 

      |
165 | | elfzelz 11023 |
. . . . . . . . . . . . . . 15
       |
166 | 124 | adantlr 696 |
. . . . . . . . . . . . . . 15
               |
167 | 165, 166 | sylan2 461 |
. . . . . . . . . . . . . 14
                   |
168 | 164, 167,
63 | fzosump1 12501 |
. . . . . . . . . . . . 13
 

  ..^               ..^                     |
169 | 168 | oveq1d 6063 |
. . . . . . . . . . . 12
 

   ..^              ..^               ..^                     ..^             |
170 | | fzofi 11276 |
. . . . . . . . . . . . . . 15
 ..^  |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
 

 ..^   |
172 | | elfzoelz 11103 |
. . . . . . . . . . . . . . 15
  ..^
  |
173 | 172, 166 | sylan2 461 |
. . . . . . . . . . . . . 14
     ..^ 
          |
174 | 171, 173 | fsumcl 12490 |
. . . . . . . . . . . . 13
 

  ..^            |
175 | 174, 26 | pncan2d 9377 |
. . . . . . . . . . . 12
 

  
 ..^                     ..^                     |
176 | 169, 175 | eqtr2d 2445 |
. . . . . . . . . . 11
 

           ..^              ..^             |
177 | 176 | oveq2d 6064 |
. . . . . . . . . 10
 

   ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)
   ..^              ..^              |
178 | 160, 177 | eqtrd 2444 |
. . . . . . . . 9
 

           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    ..^              ..^              |
179 | 137, 178 | syldan 457 |
. . . . . . . 8
 
   ..^   
           ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
   ..^              ..^              |
180 | 179 | sumeq2dv 12460 |
. . . . . . 7
     ..^               ![]_ ]_](_urbrack.gif)      ..^       ![]_ ]_](_urbrack.gif)
   ..^              ..^              |
181 | | csbeq1 3222 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
182 | | oveq2 6056 |
. . . . . . . . . 10
  ..^  ..^   |
183 | 182 | sumeq1d 12458 |
. . . . . . . . 9
   ..^            ..^            |
184 | 181, 183 | jca 519 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ..^          
 ..^             |
185 | | csbeq1 3222 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
186 | | oveq2 6056 |
. . . . . . . . . 10
    ..^  ..^     |
187 | 186 | sumeq1d 12458 |
. . . . . . . . 9
     ..^            ..^              |
188 | 185, 187 | jca 519 |
. . . . . . . 8
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)   ..^            ..^               |
189 | | csbeq1 3222 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
190 | | oveq2 6056 |
. . . . . . . . . 10
    ..^  ..^     |
191 | 190 | sumeq1d 12458 |
. . . . . . . . 9
     ..^            ..^              |
192 | 189, 191 | jca 519 |
. . . . . . . 8
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)   ..^            ..^               |
193 | | csbeq1 3222 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
194 | | oveq2 6056 |
. . . . . . . . . 10
    ..^  ..^     |
195 | 194 | sumeq1d 12458 |
. . . . . . . . 9
     ..^            ..^              |
196 | 193, 195 | jca 519 |
. . . . . . . 8
    
 ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)   ..^            ..^               |
197 | | elfzuz 11019 |
. . . . . . . . . 10
                 |
198 | 5 | uztrn2 10467 |
. . . . . . . . . 10
   
   
     |
199 | 4, 197, 198 | syl2an 464 |
. . . . . . . . 9
 
     
     |
200 | 41 | ralrimiva 2757 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
  |
201 | | csbeq1 3222 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
202 | 201 | eleq1d 2478 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
203 | 202 | rspccva 3019 |
. . . . . . . . . 10
     ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)   |
204 | 200, 203 | sylan 458 |
. . . . . . . . 9
 

  ![]_ ]_](_urbrack.gif)   |
205 | 199, 204 | syldan 457 |
. . . . . . . 8
 
     
     ![]_ ]_](_urbrack.gif)   |
206 | | fzofi 11276 |
. . . . . . . . . . 11
 ..^  |
207 | 206 | a1i 11 |
. . . . . . . . . 10
  ..^   |
208 | | elfzoelz 11103 |
. . . . . . . . . . 11
  ..^
  |
209 | 208, 124 | sylan2 461 |
. . . . . . . . . 10
 
 ..^            |
210 | 207, 209 | fsumcl 12490 |
. . . . . . . . 9
 
 ..^            |
211 | 210 | adantr 452 |
. . . . . . . 8
 
     
     ..^            |
212 | 184, 188,
192, 196, 9, 205, 211 | fsumparts 12548 |
. . . . . . 7
     ..^       ![]_ ]_](_urbrack.gif)
   ..^              ..^                   ![]_ ]_](_urbrack.gif)   ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                |
213 | 180, 212 | eqtrd 2444 |
. . . . . 6
     ..^               ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                |
214 | 213 | fveq2d 5699 |
. . . . 5
    
   ..^               ![]_ ]_](_urbrack.gif)          
  ![]_ ]_](_urbrack.gif)   ..^               
  ![]_ ]_](_urbrack.gif)
  ..^                  ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                 |
215 | 135, 157 | abs2dif2d 12223 |
. . . . 5
        
  ![]_ ]_](_urbrack.gif)   ..^               
  ![]_ ]_](_urbrack.gif)
  ..^                  ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                         ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                 |
216 | 214, 215 | eqbrtrd 4200 |
. . . 4
    
   ..^               ![]_ ]_](_urbrack.gif)          
  ![]_ ]_](_urbrack.gif)   ..^               
  ![]_ ]_](_urbrack.gif)
  ..^                  
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                 |
217 | 117, 101 | readdcld 9079 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)    |
218 | 217, 95 | remulcld 9080 |
. . . . . 6
    
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
219 | 181, 185,
189, 193, 9, 205 | fsumtscopo 12544 |
. . . . . . . 8
     ..^       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
220 | 137, 40 | syldan 457 |
. . . . . . . . . 10
 
   ..^   
  ![]_ ]_](_urbrack.gif)   |
221 | 137, 146 | syldan 457 |
. . . . . . . . . 10
 
   ..^   
    ![]_ ]_](_urbrack.gif)   |
222 | 220, 221 | resubcld 9429 |
. . . . . . . . 9
 
   ..^   
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
223 | 83, 222 | fsumrecl 12491 |
. . . . . . . 8
     ..^       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
224 | 219, 223 | eqeltrrd 2487 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)    |
225 | 224, 95 | remulcld 9080 |
. . . . . 6
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
226 | 127 | abscld 12201 |
. . . . . . . 8
         ![]_ ]_](_urbrack.gif)
  ..^                |
227 | 134 | abscld 12201 |
. . . . . . . 8
         ![]_ ]_](_urbrack.gif)
  ..^                |
228 | 226, 227 | readdcld 9079 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)
  ..^                      ![]_ ]_](_urbrack.gif)
  ..^                 |
229 | 127, 134 | abs2dif2d 12223 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                        ![]_ ]_](_urbrack.gif)   ..^                      ![]_ ]_](_urbrack.gif)
  ..^                 |
230 | 117, 95 | remulcld 9080 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)    |
231 | 101, 95 | remulcld 9080 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)    |
232 | 118, 126 | absmuld 12219 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)
  ..^                   
  ![]_ ]_](_urbrack.gif)       ..^                |
233 | | eluzelre 10461 |
. . . . . . . . . . . . . . . . . . 19
    
  |
234 | 233 | adantl 453 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
235 | | eluzle 10462 |
. . . . . . . . . . . . . . . . . . 19
    
  |
236 | 235 | adantl 453 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
237 | 32 | nnred 9979 |
. . . . . . . . . . . . . . . . . . . 20
   |
238 | 237 | adantr 452 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
239 | | elicopnf 10964 |
. . . . . . . . . . . . . . . . . . 19
    
     |
240 | 238, 239 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
    
    
    |
241 | 234, 236,
240 | mpbir2and 889 |
. . . . . . . . . . . . . . . . 17
 
    
     |
242 | 241 | ex 424 |
. . . . . . . . . . . . . . . 16
            |
243 | 242 | ssrdv 3322 |
. . . . . . . . . . . . . . 15
          |
244 | 32 | nnzd 10338 |
. . . . . . . . . . . . . . . . 17
   |
245 | 49 | peano2zd 10342 |
. . . . . . . . . . . . . . . . 17
     |
246 | 103 | rpred 10612 |
. . . . . . . . . . . . . . . . . 18
   |
247 | 4 | nnred 9979 |
. . . . . . . . . . . . . . . . . 18
     |
248 | | dchrisumlem2.2 |
. . . . . . . . . . . . . . . . . 18

  |
249 | | dchrisumlem2.3 |
. . . . . . . . . . . . . . . . . 18

    |
250 | 237, 246,
247, 248, 249 | letrd 9191 |
. . . . . . . . . . . . . . . . 17

    |
251 | | eluz2 10458 |
. . . . . . . . . . . . . . . . 17
               |
252 | 244, 245,
250, 251 | syl3anbrc 1138 |
. . . . . . . . . . . . . . . 16
         |
253 | | uztrn 10466 |
. . . . . . . . . . . . . . . 16
       
         
       |
254 | 9, 252, 253 | syl2anc 643 |
. . . . . . . . . . . . . . 15
         |
255 | 243, 254 | sseldd 3317 |
. . . . . . . . . . . . . 14
        |
256 | 115 | simprd 450 |
. . . . . . . . . . . . . 14
      
    ![]_ ]_](_urbrack.gif)    |
257 | 255, 256 | mpd 15 |
. . . . . . . . . . . . 13

    ![]_ ]_](_urbrack.gif)   |
258 | 117, 257 | absidd 12188 |
. . . . . . . . . . . 12
     
  ![]_ ]_](_urbrack.gif)   
  ![]_ ]_](_urbrack.gif)   |
259 | 258 | oveq1d 6063 |
. . . . . . . . . . 11
      
  ![]_ ]_](_urbrack.gif)       ..^                   ![]_ ]_](_urbrack.gif)
     ..^                |
260 | 232, 259 | eqtrd 2444 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif)
  ..^                   ![]_ ]_](_urbrack.gif)      ..^                |
261 | 126 | abscld 12201 |
. . . . . . . . . . 11
      ..^               |
262 | 113 | nnnn0d 10238 |
. . . . . . . . . . . 12
     |
263 | | dchrisum.10 |
. . . . . . . . . . . . 13
   ..^       ..^             |
264 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 21144 |
. . . . . . . . . . . 12
 
        ..^            
  |
265 | 262, 264 | mpdan 650 |
. . . . . . . . . . 11
      ..^               |
266 | 261, 95, 117, 257, 265 | lemul2ad 9915 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)      ..^                   ![]_ ]_](_urbrack.gif)
   |
267 | 260, 266 | eqbrtrd 4200 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)
  ..^                   ![]_ ]_](_urbrack.gif)
   |
268 | 128, 133 | absmuld 12219 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)
  ..^                      ![]_ ]_](_urbrack.gif)       ..^                |
269 | 243, 252 | sseldd 3317 |
. . . . . . . . . . . . . 14
        |
270 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36 | dchrisumlema 21143 |
. . . . . . . . . . . . . . 15
         ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)     |
271 | 270 | simprd 450 |
. . . . . . . . . . . . . 14
      
    ![]_ ]_](_urbrack.gif)    |
272 | 269, 271 | mpd 15 |
. . . . . . . . . . . . 13

    ![]_ ]_](_urbrack.gif)   |
273 | 101, 272 | absidd 12188 |
. . . . . . . . . . . 12
        ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
274 | 273 | oveq1d 6063 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)       ..^                   ![]_ ]_](_urbrack.gif)
     ..^                |
275 | 268, 274 | eqtrd 2444 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif)
  ..^                   ![]_ ]_](_urbrack.gif)      ..^                |
276 | 133 | abscld 12201 |
. . . . . . . . . . 11
      ..^               |
277 | 4 | nnnn0d 10238 |
. . . . . . . . . . . 12
     |
278 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 21144 |
. . . . . . . . . . . 12
 
        ..^            
  |
279 | 277, 278 | mpdan 650 |
. . . . . . . . . . 11
      ..^               |
280 | 276, 95, 101, 272, 279 | lemul2ad 9915 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)      ..^                   ![]_ ]_](_urbrack.gif)
   |
281 | 275, 280 | eqbrtrd 4200 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)
  ..^                   ![]_ ]_](_urbrack.gif)
   |
282 | 226, 227,
230, 231, 267, 281 | le2addd 9608 |
. . . . . . . 8
          ![]_ ]_](_urbrack.gif)
  ..^                      ![]_ ]_](_urbrack.gif)
  ..^                  
  ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)     |
283 | 95 | recnd 9078 |
. . . . . . . . 9
   |
284 | 118, 128,
283 | adddird 9077 |
. . . . . . . 8
    
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
   
  ![]_ ]_](_urbrack.gif)
    |
285 | 282, 284 | breqtrrd 4206 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)
  ..^                      ![]_ ]_](_urbrack.gif)
  ..^                  
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
286 | 136, 228,
218, 229, 285 | letrd 9191 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
287 | 156 | abscld 12201 |
. . . . . . . 8
 
   ..^   
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ..^                |
288 | 83, 287 | fsumrecl 12491 |
. . . . . . 7
     ..^             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                |
289 | 83, 156 | fsumabs 12543 |
. . . . . . 7
    
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                  ..^             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                |
290 | 95 | adantr 452 |
. . . . . . . . . 10
 
   ..^   
  |
291 | 222, 290 | remulcld 9080 |
. . . . . . . . 9
 
   ..^   
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
292 | 137, 148 | syldan 457 |
. . . . . . . . . . . 12
 
   ..^   
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
293 | 153 | adantr 452 |
. . . . . . . . . . . 12
 
   ..^   
  ..^              |
294 | 292, 293 | absmuld 12219 |
. . . . . . . . . . 11
 
   ..^   
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ..^                       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ..^                |
295 | | elfzouz 11107 |
. . . . . . . . . . . . . . 15
    ..^  
        |
296 | | uztrn 10466 |
. . . . . . . . . . . . . . 15
     
               |
297 | 295, 252,
296 | syl2anr 465 |
. . . . . . . . . . . . . 14
 
   ..^   
      |
298 | 5 | uztrn2 10467 |
. . . . . . . . . . . . . . . . 17
 
       |
299 | 32, 298 | sylan 458 |
. . . . . . . . . . . . . . . 16
 
    
  |
300 | 299, 139 | syl 16 |
. . . . . . . . . . . . . . 15
 
    
    |
301 | 299 | nnrpd 10611 |
. . . . . . . . . . . . . . . 16
 
    
  |
302 | 34 | 3expia 1155 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
303 | 302 | ralrimivva 2766 |
. . . . . . . . . . . . . . . . 17
    
    |
304 | 303 | adantr 452 |
. . . . . . . . . . . . . . . 16
 
    
    
   |
305 | | nfcv 2548 |
. . . . . . . . . . . . . . . . . 18
   |
306 | | nfv 1626 |
. . . . . . . . . . . . . . . . . . 19
  
  |
307 | | nfcv 2548 |
. . . . . . . . . . . . . . . . . . . 20
   |
308 | | nfcv 2548 |
. . . . . . . . . . . . . . . . . . . 20
  |
309 | 307, 308,
60 | nfbr 4224 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)  |
310 | 306, 309 | nfim 1828 |
. . . . . . . . . . . . . . . . . 18
   

  ![]_ ]_](_urbrack.gif)   |
311 | 305, 310 | nfral 2727 |
. . . . . . . . . . . . . . . . 17
  
 
   ![]_ ]_](_urbrack.gif)   |
312 | | breq2 4184 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
313 | | breq1 4183 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
314 | 312, 313 | anbi12d 692 |
. . . . . . . . . . . . . . . . . . 19
  
 
    |
315 | 64 | breq2d 4192 |
. . . . . . . . . . . . . . . . . . 19
 
  ![]_ ]_](_urbrack.gif)    |
316 | 314, 315 | imbi12d 312 |
. . . . . . . . . . . . . . . . . 18
    
      ![]_ ]_](_urbrack.gif)     |
317 | 316 | ralbidv 2694 |
. . . . . . . . . . . . . . . . 17
  
 
    

  ![]_ ]_](_urbrack.gif)     |
318 | 311, 317 | rspc 3014 |
. . . . . . . . . . . . . . . 16

 
           ![]_ ]_](_urbrack.gif)     |
319 | 301, 304,
318 | sylc 58 |
. . . . . . . . . . . . . . 15
 
    
      ![]_ ]_](_urbrack.gif)    |
320 | 234 | lep1d 9906 |
. . . . . . . . . . . . . . . 16
 
    
    |
321 | 236, 320 | jca 519 |
. . . . . . . . . . . . . . 15
 
    
      |
322 | | breq2 4184 |
. . . . . . . . . . . . . . . . . 18
   
     |
323 | 322 | anbi2d 685 |
. . . . . . . . . . . . . . . . 17
    
 
      |
324 | | ovex 6073 |
. . . . . . . . . . . . . . . . . . . . 21
   |
325 | 324 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
       |
326 | | eqtr3 2431 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
327 | 31 | equcoms 1689 |
. . . . . . . . . . . . . . . . . . . . 21
   |
328 | 326, 327 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
329 | 325, 328 | csbied 3261 |
. . . . . . . . . . . . . . . . . . 19
       ![]_ ]_](_urbrack.gif)   |
330 | 329 | eqcomd 2417 |
. . . . . . . . . . . . . . . . . 18
       ![]_ ]_](_urbrack.gif)   |
331 | 330 | breq1d 4190 |
. . . . . . . . . . . . . . . . 17
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
332 | 323, 331 | imbi12d 312 |
. . . . . . . . . . . . . . . 16
     

  ![]_ ]_](_urbrack.gif) 
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
333 | 332 | rspcv 3016 |
. . . . . . . . . . . . . . 15
  
 
 
   ![]_ ]_](_urbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
334 | 300, 319,
321, 333 | syl3c 59 |
. . . . . . . . . . . . . 14
 
    
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
335 | 297, 334 | syldan 457 |
. . . . . . . . . . . . 13
 
   ..^   
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
336 | 221, 220,
335 | abssuble0d 12198 |
. . . . . . . . . . . 12
 
   ..^   
        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
337 | 336 | oveq1d 6063 |
. . . . . . . . . . 11
 
   ..^   
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)        ..^                  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       ..^                |
338 | 294, 337 | eqtrd 2444 |
. . . . . . . . . 10
 
   ..^   
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ..^                  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       ..^                |
339 | 293 | abscld 12201 |
. . . . . . . . . . 11
 
   ..^   
   
 ..^               |
340 | 220, 221 | subge0d 9580 |
. . . . . . . . . . . 12
 
   ..^   
    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
341 | 335, 340 | mpbird 224 |
. . . . . . . . . . 11
 
   ..^   
   ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
342 | 137 | peano2nnd 9981 |
. . . . . . . . . . . . 13
 
   ..^   
    |
343 | 342 | nnnn0d 10238 |
. . . . . . . . . . . 12
 
   ..^   
    |
344 | 19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263 | dchrisumlem1 21144 |
. . . . . . . . . . . 12
 
        ..^            
  |
345 | 343, 344 | syldan 457 |
. . . . . . . . . . 11
 
   ..^   
   
 ..^            
  |
346 | 339, 290,
222, 341, 345 | lemul2ad 9915 |
. . . . . . . . . 10
 
   ..^   
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)       ..^                  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
347 | 338, 346 | eqbrtrd 4200 |
. . . . . . . . 9
 
   ..^   
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ..^                  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
348 | 83, 287, 291, 347 | fsumle 12541 |
. . . . . . . 8
     ..^             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                  ..^        ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
349 | 222 | recnd 9078 |
. . . . . . . . . 10
 
   ..^   
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
350 | 83, 283, 349 | fsummulc1 12531 |
. . . . . . . . 9
      ..^       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)       ..^        ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     |
351 | 219 | oveq1d 6063 |
. . . . . . . . 9
      ..^       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)     |
352 | 350, 351 | eqtr3d 2446 |
. . . . . . . 8
     ..^        ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)     |
353 | 348, 352 | breqtrd 4204 |
. . . . . . 7
     ..^             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                    ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)     |
354 | 158, 288,
225, 289, 353 | letrd 9191 |
. . . . . 6
    
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                    ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)     |
355 | 136, 158,
218, 225, 286, 354 | le2addd 9608 |
. . . . 5
           ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                   
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)      |
356 | 128 | 2timesd 10174 |
. . . . . . . 8
   
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
357 | 128, 118,
128 | ppncand 9415 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
358 | 128, 118 | addcomd 9232 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
359 | 358 | oveq1d 6063 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)     |
360 | 356, 357,
359 | 3eqtr2d 2450 |
. . . . . . 7
   
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)     |
361 | 360 | oveq1d 6063 |
. . . . . 6
       ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)      |
362 | | 2cn 10034 |
. . . . . . . 8
 |
363 | 362 | a1i 11 |
. . . . . . 7
   |
364 | 363, 128,
283 | mul32d 9240 |
. . . . . 6
       ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
365 | 217 | recnd 9078 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)    |
366 | 224 | recnd 9078 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)    |
367 | 365, 366,
283 | adddird 9077 |
. . . . . 6
     
  ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)        
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)      |
368 | 361, 364,
367 | 3eqtr3d 2452 |
. . . . 5
     
  ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
 
  ![]_ ]_](_urbrack.gif)      |
369 | 355, 368 | breqtrrd 4206 |
. . . 4
           ![]_ ]_](_urbrack.gif)
  ..^                  ![]_ ]_](_urbrack.gif)
  ..^                  
   ..^          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    ..^                   
  ![]_ ]_](_urbrack.gif)    |
370 | 92, 159, 102, 216, 369 | letrd 9191 |
. . 3
    
   ..^               ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
371 | | 2nn0 10202 |
. . . . . 6
 |
372 | | nn0ge0 10211 |
. . . . . 6

  |
373 | 371, 372 | mp1i 12 |
. . . . 5

  |
374 | | 0re 9055 |
. . . . . . 7
 |
375 | 374 | a1i 11 |
. . . . . 6
   |
376 | 126 | absge0d 12209 |
. . . . . 6

   
 ..^               |
377 | 375, 261,
95, 376, 265 | letrd 9191 |
. . . . 5

  |
378 | 94, 95, 373, 377 | mulge0d 9567 |
. . . 4

    |
379 | 4 | nnrpd 10611 |
. . . . 5
     |
380 | | nfv 1626 |
. . . . . . . . 9
  
  |
381 | 307, 308,
105 | nfbr 4224 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)  |
382 | 380, 381 | nfim 1828 |
. . . . . . . 8
    
  ![]_ ]_](_urbrack.gif)   |
383 | 305, 382 | nfral 2727 |
. . . . . . 7
  
 
   ![]_ ]_](_urbrack.gif)   |
384 | | breq2 4184 |
. . . . . . . . . 10
 
   |
385 | | breq1 4183 |
. . . . . . . . . 10
 
   |
386 | 384, 385 | anbi12d 692 |
. . . . . . . . 9
  
 
    |
387 | 107 | breq2d 4192 |
. . . . . . . . 9
 
  ![]_ ]_](_urbrack.gif)    |
388 | 386, 387 | imbi12d 312 |
. . . . . . . 8
    
      ![]_ ]_](_urbrack.gif)     |
389 | 388 | ralbidv 2694 |
. . . . . . 7
  
 
     
  ![]_ ]_](_urbrack.gif)     |
390 | 383, 389 | rspc 3014 |
. . . . . 6

 
           ![]_ ]_](_urbrack.gif)     |
391 | 103, 303,
390 | sylc 58 |
. . . . 5
    
  ![]_ ]_](_urbrack.gif)    |
392 | 248, 249 | jca 519 |
. . . . 5
 
     |
393 | | breq2 4184 |
. . . . . . . 8
   
     |
394 | 393 | anbi2d 685 |
. . . . . . 7
    
 
      |
395 | | ovex 6073 |
. . . . . . . . . . 11
   |
396 | 395 | a1i 11 |
. . . . . . . . . 10
       |
397 | | eqtr3 2431 |
. . . . . . . . . . 11
   
     |
398 | 397, 327 | syl 16 |
. . . . . . . . . 10
   
     |
399 | 396, 398 | csbied 3261 |
. . . . . . . . 9
       ![]_ ]_](_urbrack.gif)   |
400 | 399 | eqcomd 2417 |
. . . . . . . 8
       ![]_ ]_](_urbrack.gif)   |
401 | 400 | breq1d 4190 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
402 | 394, 401 | imbi12d 312 |
. . . . . 6
      
  ![]_ ]_](_urbrack.gif) 
         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
403 | 402 | rspcv 3016 |
. . . . 5
  
 
 
   ![]_ ]_](_urbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
404 | 379, 391,
392, 403 | syl3c 59 |
. . . 4
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
405 | 101, 110,
96, 378, 404 | lemul2ad 9915 |
. . 3
     
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
406 | 92, 102, 111, 370, 405 | letrd 9191 |
. 2
    
   ..^               ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    |
407 | 91, 406 | eqbrtrd 4200 |
1
    
                 ![]_ ]_](_urbrack.gif)    |