Step | Hyp | Ref
| Expression |
1 | | dvbsss 22857 |
. . . . . . . 8
   |
2 | | id 22 |
. . . . . . . . 9

  |
3 | | fperdvper.g |
. . . . . . . . . 10
   |
4 | 3 | dmeqi 5036 |
. . . . . . . . 9
   |
5 | 2, 4 | syl6eleq 2539 |
. . . . . . . 8

    |
6 | 1, 5 | sseldi 3430 |
. . . . . . 7

  |
7 | 6 | adantl 468 |
. . . . . 6
 
   |
8 | | fperdvper.t |
. . . . . . 7
   |
9 | 8 | adantr 467 |
. . . . . 6
 
   |
10 | 7, 9 | readdcld 9670 |
. . . . 5
 
     |
11 | | reopn 37502 |
. . . . . . 7
     |
12 | | retop 21782 |
. . . . . . . 8
     |
13 | | ssid 3451 |
. . . . . . . . 9
 |
14 | 13 | a1i 11 |
. . . . . . . 8
 
   |
15 | | uniretop 21783 |
. . . . . . . . 9
      |
16 | 15 | isopn3 20082 |
. . . . . . . 8
      
                    |
17 | 12, 14, 16 | sylancr 669 |
. . . . . . 7
 
                     |
18 | 11, 17 | mpbii 215 |
. . . . . 6
 
       
       |
19 | 18 | eqcomd 2457 |
. . . . 5
 
               |
20 | 10, 19 | eleqtrd 2531 |
. . . 4
 
                 |
21 | 5 | adantl 468 |
. . . . . . . 8
 
     |
22 | 3 | fveq1i 5866 |
. . . . . . . . . 10
           |
23 | 22 | eqcomi 2460 |
. . . . . . . . 9
           |
24 | 23 | a1i 11 |
. . . . . . . 8
 
             |
25 | | dvf 22862 |
. . . . . . . . . . . 12
         |
26 | | ffun 5731 |
. . . . . . . . . . . 12
             |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . 11
   |
28 | 27 | a1i 11 |
. . . . . . . . . 10
     |
29 | | funbrfv2b 5909 |
. . . . . . . . . 10
  
        
                 |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
           

              |
31 | 30 | adantr 467 |
. . . . . . . 8
 
         
                 |
32 | 21, 24, 31 | mpbir2and 933 |
. . . . . . 7
 
           |
33 | | eqid 2451 |
. . . . . . . . 9
  ℂfld   ℂfld |
34 | 33 | tgioo2 21821 |
. . . . . . . 8
       ℂfld
↾t   |
35 | | eqid 2451 |
. . . . . . . 8
                                         |
36 | | ax-resscn 9596 |
. . . . . . . . 9
 |
37 | 36 | a1i 11 |
. . . . . . . 8
 
   |
38 | | fperdvper.f |
. . . . . . . . 9
       |
39 | 38 | adantr 467 |
. . . . . . . 8
 
       |
40 | 34, 33, 35, 37, 39, 14 | eldv 22853 |
. . . . . . 7
 
         
       
                              lim      |
41 | 32, 40 | mpbid 214 |
. . . . . 6
 
             
                         lim     |
42 | 41 | simprd 465 |
. . . . 5
 
                          lim    |
43 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . 20
   
      
                     
                         
      |
44 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
45 | 44 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
46 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . 22
      
    |
47 | 45, 46 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . 21
               
                       |
48 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
49 | 48 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
50 | 49 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

        |
51 | 8 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
52 | 51 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

     
  |
53 | 50, 52 | npcand 9990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

            |
54 | 53 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

            |
55 | 54 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

                    |
56 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
57 | 48 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

        |
58 | 8 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

     
  |
59 | 57, 58 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

          |
60 | 59 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
61 | 60 | imdistani 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

      
     |
62 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     |
63 | 62 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

       |
64 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
65 | 64 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
66 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
67 | 65, 66 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             
                 |
68 | 63, 67 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                   |
69 | | fperdvper.fper |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

            |
70 | 68, 69 | vtoclg 3107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
                    |
71 | 56, 61, 70 | mpsyl 65 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

                      |
72 | 55, 71 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

                  |
73 | 72 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
            |
74 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
  |
75 | 6 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
  |
76 | 74, 75, 69 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
            |
77 | 73, 76 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
        
                 |
78 | 49 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
  |
79 | 74, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
  |
80 | 7 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
   |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
  |
82 | 78, 79, 81 | subsub4d 10017 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
     
    |
83 | 79, 81 | addcomd 9835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
      |
84 | 83 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
          |
85 | 82, 84 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
          |
86 | 77, 85 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
              
                       |
87 | 47, 86 | sylan9eqr 2507 |
. . . . . . . . . . . . . . . . . . . 20
   
       
                                       |
88 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . 20
   
      

       |
89 | 38 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

            |
90 | 89, 59 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

              |
91 | 90 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
        |
92 | 39, 7 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
93 | 92 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
      |
94 | 91, 93 | subcld 9986 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
              |
95 | 78, 79 | subcld 9986 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
    |
96 | 95, 81 | subcld 9986 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
      |
97 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
               |
98 | 49 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
             |
99 | 79 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
             |
100 | 81 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
             |
101 | 98, 99, 100 | subadd2d 10005 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                   |
102 | 97, 101 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
               |
103 | 102 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
               |
104 | | eldifsni 4098 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
105 | 104 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
               |
106 | 105 | neneqd 2629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
          

   |
107 | 103, 106 | pm2.65da 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
    |
108 | 107 | neqned 2631 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
    |
109 | 95, 81, 108 | subne0d 9995 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
      |
110 | 94, 96, 109 | divcld 10383 |
. . . . . . . . . . . . . . . . . . . 20
   
      
                    |
111 | 43, 87, 88, 110 | fvmptd 5954 |
. . . . . . . . . . . . . . . . . . 19
   
      
                 
                                |
112 | 111 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . 18
   
      
                       
                              |
113 | 112 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
   
      
                                                              |
114 | 113 | adantr 467 |
. . . . . . . . . . . . . . . 16
   
                    
                                                              |
115 | 114 | adantllr 725 |
. . . . . . . . . . . . . . 15
     
                                                                  
                                                              |
116 | | simpllr 769 |
. . . . . . . . . . . . . . . . . 18
     
                                                               
                                               |
117 | 48 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . 20
     
                                                                 |
118 | 8 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . . 20
     
                                                              
  |
119 | 117, 118 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . 19
     
                                                                   |
120 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
121 | 107, 120 | nsyl 125 |
. . . . . . . . . . . . . . . . . . . . 21
   
      
      |
122 | 121 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
   
                       |
123 | 122 | adantllr 725 |
. . . . . . . . . . . . . . . . . . 19
     
                                                                     |
124 | 119, 123 | eldifd 3415 |
. . . . . . . . . . . . . . . . . 18
     
                                                                       |
125 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
126 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
127 | 126 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
128 | 127 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
129 | 125, 128 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . 20
                           |
130 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                       |
131 | 130 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                           |
132 | 131 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                   |
133 | 132 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . 20
                                 
                                   |
134 | 129, 133 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . 19
            
                              
                                                 |
135 | 134 | rspccva 3149 |
. . . . . . . . . . . . . . . . . 18
                                                                                                       |
136 | 116, 124,
135 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
     
                                                                           
                                   |
137 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      
                                          |
138 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
       
       |
139 | 138 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
       
               |
140 | 139 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
       
                           |
141 | 138 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
       
           |
142 | 140, 141 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
       
                                     |
143 | 48 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
      
  |
144 | 74, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
      
  |
145 | 143, 144 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      
    |
146 | 145, 121 | eldifd 3415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
      
        |
147 | 137, 142,
146, 110 | fvmptd 5954 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
                                              |
148 | 147 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      
                                              |
149 | 148 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
     

                           
                                                                                |
150 | 149 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
     

                           
                                                                                    |
151 | 150 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
     

                           
                                                                                            |
152 | 108 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                     |
153 | 85 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      
          |
154 | 153 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                           |
155 | 154 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                                   |
156 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                           |
157 | 155, 156 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                           |
158 | 152, 157 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                               |
159 | 158 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
     

                           
                                                |
160 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
     

                           
                                                                                  |
161 | 159, 160 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
     

                           
                                                                    |
162 | 151, 161 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . . . 19
     

                           
                                                            |
163 | 162 | ex 436 |
. . . . . . . . . . . . . . . . . 18
   
                                                               
                           |
164 | 163 | adantllr 725 |
. . . . . . . . . . . . . . . . 17
     
                                                                                                             
                           |
165 | 136, 164 | mpd 15 |
. . . . . . . . . . . . . . . 16
     
                                                                                         |
166 | 165 | adantrl 722 |
. . . . . . . . . . . . . . 15
     
                                                                  
                          |
167 | 115, 166 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
     
                                                                  
                                      |
168 | 167 | ex 436 |
. . . . . . . . . . . . 13
   
                                                          
        
                                       |
169 | 168 | ralrimiva 2802 |
. . . . . . . . . . . 12
                                                                                                  
            |
170 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . 19
                                               |
171 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
172 | 171 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
173 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . 21
       |
174 | 172, 173 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . 20
                               |
175 | 174 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
     
                               |
176 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
           |
177 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . 20
               |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
                     |
179 | 170, 175,
176, 178 | fvmptd 5954 |
. . . . . . . . . . . . . . . . . 18
                                             |
180 | 179 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
                                                 |
181 | 180 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                                         |
182 | 181 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
     
                                               
          
                                                                  |
183 | | simpll 760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
184 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
185 | 184 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
186 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
187 | 186 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  

     |
188 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
189 | 188 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
190 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
191 | 189, 190 | eqeq12d 2466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
192 | 187, 191 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
             
               |
193 | 192, 69 | chvarv 2107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

            |
194 | 193 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

            |
195 | 183, 185,
194 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
    
            |
196 | 6 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
    
  |
197 | 183, 196,
69 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
            |
198 | 197 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
    
            |
199 | 195, 198 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
                          |
200 | 185 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
201 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
202 | 183, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
203 | 200, 201,
202 | pnpcan2d 10024 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
    
          |
204 | 203 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
          |
205 | 199, 204 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
                                      |
206 | 205 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . 20
   
    
                            
             |
207 | 206 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
   
    
                                          
       |
208 | 207 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
                                                               |
209 | 208 | adantllr 725 |
. . . . . . . . . . . . . . . . 17
     
                                               
          
           
                                          
       |
210 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . 19
     
                                               
          
           
                                               
            |
211 | 184 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . . . . 21
     
                                               
          
           
  |
212 | 8 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . . . 21
     
                                               
          
           
  |
213 | 211, 212 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . 20
     
                                               
          
           
    |
214 | | eldifsni 4098 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
215 | 214 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
  |
216 | 200, 201,
202, 215 | addneintr2d 9841 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
    
      |
217 | 216 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                   |
218 | 217 | adantllr 725 |
. . . . . . . . . . . . . . . . . . . . 21
     
                                               
          
           
      |
219 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
220 | 219 | necon3ai 2649 |
. . . . . . . . . . . . . . . . . . . . 21
             |
221 | 218, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
     
                                               
          
           
        |
222 | 213, 221 | eldifd 3415 |
. . . . . . . . . . . . . . . . . . 19
     
                                               
          
           
          |
223 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
224 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
    |
225 | 224 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
               |
226 | 225 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . . 22
           
             |
227 | 223, 226 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
228 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                         
                             
           |
229 | 228 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          
                               
            |
230 | 229 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
                        
                                        
             |
231 | 230 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . . 21
                              
                                   
              |
232 | 227, 231 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
       
        
                                    
                                           
               |
233 | 232 | rspccva 3149 |
. . . . . . . . . . . . . . . . . . 19
                                                 
                  
                                           
              |
234 | 210, 222,
233 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
     
                                               
          
           
                                           
              |
235 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    
                     
                         
      |
236 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
237 | 236 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                               |
238 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          
    |
239 | 237, 238 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
                           |
240 | 239 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
     
                                
            |
241 | 183, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
    
  |
242 | 185, 241 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
    
    |
243 | 216, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
    
        |
244 | 242, 243 | eldifd 3415 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    
          |
245 | 205, 177 | syl6eqelr 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
    
                  
     |
246 | 235, 240,
244, 245 | fvmptd 5954 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
    
                 
                                
     |
247 | 246 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
    
                  
                         
           |
248 | 247 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

                
          
                                                   
                                
           |
249 | 248 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . . 22
     

                
          
                                                           
                           
            |
250 | 249 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . 21
     

                
           |