Proof of Theorem fourierdlem85
Step | Hyp | Ref
| Expression |
1 | | fourierdlem85.a |
. . 3
|
2 | | eqid 2622 |
. . . 4
|
3 | | eqid 2622 |
. . . 4
|
4 | | eqid 2622 |
. . . 4
|
5 | | pire 24210 |
. . . . . . . . . . 11
|
6 | 5 | renegcli 10342 |
. . . . . . . . . 10
|
7 | 6 | rexri 10097 |
. . . . . . . . 9
|
8 | 7 | a1i 11 |
. . . . . . . 8
..^ |
9 | 5 | rexri 10097 |
. . . . . . . . 9
|
10 | 9 | a1i 11 |
. . . . . . . 8
..^ |
11 | | fourierdlem85.o |
. . . . . . . . . . 11
..^ |
12 | | fourierdlem85.m |
. . . . . . . . . . 11
|
13 | 5 | a1i 11 |
. . . . . . . . . . . . 13
|
14 | 13 | renegcld 10457 |
. . . . . . . . . . . 12
|
15 | | fourierdlem85.v |
. . . . . . . . . . . . . . . 16
|
16 | | fourierdlem85.p |
. . . . . . . . . . . . . . . . . 18
..^ |
17 | 16 | fourierdlem2 40326 |
. . . . . . . . . . . . . . . . 17
..^ |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
19 | 15, 18 | mpbid 222 |
. . . . . . . . . . . . . . 15
..^ |
20 | 19 | simpld 475 |
. . . . . . . . . . . . . 14
|
21 | | elmapi 7879 |
. . . . . . . . . . . . . 14
|
22 | | frn 6053 |
. . . . . . . . . . . . . 14
|
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . . . . 13
|
24 | | fourierdlem85.x |
. . . . . . . . . . . . 13
|
25 | 23, 24 | sseldd 3604 |
. . . . . . . . . . . 12
|
26 | | fourierdlem85.q |
. . . . . . . . . . . 12
|
27 | 14, 13, 25, 16, 11, 12, 15, 26 | fourierdlem14 40338 |
. . . . . . . . . . 11
|
28 | 11, 12, 27 | fourierdlem15 40339 |
. . . . . . . . . 10
|
29 | 28 | adantr 481 |
. . . . . . . . 9
..^ |
30 | 29 | adantr 481 |
. . . . . . . 8
..^ |
31 | | simplr 792 |
. . . . . . . 8
..^ ..^ |
32 | 8, 10, 30, 31 | fourierdlem8 40332 |
. . . . . . 7
..^ |
33 | | ioossicc 12259 |
. . . . . . . . 9
|
34 | 33 | sseli 3599 |
. . . . . . . 8
|
35 | 34 | adantl 482 |
. . . . . . 7
..^ |
36 | 32, 35 | sseldd 3604 |
. . . . . 6
..^ |
37 | | fourierdlem85.f |
. . . . . . . . . . 11
|
38 | | ioossre 12235 |
. . . . . . . . . . . . . 14
|
39 | 38 | a1i 11 |
. . . . . . . . . . . . 13
|
40 | 37, 39 | fssresd 6071 |
. . . . . . . . . . . 12
|
41 | | ax-resscn 9993 |
. . . . . . . . . . . . 13
|
42 | 39, 41 | syl6ss 3615 |
. . . . . . . . . . . 12
|
43 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
44 | | pnfxr 10092 |
. . . . . . . . . . . . . 14
|
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
|
46 | 25 | ltpnfd 11955 |
. . . . . . . . . . . . 13
|
47 | 43, 45, 25, 46 | lptioo1cn 39878 |
. . . . . . . . . . . 12
ℂfld |
48 | | fourierdlem85.y |
. . . . . . . . . . . 12
lim |
49 | 40, 42, 47, 48 | limcrecl 39861 |
. . . . . . . . . . 11
|
50 | | fourierdlem85.w |
. . . . . . . . . . 11
|
51 | | fourierdlem85.h |
. . . . . . . . . . 11
|
52 | 37, 25, 49, 50, 51 | fourierdlem9 40333 |
. . . . . . . . . 10
|
53 | 41 | a1i 11 |
. . . . . . . . . 10
|
54 | 52, 53 | fssd 6057 |
. . . . . . . . 9
|
55 | 54 | ad2antrr 762 |
. . . . . . . 8
..^ |
56 | 55, 36 | ffvelrnd 6360 |
. . . . . . 7
..^ |
57 | | fourierdlem85.k |
. . . . . . . . . . 11
|
58 | 57 | fourierdlem43 40367 |
. . . . . . . . . 10
|
59 | 58 | a1i 11 |
. . . . . . . . 9
..^ |
60 | 59, 36 | ffvelrnd 6360 |
. . . . . . . 8
..^ |
61 | 60 | recnd 10068 |
. . . . . . 7
..^ |
62 | 56, 61 | mulcld 10060 |
. . . . . 6
..^ |
63 | | fourierdlem85.u |
. . . . . . 7
|
64 | 63 | fvmpt2 6291 |
. . . . . 6
|
65 | 36, 62, 64 | syl2anc 693 |
. . . . 5
..^ |
66 | 65, 62 | eqeltrd 2701 |
. . . 4
..^ |
67 | | fourierdlem85.n |
. . . . . . . . . 10
|
68 | | fourierdlem85.s |
. . . . . . . . . 10
|
69 | 67, 68 | fourierdlem18 40342 |
. . . . . . . . 9
|
70 | | cncff 22696 |
. . . . . . . . 9
|
71 | 69, 70 | syl 17 |
. . . . . . . 8
|
72 | 71 | adantr 481 |
. . . . . . 7
..^ |
73 | 72 | adantr 481 |
. . . . . 6
..^ |
74 | 73, 36 | ffvelrnd 6360 |
. . . . 5
..^ |
75 | 74 | recnd 10068 |
. . . 4
..^ |
76 | | eqid 2622 |
. . . . . 6
|
77 | | eqid 2622 |
. . . . . 6
|
78 | | eqid 2622 |
. . . . . 6
|
79 | | fourierdlem85.r |
. . . . . . . 8
..^ lim |
80 | | fourierdlem85.i |
. . . . . . . 8
|
81 | | fourierdlem85.ifn |
. . . . . . . 8
..^ |
82 | | fourierdlem85.e |
. . . . . . . 8
lim |
83 | | eqid 2622 |
. . . . . . . 8
|
84 | 25, 16, 37, 24, 48, 50, 51, 12, 15, 79, 26, 11, 80, 81, 82, 83 | fourierdlem75 40398 |
. . . . . . 7
..^ lim |
85 | 52 | adantr 481 |
. . . . . . . . 9
..^ |
86 | 7 | a1i 11 |
. . . . . . . . . . 11
..^ |
87 | 9 | a1i 11 |
. . . . . . . . . . 11
..^ |
88 | | simpr 477 |
. . . . . . . . . . 11
..^ ..^ |
89 | 86, 87, 29, 88 | fourierdlem8 40332 |
. . . . . . . . . 10
..^ |
90 | 33, 89 | syl5ss 3614 |
. . . . . . . . 9
..^ |
91 | 85, 90 | feqresmpt 6250 |
. . . . . . . 8
..^ |
92 | 91 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
93 | 84, 92 | eleqtrd 2703 |
. . . . . 6
..^ lim |
94 | | limcresi 23649 |
. . . . . . . 8
lim lim |
95 | | ssid 3624 |
. . . . . . . . . . . 12
|
96 | | cncfss 22702 |
. . . . . . . . . . . 12
|
97 | 41, 95, 96 | mp2an 708 |
. . . . . . . . . . 11
|
98 | 57 | fourierdlem62 40385 |
. . . . . . . . . . 11
|
99 | 97, 98 | sselii 3600 |
. . . . . . . . . 10
|
100 | 99 | a1i 11 |
. . . . . . . . 9
..^ |
101 | | elfzofz 12485 |
. . . . . . . . . . 11
..^
|
102 | 101 | adantl 482 |
. . . . . . . . . 10
..^ |
103 | 29, 102 | ffvelrnd 6360 |
. . . . . . . . 9
..^ |
104 | 100, 103 | cnlimci 23653 |
. . . . . . . 8
..^ lim |
105 | 94, 104 | sseldi 3601 |
. . . . . . 7
..^
lim |
106 | | cncff 22696 |
. . . . . . . . . 10
|
107 | 99, 106 | mp1i 13 |
. . . . . . . . 9
..^ |
108 | 107, 90 | feqresmpt 6250 |
. . . . . . . 8
..^ |
109 | 108 | oveq1d 6665 |
. . . . . . 7
..^ lim lim |
110 | 105, 109 | eleqtrd 2703 |
. . . . . 6
..^ lim |
111 | 76, 77, 78, 56, 61, 93, 110 | mullimc 39848 |
. . . . 5
..^
lim |
112 | 65 | mpteq2dva 4744 |
. . . . . 6
..^ |
113 | 112 | oveq1d 6665 |
. . . . 5
..^ lim lim |
114 | 111, 113 | eleqtrrd 2704 |
. . . 4
..^
lim |
115 | | limcresi 23649 |
. . . . . 6
lim lim |
116 | 69 | adantr 481 |
. . . . . . 7
..^ |
117 | 116, 103 | cnlimci 23653 |
. . . . . 6
..^ lim |
118 | 115, 117 | sseldi 3601 |
. . . . 5
..^
lim |
119 | 72, 90 | feqresmpt 6250 |
. . . . . 6
..^ |
120 | 119 | oveq1d 6665 |
. . . . 5
..^ lim lim |
121 | 118, 120 | eleqtrd 2703 |
. . . 4
..^ lim |
122 | 2, 3, 4, 66, 75, 114, 121 | mullimc 39848 |
. . 3
..^ lim |
123 | 1, 122 | syl5eqel 2705 |
. 2
..^ lim |
124 | | fourierdlem85.g |
. . . . 5
|
125 | 124 | reseq1i 5392 |
. . . 4
|
126 | 90 | resmptd 5452 |
. . . 4
..^ |
127 | 125, 126 | syl5req 2669 |
. . 3
..^ |
128 | 127 | oveq1d 6665 |
. 2
..^ lim lim |
129 | 123, 128 | eleqtrd 2703 |
1
..^ lim |