Step | Hyp | Ref
| Expression |
1 | | dvply1.f |
. . 3
                     |
2 | 1 | oveq2d 6304 |
. 2
                         |
3 | | eqid 2450 |
. . . . . 6
  ℂfld   ℂfld |
4 | 3 | cnfldtop 21797 |
. . . . 5
  ℂfld  |
5 | 3 | cnfldtopon 21796 |
. . . . . . 7
  ℂfld TopOn   |
6 | 5 | toponunii 19940 |
. . . . . 6
   ℂfld |
7 | 6 | restid 15325 |
. . . . 5
   ℂfld    ℂfld
↾t    ℂfld  |
8 | 4, 7 | ax-mp 5 |
. . . 4
   ℂfld ↾t    ℂfld |
9 | 8 | eqcomi 2459 |
. . 3
  ℂfld    ℂfld ↾t   |
10 | | cnelprrecn 9629 |
. . . 4
    |
11 | 10 | a1i 11 |
. . 3
      |
12 | 6 | topopn 19929 |
. . . 4
   ℂfld   ℂfld  |
13 | 4, 12 | mp1i 13 |
. . 3
   ℂfld  |
14 | | fzfid 12183 |
. . 3
       |
15 | | dvply1.a |
. . . . . . 7
       |
16 | | elfznn0 11884 |
. . . . . . 7
       |
17 | | ffvelrn 6018 |
. . . . . . 7
     
       |
18 | 15, 16, 17 | syl2an 480 |
. . . . . 6
 
           |
19 | 18 | adantr 467 |
. . . . 5
               |
20 | | simpr 463 |
. . . . . 6
           |
21 | 16 | ad2antlr 732 |
. . . . . 6
           |
22 | 20, 21 | expcld 12413 |
. . . . 5
               |
23 | 19, 22 | mulcld 9660 |
. . . 4
                     |
24 | 23 | 3impa 1202 |
. . 3
 
   

            |
25 | 18 | 3adant3 1027 |
. . . 4
 
   

      |
26 | | 0cnd 9633 |
. . . . 5
      

   |
27 | | simpl2 1011 |
. . . . . . . 8
      

       |
28 | 27, 16 | syl 17 |
. . . . . . 7
      

   |
29 | 28 | nn0cnd 10924 |
. . . . . 6
      

   |
30 | | simpl3 1012 |
. . . . . . 7
      

   |
31 | | simpr 463 |
. . . . . . . . 9
      


  |
32 | | elnn0 10868 |
. . . . . . . . . 10

    |
33 | 28, 32 | sylib 200 |
. . . . . . . . 9
      

 
   |
34 | | orel2 385 |
. . . . . . . . 9
       |
35 | 31, 33, 34 | sylc 62 |
. . . . . . . 8
      

   |
36 | | nnm1nn0 10908 |
. . . . . . . 8
     |
37 | 35, 36 | syl 17 |
. . . . . . 7
      

     |
38 | 30, 37 | expcld 12413 |
. . . . . 6
      

         |
39 | 29, 38 | mulcld 9660 |
. . . . 5
      

           |
40 | 26, 39 | ifclda 3912 |
. . . 4
 
   

               |
41 | 25, 40 | mulcld 9660 |
. . 3
 
   

                     |
42 | 10 | a1i 11 |
. . . 4
 
          |
43 | | c0ex 9634 |
. . . . . 6
 |
44 | | ovex 6316 |
. . . . . 6
         |
45 | 43, 44 | ifex 3948 |
. . . . 5
              |
46 | 45 | a1i 11 |
. . . 4
                        |
47 | 16 | adantl 468 |
. . . . 5
 
       |
48 | | dvexp2 22901 |
. . . . 5

                         |
49 | 47, 48 | syl 17 |
. . . 4
 
                              |
50 | 42, 22, 46, 49, 18 | dvmptcmul 22911 |
. . 3
 
                                          |
51 | 9, 3, 11, 13, 14, 24, 41, 50 | dvmptfsum 22920 |
. 2
                                                  |
52 | | elfznn 11825 |
. . . . . . . . . . 11
       |
53 | 52 | nnne0d 10651 |
. . . . . . . . . 10
       |
54 | 53 | neneqd 2628 |
. . . . . . . . 9
    
  |
55 | 54 | adantl 468 |
. . . . . . . 8
        
  |
56 | 55 | iffalsed 3891 |
. . . . . . 7
                                |
57 | 56 | oveq2d 6304 |
. . . . . 6
                                            |
58 | 57 | sumeq2dv 13762 |
. . . . 5
 

                                               |
59 | | 1eluzge0 11199 |
. . . . . . 7
     |
60 | | fzss1 11834 |
. . . . . . 7
    
          |
61 | 59, 60 | mp1i 13 |
. . . . . 6
 

          |
62 | 15 | adantr 467 |
. . . . . . . 8
 

      |
63 | 52 | nnnn0d 10922 |
. . . . . . . 8
       |
64 | 62, 63, 17 | syl2an 480 |
. . . . . . 7
               |
65 | 53 | adantl 468 |
. . . . . . . . . 10
           |
66 | 65 | neneqd 2628 |
. . . . . . . . 9
        
  |
67 | 66 | iffalsed 3891 |
. . . . . . . 8
                                |
68 | 63 | adantl 468 |
. . . . . . . . . 10
           |
69 | 68 | nn0cnd 10924 |
. . . . . . . . 9
           |
70 | | simplr 761 |
. . . . . . . . . 10
           |
71 | 52, 36 | syl 17 |
. . . . . . . . . . 11
         |
72 | 71 | adantl 468 |
. . . . . . . . . 10
             |
73 | 70, 72 | expcld 12413 |
. . . . . . . . 9
                 |
74 | 69, 73 | mulcld 9660 |
. . . . . . . 8
                   |
75 | 67, 74 | eqeltrd 2528 |
. . . . . . 7
                        |
76 | 64, 75 | mulcld 9660 |
. . . . . 6
                              |
77 | | eldifn 3555 |
. . . . . . . . . . . 12
          
      |
78 | | 0p1e1 10718 |
. . . . . . . . . . . . . 14
   |
79 | 78 | oveq1i 6298 |
. . . . . . . . . . . . 13
           |
80 | 79 | eleq2i 2520 |
. . . . . . . . . . . 12
      
      |
81 | 77, 80 | sylnibr 307 |
. . . . . . . . . . 11
          
        |
82 | 81 | adantl 468 |
. . . . . . . . . 10
              
        |
83 | | eldifi 3554 |
. . . . . . . . . . . 12
                 |
84 | 83 | adantl 468 |
. . . . . . . . . . 11
              
      |
85 | | dvply1.n |
. . . . . . . . . . . . . 14
   |
86 | | nn0uz 11190 |
. . . . . . . . . . . . . 14
     |
87 | 85, 86 | syl6eleq 2538 |
. . . . . . . . . . . . 13
       |
88 | 87 | ad2antrr 731 |
. . . . . . . . . . . 12
              
      |
89 | | elfzp12 11870 |
. . . . . . . . . . . 12
    
                |
90 | 88, 89 | syl 17 |
. . . . . . . . . . 11
              
                |
91 | 84, 90 | mpbid 214 |
. . . . . . . . . 10
              
          |
92 | | orel2 385 |
. . . . . . . . . 10
                   |
93 | 82, 91, 92 | sylc 62 |
. . . . . . . . 9
              
  |
94 | 93 | iftrued 3888 |
. . . . . . . 8
              
               |
95 | 94 | oveq2d 6304 |
. . . . . . 7
              
                           |
96 | 62, 16, 17 | syl2an 480 |
. . . . . . . . 9
               |
97 | 96 | mul01d 9829 |
. . . . . . . 8
                 |
98 | 83, 97 | sylan2 477 |
. . . . . . 7
              
        |
99 | 95, 98 | eqtrd 2484 |
. . . . . 6
              
                     |
100 | | fzfid 12183 |
. . . . . 6
 

      |
101 | 61, 76, 99, 100 | fsumss 13784 |
. . . . 5
 

                                                    |
102 | | elfznn0 11884 |
. . . . . . . . . . . . . . 15
         |
103 | 102 | adantl 468 |
. . . . . . . . . . . . . 14
       
     |
104 | 103 | nn0cnd 10924 |
. . . . . . . . . . . . 13
       
     |
105 | | ax-1cn 9594 |
. . . . . . . . . . . . 13
 |
106 | | pncan 9878 |
. . . . . . . . . . . . 13
 
       |
107 | 104, 105,
106 | sylancl 667 |
. . . . . . . . . . . 12
       
         |
108 | 107 | oveq2d 6304 |
. . . . . . . . . . 11
       
                 |
109 | 108 | oveq2d 6304 |
. . . . . . . . . 10
       
                         |
110 | 109 | oveq2d 6304 |
. . . . . . . . 9
       
                                         |
111 | 15 | ad2antrr 731 |
. . . . . . . . . . 11
       
         |
112 | | peano2nn0 10907 |
. . . . . . . . . . . . 13

    |
113 | 102, 112 | syl 17 |
. . . . . . . . . . . 12
           |
114 | 113 | adantl 468 |
. . . . . . . . . . 11
       
       |
115 | 111, 114 | ffvelrnd 6021 |
. . . . . . . . . 10
       
           |
116 | 114 | nn0cnd 10924 |
. . . . . . . . . 10
       
       |
117 | | simplr 761 |
. . . . . . . . . . 11
       
     |
118 | 117, 103 | expcld 12413 |
. . . . . . . . . 10
       
         |
119 | 115, 116,
118 | mulassd 9663 |
. . . . . . . . 9
       
                                     |
120 | 115, 116 | mulcomd 9661 |
. . . . . . . . . 10
       
                         |
121 | 120 | oveq1d 6303 |
. . . . . . . . 9
       
                                     |
122 | 110, 119,
121 | 3eqtr2d 2490 |
. . . . . . . 8
       
                                         |
123 | 122 | sumeq2dv 13762 |
. . . . . . 7
 

    
                       
                         |
124 | | 1m1e0 10675 |
. . . . . . . . 9
   |
125 | 124 | oveq1i 6298 |
. . . . . . . 8
           
   |
126 | 125 | sumeq1i 13757 |
. . . . . . 7
      
                       
                            |
127 | | oveq1 6295 |
. . . . . . . . . 10
       |
128 | 127 | fveq2d 5867 |
. . . . . . . . . 10
               |
129 | 127, 128 | oveq12d 6306 |
. . . . . . . . 9
                       |
130 | | oveq2 6296 |
. . . . . . . . 9
           |
131 | 129, 130 | oveq12d 6306 |
. . . . . . . 8
                                   |
132 | 131 | cbvsumv 13755 |
. . . . . . 7
    
                   
                        |
133 | 123, 126,
132 | 3eqtr4g 2509 |
. . . . . 6
 

      
                       
                         |
134 | | 1zzd 10965 |
. . . . . . 7
 

  |
135 | 85 | adantr 467 |
. . . . . . . 8
 

  |
136 | 135 | nn0zd 11035 |
. . . . . . 7
 

  |
137 | 64, 74 | mulcld 9660 |
. . . . . . 7
                         |
138 | | fveq2 5863 |
. . . . . . . 8
               |
139 | | id 22 |
. . . . . . . . 9
       |
140 | | oveq1 6295 |
. . . . . . . . . 10
           |
141 | 140 | oveq2d 6304 |
. . . . . . . . 9
                   |
142 | 139, 141 | oveq12d 6306 |
. . . . . . . 8
                         |
143 | 138, 142 | oveq12d 6306 |
. . . . . . 7
                                       |
144 | 134, 134,
136, 137, 143 | fsumshftm 13835 |
. . . . . 6
 

                    
                               |
145 | | elfznn0 11884 |
. . . . . . . . . 10
         |
146 | 145 | adantl 468 |
. . . . . . . . 9
       
     |
147 | | ovex 6316 |
. . . . . . . . 9
           |
148 | | dvply1.b |
. . . . . . . . . 10
             |
149 | 148 | fvmpt2 5955 |
. . . . . . . . 9
                             |
150 | 146, 147,
149 | sylancl 667 |
. . . . . . . 8
       
                   |
151 | 150 | oveq1d 6303 |
. . . . . . 7
       
                               |
152 | 151 | sumeq2dv 13762 |
. . . . . 6
 

    
             
                         |
153 | 133, 144,
152 | 3eqtr4d 2494 |
. . . . 5
 

                    
                   |
154 | 58, 101, 153 | 3eqtr3d 2492 |
. . . 4
 

                                             |
155 | 154 | mpteq2dva 4488 |
. . 3
                                                  |
156 | | dvply1.g |
. . 3
      
                |
157 | 155, 156 | eqtr4d 2487 |
. 2
                              |
158 | 2, 51, 157 | 3eqtrd 2488 |
1
     |