Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . . 6
β’ (π = π β (π β β β π β β)) |
2 | 1 | anbi2d 630 |
. . . . 5
β’ (π = π β ((π β§ π β β) β (π β§ π β β))) |
3 | | fveq2 6889 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
4 | | fveq2 6889 |
. . . . . . . . . 10
β’ (π = π β (π·βπ) = (π·βπ)) |
5 | 4 | fveq1d 6891 |
. . . . . . . . 9
β’ (π = π β ((π·βπ)β(π‘ β π)) = ((π·βπ)β(π‘ β π))) |
6 | 5 | oveq2d 7422 |
. . . . . . . 8
β’ (π = π β ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) = ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π)))) |
7 | 6 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π‘ β (-Ο(,)Ο)) β ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) = ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π)))) |
8 | 7 | itgeq2dv 25291 |
. . . . . 6
β’ (π = π β β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) |
9 | 3, 8 | eqeq12d 2749 |
. . . . 5
β’ (π = π β ((πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ β (πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘)) |
10 | 2, 9 | imbi12d 345 |
. . . 4
β’ (π = π β (((π β§ π β β) β (πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) β ((π β§ π β β) β (πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘))) |
11 | | fourierdlem111.6 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β πΉ:ββΆβ) |
13 | | eqid 2733 |
. . . . 5
β’
(-Ο(,)Ο) = (-Ο(,)Ο) |
14 | | ioossre 13382 |
. . . . . . . . 9
β’
(-Ο(,)Ο) β β |
15 | 14 | a1i 11 |
. . . . . . . 8
β’ (π β (-Ο(,)Ο) β
β) |
16 | 11, 15 | feqresmpt 6959 |
. . . . . . 7
β’ (π β (πΉ βΎ (-Ο(,)Ο)) = (π₯ β (-Ο(,)Ο) β¦
(πΉβπ₯))) |
17 | | ioossicc 13407 |
. . . . . . . . 9
β’
(-Ο(,)Ο) β (-Ο[,]Ο) |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ (π β (-Ο(,)Ο) β
(-Ο[,]Ο)) |
19 | | ioombl 25074 |
. . . . . . . . 9
β’
(-Ο(,)Ο) β dom vol |
20 | 19 | a1i 11 |
. . . . . . . 8
β’ (π β (-Ο(,)Ο) β dom
vol) |
21 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (-Ο[,]Ο)) β πΉ:ββΆβ) |
22 | | pire 25960 |
. . . . . . . . . . . . . . 15
β’ Ο
β β |
23 | 22 | renegcli 11518 |
. . . . . . . . . . . . . 14
β’ -Ο
β β |
24 | 23, 22 | elicc2i 13387 |
. . . . . . . . . . . . 13
β’ (π‘ β (-Ο[,]Ο) β
(π‘ β β β§
-Ο β€ π‘ β§ π‘ β€ Ο)) |
25 | 24 | simp1bi 1146 |
. . . . . . . . . . . 12
β’ (π‘ β (-Ο[,]Ο) β
π‘ β
β) |
26 | 25 | ssriv 3986 |
. . . . . . . . . . 11
β’
(-Ο[,]Ο) β β |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ (π β (-Ο[,]Ο) β
β) |
28 | 27 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π₯ β (-Ο[,]Ο)) β π₯ β
β) |
29 | 21, 28 | ffvelcdmd 7085 |
. . . . . . . 8
β’ ((π β§ π₯ β (-Ο[,]Ο)) β (πΉβπ₯) β β) |
30 | 11, 27 | feqresmpt 6959 |
. . . . . . . . 9
β’ (π β (πΉ βΎ (-Ο[,]Ο)) = (π₯ β (-Ο[,]Ο) β¦
(πΉβπ₯))) |
31 | | fourierdlem111.p |
. . . . . . . . . 10
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
32 | | fourierdlem111.m |
. . . . . . . . . 10
β’ (π β π β β) |
33 | | fourierdlem111.q |
. . . . . . . . . 10
β’ (π β π β (πβπ)) |
34 | | ax-resscn 11164 |
. . . . . . . . . . . . 13
β’ β
β β |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
36 | 11, 35 | fssd 6733 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
37 | 36, 27 | fssresd 6756 |
. . . . . . . . . 10
β’ (π β (πΉ βΎ
(-Ο[,]Ο)):(-Ο[,]Ο)βΆβ) |
38 | | ioossicc 13407 |
. . . . . . . . . . . . 13
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
39 | 23 | rexri 11269 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β* |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β -Ο β
β*) |
41 | 22 | rexri 11269 |
. . . . . . . . . . . . . . 15
β’ Ο
β β* |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β Ο β
β*) |
43 | 31, 32, 33 | fourierdlem15 44825 |
. . . . . . . . . . . . . . 15
β’ (π β π:(0...π)βΆ(-Ο[,]Ο)) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆ(-Ο[,]Ο)) |
45 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π β (0..^π)) |
46 | 40, 42, 44, 45 | fourierdlem8 44818 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β
(-Ο[,]Ο)) |
47 | 38, 46 | sstrid 3993 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β
(-Ο[,]Ο)) |
48 | 47 | resabs1d 6011 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) = (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
49 | | fourierdlem111.fcn |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
50 | 48, 49 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
51 | | fourierdlem111.r |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
52 | 48 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
53 | 51, 52 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π
β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
54 | | fourierdlem111.l |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β πΏ β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
55 | 48 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
56 | 54, 55 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β πΏ β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
57 | 31, 32, 33, 37, 50, 53, 56 | fourierdlem69 44878 |
. . . . . . . . 9
β’ (π β (πΉ βΎ (-Ο[,]Ο)) β
πΏ1) |
58 | 30, 57 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (π₯ β (-Ο[,]Ο) β¦ (πΉβπ₯)) β
πΏ1) |
59 | 18, 20, 29, 58 | iblss 25314 |
. . . . . . 7
β’ (π β (π₯ β (-Ο(,)Ο) β¦ (πΉβπ₯)) β
πΏ1) |
60 | 16, 59 | eqeltrd 2834 |
. . . . . 6
β’ (π β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
61 | 60 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β (πΉ βΎ (-Ο(,)Ο)) β
πΏ1) |
62 | | fourierdlem111.a |
. . . . 5
β’ π΄ = (π β β0 β¦
(β«(-Ο(,)Ο)((πΉβπ‘) Β· (cosβ(π Β· π‘))) dπ‘ / Ο)) |
63 | | fourierdlem111.b |
. . . . 5
β’ π΅ = (π β β β¦
(β«(-Ο(,)Ο)((πΉβπ‘) Β· (sinβ(π Β· π‘))) dπ‘ / Ο)) |
64 | | fourierdlem111.x |
. . . . . 6
β’ (π β π β β) |
65 | 64 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
66 | | fourierdlem111.s |
. . . . 5
β’ π = (π β β β¦ (((π΄β0) / 2) + Ξ£π β (1...π)(((π΄βπ) Β· (cosβ(π Β· π))) + ((π΅βπ) Β· (sinβ(π Β· π)))))) |
67 | | fourierdlem111.d |
. . . . 5
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
68 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
69 | 12, 13, 61, 62, 63, 65, 66, 67, 68 | fourierdlem83 44892 |
. . . 4
β’ ((π β§ π β β) β (πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) |
70 | 10, 69 | chvarvv 2003 |
. . 3
β’ ((π β§ π β β) β (πβπ) = β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) |
71 | 23 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β -Ο β
β) |
72 | 22 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β Ο β
β) |
73 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β (-Ο[,]Ο)) β πΉ:ββΆβ) |
74 | 25 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π‘ β (-Ο[,]Ο)) β π‘ β
β) |
75 | 73, 74 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π‘ β (-Ο[,]Ο)) β (πΉβπ‘) β β) |
76 | 75 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β (πΉβπ‘) β β) |
77 | 67 | dirkerf 44800 |
. . . . . . . . 9
β’ (π β β β (π·βπ):ββΆβ) |
78 | 77 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β (π·βπ):ββΆβ) |
79 | 64 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β (-Ο[,]Ο)) β π β
β) |
80 | 74, 79 | resubcld 11639 |
. . . . . . . . 9
β’ ((π β§ π‘ β (-Ο[,]Ο)) β (π‘ β π) β β) |
81 | 80 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β (π‘ β π) β β) |
82 | 78, 81 | ffvelcdmd 7085 |
. . . . . . 7
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β ((π·βπ)β(π‘ β π)) β β) |
83 | 82 | recnd 11239 |
. . . . . 6
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β ((π·βπ)β(π‘ β π)) β β) |
84 | 76, 83 | mulcld 11231 |
. . . . 5
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) β β) |
85 | 71, 72, 84 | itgioo 25325 |
. . . 4
β’ ((π β§ π β β) β
β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«(-Ο[,]Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) |
86 | | fvres 6908 |
. . . . . . . 8
β’ (π‘ β (-Ο[,]Ο) β
((πΉ βΎ
(-Ο[,]Ο))βπ‘) =
(πΉβπ‘)) |
87 | 86 | eqcomd 2739 |
. . . . . . 7
β’ (π‘ β (-Ο[,]Ο) β
(πΉβπ‘) = ((πΉ βΎ (-Ο[,]Ο))βπ‘)) |
88 | 87 | oveq1d 7421 |
. . . . . 6
β’ (π‘ β (-Ο[,]Ο) β
((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) = (((πΉ βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π)))) |
89 | 88 | adantl 483 |
. . . . 5
β’ (((π β§ π β β) β§ π‘ β (-Ο[,]Ο)) β ((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) = (((πΉ βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π)))) |
90 | 89 | itgeq2dv 25291 |
. . . 4
β’ ((π β§ π β β) β
β«(-Ο[,]Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«(-Ο[,]Ο)(((πΉ βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘) |
91 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π¦ β β) β π = π) |
92 | 91 | oveq2d 7422 |
. . . . . . . . . . . 12
β’ ((π = π β§ π¦ β β) β (2 Β· π) = (2 Β· π)) |
93 | 92 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π = π β§ π¦ β β) β ((2 Β· π) + 1) = ((2 Β· π) + 1)) |
94 | 93 | oveq1d 7421 |
. . . . . . . . . 10
β’ ((π = π β§ π¦ β β) β (((2 Β· π) + 1) / (2 Β· Ο)) =
(((2 Β· π) + 1) / (2
Β· Ο))) |
95 | 91 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π¦ β β) β (π + (1 / 2)) = (π + (1 / 2))) |
96 | 95 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ ((π = π β§ π¦ β β) β ((π + (1 / 2)) Β· π¦) = ((π + (1 / 2)) Β· π¦)) |
97 | 96 | fveq2d 6893 |
. . . . . . . . . . 11
β’ ((π = π β§ π¦ β β) β (sinβ((π + (1 / 2)) Β· π¦)) = (sinβ((π + (1 / 2)) Β· π¦))) |
98 | 97 | oveq1d 7421 |
. . . . . . . . . 10
β’ ((π = π β§ π¦ β β) β ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))) =
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2))))) |
99 | 94, 98 | ifeq12d 4549 |
. . . . . . . . 9
β’ ((π = π β§ π¦ β β) β if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2))))) =
if((π¦ mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2)))))) |
100 | 99 | mpteq2dva 5248 |
. . . . . . . 8
β’ (π = π β (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ / 2)))))) =
(π¦ β β β¦
if((π¦ mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2))))))) |
101 | 100 | cbvmptv 5261 |
. . . . . . 7
β’ (π β β β¦ (π¦ β β β¦
if((π¦ mod (2 Β·
Ο)) = 0, (((2 Β· π) + 1) / (2 Β· Ο)),
((sinβ((π + (1 / 2))
Β· π¦)) / ((2 Β·
Ο) Β· (sinβ(π¦ / 2))))))) = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
102 | 67, 101 | eqtri 2761 |
. . . . . 6
β’ π· = (π β β β¦ (π¦ β β β¦ if((π¦ mod (2 Β· Ο)) = 0,
(((2 Β· π) + 1) / (2
Β· Ο)), ((sinβ((π + (1 / 2)) Β· π¦)) / ((2 Β· Ο) Β·
(sinβ(π¦ /
2))))))) |
103 | | fveq2 6889 |
. . . . . . . 8
β’ (π = π‘ β ((πΉ βΎ (-Ο[,]Ο))βπ ) = ((πΉ βΎ (-Ο[,]Ο))βπ‘)) |
104 | | oveq1 7413 |
. . . . . . . . 9
β’ (π = π‘ β (π β π) = (π‘ β π)) |
105 | 104 | fveq2d 6893 |
. . . . . . . 8
β’ (π = π‘ β ((π·βπ)β(π β π)) = ((π·βπ)β(π‘ β π))) |
106 | 103, 105 | oveq12d 7424 |
. . . . . . 7
β’ (π = π‘ β (((πΉ βΎ (-Ο[,]Ο))βπ ) Β· ((π·βπ)β(π β π))) = (((πΉ βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π)))) |
107 | 106 | cbvmptv 5261 |
. . . . . 6
β’ (π β (-Ο[,]Ο) β¦
(((πΉ βΎ
(-Ο[,]Ο))βπ )
Β· ((π·βπ)β(π β π)))) = (π‘ β (-Ο[,]Ο) β¦ (((πΉ βΎ
(-Ο[,]Ο))βπ‘)
Β· ((π·βπ)β(π‘ β π)))) |
108 | 33 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β (πβπ)) |
109 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
110 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
111 | 64 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
112 | 37 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β (πΉ βΎ
(-Ο[,]Ο)):(-Ο[,]Ο)βΆβ) |
113 | 50 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0..^π)) β ((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
114 | 53 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0..^π)) β π
β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
115 | 56 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0..^π)) β πΏ β (((πΉ βΎ (-Ο[,]Ο)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
116 | 102, 31, 107, 108, 109, 110, 111, 112, 113, 114, 115 | fourierdlem101 44910 |
. . . . 5
β’ ((π β§ π β β) β
β«(-Ο[,]Ο)(((πΉ
βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«((-Ο β π)[,](Ο β π))(((πΉ βΎ (-Ο[,]Ο))β(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦) |
117 | | oveq2 7414 |
. . . . . . . . . 10
β’ (π = π¦ β (π + π ) = (π + π¦)) |
118 | 117 | fveq2d 6893 |
. . . . . . . . 9
β’ (π = π¦ β (πΉβ(π + π )) = (πΉβ(π + π¦))) |
119 | | fveq2 6889 |
. . . . . . . . 9
β’ (π = π¦ β ((π·βπ)βπ ) = ((π·βπ)βπ¦)) |
120 | 118, 119 | oveq12d 7424 |
. . . . . . . 8
β’ (π = π¦ β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦))) |
121 | 120 | cbvitgv 25286 |
. . . . . . 7
β’
β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦ |
122 | 121 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦) |
123 | 23 | a1i 11 |
. . . . . . . . 9
β’ (π β -Ο β
β) |
124 | 123, 64 | resubcld 11639 |
. . . . . . . 8
β’ (π β (-Ο β π) β
β) |
125 | 124 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β (-Ο β π) β
β) |
126 | 22 | a1i 11 |
. . . . . . . . 9
β’ (π β Ο β
β) |
127 | 126, 64 | resubcld 11639 |
. . . . . . . 8
β’ (π β (Ο β π) β
β) |
128 | 127 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β (Ο β π) β
β) |
129 | 36 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β πΉ:ββΆβ) |
130 | 64 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β π β β) |
131 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β π¦ β ((-Ο β π)[,](Ο β π))) |
132 | 124 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (-Ο β π) β β) |
133 | 127 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (Ο β π) β β) |
134 | | elicc2 13386 |
. . . . . . . . . . . . . 14
β’ (((-Ο
β π) β β
β§ (Ο β π)
β β) β (π¦
β ((-Ο β π)[,](Ο β π)) β (π¦ β β β§ (-Ο β π) β€ π¦ β§ π¦ β€ (Ο β π)))) |
135 | 132, 133,
134 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π¦ β ((-Ο β π)[,](Ο β π)) β (π¦ β β β§ (-Ο β π) β€ π¦ β§ π¦ β€ (Ο β π)))) |
136 | 131, 135 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π¦ β β β§ (-Ο β π) β€ π¦ β§ π¦ β€ (Ο β π))) |
137 | 136 | simp1d 1143 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β π¦ β β) |
138 | 130, 137 | readdcld 11240 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + π¦) β β) |
139 | 129, 138 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (πΉβ(π + π¦)) β β) |
140 | 139 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β (πΉβ(π + π¦)) β β) |
141 | 77 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π·βπ):ββΆβ) |
142 | 137 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β π¦ β β) |
143 | 141, 142 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β ((π·βπ)βπ¦) β β) |
144 | 143 | recnd 11239 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β ((π·βπ)βπ¦) β β) |
145 | 140, 144 | mulcld 11231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β ((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) β β) |
146 | 125, 128,
145 | itgioo 25325 |
. . . . . 6
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦ = β«((-Ο β π)[,](Ο β π))((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦) |
147 | 23 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β -Ο β
β) |
148 | 22 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β Ο β
β) |
149 | 64 | recnd 11239 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
150 | 126 | recnd 11239 |
. . . . . . . . . . . . . . . . 17
β’ (π β Ο β
β) |
151 | 150 | negcld 11555 |
. . . . . . . . . . . . . . . 16
β’ (π β -Ο β
β) |
152 | 149, 151 | pncan3d 11571 |
. . . . . . . . . . . . . . 15
β’ (π β (π + (-Ο β π)) = -Ο) |
153 | 152 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (π β -Ο = (π + (-Ο β π))) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β -Ο = (π + (-Ο β π))) |
155 | 136 | simp2d 1144 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (-Ο β π) β€ π¦) |
156 | 132, 137,
130, 155 | leadd2dd 11826 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + (-Ο β π)) β€ (π + π¦)) |
157 | 154, 156 | eqbrtrd 5170 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β -Ο β€ (π + π¦)) |
158 | 136 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β π¦ β€ (Ο β π)) |
159 | 137, 133,
130, 158 | leadd2dd 11826 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + π¦) β€ (π + (Ο β π))) |
160 | 149 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β π β β) |
161 | 150 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β Ο β
β) |
162 | 160, 161 | pncan3d 11571 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + (Ο β π)) = Ο) |
163 | 159, 162 | breqtrd 5174 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + π¦) β€ Ο) |
164 | 147, 148,
138, 157, 163 | eliccd 44204 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (π + π¦) β (-Ο[,]Ο)) |
165 | | fvres 6908 |
. . . . . . . . . . 11
β’ ((π + π¦) β (-Ο[,]Ο) β ((πΉ βΎ
(-Ο[,]Ο))β(π +
π¦)) = (πΉβ(π + π¦))) |
166 | 164, 165 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β ((πΉ βΎ (-Ο[,]Ο))β(π + π¦)) = (πΉβ(π + π¦))) |
167 | 166 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π¦ β ((-Ο β π)[,](Ο β π))) β (πΉβ(π + π¦)) = ((πΉ βΎ (-Ο[,]Ο))β(π + π¦))) |
168 | 167 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β (πΉβ(π + π¦)) = ((πΉ βΎ (-Ο[,]Ο))β(π + π¦))) |
169 | 168 | oveq1d 7421 |
. . . . . . 7
β’ (((π β§ π β β) β§ π¦ β ((-Ο β π)[,](Ο β π))) β ((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) = (((πΉ βΎ (-Ο[,]Ο))β(π + π¦)) Β· ((π·βπ)βπ¦))) |
170 | 169 | itgeq2dv 25291 |
. . . . . 6
β’ ((π β§ π β β) β β«((-Ο β
π)[,](Ο β π))((πΉβ(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦ = β«((-Ο β π)[,](Ο β π))(((πΉ βΎ (-Ο[,]Ο))β(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦) |
171 | 122, 146,
170 | 3eqtrrd 2778 |
. . . . 5
β’ ((π β§ π β β) β β«((-Ο β
π)[,](Ο β π))(((πΉ βΎ (-Ο[,]Ο))β(π + π¦)) Β· ((π·βπ)βπ¦)) dπ¦ = β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
172 | 116, 171 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β
β«(-Ο[,]Ο)(((πΉ
βΎ (-Ο[,]Ο))βπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
173 | 85, 90, 172 | 3eqtrd 2777 |
. . 3
β’ ((π β§ π β β) β
β«(-Ο(,)Ο)((πΉβπ‘) Β· ((π·βπ)β(π‘ β π))) dπ‘ = β«((-Ο β π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
174 | | elioore 13351 |
. . . . . . . . 9
β’ (π β ((-Ο β π)(,)(Ο β π)) β π β β) |
175 | 174 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β π β β) |
176 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((-Ο β π)(,)(Ο β π))) β πΉ:ββΆβ) |
177 | 64 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((-Ο β π)(,)(Ο β π))) β π β β) |
178 | 174 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((-Ο β π)(,)(Ο β π))) β π β β) |
179 | 177, 178 | readdcld 11240 |
. . . . . . . . . . 11
β’ ((π β§ π β ((-Ο β π)(,)(Ο β π))) β (π + π ) β β) |
180 | 176, 179 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ ((π β§ π β ((-Ο β π)(,)(Ο β π))) β (πΉβ(π + π )) β β) |
181 | 180 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β (πΉβ(π + π )) β β) |
182 | 77 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β (π·βπ):ββΆβ) |
183 | 182, 175 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β ((π·βπ)βπ ) β β) |
184 | 183 | recnd 11239 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β ((π·βπ)βπ ) β β) |
185 | 181, 184 | mulcld 11231 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
186 | | fourierdlem111.g |
. . . . . . . . . 10
β’ πΊ = (π₯ β β β¦ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) |
187 | | oveq2 7414 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (π + π₯) = (π + π )) |
188 | 187 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πΉβ(π + π₯)) = (πΉβ(π + π ))) |
189 | | fveq2 6889 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((π·βπ)βπ₯) = ((π·βπ)βπ )) |
190 | 188, 189 | oveq12d 7424 |
. . . . . . . . . . 11
β’ (π₯ = π β ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
191 | 190 | cbvmptv 5261 |
. . . . . . . . . 10
β’ (π₯ β β β¦ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) = (π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
192 | 186, 191 | eqtri 2761 |
. . . . . . . . 9
β’ πΊ = (π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
193 | 192 | fvmpt2 7007 |
. . . . . . . 8
β’ ((π β β β§ ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
194 | 175, 185,
193 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
195 | 194 | eqcomd 2739 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((-Ο β π)(,)(Ο β π))) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = (πΊβπ )) |
196 | 195 | itgeq2dv 25291 |
. . . . 5
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«((-Ο β π)(,)(Ο β π))(πΊβπ ) dπ ) |
197 | 36 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β πΉ:ββΆβ) |
198 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β π β β) |
199 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β π₯ β β) |
200 | 198, 199 | readdcld 11240 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (π + π₯) β β) |
201 | 197, 200 | ffvelcdmd 7085 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (πΉβ(π + π₯)) β β) |
202 | 201 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβ(π + π₯)) β β) |
203 | 77 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π·βπ):ββΆβ) |
204 | 203 | ffvelcdmda 7084 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β ((π·βπ)βπ₯) β β) |
205 | 204 | recnd 11239 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((π·βπ)βπ₯) β β) |
206 | 202, 205 | mulcld 11231 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) β β) |
207 | 206, 186 | fmptd 7111 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΊ:ββΆβ) |
208 | 207 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((-Ο β π)[,](Ο β π))) β πΊ:ββΆβ) |
209 | 124 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((-Ο β π)[,](Ο β π))) β (-Ο β π) β β) |
210 | 127 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((-Ο β π)[,](Ο β π))) β (Ο β π) β β) |
211 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β ((-Ο β π)[,](Ο β π))) β π β ((-Ο β π)[,](Ο β π))) |
212 | | eliccre 44205 |
. . . . . . . . . 10
β’ (((-Ο
β π) β β
β§ (Ο β π)
β β β§ π
β ((-Ο β π)[,](Ο β π))) β π β β) |
213 | 209, 210,
211, 212 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β ((-Ο β π)[,](Ο β π))) β π β β) |
214 | 213 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((-Ο β π)[,](Ο β π))) β π β β) |
215 | 208, 214 | ffvelcdmd 7085 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((-Ο β π)[,](Ο β π))) β (πΊβπ ) β β) |
216 | 125, 128,
215 | itgioo 25325 |
. . . . . 6
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))(πΊβπ ) dπ = β«((-Ο β π)[,](Ο β π))(πΊβπ ) dπ ) |
217 | | fveq2 6889 |
. . . . . . 7
β’ (π = π₯ β (πΊβπ ) = (πΊβπ₯)) |
218 | 217 | cbvitgv 25286 |
. . . . . 6
β’
β«((-Ο β π)[,](Ο β π))(πΊβπ ) dπ = β«((-Ο β π)[,](Ο β π))(πΊβπ₯) dπ₯ |
219 | 216, 218 | eqtrdi 2789 |
. . . . 5
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))(πΊβπ ) dπ = β«((-Ο β π)[,](Ο β π))(πΊβπ₯) dπ₯) |
220 | 196, 219 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«((-Ο β π)[,](Ο β π))(πΊβπ₯) dπ₯) |
221 | | eqid 2733 |
. . . . . . 7
β’ ((Ο
β π) β (-Ο
β π)) = ((Ο
β π) β (-Ο
β π)) |
222 | 111 | renegcld 11638 |
. . . . . . 7
β’ ((π β§ π β β) β -π β β) |
223 | | fourierdlem111.o |
. . . . . . 7
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
224 | 31 | fourierdlem2 44812 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
225 | 32, 224 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
226 | 33, 225 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
227 | 226 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β π β (β βm
(0...π))) |
228 | | elmapi 8840 |
. . . . . . . . . . . . . . 15
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
229 | 227, 228 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π:(0...π)βΆβ) |
230 | 229 | ffvelcdmda 7084 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
231 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β π β β) |
232 | 230, 231 | resubcld 11639 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β ((πβπ) β π) β β) |
233 | | fourierdlem111.14 |
. . . . . . . . . . . 12
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
234 | 232, 233 | fmptd 7111 |
. . . . . . . . . . 11
β’ (π β π:(0...π)βΆβ) |
235 | | reex 11198 |
. . . . . . . . . . . . 13
β’ β
β V |
236 | | ovex 7439 |
. . . . . . . . . . . . 13
β’
(0...π) β
V |
237 | 235, 236 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (β
β V β§ (0...π)
β V) |
238 | | elmapg 8830 |
. . . . . . . . . . . 12
β’ ((β
β V β§ (0...π)
β V) β (π β
(β βm (0...π)) β π:(0...π)βΆβ)) |
239 | 237, 238 | mp1i 13 |
. . . . . . . . . . 11
β’ (π β (π β (β βm
(0...π)) β π:(0...π)βΆβ)) |
240 | 234, 239 | mpbird 257 |
. . . . . . . . . 10
β’ (π β π β (β βm
(0...π))) |
241 | 233 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π = (π β (0...π) β¦ ((πβπ) β π))) |
242 | | fveq2 6889 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (πβπ) = (πβ0)) |
243 | 226 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πβ0) = -Ο β§ (πβπ) = Ο) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
244 | 243 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β ((πβ0) = -Ο β§ (πβπ) = Ο)) |
245 | 244 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β (πβ0) = -Ο) |
246 | 242, 245 | sylan9eqr 2795 |
. . . . . . . . . . . . 13
β’ ((π β§ π = 0) β (πβπ) = -Ο) |
247 | 246 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π = 0) β ((πβπ) β π) = (-Ο β π)) |
248 | | 0zd 12567 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β€) |
249 | 32 | nnzd 12582 |
. . . . . . . . . . . . . 14
β’ (π β π β β€) |
250 | | 0red 11214 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 0 β
β) |
251 | | nnre 12216 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
252 | | nngt0 12240 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 0 <
π) |
253 | 250, 251,
252 | ltled 11359 |
. . . . . . . . . . . . . . 15
β’ (π β β β 0 β€
π) |
254 | 32, 253 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β 0 β€ π) |
255 | | eluz2 12825 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β0) β (0 β β€ β§ π β β€ β§ 0 β€
π)) |
256 | 248, 249,
254, 255 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
β’ (π β π β
(β€β₯β0)) |
257 | | eluzfz1 13505 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . 12
β’ (π β 0 β (0...π)) |
259 | 241, 247,
258, 124 | fvmptd 7003 |
. . . . . . . . . . 11
β’ (π β (πβ0) = (-Ο β π)) |
260 | | fveq2 6889 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
261 | 244 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) = Ο) |
262 | 260, 261 | sylan9eqr 2795 |
. . . . . . . . . . . . 13
β’ ((π β§ π = π) β (πβπ) = Ο) |
263 | 262 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π = π) β ((πβπ) β π) = (Ο β π)) |
264 | | eluzfz2 13506 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β0) β π β (0...π)) |
265 | 256, 264 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β (0...π)) |
266 | 241, 263,
265, 127 | fvmptd 7003 |
. . . . . . . . . . 11
β’ (π β (πβπ) = (Ο β π)) |
267 | 259, 266 | jca 513 |
. . . . . . . . . 10
β’ (π β ((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π))) |
268 | 229 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
269 | | elfzofz 13645 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β π β (0...π)) |
270 | 269 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
271 | 268, 270 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
272 | | fzofzp1 13726 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β (π + 1) β (0...π)) |
273 | 272 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
274 | 268, 273 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
275 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π β β) |
276 | 243 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
277 | 276 | r19.21bi 3249 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
278 | 271, 274,
275, 277 | ltsub1dd 11823 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) < ((πβ(π + 1)) β π)) |
279 | 270, 232 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβπ) β π) β β) |
280 | 233 | fvmpt2 7007 |
. . . . . . . . . . . . 13
β’ ((π β (0...π) β§ ((πβπ) β π) β β) β (πβπ) = ((πβπ) β π)) |
281 | 270, 279,
280 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) = ((πβπ) β π)) |
282 | | fveq2 6889 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
283 | 282 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβπ) β π) = ((πβπ) β π)) |
284 | 283 | cbvmptv 5261 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β¦ ((πβπ) β π)) = (π β (0...π) β¦ ((πβπ) β π)) |
285 | 233, 284 | eqtri 2761 |
. . . . . . . . . . . . . 14
β’ π = (π β (0...π) β¦ ((πβπ) β π)) |
286 | 285 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π = (π β (0...π) β¦ ((πβπ) β π))) |
287 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
288 | 287 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
289 | 288 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π = (π + 1)) β ((πβπ) β π) = ((πβ(π + 1)) β π)) |
290 | 274, 275 | resubcld 11639 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β π) β β) |
291 | 286, 289,
273, 290 | fvmptd 7003 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβ(π + 1)) β π)) |
292 | 278, 281,
291 | 3brtr4d 5180 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
293 | 292 | ralrimiva 3147 |
. . . . . . . . . 10
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
294 | 240, 267,
293 | jca32 517 |
. . . . . . . . 9
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
295 | 223 | fourierdlem2 44812 |
. . . . . . . . . 10
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
296 | 32, 295 | syl 17 |
. . . . . . . . 9
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = (-Ο β π) β§ (πβπ) = (Ο β π)) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
297 | 294, 296 | mpbird 257 |
. . . . . . . 8
β’ (π β π β (πβπ)) |
298 | 297 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β (πβπ)) |
299 | 150, 151,
149 | nnncan2d 11603 |
. . . . . . . . . . . 12
β’ (π β ((Ο β π) β (-Ο β π)) = (Ο β
-Ο)) |
300 | | picn 25961 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
301 | 300 | 2timesi 12347 |
. . . . . . . . . . . . 13
β’ (2
Β· Ο) = (Ο + Ο) |
302 | | fourierdlem111.t |
. . . . . . . . . . . . 13
β’ π = (2 Β·
Ο) |
303 | 300, 300 | subnegi 11536 |
. . . . . . . . . . . . 13
β’ (Ο
β -Ο) = (Ο + Ο) |
304 | 301, 302,
303 | 3eqtr4i 2771 |
. . . . . . . . . . . 12
β’ π = (Ο β
-Ο) |
305 | 299, 304 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π β ((Ο β π) β (-Ο β π)) = π) |
306 | 305 | oveq2d 7422 |
. . . . . . . . . 10
β’ (π β (π₯ + ((Ο β π) β (-Ο β π))) = (π₯ + π)) |
307 | 306 | fveq2d 6893 |
. . . . . . . . 9
β’ (π β (πΊβ(π₯ + ((Ο β π) β (-Ο β π)))) = (πΊβ(π₯ + π))) |
308 | 307 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβ(π₯ + ((Ο β π) β (-Ο β π)))) = (πΊβ(π₯ + π))) |
309 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β π₯ β β) |
310 | 186 | fvmpt2 7007 |
. . . . . . . . . 10
β’ ((π₯ β β β§ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) β β) β (πΊβπ₯) = ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) |
311 | 309, 206,
310 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβπ₯) = ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯))) |
312 | 149 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β π β β) |
313 | 199 | recnd 11239 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β π₯ β β) |
314 | | 2re 12283 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
315 | 314, 22 | remulcli 11227 |
. . . . . . . . . . . . . . . . . . 19
β’ (2
Β· Ο) β β |
316 | 302, 315 | eqeltri 2830 |
. . . . . . . . . . . . . . . . . 18
β’ π β β |
317 | 316 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
318 | 317 | recnd 11239 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
319 | 318 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β π β β) |
320 | 312, 313,
319 | addassd 11233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β ((π + π₯) + π) = (π + (π₯ + π))) |
321 | 320 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (π + (π₯ + π)) = ((π + π₯) + π)) |
322 | 321 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (πΉβ(π + (π₯ + π))) = (πΉβ((π + π₯) + π))) |
323 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β π) |
324 | 323, 200 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (π β§ (π + π₯) β β)) |
325 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + π₯) β (π β β β (π + π₯) β β)) |
326 | 325 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = (π + π₯) β ((π β§ π β β) β (π β§ (π + π₯) β β))) |
327 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + π₯) β (π + π) = ((π + π₯) + π)) |
328 | 327 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + π₯) β (πΉβ(π + π)) = (πΉβ((π + π₯) + π))) |
329 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + π₯) β (πΉβπ ) = (πΉβ(π + π₯))) |
330 | 328, 329 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
β’ (π = (π + π₯) β ((πΉβ(π + π)) = (πΉβπ ) β (πΉβ((π + π₯) + π)) = (πΉβ(π + π₯)))) |
331 | 326, 330 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = (π + π₯) β (((π β§ π β β) β (πΉβ(π + π)) = (πΉβπ )) β ((π β§ (π + π₯) β β) β (πΉβ((π + π₯) + π)) = (πΉβ(π + π₯))))) |
332 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β β β π β β)) |
333 | 332 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((π β§ π₯ β β) β (π β§ π β β))) |
334 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π₯ + π) = (π + π)) |
335 | 334 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πΉβ(π₯ + π)) = (πΉβ(π + π))) |
336 | | fveq2 6889 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ )) |
337 | 335, 336 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ(π + π)) = (πΉβπ ))) |
338 | 333, 337 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ π β β) β (πΉβ(π + π)) = (πΉβπ )))) |
339 | | fourierdlem111.fper |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
340 | 338, 339 | chvarvv 2003 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβ(π + π)) = (πΉβπ )) |
341 | 331, 340 | vtoclg 3557 |
. . . . . . . . . . . . 13
β’ ((π + π₯) β β β ((π β§ (π + π₯) β β) β (πΉβ((π + π₯) + π)) = (πΉβ(π + π₯)))) |
342 | 200, 324,
341 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (πΉβ((π + π₯) + π)) = (πΉβ(π + π₯))) |
343 | 322, 342 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (πΉβ(π + π₯)) = (πΉβ(π + (π₯ + π)))) |
344 | 343 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβ(π + π₯)) = (πΉβ(π + (π₯ + π)))) |
345 | 67, 302 | dirkerper 44799 |
. . . . . . . . . . . 12
β’ ((π β β β§ π₯ β β) β ((π·βπ)β(π₯ + π)) = ((π·βπ)βπ₯)) |
346 | 345 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((π β β β§ π₯ β β) β ((π·βπ)βπ₯) = ((π·βπ)β(π₯ + π))) |
347 | 346 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((π·βπ)βπ₯) = ((π·βπ)β(π₯ + π))) |
348 | 344, 347 | oveq12d 7424 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) = ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π)))) |
349 | 192 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β πΊ = (π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ )))) |
350 | | oveq2 7414 |
. . . . . . . . . . . . . 14
β’ (π = (π₯ + π) β (π + π ) = (π + (π₯ + π))) |
351 | 350 | fveq2d 6893 |
. . . . . . . . . . . . 13
β’ (π = (π₯ + π) β (πΉβ(π + π )) = (πΉβ(π + (π₯ + π)))) |
352 | | fveq2 6889 |
. . . . . . . . . . . . 13
β’ (π = (π₯ + π) β ((π·βπ)βπ ) = ((π·βπ)β(π₯ + π))) |
353 | 351, 352 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ (π = (π₯ + π) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π)))) |
354 | 353 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π₯ β β) β§ π = (π₯ + π)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π)))) |
355 | 316 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β π β β) |
356 | 309, 355 | readdcld 11240 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ + π) β β) |
357 | 316 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β π β β) |
358 | 199, 357 | readdcld 11240 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β (π₯ + π) β β) |
359 | 198, 358 | readdcld 11240 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (π + (π₯ + π)) β β) |
360 | 197, 359 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (πΉβ(π + (π₯ + π))) β β) |
361 | 360 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβ(π + (π₯ + π))) β β) |
362 | 77 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β β) β (π·βπ):ββΆβ) |
363 | 362, 356 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β β) β ((π·βπ)β(π₯ + π)) β β) |
364 | 363 | recnd 11239 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β ((π·βπ)β(π₯ + π)) β β) |
365 | 361, 364 | mulcld 11231 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π))) β β) |
366 | 349, 354,
356, 365 | fvmptd 7003 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβ(π₯ + π)) = ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π)))) |
367 | 366 | eqcomd 2739 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + (π₯ + π))) Β· ((π·βπ)β(π₯ + π))) = (πΊβ(π₯ + π))) |
368 | 311, 348,
367 | 3eqtrrd 2778 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβ(π₯ + π)) = (πΊβπ₯)) |
369 | 308, 368 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β (πΊβ(π₯ + ((Ο β π) β (-Ο β π)))) = (πΊβπ₯)) |
370 | 192 | reseq1i 5976 |
. . . . . . . . . 10
β’ (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) βΎ ((πβπ)(,)(πβ(π + 1)))) |
371 | 370 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) βΎ ((πβπ)(,)(πβ(π + 1))))) |
372 | | ioossre 13382 |
. . . . . . . . . 10
β’ ((πβπ)(,)(πβ(π + 1))) β β |
373 | | resmpt 6036 |
. . . . . . . . . 10
β’ (((πβπ)(,)(πβ(π + 1))) β β β ((π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ )))) |
374 | 372, 373 | ax-mp 5 |
. . . . . . . . 9
β’ ((π β β β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
375 | 371, 374 | eqtrdi 2789 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ )))) |
376 | 271 | rexrd 11261 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
377 | 376 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
378 | 274 | rexrd 11261 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
379 | 378 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
380 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
381 | | elioore 13351 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π β β) |
382 | 381 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
383 | 380, 382 | readdcld 11240 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
384 | 383 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β β) |
385 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯ β ((πβπ)(,)(πβ(π + 1))) β π β ((πβπ)(,)(πβ(π + 1))))) |
386 | 385 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β ((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))))) |
387 | 187 | breq2d 5160 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((πβπ) < (π + π₯) β (πβπ) < (π + π ))) |
388 | 386, 387 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π₯)) β (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )))) |
389 | 149 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β π β β) |
390 | 281, 279 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
391 | 390 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
392 | 389, 391 | addcomd 11413 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (π + (πβπ)) = ((πβπ) + π)) |
393 | 281 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β ((πβπ) + π) = (((πβπ) β π) + π)) |
394 | 271 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
395 | 394, 389 | npcand 11572 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (((πβπ) β π) + π) = (πβπ)) |
396 | 392, 393,
395 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) = (π + (πβπ))) |
397 | 396 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
398 | 390 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
399 | | elioore 13351 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β π₯ β β) |
400 | 399 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π₯ β β) |
401 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
402 | 390 | rexrd 11261 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
403 | 402 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
404 | 291, 290 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
405 | 404 | rexrd 11261 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
406 | 405 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
407 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π₯ β ((πβπ)(,)(πβ(π + 1)))) |
408 | | ioogtlb 44195 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π₯) |
409 | 403, 406,
407, 408 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π₯) |
410 | 398, 400,
401, 409 | ltadd2dd 11370 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π₯)) |
411 | 397, 410 | eqbrtrd 5170 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π₯)) |
412 | 388, 411 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π )) |
413 | 187 | breq1d 5158 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((π + π₯) < (πβ(π + 1)) β (π + π ) < (πβ(π + 1)))) |
414 | 386, 413 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) < (πβ(π + 1))) β (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))))) |
415 | 404 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
416 | | iooltub 44210 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π₯ < (πβ(π + 1))) |
417 | 403, 406,
407, 416 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π₯ < (πβ(π + 1))) |
418 | 400, 415,
401, 417 | ltadd2dd 11370 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) < (π + (πβ(π + 1)))) |
419 | 404 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
420 | 389, 419 | addcomd 11413 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = ((πβ(π + 1)) + π)) |
421 | 291 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) + π) = (((πβ(π + 1)) β π) + π)) |
422 | 274 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
423 | 422, 389 | npcand 11572 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (((πβ(π + 1)) β π) + π) = (πβ(π + 1))) |
424 | 420, 421,
423 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
425 | 424 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
426 | 418, 425 | breqtrd 5174 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) < (πβ(π + 1))) |
427 | 414, 426 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) < (πβ(π + 1))) |
428 | 377, 379,
384, 412, 427 | eliood 44198 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π + π ) β ((πβπ)(,)(πβ(π + 1)))) |
429 | 187 | cbvmptv 5261 |
. . . . . . . . . . . . 13
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π )) |
430 | 429 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π ))) |
431 | | ioossre 13382 |
. . . . . . . . . . . . . . 15
β’ ((πβπ)(,)(πβ(π + 1))) β β |
432 | 431 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ)(,)(πβ(π + 1))) β β) |
433 | 11, 432 | feqresmpt 6959 |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβπ₯))) |
434 | 433 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβπ₯))) |
435 | | fveq2 6889 |
. . . . . . . . . . . 12
β’ (π₯ = (π + π ) β (πΉβπ₯) = (πΉβ(π + π ))) |
436 | 428, 430,
434, 435 | fmptco 7124 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π )))) |
437 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π₯ β β β¦ (π + π₯)) = (π₯ β β β¦ (π + π₯)) |
438 | | ssid 4004 |
. . . . . . . . . . . . . . . . 17
β’ β
β β |
439 | 438 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
β) |
440 | 439, 149,
439 | constcncfg 44575 |
. . . . . . . . . . . . . . 15
β’ (π β (π₯ β β β¦ π) β (ββcnββ)) |
441 | | cncfmptid 24421 |
. . . . . . . . . . . . . . . . 17
β’ ((β
β β β§ β β β) β (π₯ β β β¦ π₯) β (ββcnββ)) |
442 | 438, 438,
441 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β¦ π₯) β (ββcnββ) |
443 | 442 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (π₯ β β β¦ π₯) β (ββcnββ)) |
444 | 440, 443 | addcncf 24953 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β β β¦ (π + π₯)) β (ββcnββ)) |
445 | 444 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (π₯ β β β¦ (π + π₯)) β (ββcnββ)) |
446 | | ioosscn 13383 |
. . . . . . . . . . . . . 14
β’ ((πβπ)(,)(πβ(π + 1))) β β |
447 | 446 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
448 | | ioosscn 13383 |
. . . . . . . . . . . . . 14
β’ ((πβπ)(,)(πβ(π + 1))) β β |
449 | 448 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
450 | 376 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
451 | 378 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
452 | 64 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
453 | 399 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β π₯ β β) |
454 | 452, 453 | readdcld 11240 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β β) |
455 | 454 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β β) |
456 | 450, 451,
455, 411, 426 | eliood 44198 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β ((πβπ)(,)(πβ(π + 1)))) |
457 | 437, 445,
447, 449, 456 | cncfmptssg 44574 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) β (((πβπ)(,)(πβ(π + 1)))βcnβ((πβπ)(,)(πβ(π + 1))))) |
458 | 457, 49 | cncfco 24415 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
459 | 436, 458 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
460 | 459 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
461 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β β β¦ ((π·βπ)βπ )) = (π β β β¦ ((π·βπ)βπ )) |
462 | 77 | feqmptd 6958 |
. . . . . . . . . . . 12
β’ (π β β β (π·βπ) = (π β β β¦ ((π·βπ)βπ ))) |
463 | | cncfss 24407 |
. . . . . . . . . . . . . 14
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
464 | 34, 438, 463 | mp2an 691 |
. . . . . . . . . . . . 13
β’
(ββcnββ)
β (ββcnββ) |
465 | 67 | dirkercncf 44810 |
. . . . . . . . . . . . 13
β’ (π β β β (π·βπ) β (ββcnββ)) |
466 | 464, 465 | sselid 3980 |
. . . . . . . . . . . 12
β’ (π β β β (π·βπ) β (ββcnββ)) |
467 | 462, 466 | eqeltrrd 2835 |
. . . . . . . . . . 11
β’ (π β β β (π β β β¦ ((π·βπ)βπ )) β (ββcnββ)) |
468 | 372 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β ((πβπ)(,)(πβ(π + 1))) β β) |
469 | 438 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β β
β β) |
470 | | cncff 24401 |
. . . . . . . . . . . . . 14
β’ ((π·βπ) β (ββcnββ) β (π·βπ):ββΆβ) |
471 | 466, 470 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β (π·βπ):ββΆβ) |
472 | 471 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π·βπ):ββΆβ) |
473 | 381 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
474 | 472, 473 | ffvelcdmd 7085 |
. . . . . . . . . . 11
β’ ((π β β β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((π·βπ)βπ ) β β) |
475 | 461, 467,
468, 469, 474 | cncfmptssg 44574 |
. . . . . . . . . 10
β’ (π β β β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π·βπ)βπ )) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
476 | 475 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((π·βπ)βπ )) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
477 | 460, 476 | mulcncf 24955 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
478 | 375, 477 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
479 | 453, 201 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π₯)) β β) |
480 | 479 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π₯)) β β) |
481 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) |
482 | 480, 481 | fmptd 7111 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
483 | 482 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
484 | 77 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β (π·βπ):ββΆβ) |
485 | 372 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β β) |
486 | 484, 485 | fssresd 6756 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
487 | 34 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β β β
β) |
488 | 486, 487 | fssd 6733 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
489 | | eqid 2733 |
. . . . . . . . 9
β’ (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) |
490 | | fdm 6724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ:ββΆβ β
dom πΉ =
β) |
491 | 36, 490 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom πΉ = β) |
492 | 431, 491 | sseqtrrid 4035 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((πβπ)(,)(πβ(π + 1))) β dom πΉ) |
493 | | ssdmres 6003 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ)(,)(πβ(π + 1))) β dom πΉ β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
494 | 492, 493 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
495 | 494 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πβπ)(,)(πβ(π + 1))) = dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
496 | 495 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β ((πβπ)(,)(πβ(π + 1))) = dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
497 | 456, 496 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1))))) |
498 | 271 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
499 | 498, 411 | gtned 11346 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β (πβπ)) |
500 | | eldifsn 4790 |
. . . . . . . . . . . . . . 15
β’ ((π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)}) β ((π + π₯) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β§ (π + π₯) β (πβπ))) |
501 | 497, 499,
500 | sylanbrc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)})) |
502 | 501 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)})) |
503 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) |
504 | 503 | rnmptss 7119 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
((πβπ)(,)(πβ(π + 1)))(π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)}) β ran (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)})) |
505 | 502, 504 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ran (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβπ)})) |
506 | | eqidd 2734 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))) |
507 | | oveq2 7414 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (πβπ) β (π + π₯) = (π + (πβπ))) |
508 | 507 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ = (πβπ)) β (π + π₯) = (π + (πβπ))) |
509 | 390 | leidd 11777 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβπ) β€ (πβπ)) |
510 | 390, 404,
292 | ltled 11359 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβπ) β€ (πβ(π + 1))) |
511 | 390, 404,
390, 509, 510 | eliccd 44204 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (πβπ) β ((πβπ)[,](πβ(π + 1)))) |
512 | 396, 271 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π + (πβπ)) β β) |
513 | 506, 508,
511, 512 | fvmptd 7003 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβπ)) = (π + (πβπ))) |
514 | 396 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (πβπ)) = (πβπ)) |
515 | 513, 514 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) = ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβπ))) |
516 | 390, 404 | iccssred 13408 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β β) |
517 | 516, 34 | sstrdi 3994 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β β) |
518 | 517 | resmptd 6039 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((π₯ β β β¦ (π + π₯)) βΎ ((πβπ)[,](πβ(π + 1)))) = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))) |
519 | | rescncf 24405 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ)[,](πβ(π + 1))) β β β ((π₯ β β β¦ (π + π₯)) β (ββcnββ) β ((π₯ β β β¦ (π + π₯)) βΎ ((πβπ)[,](πβ(π + 1)))) β (((πβπ)[,](πβ(π + 1)))βcnββ))) |
520 | 517, 445,
519 | sylc 65 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((π₯ β β β¦ (π + π₯)) βΎ ((πβπ)[,](πβ(π + 1)))) β (((πβπ)[,](πβ(π + 1)))βcnββ)) |
521 | 518, 520 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) β (((πβπ)[,](πβ(π + 1)))βcnββ)) |
522 | 521, 511 | cnlimci 25398 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβπ)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ))) |
523 | 515, 522 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ))) |
524 | | ioossicc 13407 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) |
525 | | resmpt 6036 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) |
526 | 524, 525 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) |
527 | 526 | eqcomi 2742 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) |
528 | 527 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1))))) |
529 | 528 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ)) = (((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
530 | 149 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β π β β) |
531 | 390 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β (πβπ) β β) |
532 | 404 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β (πβ(π + 1)) β β) |
533 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β π₯ β ((πβπ)[,](πβ(π + 1)))) |
534 | | eliccre 44205 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) β β β§ (πβ(π + 1)) β β β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β π₯ β β) |
535 | 531, 532,
533, 534 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β π₯ β β) |
536 | 535 | recnd 11239 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β π₯ β β) |
537 | 530, 536 | addcld 11230 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)[,](πβ(π + 1)))) β (π + π₯) β β) |
538 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) = (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) |
539 | 537, 538 | fmptd 7111 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)):((πβπ)[,](πβ(π + 1)))βΆβ) |
540 | 390, 404,
292, 539 | limciccioolb 44324 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ))) |
541 | 529, 540 | eqtr2d 2774 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ)) = ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ))) |
542 | 523, 541 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβπ) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβπ))) |
543 | 505, 542,
51 | limccog 44323 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π
β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) limβ (πβπ))) |
544 | 36, 432 | fssresd 6756 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
545 | 544 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
546 | 456, 503 | fmptd 7111 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)):((πβπ)(,)(πβ(π + 1)))βΆ((πβπ)(,)(πβ(π + 1)))) |
547 | | fcompt 7128 |
. . . . . . . . . . . . . 14
β’ (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β§ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)):((πβπ)(,)(πβ(π + 1)))βΆ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) = (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦)))) |
548 | 545, 546,
547 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) = (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦)))) |
549 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) |
550 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (π + π₯) = (π + π¦)) |
551 | 550 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β§ π₯ = π¦) β (π + π₯) = (π + π¦)) |
552 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ β ((πβπ)(,)(πβ(π + 1)))) |
553 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
554 | 372, 552 | sselid 3980 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ β β) |
555 | 553, 554 | readdcld 11240 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + π¦) β β) |
556 | 549, 551,
552, 555 | fvmptd 7003 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦) = (π + π¦)) |
557 | 556 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π¦))) |
558 | 557 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦)) = ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π¦))) |
559 | 376 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
560 | 378 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
561 | 555 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + π¦) β β) |
562 | 396 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) = (π + (πβπ))) |
563 | 390 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β β) |
564 | 554 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ β β) |
565 | 64 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π β β) |
566 | 402 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) β
β*) |
567 | 405 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
568 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ β ((πβπ)(,)(πβ(π + 1)))) |
569 | | ioogtlb 44195 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π¦) |
570 | 566, 567,
568, 569 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < π¦) |
571 | 563, 564,
565, 570 | ltadd2dd 11370 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβπ)) < (π + π¦)) |
572 | 562, 571 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβπ) < (π + π¦)) |
573 | 404 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (πβ(π + 1)) β β) |
574 | | iooltub 44210 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ < (πβ(π + 1))) |
575 | 566, 567,
568, 574 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β π¦ < (πβ(π + 1))) |
576 | 564, 573,
565, 575 | ltadd2dd 11370 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + π¦) < (π + (πβ(π + 1)))) |
577 | 424 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + (πβ(π + 1))) = (πβ(π + 1))) |
578 | 576, 577 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + π¦) < (πβ(π + 1))) |
579 | 559, 560,
561, 572, 578 | eliood 44198 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β (π + π¦) β ((πβπ)(,)(πβ(π + 1)))) |
580 | | fvres 6908 |
. . . . . . . . . . . . . . . . 17
β’ ((π + π¦) β ((πβπ)(,)(πβ(π + 1))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π¦)) = (πΉβ(π + π¦))) |
581 | 579, 580 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β(π + π¦)) = (πΉβ(π + π¦))) |
582 | 558, 581 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π¦ β ((πβπ)(,)(πβ(π + 1)))) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦)) = (πΉβ(π + π¦))) |
583 | 582 | mpteq2dva 5248 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦))) = (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π¦)))) |
584 | 550 | fveq2d 6893 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π¦ β (πΉβ(π + π₯)) = (πΉβ(π + π¦))) |
585 | 584 | cbvmptv 5261 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) = (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π¦))) |
586 | 583, 585 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (π¦ β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))β((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))βπ¦))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))) |
587 | 548, 586 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))) |
588 | 587 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) limβ (πβπ)) = ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβπ))) |
589 | 543, 588 | eleqtrd 2836 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π
β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβπ))) |
590 | 589 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β π
β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβπ))) |
591 | | fvres 6908 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β ((πβπ)[,](πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβπ)) = ((π·βπ)β(πβπ))) |
592 | 511, 591 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβπ)) = ((π·βπ)β(πβπ))) |
593 | 592 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((π·βπ)β(πβπ)) = (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβπ))) |
594 | 593 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ)β(πβπ)) = (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβπ))) |
595 | 516 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (0..^π)) β ((πβπ)[,](πβ(π + 1))) β β) |
596 | 465 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (0..^π)) β (π·βπ) β (ββcnββ)) |
597 | | rescncf 24405 |
. . . . . . . . . . . . 13
β’ (((πβπ)[,](πβ(π + 1))) β β β ((π·βπ) β (ββcnββ) β ((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) β (((πβπ)[,](πβ(π + 1)))βcnββ))) |
598 | 595, 596,
597 | sylc 65 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) β (((πβπ)[,](πβ(π + 1)))βcnββ)) |
599 | 511 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβπ) β ((πβπ)[,](πβ(π + 1)))) |
600 | 598, 599 | cnlimci 25398 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβπ)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβπ))) |
601 | 594, 600 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ)β(πβπ)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβπ))) |
602 | 524 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1)))) |
603 | 602 | resabs1d 6011 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))) |
604 | 603 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) = (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1))))) |
605 | 604 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
606 | 605 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
607 | 390 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβπ) β β) |
608 | 404 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβ(π + 1)) β β) |
609 | 292 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
610 | 471 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (0..^π)) β (π·βπ):ββΆβ) |
611 | 610, 595 | fssresd 6756 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))):((πβπ)[,](πβ(π + 1)))βΆβ) |
612 | 607, 608,
609, 611 | limciccioolb 44324 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ)) = (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβπ))) |
613 | 606, 612 | eqtr2d 2774 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβπ)) = (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
614 | 601, 613 | eleqtrd 2836 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ)β(πβπ)) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
615 | 483, 488,
489, 590, 614 | mullimcf 44326 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β (π
Β· ((π·βπ)β(πβπ))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) limβ (πβπ))) |
616 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) = (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))) |
617 | 188 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β§ π₯ = π ) β (πΉβ(π + π₯)) = (πΉβ(π + π ))) |
618 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β π β ((πβπ)(,)(πβ(π + 1)))) |
619 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β πΉ:ββΆβ) |
620 | 619, 383 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
621 | 620 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (πΉβ(π + π )) β β) |
622 | 616, 617,
618, 621 | fvmptd 7003 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) = (πΉβ(π + π ))) |
623 | 622 | adantllr 718 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) = (πΉβ(π + π ))) |
624 | | fvres 6908 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ)(,)(πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ) = ((π·βπ)βπ )) |
625 | 624 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ) = ((π·βπ)βπ )) |
626 | 623, 625 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ )) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
627 | 626 | eqcomd 2739 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π β (0..^π)) β§ π β ((πβπ)(,)(πβ(π + 1)))) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) |
628 | 627 | mpteq2dva 5248 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) = (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ )))) |
629 | 375, 628 | eqtr2d 2774 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β (π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) = (πΊ βΎ ((πβπ)(,)(πβ(π + 1))))) |
630 | 629 | oveq1d 7421 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) limβ (πβπ)) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
631 | 615, 630 | eleqtrd 2836 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (0..^π)) β (π
Β· ((π·βπ)β(πβπ))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
632 | 455, 426 | ltned 11347 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β (πβ(π + 1))) |
633 | | eldifsn 4790 |
. . . . . . . . . . . . . . 15
β’ ((π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))}) β ((π + π₯) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β§ (π + π₯) β (πβ(π + 1)))) |
634 | 497, 632,
633 | sylanbrc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β ((πβπ)(,)(πβ(π + 1)))) β (π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))})) |
635 | 634 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β βπ₯ β ((πβπ)(,)(πβ(π + 1)))(π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))})) |
636 | 503 | rnmptss 7119 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
((πβπ)(,)(πβ(π + 1)))(π + π₯) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))}) β ran (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))})) |
637 | 635, 636 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ran (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) β (dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β {(πβ(π + 1))})) |
638 | 404 | leidd 11777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β€ (πβ(π + 1))) |
639 | 390, 404,
404, 510, 638 | eliccd 44204 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β ((πβπ)[,](πβ(π + 1)))) |
640 | 521, 639 | cnlimci 25398 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβ(π + 1))) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1)))) |
641 | | oveq2 7414 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πβ(π + 1)) β (π + π₯) = (π + (πβ(π + 1)))) |
642 | 641 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ = (πβ(π + 1))) β (π + π₯) = (π + (πβ(π + 1)))) |
643 | 275, 404 | readdcld 11240 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (πβ(π + 1))) β β) |
644 | 506, 642,
639, 643 | fvmptd 7003 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβ(π + 1))) = (π + (πβ(π + 1)))) |
645 | 644, 424 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯))β(πβ(π + 1))) = (πβ(π + 1))) |
646 | 528 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1))) = (((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
647 | 390, 404,
292, 539 | limcicciooub 44340 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1)))) |
648 | 646, 647 | eqtr2d 2774 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π₯ β ((πβπ)[,](πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1))) = ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1)))) |
649 | 640, 645,
648 | 3eltr3d 2848 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯)) limβ (πβ(π + 1)))) |
650 | 637, 649,
54 | limccog 44323 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β πΏ β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) limβ (πβ(π + 1)))) |
651 | 587 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (π + π₯))) limβ (πβ(π + 1))) = ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβ(π + 1)))) |
652 | 650, 651 | eleqtrd 2836 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β πΏ β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβ(π + 1)))) |
653 | 652 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β πΏ β ((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯))) limβ (πβ(π + 1)))) |
654 | 639 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβ(π + 1)) β ((πβπ)[,](πβ(π + 1)))) |
655 | 598, 654 | cnlimci 25398 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβ(π + 1)))) |
656 | | fvres 6908 |
. . . . . . . . . . 11
β’ ((πβ(π + 1)) β ((πβπ)[,](πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβ(π + 1))) = ((π·βπ)β(πβ(π + 1)))) |
657 | 654, 656 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1))))β(πβ(π + 1))) = ((π·βπ)β(πβ(π + 1)))) |
658 | 607, 608,
609, 611 | limcicciooub 44340 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβ(π + 1)))) |
659 | 658 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβ(π + 1))) = ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
660 | | resabs1 6010 |
. . . . . . . . . . . . 13
β’ (((πβπ)(,)(πβ(π + 1))) β ((πβπ)[,](πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))) |
661 | 524, 660 | mp1i 13 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) = ((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))) |
662 | 661 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0..^π)) β ((((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1))) = (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
663 | 659, 662 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0..^π)) β (((π·βπ) βΎ ((πβπ)[,](πβ(π + 1)))) limβ (πβ(π + 1))) = (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
664 | 655, 657,
663 | 3eltr3d 2848 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π·βπ)β(πβ(π + 1))) β (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
665 | 483, 488,
489, 653, 664 | mullimcf 44326 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΏ Β· ((π·βπ)β(πβ(π + 1)))) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) limβ (πβ(π + 1)))) |
666 | 629 | oveq1d 7421 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0..^π)) β ((π β ((πβπ)(,)(πβ(π + 1))) β¦ (((π₯ β ((πβπ)(,)(πβ(π + 1))) β¦ (πΉβ(π + π₯)))βπ ) Β· (((π·βπ) βΎ ((πβπ)(,)(πβ(π + 1))))βπ ))) limβ (πβ(π + 1))) = ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
667 | 665, 666 | eleqtrd 2836 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (0..^π)) β (πΏ Β· ((π·βπ)β(πβ(π + 1)))) β ((πΊ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβ(π + 1)))) |
668 | 125, 128,
221, 222, 223, 109, 298, 207, 369, 478, 631, 667 | fourierdlem110 44919 |
. . . . . 6
β’ ((π β§ π β β) β β«(((-Ο β
π) β -π)[,]((Ο β π) β -π))(πΊβπ₯) dπ₯ = β«((-Ο β π)[,](Ο β π))(πΊβπ₯) dπ₯) |
669 | 668 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π β β) β β«((-Ο β
π)[,](Ο β π))(πΊβπ₯) dπ₯ = β«(((-Ο β π) β -π)[,]((Ο β π) β -π))(πΊβπ₯) dπ₯) |
670 | 124 | recnd 11239 |
. . . . . . . . . 10
β’ (π β (-Ο β π) β
β) |
671 | 670, 149 | subnegd 11575 |
. . . . . . . . 9
β’ (π β ((-Ο β π) β -π) = ((-Ο β π) + π)) |
672 | 151, 149 | npcand 11572 |
. . . . . . . . 9
β’ (π β ((-Ο β π) + π) = -Ο) |
673 | 671, 672 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((-Ο β π) β -π) = -Ο) |
674 | 127 | recnd 11239 |
. . . . . . . . . 10
β’ (π β (Ο β π) β
β) |
675 | 674, 149 | subnegd 11575 |
. . . . . . . . 9
β’ (π β ((Ο β π) β -π) = ((Ο β π) + π)) |
676 | 150, 149 | npcand 11572 |
. . . . . . . . 9
β’ (π β ((Ο β π) + π) = Ο) |
677 | 675, 676 | eqtrd 2773 |
. . . . . . . 8
β’ (π β ((Ο β π) β -π) = Ο) |
678 | 673, 677 | oveq12d 7424 |
. . . . . . 7
β’ (π β (((-Ο β π) β -π)[,]((Ο β π) β -π)) = (-Ο[,]Ο)) |
679 | 678 | itgeq1d 44660 |
. . . . . 6
β’ (π β β«(((-Ο β
π) β -π)[,]((Ο β π) β -π))(πΊβπ₯) dπ₯ = β«(-Ο[,]Ο)(πΊβπ₯) dπ₯) |
680 | 679 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β β«(((-Ο β
π) β -π)[,]((Ο β π) β -π))(πΊβπ₯) dπ₯ = β«(-Ο[,]Ο)(πΊβπ₯) dπ₯) |
681 | 669, 680 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β β«((-Ο β
π)[,](Ο β π))(πΊβπ₯) dπ₯ = β«(-Ο[,]Ο)(πΊβπ₯) dπ₯) |
682 | | fveq2 6889 |
. . . . . 6
β’ (π₯ = π β (πΊβπ₯) = (πΊβπ )) |
683 | 682 | cbvitgv 25286 |
. . . . 5
β’
β«(-Ο(,)Ο)(πΊβπ₯) dπ₯ = β«(-Ο(,)Ο)(πΊβπ ) dπ |
684 | 207 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (-Ο[,]Ο)) β πΊ:ββΆβ) |
685 | 28 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (-Ο[,]Ο)) β π₯ β
β) |
686 | 684, 685 | ffvelcdmd 7085 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β (-Ο[,]Ο)) β (πΊβπ₯) β β) |
687 | 71, 72, 686 | itgioo 25325 |
. . . . 5
β’ ((π β§ π β β) β
β«(-Ο(,)Ο)(πΊβπ₯) dπ₯ = β«(-Ο[,]Ο)(πΊβπ₯) dπ₯) |
688 | | elioore 13351 |
. . . . . . . 8
β’ (π β (-Ο(,)Ο) β
π β
β) |
689 | 688 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β π β
β) |
690 | 36 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (-Ο(,)Ο)) β πΉ:ββΆβ) |
691 | 64 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (-Ο(,)Ο)) β π β
β) |
692 | 688 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β (-Ο(,)Ο)) β π β
β) |
693 | 691, 692 | readdcld 11240 |
. . . . . . . . . 10
β’ ((π β§ π β (-Ο(,)Ο)) β (π + π ) β β) |
694 | 690, 693 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ ((π β§ π β (-Ο(,)Ο)) β (πΉβ(π + π )) β β) |
695 | 694 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β (πΉβ(π + π )) β β) |
696 | 77 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β (π·βπ):ββΆβ) |
697 | 696, 689 | ffvelcdmd 7085 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β ((π·βπ)βπ ) β β) |
698 | 697 | recnd 11239 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β ((π·βπ)βπ ) β β) |
699 | 695, 698 | mulcld 11231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
700 | 689, 699,
193 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (-Ο(,)Ο)) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
701 | 700 | itgeq2dv 25291 |
. . . . 5
β’ ((π β§ π β β) β
β«(-Ο(,)Ο)(πΊβπ ) dπ = β«(-Ο(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
702 | 683, 687,
701 | 3eqtr3a 2797 |
. . . 4
β’ ((π β§ π β β) β
β«(-Ο[,]Ο)(πΊβπ₯) dπ₯ = β«(-Ο(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
703 | 220, 681,
702 | 3eqtrd 2777 |
. . 3
β’ ((π β§ π β β) β β«((-Ο β
π)(,)(Ο β π))((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = β«(-Ο(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
704 | 70, 173, 703 | 3eqtrd 2777 |
. 2
β’ ((π β§ π β β) β (πβπ) = β«(-Ο(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ ) |
705 | 72 | renegcld 11638 |
. . 3
β’ ((π β§ π β β) β -Ο β
β) |
706 | | 0red 11214 |
. . . 4
β’ ((π β§ π β β) β 0 β
β) |
707 | | 0re 11213 |
. . . . . 6
β’ 0 β
β |
708 | | negpilt0 43977 |
. . . . . 6
β’ -Ο
< 0 |
709 | 23, 707, 708 | ltleii 11334 |
. . . . 5
β’ -Ο
β€ 0 |
710 | 709 | a1i 11 |
. . . 4
β’ ((π β§ π β β) β -Ο β€
0) |
711 | | pipos 25962 |
. . . . . 6
β’ 0 <
Ο |
712 | 707, 22, 711 | ltleii 11334 |
. . . . 5
β’ 0 β€
Ο |
713 | 712 | a1i 11 |
. . . 4
β’ ((π β§ π β β) β 0 β€
Ο) |
714 | 71, 72, 706, 710, 713 | eliccd 44204 |
. . 3
β’ ((π β§ π β β) β 0 β
(-Ο[,]Ο)) |
715 | | ioossicc 13407 |
. . . . 5
β’
(-Ο(,)0) β (-Ο[,]0) |
716 | 715 | a1i 11 |
. . . 4
β’ ((π β§ π β β) β (-Ο(,)0) β
(-Ο[,]0)) |
717 | | ioombl 25074 |
. . . . 5
β’
(-Ο(,)0) β dom vol |
718 | 717 | a1i 11 |
. . . 4
β’ ((π β§ π β β) β (-Ο(,)0) β
dom vol) |
719 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (-Ο[,]0)) β πΉ:ββΆβ) |
720 | 64 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (-Ο[,]0)) β π β β) |
721 | 23 | a1i 11 |
. . . . . . . . . 10
β’ (π β (-Ο[,]0) β -Ο
β β) |
722 | | 0red 11214 |
. . . . . . . . . 10
β’ (π β (-Ο[,]0) β 0
β β) |
723 | | id 22 |
. . . . . . . . . 10
β’ (π β (-Ο[,]0) β π β
(-Ο[,]0)) |
724 | | eliccre 44205 |
. . . . . . . . . 10
β’ ((-Ο
β β β§ 0 β β β§ π β (-Ο[,]0)) β π β
β) |
725 | 721, 722,
723, 724 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (-Ο[,]0) β π β
β) |
726 | 725 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (-Ο[,]0)) β π β
β) |
727 | 720, 726 | readdcld 11240 |
. . . . . . 7
β’ ((π β§ π β (-Ο[,]0)) β (π + π ) β β) |
728 | 719, 727 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β (-Ο[,]0)) β (πΉβ(π + π )) β β) |
729 | 728 | adantlr 714 |
. . . . 5
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β (πΉβ(π + π )) β β) |
730 | 77 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β (π·βπ):ββΆβ) |
731 | 725 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β π β
β) |
732 | 730, 731 | ffvelcdmd 7085 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β ((π·βπ)βπ ) β β) |
733 | 732 | recnd 11239 |
. . . . 5
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β ((π·βπ)βπ ) β β) |
734 | 729, 733 | mulcld 11231 |
. . . 4
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
735 | 731, 734,
193 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
736 | 735 | eqcomd 2739 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (-Ο[,]0)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = (πΊβπ )) |
737 | 736 | mpteq2dva 5248 |
. . . . 5
β’ ((π β§ π β β) β (π β (-Ο[,]0) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) = (π β (-Ο[,]0) β¦ (πΊβπ ))) |
738 | 305 | oveq2d 7422 |
. . . . . . . . 9
β’ (π β (π + ((Ο β π) β (-Ο β π))) = (π + π)) |
739 | 738 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β (π + ((Ο β π) β (-Ο β π))) = (π + π)) |
740 | 739 | fveq2d 6893 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β β) β (πΊβ(π + ((Ο β π) β (-Ο β π)))) = (πΊβ(π + π))) |
741 | 186 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β πΊ = (π₯ β β β¦ ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)))) |
742 | | oveq2 7414 |
. . . . . . . . . . 11
β’ (π₯ = (π + π) β (π + π₯) = (π + (π + π))) |
743 | 742 | fveq2d 6893 |
. . . . . . . . . 10
β’ (π₯ = (π + π) β (πΉβ(π + π₯)) = (πΉβ(π + (π + π)))) |
744 | | fveq2 6889 |
. . . . . . . . . 10
β’ (π₯ = (π + π) β ((π·βπ)βπ₯) = ((π·βπ)β(π + π))) |
745 | 743, 744 | oveq12d 7424 |
. . . . . . . . 9
β’ (π₯ = (π + π) β ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) = ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π)))) |
746 | 745 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π β β) β§ π₯ = (π + π)) β ((πΉβ(π + π₯)) Β· ((π·βπ)βπ₯)) = ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π)))) |
747 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
748 | 316 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
749 | 747, 748 | readdcld 11240 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π + π) β β) |
750 | 749 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β (π + π) β β) |
751 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΉ:ββΆβ) |
752 | 64 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
753 | 752, 749 | readdcld 11240 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π + (π + π)) β β) |
754 | 751, 753 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβ(π + (π + π))) β β) |
755 | 754 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β (πΉβ(π + (π + π))) β β) |
756 | 77 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β β) β (π·βπ):ββΆβ) |
757 | 756, 750 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β ((π·βπ)β(π + π)) β β) |
758 | 757 | recnd 11239 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β ((π·βπ)β(π + π)) β β) |
759 | 755, 758 | mulcld 11231 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π))) β β) |
760 | 741, 746,
750, 759 | fvmptd 7003 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β β) β (πΊβ(π + π)) = ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π)))) |
761 | 149 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
762 | 747 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
763 | 318 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β β) |
764 | 761, 762,
763 | addassd 11233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((π + π ) + π) = (π + (π + π))) |
765 | 764 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π + (π + π)) = ((π + π ) + π)) |
766 | 765 | fveq2d 6893 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβ(π + (π + π))) = (πΉβ((π + π ) + π))) |
767 | 752, 747 | readdcld 11240 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π + π ) β β) |
768 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π) |
769 | 768, 767 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π β§ (π + π ) β β)) |
770 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + π ) β (π₯ β β β (π + π ) β β)) |
771 | 770 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + π ) β ((π β§ π₯ β β) β (π β§ (π + π ) β β))) |
772 | | oveq1 7413 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π + π ) β (π₯ + π) = ((π + π ) + π)) |
773 | 772 | fveq2d 6893 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + π ) β (πΉβ(π₯ + π)) = (πΉβ((π + π ) + π))) |
774 | 773, 435 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + π ) β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ((π + π ) + π)) = (πΉβ(π + π )))) |
775 | 771, 774 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π₯ = (π + π ) β (((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ (π + π ) β β) β (πΉβ((π + π ) + π)) = (πΉβ(π + π ))))) |
776 | 775, 339 | vtoclg 3557 |
. . . . . . . . . . . 12
β’ ((π + π ) β β β ((π β§ (π + π ) β β) β (πΉβ((π + π ) + π)) = (πΉβ(π + π )))) |
777 | 767, 769,
776 | sylc 65 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβ((π + π ) + π)) = (πΉβ(π + π ))) |
778 | 766, 777 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβ(π + (π + π))) = (πΉβ(π + π ))) |
779 | 778 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β (πΉβ(π + (π + π))) = (πΉβ(π + π ))) |
780 | 67, 302 | dirkerper 44799 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β ((π·βπ)β(π + π)) = ((π·βπ)βπ )) |
781 | 780 | adantll 713 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β ((π·βπ)β(π + π)) = ((π·βπ)βπ )) |
782 | 779, 781 | oveq12d 7424 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π))) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
783 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β π β β) |
784 | 782, 759 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
785 | 783, 784,
193 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
786 | 785 | eqcomd 2739 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = (πΊβπ )) |
787 | 782, 786 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β β) β ((πΉβ(π + (π + π))) Β· ((π·βπ)β(π + π))) = (πΊβπ )) |
788 | 740, 760,
787 | 3eqtrd 2777 |
. . . . . 6
β’ (((π β§ π β β) β§ π β β) β (πΊβ(π + ((Ο β π) β (-Ο β π)))) = (πΊβπ )) |
789 | | 0ltpnf 13099 |
. . . . . . . 8
β’ 0 <
+β |
790 | | pnfxr 11265 |
. . . . . . . . 9
β’ +β
β β* |
791 | | elioo2 13362 |
. . . . . . . . 9
β’ ((-Ο
β β* β§ +β β β*) β (0
β (-Ο(,)+β) β (0 β β β§ -Ο < 0 β§ 0
< +β))) |
792 | 39, 790, 791 | mp2an 691 |
. . . . . . . 8
β’ (0 β
(-Ο(,)+β) β (0 β β β§ -Ο < 0 β§ 0 <
+β)) |
793 | 707, 708,
789, 792 | mpbir3an 1342 |
. . . . . . 7
β’ 0 β
(-Ο(,)+β) |
794 | 793 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β 0 β
(-Ο(,)+β)) |
795 | 223, 221,
109, 298, 207, 788, 478, 631, 667, 71, 794 | fourierdlem105 44914 |
. . . . 5
β’ ((π β§ π β β) β (π β (-Ο[,]0) β¦ (πΊβπ )) β
πΏ1) |
796 | 737, 795 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β β) β (π β (-Ο[,]0) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
797 | 716, 718,
734, 796 | iblss 25314 |
. . 3
β’ ((π β§ π β β) β (π β (-Ο(,)0) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
798 | | elioore 13351 |
. . . . . . . 8
β’ (π β (0(,)Ο) β π β
β) |
799 | 798 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β π β β) |
800 | 799, 784 | syldan 592 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) β β) |
801 | 799, 800,
193 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β (πΊβπ ) = ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) |
802 | 801 | eqcomd 2739 |
. . . . 5
β’ (((π β§ π β β) β§ π β (0(,)Ο)) β ((πΉβ(π + π )) Β· ((π·βπ)βπ )) = (πΊβπ )) |
803 | 802 | mpteq2dva 5248 |
. . . 4
β’ ((π β§ π β β) β (π β (0(,)Ο) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) = (π β (0(,)Ο) β¦ (πΊβπ ))) |
804 | | ioossicc 13407 |
. . . . . 6
β’
(0(,)Ο) β (0[,]Ο) |
805 | 804 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β (0(,)Ο) β
(0[,]Ο)) |
806 | | ioombl 25074 |
. . . . . 6
β’
(0(,)Ο) β dom vol |
807 | 806 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β (0(,)Ο) β dom
vol) |
808 | 207 | adantr 482 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0[,]Ο)) β πΊ:ββΆβ) |
809 | | 0red 11214 |
. . . . . . . 8
β’ ((π β§ π β (0[,]Ο)) β 0 β
β) |
810 | 22 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (0[,]Ο)) β Ο β
β) |
811 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (0[,]Ο)) β π β (0[,]Ο)) |
812 | | eliccre 44205 |
. . . . . . . 8
β’ ((0
β β β§ Ο β β β§ π β (0[,]Ο)) β π β β) |
813 | 809, 810,
811, 812 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (0[,]Ο)) β π β β) |
814 | 813 | adantlr 714 |
. . . . . 6
β’ (((π β§ π β β) β§ π β (0[,]Ο)) β π β β) |
815 | 808, 814 | ffvelcdmd 7085 |
. . . . 5
β’ (((π β§ π β β) β§ π β (0[,]Ο)) β (πΊβπ ) β β) |
816 | | 0xr 11258 |
. . . . . . . 8
β’ 0 β
β* |
817 | 816 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β 0 β
β*) |
818 | 790 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β +β β
β*) |
819 | 711 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β 0 <
Ο) |
820 | | ltpnf 13097 |
. . . . . . . 8
β’ (Ο
β β β Ο < +β) |
821 | 22, 820 | mp1i 13 |
. . . . . . 7
β’ ((π β§ π β β) β Ο <
+β) |
822 | 817, 818,
72, 819, 821 | eliood 44198 |
. . . . . 6
β’ ((π β§ π β β) β Ο β
(0(,)+β)) |
823 | 223, 221,
109, 298, 207, 788, 478, 631, 667, 706, 822 | fourierdlem105 44914 |
. . . . 5
β’ ((π β§ π β β) β (π β (0[,]Ο) β¦ (πΊβπ )) β
πΏ1) |
824 | 805, 807,
815, 823 | iblss 25314 |
. . . 4
β’ ((π β§ π β β) β (π β (0(,)Ο) β¦ (πΊβπ )) β
πΏ1) |
825 | 803, 824 | eqeltrd 2834 |
. . 3
β’ ((π β§ π β β) β (π β (0(,)Ο) β¦ ((πΉβ(π + π )) Β· ((π·βπ)βπ ))) β
πΏ1) |
826 | 705, 72, 714, 699, 797, 825 | itgsplitioo 25347 |
. 2
β’ ((π β§ π β β) β
β«(-Ο(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |
827 | 704, 826 | eqtrd 2773 |
1
β’ ((π β§ π β β) β (πβπ) = (β«(-Ο(,)0)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ + β«(0(,)Ο)((πΉβ(π + π )) Β· ((π·βπ)βπ )) dπ )) |