Step | Hyp | Ref
| Expression |
1 | | fourierdlem76.ch |
. . 3
β’ (π β (((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1))))) |
2 | | eqid 2737 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / π )) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / π )) |
3 | | eqid 2737 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / (2 Β· (sinβ(π / 2))))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / (2 Β· (sinβ(π / 2))))) |
4 | | eqid 2737 |
. . . . 5
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) |
5 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β π) |
6 | 1, 5 | sylbi 216 |
. . . . . . . . . 10
β’ (π β π) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π) |
8 | | ioossicc 13357 |
. . . . . . . . . 10
β’ (π΄(,)π΅) β (π΄[,]π΅) |
9 | | fourierdlem76.a |
. . . . . . . . . . . . . 14
β’ (π β π΄ β β) |
10 | 9 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ (π β π΄ β
β*) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΄ β
β*) |
12 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΄ β
β*) |
13 | | fourierdlem76.b |
. . . . . . . . . . . . . 14
β’ (π β π΅ β β) |
14 | 13 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ (π β π΅ β
β*) |
15 | 6, 14 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π΅ β
β*) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΅ β
β*) |
17 | | elioore 13301 |
. . . . . . . . . . . 12
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
18 | 17 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
19 | 6, 9 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΄ β β) |
21 | | fourierdlem76.t |
. . . . . . . . . . . . . . . . . . 19
β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) |
22 | | prfi 9273 |
. . . . . . . . . . . . . . . . . . . . 21
β’ {π΄, π΅} β Fin |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π΄, π΅} β Fin) |
24 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β Fin) |
25 | | fourierdlem76.q |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
26 | 25 | rnmptfi 43462 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((0...π) β Fin
β ran π β
Fin) |
27 | | infi 9219 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (ran
π β Fin β (ran
π β© (π΄(,)π΅)) β Fin) |
28 | 24, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ran π β© (π΄(,)π΅)) β Fin) |
29 | | unfi 9123 |
. . . . . . . . . . . . . . . . . . . 20
β’ (({π΄, π΅} β Fin β§ (ran π β© (π΄(,)π΅)) β Fin) β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) β Fin) |
30 | 23, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) β Fin) |
31 | 21, 30 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β Fin) |
32 | | prssg 4784 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β β β§ π΅ β β) β {π΄, π΅} β β)) |
33 | 9, 13, 32 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π΄ β β β§ π΅ β β) β {π΄, π΅} β β)) |
34 | 9, 13, 33 | mpbi2and 711 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π΄, π΅} β β) |
35 | | inss2 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (ran
π β© (π΄(,)π΅)) β (π΄(,)π΅) |
36 | | ioossre 13332 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄(,)π΅) β β |
37 | 35, 36 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (ran
π β© (π΄(,)π΅)) β β |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ran π β© (π΄(,)π΅)) β β) |
39 | 34, 38 | unssd 4151 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) β β) |
40 | 21, 39 | eqsstrid 3997 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
41 | | fourierdlem76.s |
. . . . . . . . . . . . . . . . . 18
β’ π = (β©ππ Isom < , < ((0...π), π)) |
42 | | fourierdlem76.n |
. . . . . . . . . . . . . . . . . 18
β’ π = ((β―βπ) β 1) |
43 | 31, 40, 41, 42 | fourierdlem36 44458 |
. . . . . . . . . . . . . . . . 17
β’ (π β π Isom < , < ((0...π), π)) |
44 | 6, 43 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π Isom < , < ((0...π), π)) |
45 | | isof1o 7273 |
. . . . . . . . . . . . . . . 16
β’ (π Isom < , < ((0...π), π) β π:(0...π)β1-1-ontoβπ) |
46 | | f1of 6789 |
. . . . . . . . . . . . . . . 16
β’ (π:(0...π)β1-1-ontoβπ β π:(0...π)βΆπ) |
47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆπ) |
48 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
49 | 47, 48 | fssd 6691 |
. . . . . . . . . . . . . 14
β’ (π β π:(0...π)βΆβ) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π:(0...π)βΆβ) |
51 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β π β (0..^π)) |
52 | 1, 51 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β π β (0..^π)) |
53 | | elfzofz 13595 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β π β (0...π)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β (0...π)) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (0...π)) |
56 | 50, 55 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
57 | 43, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π:(0...π)βΆπ) |
58 | | frn 6680 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(0...π)βΆπ β ran π β π) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ran π β π) |
60 | 9 | leidd 11728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ β€ π΄) |
61 | | fourierdlem76.altb |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΄ < π΅) |
62 | 9, 13, 61 | ltled 11310 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ β€ π΅) |
63 | 9, 13, 9, 60, 62 | eliccd 43816 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β (π΄[,]π΅)) |
64 | 13 | leidd 11728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΅ β€ π΅) |
65 | 9, 13, 13, 62, 64 | eliccd 43816 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅ β (π΄[,]π΅)) |
66 | | prssg 4784 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β (π΄[,]π΅) β§ π΅ β (π΄[,]π΅)) β {π΄, π΅} β (π΄[,]π΅))) |
67 | 9, 13, 66 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π΄ β (π΄[,]π΅) β§ π΅ β (π΄[,]π΅)) β {π΄, π΅} β (π΄[,]π΅))) |
68 | 63, 65, 67 | mpbi2and 711 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π΄, π΅} β (π΄[,]π΅)) |
69 | 35, 8 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . 20
β’ (ran
π β© (π΄(,)π΅)) β (π΄[,]π΅) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (ran π β© (π΄(,)π΅)) β (π΄[,]π΅)) |
71 | 68, 70 | unssd 4151 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) β (π΄[,]π΅)) |
72 | 21, 71 | eqsstrid 3997 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (π΄[,]π΅)) |
73 | 59, 72 | sstrd 3959 |
. . . . . . . . . . . . . . . 16
β’ (π β ran π β (π΄[,]π΅)) |
74 | 6, 73 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ran π β (π΄[,]π΅)) |
75 | | ffun 6676 |
. . . . . . . . . . . . . . . . 17
β’ (π:(0...π)βΆβ β Fun π) |
76 | 49, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β Fun π) |
77 | | fdm 6682 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:(0...π)βΆβ β dom π = (0...π)) |
78 | 49, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom π = (0...π)) |
79 | 78 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) = dom π) |
80 | 54, 79 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
β’ (π β π β dom π) |
81 | | fvelrn 7032 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
π β§ π β dom π) β (πβπ) β ran π) |
82 | 76, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) β ran π) |
83 | 74, 82 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) β (π΄[,]π΅)) |
84 | | iccgelb 13327 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πβπ) β (π΄[,]π΅)) β π΄ β€ (πβπ)) |
85 | 11, 15, 83, 84 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β π΄ β€ (πβπ)) |
86 | 85 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΄ β€ (πβπ)) |
87 | 56 | rexrd 11212 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
88 | | fzofzp1 13676 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β (π + 1) β (0...π)) |
89 | 52, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + 1) β (0...π)) |
90 | 49, 89 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π + 1)) β β) |
91 | 90 | rexrd 11212 |
. . . . . . . . . . . . . 14
β’ (π β (πβ(π + 1)) β
β*) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
93 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)(,)(πβ(π + 1)))) |
94 | | ioogtlb 43807 |
. . . . . . . . . . . . 13
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
95 | 87, 92, 93, 94 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
96 | 20, 56, 18, 86, 95 | lelttrd 11320 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΄ < π ) |
97 | 90 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
98 | 6, 13 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
99 | 98 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π΅ β β) |
100 | | iooltub 43822 |
. . . . . . . . . . . . 13
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
101 | 87, 92, 93, 100 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
102 | 89, 79 | eleqtrd 2840 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + 1) β dom π) |
103 | | fvelrn 7032 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
π β§ (π + 1) β dom π) β (πβ(π + 1)) β ran π) |
104 | 76, 102, 103 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π + 1)) β ran π) |
105 | 74, 104 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ (π β (πβ(π + 1)) β (π΄[,]π΅)) |
106 | | iccleub 13326 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πβ(π + 1)) β (π΄[,]π΅)) β (πβ(π + 1)) β€ π΅) |
107 | 11, 15, 105, 106 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (πβ(π + 1)) β€ π΅) |
108 | 107 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β€ π΅) |
109 | 18, 97, 99, 101, 108 | ltletrd 11322 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < π΅) |
110 | 12, 16, 18, 96, 109 | eliood 43810 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (π΄(,)π΅)) |
111 | 8, 110 | sselid 3947 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (π΄[,]π΅)) |
112 | | fourierdlem76.f |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
113 | 112 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄[,]π΅)) β πΉ:ββΆβ) |
114 | | fourierdlem76.xre |
. . . . . . . . . . . 12
β’ (π β π β β) |
115 | 114 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
116 | 9, 13 | iccssred 13358 |
. . . . . . . . . . . 12
β’ (π β (π΄[,]π΅) β β) |
117 | 116 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΄[,]π΅)) β π β β) |
118 | 115, 117 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄[,]π΅)) β (π + π ) β β) |
119 | 113, 118 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (π΄[,]π΅)) β (πΉβ(π + π )) β β) |
120 | 7, 111, 119 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
121 | 120 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
122 | | fourierdlem76.c |
. . . . . . . . . 10
β’ (π β πΆ β β) |
123 | 122 | recnd 11190 |
. . . . . . . . 9
β’ (π β πΆ β β) |
124 | 6, 123 | syl 17 |
. . . . . . . 8
β’ (π β πΆ β β) |
125 | 124 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β πΆ β β) |
126 | 121, 125 | subcld 11519 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) β πΆ) β β) |
127 | | ioossre 13332 |
. . . . . . . . 9
β’ ((πβπ)(,)(πβ(π + 1))) β β |
128 | 127 | a1i 11 |
. . . . . . . 8
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
129 | 128 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
130 | 129 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
131 | | nne 2948 |
. . . . . . . . . . . 12
β’ (Β¬
π β 0 β π = 0) |
132 | 131 | biimpi 215 |
. . . . . . . . . . 11
β’ (Β¬
π β 0 β π = 0) |
133 | 132 | eqcomd 2743 |
. . . . . . . . . 10
β’ (Β¬
π β 0 β 0 = π ) |
134 | 133 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β (π΄[,]π΅)) β§ Β¬ π β 0) β 0 = π ) |
135 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β (π΄[,]π΅)) β π β (π΄[,]π΅)) |
136 | 135 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (π΄[,]π΅)) β§ Β¬ π β 0) β π β (π΄[,]π΅)) |
137 | 134, 136 | eqeltrd 2838 |
. . . . . . . 8
β’ (((π β§ π β (π΄[,]π΅)) β§ Β¬ π β 0) β 0 β (π΄[,]π΅)) |
138 | | fourierdlem76.n0 |
. . . . . . . . 9
β’ (π β Β¬ 0 β (π΄[,]π΅)) |
139 | 138 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (π΄[,]π΅)) β§ Β¬ π β 0) β Β¬ 0 β (π΄[,]π΅)) |
140 | 137, 139 | condan 817 |
. . . . . . 7
β’ ((π β§ π β (π΄[,]π΅)) β π β 0) |
141 | 7, 111, 140 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β 0) |
142 | 126, 130,
141 | divcld 11938 |
. . . . 5
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((πΉβ(π + π )) β πΆ) / π ) β β) |
143 | | 2cnd 12238 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β 2 β
β) |
144 | 130 | halfcld 12405 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π / 2) β β) |
145 | 144 | sincld 16019 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (sinβ(π / 2)) β
β) |
146 | 143, 145 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (2 Β· (sinβ(π / 2))) β
β) |
147 | 17 | recnd 11190 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
148 | 147 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
149 | 148 | halfcld 12405 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π / 2) β β) |
150 | 149 | sincld 16019 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (sinβ(π / 2)) β
β) |
151 | | 2ne0 12264 |
. . . . . . . 8
β’ 2 β
0 |
152 | 151 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β 2 β 0) |
153 | | fourierdlem76.ab |
. . . . . . . . . . 11
β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) |
154 | 6, 153 | syl 17 |
. . . . . . . . . 10
β’ (π β (π΄[,]π΅) β (-Ο[,]Ο)) |
155 | 154 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π΄[,]π΅) β (-Ο[,]Ο)) |
156 | 155, 111 | sseldd 3950 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (-Ο[,]Ο)) |
157 | | fourierdlem44 44466 |
. . . . . . . 8
β’ ((π β (-Ο[,]Ο) β§
π β 0) β
(sinβ(π / 2)) β
0) |
158 | 156, 141,
157 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (sinβ(π / 2)) β 0) |
159 | 143, 150,
152, 158 | mulne0d 11814 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (2 Β· (sinβ(π / 2))) β 0) |
160 | 130, 146,
159 | divcld 11938 |
. . . . 5
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π / (2 Β· (sinβ(π / 2)))) β β) |
161 | | eqid 2737 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β πΆ)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β πΆ)) |
162 | | eqid 2737 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) |
163 | 141 | neneqd 2949 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π = 0) |
164 | | velsn 4607 |
. . . . . . . 8
β’ (π β {0} β π = 0) |
165 | 163, 164 | sylnibr 329 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ π β {0}) |
166 | 130, 165 | eldifd 3926 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (β β
{0})) |
167 | | eqid 2737 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) |
168 | | eqid 2737 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ πΆ) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ πΆ) |
169 | | elfzofz 13595 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β π β (0...π)) |
170 | 169 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
171 | | pire 25831 |
. . . . . . . . . . . . . . . . . . . . 21
β’ Ο
β β |
172 | 171 | renegcli 11469 |
. . . . . . . . . . . . . . . . . . . 20
β’ -Ο
β β |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β -Ο β
β) |
174 | 173, 114 | readdcld 11191 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (-Ο + π) β β) |
175 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Ο β
β) |
176 | 175, 114 | readdcld 11191 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Ο + π) β β) |
177 | 174, 176 | iccssred 13358 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((-Ο + π)[,](Ο + π)) β β) |
178 | 177 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((-Ο + π)[,](Ο + π)) β β) |
179 | | fourierdlem76.p |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
180 | | fourierdlem76.m |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
181 | | fourierdlem76.v |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (πβπ)) |
182 | 179, 180,
181 | fourierdlem15 44437 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π:(0...π)βΆ((-Ο + π)[,](Ο + π))) |
183 | 182 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ((-Ο + π)[,](Ο + π))) |
184 | 183, 170 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) β ((-Ο + π)[,](Ο + π))) |
185 | 178, 184 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
186 | 114 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β β) |
187 | 185, 186 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) β β) |
188 | 25 | fvmpt2 6964 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π) β§ ((πβπ) β π) β β) β (πβπ) = ((πβπ) β π)) |
189 | 170, 187,
188 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) = ((πβπ) β π)) |
190 | 189, 187 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
191 | 190 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (πβπ) β β) |
192 | 191 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
193 | 1, 192 | sylbi 216 |
. . . . . . . . 9
β’ (π β (πβπ) β β) |
194 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
195 | 194 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
196 | 195 | cbvmptv 5223 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
197 | 25, 196 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
198 | 197 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π = (π β (0...π) β¦ ((πβπ) β π))) |
199 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
200 | 199 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
201 | 200 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
202 | | fzofzp1 13676 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β (π + 1) β (0...π)) |
203 | 202 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
204 | 183, 203 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β ((-Ο + π)[,](Ο + π))) |
205 | 178, 204 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
206 | 205, 186 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β π) β β) |
207 | 198, 201,
203, 206 | fvmptd 6960 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
208 | 207, 206 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
209 | 208 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (πβ(π + 1)) β β) |
210 | 209 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
211 | 1, 210 | sylbi 216 |
. . . . . . . . 9
β’ (π β (πβ(π + 1)) β β) |
212 | 179 | fourierdlem2 44424 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
213 | 180, 212 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
214 | 181, 213 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο + π) β§ (πβπ) = (Ο + π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
215 | 214 | simprrd 773 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
216 | 215 | r19.21bi 3237 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
217 | 185, 205,
186, 216 | ltsub1dd 11774 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) < ((πβ(π + 1)) β π)) |
218 | 217, 189,
207 | 3brtr4d 5142 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
219 | 218 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
220 | 219 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (πβ(π + 1))) |
221 | 1, 220 | sylbi 216 |
. . . . . . . . 9
β’ (π β (πβπ) < (πβ(π + 1))) |
222 | 1 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1))))) |
223 | 222 | simplrd 769 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (0..^π)) |
224 | 6, 223, 185 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβπ) β β) |
225 | 224 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) β
β*) |
226 | 225 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
227 | 6, 223, 205 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ(π + 1)) β β) |
228 | 227 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ(π + 1)) β
β*) |
229 | 228 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
230 | 6, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
231 | 230 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
232 | | elioore 13301 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
233 | 232 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
234 | 231, 233 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
235 | 6, 223, 189 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβπ) = ((πβπ) β π)) |
236 | 235 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + (πβπ)) = (π + ((πβπ) β π))) |
237 | 230 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
238 | 224 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβπ) β β) |
239 | 237, 238 | pncan3d 11522 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + ((πβπ) β π)) = (πβπ)) |
240 | 236, 239 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβπ) = (π + (πβπ))) |
241 | 240 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
242 | 193 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
243 | 193 | rexrd 11212 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβπ) β
β*) |
244 | 243 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
245 | 211 | rexrd 11212 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβ(π + 1)) β
β*) |
246 | 245 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
247 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)(,)(πβ(π + 1)))) |
248 | | ioogtlb 43807 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
249 | 244, 246,
247, 248 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
250 | 242, 233,
231, 249 | ltadd2dd 11321 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π )) |
251 | 241, 250 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )) |
252 | 211 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
253 | | iooltub 43822 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
254 | 244, 246,
247, 253 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
255 | 233, 252,
231, 254 | ltadd2dd 11321 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (π + (πβ(π + 1)))) |
256 | 6, 223, 207 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
257 | 256 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + (πβ(π + 1))) = (π + ((πβ(π + 1)) β π))) |
258 | 227 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβ(π + 1)) β β) |
259 | 237, 258 | pncan3d 11522 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + ((πβ(π + 1)) β π)) = (πβ(π + 1))) |
260 | 257, 259 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + (πβ(π + 1))) = (πβ(π + 1))) |
261 | 260 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
262 | 255, 261 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
263 | 226, 229,
234, 251, 262 | eliood 43810 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β ((πβπ)(,)(πβ(π + 1)))) |
264 | | fvres 6866 |
. . . . . . . . . . . . 13
β’ ((π + π ) β ((πβπ)(,)(πβ(π + 1))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
265 | 263, 264 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )) = (πΉβ(π + π ))) |
266 | 265 | eqcomd 2743 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) |
267 | 266 | mpteq2dva 5210 |
. . . . . . . . . 10
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )))) |
268 | | ioosscn 13333 |
. . . . . . . . . . . 12
β’ ((πβπ)(,)(πβ(π + 1))) β β |
269 | 268 | a1i 11 |
. . . . . . . . . . 11
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
270 | | fourierdlem76.fcn |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
271 | 6, 223, 270 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
272 | | ioosscn 13333 |
. . . . . . . . . . . 12
β’ ((πβπ)(,)(πβ(π + 1))) β β |
273 | 272 | a1i 11 |
. . . . . . . . . . 11
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
274 | 269, 271,
273, 237, 263 | fourierdlem23 44445 |
. . . . . . . . . 10
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
275 | 267, 274 | eqeltrd 2838 |
. . . . . . . . 9
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
276 | 6, 112 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
277 | | ioossre 13332 |
. . . . . . . . . . 11
β’ ((πβπ)(,)(πβ(π + 1))) β β |
278 | 277 | a1i 11 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
279 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) |
280 | | ioossre 13332 |
. . . . . . . . . . 11
β’ ((πβπ)(,)(πβ(π + 1))) β β |
281 | 280 | a1i 11 |
. . . . . . . . . 10
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
282 | 233, 254 | ltned 11298 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (πβ(π + 1))) |
283 | | fourierdlem76.l |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
284 | 6, 223, 283 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
285 | 260 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (π β (πβ(π + 1)) = (π + (πβ(π + 1)))) |
286 | 285 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβ(π + 1))))) |
287 | 284, 286 | eleqtrd 2840 |
. . . . . . . . . 10
β’ (π β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβ(π + 1))))) |
288 | 211 | recnd 11190 |
. . . . . . . . . 10
β’ (π β (πβ(π + 1)) β β) |
289 | 276, 230,
278, 279, 263, 281, 282, 287, 288 | fourierdlem53 44474 |
. . . . . . . . 9
β’ (π β πΏ β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβ(π + 1)))) |
290 | 49, 54 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (π β (πβπ) β β) |
291 | | elfzoelz 13579 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β π β β€) |
292 | | zre 12510 |
. . . . . . . . . . . 12
β’ (π β β€ β π β
β) |
293 | 52, 291, 292 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β π β β) |
294 | 293 | ltp1d 12092 |
. . . . . . . . . 10
β’ (π β π < (π + 1)) |
295 | | isorel 7276 |
. . . . . . . . . . 11
β’ ((π Isom < , < ((0...π), π) β§ (π β (0...π) β§ (π + 1) β (0...π))) β (π < (π + 1) β (πβπ) < (πβ(π + 1)))) |
296 | 44, 54, 89, 295 | syl12anc 836 |
. . . . . . . . . 10
β’ (π β (π < (π + 1) β (πβπ) < (πβ(π + 1)))) |
297 | 294, 296 | mpbid 231 |
. . . . . . . . 9
β’ (π β (πβπ) < (πβ(π + 1))) |
298 | 1 | simprbi 498 |
. . . . . . . . 9
β’ (π β ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) |
299 | | eqid 2737 |
. . . . . . . . 9
β’ if((πβ(π + 1)) = (πβ(π + 1)), πΏ, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβ(π + 1)))) = if((πβ(π + 1)) = (πβ(π + 1)), πΏ, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβ(π + 1)))) |
300 | | eqid 2737 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt (((πβπ)(,)(πβ(π + 1))) βͺ {(πβ(π + 1))})) =
((TopOpenββfld) βΎt (((πβπ)(,)(πβ(π + 1))) βͺ {(πβ(π + 1))})) |
301 | 193, 211,
221, 275, 289, 290, 90, 297, 298, 299, 300 | fourierdlem33 44455 |
. . . . . . . 8
β’ (π β if((πβ(π + 1)) = (πβ(π + 1)), πΏ, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβ(π + 1)))) β (((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
302 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))) |
303 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β§ π = (πβ(π + 1))) β π = (πβ(π + 1))) |
304 | 303 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β§ π = (πβ(π + 1))) β (π + π ) = (π + (πβ(π + 1)))) |
305 | 304 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β§ π = (πβ(π + 1))) β (πΉβ(π + π )) = (πΉβ(π + (πβ(π + 1))))) |
306 | 243 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβπ) β
β*) |
307 | 245 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β
β*) |
308 | 90 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β β) |
309 | 193, 211,
290, 90, 297, 298 | fourierdlem10 44432 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ) β€ (πβπ) β§ (πβ(π + 1)) β€ (πβ(π + 1)))) |
310 | 309 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β (πβπ) β€ (πβπ)) |
311 | 193, 290,
90, 310, 297 | lelttrd 11320 |
. . . . . . . . . . . 12
β’ (π β (πβπ) < (πβ(π + 1))) |
312 | 311 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβπ) < (πβ(π + 1))) |
313 | 211 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β β) |
314 | 309 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β (πβ(π + 1)) β€ (πβ(π + 1))) |
315 | 314 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β€ (πβ(π + 1))) |
316 | | neqne 2952 |
. . . . . . . . . . . . . 14
β’ (Β¬
(πβ(π + 1)) = (πβ(π + 1)) β (πβ(π + 1)) β (πβ(π + 1))) |
317 | 316 | necomd 3000 |
. . . . . . . . . . . . 13
β’ (Β¬
(πβ(π + 1)) = (πβ(π + 1)) β (πβ(π + 1)) β (πβ(π + 1))) |
318 | 317 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β (πβ(π + 1))) |
319 | 308, 313,
315, 318 | leneltd 11316 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) < (πβ(π + 1))) |
320 | 306, 307,
308, 312, 319 | eliood 43810 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πβ(π + 1)) β ((πβπ)(,)(πβ(π + 1)))) |
321 | 230, 90 | readdcld 11191 |
. . . . . . . . . . . 12
β’ (π β (π + (πβ(π + 1))) β β) |
322 | 276, 321 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ (π β (πΉβ(π + (πβ(π + 1)))) β β) |
323 | 322 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β (πΉβ(π + (πβ(π + 1)))) β β) |
324 | 302, 305,
320, 323 | fvmptd 6960 |
. . . . . . . . 9
β’ ((π β§ Β¬ (πβ(π + 1)) = (πβ(π + 1))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβ(π + 1))) = (πΉβ(π + (πβ(π + 1))))) |
325 | 324 | ifeq2da 4523 |
. . . . . . . 8
β’ (π β if((πβ(π + 1)) = (πβ(π + 1)), πΏ, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβ(π + 1)))) = if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1)))))) |
326 | 298 | resmptd 5999 |
. . . . . . . . 9
β’ (π β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))) |
327 | 326 | oveq1d 7377 |
. . . . . . . 8
β’ (π β (((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβ(π + 1)))) |
328 | 301, 325,
327 | 3eltr3d 2852 |
. . . . . . 7
β’ (π β if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβ(π + 1)))) |
329 | | ax-resscn 11115 |
. . . . . . . . 9
β’ β
β β |
330 | 128, 329 | sstrdi 3961 |
. . . . . . . 8
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
331 | 90 | recnd 11190 |
. . . . . . . 8
β’ (π β (πβ(π + 1)) β β) |
332 | 168, 330,
124, 331 | constlimc 43939 |
. . . . . . 7
β’ (π β πΆ β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ πΆ) limβ (πβ(π + 1)))) |
333 | 167, 168,
161, 121, 125, 328, 332 | sublimc 43967 |
. . . . . 6
β’ (π β (if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β πΆ)) limβ (πβ(π + 1)))) |
334 | 330, 162,
331 | idlimc 43941 |
. . . . . 6
β’ (π β (πβ(π + 1)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) limβ (πβ(π + 1)))) |
335 | 6, 105 | jca 513 |
. . . . . . 7
β’ (π β (π β§ (πβ(π + 1)) β (π΄[,]π΅))) |
336 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = (πβ(π + 1)) β (π β (π΄[,]π΅) β (πβ(π + 1)) β (π΄[,]π΅))) |
337 | 336 | anbi2d 630 |
. . . . . . . . 9
β’ (π = (πβ(π + 1)) β ((π β§ π β (π΄[,]π΅)) β (π β§ (πβ(π + 1)) β (π΄[,]π΅)))) |
338 | | neeq1 3007 |
. . . . . . . . 9
β’ (π = (πβ(π + 1)) β (π β 0 β (πβ(π + 1)) β 0)) |
339 | 337, 338 | imbi12d 345 |
. . . . . . . 8
β’ (π = (πβ(π + 1)) β (((π β§ π β (π΄[,]π΅)) β π β 0) β ((π β§ (πβ(π + 1)) β (π΄[,]π΅)) β (πβ(π + 1)) β 0))) |
340 | 339, 140 | vtoclg 3528 |
. . . . . . 7
β’ ((πβ(π + 1)) β β β ((π β§ (πβ(π + 1)) β (π΄[,]π΅)) β (πβ(π + 1)) β 0)) |
341 | 90, 335, 340 | sylc 65 |
. . . . . 6
β’ (π β (πβ(π + 1)) β 0) |
342 | 161, 162,
2, 126, 166, 333, 334, 341, 141 | divlimc 43971 |
. . . . 5
β’ (π β ((if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / π )) limβ (πβ(π + 1)))) |
343 | | eqid 2737 |
. . . . . 6
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) |
344 | 143, 150 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (2 Β· (sinβ(π / 2))) β
β) |
345 | 159 | neneqd 2949 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ (2 Β·
(sinβ(π / 2))) =
0) |
346 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
347 | 346 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β 2 β
β) |
348 | 17 | rehalfcld 12407 |
. . . . . . . . . . . 12
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (π / 2) β β) |
349 | 348 | resincld 16032 |
. . . . . . . . . . 11
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (sinβ(π / 2)) β β) |
350 | 349 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (sinβ(π / 2)) β
β) |
351 | 347, 350 | remulcld 11192 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (2 Β· (sinβ(π / 2))) β
β) |
352 | | elsng 4605 |
. . . . . . . . 9
β’ ((2
Β· (sinβ(π /
2))) β β β ((2 Β· (sinβ(π / 2))) β {0} β (2 Β·
(sinβ(π / 2))) =
0)) |
353 | 351, 352 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((2 Β·
(sinβ(π / 2))) β
{0} β (2 Β· (sinβ(π / 2))) = 0)) |
354 | 345, 353 | mtbird 325 |
. . . . . . 7
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β Β¬ (2 Β·
(sinβ(π / 2))) β
{0}) |
355 | 344, 354 | eldifd 3926 |
. . . . . 6
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (2 Β· (sinβ(π / 2))) β (β β
{0})) |
356 | | eqid 2737 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) |
357 | | eqid 2737 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (sinβ(π / 2))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (sinβ(π / 2))) |
358 | | 2cnd 12238 |
. . . . . . . 8
β’ (π β 2 β
β) |
359 | 356, 330,
358, 331 | constlimc 43939 |
. . . . . . 7
β’ (π β 2 β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) limβ
(πβ(π + 1)))) |
360 | 348 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπ)(,)(πβ(π + 1))) β§ (π / 2) β ((πβ(π + 1)) / 2))) β (π / 2) β β) |
361 | | recn 11148 |
. . . . . . . . . 10
β’ (π₯ β β β π₯ β
β) |
362 | 361 | sincld 16019 |
. . . . . . . . 9
β’ (π₯ β β β
(sinβπ₯) β
β) |
363 | 362 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (sinβπ₯) β
β) |
364 | | eqid 2737 |
. . . . . . . . 9
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / 2)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / 2)) |
365 | | 2cn 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
366 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ (2 β
(β β {0}) β (2 β β β§ 2 β
0)) |
367 | 365, 151,
366 | mpbir2an 710 |
. . . . . . . . . 10
β’ 2 β
(β β {0}) |
368 | 367 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β 2 β (β β
{0})) |
369 | 151 | a1i 11 |
. . . . . . . . 9
β’ (π β 2 β 0) |
370 | 162, 356,
364, 148, 368, 334, 359, 369, 152 | divlimc 43971 |
. . . . . . . 8
β’ (π β ((πβ(π + 1)) / 2) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / 2)) limβ (πβ(π + 1)))) |
371 | | sinf 16013 |
. . . . . . . . . . . . . 14
β’
sin:ββΆβ |
372 | 371 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β sin:ββΆβ) |
373 | 329 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β β β β) |
374 | 372, 373 | feqresmpt 6916 |
. . . . . . . . . . . 12
β’ (β€
β (sin βΎ β) = (π₯ β β β¦ (sinβπ₯))) |
375 | 374 | mptru 1549 |
. . . . . . . . . . 11
β’ (sin
βΎ β) = (π₯
β β β¦ (sinβπ₯)) |
376 | | resincncf 44190 |
. . . . . . . . . . 11
β’ (sin
βΎ β) β (ββcnββ) |
377 | 375, 376 | eqeltrri 2835 |
. . . . . . . . . 10
β’ (π₯ β β β¦
(sinβπ₯)) β
(ββcnββ) |
378 | 377 | a1i 11 |
. . . . . . . . 9
β’ (π β (π₯ β β β¦ (sinβπ₯)) β (ββcnββ)) |
379 | 90 | rehalfcld 12407 |
. . . . . . . . 9
β’ (π β ((πβ(π + 1)) / 2) β β) |
380 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = ((πβ(π + 1)) / 2) β (sinβπ₯) = (sinβ((πβ(π + 1)) / 2))) |
381 | 378, 379,
380 | cnmptlimc 25270 |
. . . . . . . 8
β’ (π β (sinβ((πβ(π + 1)) / 2)) β ((π₯ β β β¦ (sinβπ₯)) limβ ((πβ(π + 1)) / 2))) |
382 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = (π / 2) β (sinβπ₯) = (sinβ(π / 2))) |
383 | | fveq2 6847 |
. . . . . . . . 9
β’ ((π / 2) = ((πβ(π + 1)) / 2) β (sinβ(π / 2)) = (sinβ((πβ(π + 1)) / 2))) |
384 | 383 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπ)(,)(πβ(π + 1))) β§ (π / 2) = ((πβ(π + 1)) / 2))) β (sinβ(π / 2)) = (sinβ((πβ(π + 1)) / 2))) |
385 | 360, 363,
370, 381, 382, 384 | limcco 25273 |
. . . . . . 7
β’ (π β (sinβ((πβ(π + 1)) / 2)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (sinβ(π / 2))) limβ
(πβ(π + 1)))) |
386 | 356, 357,
343, 143, 150, 359, 385 | mullimc 43931 |
. . . . . 6
β’ (π β (2 Β·
(sinβ((πβ(π + 1)) / 2))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) limβ
(πβ(π + 1)))) |
387 | 331 | halfcld 12405 |
. . . . . . . 8
β’ (π β ((πβ(π + 1)) / 2) β β) |
388 | 387 | sincld 16019 |
. . . . . . 7
β’ (π β (sinβ((πβ(π + 1)) / 2)) β β) |
389 | 154, 105 | sseldd 3950 |
. . . . . . . 8
β’ (π β (πβ(π + 1)) β
(-Ο[,]Ο)) |
390 | | fourierdlem44 44466 |
. . . . . . . 8
β’ (((πβ(π + 1)) β (-Ο[,]Ο) β§ (πβ(π + 1)) β 0) β (sinβ((πβ(π + 1)) / 2)) β 0) |
391 | 389, 341,
390 | syl2anc 585 |
. . . . . . 7
β’ (π β (sinβ((πβ(π + 1)) / 2)) β 0) |
392 | 358, 388,
369, 391 | mulne0d 11814 |
. . . . . 6
β’ (π β (2 Β·
(sinβ((πβ(π + 1)) / 2))) β
0) |
393 | 162, 343,
3, 148, 355, 334, 386, 392, 159 | divlimc 43971 |
. . . . 5
β’ (π β ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / (2 Β· (sinβ(π / 2))))) limβ (πβ(π + 1)))) |
394 | 2, 3, 4, 142, 160, 342, 393 | mullimc 43931 |
. . . 4
β’ (π β (((if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) Β· ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2))))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) limβ (πβ(π + 1)))) |
395 | | fourierdlem76.d |
. . . . 5
β’ π· = (((if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) Β· ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2))))) |
396 | 395 | a1i 11 |
. . . 4
β’ (π β π· = (((if((πβ(π + 1)) = (πβ(π + 1)), πΏ, (πΉβ(π + (πβ(π + 1))))) β πΆ) / (πβ(π + 1))) Β· ((πβ(π + 1)) / (2 Β· (sinβ((πβ(π + 1)) / 2)))))) |
397 | | fourierdlem76.o |
. . . . . . 7
β’ π = (π β (π΄[,]π΅) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) |
398 | 397 | reseq1i 5938 |
. . . . . 6
β’ (π βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β (π΄[,]π΅) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) βΎ ((πβπ)(,)(πβ(π + 1)))) |
399 | | ioossicc 13357 |
. . . . . . . 8
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
400 | | iccss 13339 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β β) β§ (π΄ β€ (πβπ) β§ (πβ(π + 1)) β€ π΅)) β ((πβπ)[,](πβ(π + 1))) β (π΄[,]π΅)) |
401 | 19, 98, 85, 107, 400 | syl22anc 838 |
. . . . . . . 8
β’ (π β ((πβπ)[,](πβ(π + 1))) β (π΄[,]π΅)) |
402 | 399, 401 | sstrid 3960 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (π΄[,]π΅)) |
403 | 402 | resmptd 5999 |
. . . . . 6
β’ (π β ((π β (π΄[,]π΅) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2))))))) |
404 | 398, 403 | eqtrid 2789 |
. . . . 5
β’ (π β (π βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2))))))) |
405 | 404 | oveq1d 7377 |
. . . 4
β’ (π β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) limβ (πβ(π + 1)))) |
406 | 394, 396,
405 | 3eltr4d 2853 |
. . 3
β’ (π β π· β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
407 | 1, 406 | sylbir 234 |
. 2
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β π· β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
408 | 242, 249 | gtned 11297 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β (πβπ)) |
409 | | fourierdlem76.r |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
410 | 6, 223, 409 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
411 | 240 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
412 | 410, 411 | eleqtrd 2840 |
. . . . . . . . . 10
β’ (π β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (π + (πβπ)))) |
413 | 193 | recnd 11190 |
. . . . . . . . . 10
β’ (π β (πβπ) β β) |
414 | 276, 230,
278, 279, 263, 281, 408, 412, 413 | fourierdlem53 44474 |
. . . . . . . . 9
β’ (π β π
β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβπ))) |
415 | | eqid 2737 |
. . . . . . . . 9
β’ if((πβπ) = (πβπ), π
, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβπ))) = if((πβπ) = (πβπ), π
, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβπ))) |
416 | | eqid 2737 |
. . . . . . . . 9
β’
((TopOpenββfld) βΎt ((πβπ)[,)(πβ(π + 1)))) =
((TopOpenββfld) βΎt ((πβπ)[,)(πβ(π + 1)))) |
417 | 193, 211,
221, 275, 414, 290, 90, 297, 298, 415, 416 | fourierdlem32 44454 |
. . . . . . . 8
β’ (π β if((πβπ) = (πβπ), π
, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβπ))) β (((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
418 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))) |
419 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (π + π ) = (π + (πβπ))) |
420 | 419 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (πΉβ(π + π )) = (πΉβ(π + (πβπ)))) |
421 | 420 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ Β¬ (πβπ) = (πβπ)) β§ π = (πβπ)) β (πΉβ(π + π )) = (πΉβ(π + (πβπ)))) |
422 | 243 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β
β*) |
423 | 245 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβ(π + 1)) β
β*) |
424 | 290 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β β) |
425 | 193 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β β) |
426 | 310 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β€ (πβπ)) |
427 | | neqne 2952 |
. . . . . . . . . . . . 13
β’ (Β¬
(πβπ) = (πβπ) β (πβπ) β (πβπ)) |
428 | 427 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β (πβπ)) |
429 | 425, 424,
426, 428 | leneltd 11316 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) < (πβπ)) |
430 | 90 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβ(π + 1)) β β) |
431 | 211 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβ(π + 1)) β β) |
432 | 297 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) < (πβ(π + 1))) |
433 | 314 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβ(π + 1)) β€ (πβ(π + 1))) |
434 | 424, 430,
431, 432, 433 | ltletrd 11322 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) < (πβ(π + 1))) |
435 | 422, 423,
424, 429, 434 | eliood 43810 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πβπ) β ((πβπ)(,)(πβ(π + 1)))) |
436 | 230, 290 | readdcld 11191 |
. . . . . . . . . . . 12
β’ (π β (π + (πβπ)) β β) |
437 | 276, 436 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ (π β (πΉβ(π + (πβπ))) β β) |
438 | 437 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β (πΉβ(π + (πβπ))) β β) |
439 | 418, 421,
435, 438 | fvmptd 6960 |
. . . . . . . . 9
β’ ((π β§ Β¬ (πβπ) = (πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβπ)) = (πΉβ(π + (πβπ)))) |
440 | 439 | ifeq2da 4523 |
. . . . . . . 8
β’ (π β if((πβπ) = (πβπ), π
, ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))β(πβπ))) = if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ))))) |
441 | 326 | oveq1d 7377 |
. . . . . . . 8
β’ (π β (((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβπ))) |
442 | 417, 440,
441 | 3eltr3d 2852 |
. . . . . . 7
β’ (π β if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) limβ (πβπ))) |
443 | 290 | recnd 11190 |
. . . . . . . 8
β’ (π β (πβπ) β β) |
444 | 168, 330,
124, 443 | constlimc 43939 |
. . . . . . 7
β’ (π β πΆ β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ πΆ) limβ (πβπ))) |
445 | 167, 168,
161, 121, 125, 442, 444 | sublimc 43967 |
. . . . . 6
β’ (π β (if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β πΆ) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β πΆ)) limβ (πβπ))) |
446 | 330, 162,
443 | idlimc 43941 |
. . . . . 6
β’ (π β (πβπ) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) limβ (πβπ))) |
447 | 6, 83 | jca 513 |
. . . . . . 7
β’ (π β (π β§ (πβπ) β (π΄[,]π΅))) |
448 | | eleq1 2826 |
. . . . . . . . . 10
β’ (π = (πβπ) β (π β (π΄[,]π΅) β (πβπ) β (π΄[,]π΅))) |
449 | 448 | anbi2d 630 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β§ π β (π΄[,]π΅)) β (π β§ (πβπ) β (π΄[,]π΅)))) |
450 | | neeq1 3007 |
. . . . . . . . 9
β’ (π = (πβπ) β (π β 0 β (πβπ) β 0)) |
451 | 449, 450 | imbi12d 345 |
. . . . . . . 8
β’ (π = (πβπ) β (((π β§ π β (π΄[,]π΅)) β π β 0) β ((π β§ (πβπ) β (π΄[,]π΅)) β (πβπ) β 0))) |
452 | 451, 140 | vtoclg 3528 |
. . . . . . 7
β’ ((πβπ) β (π΄[,]π΅) β ((π β§ (πβπ) β (π΄[,]π΅)) β (πβπ) β 0)) |
453 | 83, 447, 452 | sylc 65 |
. . . . . 6
β’ (π β (πβπ) β 0) |
454 | 161, 162,
2, 126, 166, 445, 446, 453, 141 | divlimc 43971 |
. . . . 5
β’ (π β ((if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / π )) limβ (πβπ))) |
455 | 356, 330,
358, 443 | constlimc 43939 |
. . . . . . 7
β’ (π β 2 β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) limβ
(πβπ))) |
456 | 348 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπ)(,)(πβ(π + 1))) β§ (π / 2) β ((πβπ) / 2))) β (π / 2) β β) |
457 | 162, 356,
364, 148, 368, 446, 455, 369, 152 | divlimc 43971 |
. . . . . . . 8
β’ (π β ((πβπ) / 2) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / 2)) limβ (πβπ))) |
458 | 290 | rehalfcld 12407 |
. . . . . . . . 9
β’ (π β ((πβπ) / 2) β β) |
459 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = ((πβπ) / 2) β (sinβπ₯) = (sinβ((πβπ) / 2))) |
460 | 378, 458,
459 | cnmptlimc 25270 |
. . . . . . . 8
β’ (π β (sinβ((πβπ) / 2)) β ((π₯ β β β¦ (sinβπ₯)) limβ ((πβπ) / 2))) |
461 | | fveq2 6847 |
. . . . . . . . 9
β’ ((π / 2) = ((πβπ) / 2) β (sinβ(π / 2)) = (sinβ((πβπ) / 2))) |
462 | 461 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ (π β ((πβπ)(,)(πβ(π + 1))) β§ (π / 2) = ((πβπ) / 2))) β (sinβ(π / 2)) = (sinβ((πβπ) / 2))) |
463 | 456, 363,
457, 460, 382, 462 | limcco 25273 |
. . . . . . 7
β’ (π β (sinβ((πβπ) / 2)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (sinβ(π / 2))) limβ
(πβπ))) |
464 | 356, 357,
343, 143, 150, 455, 463 | mullimc 43931 |
. . . . . 6
β’ (π β (2 Β·
(sinβ((πβπ) / 2))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) limβ
(πβπ))) |
465 | 443 | halfcld 12405 |
. . . . . . . 8
β’ (π β ((πβπ) / 2) β β) |
466 | 465 | sincld 16019 |
. . . . . . 7
β’ (π β (sinβ((πβπ) / 2)) β β) |
467 | 154, 83 | sseldd 3950 |
. . . . . . . 8
β’ (π β (πβπ) β (-Ο[,]Ο)) |
468 | | fourierdlem44 44466 |
. . . . . . . 8
β’ (((πβπ) β (-Ο[,]Ο) β§ (πβπ) β 0) β (sinβ((πβπ) / 2)) β 0) |
469 | 467, 453,
468 | syl2anc 585 |
. . . . . . 7
β’ (π β (sinβ((πβπ) / 2)) β 0) |
470 | 358, 466,
369, 469 | mulne0d 11814 |
. . . . . 6
β’ (π β (2 Β·
(sinβ((πβπ) / 2))) β
0) |
471 | 162, 343,
3, 148, 355, 446, 464, 470, 159 | divlimc 43971 |
. . . . 5
β’ (π β ((πβπ) / (2 Β· (sinβ((πβπ) / 2)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / (2 Β· (sinβ(π / 2))))) limβ (πβπ))) |
472 | 2, 3, 4, 142, 160, 454, 471 | mullimc 43931 |
. . . 4
β’ (π β (((if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) Β· ((πβπ) / (2 Β· (sinβ((πβπ) / 2))))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) limβ (πβπ))) |
473 | | fourierdlem76.e |
. . . . 5
β’ πΈ = (((if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) Β· ((πβπ) / (2 Β· (sinβ((πβπ) / 2))))) |
474 | 473 | a1i 11 |
. . . 4
β’ (π β πΈ = (((if((πβπ) = (πβπ), π
, (πΉβ(π + (πβπ)))) β πΆ) / (πβπ)) Β· ((πβπ) / (2 Β· (sinβ((πβπ) / 2)))))) |
475 | 404 | oveq1d 7377 |
. . . 4
β’ (π β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) limβ (πβπ))) |
476 | 472, 474,
475 | 3eltr4d 2853 |
. . 3
β’ (π β πΈ β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
477 | 1, 476 | sylbir 234 |
. 2
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β πΈ β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
478 | 298 | sselda 3949 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)(,)(πβ(π + 1)))) |
479 | 478, 266 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) |
480 | 479 | mpteq2dva 5210 |
. . . . . . . 8
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π )))) |
481 | 225 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
482 | 228 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
483 | 230 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
484 | 483, 129 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
485 | 240 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
486 | 193 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
487 | 243 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
488 | 245 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
489 | 487, 488,
478, 248 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π ) |
490 | 486, 18, 483, 489 | ltadd2dd 11321 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π )) |
491 | 485, 490 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )) |
492 | 211 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
493 | 487, 488,
478, 253 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π < (πβ(π + 1))) |
494 | 18, 492, 483, 493 | ltadd2dd 11321 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (π + (πβ(π + 1)))) |
495 | 260 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
496 | 494, 495 | breqtrd 5136 |
. . . . . . . . . 10
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
497 | 481, 482,
484, 491, 496 | eliood 43810 |
. . . . . . . . 9
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β ((πβπ)(,)(πβ(π + 1)))) |
498 | 269, 271,
330, 237, 497 | fourierdlem23 44445 |
. . . . . . . 8
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
499 | 480, 498 | eqeltrd 2838 |
. . . . . . 7
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
500 | | ssid 3971 |
. . . . . . . . 9
β’ β
β β |
501 | 500 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β) |
502 | 330, 124,
501 | constcncfg 44187 |
. . . . . . 7
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ πΆ) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
503 | 499, 502 | subcncf 24825 |
. . . . . 6
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) β πΆ)) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
504 | 166 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β ((πβπ)(,)(πβ(π + 1)))π β (β β
{0})) |
505 | | dfss3 3937 |
. . . . . . . 8
β’ (((πβπ)(,)(πβ(π + 1))) β (β β {0}) β
βπ β ((πβπ)(,)(πβ(π + 1)))π β (β β
{0})) |
506 | 504, 505 | sylibr 233 |
. . . . . . 7
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (β β
{0})) |
507 | | difssd 4097 |
. . . . . . 7
β’ (π β (β β {0})
β β) |
508 | 506, 507 | idcncfg 44188 |
. . . . . 6
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) β (((πβπ)(,)(πβ(π + 1)))βcnβ(β β {0}))) |
509 | 503, 508 | divcncf 24827 |
. . . . 5
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((πΉβ(π + π )) β πΆ) / π )) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
510 | 330, 501 | idcncfg 44188 |
. . . . . 6
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ π ) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
511 | 355, 343 | fmptd 7067 |
. . . . . . 7
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))):((πβπ)(,)(πβ(π + 1)))βΆ(β β
{0})) |
512 | 330, 358,
501 | constcncfg 44187 |
. . . . . . . . 9
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
513 | | sincn 25819 |
. . . . . . . . . . 11
β’ sin
β (ββcnββ) |
514 | 513 | a1i 11 |
. . . . . . . . . 10
β’ (π β sin β
(ββcnββ)) |
515 | 367 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β (β β
{0})) |
516 | 330, 515,
507 | constcncfg 44187 |
. . . . . . . . . . 11
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ 2) β (((πβπ)(,)(πβ(π + 1)))βcnβ(β β {0}))) |
517 | 510, 516 | divcncf 24827 |
. . . . . . . . . 10
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / 2)) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
518 | 514, 517 | cncfmpt1f 24293 |
. . . . . . . . 9
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (sinβ(π / 2))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
519 | 512, 518 | mulcncf 24826 |
. . . . . . . 8
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
520 | | cncfcdm 24277 |
. . . . . . . 8
β’
(((β β {0}) β β β§ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) β (((πβπ)(,)(πβ(π + 1)))βcnβ(β β {0})) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))):((πβπ)(,)(πβ(π + 1)))βΆ(β β
{0}))) |
521 | 507, 519,
520 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) β (((πβπ)(,)(πβ(π + 1)))βcnβ(β β {0})) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))):((πβπ)(,)(πβ(π + 1)))βΆ(β β
{0}))) |
522 | 511, 521 | mpbird 257 |
. . . . . 6
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (2 Β· (sinβ(π / 2)))) β (((πβπ)(,)(πβ(π + 1)))βcnβ(β β {0}))) |
523 | 510, 522 | divcncf 24827 |
. . . . 5
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π / (2 Β· (sinβ(π / 2))))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
524 | 509, 523 | mulcncf 24826 |
. . . 4
β’ (π β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((((πΉβ(π + π )) β πΆ) / π ) Β· (π / (2 Β· (sinβ(π / 2)))))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
525 | 404, 524 | eqeltrd 2838 |
. . 3
β’ (π β (π βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
526 | 1, 525 | sylbir 234 |
. 2
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β (π βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
527 | 407, 477,
526 | jca31 516 |
1
β’ ((((π β§ π β (0..^π)) β§ π β (0..^π)) β§ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) β ((π· β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) β§ πΈ β ((π βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) β§ (π βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ))) |