Step | Hyp | Ref
| Expression |
1 | | nnuz 11222 |
. . . . . . 7
     |
2 | | 1zzd 10996 |
. . . . . . 7
  |
3 | | eqidd 2462 |
. . . . . . . . 9
                                       |
4 | | oveq2 6322 |
. . . . . . . . . . . . . 14
       |
5 | 4 | oveq1d 6329 |
. . . . . . . . . . . . 13
           |
6 | 5 | oveq1d 6329 |
. . . . . . . . . . . 12
               |
7 | 6 | fveq2d 5891 |
. . . . . . . . . . 11
                       |
8 | 7, 5 | oveq12d 6332 |
. . . . . . . . . 10
                                   |
9 | 8 | adantl 472 |
. . . . . . . . 9
 
                                   |
10 | | id 22 |
. . . . . . . . 9
   |
11 | | ovex 6342 |
. . . . . . . . . 10
                 |
12 | 11 | a1i 11 |
. . . . . . . . 9
                   |
13 | 3, 9, 10, 12 | fvmptd 5976 |
. . . . . . . 8
                                         |
14 | 13 | adantl 472 |
. . . . . . 7
                                          |
15 | | 2z 10997 |
. . . . . . . . . . . . . . 15
 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . 14
   |
17 | | nnz 10987 |
. . . . . . . . . . . . . 14
   |
18 | 16, 17 | zmulcld 11074 |
. . . . . . . . . . . . 13
     |
19 | | 1zzd 10996 |
. . . . . . . . . . . . 13
   |
20 | 18, 19 | zsubcld 11073 |
. . . . . . . . . . . 12
       |
21 | 20 | zcnd 11069 |
. . . . . . . . . . 11
       |
22 | | fouriersw.x |
. . . . . . . . . . . . 13
 |
23 | 22 | recni 9680 |
. . . . . . . . . . . 12
 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
   |
25 | 21, 24 | mulcld 9688 |
. . . . . . . . . 10
         |
26 | 25 | sincld 14232 |
. . . . . . . . 9
             |
27 | | 0red 9669 |
. . . . . . . . . 10
   |
28 | | 2re 10706 |
. . . . . . . . . . . . . 14
 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . 13
   |
30 | | 1red 9683 |
. . . . . . . . . . . . 13
   |
31 | 29, 30 | remulcld 9696 |
. . . . . . . . . . . 12
     |
32 | 31, 30 | resubcld 10074 |
. . . . . . . . . . 11
       |
33 | 20 | zred 11068 |
. . . . . . . . . . 11
       |
34 | | 0lt1 10163 |
. . . . . . . . . . . . 13
 |
35 | | 2t1e2 10786 |
. . . . . . . . . . . . . . 15
   |
36 | 35 | oveq1i 6324 |
. . . . . . . . . . . . . 14
       |
37 | | 2m1e1 10751 |
. . . . . . . . . . . . . 14
   |
38 | 36, 37 | eqtr2i 2484 |
. . . . . . . . . . . . 13
     |
39 | 34, 38 | breqtri 4439 |
. . . . . . . . . . . 12
     |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
       |
41 | 18 | zred 11068 |
. . . . . . . . . . . 12
     |
42 | | nnre 10643 |
. . . . . . . . . . . . 13
   |
43 | | 0le2 10727 |
. . . . . . . . . . . . . 14
 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . 13
   |
45 | | nnge1 10662 |
. . . . . . . . . . . . 13
   |
46 | 30, 42, 29, 44, 45 | lemul2ad 10574 |
. . . . . . . . . . . 12
       |
47 | 31, 41, 30, 46 | lesub1dd 10256 |
. . . . . . . . . . 11
           |
48 | 27, 32, 33, 40, 47 | ltletrd 9820 |
. . . . . . . . . 10
       |
49 | 27, 48 | gtned 9795 |
. . . . . . . . 9
       |
50 | 26, 21, 49 | divcld 10410 |
. . . . . . . 8
                   |
51 | 50 | adantl 472 |
. . . . . . 7
                    |
52 | | picn 23462 |
. . . . . . . . . . 11
 |
53 | 52 | a1i 11 |
. . . . . . . . . 10
  |
54 | | 4cn 10714 |
. . . . . . . . . . 11
 |
55 | 54 | a1i 11 |
. . . . . . . . . 10
  |
56 | | 4ne0 10733 |
. . . . . . . . . . 11
 |
57 | 56 | a1i 11 |
. . . . . . . . . 10
  |
58 | 53, 55, 57 | divcld 10410 |
. . . . . . . . 9
    |
59 | | eqid 2461 |
. . . . . . . . . . . . . . . 16
                                       |
60 | | 0cnd 9661 |
. . . . . . . . . . . . . . . . 17
   |
61 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   |
62 | | nncn 10644 |
. . . . . . . . . . . . . . . . . . . 20
   |
63 | | mulcl 9648 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
64 | 62, 52, 63 | sylancl 673 |
. . . . . . . . . . . . . . . . . . 19
     |
65 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
66 | | nnne0 10669 |
. . . . . . . . . . . . . . . . . . . 20
   |
67 | | 0re 9668 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
68 | | pipos 23463 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
69 | 67, 68 | gtneii 9771 |
. . . . . . . . . . . . . . . . . . . . 21
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
71 | 62, 65, 66, 70 | mulne0d 10291 |
. . . . . . . . . . . . . . . . . . 19
     |
72 | 61, 64, 71 | divcld 10410 |
. . . . . . . . . . . . . . . . . 18
       |
73 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
74 | 62, 73 | mulcld 9688 |
. . . . . . . . . . . . . . . . . . 19
     |
75 | 74 | sincld 14232 |
. . . . . . . . . . . . . . . . . 18
         |
76 | 72, 75 | mulcld 9688 |
. . . . . . . . . . . . . . . . 17
               |
77 | 60, 76 | ifcld 3935 |
. . . . . . . . . . . . . . . 16
                    |
78 | 59, 77 | fmpti 6067 |
. . . . . . . . . . . . . . 15
                        |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . 14
                         |
80 | | eqidd 2462 |
. . . . . . . . . . . . . . . . . 18
                                         |
81 | | breq2 4419 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
82 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
83 | 82 | oveq2d 6330 |
. . . . . . . . . . . . . . . . . . . . 21
           |
84 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
85 | 84 | fveq2d 5891 |
. . . . . . . . . . . . . . . . . . . . 21
               |
86 | 83, 85 | oveq12d 6332 |
. . . . . . . . . . . . . . . . . . . 20
                           |
87 | 81, 86 | ifbieq2d 3917 |
. . . . . . . . . . . . . . . . . . 19
                                     |
88 | 87 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
 
   
                                 |
89 | | c0ex 9662 |
. . . . . . . . . . . . . . . . . . . 20
 |
90 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . 20
             |
91 | 89, 90 | ifex 3960 |
. . . . . . . . . . . . . . . . . . 19
                  |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                    |
93 | 80, 88, 10, 92 | fvmptd 5976 |
. . . . . . . . . . . . . . . . 17
                                           |
94 | 93 | adantr 471 |
. . . . . . . . . . . . . . . 16
                              
                |
95 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
         |
96 | | simpl 463 |
. . . . . . . . . . . . . . . . . . 19
       |
97 | | 2nn 10795 |
. . . . . . . . . . . . . . . . . . 19
 |
98 | | nndivdvds 14359 |
. . . . . . . . . . . . . . . . . . 19
 
       |
99 | 96, 97, 98 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
           |
100 | 95, 99 | mpbird 240 |
. . . . . . . . . . . . . . . . 17
       |
101 | 100 | iftrued 3900 |
. . . . . . . . . . . . . . . 16
                        |
102 | 94, 101 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
                              |
103 | 102 | 3adant1 1032 |
. . . . . . . . . . . . . 14
                             |
104 | | fouriersw.f |
. . . . . . . . . . . . . . . . . 18
           |
105 | | 1re 9667 |
. . . . . . . . . . . . . . . . . . . 20
 |
106 | 105 | renegcli 9960 |
. . . . . . . . . . . . . . . . . . . 20
  |
107 | 105, 106 | keepel 3959 |
. . . . . . . . . . . . . . . . . . 19
   
     |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
           |
109 | 104, 108 | fmpti 6067 |
. . . . . . . . . . . . . . . . 17
     |
110 | | fouriersw.t |
. . . . . . . . . . . . . . . . 17
   |
111 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
112 | 111 | breq1d 4425 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
     |
113 | 112 | ifbid 3914 |
. . . . . . . . . . . . . . . . . . . . . 22
            
      |
114 | 113 | cbvmptv 4508 |
. . . . . . . . . . . . . . . . . . . . 21
    
                |
115 | 104, 114 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . 20
           |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
             |
117 | | oveq1 6321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
       |
118 | | pire 23461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
119 | 28, 118 | remulcli 9682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
120 | 110, 119 | eqeltri 2535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
121 | 120 | recni 9680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
122 | 121 | mulid2i 9671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
123 | 122 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
124 | 123 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
125 | 124 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
126 | 117, 125 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
         |
127 | 126 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
128 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
  |
129 | | 2pos 10728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
130 | 28, 118, 129, 68 | mulgt0ii 9793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
131 | 110 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
132 | 130, 131 | breqtri 4439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
133 | 120, 132 | elrpii 11333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
  |
135 | | 1zzd 10996 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
136 | | modcyc 12163 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
137 | 128, 134,
135, 136 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . 22
 
             |
138 | 127, 137 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
139 | 138 | breq1d 4425 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
140 | 139 | ifbid 3914 |
. . . . . . . . . . . . . . . . . . 19
 
                     |
141 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
   |
142 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
143 | 141, 142 | readdcld 9695 |
. . . . . . . . . . . . . . . . . . 19
     |
144 | 116, 140,
143, 108 | fvmptd 5976 |
. . . . . . . . . . . . . . . . . 18
                 |
145 | 104 | fvmpt2 5979 |
. . . . . . . . . . . . . . . . . . 19
                         |
146 | 107, 145 | mpan2 682 |
. . . . . . . . . . . . . . . . . 18
               |
147 | 144, 146 | eqtr4d 2498 |
. . . . . . . . . . . . . . . . 17
             |
148 | | eqid 2461 |
. . . . . . . . . . . . . . . . 17
                   |
149 | | snfi 7675 |
. . . . . . . . . . . . . . . . . 18
   |
150 | | eldifi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
151 | | 0xr 9712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
153 | 118 | rexri 9718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
154 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
155 | | elioore 11694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        |
156 | 155 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
  |
157 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
  |
158 | 118 | renegcli 9960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  |
159 | 158 | rexri 9718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  |
160 | | iooltub 37647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
161 | 159, 153,
160 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        |
162 | 161 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
163 | 152, 154,
156, 157, 162 | eliood 37632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
      |
164 | | negpilt0 37527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  |
165 | 158, 67, 164 | ltleii 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  |
166 | | iooss1 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
            |
167 | 159, 165,
166 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          |
168 | 167 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
169 | 104 | reseq1i 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       |
170 | | ioossre 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
171 | | resmpt 5172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    
                        
       |
172 | 170, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                        
      |
173 | | elioore 11694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
174 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
175 | | 0red 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
176 | | ioogtlb 37629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
         |
177 | 151, 153,
176 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
178 | 175, 173,
177 | ltled 9808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
179 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
180 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
181 | 168, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
182 | | pirp 23464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 |
183 | | 2timesgt 37538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42

    |
184 | 182, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
185 | 184, 131 | breqtri 4439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       |
187 | 173, 179,
180, 181, 186 | lttrd 9821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
188 | | modid 12152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
 
    |
189 | 173, 174,
178, 187, 188 | syl22anc 1277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
   |
190 | 189, 181 | eqbrtrd 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
   |
191 | 190 | iftrued 3900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
192 | 191 | mpteq2ia 4498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        
            |
193 | 169, 172,
192 | 3eqtrri 2488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             |
194 | 193 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
       |
195 | | reelprrecn 9656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    |
196 | 195 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
197 | | iooretop 21834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         |
198 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  ℂfld   ℂfld |
199 | 198 | tgioo2 21869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       ℂfld
↾t   |
200 | 197, 199 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       ℂfld
↾t   |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
   ℂfld ↾t    |
202 | | 1cnd 9684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
203 | 196, 201,
202 | dvmptconst 37822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                |
204 | 203 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
205 | | ssid 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 |
206 | | ax-resscn 9621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
207 | | fss 5759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
208 | 109, 206,
207 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
209 | | dvresioo 37830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
                       |
210 | 205, 208,
209 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                 |
211 | 194, 204,
210 | 3eqtr3i 2491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
               |
212 | 211 | dmeqi 5054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
213 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
214 | 89, 213 | dmmpti 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
215 | 212, 214 | eqtr3i 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
216 | | ssdmres 5144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
              |
217 | 215, 216 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
218 | 217 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
219 | 168, 218 | elind 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
    |
220 | | dmres 5143 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               
   |
221 | 219, 220 | syl6eleqr 2550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                |
222 | 163, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
           |
223 | 222 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
224 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
225 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
226 | 155 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
  |
227 | | ioogtlb 37629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
228 | 159, 153,
227 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         |
229 | 228 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
230 | | 0red 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
231 | | neqne 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
232 | 231 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
233 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
  |
234 | 226, 230,
232, 233 | lttri5d 37554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
235 | 224, 225,
226, 229, 234 | eliood 37632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
       |
236 | 67, 118, 68 | ltleii 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
237 | | iooss2 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
238 | 153, 236,
237 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
239 | 238 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
240 | 104 | reseq1i 5119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                         |
241 | | ioossre 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      |
242 | | resmpt 5172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
                          
       |
243 | 241, 242 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                          
      |
244 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
        |
245 | | elioore 11694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
        |
246 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
        |
247 | 245, 246 | modcld 12133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      
   |
248 | 245, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
          |
249 | 52 | 2timesi 10758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
     |
250 | 110, 249 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   |
251 | 250 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     
   |
252 | | negpicn 23465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
  |
253 | 252, 52, 52 | addassi 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   
       |
254 | 253 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
        
  |
255 | 52 | negidi 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
    |
256 | 52, 252, 255 | addcomli 9850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    |
257 | 256 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   
    |
258 | 52 | addid2i 9846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   |
259 | 257, 258 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   
  |
260 | 251, 254,
259 | 3eqtrri 2488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
    |
261 | 260 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
           |
262 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
         |
263 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
        |
264 | 239, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
         |
265 | 262, 245,
263, 264 | ltadd1dd 10251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             |
266 | 261, 265 | eqbrtrd 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
          |
267 | 244, 248,
266 | ltled 9808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
          |
268 | | 0red 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
        |
269 | 158, 120 | readdcli 9681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    |
270 | 269 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
           |
271 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
        |
272 | 271, 260 | syl6breq 4455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
           |
273 | 268, 270,
248, 272, 265 | lttrd 9821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
          |
274 | 268, 248,
273 | ltled 9808 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
          |
275 | 245 | recnd 9694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
        |
276 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
        |
277 | 275, 276 | addcomd 9860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
            |
278 | | iooltub 37647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
           |
279 | 159, 151,
278 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
        |
280 | | ltaddneg 37545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
       |
281 | 245, 120,
280 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
      
     |
282 | 279, 281 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
      
   |
283 | 277, 282 | eqbrtrd 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
          |
284 | 274, 283 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
      
       |
285 | | modid2 12155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
                 |
286 | 248, 133,
285 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
            
         |
287 | 284, 286 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
        
     |
288 | 125 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
         |
289 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
290 | | 1zzd 10996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   |
291 | 141, 289,
290, 136 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
           |
292 | 288, 291 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   
     |
293 | 245, 292 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
        
     |
294 | 287, 293 | eqtr3d 2497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
            |
295 | 267, 294 | breqtrd 4440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
          |
296 | 244, 247,
295 | lensymd 9811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
   |
297 | 296 | iffalsed 3903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
298 | 297 | mpteq2ia 4498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
              |
299 | 240, 243,
298 | 3eqtrri 2488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                |
300 | 299 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    |
301 | | iooretop 21834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          |
302 | 301, 199 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        ℂfld
↾t   |
303 | 302 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
        ℂfld
↾t    |
304 | 202 | negcld 9998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
305 | 196, 303,
304 | dvmptconst 37822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   |
306 | 305 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  |
307 | | dvresioo 37830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
                         |
308 | 205, 208,
307 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                   |
309 | 300, 306,
308 | 3eqtr3i 2491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
310 | 309 | dmeqi 5054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 |
311 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
312 | 89, 311 | dmmpti 5728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             |
313 | 310, 312 | eqtr3i 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
314 | | ssdmres 5144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
 
                |
315 | 313, 314 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        |
316 | 315 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
317 | 239, 316 | elind 3629 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
    |
318 | 317, 220 | syl6eleqr 2550 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
319 | 235, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
           |
320 | 223, 319 | pm2.61dan 805 |
. . . . . . . . . . . . . . . . . . . . . 22
      

           |
321 | 150, 320 | sylan 478 |
. . . . . . . . . . . . . . . . . . . . 21
                 

           |
322 | | eldifn 3567 |
. . . . . . . . . . . . . . . . . . . . . 22
                
           |
323 | 322 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
                 

           |
324 | 321, 323 | condan 808 |
. . . . . . . . . . . . . . . . . . . 20
                   |
325 | | elsn 3993 |
. . . . . . . . . . . . . . . . . . . 20
     |
326 | 324, 325 | sylibr 217 |
. . . . . . . . . . . . . . . . . . 19
                     |
327 | 326 | ssriv 3447 |
. . . . . . . . . . . . . . . . . 18
                   |
328 | | ssfi 7817 |
. . . . . . . . . . . . . . . . . 18
                                         |
329 | 149, 327,
328 | mp2an 683 |
. . . . . . . . . . . . . . . . 17
                 |
330 | | inss1 3663 |
. . . . . . . . . . . . . . . . . . . . . 22
     
         |
331 | 220, 330 | eqsstri 3473 |
. . . . . . . . . . . . . . . . . . . . 21
               |
332 | | ioosscn 37628 |
. . . . . . . . . . . . . . . . . . . . 21
      |
333 | 331, 332 | sstri 3452 |
. . . . . . . . . . . . . . . . . . . 20
          |
334 | 333 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
           |
335 | | dvf 22910 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
336 | | fresin 5774 |
. . . . . . . . . . . . . . . . . . . . . 22
                      
          |
337 | | ffdm 5765 |
. . . . . . . . . . . . . . . . . . . . . 22
                                             
           
         |
338 | 335, 336,
337 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
                               
 

        |
339 | 338 | simpli 464 |
. . . . . . . . . . . . . . . . . . . 20
                       |
340 | 339 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
                        |
341 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
342 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
343 | | ioossre 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      |
344 | 331 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
345 | 343, 344 | sseldi 3441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
346 | 345 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
  |
347 | 344, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
348 | 347 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
349 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
350 | 341, 342,
346, 348, 349 | eliood 37632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
       |
351 | | elun1 3612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
352 | 350, 351 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
             |
353 | | simpl 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          

           |
354 | | 0red 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          

  |
355 | 345 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          

  |
356 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          

  |
357 | 354, 355,
356 | nltled 9810 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          

  |
358 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
359 | 205 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  |
360 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
361 | 208 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      |
362 | | 0red 9669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  |
363 | | mnfxr 11442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
364 | 363 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
365 | 362 | mnfltd 11454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
366 | 360, 364,
362, 365 | lptioo2 37748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 |
367 | | incom 3636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
368 | | ioossre 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    |
369 | | df-ss 3429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
    
     |
370 | 368, 369 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
371 | 367, 370 | eqtr2i 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
372 | 371 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                          
      |
373 | 366, 372 | syl6eleq 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
       |
374 | | pnfxr 11440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 |
375 | 374 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
376 | 362 | ltpnfd 11451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
377 | 360, 362,
375, 376 | lptioo1 37749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 |
378 | | incom 3636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           |
379 | | ioossre 11724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    |
380 | | df-ss 3429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
              |
381 | 379, 380 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         |
382 | 378, 381 | eqtr2i 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
   |
383 | 382 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
                    |
384 | 377, 383 | syl6eleq 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           
 
     |
385 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
386 | | mnfle 11463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
   |
387 | 159, 386 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  |
388 | | iooss1 11699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       
     |
389 | 363, 387,
388 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         |
390 | 389 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          |
391 | | ioosscn 37628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    |
392 | 390, 391 | syl6ss 3455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
393 | | 0cnd 9661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
394 | 385, 392,
304, 393 | constlimc 37741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
          lim    |
395 | | resabs1 5151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
                        |
396 | 389, 395 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
          
       |
397 | 299, 396 | eqtr4i 2486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
         
           |
398 | 397 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         lim               lim   |
399 | | fssres 5771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                        |
400 | 208, 368,
399 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37

            |
401 | 400 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
              |
402 | 391 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
  
  |
403 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   ℂfld ↾t            ℂfld ↾t          |
404 | | 0le0 10726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
 |
405 | | elioc2 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
        ![(,] (,]](_ioc.gif) 
      |
406 | 159, 67, 405 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    ![(,] (,]](_ioc.gif) 
     |
407 | 67, 164, 404, 406 | mpbir3an 1196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   ![(,] (,]](_ioc.gif)   |
408 | 198 | cnfldtop 21852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
  ℂfld  |
409 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 ![(,] (,]](_ioc.gif)   |
410 | | resttop 20224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
    ℂfld
 ![(,] (,]](_ioc.gif)      ℂfld
↾t
 ![(,] (,]](_ioc.gif)     |
411 | 408, 409,
410 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   ℂfld ↾t  ![(,] (,]](_ioc.gif)    |
412 | 159 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
   |
413 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
     ↾t  ![(,] (,]](_ioc.gif)       
↾t
 ![(,] (,]](_ioc.gif)    |
414 | 387 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
   |
415 | 364, 412,
362, 360, 413, 414, 362 | iocopn 37658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   ![(,] (,]](_ioc.gif)       ↾t  ![(,] (,]](_ioc.gif)     |
416 | 415 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   ![(,] (,]](_ioc.gif)       ↾t  ![(,] (,]](_ioc.gif)    |
417 | 199 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
     ↾t  ![(,] (,]](_ioc.gif)       ℂfld ↾t 
↾t
 ![(,] (,]](_ioc.gif)    |
418 | | iocssre 11742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
   ![(,] (,]](_ioc.gif)    |
419 | 363, 67, 418 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 ![(,] (,]](_ioc.gif)   |
420 | 195 | elexi 3066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 |
421 | | restabs 20229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    ℂfld
 ![(,] (,]](_ioc.gif) 
     ℂfld
↾t 
↾t
 ![(,] (,]](_ioc.gif)      ℂfld
↾t
 ![(,] (,]](_ioc.gif)     |
422 | 408, 419,
420, 421 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
    ℂfld
↾t 
↾t
 ![(,] (,]](_ioc.gif)      ℂfld
↾t
 ![(,] (,]](_ioc.gif)    |
423 | 417, 422 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     ↾t  ![(,] (,]](_ioc.gif)      ℂfld ↾t  ![(,] (,]](_ioc.gif)    |
424 | 416, 423 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   ![(,] (,]](_ioc.gif)     ℂfld
↾t
 ![(,] (,]](_ioc.gif)    |
425 | | isopn3i 20146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     ℂfld
↾t
 ![(,] (,]](_ioc.gif)      ![(,] (,]](_ioc.gif)     ℂfld
↾t
 ![(,] (,]](_ioc.gif)           ℂfld
↾t
 ![(,] (,]](_ioc.gif)         ![(,] (,]](_ioc.gif)      ![(,] (,]](_ioc.gif)    |
426 | 411, 424,
425 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       ℂfld ↾t  ![(,] (,]](_ioc.gif)         ![(,] (,]](_ioc.gif)      ![(,] (,]](_ioc.gif)   |
427 | | mnflt0 11455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 |
428 | | snunioo2 37643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
          ![(,] (,]](_ioc.gif)    |
429 | 363, 151,
427, 428 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
        ![(,] (,]](_ioc.gif)   |
430 | 429 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 ![(,] (,]](_ioc.gif)          |
431 | 430 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   ℂfld ↾t  ![(,] (,]](_ioc.gif)      ℂfld
↾t          |
432 | 431 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
      ℂfld
↾t
 ![(,] (,]](_ioc.gif)          ℂfld
↾t           |
433 | | snunioo2 37643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
                 ![(,] (,]](_ioc.gif)    |
434 | 159, 151,
164, 433 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
            ![(,] (,]](_ioc.gif)   |
435 | 434 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   ![(,] (,]](_ioc.gif)            |
436 | 432, 435 | fveq12i 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       ℂfld ↾t  ![(,] (,]](_ioc.gif)         ![(,] (,]](_ioc.gif)          ℂfld
↾t                       |
437 | 426, 436 | eqtr3i 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   ![(,] (,]](_ioc.gif)         ℂfld
↾t                       |
438 | 407, 437 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       ℂfld
↾t                       |
439 | 438 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       ℂfld
↾t                        |
440 | 401, 390,
402, 198, 403, 439 | limcres 22889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  
          lim   
    lim    |
441 | 440 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             lim        lim   |
442 | 398, 441 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         lim   
    lim   |
443 | 394, 442 | syl6eleq 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       lim    |
444 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             |
445 | | ioosscn 37628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
446 | 445 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      |
447 | 444, 446,
202, 393 | constlimc 37741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       lim    |
448 | | ltpnf 11450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   |
449 | | xrltle 11476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   
   |
450 | 153, 374,
449 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39

  |
451 | 118, 448,
450 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 |
452 | | iooss2 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
           |
453 | 374, 451,
452 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
        |
454 | | resabs1 5151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       
 
         
       |
455 | 453, 454 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
         
      |
456 | 193, 455 | eqtr4i 2486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  |
457 | 456 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       lim    
        
lim   |
458 | | fssres 5771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
            
           |
459 | 208, 379,
458 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
             |
460 | 459 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
  
           |
461 | 453 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         |
462 | | ioosscn 37628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    |
463 | 462 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
464 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   ℂfld ↾t    
       ℂfld
↾t          |
465 | | elico2 11726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       
     |
466 | 67, 153, 465 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    
    |
467 | 67, 404, 68, 466 | mpbir3an 1196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     |
468 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
    |
469 | | resttop 20224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
    ℂfld
  
    ℂfld
↾t       |
470 | 408, 468,
469 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
   ℂfld ↾t      |
471 | 153 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
  |
472 | | eqid 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
     ↾t  
       ↾t  
   |
473 | 451 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
  |
474 | 362, 471,
375, 360, 472, 473 | icoopn 37663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   
   
 ↾t  
    |
475 | 474 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
         ↾t      |
476 | 199 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
     ↾t  
      ℂfld
↾t 
↾t      |
477 | | rge0ssre 11768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    |
478 | | restabs 20229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    ℂfld
        ℂfld
↾t 
↾t        ℂfld
↾t       |
479 | 408, 477,
420, 478 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
    ℂfld
↾t 
↾t        ℂfld
↾t      |
480 | 476, 479 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     ↾t  
     ℂfld ↾t      |
481 | 475, 480 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       ℂfld
↾t      |
482 | | isopn3i 20146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     ℂfld
↾t        
   ℂfld ↾t             ℂfld
↾t                   |
483 | 470, 481,
482 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       ℂfld ↾t                  |
484 | | 0ltpnf 11452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 |
485 | | snunioo1 37650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
  
            |
486 | 151, 374,
484, 485 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
           |
487 | 486 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
      
    |
488 | 487 | oveq2i 6325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
   ℂfld ↾t        ℂfld
↾t          |
489 | 488 | fveq2i 5890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
      ℂfld
↾t            ℂfld
↾t           |
490 | | snunioo1 37650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
       
         |
491 | 151, 153,
68, 490 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
             |
492 | 491 | eqcomi 2470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
             |
493 | 489, 492 | fveq12i 5892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       ℂfld ↾t                    ℂfld
↾t                
     |
494 | 483, 493 | eqtr3i 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
           ℂfld
↾t                
     |
495 | 467, 494 | eleqtri 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
       ℂfld
↾t                
     |
496 | 495 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       ℂfld
↾t                
      |
497 | 460, 461,
463, 198, 464, 496 | limcres 22889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            lim       
lim    |
498 | 497 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
       lim     
  lim
  |
499 | 457, 498 | eqtri 2483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       lim       
lim   |
500 | 447, 499 | syl6eleq 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
  lim
   |
501 | | neg1lt0 10743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  |
502 | 106, 67, 105 | lttri 9785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  

   |
503 | 501, 34, 502 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  |
504 | 106, 503 | ltneii 9772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  |
505 | 504 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
506 | 198, 359,
360, 361, 362, 373, 384, 443, 500, 505 | jumpncnp 37813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        ℂfld      |
507 | 506 | trud 1463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        ℂfld     |
508 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            |
509 | 208 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                |
510 | 205 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            |
511 | | inss2 3664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
      |
512 | 220, 511 | eqsstri 3473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            |
513 | 512 | sseli 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              |
514 | 199, 198 | dvcnp2 22922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
           ℂfld      |
515 | 508, 509,
510, 513, 514 | syl31anc 1279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                  ℂfld      |
516 | 507, 515 | mto 181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          |
517 | 516 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

           |
518 | 358, 517 | eqneltrd 2558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

           |
519 | 518 | necon2ai 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
520 | 519 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          

  |
521 | 354, 355,
357, 520 | leneltd 9814 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          

  |
522 | 344, 163 | sylan 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
      |
523 | | elun2 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  |
524 | 522, 523 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
             |
525 | 353, 521,
524 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . 23
          

             |
526 | 352, 525 | pm2.61dan 805 |
. . . . . . . . . . . . . . . . . . . . . 22
                       |
527 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
528 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
529 | 527, 528 | unipr 4224 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
530 | 526, 529 | syl6eleqr 2550 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
531 | 530 | ssriv 3447 |
. . . . . . . . . . . . . . . . . . . 20
                       |
532 | 531 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
                        |
533 | | ineq2 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                   |
534 | | retop 21830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
535 | | ovex 6342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
536 | 535 | resex 5166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
          |
537 | 536 | dmex 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          |
538 | 534, 537 | pm3.2i 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                |
539 | 318 | ssriv 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
540 | | ssid 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
541 | 301, 539,
540 | 3pm3.2i 1192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
                     |
542 | | restopnb 20239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                         ↾t              |
543 | 538, 541,
542 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
          ↾t             |
544 | 301, 543 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ↾t            |
545 | | inss2 3664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      |
546 | 539, 540 | ssini 3666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      |
547 | 545, 546 | eqssi 3459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                      |
548 | 199 | oveq1i 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     ↾t               ℂfld
↾t 
↾t            |
549 | 331, 343 | sstri 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          |
550 | | restabs 20229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    ℂfld
              ℂfld ↾t  ↾t              ℂfld
↾t             |
551 | 408, 549,
420, 550 | mp3an 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ℂfld
↾t 
↾t              ℂfld
↾t            |
552 | 548, 551 | eqtr2i 2484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ℂfld ↾t                ↾t            |
553 | 544, 547,
552 | 3eltr4i 2552 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   ℂfld ↾t            |
554 | 533, 553 | syl6eqel 2547 |
. . . . . . . . . . . . . . . . . . . . . 22
                    ℂfld ↾t             |
555 | 554 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
                                  ℂfld ↾t             |
556 | | neqne 2642 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
557 | | elprn1 37750 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
      |
558 | 556, 557 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
      |
559 | | ineq2 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
560 | 221 | ssriv 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
              |
561 | | ssid 3462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         |
562 | 197, 560,
561 | 3pm3.2i 1192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                |
563 | | restopnb 20239 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                                                  
↾t              |
564 | 538, 562,
563 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                  ↾t             |
565 | 197, 564 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         ↾t            |
566 | | inss2 3664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    |
567 | 560, 561 | ssini 3666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    |
568 | 566, 567 | eqssi 3459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                    |
569 | 565, 568,
552 | 3eltr4i 2552 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  ℂfld ↾t            |
570 | 559, 569 | syl6eqel 2547 |
. . . . . . . . . . . . . . . . . . . . . 22
     |