Step | Hyp | Ref
| Expression |
1 | | pire 24210 |
. . . . 5
|
2 | 1 | renegcli 10342 |
. . . 4
|
3 | 2 | a1i 11 |
. . 3
|
4 | 1 | a1i 11 |
. . 3
|
5 | | negpilt0 39492 |
. . . . 5
|
6 | | pipos 24212 |
. . . . 5
|
7 | | 0re 10040 |
. . . . . 6
|
8 | 2, 7, 1 | lttri 10163 |
. . . . 5
|
9 | 5, 6, 8 | mp2an 708 |
. . . 4
|
10 | 9 | a1i 11 |
. . 3
|
11 | | fourierdlem94.p |
. . 3
..^ |
12 | | picn 24211 |
. . . . 5
|
13 | 12 | 2timesi 11147 |
. . . 4
|
14 | | fourierdlem94.t |
. . . 4
|
15 | 12, 12 | subnegi 10360 |
. . . 4
|
16 | 13, 14, 15 | 3eqtr4i 2654 |
. . 3
|
17 | | fourierdlem94.m |
. . 3
|
18 | | fourierdlem94.q |
. . 3
|
19 | | ssid 3624 |
. . . 4
|
20 | 19 | a1i 11 |
. . 3
|
21 | | fourierdlem94.f |
. . 3
|
22 | | simp2 1062 |
. . . 4
|
23 | | zre 11381 |
. . . . . 6
|
24 | 23 | 3ad2ant3 1084 |
. . . . 5
|
25 | | 2re 11090 |
. . . . . . . . . 10
|
26 | 25, 1 | remulcli 10054 |
. . . . . . . . 9
|
27 | 26 | a1i 11 |
. . . . . . . 8
|
28 | 14, 27 | syl5eqel 2705 |
. . . . . . 7
|
29 | 28 | adantr 481 |
. . . . . 6
|
30 | 29 | 3adant2 1080 |
. . . . 5
|
31 | 24, 30 | remulcld 10070 |
. . . 4
|
32 | 22, 31 | readdcld 10069 |
. . 3
|
33 | | simp1 1061 |
. . . 4
|
34 | | simp3 1063 |
. . . 4
|
35 | | ax-resscn 9993 |
. . . . . . . . 9
|
36 | 35 | a1i 11 |
. . . . . . . 8
|
37 | 21, 36 | fssd 6057 |
. . . . . . 7
|
38 | 37 | adantr 481 |
. . . . . 6
|
39 | 38 | adantr 481 |
. . . . 5
|
40 | 29 | adantr 481 |
. . . . 5
|
41 | | simplr 792 |
. . . . 5
|
42 | | simpr 477 |
. . . . 5
|
43 | | eleq1 2689 |
. . . . . . . . 9
|
44 | 43 | anbi2d 740 |
. . . . . . . 8
|
45 | | oveq1 6657 |
. . . . . . . . . 10
|
46 | 45 | fveq2d 6195 |
. . . . . . . . 9
|
47 | | fveq2 6191 |
. . . . . . . . 9
|
48 | 46, 47 | eqeq12d 2637 |
. . . . . . . 8
|
49 | 44, 48 | imbi12d 334 |
. . . . . . 7
|
50 | | fourierdlem94.per |
. . . . . . 7
|
51 | 49, 50 | chvarv 2263 |
. . . . . 6
|
52 | 51 | ad4ant14 1293 |
. . . . 5
|
53 | 39, 40, 41, 42, 52 | fperiodmul 39518 |
. . . 4
|
54 | 33, 34, 22, 53 | syl21anc 1325 |
. . 3
|
55 | 35 | a1i 11 |
. . . 4
..^ |
56 | | ioossre 12235 |
. . . . . . . 8
|
57 | 56 | a1i 11 |
. . . . . . 7
|
58 | 21, 57 | fssresd 6071 |
. . . . . 6
|
59 | 58, 36 | fssd 6057 |
. . . . 5
|
60 | 59 | adantr 481 |
. . . 4
..^ |
61 | 56 | a1i 11 |
. . . 4
..^ |
62 | 37 | adantr 481 |
. . . . . . 7
..^ |
63 | 19 | a1i 11 |
. . . . . . 7
..^ |
64 | | eqid 2622 |
. . . . . . . 8
ℂfld ℂfld |
65 | 64 | tgioo2 22606 |
. . . . . . . 8
ℂfld
↾t |
66 | 64, 65 | dvres 23675 |
. . . . . . 7
|
67 | 55, 62, 63, 61, 66 | syl22anc 1327 |
. . . . . 6
..^
|
68 | 67 | dmeqd 5326 |
. . . . 5
..^
|
69 | | ioontr 39736 |
. . . . . . . 8
|
70 | 69 | reseq2i 5393 |
. . . . . . 7
|
71 | 70 | dmeqi 5325 |
. . . . . 6
|
72 | 71 | a1i 11 |
. . . . 5
..^
|
73 | | fourierdlem94.dvcn |
. . . . . 6
..^ |
74 | | cncff 22696 |
. . . . . 6
|
75 | | fdm 6051 |
. . . . . 6
|
76 | 73, 74, 75 | 3syl 18 |
. . . . 5
..^
|
77 | 68, 72, 76 | 3eqtrd 2660 |
. . . 4
..^
|
78 | | dvcn 23684 |
. . . 4
|
79 | 55, 60, 61, 77, 78 | syl31anc 1329 |
. . 3
..^ |
80 | 61, 35 | syl6ss 3615 |
. . . 4
..^ |
81 | 11 | fourierdlem2 40326 |
. . . . . . . . . . . 12
..^ |
82 | 17, 81 | syl 17 |
. . . . . . . . . . 11
..^ |
83 | 18, 82 | mpbid 222 |
. . . . . . . . . 10
..^ |
84 | 83 | simpld 475 |
. . . . . . . . 9
|
85 | | elmapi 7879 |
. . . . . . . . 9
|
86 | 84, 85 | syl 17 |
. . . . . . . 8
|
87 | 86 | adantr 481 |
. . . . . . 7
..^ |
88 | | elfzofz 12485 |
. . . . . . . 8
..^
|
89 | 88 | adantl 482 |
. . . . . . 7
..^ |
90 | 87, 89 | ffvelrnd 6360 |
. . . . . 6
..^ |
91 | 90 | rexrd 10089 |
. . . . 5
..^ |
92 | | fzofzp1 12565 |
. . . . . . 7
..^
|
93 | 92 | adantl 482 |
. . . . . 6
..^ |
94 | 87, 93 | ffvelrnd 6360 |
. . . . 5
..^ |
95 | 83 | simprrd 797 |
. . . . . 6
..^ |
96 | 95 | r19.21bi 2932 |
. . . . 5
..^ |
97 | 64, 91, 94, 96 | lptioo2cn 39877 |
. . . 4
..^ ℂfld |
98 | 58 | adantr 481 |
. . . . 5
..^ |
99 | 36, 37, 20 | dvbss 23665 |
. . . . . . . 8
|
100 | | dvfre 23714 |
. . . . . . . . 9
|
101 | 21, 20, 100 | syl2anc 693 |
. . . . . . . 8
|
102 | 83 | simprd 479 |
. . . . . . . . 9
..^ |
103 | 102 | simplld 791 |
. . . . . . . 8
|
104 | 102 | simplrd 793 |
. . . . . . . 8
|
105 | 73, 74 | syl 17 |
. . . . . . . . 9
..^ |
106 | 94 | rexrd 10089 |
. . . . . . . . . 10
..^ |
107 | 64, 106, 90, 96 | lptioo1cn 39878 |
. . . . . . . . 9
..^ ℂfld |
108 | | fourierdlem94.dvlb |
. . . . . . . . 9
..^ lim |
109 | 105, 80, 107, 108, 64 | ellimciota 39846 |
. . . . . . . 8
..^
lim lim |
110 | | fourierdlem94.dvub |
. . . . . . . . 9
..^ lim |
111 | 105, 80, 97, 110, 64 | ellimciota 39846 |
. . . . . . . 8
..^
lim lim |
112 | 23 | adantl 482 |
. . . . . . . . . . . 12
|
113 | 112, 29 | remulcld 10070 |
. . . . . . . . . . 11
|
114 | 38 | adantr 481 |
. . . . . . . . . . . 12
|
115 | 29 | adantr 481 |
. . . . . . . . . . . 12
|
116 | | simplr 792 |
. . . . . . . . . . . 12
|
117 | | simpr 477 |
. . . . . . . . . . . 12
|
118 | 50 | ad4ant14 1293 |
. . . . . . . . . . . 12
|
119 | 114, 115,
116, 117, 118 | fperiodmul 39518 |
. . . . . . . . . . 11
|
120 | | eqid 2622 |
. . . . . . . . . . 11
|
121 | 38, 113, 119, 120 | fperdvper 40133 |
. . . . . . . . . 10
|
122 | 121 | an32s 846 |
. . . . . . . . 9
|
123 | 122 | simpld 475 |
. . . . . . . 8
|
124 | 122 | simprd 479 |
. . . . . . . 8
|
125 | | fveq2 6191 |
. . . . . . . . . 10
|
126 | | oveq1 6657 |
. . . . . . . . . . 11
|
127 | 126 | fveq2d 6195 |
. . . . . . . . . 10
|
128 | 125, 127 | oveq12d 6668 |
. . . . . . . . 9
|
129 | 128 | cbvmptv 4750 |
. . . . . . . 8
..^ ..^ |
130 | | eqid 2622 |
. . . . . . . 8
|
131 | 99, 101, 3, 4, 10, 16, 17, 86, 103, 104, 73, 109, 111, 123, 124, 129, 130 | fourierdlem71 40394 |
. . . . . . 7
|
132 | 131 | adantr 481 |
. . . . . 6
..^ |
133 | | nfv 1843 |
. . . . . . . . . 10
..^ |
134 | | nfra1 2941 |
. . . . . . . . . 10
|
135 | 133, 134 | nfan 1828 |
. . . . . . . . 9
..^ |
136 | 67, 70 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
..^
|
137 | 136 | fveq1d 6193 |
. . . . . . . . . . . . . 14
..^ |
138 | | fvres 6207 |
. . . . . . . . . . . . . 14
|
139 | 137, 138 | sylan9eq 2676 |
. . . . . . . . . . . . 13
..^ |
140 | 139 | fveq2d 6195 |
. . . . . . . . . . . 12
..^ |
141 | 140 | adantlr 751 |
. . . . . . . . . . 11
..^
|
142 | | simplr 792 |
. . . . . . . . . . . 12
..^
|
143 | | ssdmres 5420 |
. . . . . . . . . . . . . . 15
|
144 | 76, 143 | sylibr 224 |
. . . . . . . . . . . . . 14
..^
|
145 | 144 | ad2antrr 762 |
. . . . . . . . . . . . 13
..^
|
146 | | simpr 477 |
. . . . . . . . . . . . 13
..^
|
147 | 145, 146 | sseldd 3604 |
. . . . . . . . . . . 12
..^
|
148 | | rspa 2930 |
. . . . . . . . . . . 12
|
149 | 142, 147,
148 | syl2anc 693 |
. . . . . . . . . . 11
..^
|
150 | 141, 149 | eqbrtrd 4675 |
. . . . . . . . . 10
..^
|
151 | 150 | ex 450 |
. . . . . . . . 9
..^
|
152 | 135, 151 | ralrimi 2957 |
. . . . . . . 8
..^
|
153 | 152 | ex 450 |
. . . . . . 7
..^ |
154 | 153 | reximdv 3016 |
. . . . . 6
..^ |
155 | 132, 154 | mpd 15 |
. . . . 5
..^ |
156 | 90, 94, 98, 77, 155 | ioodvbdlimc2 40150 |
. . . 4
..^ lim |
157 | 60, 80, 97, 156, 64 | ellimciota 39846 |
. . 3
..^
lim lim |
158 | | fourierdlem94.x |
. . 3
|
159 | | oveq2 6658 |
. . . . . . 7
|
160 | 159 | oveq1d 6665 |
. . . . . 6
|
161 | 160 | fveq2d 6195 |
. . . . 5
|
162 | 161 | oveq1d 6665 |
. . . 4
|
163 | 162 | cbvmptv 4750 |
. . 3
|
164 | | id 22 |
. . . . 5
|
165 | | fveq2 6191 |
. . . . 5
|
166 | 164, 165 | oveq12d 6668 |
. . . 4
|
167 | 166 | cbvmptv 4750 |
. . 3
|
168 | 3, 4, 10, 11, 16, 17, 18, 20, 21, 32, 54, 79, 157, 158, 163, 167 | fourierdlem49 40372 |
. 2
lim |
169 | 90, 94, 98, 77, 155 | ioodvbdlimc1 40148 |
. . . 4
..^ lim |
170 | 60, 80, 107, 169, 64 | ellimciota 39846 |
. . 3
..^
lim lim |
171 | | biid 251 |
. . 3
..^
..^ |
172 | 3, 4, 10, 11, 16, 17, 18, 21, 32, 54, 79, 170, 158, 163, 167, 171 | fourierdlem48 40371 |
. 2
lim
|
173 | 168, 172 | jca 554 |
1
lim lim |