Step | Hyp | Ref
| Expression |
1 | | 1elunit 11751 |
. . 3
  ![[,] [,]](_icc.gif)   |
2 | | 0elunit 11750 |
. . 3
  ![[,] [,]](_icc.gif)   |
3 | | 0red 9644 |
. . . 4
 

    |
4 | | 1red 9658 |
. . . 4
 

    |
5 | | dvlipcn.d |
. . . . . . . . . . . . . 14

    |
6 | | ssid 3451 |
. . . . . . . . . . . . . . . 16
 |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15

  |
8 | | dvlipcn.f |
. . . . . . . . . . . . . . 15
       |
9 | | dvlipcn.x |
. . . . . . . . . . . . . . 15

  |
10 | 7, 8, 9 | dvbss 22856 |
. . . . . . . . . . . . . 14
     |
11 | 5, 10 | sstrd 3442 |
. . . . . . . . . . . . 13

  |
12 | 11, 9 | sstrd 3442 |
. . . . . . . . . . . 12

  |
13 | 12 | adantr 467 |
. . . . . . . . . . 11
 

    |
14 | | simprl 764 |
. . . . . . . . . . 11
 

 
  |
15 | 13, 14 | sseldd 3433 |
. . . . . . . . . 10
 

 
  |
16 | 15 | adantr 467 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)     |
17 | | unitssre 11779 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
18 | | ax-resscn 9596 |
. . . . . . . . . . 11
 |
19 | 17, 18 | sstri 3441 |
. . . . . . . . . 10
  ![[,] [,]](_icc.gif)   |
20 | | simpr 463 |
. . . . . . . . . 10
   
 
  ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
21 | 19, 20 | sseldi 3430 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)     |
22 | 16, 21 | mulcomd 9664 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)   
     |
23 | | simprr 766 |
. . . . . . . . . . 11
 

 
  |
24 | 13, 23 | sseldd 3433 |
. . . . . . . . . 10
 

 
  |
25 | 24 | adantr 467 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)     |
26 | | iirev 21957 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
27 | 26 | adantl 468 |
. . . . . . . . . 10
   
 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)    |
28 | 19, 27 | sseldi 3430 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)       |
29 | 25, 28 | mulcomd 9664 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)   
         |
30 | 22, 29 | oveq12d 6308 |
. . . . . . 7
   
 
  ![[,] [,]](_icc.gif)                     |
31 | | dvlipcn.a |
. . . . . . . . 9
   |
32 | 31 | ad2antrr 732 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)     |
33 | | dvlipcn.r |
. . . . . . . . 9
   |
34 | 33 | ad2antrr 732 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)     |
35 | 14 | adantr 467 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)     |
36 | 23 | adantr 467 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)     |
37 | | dvlipcn.b |
. . . . . . . . 9
          |
38 | 37 | blcvx 21816 |
. . . . . . . 8
    
  ![[,] [,]](_icc.gif)              |
39 | 32, 34, 35, 36, 20, 38 | syl23anc 1275 |
. . . . . . 7
   
 
  ![[,] [,]](_icc.gif)             |
40 | 30, 39 | eqeltrd 2529 |
. . . . . 6
   
 
  ![[,] [,]](_icc.gif)             |
41 | | eqidd 2452 |
. . . . . 6
 

     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
42 | 8, 11 | fssresd 5750 |
. . . . . . . . 9
         |
43 | 42 | feqmptd 5918 |
. . . . . . . 8
             |
44 | | fvres 5879 |
. . . . . . . . 9
             |
45 | 44 | mpteq2ia 4485 |
. . . . . . . 8
  
            |
46 | 43, 45 | syl6eq 2501 |
. . . . . . 7
           |
47 | 46 | adantr 467 |
. . . . . 6
 

            |
48 | | fveq2 5865 |
. . . . . 6
                           |
49 | 40, 41, 47, 48 | fmptco 6056 |
. . . . 5
 

        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)                 |
50 | | eqid 2451 |
. . . . . . . 8
   ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)            |
51 | 40, 50 | fmptd 6046 |
. . . . . . 7
 

     ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)      |
52 | | eqid 2451 |
. . . . . . . . 9
  ℂfld   ℂfld |
53 | 52 | addcn 21897 |
. . . . . . . . . 10
    ℂfld   ℂfld   ℂfld  |
54 | 53 | a1i 11 |
. . . . . . . . 9
 

 
    ℂfld
  ℂfld   ℂfld   |
55 | | cncfmptc 21943 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
56 | 19, 6, 55 | mp3an23 1356 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
57 | 15, 56 | syl 17 |
. . . . . . . . . 10
 

     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
58 | | cncfmptid 21944 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
59 | 19, 6, 58 | mp2an 678 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
60 | 59 | a1i 11 |
. . . . . . . . . 10
 

     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
61 | 57, 60 | mulcncf 22398 |
. . . . . . . . 9
 

     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
62 | | cncfmptc 21943 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
63 | 19, 6, 62 | mp3an23 1356 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
64 | 24, 63 | syl 17 |
. . . . . . . . . 10
 

     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
65 | 52 | subcn 21898 |
. . . . . . . . . . . 12
    ℂfld   ℂfld   ℂfld  |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
 

 
    ℂfld
  ℂfld   ℂfld   |
67 | | ax-1cn 9597 |
. . . . . . . . . . . . 13
 |
68 | | cncfmptc 21943 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
69 | 67, 19, 6, 68 | mp3an 1364 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
70 | 69 | a1i 11 |
. . . . . . . . . . 11
 

     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
71 | 52, 66, 70, 60 | cncfmpt2f 21946 |
. . . . . . . . . 10
 

     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)       |
72 | 64, 71 | mulcncf 22398 |
. . . . . . . . 9
 

     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       |
73 | 52, 54, 61, 72 | cncfmpt2f 21946 |
. . . . . . . 8
 

     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
74 | | cncffvrn 21930 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       |
75 | 13, 73, 74 | syl2anc 667 |
. . . . . . 7
 

      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       |
76 | 51, 75 | mpbird 236 |
. . . . . 6
 

     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)       |
77 | 6 | a1i 11 |
. . . . . . 7
 

    |
78 | 42 | adantr 467 |
. . . . . . 7
 

          |
79 | 52 | cnfldtop 21804 |
. . . . . . . . . . . . . . 15
  ℂfld  |
80 | 52 | cnfldtopon 21803 |
. . . . . . . . . . . . . . . . 17
  ℂfld TopOn   |
81 | 80 | toponunii 19947 |
. . . . . . . . . . . . . . . 16
   ℂfld |
82 | 81 | restid 15332 |
. . . . . . . . . . . . . . 15
   ℂfld    ℂfld
↾t    ℂfld  |
83 | 79, 82 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ℂfld ↾t    ℂfld |
84 | 83 | eqcomi 2460 |
. . . . . . . . . . . . 13
  ℂfld    ℂfld ↾t   |
85 | 52, 84 | dvres 22866 |
. . . . . . . . . . . 12
                        ℂfld       |
86 | 7, 8, 9, 12, 85 | syl22anc 1269 |
. . . . . . . . . . 11
              ℂfld       |
87 | | cnxmet 21793 |
. . . . . . . . . . . . . . . 16

      |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . 15
 
       |
89 | 52 | cnfldtopn 21802 |
. . . . . . . . . . . . . . . 16
  ℂfld       |
90 | 89 | blopn 21515 |
. . . . . . . . . . . . . . 15
  
    
            ℂfld  |
91 | 88, 31, 33, 90 | syl3anc 1268 |
. . . . . . . . . . . . . 14
            ℂfld  |
92 | 37, 91 | syl5eqel 2533 |
. . . . . . . . . . . . 13
   ℂfld  |
93 | | isopn3i 20098 |
. . . . . . . . . . . . 13
    ℂfld
  ℂfld
      ℂfld      |
94 | 79, 92, 93 | sylancr 669 |
. . . . . . . . . . . 12
       ℂfld      |
95 | 94 | reseq2d 5105 |
. . . . . . . . . . 11
          ℂfld           |
96 | 86, 95 | eqtrd 2485 |
. . . . . . . . . 10
           |
97 | 96 | dmeqd 5037 |
. . . . . . . . 9
  
        |
98 | | dmres 5125 |
. . . . . . . . . 10
     
   |
99 | | df-ss 3418 |
. . . . . . . . . . 11

 
      |
100 | 5, 99 | sylib 200 |
. . . . . . . . . 10
  
    |
101 | 98, 100 | syl5eq 2497 |
. . . . . . . . 9
       |
102 | 97, 101 | eqtrd 2485 |
. . . . . . . 8
  
    |
103 | 102 | adantr 467 |
. . . . . . 7
 

        |
104 | | dvcn 22875 |
. . . . . . 7
                       |
105 | 77, 78, 13, 103, 104 | syl31anc 1271 |
. . . . . 6
 

          |
106 | 76, 105 | cncfco 21939 |
. . . . 5
 

        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       |
107 | 49, 106 | eqeltrrd 2530 |
. . . 4
 

     ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)       |
108 | 18 | a1i 11 |
. . . . . . . 8
 

    |
109 | 17 | a1i 11 |
. . . . . . . 8
 

    ![[,] [,]](_icc.gif) 
  |
110 | 8 | ad2antrr 732 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)         |
111 | 11 | ad2antrr 732 |
. . . . . . . . . 10
   
 
  ![[,] [,]](_icc.gif)     |
112 | 111, 40 | sseldd 3433 |
. . . . . . . . 9
   
 
  ![[,] [,]](_icc.gif)             |
113 | 110, 112 | ffvelrnd 6023 |
. . . . . . . 8
   
 
  ![[,] [,]](_icc.gif)       
         |
114 | 52 | tgioo2 21821 |
. . . . . . . 8
       ℂfld
↾t   |
115 | | 1re 9642 |
. . . . . . . . 9
 |
116 | | iccntr 21839 |
. . . . . . . . 9
 
       
      ![[,] [,]](_icc.gif)         |
117 | 3, 115, 116 | sylancl 668 |
. . . . . . . 8
 

        
      ![[,] [,]](_icc.gif)         |
118 | 108, 109,
113, 114, 52, 117 | dvmptntr 22925 |
. . . . . . 7
 

      ![[,] [,]](_icc.gif)                                      |
119 | | reelprrecn 9631 |
. . . . . . . . 9
    |
120 | 119 | a1i 11 |
. . . . . . . 8
 

       |
121 | | cnelprrecn 9632 |
. . . . . . . . 9
    |
122 | 121 | a1i 11 |
. . . . . . . 8
 

       |
123 | | ioossicc 11720 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   |
124 | 123 | sseli 3428 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)    |
125 | 124, 40 | sylan2 477 |
. . . . . . . 8
   
 
               |
126 | 15, 24 | subcld 9986 |
. . . . . . . . 9
 

      |
127 | 126 | adantr 467 |
. . . . . . . 8
   
 
     
   |
128 | 11 | adantr 467 |
. . . . . . . . . 10
 

    |
129 | 128 | sselda 3432 |
. . . . . . . . 9
   
 
   |
130 | 8 | adantr 467 |
. . . . . . . . . 10
 

        |
131 | 130 | ffvelrnda 6022 |
. . . . . . . . 9
   
 
       |
132 | 129, 131 | syldan 473 |
. . . . . . . 8
   
 
       |
133 | | fvex 5875 |
. . . . . . . . 9
       |
134 | 133 | a1i 11 |
. . . . . . . 8
   
 
         |
135 | 15 | adantr 467 |
. . . . . . . . . . 11
   
 
       |
136 | 124, 21 | sylan2 477 |
. . . . . . . . . . 11
   
 
       |
137 | 135, 136 | mulcld 9663 |
. . . . . . . . . 10
   
 
     
   |
138 | | 1red 9658 |
. . . . . . . . . . . 12
   
 
       |
139 | | simpr 463 |
. . . . . . . . . . . . . 14
   
 

  |
140 | 139 | recnd 9669 |
. . . . . . . . . . . . 13
   
 

  |
141 | | 1red 9658 |
. . . . . . . . . . . . 13
   
 

  |
142 | 120 | dvmptid 22911 |
. . . . . . . . . . . . 13
 

          |
143 | | ioossre 11696 |
. . . . . . . . . . . . . 14
     |
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
 

     
  |
145 | | iooretop 21786 |
. . . . . . . . . . . . . 14
         |
146 | 145 | a1i 11 |
. . . . . . . . . . . . 13
 

            |
147 | 120, 140,
141, 142, 144, 114, 52, 146 | dvmptres 22917 |
. . . . . . . . . . . 12
 

                  |
148 | 120, 136,
138, 147, 15 | dvmptcmul 22918 |
. . . . . . . . . . 11
 

                      |
149 | 15 | mulid1d 9660 |
. . . . . . . . . . . 12
 

      |
150 | 149 | mpteq2dv 4490 |
. . . . . . . . . . 11
 

                  |
151 | 148, 150 | eqtrd 2485 |
. . . . . . . . . 10
 

                    |
152 | 24 | adantr 467 |
. . . . . . . . . . 11
   
 
       |
153 | 124, 28 | sylan2 477 |
. . . . . . . . . . 11
   
 
         |
154 | 152, 153 | mulcld 9663 |
. . . . . . . . . 10
   
 
     
     |
155 | | negex 9873 |
. . . . . . . . . . 11
  |
156 | 155 | a1i 11 |
. . . . . . . . . 10
   
 
        |
157 | | negex 9873 |
. . . . . . . . . . . . 13
  |
158 | 157 | a1i 11 |
. . . . . . . . . . . 12
   
 
        |
159 | | 1cnd 9659 |
. . . . . . . . . . . . . 14
   
 
       |
160 | | 0red 9644 |
. . . . . . . . . . . . . 14
   
 
       |
161 | | 1cnd 9659 |
. . . . . . . . . . . . . . 15
   
 

  |
162 | | 0red 9644 |
. . . . . . . . . . . . . . 15
   
 

  |
163 | | 1cnd 9659 |
. . . . . . . . . . . . . . . 16
 

    |
164 | 120, 163 | dvmptc 22912 |
. . . . . . . . . . . . . . 15
 

          |
165 | 120, 161,
162, 164, 144, 114, 52, 146 | dvmptres 22917 |
. . . . . . . . . . . . . 14
 

                  |
166 | 120, 159,
160, 165, 136, 138, 147 | dvmptsub 22921 |
. . . . . . . . . . . . 13
 

                      |
167 | | df-neg 9863 |
. . . . . . . . . . . . . 14
    |
168 | 167 | mpteq2i 4486 |
. . . . . . . . . . . . 13
                |
169 | 166, 168 | syl6eqr 2503 |
. . . . . . . . . . . 12
 

                     |
170 | 120, 153,
158, 169, 24 | dvmptcmul 22918 |
. . . . . . . . . . 11
 

                         |
171 | | neg1cn 10713 |
. . . . . . . . . . . . . 14
  |
172 | | mulcom 9625 |
. . . . . . . . . . . . . 14
            |
173 | 24, 171, 172 | sylancl 668 |
. . . . . . . . . . . . 13
 

          |
174 | 24 | mulm1d 10070 |
. . . . . . . . . . . . 13
 

        |
175 | 173, 174 | eqtrd 2485 |
. . . . . . . . . . . 12
 

        |
176 | 175 | mpteq2dv 4490 |
. . . . . . . . . . 11
 

                    |
177 | 170, 176 | eqtrd 2485 |
. . . . . . . . . 10
 

                       |
178 | 120, 137,
135, 151, 154, 156, 177 | dvmptadd 22914 |
. . . . . . . . 9
 

                             |
179 | 15, 24 | negsubd 9992 |
. . . . . . . . . 10
 

         |
180 | 179 | mpteq2dv 4490 |
. . . . . . . . 9
 

                     |
181 | 178, 180 | eqtrd 2485 |
. . . . . . . 8
 

                            |
182 | 9 | adantr 467 |
. . . . . . . . . . 11
 

    |
183 | 77, 130, 182, 13, 85 | syl22anc 1269 |
. . . . . . . . . 10
 

               ℂfld       |
184 | 94 | adantr 467 |
. . . . . . . . . . 11
 

        ℂfld      |
185 | 184 | reseq2d 5105 |
. . . . . . . . . 10
 

           ℂfld           |
186 | 183, 185 | eqtrd 2485 |
. . . . . . . . 9
 

            |
187 | 47 | oveq2d 6306 |
. . . . . . . . 9
 

                |
188 | | dvfcn 22863 |
. . . . . . . . . . . . 13
       
     |
189 | 103 | feq2d 5715 |
. . . . . . . . . . . . 13
 

    
                     |
190 | 188, 189 | mpbii 215 |
. . . . . . . . . . . 12
 

            |
191 | 186 | feq1d 5714 |
. . . . . . . . . . . 12
 

    
     
           |
192 | 190, 191 | mpbid 214 |
. . . . . . . . . . 11
 

            |
193 | 192 | feqmptd 5918 |
. . . . . . . . . 10
 

                  |
194 | | fvres 5879 |
. . . . . . . . . . 11
                 |
195 | 194 | mpteq2ia 4485 |
. . . . . . . . . 10
                   |
196 | 193, 195 | syl6eq 2501 |
. . . . . . . . 9
 

                |
197 | 186, 187,
196 | 3eqtr3d 2493 |
. . . . . . . 8
 

                    |
198 | | fveq2 5865 |
. . . . . . . 8
                               |
199 | 120, 122,
125, 127, 132, 134, 181, 197, 48, 198 | dvmptco 22926 |
. . . . . . 7
 

                                                |
200 | 118, 199 | eqtrd 2485 |
. . . . . 6
 

      ![[,] [,]](_icc.gif)                                          |
201 | 200 | dmeqd 5037 |
. . . . 5
 

      ![[,] [,]](_icc.gif)                                    
     |
202 | | ovex 6318 |
. . . . . . 7
       
           |
203 | 202 | rgenw 2749 |
. . . . . 6
                         |
204 | | dmmptg 5332 |
. . . . . 6
 
                                           
         |
205 | 203, 204 | mp1i 13 |
. . . . 5
 

                      
         |
206 | 201, 205 | eqtrd 2485 |
. . . 4
 

      ![[,] [,]](_icc.gif)                      |
207 | | dvlipcn.m |
. . . . . 6
   |
208 | 207 | adantr 467 |
. . . . 5
 

 
  |
209 | 126 | abscld 13498 |
. . . . 5
 

     
    |
210 | 208, 209 | remulcld 9671 |
. . . 4
 

            |
211 | 200 | fveq1d 5867 |
. . . . . . . . . . 11
 

       ![[,] [,]](_icc.gif)                                        
        |
212 | | eqid 2451 |
. . . . . . . . . . . . 13
            
                                    |
213 | 212 | fvmpt2 5957 |
. . . . . . . . . . . 12
                     
                                                   |
214 | 202, 213 | mpan2 677 |
. . . . . . . . . . 11
                          
             
            |
215 | 211, 214 | sylan9eq 2505 |
. . . . . . . . . 10
   
 
          ![[,] [,]](_icc.gif)                          
            |
216 | 215 | fveq2d 5869 |
. . . . . . . . 9
   
 
             ![[,] [,]](_icc.gif)                                            |
217 | | dvfcn 22863 |
. . . . . . . . . . 11
         |
218 | 5 | ad2antrr 732 |
. . . . . . . . . . . 12
   
 
         |
219 | 218, 125 | sseldd 3433 |
. . . . . . . . . . 11
   
 
                 |
220 | | ffvelrn 6020 |
. . . . . . . . . . 11
                  
        
         |
221 | 217, 219,
220 | sylancr 669 |
. . . . . . . . . 10
   
 
           
         |
222 | 221, 127 | absmuld 13516 |
. . . . . . . . 9
   
 
                                     
                 |
223 | 216, 222 | eqtrd 2485 |
. . . . . . . 8
   
 
             ![[,] [,]](_icc.gif)                                                |
224 | 221 | abscld 13498 |
. . . . . . . . 9
   
 
                         |
225 | 207 | ad2antrr 732 |
. . . . . . . . 9
   
 
       |
226 | 127 | abscld 13498 |
. . . . . . . . 9
   
 
             |
227 | 127 | absge0d 13506 |
. . . . . . . . 9
   
 
        
    |
228 | | dvlipcn.l |
. . . . . . . . . . . . 13
 
             |
229 | 228 | ralrimiva 2802 |
. . . . . . . . . . . 12
              |
230 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
231 | 230 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                       |
232 | 231 | breq1d 4412 |
. . . . . . . . . . . . 13
           
             |
233 | 232 | cbvralv 3019 |
. . . . . . . . . . . 12
 
                       |
234 | 229, 233 | sylib 200 |
. . . . . . . . . . 11
              |
235 | 234 | ad2antrr 732 |
. . . . . . . . . 10
   
 
     
            |
236 | | fveq2 5865 |
. . . . . . . . . . . . 13
                               |
237 | 236 | fveq2d 5869 |
. . . . . . . . . . . 12
                            
          |
238 | 237 | breq1d 4412 |
. . . . . . . . . . 11
                   
                     |
239 | 238 | rspcv 3146 |
. . . . . . . . . 10
          
                               |
240 | 125, 235,
239 | sylc 62 |
. . . . . . . . 9
   
 
                         |
241 | 224, 225,
226, 227, 240 | lemul1ad 10546 |
. . . . . . . 8
   
 
               
                         |
242 | 223, 241 | eqbrtrd 4423 |
. . . . . . 7
   
 
             ![[,] [,]](_icc.gif)                              |
243 | 242 | ralrimiva 2802 |
. . . . . 6
 

  
             ![[,] [,]](_icc.gif)                    
         |
244 | | nfv 1761 |
. . . . . . 7
          ![[,] [,]](_icc.gif)                    
        |
245 | | nfcv 2592 |
. . . . . . . . 9
   |
246 | | nfcv 2592 |
. . . . . . . . . . 11
   |
247 | | nfcv 2592 |
. . . . . . . . . . 11
  |
248 | | nfmpt1 4492 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)                |
249 | 246, 247,
248 | nfov 6316 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)                 |
250 | | nfcv 2592 |
. . . . . . . . . 10
   |
251 | 249, 250 | nffv 5872 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)                    |
252 | 245, 251 | nffv 5872 |
. . . . . . . 8
          ![[,] [,]](_icc.gif)                     |
253 | | nfcv 2592 |
. . . . . . . 8
  |
254 | | nfcv 2592 |
. . . . . . . 8
           |
255 | 252, 253,
254 | nfbr 4447 |
. . . . . . 7
          ![[,] [,]](_icc.gif)                    
        |
256 | | fveq2 5865 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)                     |
257 | 256 | fveq2d 5869 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)                            ![[,] [,]](_icc.gif)                      |
258 | 257 | breq1d 4412 |
. . . . . . 7
          ![[,] [,]](_icc.gif)                    
      
        ![[,] [,]](_icc.gif)                               |
259 | 244, 255,
258 | cbvral 3015 |
. . . . . 6
 
             ![[,] [,]](_icc.gif)                   
    
  
              ![[,] [,]](_icc.gif)                    
         |
260 | 243, 259 | sylib 200 |
. . . . 5
 

  
             ![[,] [,]](_icc.gif)                    
         |
261 | 260 | r19.21bi 2757 |
. . . 4
   
 
             ![[,] [,]](_icc.gif)                              |
262 | 3, 4, 107, 206, 210, 261 | dvlip 22945 |
. . 3
   
 
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                                      |
263 | 1, 2, 262 | mpanr12 691 |
. 2
 

          ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                                      |
264 | | oveq2 6298 |
. . . . . . . . 9
 
     |
265 | | oveq2 6298 |
. . . . . . . . . . 11
       |
266 | | 1m1e0 10678 |
. . . . . . . . . . 11
   |
267 | 265, 266 | syl6eq 2501 |
. . . . . . . . . 10
     |
268 | 267 | oveq2d 6306 |
. . . . . . . . 9
 
       |
269 | 264, 268 | oveq12d 6308 |
. . . . . . . 8
                 |
270 | 269 | fveq2d 5869 |
. . . . . . 7
     
                   |
271 | | eqid 2451 |
. . . . . . 7
   ![[,] [,]](_icc.gif)                  ![[,] [,]](_icc.gif)                |
272 | | fvex 5875 |
. . . . . . 7
           |
273 | 270, 271,
272 | fvmpt 5948 |
. . . . . 6
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                              |
274 | 1, 273 | ax-mp 5 |
. . . . 5
    ![[,] [,]](_icc.gif)                             |
275 | 24 | mul01d 9832 |
. . . . . . . 8
 

      |
276 | 149, 275 | oveq12d 6308 |
. . . . . . 7
 

            |
277 | 15 | addid1d 9833 |
. . . . . . 7
 

      |
278 | 276, 277 | eqtrd 2485 |
. . . . . 6
 

          |
279 | 278 | fveq2d 5869 |
. . . . 5
 

                  |
280 | 274, 279 | syl5eq 2497 |
. . . 4
 

      ![[,] [,]](_icc.gif)                        |
281 | | oveq2 6298 |
. . . . . . . . 9
 
     |
282 | | oveq2 6298 |
. . . . . . . . . . 11
       |
283 | | 1m0e1 10720 |
. . . . . . . . . . 11
   |
284 | 282, 283 | syl6eq 2501 |
. . . . . . . . . 10
     |
285 | 284 | oveq2d 6306 |
. . . . . . . . 9
 
       |
286 | 281, 285 | oveq12d 6308 |
. . . . . . . 8
                 |
287 | 286 | fveq2d 5869 |
. . . . . . 7
     
                   |
288 | | fvex 5875 |
. . . . . . 7
           |
289 | 287, 271,
288 | fvmpt 5948 |
. . . . . 6
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)                              |
290 | 2, 289 | ax-mp 5 |
. . . . 5
    ![[,] [,]](_icc.gif)                             |
291 | 15 | mul01d 9832 |
. . . . . . . 8
 

      |
292 | 24 | mulid1d 9660 |
. . . . . . . 8
 

      |
293 | 291, 292 | oveq12d 6308 |
. . . . . . 7
 

            |
294 | 24 | addid2d 9834 |
. . . . . . 7
 

      |
295 | 293, 294 | eqtrd 2485 |
. . . . . 6
 

          |
296 | 295 | fveq2d 5869 |
. . . . 5
 

                  |
297 | 290, 296 | syl5eq 2497 |
. . . 4
 

      ![[,] [,]](_icc.gif)                        |
298 | 280, 297 | oveq12d 6308 |
. . 3
 

       ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                               |
299 | 298 | fveq2d 5869 |
. 2
 

          ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                                    |
300 | 283 | fveq2i 5868 |
. . . . 5
           |
301 | | abs1 13360 |
. . . . 5
     |
302 | 300, 301 | eqtri 2473 |
. . . 4
       |
303 | 302 | oveq2i 6301 |
. . 3
                           |
304 | 210 | recnd 9669 |
. . . 4
 

            |
305 | 304 | mulid1d 9660 |
. . 3
 

                      |
306 | 303, 305 | syl5eq 2497 |
. 2
 

                            |
307 | 263, 299,
306 | 3brtr3d 4432 |
1
 

               
    
     |