Step | Hyp | Ref
| Expression |
1 | | fzofi 12225 |
. . . . . 6
 ..^  |
2 | 1 | a1i 11 |
. . . . 5
  ..^   |
3 | | dvfsumabs.x |
. . . . 5
 
 ..^    |
4 | | dvfsumabs.m |
. . . . . . . . . . . . 13
       |
5 | | eluzel2 11187 |
. . . . . . . . . . . . 13
    
  |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
   |
7 | | eluzelz 11192 |
. . . . . . . . . . . . 13
    
  |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
   |
9 | | fzval2 11813 |
. . . . . . . . . . . 12
 
        ![[,] [,]](_icc.gif)     |
10 | 6, 8, 9 | syl2anc 673 |
. . . . . . . . . . 11
        ![[,] [,]](_icc.gif)     |
11 | | inss1 3643 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)   |
12 | 10, 11 | syl6eqss 3468 |
. . . . . . . . . 10
    
  ![[,] [,]](_icc.gif)    |
13 | 12 | sselda 3418 |
. . . . . . . . 9
 
    
  ![[,] [,]](_icc.gif)    |
14 | | dvfsumabs.a |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
15 | | cncff 22003 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
17 | | eqid 2471 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
18 | 17 | fmpt 6058 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      |
19 | 16, 18 | sylibr 217 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)     |
20 | | nfcsb1v 3365 |
. . . . . . . . . . . 12
  
 ![]_ ]_](_urbrack.gif)  |
21 | 20 | nfel1 2626 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)
 |
22 | | csbeq1a 3358 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)   |
23 | 22 | eleq1d 2533 |
. . . . . . . . . . 11
 
  ![]_ ]_](_urbrack.gif)    |
24 | 21, 23 | rspc 3130 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)    |
25 | 19, 24 | mpan9 477 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
  ![]_ ]_](_urbrack.gif)   |
26 | 13, 25 | syldan 478 |
. . . . . . . 8
 
    
  ![]_ ]_](_urbrack.gif)   |
27 | 26 | ralrimiva 2809 |
. . . . . . 7
         ![]_ ]_](_urbrack.gif)
  |
28 | | fzofzp1 12037 |
. . . . . . 7
  ..^
        |
29 | | csbeq1 3352 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
30 | 29 | eleq1d 2533 |
. . . . . . . 8
    
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)
   |
31 | 30 | rspccva 3135 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)
  |
32 | 27, 28, 31 | syl2an 485 |
. . . . . 6
 
 ..^      ![]_ ]_](_urbrack.gif)
  |
33 | | elfzofz 11962 |
. . . . . . 7
  ..^
      |
34 | | csbeq1 3352 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
35 | 34 | eleq1d 2533 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
   |
36 | 35 | rspccva 3135 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)
  |
37 | 27, 33, 36 | syl2an 485 |
. . . . . 6
 
 ..^    ![]_ ]_](_urbrack.gif)
  |
38 | 32, 37 | subcld 10005 |
. . . . 5
 
 ..^       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
39 | 2, 3, 38 | fsumsub 13926 |
. . . 4
   ..^        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ..^    ..^       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
40 | | vex 3034 |
. . . . . . . 8
 |
41 | 40 | a1i 11 |
. . . . . . 7
   |
42 | | eqeq2 2482 |
. . . . . . . . 9
 
   |
43 | 42 | biimpa 492 |
. . . . . . . 8
 
   |
44 | | dvfsumabs.c |
. . . . . . . 8
   |
45 | 43, 44 | syl 17 |
. . . . . . 7
 
   |
46 | 41, 45 | csbied 3376 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)   |
47 | 40 | a1i 11 |
. . . . . . 7
   |
48 | | eqeq2 2482 |
. . . . . . . . 9
 
   |
49 | 48 | biimpa 492 |
. . . . . . . 8
 
   |
50 | | dvfsumabs.d |
. . . . . . . 8
   |
51 | 49, 50 | syl 17 |
. . . . . . 7
 
   |
52 | 47, 51 | csbied 3376 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)   |
53 | 34, 29, 46, 52, 4, 26 | telfsumo2 13940 |
. . . . 5
   ..^       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
54 | 53 | oveq2d 6324 |
. . . 4
    ..^    ..^       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    
 ..^  
    |
55 | 39, 54 | eqtrd 2505 |
. . 3
   ..^        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ..^       |
56 | 55 | fveq2d 5883 |
. 2
    
 ..^        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)          ..^  
     |
57 | 3, 38 | subcld 10005 |
. . . . 5
 
 ..^        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
58 | 2, 57 | fsumcl 13876 |
. . . 4
   ..^        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
59 | 58 | abscld 13575 |
. . 3
    
 ..^        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
60 | 57 | abscld 13575 |
. . . 4
 
 ..^     
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
61 | 2, 60 | fsumrecl 13877 |
. . 3
   ..^           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
62 | | dvfsumabs.y |
. . . 4
 
 ..^    |
63 | 2, 62 | fsumrecl 13877 |
. . 3
   ..^    |
64 | 2, 57 | fsumabs 13938 |
. . 3
    
 ..^        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ..^           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
65 | | elfzoelz 11947 |
. . . . . . . . . 10
  ..^
  |
66 | 65 | adantl 473 |
. . . . . . . . 9
 
 ..^    |
67 | 66 | zred 11063 |
. . . . . . . 8
 
 ..^    |
68 | 67 | rexrd 9708 |
. . . . . . 7
 
 ..^    |
69 | | peano2re 9824 |
. . . . . . . . 9
     |
70 | 67, 69 | syl 17 |
. . . . . . . 8
 
 ..^      |
71 | 70 | rexrd 9708 |
. . . . . . 7
 
 ..^      |
72 | 67 | lep1d 10560 |
. . . . . . 7
 
 ..^      |
73 | | ubicc2 11775 |
. . . . . . 7
   
       ![[,] [,]](_icc.gif)      |
74 | 68, 71, 72, 73 | syl3anc 1292 |
. . . . . 6
 
 ..^      ![[,] [,]](_icc.gif)      |
75 | | lbicc2 11774 |
. . . . . . 7
   
     ![[,] [,]](_icc.gif)      |
76 | 68, 71, 72, 75 | syl3anc 1292 |
. . . . . 6
 
 ..^    ![[,] [,]](_icc.gif)      |
77 | 6 | zred 11063 |
. . . . . . . . . . . 12
   |
78 | 77 | adantr 472 |
. . . . . . . . . . 11
 
 ..^    |
79 | 8 | zred 11063 |
. . . . . . . . . . . 12
   |
80 | 79 | adantr 472 |
. . . . . . . . . . 11
 
 ..^    |
81 | | elfzole1 11955 |
. . . . . . . . . . . 12
  ..^
  |
82 | 81 | adantl 473 |
. . . . . . . . . . 11
 
 ..^    |
83 | 28 | adantl 473 |
. . . . . . . . . . . 12
 
 ..^          |
84 | | elfzle2 11829 |
. . . . . . . . . . . 12
           |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
 
 ..^      |
86 | | iccss 11727 |
. . . . . . . . . . 11
    
      ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
87 | 78, 80, 82, 85, 86 | syl22anc 1293 |
. . . . . . . . . 10
 
 ..^    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
88 | 87 | resmptd 5162 |
. . . . . . . . 9
 
 ..^      ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)           |
89 | | eqid 2471 |
. . . . . . . . . . 11
  ℂfld   ℂfld |
90 | 89 | subcn 21976 |
. . . . . . . . . . . 12
    ℂfld   ℂfld   ℂfld  |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
 
 ..^      ℂfld
  ℂfld   ℂfld   |
92 | | iccssre 11741 |
. . . . . . . . . . . . . . . 16
 
   ![[,] [,]](_icc.gif) 
  |
93 | 77, 79, 92 | syl2anc 673 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif) 
  |
94 | 93 | adantr 472 |
. . . . . . . . . . . . . 14
 
 ..^    ![[,] [,]](_icc.gif)    |
95 | | ax-resscn 9614 |
. . . . . . . . . . . . . 14
 |
96 | 94, 95 | syl6ss 3430 |
. . . . . . . . . . . . 13
 
 ..^    ![[,] [,]](_icc.gif)    |
97 | | ssid 3437 |
. . . . . . . . . . . . . 14
 |
98 | 97 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^    |
99 | | cncfmptc 22021 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 

   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
100 | 3, 96, 98, 99 | syl3anc 1292 |
. . . . . . . . . . . 12
 
 ..^     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
101 | | cncfmptid 22022 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
102 | 96, 97, 101 | sylancl 675 |
. . . . . . . . . . . 12
 
 ..^     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
103 | 100, 102 | mulcncf 22476 |
. . . . . . . . . . 11
 
 ..^     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
104 | 14 | adantr 472 |
. . . . . . . . . . 11
 
 ..^     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
105 | 89, 91, 103, 104 | cncfmpt2f 22024 |
. . . . . . . . . 10
 
 ..^     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
106 | | rescncf 22007 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          |
107 | 87, 105, 106 | sylc 61 |
. . . . . . . . 9
 
 ..^      ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)         |
108 | 88, 107 | eqeltrrd 2550 |
. . . . . . . 8
 
 ..^     ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
109 | 95 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^    |
110 | 87, 94 | sstrd 3428 |
. . . . . . . . . . . 12
 
 ..^    ![[,] [,]](_icc.gif)      |
111 | 87 | sselda 3418 |
. . . . . . . . . . . . 13
    ..^    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
112 | 3 | adantr 472 |
. . . . . . . . . . . . . . 15
    ..^    ![[,] [,]](_icc.gif)     |
113 | 96 | sselda 3418 |
. . . . . . . . . . . . . . 15
    ..^    ![[,] [,]](_icc.gif)     |
114 | 112, 113 | mulcld 9681 |
. . . . . . . . . . . . . 14
    ..^    ![[,] [,]](_icc.gif)   
   |
115 | 19 | r19.21bi 2776 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)  
  |
116 | 115 | adantlr 729 |
. . . . . . . . . . . . . 14
    ..^    ![[,] [,]](_icc.gif)     |
117 | 114, 116 | subcld 10005 |
. . . . . . . . . . . . 13
    ..^    ![[,] [,]](_icc.gif)         |
118 | 111, 117 | syldan 478 |
. . . . . . . . . . . 12
    ..^    ![[,] [,]](_icc.gif)           |
119 | 89 | tgioo2 21899 |
. . . . . . . . . . . 12
       ℂfld
↾t   |
120 | | iccntr 21917 |
. . . . . . . . . . . . 13
                  ![[,] [,]](_icc.gif)             |
121 | 67, 70, 120 | syl2anc 673 |
. . . . . . . . . . . 12
 
 ..^               ![[,] [,]](_icc.gif)             |
122 | 109, 110,
118, 119, 89, 121 | dvmptntr 23004 |
. . . . . . . . . . 11
 
 ..^   
  ![[,] [,]](_icc.gif)                          |
123 | | reelprrecn 9649 |
. . . . . . . . . . . . 13
    |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^   
   |
125 | | ioossicc 11745 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif)   |
126 | 125 | sseli 3414 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)    |
127 | 126, 117 | sylan2 482 |
. . . . . . . . . . . 12
    ..^             |
128 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
    ..^       
   |
130 | 126, 114 | sylan2 482 |
. . . . . . . . . . . . 13
    ..^       
   |
131 | 3 | adantr 472 |
. . . . . . . . . . . . 13
    ..^         |
132 | 125, 96 | syl5ss 3429 |
. . . . . . . . . . . . . . . 16
 
 ..^        |
133 | 132 | sselda 3418 |
. . . . . . . . . . . . . . 15
    ..^         |
134 | | 1cnd 9677 |
. . . . . . . . . . . . . . 15
    ..^         |
135 | 109 | sselda 3418 |
. . . . . . . . . . . . . . . 16
    ..^     |
136 | | 1cnd 9677 |
. . . . . . . . . . . . . . . 16
    ..^     |
137 | 124 | dvmptid 22990 |
. . . . . . . . . . . . . . . 16
 
 ..^   
      |
138 | 125, 94 | syl5ss 3429 |
. . . . . . . . . . . . . . . 16
 
 ..^        |
139 | | iooretop 21864 |
. . . . . . . . . . . . . . . . 17
         |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
 ..^            |
141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 22996 |
. . . . . . . . . . . . . . 15
 
 ..^   
              |
142 | 124, 133,
134, 141, 3 | dvmptcmul 22997 |
. . . . . . . . . . . . . 14
 
 ..^   
                  |
143 | 3 | mulid1d 9678 |
. . . . . . . . . . . . . . 15
 
 ..^      |
144 | 143 | mpteq2dv 4483 |
. . . . . . . . . . . . . 14
 
 ..^                  |
145 | 142, 144 | eqtrd 2505 |
. . . . . . . . . . . . 13
 
 ..^   
                |
146 | 126, 116 | sylan2 482 |
. . . . . . . . . . . . 13
    ..^         |
147 | | dvfsumabs.v |
. . . . . . . . . . . . . 14
 
    
  |
148 | 147 | adantlr 729 |
. . . . . . . . . . . . 13
    ..^         |
149 | | dvfsumabs.b |
. . . . . . . . . . . . . 14
                 |
150 | 149 | adantr 472 |
. . . . . . . . . . . . 13
 
 ..^   
              |
151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 23000 |
. . . . . . . . . . . 12
 
 ..^   
                    |
152 | 78 | rexrd 9708 |
. . . . . . . . . . . . . 14
 
 ..^    |
153 | | iooss1 11696 |
. . . . . . . . . . . . . 14
                 |
154 | 152, 82, 153 | syl2anc 673 |
. . . . . . . . . . . . 13
 
 ..^                |
155 | 80 | rexrd 9708 |
. . . . . . . . . . . . . 14
 
 ..^    |
156 | | iooss2 11697 |
. . . . . . . . . . . . . 14
          
      |
157 | 155, 85, 156 | syl2anc 673 |
. . . . . . . . . . . . 13
 
 ..^              |
158 | 154, 157 | sstrd 3428 |
. . . . . . . . . . . 12
 
 ..^              |
159 | | iooretop 21864 |
. . . . . . . . . . . . 13
           |
160 | 159 | a1i 11 |
. . . . . . . . . . . 12
 
 ..^              |
161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 22996 |
. . . . . . . . . . 11
 
 ..^   
                        |
162 | 122, 161 | eqtrd 2505 |
. . . . . . . . . 10
 
 ..^   
  ![[,] [,]](_icc.gif)                      |
163 | 162 | dmeqd 5042 |
. . . . . . . . 9
 
 ..^ 
    ![[,] [,]](_icc.gif)                      |
164 | | eqid 2471 |
. . . . . . . . . 10
                     |
165 | 128, 164 | dmmpti 5717 |
. . . . . . . . 9
                 |
166 | 163, 165 | syl6eq 2521 |
. . . . . . . 8
 
 ..^ 
    ![[,] [,]](_icc.gif)                  |
167 | 162 | adantr 472 |
. . . . . . . . . . . . . 14
    ..^             ![[,] [,]](_icc.gif)                      |
168 | 167 | fveq1d 5881 |
. . . . . . . . . . . . 13
    ..^              ![[,] [,]](_icc.gif)                             |
169 | | simpr 468 |
. . . . . . . . . . . . . 14
    ..^                 |
170 | 164 | fvmpt2 5972 |
. . . . . . . . . . . . . 14
        
                    |
171 | 169, 128,
170 | sylancl 675 |
. . . . . . . . . . . . 13
    ..^                           |
172 | 168, 171 | eqtrd 2505 |
. . . . . . . . . . . 12
    ..^              ![[,] [,]](_icc.gif)                 |
173 | 172 | fveq2d 5883 |
. . . . . . . . . . 11
    ..^                 ![[,] [,]](_icc.gif)                 
    |
174 | | dvfsumabs.l |
. . . . . . . . . . . 12
 
  ..^                 |
175 | 174 | anassrs 660 |
. . . . . . . . . . 11
    ..^                 |
176 | 173, 175 | eqbrtrd 4416 |
. . . . . . . . . 10
    ..^                 ![[,] [,]](_icc.gif)                |
177 | 176 | ralrimiva 2809 |
. . . . . . . . 9
 
 ..^                  ![[,] [,]](_icc.gif)                |
178 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
179 | | nfcv 2612 |
. . . . . . . . . . . . . 14
   |
180 | | nfcv 2612 |
. . . . . . . . . . . . . 14
  |
181 | | nfmpt1 4485 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)          |
182 | 179, 180,
181 | nfov 6334 |
. . . . . . . . . . . . 13
      ![[,] [,]](_icc.gif)           |
183 | | nfcv 2612 |
. . . . . . . . . . . . 13
   |
184 | 182, 183 | nffv 5886 |
. . . . . . . . . . . 12
    
  ![[,] [,]](_icc.gif)              |
185 | 178, 184 | nffv 5886 |
. . . . . . . . . . 11
          ![[,] [,]](_icc.gif)               |
186 | | nfcv 2612 |
. . . . . . . . . . 11
  |
187 | | nfcv 2612 |
. . . . . . . . . . 11
   |
188 | 185, 186,
187 | nfbr 4440 |
. . . . . . . . . 10
          ![[,] [,]](_icc.gif)               |
189 | | fveq2 5879 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)               |
190 | 189 | fveq2d 5883 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                |
191 | 190 | breq1d 4405 |
. . . . . . . . . 10
          ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)             
   |
192 | 188, 191 | rspc 3130 |
. . . . . . . . 9
        
               ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                 |
193 | 177, 192 | mpan9 477 |
. . . . . . . 8
    ..^                 ![[,] [,]](_icc.gif)                |
194 | 67, 70, 108, 166, 62, 193 | dvlip 23024 |
. . . . . . 7
    ..^       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                          |
195 | 194 | ex 441 |
. . . . . 6
 
 ..^        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)             
             |
196 | 74, 76, 195 | mp2and 693 |
. . . . 5
 
 ..^          ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                          |
197 | | ovex 6336 |
. . . . . . . . 9
         ![]_ ]_](_urbrack.gif)   |
198 | | nfcv 2612 |
. . . . . . . . . 10
     |
199 | | nfcv 2612 |
. . . . . . . . . . 11
       |
200 | | nfcv 2612 |
. . . . . . . . . . 11
  |
201 | | nfcsb1v 3365 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)  |
202 | 199, 200,
201 | nfov 6334 |
. . . . . . . . . 10
           ![]_ ]_](_urbrack.gif)   |
203 | | oveq2 6316 |
. . . . . . . . . . 11
   
       |
204 | | csbeq1a 3358 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)   |
205 | 203, 204 | oveq12d 6326 |
. . . . . . . . . 10
                ![]_ ]_](_urbrack.gif)    |
206 | | eqid 2471 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          |
207 | 198, 202,
205, 206 | fvmptf 5981 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)             ![]_ ]_](_urbrack.gif)       ![[,] [,]](_icc.gif)                       ![]_ ]_](_urbrack.gif)    |
208 | 74, 197, 207 | sylancl 675 |
. . . . . . . 8
 
 ..^      ![[,] [,]](_icc.gif)                       ![]_ ]_](_urbrack.gif)    |
209 | 67 | recnd 9687 |
. . . . . . . . . . 11
 
 ..^    |
210 | 3, 209 | mulcld 9681 |
. . . . . . . . . 10
 
 ..^      |
211 | 210, 37 | subcld 10005 |
. . . . . . . . 9
 
 ..^       ![]_ ]_](_urbrack.gif)    |
212 | | nfcv 2612 |
. . . . . . . . . 10
   |
213 | | nfcv 2612 |
. . . . . . . . . . 11
     |
214 | | nfcsb1v 3365 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
215 | 213, 200,
214 | nfov 6334 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)   |
216 | | oveq2 6316 |
. . . . . . . . . . 11
 
     |
217 | | csbeq1a 3358 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   |
218 | 216, 217 | oveq12d 6326 |
. . . . . . . . . 10
          ![]_ ]_](_urbrack.gif)    |
219 | 212, 215,
218, 206 | fvmptf 5981 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)         ![]_ ]_](_urbrack.gif)       ![[,] [,]](_icc.gif)                 ![]_ ]_](_urbrack.gif)    |
220 | 76, 211, 219 | syl2anc 673 |
. . . . . . . 8
 
 ..^      ![[,] [,]](_icc.gif)                 ![]_ ]_](_urbrack.gif)    |
221 | 208, 220 | oveq12d 6326 |
. . . . . . 7
 
 ..^       ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
222 | | peano2cn 9823 |
. . . . . . . . . 10
     |
223 | 209, 222 | syl 17 |
. . . . . . . . 9
 
 ..^      |
224 | 3, 223 | mulcld 9681 |
. . . . . . . 8
 
 ..^        |
225 | 224, 210,
32, 37 | sub4d 10054 |
. . . . . . 7
 
 ..^                ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
226 | | 1cnd 9677 |
. . . . . . . . . . 11
 
 ..^    |
227 | 209, 226 | pncan2d 10007 |
. . . . . . . . . 10
 
 ..^        |
228 | 227 | oveq2d 6324 |
. . . . . . . . 9
 
 ..^            |
229 | 3, 223, 209 | subdid 10095 |
. . . . . . . . 9
 
 ..^                  |
230 | 228, 229,
143 | 3eqtr3d 2513 |
. . . . . . . 8
 
 ..^       
    |
231 | 230 | oveq1d 6323 |
. . . . . . 7
 
 ..^                ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
232 | 221, 225,
231 | 3eqtr2rd 2512 |
. . . . . 6
 
 ..^        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)               |
233 | 232 | fveq2d 5883 |
. . . . 5
 
 ..^     
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)            ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                |
234 | 227 | fveq2d 5883 |
. . . . . . . 8
 
 ..^                |
235 | | abs1 13437 |
. . . . . . . 8
     |
236 | 234, 235 | syl6eq 2521 |
. . . . . . 7
 
 ..^            |
237 | 236 | oveq2d 6324 |
. . . . . 6
 
 ..^                |
238 | 62 | recnd 9687 |
. . . . . . 7
 
 ..^    |
239 | 238 | mulid1d 9678 |
. . . . . 6
 
 ..^      |
240 | 237, 239 | eqtr2d 2506 |
. . . . 5
 
 ..^              |
241 | 196, 233,
240 | 3brtr4d 4426 |
. . . 4
 
 ..^     
     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
  |
242 | 2, 60, 62, 241 | fsumle 13936 |
. . 3
   ..^           ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ..^    |
243 | 59, 61, 63, 64, 242 | letrd 9809 |
. 2
    
 ..^        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ..^    |
244 | 56, 243 | eqbrtrrd 4418 |
1
       ..^  
     ..^    |