Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π β§ (πΈβπ) = π΅) β π) |
2 | | 0zd 12567 |
. . . . . 6
β’ (π β 0 β
β€) |
3 | | fourierdlem48.m |
. . . . . . 7
β’ (π β π β β) |
4 | 3 | nnzd 12582 |
. . . . . 6
β’ (π β π β β€) |
5 | 3 | nngt0d 12258 |
. . . . . 6
β’ (π β 0 < π) |
6 | | fzolb 13635 |
. . . . . 6
β’ (0 β
(0..^π) β (0 β
β€ β§ π β
β€ β§ 0 < π)) |
7 | 2, 4, 5, 6 | syl3anbrc 1344 |
. . . . 5
β’ (π β 0 β (0..^π)) |
8 | 7 | adantr 482 |
. . . 4
β’ ((π β§ (πΈβπ) = π΅) β 0 β (0..^π)) |
9 | | fourierdlem48.b |
. . . . . . . . . 10
β’ (π β π΅ β β) |
10 | | fourierdlem48.x |
. . . . . . . . . 10
β’ (π β π β β) |
11 | 9, 10 | resubcld 11639 |
. . . . . . . . 9
β’ (π β (π΅ β π) β β) |
12 | | fourierdlem48.t |
. . . . . . . . . 10
β’ π = (π΅ β π΄) |
13 | | fourierdlem48.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
14 | 9, 13 | resubcld 11639 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β β) |
15 | 12, 14 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β π β β) |
16 | | fourierdlem48.altb |
. . . . . . . . . . . 12
β’ (π β π΄ < π΅) |
17 | 13, 9 | posdifd 11798 |
. . . . . . . . . . . 12
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
18 | 16, 17 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β 0 < (π΅ β π΄)) |
19 | 18, 12 | breqtrrdi 5190 |
. . . . . . . . . 10
β’ (π β 0 < π) |
20 | 19 | gt0ne0d 11775 |
. . . . . . . . 9
β’ (π β π β 0) |
21 | 11, 15, 20 | redivcld 12039 |
. . . . . . . 8
β’ (π β ((π΅ β π) / π) β β) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΈβπ) = π΅) β ((π΅ β π) / π) β β) |
23 | 22 | flcld 13760 |
. . . . . 6
β’ ((π β§ (πΈβπ) = π΅) β (ββ((π΅ β π) / π)) β β€) |
24 | | 1zzd 12590 |
. . . . . 6
β’ ((π β§ (πΈβπ) = π΅) β 1 β β€) |
25 | 23, 24 | zsubcld 12668 |
. . . . 5
β’ ((π β§ (πΈβπ) = π΅) β ((ββ((π΅ β π) / π)) β 1) β
β€) |
26 | | id 22 |
. . . . . . . 8
β’ ((πΈβπ) = π΅ β (πΈβπ) = π΅) |
27 | 12 | a1i 11 |
. . . . . . . 8
β’ ((πΈβπ) = π΅ β π = (π΅ β π΄)) |
28 | 26, 27 | oveq12d 7424 |
. . . . . . 7
β’ ((πΈβπ) = π΅ β ((πΈβπ) β π) = (π΅ β (π΅ β π΄))) |
29 | 9 | recnd 11239 |
. . . . . . . 8
β’ (π β π΅ β β) |
30 | 13 | recnd 11239 |
. . . . . . . 8
β’ (π β π΄ β β) |
31 | 29, 30 | nncand 11573 |
. . . . . . 7
β’ (π β (π΅ β (π΅ β π΄)) = π΄) |
32 | 28, 31 | sylan9eqr 2795 |
. . . . . 6
β’ ((π β§ (πΈβπ) = π΅) β ((πΈβπ) β π) = π΄) |
33 | | fourierdlem48.q |
. . . . . . . . . . . . . 14
β’ (π β π β (πβπ)) |
34 | | fourierdlem48.p |
. . . . . . . . . . . . . . . 16
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
35 | 34 | fourierdlem2 44812 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
36 | 3, 35 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
37 | 33, 36 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
38 | 37 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β π β (β βm
(0...π))) |
39 | | elmapi 8840 |
. . . . . . . . . . . 12
β’ (π β (β
βm (0...π))
β π:(0...π)βΆβ) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
β’ (π β π:(0...π)βΆβ) |
41 | 3 | nnnn0d 12529 |
. . . . . . . . . . . . 13
β’ (π β π β
β0) |
42 | | nn0uz 12861 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
43 | 41, 42 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β0)) |
44 | | eluzfz1 13505 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
β’ (π β 0 β (0...π)) |
46 | 40, 45 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (π β (πβ0) β β) |
47 | 46 | rexrd 11261 |
. . . . . . . . 9
β’ (π β (πβ0) β
β*) |
48 | | 1zzd 12590 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
49 | | 0le1 11734 |
. . . . . . . . . . . . 13
β’ 0 β€
1 |
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 0 β€ 1) |
51 | 3 | nnge1d 12257 |
. . . . . . . . . . . 12
β’ (π β 1 β€ π) |
52 | 2, 4, 48, 50, 51 | elfzd 13489 |
. . . . . . . . . . 11
β’ (π β 1 β (0...π)) |
53 | 40, 52 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ (π β (πβ1) β β) |
54 | 53 | rexrd 11261 |
. . . . . . . . 9
β’ (π β (πβ1) β
β*) |
55 | 13 | rexrd 11261 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
56 | 37 | simprd 497 |
. . . . . . . . . . 11
β’ (π β (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
57 | 56 | simplld 767 |
. . . . . . . . . 10
β’ (π β (πβ0) = π΄) |
58 | 13 | leidd 11777 |
. . . . . . . . . 10
β’ (π β π΄ β€ π΄) |
59 | 57, 58 | eqbrtrd 5170 |
. . . . . . . . 9
β’ (π β (πβ0) β€ π΄) |
60 | 57 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β π΄ = (πβ0)) |
61 | | 0re 11213 |
. . . . . . . . . . . . 13
β’ 0 β
β |
62 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (π β (0..^π) β 0 β (0..^π))) |
63 | 62 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β ((π β§ π β (0..^π)) β (π β§ 0 β (0..^π)))) |
64 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (πβπ) = (πβ0)) |
65 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π + 1) = (0 + 1)) |
66 | 65 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (πβ(π + 1)) = (πβ(0 + 1))) |
67 | 64, 66 | breq12d 5161 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β ((πβπ) < (πβ(π + 1)) β (πβ0) < (πβ(0 + 1)))) |
68 | 63, 67 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ 0 β (0..^π)) β (πβ0) < (πβ(0 + 1))))) |
69 | 37 | simprrd 773 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
70 | 69 | r19.21bi 3249 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
71 | 68, 70 | vtoclg 3557 |
. . . . . . . . . . . . 13
β’ (0 β
β β ((π β§ 0
β (0..^π)) β
(πβ0) < (πβ(0 +
1)))) |
72 | 61, 71 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β§ 0 β (0..^π)) β (πβ0) < (πβ(0 + 1))) |
73 | 7, 72 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (πβ0) < (πβ(0 + 1))) |
74 | | 1e0p1 12716 |
. . . . . . . . . . . 12
β’ 1 = (0 +
1) |
75 | 74 | fveq2i 6892 |
. . . . . . . . . . 11
β’ (πβ1) = (πβ(0 + 1)) |
76 | 73, 75 | breqtrrdi 5190 |
. . . . . . . . . 10
β’ (π β (πβ0) < (πβ1)) |
77 | 60, 76 | eqbrtrd 5170 |
. . . . . . . . 9
β’ (π β π΄ < (πβ1)) |
78 | 47, 54, 55, 59, 77 | elicod 13371 |
. . . . . . . 8
β’ (π β π΄ β ((πβ0)[,)(πβ1))) |
79 | 75 | oveq2i 7417 |
. . . . . . . 8
β’ ((πβ0)[,)(πβ1)) = ((πβ0)[,)(πβ(0 + 1))) |
80 | 78, 79 | eleqtrdi 2844 |
. . . . . . 7
β’ (π β π΄ β ((πβ0)[,)(πβ(0 + 1)))) |
81 | 80 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΈβπ) = π΅) β π΄ β ((πβ0)[,)(πβ(0 + 1)))) |
82 | 32, 81 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ (πΈβπ) = π΅) β ((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1)))) |
83 | | fourierdlem48.e |
. . . . . . . . . . 11
β’ πΈ = (π₯ β β β¦ (π₯ + (πβπ₯))) |
84 | 83 | a1i 11 |
. . . . . . . . . 10
β’ (π β πΈ = (π₯ β β β¦ (π₯ + (πβπ₯)))) |
85 | | id 22 |
. . . . . . . . . . . 12
β’ (π₯ = π β π₯ = π) |
86 | | fveq2 6889 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
87 | 85, 86 | oveq12d 7424 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ + (πβπ₯)) = (π + (πβπ))) |
88 | 87 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ = π) β (π₯ + (πβπ₯)) = (π + (πβπ))) |
89 | | fourierdlem48.z |
. . . . . . . . . . . . . 14
β’ π = (π₯ β β β¦
((ββ((π΅ β
π₯) / π)) Β· π)) |
90 | 89 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β π = (π₯ β β β¦
((ββ((π΅ β
π₯) / π)) Β· π))) |
91 | | oveq2 7414 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π΅ β π₯) = (π΅ β π)) |
92 | 91 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((π΅ β π₯) / π) = ((π΅ β π) / π)) |
93 | 92 | fveq2d 6893 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (ββ((π΅ β π₯) / π)) = (ββ((π΅ β π) / π))) |
94 | 93 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β π) / π)) Β· π)) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ = π) β ((ββ((π΅ β π₯) / π)) Β· π) = ((ββ((π΅ β π) / π)) Β· π)) |
96 | 21 | flcld 13760 |
. . . . . . . . . . . . . . 15
β’ (π β (ββ((π΅ β π) / π)) β β€) |
97 | 96 | zred 12663 |
. . . . . . . . . . . . . 14
β’ (π β (ββ((π΅ β π) / π)) β β) |
98 | 97, 15 | remulcld 11241 |
. . . . . . . . . . . . 13
β’ (π β ((ββ((π΅ β π) / π)) Β· π) β β) |
99 | 90, 95, 10, 98 | fvmptd 7003 |
. . . . . . . . . . . 12
β’ (π β (πβπ) = ((ββ((π΅ β π) / π)) Β· π)) |
100 | 99, 98 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β (πβπ) β β) |
101 | 10, 100 | readdcld 11240 |
. . . . . . . . . 10
β’ (π β (π + (πβπ)) β β) |
102 | 84, 88, 10, 101 | fvmptd 7003 |
. . . . . . . . 9
β’ (π β (πΈβπ) = (π + (πβπ))) |
103 | 99 | oveq2d 7422 |
. . . . . . . . 9
β’ (π β (π + (πβπ)) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
104 | 102, 103 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (πΈβπ) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
105 | 104 | oveq1d 7421 |
. . . . . . 7
β’ (π β ((πΈβπ) β π) = ((π + ((ββ((π΅ β π) / π)) Β· π)) β π)) |
106 | 10 | recnd 11239 |
. . . . . . . 8
β’ (π β π β β) |
107 | 98 | recnd 11239 |
. . . . . . . 8
β’ (π β ((ββ((π΅ β π) / π)) Β· π) β β) |
108 | 15 | recnd 11239 |
. . . . . . . 8
β’ (π β π β β) |
109 | 106, 107,
108 | addsubassd 11588 |
. . . . . . 7
β’ (π β ((π + ((ββ((π΅ β π) / π)) Β· π)) β π) = (π + (((ββ((π΅ β π) / π)) Β· π) β π))) |
110 | 96 | zcnd 12664 |
. . . . . . . . 9
β’ (π β (ββ((π΅ β π) / π)) β β) |
111 | 110, 108 | mulsubfacd 11672 |
. . . . . . . 8
β’ (π β (((ββ((π΅ β π) / π)) Β· π) β π) = (((ββ((π΅ β π) / π)) β 1) Β· π)) |
112 | 111 | oveq2d 7422 |
. . . . . . 7
β’ (π β (π + (((ββ((π΅ β π) / π)) Β· π) β π)) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π))) |
113 | 105, 109,
112 | 3eqtrd 2777 |
. . . . . 6
β’ (π β ((πΈβπ) β π) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π))) |
114 | 113 | adantr 482 |
. . . . 5
β’ ((π β§ (πΈβπ) = π΅) β ((πΈβπ) β π) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π))) |
115 | | oveq1 7413 |
. . . . . . . . 9
β’ (π = ((ββ((π΅ β π) / π)) β 1) β (π Β· π) = (((ββ((π΅ β π) / π)) β 1) Β· π)) |
116 | 115 | oveq2d 7422 |
. . . . . . . 8
β’ (π = ((ββ((π΅ β π) / π)) β 1) β (π + (π Β· π)) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π))) |
117 | 116 | eqeq2d 2744 |
. . . . . . 7
β’ (π = ((ββ((π΅ β π) / π)) β 1) β (((πΈβπ) β π) = (π + (π Β· π)) β ((πΈβπ) β π) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π)))) |
118 | 117 | anbi2d 630 |
. . . . . 6
β’ (π = ((ββ((π΅ β π) / π)) β 1) β ((((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))) β (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π))))) |
119 | 118 | rspcev 3613 |
. . . . 5
β’
((((ββ((π΅ β π) / π)) β 1) β β€ β§ (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (((ββ((π΅ β π) / π)) β 1) Β· π)))) β βπ β β€ (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) |
120 | 25, 82, 114, 119 | syl12anc 836 |
. . . 4
β’ ((π β§ (πΈβπ) = π΅) β βπ β β€ (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) |
121 | 64, 66 | oveq12d 7424 |
. . . . . . . 8
β’ (π = 0 β ((πβπ)[,)(πβ(π + 1))) = ((πβ0)[,)(πβ(0 + 1)))) |
122 | 121 | eleq2d 2820 |
. . . . . . 7
β’ (π = 0 β (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β ((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))))) |
123 | 122 | anbi1d 631 |
. . . . . 6
β’ (π = 0 β ((((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))) β (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))))) |
124 | 123 | rexbidv 3179 |
. . . . 5
β’ (π = 0 β (βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))) β βπ β β€ (((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))))) |
125 | 124 | rspcev 3613 |
. . . 4
β’ ((0
β (0..^π) β§
βπ β β€
(((πΈβπ) β π) β ((πβ0)[,)(πβ(0 + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) β βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) |
126 | 8, 120, 125 | syl2anc 585 |
. . 3
β’ ((π β§ (πΈβπ) = π΅) β βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) |
127 | | ovex 7439 |
. . . 4
β’ ((πΈβπ) β π) β V |
128 | | eleq1 2822 |
. . . . . . . 8
β’ (π¦ = ((πΈβπ) β π) β (π¦ β ((πβπ)[,)(πβ(π + 1))) β ((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))))) |
129 | | eqeq1 2737 |
. . . . . . . 8
β’ (π¦ = ((πΈβπ) β π) β (π¦ = (π + (π Β· π)) β ((πΈβπ) β π) = (π + (π Β· π)))) |
130 | 128, 129 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = ((πΈβπ) β π) β ((π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))))) |
131 | 130 | 2rexbidv 3220 |
. . . . . 6
β’ (π¦ = ((πΈβπ) β π) β (βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π))))) |
132 | 131 | anbi2d 630 |
. . . . 5
β’ (π¦ = ((πΈβπ) β π) β ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β (π β§ βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))))) |
133 | 132 | imbi1d 342 |
. . . 4
β’ (π¦ = ((πΈβπ) β π) β (((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) β ((π β§ βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
))) |
134 | | simpr 486 |
. . . . 5
β’ ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) |
135 | | nfv 1918 |
. . . . . . 7
β’
β²ππ |
136 | | nfre1 3283 |
. . . . . . 7
β’
β²πβπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) |
137 | 135, 136 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) |
138 | | nfv 1918 |
. . . . . . 7
β’
β²ππ |
139 | | nfcv 2904 |
. . . . . . . 8
β’
β²π(0..^π) |
140 | | nfre1 3283 |
. . . . . . . 8
β’
β²πβπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) |
141 | 139, 140 | nfrexw 3311 |
. . . . . . 7
β’
β²πβπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) |
142 | 138, 141 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) |
143 | | simp1 1137 |
. . . . . . . . . 10
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β π) |
144 | | simp2l 1200 |
. . . . . . . . . 10
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β π β (0..^π)) |
145 | | simp3l 1202 |
. . . . . . . . . 10
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β π¦ β ((πβπ)[,)(πβ(π + 1)))) |
146 | 143, 144,
145 | jca31 516 |
. . . . . . . . 9
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1))))) |
147 | | simp2r 1201 |
. . . . . . . . 9
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β π β β€) |
148 | | simp3r 1203 |
. . . . . . . . 9
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β π¦ = (π + (π Β· π))) |
149 | | fourierdlem48.ch |
. . . . . . . . . 10
β’ (π β ((((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β§ π β β€) β§ π¦ = (π + (π Β· π)))) |
150 | 149 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β§ π β β€) β§ π¦ = (π + (π Β· π)))) |
151 | 150 | simplld 767 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1))))) |
152 | 151 | simplld 767 |
. . . . . . . . . . . . . . . 16
β’ (π β π) |
153 | | fourierdlem48.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:π·βΆβ) |
154 | | frel 6720 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:π·βΆβ β Rel πΉ) |
155 | 152, 153,
154 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β Rel πΉ) |
156 | | resindm 6029 |
. . . . . . . . . . . . . . . 16
β’ (Rel
πΉ β (πΉ βΎ ((π(,)+β) β© dom πΉ)) = (πΉ βΎ (π(,)+β))) |
157 | 156 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (Rel
πΉ β (πΉ βΎ (π(,)+β)) = (πΉ βΎ ((π(,)+β) β© dom πΉ))) |
158 | 155, 157 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ (π(,)+β)) = (πΉ βΎ ((π(,)+β) β© dom πΉ))) |
159 | | fdm 6724 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:π·βΆβ β dom πΉ = π·) |
160 | 152, 153,
159 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β dom πΉ = π·) |
161 | 160 | ineq2d 4212 |
. . . . . . . . . . . . . . 15
β’ (π β ((π(,)+β) β© dom πΉ) = ((π(,)+β) β© π·)) |
162 | 161 | reseq2d 5980 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ ((π(,)+β) β© dom πΉ)) = (πΉ βΎ ((π(,)+β) β© π·))) |
163 | 158, 162 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ (π(,)+β)) = (πΉ βΎ ((π(,)+β) β© π·))) |
164 | 163 | oveq1d 7421 |
. . . . . . . . . . . 12
β’ (π β ((πΉ βΎ (π(,)+β)) limβ π) = ((πΉ βΎ ((π(,)+β) β© π·)) limβ π)) |
165 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:π·βΆβ) |
166 | | ax-resscn 11164 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
167 | 166 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β β β
β) |
168 | 165, 167 | fssd 6733 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:π·βΆβ) |
169 | | inss2 4229 |
. . . . . . . . . . . . . . 15
β’ ((π(,)+β) β© π·) β π· |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β ((π(,)+β) β© π·) β π·) |
171 | 168, 170 | fssresd 6756 |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ ((π(,)+β) β© π·)):((π(,)+β) β© π·)βΆβ) |
172 | | pnfxr 11265 |
. . . . . . . . . . . . . . . 16
β’ +β
β β* |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β +β β
β*) |
174 | 151 | simplrd 769 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (0..^π)) |
175 | 40 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
176 | | fzofzp1 13726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (π + 1) β (0...π)) |
177 | 176 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
178 | 175, 177 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
179 | 152, 174,
178 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πβ(π + 1)) β β) |
180 | 150 | simplrd 769 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β€) |
181 | 180 | zred 12663 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
182 | 152, 15 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
183 | 181, 182 | remulcld 11241 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π Β· π) β β) |
184 | 179, 183 | resubcld 11639 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πβ(π + 1)) β (π Β· π)) β β) |
185 | 184 | rexrd 11261 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβ(π + 1)) β (π Β· π)) β
β*) |
186 | 184 | ltpnfd 13098 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πβ(π + 1)) β (π Β· π)) < +β) |
187 | 185, 173,
186 | xrltled 13126 |
. . . . . . . . . . . . . . 15
β’ (π β ((πβ(π + 1)) β (π Β· π)) β€ +β) |
188 | | iooss2 13357 |
. . . . . . . . . . . . . . 15
β’
((+β β β* β§ ((πβ(π + 1)) β (π Β· π)) β€ +β) β (π(,)((πβ(π + 1)) β (π Β· π))) β (π(,)+β)) |
189 | 173, 187,
188 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) β (π(,)+β)) |
190 | 180 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β€) |
191 | 190 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β) |
192 | 182 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β) |
194 | 191, 193 | mulneg1d 11664 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (-π Β· π) = -(π Β· π)) |
195 | 194 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + (-π Β· π)) = ((π€ + (π Β· π)) + -(π Β· π))) |
196 | | elioore 13351 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β (π(,)((πβ(π + 1)) β (π Β· π))) β π€ β β) |
197 | 196 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (π(,)((πβ(π + 1)) β (π Β· π))) β π€ β β) |
198 | 197 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β β) |
199 | 191, 193 | mulcld 11231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π Β· π) β β) |
200 | 198, 199 | addcld 11230 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β β) |
201 | 200, 199 | negsubd 11574 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + -(π Β· π)) = ((π€ + (π Β· π)) β (π Β· π))) |
202 | 198, 199 | pncand 11569 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) β (π Β· π)) = π€) |
203 | 195, 201,
202 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ = ((π€ + (π Β· π)) + (-π Β· π))) |
204 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π) |
205 | 151 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β§ π β (0..^π))) |
206 | | fourierdlem48.cn |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0..^π)) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
207 | | cncff 24401 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ) β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ) |
208 | | fdm 6724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))):((πβπ)(,)(πβ(π + 1)))βΆβ β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
209 | 206, 207,
208 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0..^π)) β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
210 | | ssdmres 6003 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ)(,)(πβ(π + 1))) β dom πΉ β dom (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) = ((πβπ)(,)(πβ(π + 1)))) |
211 | 209, 210 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β dom πΉ) |
212 | 153, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β dom πΉ = π·) |
213 | 212 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0..^π)) β dom πΉ = π·) |
214 | 211, 213 | sseqtrd 4022 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0..^π)) β ((πβπ)(,)(πβ(π + 1))) β π·) |
215 | 205, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((πβπ)(,)(πβ(π + 1))) β π·) |
216 | 215 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((πβπ)(,)(πβ(π + 1))) β π·) |
217 | | elfzofz 13645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0..^π) β π β (0...π)) |
218 | 217 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
219 | 175, 218 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
220 | 152, 174,
219 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πβπ) β β) |
221 | 220 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πβπ) β
β*) |
222 | 221 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβπ) β
β*) |
223 | 179 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πβ(π + 1)) β
β*) |
224 | 223 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβ(π + 1)) β
β*) |
225 | 196 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β β) |
226 | 190 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β) |
227 | 204, 15 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β) |
228 | 226, 227 | remulcld 11241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π Β· π) β β) |
229 | 225, 228 | readdcld 11240 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β β) |
230 | 220 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβπ) β β) |
231 | 152, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β) |
232 | 231, 183 | readdcld 11240 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π + (π Β· π)) β β) |
233 | 232 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π + (π Β· π)) β β) |
234 | 149 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π¦ = (π + (π Β· π))) |
235 | 234 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π + (π Β· π)) = π¦) |
236 | 151 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π¦ β ((πβπ)[,)(πβ(π + 1)))) |
237 | 235, 236 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π + (π Β· π)) β ((πβπ)[,)(πβ(π + 1)))) |
238 | | icogelb 13372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§
(π + (π Β· π)) β ((πβπ)[,)(πβ(π + 1)))) β (πβπ) β€ (π + (π Β· π))) |
239 | 221, 223,
237, 238 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πβπ) β€ (π + (π Β· π))) |
240 | 239 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβπ) β€ (π + (π Β· π))) |
241 | 204, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β) |
242 | 241 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β
β*) |
243 | 179 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβ(π + 1)) β β) |
244 | 243, 228 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((πβ(π + 1)) β (π Β· π)) β β) |
245 | 244 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((πβ(π + 1)) β (π Β· π)) β
β*) |
246 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) |
247 | | ioogtlb 44195 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β*
β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π < π€) |
248 | 242, 245,
246, 247 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π < π€) |
249 | 241, 225,
228, 248 | ltadd1dd 11822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π + (π Β· π)) < (π€ + (π Β· π))) |
250 | 230, 233,
229, 240, 249 | lelttrd 11369 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πβπ) < (π€ + (π Β· π))) |
251 | | iooltub 44210 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β*
β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ < ((πβ(π + 1)) β (π Β· π))) |
252 | 242, 245,
246, 251 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ < ((πβ(π + 1)) β (π Β· π))) |
253 | 225, 244,
228, 252 | ltadd1dd 11822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) < (((πβ(π + 1)) β (π Β· π)) + (π Β· π))) |
254 | 179 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (πβ(π + 1)) β β) |
255 | 183 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π Β· π) β β) |
256 | 254, 255 | npcand 11572 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((πβ(π + 1)) β (π Β· π)) + (π Β· π)) = (πβ(π + 1))) |
257 | 256 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (((πβ(π + 1)) β (π Β· π)) + (π Β· π)) = (πβ(π + 1))) |
258 | 253, 257 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) < (πβ(π + 1))) |
259 | 222, 224,
229, 250, 258 | eliood 44198 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β ((πβπ)(,)(πβ(π + 1)))) |
260 | 216, 259 | sseldd 3983 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β π·) |
261 | 190 | znegcld 12665 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β -π β β€) |
262 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ + (π Β· π)) β V |
263 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = (π€ + (π Β· π)) β (π₯ β π· β (π€ + (π Β· π)) β π·)) |
264 | 263 | 3anbi2d 1442 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (π€ + (π Β· π)) β ((π β§ π₯ β π· β§ -π β β€) β (π β§ (π€ + (π Β· π)) β π· β§ -π β β€))) |
265 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = (π€ + (π Β· π)) β (π₯ + (-π Β· π)) = ((π€ + (π Β· π)) + (-π Β· π))) |
266 | 265 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (π€ + (π Β· π)) β ((π₯ + (-π Β· π)) β π· β ((π€ + (π Β· π)) + (-π Β· π)) β π·)) |
267 | 264, 266 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = (π€ + (π Β· π)) β (((π β§ π₯ β π· β§ -π β β€) β (π₯ + (-π Β· π)) β π·) β ((π β§ (π€ + (π Β· π)) β π· β§ -π β β€) β ((π€ + (π Β· π)) + (-π Β· π)) β π·))) |
268 | | negex 11455 |
. . . . . . . . . . . . . . . . . . . 20
β’ -π β V |
269 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = -π β (π β β€ β -π β β€)) |
270 | 269 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = -π β ((π β§ π₯ β π· β§ π β β€) β (π β§ π₯ β π· β§ -π β β€))) |
271 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = -π β (π Β· π) = (-π Β· π)) |
272 | 271 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = -π β (π₯ + (π Β· π)) = (π₯ + (-π Β· π))) |
273 | 272 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = -π β ((π₯ + (π Β· π)) β π· β (π₯ + (-π Β· π)) β π·)) |
274 | 270, 273 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = -π β (((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) β ((π β§ π₯ β π· β§ -π β β€) β (π₯ + (-π Β· π)) β π·))) |
275 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (π β β€ β π β β€)) |
276 | 275 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((π β§ π₯ β π· β§ π β β€) β (π β§ π₯ β π· β§ π β β€))) |
277 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π Β· π) = (π Β· π)) |
278 | 277 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (π₯ + (π Β· π)) = (π₯ + (π Β· π))) |
279 | 278 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((π₯ + (π Β· π)) β π· β (π₯ + (π Β· π)) β π·)) |
280 | 276, 279 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) β ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·))) |
281 | | fourierdlem48.dper |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) |
282 | 280, 281 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) |
283 | 268, 274,
282 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π· β§ -π β β€) β (π₯ + (-π Β· π)) β π·) |
284 | 262, 267,
283 | vtocl 3550 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π€ + (π Β· π)) β π· β§ -π β β€) β ((π€ + (π Β· π)) + (-π Β· π)) β π·) |
285 | 204, 260,
261, 284 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + (-π Β· π)) β π·) |
286 | 203, 285 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β π·) |
287 | 286 | ralrimiva 3147 |
. . . . . . . . . . . . . . 15
β’ (π β βπ€ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ β π·) |
288 | | dfss3 3970 |
. . . . . . . . . . . . . . 15
β’ ((π(,)((πβ(π + 1)) β (π Β· π))) β π· β βπ€ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ β π·) |
289 | 287, 288 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) β π·) |
290 | 189, 289 | ssind 4232 |
. . . . . . . . . . . . 13
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) β ((π(,)+β) β© π·)) |
291 | | ioosscn 13383 |
. . . . . . . . . . . . . 14
β’ (π(,)+β) β
β |
292 | | ssinss1 4237 |
. . . . . . . . . . . . . 14
β’ ((π(,)+β) β β
β ((π(,)+β)
β© π·) β
β) |
293 | 291, 292 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (π β ((π(,)+β) β© π·) β β) |
294 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) =
(TopOpenββfld) |
295 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) = ((TopOpenββfld)
βΎt (((π(,)+β) β© π·) βͺ {π})) |
296 | 231 | rexrd 11261 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β*) |
297 | 231 | leidd 11777 |
. . . . . . . . . . . . . . 15
β’ (π β π β€ π) |
298 | 234 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π¦ β (π Β· π)) = ((π + (π Β· π)) β (π Β· π))) |
299 | 231 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
300 | 299, 255 | pncand 11569 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π + (π Β· π)) β (π Β· π)) = π) |
301 | 298, 300 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ (π β π = (π¦ β (π Β· π))) |
302 | | icossre 13402 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) β β β§ (πβ(π + 1)) β β*) β
((πβπ)[,)(πβ(π + 1))) β β) |
303 | 220, 223,
302 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((πβπ)[,)(πβ(π + 1))) β β) |
304 | 303, 236 | sseldd 3983 |
. . . . . . . . . . . . . . . . 17
β’ (π β π¦ β β) |
305 | | icoltub 44208 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β π¦ < (πβ(π + 1))) |
306 | 221, 223,
236, 305 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β π¦ < (πβ(π + 1))) |
307 | 304, 179,
183, 306 | ltsub1dd 11823 |
. . . . . . . . . . . . . . . 16
β’ (π β (π¦ β (π Β· π)) < ((πβ(π + 1)) β (π Β· π))) |
308 | 301, 307 | eqbrtrd 5170 |
. . . . . . . . . . . . . . 15
β’ (π β π < ((πβ(π + 1)) β (π Β· π))) |
309 | 296, 185,
296, 297, 308 | elicod 13371 |
. . . . . . . . . . . . . 14
β’ (π β π β (π[,)((πβ(π + 1)) β (π Β· π)))) |
310 | | snunioo1 44212 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β*
β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π < ((πβ(π + 1)) β (π Β· π))) β ((π(,)((πβ(π + 1)) β (π Β· π))) βͺ {π}) = (π[,)((πβ(π + 1)) β (π Β· π)))) |
311 | 296, 185,
308, 310 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π(,)((πβ(π + 1)) β (π Β· π))) βͺ {π}) = (π[,)((πβ(π + 1)) β (π Β· π)))) |
312 | 311 | fveq2d 6893 |
. . . . . . . . . . . . . . 15
β’ (π β
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β((π(,)((πβ(π + 1)) β (π Β· π))) βͺ {π})) =
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β(π[,)((πβ(π + 1)) β (π Β· π))))) |
313 | 294 | cnfldtop 24292 |
. . . . . . . . . . . . . . . . . 18
β’
(TopOpenββfld) β Top |
314 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(,)+β) β
V |
315 | 314 | inex1 5317 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π(,)+β) β© π·) β V |
316 | | snex 5431 |
. . . . . . . . . . . . . . . . . . 19
β’ {π} β V |
317 | 315, 316 | unex 7730 |
. . . . . . . . . . . . . . . . . 18
β’ (((π(,)+β) β© π·) βͺ {π}) β V |
318 | | resttop 22656 |
. . . . . . . . . . . . . . . . . 18
β’
(((TopOpenββfld) β Top β§ (((π(,)+β) β© π·) βͺ {π}) β V) β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) β Top) |
319 | 313, 317,
318 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) β Top |
320 | 319 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) β Top) |
321 | | retop 24270 |
. . . . . . . . . . . . . . . . . . 19
β’
(topGenβran (,)) β Top |
322 | 321 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (topGenβran (,))
β Top) |
323 | 317 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π(,)+β) β© π·) βͺ {π}) β V) |
324 | | iooretop 24274 |
. . . . . . . . . . . . . . . . . . 19
β’
(-β(,)((πβ(π + 1)) β (π Β· π))) β (topGenβran
(,)) |
325 | 324 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (-β(,)((πβ(π + 1)) β (π Β· π))) β (topGenβran
(,))) |
326 | | elrestr 17371 |
. . . . . . . . . . . . . . . . . 18
β’
(((topGenβran (,)) β Top β§ (((π(,)+β) β© π·) βͺ {π}) β V β§ (-β(,)((πβ(π + 1)) β (π Β· π))) β (topGenβran (,))) β
((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β ((topGenβran (,))
βΎt (((π(,)+β) β© π·) βͺ {π}))) |
327 | 322, 323,
325, 326 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β ((topGenβran (,))
βΎt (((π(,)+β) β© π·) βͺ {π}))) |
328 | | mnfxr 11268 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ -β
β β* |
329 | 328 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β -β β
β*) |
330 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β ((πβ(π + 1)) β (π Β· π)) β
β*) |
331 | | icossre 13402 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ ((πβ(π + 1)) β (π Β· π)) β β*) β (π[,)((πβ(π + 1)) β (π Β· π))) β β) |
332 | 231, 185,
331 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π[,)((πβ(π + 1)) β (π Β· π))) β β) |
333 | 332 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ β β) |
334 | 333 | mnfltd 13101 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β -β < π₯) |
335 | 296 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π β
β*) |
336 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) |
337 | | icoltub 44208 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β*
β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
338 | 335, 330,
336, 337 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
339 | 329, 330,
333, 334, 338 | eliood 44198 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) |
340 | | vsnid 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π₯ β {π₯} |
341 | 340 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β π₯ β {π₯}) |
342 | | sneq 4638 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β {π₯} = {π}) |
343 | 341, 342 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β π₯ β {π}) |
344 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β {π} β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
345 | 343, 344 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
346 | 345 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ π₯ = π) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
347 | 296 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π β
β*) |
348 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β +β β
β*) |
349 | 333 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β β) |
350 | 231 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π β β) |
351 | | icogelb 13372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β*
β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π β€ π₯) |
352 | 335, 330,
336, 351 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π β€ π₯) |
353 | 352 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π β€ π₯) |
354 | | neqne 2949 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
π₯ = π β π₯ β π) |
355 | 354 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β π) |
356 | 350, 349,
353, 355 | leneltd 11365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π < π₯) |
357 | 349 | ltpnfd 13098 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ < +β) |
358 | 347, 348,
349, 356, 357 | eliood 44198 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β (π(,)+β)) |
359 | 180 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β π β β) |
360 | 359, 192 | mulneg1d 11664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (-π Β· π) = -(π Β· π)) |
361 | 360 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β ((π€ + (π Β· π)) + (-π Β· π)) = ((π€ + (π Β· π)) + -(π Β· π))) |
362 | 361 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + (-π Β· π)) = ((π€ + (π Β· π)) + -(π Β· π))) |
363 | | ioosscn 13383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π(,)((πβ(π + 1)) β (π Β· π))) β β |
364 | 363 | sseli 3978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π€ β (π(,)((πβ(π + 1)) β (π Β· π))) β π€ β β) |
365 | 364 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β β) |
366 | 255 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π Β· π) β β) |
367 | 365, 366 | addcld 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β β) |
368 | 367, 366 | negsubd 11574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + -(π Β· π)) = ((π€ + (π Β· π)) β (π Β· π))) |
369 | 365, 366 | pncand 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) β (π Β· π)) = π€) |
370 | 362, 368,
369 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ = ((π€ + (π Β· π)) + (-π Β· π))) |
371 | 183 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π Β· π) β β) |
372 | 225, 371 | readdcld 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β β) |
373 | 222, 224,
372, 250, 258 | eliood 44198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β ((πβπ)(,)(πβ(π + 1)))) |
374 | 216, 373 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β π·) |
375 | 269 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = -π β ((π β§ (π€ + (π Β· π)) β π· β§ π β β€) β (π β§ (π€ + (π Β· π)) β π· β§ -π β β€))) |
376 | 271 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = -π β ((π€ + (π Β· π)) + (π Β· π)) = ((π€ + (π Β· π)) + (-π Β· π))) |
377 | 376 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = -π β (((π€ + (π Β· π)) + (π Β· π)) β π· β ((π€ + (π Β· π)) + (-π Β· π)) β π·)) |
378 | 375, 377 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = -π β (((π β§ (π€ + (π Β· π)) β π· β§ π β β€) β ((π€ + (π Β· π)) + (π Β· π)) β π·) β ((π β§ (π€ + (π Β· π)) β π· β§ -π β β€) β ((π€ + (π Β· π)) + (-π Β· π)) β π·))) |
379 | 263 | 3anbi2d 1442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π₯ = (π€ + (π Β· π)) β ((π β§ π₯ β π· β§ π β β€) β (π β§ (π€ + (π Β· π)) β π· β§ π β β€))) |
380 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π₯ = (π€ + (π Β· π)) β (π₯ + (π Β· π)) = ((π€ + (π Β· π)) + (π Β· π))) |
381 | 380 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π₯ = (π€ + (π Β· π)) β ((π₯ + (π Β· π)) β π· β ((π€ + (π Β· π)) + (π Β· π)) β π·)) |
382 | 379, 381 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ = (π€ + (π Β· π)) β (((π β§ π₯ β π· β§ π β β€) β (π₯ + (π Β· π)) β π·) β ((π β§ (π€ + (π Β· π)) β π· β§ π β β€) β ((π€ + (π Β· π)) + (π Β· π)) β π·))) |
383 | 262, 382,
282 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π€ + (π Β· π)) β π· β§ π β β€) β ((π€ + (π Β· π)) + (π Β· π)) β π·) |
384 | 268, 378,
383 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (π€ + (π Β· π)) β π· β§ -π β β€) β ((π€ + (π Β· π)) + (-π Β· π)) β π·) |
385 | 204, 374,
261, 384 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β ((π€ + (π Β· π)) + (-π Β· π)) β π·) |
386 | 370, 385 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π€ β π·) |
387 | 386 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βπ€ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ β π·) |
388 | 387, 288 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) β π·) |
389 | 388 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β (π(,)((πβ(π + 1)) β (π Β· π))) β π·) |
390 | 185 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β ((πβ(π + 1)) β (π Β· π)) β
β*) |
391 | 338 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
392 | 347, 390,
349, 356, 391 | eliood 44198 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) |
393 | 389, 392 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β π·) |
394 | 358, 393 | elind 4194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β ((π(,)+β) β© π·)) |
395 | | elun1 4176 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β ((π(,)+β) β© π·) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
396 | 394, 395 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β§ Β¬ π₯ = π) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
397 | 346, 396 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
398 | 339, 397 | elind 4194 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) β π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) |
399 | 296 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β π β
β*) |
400 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β ((πβ(π + 1)) β (π Β· π)) β
β*) |
401 | | elinel1 4195 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) |
402 | | elioore 13351 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β (-β(,)((πβ(π + 1)) β (π Β· π))) β π₯ β β) |
403 | 401, 402 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β π₯ β β) |
404 | 403 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β π₯ β β*) |
405 | 404 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β π₯ β β*) |
406 | | elinel2 4196 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
407 | 231 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ = π) β π β β) |
408 | 85 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β π = π₯) |
409 | 408 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ = π) β π = π₯) |
410 | 407, 409 | eqled 11314 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ = π) β π β€ π₯) |
411 | 410 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ π₯ = π) β π β€ π₯) |
412 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β π) |
413 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β π₯ β (((π(,)+β) β© π·) βͺ {π})) |
414 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
π₯ = π β Β¬ π₯ = π) |
415 | | velsn 4644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β {π} β π₯ = π) |
416 | 414, 415 | sylnibr 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
π₯ = π β Β¬ π₯ β {π}) |
417 | 416 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β Β¬ π₯ β {π}) |
418 | | elunnel2 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β (((π(,)+β) β© π·) βͺ {π}) β§ Β¬ π₯ β {π}) β π₯ β ((π(,)+β) β© π·)) |
419 | 413, 417,
418 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β π₯ β ((π(,)+β) β© π·)) |
420 | | elinel1 4195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β ((π(,)+β) β© π·) β π₯ β (π(,)+β)) |
421 | 419, 420 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β π₯ β (π(,)+β)) |
422 | 231 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β (π(,)+β)) β π β β) |
423 | | elioore 13351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β (π(,)+β) β π₯ β β) |
424 | 423 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β (π(,)+β)) β π₯ β β) |
425 | 296 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β (π(,)+β)) β π β
β*) |
426 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β (π(,)+β)) β +β β
β*) |
427 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β (π(,)+β)) β π₯ β (π(,)+β)) |
428 | | ioogtlb 44195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β*
β§ +β β β* β§ π₯ β (π(,)+β)) β π < π₯) |
429 | 425, 426,
427, 428 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π₯ β (π(,)+β)) β π < π₯) |
430 | 422, 424,
429 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β (π(,)+β)) β π β€ π₯) |
431 | 412, 421,
430 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β§ Β¬ π₯ = π) β π β€ π₯) |
432 | 411, 431 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (((π(,)+β) β© π·) βͺ {π})) β π β€ π₯) |
433 | 406, 432 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β π β€ π₯) |
434 | 328 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) β -β β
β*) |
435 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) β ((πβ(π + 1)) β (π Β· π)) β
β*) |
436 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) β π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) |
437 | | iooltub 44210 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((-β β β* β§ ((πβ(π + 1)) β (π Β· π)) β β* β§ π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
438 | 434, 435,
436, 437 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β (-β(,)((πβ(π + 1)) β (π Β· π)))) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
439 | 401, 438 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β π₯ < ((πβ(π + 1)) β (π Β· π))) |
440 | 399, 400,
405, 433, 439 | elicod 13371 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) β π₯ β (π[,)((πβ(π + 1)) β (π Β· π)))) |
441 | 398, 440 | impbida 800 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π₯ β (π[,)((πβ(π + 1)) β (π Β· π))) β π₯ β ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π})))) |
442 | 441 | eqrdv 2731 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π[,)((πβ(π + 1)) β (π Β· π))) = ((-β(,)((πβ(π + 1)) β (π Β· π))) β© (((π(,)+β) β© π·) βͺ {π}))) |
443 | | ioossre 13382 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π(,)+β) β
β |
444 | | ssinss1 4237 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π(,)+β) β β
β ((π(,)+β)
β© π·) β
β) |
445 | 443, 444 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π(,)+β) β© π·) β β) |
446 | 231 | snssd 4812 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π} β β) |
447 | 445, 446 | unssd 4186 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π(,)+β) β© π·) βͺ {π}) β β) |
448 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(topGenβran (,)) = (topGenβran (,)) |
449 | 294, 448 | rerest 24312 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π(,)+β) β© π·) βͺ {π}) β β β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) = ((topGenβran (,))
βΎt (((π(,)+β) β© π·) βͺ {π}))) |
450 | 447, 449 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) = ((topGenβran (,))
βΎt (((π(,)+β) β© π·) βͺ {π}))) |
451 | 327, 442,
450 | 3eltr4d 2849 |
. . . . . . . . . . . . . . . 16
β’ (π β (π[,)((πβ(π + 1)) β (π Β· π))) β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π}))) |
452 | | isopn3i 22578 |
. . . . . . . . . . . . . . . 16
β’
((((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})) β Top β§ (π[,)((πβ(π + 1)) β (π Β· π))) β
((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π}))) β
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β(π[,)((πβ(π + 1)) β (π Β· π)))) = (π[,)((πβ(π + 1)) β (π Β· π)))) |
453 | 320, 451,
452 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β(π[,)((πβ(π + 1)) β (π Β· π)))) = (π[,)((πβ(π + 1)) β (π Β· π)))) |
454 | 312, 453 | eqtr2d 2774 |
. . . . . . . . . . . . . 14
β’ (π β (π[,)((πβ(π + 1)) β (π Β· π))) =
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β((π(,)((πβ(π + 1)) β (π Β· π))) βͺ {π}))) |
455 | 309, 454 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (π β π β
((intβ((TopOpenββfld) βΎt (((π(,)+β) β© π·) βͺ {π})))β((π(,)((πβ(π + 1)) β (π Β· π))) βͺ {π}))) |
456 | 171, 290,
293, 294, 295, 455 | limcres 25395 |
. . . . . . . . . . . 12
β’ (π β (((πΉ βΎ ((π(,)+β) β© π·)) βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π) = ((πΉ βΎ ((π(,)+β) β© π·)) limβ π)) |
457 | 290 | resabs1d 6011 |
. . . . . . . . . . . . . 14
β’ (π β ((πΉ βΎ ((π(,)+β) β© π·)) βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) = (πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π))))) |
458 | 457 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π β (((πΉ βΎ ((π(,)+β) β© π·)) βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π) = ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) |
459 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
β) |
460 | 153, 459 | fssd 6733 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΉ:π·βΆβ) |
461 | 212 | feq2d 6701 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΉ:dom πΉβΆβ β πΉ:π·βΆβ)) |
462 | 460, 461 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:dom πΉβΆβ) |
463 | 152, 462 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ:dom πΉβΆβ) |
464 | 463 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β πΉ:dom πΉβΆβ) |
465 | 363 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β (π(,)((πβ(π + 1)) β (π Β· π))) β β) |
466 | 388, 160 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) β dom πΉ) |
467 | 466 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β (π(,)((πβ(π + 1)) β (π Β· π))) β dom πΉ) |
468 | 255 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β (π Β· π) β β) |
469 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ {π§ β β β£
βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} = {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} |
470 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π€ β (π§ = (π₯ + (π Β· π)) β π€ = (π₯ + (π Β· π)))) |
471 | 470 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = π€ β (βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π)) β βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ = (π₯ + (π Β· π)))) |
472 | 471 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β (π€ β β β§ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ = (π₯ + (π Β· π)))) |
473 | 472 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ = (π₯ + (π Β· π))) |
474 | 473 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) β βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ = (π₯ + (π Β· π))) |
475 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π₯π |
476 | | nfre1 3283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π₯βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π)) |
477 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π₯β |
478 | 476, 477 | nfrabw 3469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π₯{π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} |
479 | 478 | nfcri 2891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π₯ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} |
480 | 475, 479 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π₯(π β§ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) |
481 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π₯ π€ β π· |
482 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π))) β§ π€ = (π₯ + (π Β· π))) β π€ = (π₯ + (π Β· π))) |
483 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ = π₯ β (π€ β (π(,)((πβ(π + 1)) β (π Β· π))) β π₯ β (π(,)((πβ(π + 1)) β (π Β· π))))) |
484 | 483 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π₯ β ((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))))) |
485 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π€ = π₯ β (π€ + (π Β· π)) = (π₯ + (π Β· π))) |
486 | 485 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π₯ β ((π€ + (π Β· π)) β π· β (π₯ + (π Β· π)) β π·)) |
487 | 484, 486 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π₯ β (((π β§ π€ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π€ + (π Β· π)) β π·) β ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π₯ + (π Β· π)) β π·))) |
488 | 487, 260 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (π₯ + (π Β· π)) β π·) |
489 | 488 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π))) β§ π€ = (π₯ + (π Β· π))) β (π₯ + (π Β· π)) β π·) |
490 | 482, 489 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π))) β§ π€ = (π₯ + (π Β· π))) β π€ β π·) |
491 | 490 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π₯ β (π(,)((πβ(π + 1)) β (π Β· π))) β (π€ = (π₯ + (π Β· π)) β π€ β π·))) |
492 | 491 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) β (π₯ β (π(,)((πβ(π + 1)) β (π Β· π))) β (π€ = (π₯ + (π Β· π)) β π€ β π·))) |
493 | 480, 481,
492 | rexlimd 3264 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) β (βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π€ = (π₯ + (π Β· π)) β π€ β π·)) |
494 | 474, 493 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) β π€ β π·) |
495 | 494 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β βπ€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}π€ β π·) |
496 | | dfss3 3970 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π§ β β β£
βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β π· β βπ€ β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}π€ β π·) |
497 | 495, 496 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β π·) |
498 | 497, 160 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β dom πΉ) |
499 | 498 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} β dom πΉ) |
500 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π) |
501 | 388 | sselda 3982 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π₯ β π·) |
502 | 180 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β π β β€) |
503 | | fourierdlem48.per |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) |
504 | 500, 501,
502, 503 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) |
505 | 504 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β§ π₯ β (π(,)((πβ(π + 1)) β (π Β· π)))) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) |
506 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) |
507 | 464, 465,
467, 468, 469, 499, 505, 506 | limcperiod 44331 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β π€ β ((πΉ βΎ {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) limβ (π + (π Β· π)))) |
508 | 256 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πβ(π + 1)) = (((πβ(π + 1)) β (π Β· π)) + (π Β· π))) |
509 | 234, 508 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π¦(,)(πβ(π + 1))) = ((π + (π Β· π))(,)(((πβ(π + 1)) β (π Β· π)) + (π Β· π)))) |
510 | 231, 184,
183 | iooshift 44222 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π + (π Β· π))(,)(((πβ(π + 1)) β (π Β· π)) + (π Β· π))) = {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) |
511 | 509, 510 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))} = (π¦(,)(πβ(π + 1)))) |
512 | 511 | reseq2d 5980 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ βΎ {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) = (πΉ βΎ (π¦(,)(πβ(π + 1))))) |
513 | 512, 235 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΉ βΎ {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) limβ (π + (π Β· π))) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
514 | 513 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β ((πΉ βΎ {π§ β β β£ βπ₯ β (π(,)((πβ(π + 1)) β (π Β· π)))π§ = (π₯ + (π Β· π))}) limβ (π + (π Β· π))) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
515 | 507, 514 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) β π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
516 | 463 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β πΉ:dom πΉβΆβ) |
517 | | ioosscn 13383 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦(,)(πβ(π + 1))) β β |
518 | 517 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β (π¦(,)(πβ(π + 1))) β β) |
519 | | icogelb 13372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β (πβπ) β€ π¦) |
520 | 221, 223,
236, 519 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πβπ) β€ π¦) |
521 | | iooss1 13356 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πβπ) β β* β§ (πβπ) β€ π¦) β (π¦(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) |
522 | 221, 520,
521 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π¦(,)(πβ(π + 1))) β ((πβπ)(,)(πβ(π + 1)))) |
523 | 522, 215 | sstrd 3992 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π¦(,)(πβ(π + 1))) β π·) |
524 | 523, 160 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π¦(,)(πβ(π + 1))) β dom πΉ) |
525 | 524 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β (π¦(,)(πβ(π + 1))) β dom πΉ) |
526 | 359 | negcld 11555 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β -π β β) |
527 | 526, 192 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (-π Β· π) β β) |
528 | 527 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β (-π Β· π) β β) |
529 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ {π§ β β β£
βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} = {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} |
530 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π€ β (π§ = (π₯ + (-π Β· π)) β π€ = (π₯ + (-π Β· π)))) |
531 | 530 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = π€ β (βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π)) β βπ₯ β (π¦(,)(πβ(π + 1)))π€ = (π₯ + (-π Β· π)))) |
532 | 531 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β (π€ β β β§ βπ₯ β (π¦(,)(πβ(π + 1)))π€ = (π₯ + (-π Β· π)))) |
533 | 532 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β βπ₯ β (π¦(,)(πβ(π + 1)))π€ = (π₯ + (-π Β· π))) |
534 | 533 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) β βπ₯ β (π¦(,)(πβ(π + 1)))π€ = (π₯ + (-π Β· π))) |
535 | | nfre1 3283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π₯βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π)) |
536 | 535, 477 | nfrabw 3469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π₯{π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} |
537 | 536 | nfcri 2891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π₯ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} |
538 | 475, 537 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π₯(π β§ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) |
539 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1))) β§ π€ = (π₯ + (-π Β· π))) β π€ = (π₯ + (-π Β· π))) |
540 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1)))) β π) |
541 | 523 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1)))) β π₯ β π·) |
542 | 180 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1)))) β π β β€) |
543 | 542 | znegcld 12665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1)))) β -π β β€) |
544 | 540, 541,
543, 283 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1)))) β (π₯ + (-π Β· π)) β π·) |
545 | 544 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1))) β§ π€ = (π₯ + (-π Β· π))) β (π₯ + (-π Β· π)) β π·) |
546 | 539, 545 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β (π¦(,)(πβ(π + 1))) β§ π€ = (π₯ + (-π Β· π))) β π€ β π·) |
547 | 546 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π₯ β (π¦(,)(πβ(π + 1))) β (π€ = (π₯ + (-π Β· π)) β π€ β π·))) |
548 | 547 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) β (π₯ β (π¦(,)(πβ(π + 1))) β (π€ = (π₯ + (-π Β· π)) β π€ β π·))) |
549 | 538, 481,
548 | rexlimd 3264 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) β (βπ₯ β (π¦(,)(πβ(π + 1)))π€ = (π₯ + (-π Β· π)) β π€ β π·)) |
550 | 534, 549 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) β π€ β π·) |
551 | 550 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β βπ€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}π€ β π·) |
552 | | dfss3 3970 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π§ β β β£
βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β π· β βπ€ β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}π€ β π·) |
553 | 551, 552 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β π·) |
554 | 553, 160 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β dom πΉ) |
555 | 554 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} β dom πΉ) |
556 | 152 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β§ π₯ β (π¦(,)(πβ(π + 1)))) β π) |
557 | 541 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β§ π₯ β (π¦(,)(πβ(π + 1)))) β π₯ β π·) |
558 | 543 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β§ π₯ β (π¦(,)(πβ(π + 1)))) β -π β β€) |
559 | 272 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = -π β (πΉβ(π₯ + (π Β· π))) = (πΉβ(π₯ + (-π Β· π)))) |
560 | 559 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = -π β ((πΉβ(π₯ + (π Β· π))) = (πΉβπ₯) β (πΉβ(π₯ + (-π Β· π))) = (πΉβπ₯))) |
561 | 270, 560 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = -π β (((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) β ((π β§ π₯ β π· β§ -π β β€) β (πΉβ(π₯ + (-π Β· π))) = (πΉβπ₯)))) |
562 | 278 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πΉβ(π₯ + (π Β· π))) = (πΉβ(π₯ + (π Β· π)))) |
563 | 562 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πΉβ(π₯ + (π Β· π))) = (πΉβπ₯) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯))) |
564 | 276, 563 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) β ((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)))) |
565 | 564, 503 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π· β§ π β β€) β (πΉβ(π₯ + (π Β· π))) = (πΉβπ₯)) |
566 | 268, 561,
565 | vtocl 3550 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π· β§ -π β β€) β (πΉβ(π₯ + (-π Β· π))) = (πΉβπ₯)) |
567 | 556, 557,
558, 566 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β§ π₯ β (π¦(,)(πβ(π + 1)))) β (πΉβ(π₯ + (-π Β· π))) = (πΉβπ₯)) |
568 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
569 | 516, 518,
525, 528, 529, 555, 567, 568 | limcperiod 44331 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β π€ β ((πΉ βΎ {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) limβ (π¦ + (-π Β· π)))) |
570 | 360 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π¦ + (-π Β· π)) = (π¦ + -(π Β· π))) |
571 | 304 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π¦ β β) |
572 | 571, 255 | negsubd 11574 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π¦ + -(π Β· π)) = (π¦ β (π Β· π))) |
573 | 301 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π¦ β (π Β· π)) = π) |
574 | 570, 572,
573 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π¦ + (-π Β· π)) = π) |
575 | 574 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π = (π¦ + (-π Β· π))) |
576 | 360 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πβ(π + 1)) + (-π Β· π)) = ((πβ(π + 1)) + -(π Β· π))) |
577 | 254, 255 | negsubd 11574 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((πβ(π + 1)) + -(π Β· π)) = ((πβ(π + 1)) β (π Β· π))) |
578 | 576, 577 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((πβ(π + 1)) β (π Β· π)) = ((πβ(π + 1)) + (-π Β· π))) |
579 | 575, 578 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π(,)((πβ(π + 1)) β (π Β· π))) = ((π¦ + (-π Β· π))(,)((πβ(π + 1)) + (-π Β· π)))) |
580 | 181 | renegcld 11638 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β -π β β) |
581 | 580, 182 | remulcld 11241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (-π Β· π) β β) |
582 | 304, 179,
581 | iooshift 44222 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π¦ + (-π Β· π))(,)((πβ(π + 1)) + (-π Β· π))) = {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) |
583 | 579, 582 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} = (π(,)((πβ(π + 1)) β (π Β· π)))) |
584 | 583 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))} = (π(,)((πβ(π + 1)) β (π Β· π)))) |
585 | 584 | reseq2d 5980 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β (πΉ βΎ {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) = (πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π))))) |
586 | 574 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β (π¦ + (-π Β· π)) = π) |
587 | 585, 586 | oveq12d 7424 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β ((πΉ βΎ {π§ β β β£ βπ₯ β (π¦(,)(πβ(π + 1)))π§ = (π₯ + (-π Β· π))}) limβ (π¦ + (-π Β· π))) = ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) |
588 | 569, 587 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) β π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π)) |
589 | 515, 588 | impbida 800 |
. . . . . . . . . . . . . 14
β’ (π β (π€ β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π) β π€ β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦))) |
590 | 589 | eqrdv 2731 |
. . . . . . . . . . . . 13
β’ (π β ((πΉ βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
591 | 458, 590 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β (((πΉ βΎ ((π(,)+β) β© π·)) βΎ (π(,)((πβ(π + 1)) β (π Β· π)))) limβ π) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
592 | 164, 456,
591 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ (π(,)+β)) limβ π) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
593 | 152, 174,
70 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) < (πβ(π + 1))) |
594 | 152, 174,
206 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) β (((πβπ)(,)(πβ(π + 1)))βcnββ)) |
595 | | fourierdlem48.r |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
596 | 152, 174,
595 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β π
β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) limβ (πβπ))) |
597 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ if(π¦ = (πβπ), π
, ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ¦)) = if(π¦ = (πβπ), π
, ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ¦)) |
598 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
((TopOpenββfld) βΎt ((πβπ)[,)(πβ(π + 1)))) =
((TopOpenββfld) βΎt ((πβπ)[,)(πβ(π + 1)))) |
599 | 220, 179,
593, 594, 596, 304, 179, 306, 522, 597, 598 | fourierdlem32 44842 |
. . . . . . . . . . . . 13
β’ (π β if(π¦ = (πβπ), π
, ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ¦)) β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
600 | 522 | resabs1d 6011 |
. . . . . . . . . . . . . 14
β’ (π β ((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) βΎ (π¦(,)(πβ(π + 1)))) = (πΉ βΎ (π¦(,)(πβ(π + 1))))) |
601 | 600 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π β (((πΉ βΎ ((πβπ)(,)(πβ(π + 1)))) βΎ (π¦(,)(πβ(π + 1)))) limβ π¦) = ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
602 | 599, 601 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ (π β if(π¦ = (πβπ), π
, ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ¦)) β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦)) |
603 | | ne0i 4334 |
. . . . . . . . . . . 12
β’ (if(π¦ = (πβπ), π
, ((πΉ βΎ ((πβπ)(,)(πβ(π + 1))))βπ¦)) β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦) β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦) β β
) |
604 | 602, 603 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ (π¦(,)(πβ(π + 1)))) limβ π¦) β β
) |
605 | 592, 604 | eqnetrd 3009 |
. . . . . . . . . 10
β’ (π β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
606 | 149, 605 | sylbir 234 |
. . . . . . . . 9
β’
(((((π β§ π β (0..^π)) β§ π¦ β ((πβπ)[,)(πβ(π + 1)))) β§ π β β€) β§ π¦ = (π + (π Β· π))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
607 | 146, 147,
148, 606 | syl21anc 837 |
. . . . . . . 8
β’ ((π β§ (π β (0..^π) β§ π β β€) β§ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
608 | 607 | 3exp 1120 |
. . . . . . 7
β’ (π β ((π β (0..^π) β§ π β β€) β ((π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
))) |
609 | 608 | adantr 482 |
. . . . . 6
β’ ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((π β (0..^π) β§ π β β€) β ((π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
))) |
610 | 137, 142,
609 | rexlim2d 44328 |
. . . . 5
β’ ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β (βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
)) |
611 | 134, 610 | mpd 15 |
. . . 4
β’ ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
612 | 127, 133,
611 | vtocl 3550 |
. . 3
β’ ((π β§ βπ β (0..^π)βπ β β€ (((πΈβπ) β π) β ((πβπ)[,)(πβ(π + 1))) β§ ((πΈβπ) β π) = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
613 | 1, 126, 612 | syl2anc 585 |
. 2
β’ ((π β§ (πΈβπ) = π΅) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
614 | | iocssre 13401 |
. . . . . 6
β’ ((π΄ β β*
β§ π΅ β β)
β (π΄(,]π΅) β
β) |
615 | 55, 9, 614 | syl2anc 585 |
. . . . 5
β’ (π β (π΄(,]π΅) β β) |
616 | | ovex 7439 |
. . . . . . . . . . 11
β’
((ββ((π΅
β π₯) / π)) Β· π) β V |
617 | 89 | fvmpt2 7007 |
. . . . . . . . . . 11
β’ ((π₯ β β β§
((ββ((π΅ β
π₯) / π)) Β· π) β V) β (πβπ₯) = ((ββ((π΅ β π₯) / π)) Β· π)) |
618 | 616, 617 | mpan2 690 |
. . . . . . . . . 10
β’ (π₯ β β β (πβπ₯) = ((ββ((π΅ β π₯) / π)) Β· π)) |
619 | 618 | oveq2d 7422 |
. . . . . . . . 9
β’ (π₯ β β β (π₯ + (πβπ₯)) = (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
620 | 619 | mpteq2ia 5251 |
. . . . . . . 8
β’ (π₯ β β β¦ (π₯ + (πβπ₯))) = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
621 | 83, 620 | eqtri 2761 |
. . . . . . 7
β’ πΈ = (π₯ β β β¦ (π₯ + ((ββ((π΅ β π₯) / π)) Β· π))) |
622 | 13, 9, 16, 12, 621 | fourierdlem4 44814 |
. . . . . 6
β’ (π β πΈ:ββΆ(π΄(,]π΅)) |
623 | 622, 10 | ffvelcdmd 7085 |
. . . . 5
β’ (π β (πΈβπ) β (π΄(,]π΅)) |
624 | 615, 623 | sseldd 3983 |
. . . 4
β’ (π β (πΈβπ) β β) |
625 | 624 | adantr 482 |
. . 3
β’ ((π β§ (πΈβπ) β π΅) β (πΈβπ) β β) |
626 | | simpl 484 |
. . . 4
β’ ((π β§ (πΈβπ) β π΅) β π) |
627 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β (πΈβπ) β ran π) |
628 | | ffn 6715 |
. . . . . . . . . . . . . . 15
β’ (π:(0...π)βΆβ β π Fn (0...π)) |
629 | 40, 628 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π Fn (0...π)) |
630 | 629 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β π Fn (0...π)) |
631 | | fvelrnb 6950 |
. . . . . . . . . . . . 13
β’ (π Fn (0...π) β ((πΈβπ) β ran π β βπ β (0...π)(πβπ) = (πΈβπ))) |
632 | 630, 631 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β ((πΈβπ) β ran π β βπ β (0...π)(πβπ) = (πΈβπ))) |
633 | 627, 632 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β βπ β (0...π)(πβπ) = (πΈβπ)) |
634 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 1 β β€) |
635 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β π β β€) |
636 | 635 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β β€) |
637 | 636 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β β) |
638 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π) β 0 β€ π) |
639 | 638 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 0 β€ π) |
640 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πβπ) = (πΈβπ) β (πβπ) = (πΈβπ)) |
641 | 640 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πβπ) = (πΈβπ) β (πΈβπ) = (πβπ)) |
642 | 641 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πΈβπ) = (πβπ)) |
643 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = 0 β (πβπ) = (πβ0)) |
644 | 643 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πβπ) = (πβ0)) |
645 | 37 | simprld 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β ((πβ0) = π΄ β§ (πβπ) = π΅)) |
646 | 645 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (πβ0) = π΄) |
647 | 646 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πβ0) = π΄) |
648 | 642, 644,
647 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πΈβπ) = π΄) |
649 | 648 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πΈβπ) = π΄) |
650 | 649 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β§ π = 0) β (πΈβπ) = π΄) |
651 | 13 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β π΄ β β) |
652 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β π΄ β
β*) |
653 | 9 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π΅ β
β*) |
654 | 653 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β π΅ β
β*) |
655 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β (πΈβπ) β (π΄(,]π΅)) |
656 | | iocgtlb 44202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πΈβπ) β (π΄(,]π΅)) β π΄ < (πΈβπ)) |
657 | 652, 654,
655, 656 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β π΄ < (πΈβπ)) |
658 | 651, 657 | gtned 11346 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β (πΈβπ) β π΄) |
659 | 658 | neneqd 2946 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β Β¬ (πΈβπ) = π΄) |
660 | 659 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β§ π = 0) β Β¬ (πΈβπ) = π΄) |
661 | 650, 660 | pm2.65da 816 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β Β¬ π = 0) |
662 | 661 | neqned 2948 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β 0) |
663 | 637, 639,
662 | ne0gt0d 11348 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 0 < π) |
664 | | 0zd 12567 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 0 β β€) |
665 | | zltp1le 12609 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((0
β β€ β§ π
β β€) β (0 < π β (0 + 1) β€ π)) |
666 | 664, 636,
665 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (0 < π β (0 + 1) β€ π)) |
667 | 663, 666 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (0 + 1) β€ π) |
668 | 74, 667 | eqbrtrid 5183 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 1 β€ π) |
669 | | eluz2 12825 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β1) β (1 β β€ β§ π β β€ β§ 1 β€
π)) |
670 | 634, 636,
668, 669 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β
(β€β₯β1)) |
671 | | nnuz 12862 |
. . . . . . . . . . . . . . . . . . 19
β’ β =
(β€β₯β1) |
672 | 670, 671 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β β) |
673 | | nnm1nn0 12510 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π β 1) β
β0) |
674 | 672, 673 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β
β0) |
675 | 674, 42 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β
(β€β₯β0)) |
676 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π β β€) |
677 | | peano2zm 12602 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β€ β (π β 1) β
β€) |
678 | 635, 677 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...π) β (π β 1) β β€) |
679 | 678 | zred 12663 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β (π β 1) β β) |
680 | 635 | zred 12663 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β β) |
681 | | elfzel2 13496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...π) β π β β€) |
682 | 681 | zred 12663 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β β) |
683 | 680 | ltm1d 12143 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β (π β 1) < π) |
684 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β€ π) |
685 | 679, 680,
682, 683, 684 | ltletrd 11371 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β (π β 1) < π) |
686 | 685 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) < π) |
687 | | elfzo2 13632 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β (0..^π) β ((π β 1) β
(β€β₯β0) β§ π β β€ β§ (π β 1) < π)) |
688 | 675, 676,
686, 687 | syl3anbrc 1344 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β (0..^π)) |
689 | 40 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π:(0...π)βΆβ) |
690 | 636, 677 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β β€) |
691 | 674 | nn0ge0d 12532 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β 0 β€ (π β 1)) |
692 | 679, 682,
685 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β (π β 1) β€ π) |
693 | 692 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β€ π) |
694 | 664, 676,
690, 691, 693 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (π β 1) β (0...π)) |
695 | 689, 694 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ(π β 1)) β β) |
696 | 695 | rexrd 11261 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ(π β 1)) β
β*) |
697 | 40 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
698 | 697 | rexrd 11261 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β (πβπ) β
β*) |
699 | 698 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β (πβπ) β
β*) |
700 | 699 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβπ) β
β*) |
701 | 615 | sselda 3982 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β (πΈβπ) β β) |
702 | 701 | rexrd 11261 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β (πΈβπ) β
β*) |
703 | 702 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β
β*) |
704 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β π) |
705 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1) β
V |
706 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π β 1) β (π β (0..^π) β (π β 1) β (0..^π))) |
707 | 706 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β 1) β ((π β§ π β (0..^π)) β (π β§ (π β 1) β (0..^π)))) |
708 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π β 1) β (πβπ) = (πβ(π β 1))) |
709 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π β 1) β (π + 1) = ((π β 1) + 1)) |
710 | 709 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π β 1) β (πβ(π + 1)) = (πβ((π β 1) + 1))) |
711 | 708, 710 | breq12d 5161 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β 1) β ((πβπ) < (πβ(π + 1)) β (πβ(π β 1)) < (πβ((π β 1) + 1)))) |
712 | 707, 711 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β 1) β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ (π β 1) β (0..^π)) β (πβ(π β 1)) < (πβ((π β 1) + 1))))) |
713 | 705, 712,
70 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β 1) β (0..^π)) β (πβ(π β 1)) < (πβ((π β 1) + 1))) |
714 | 704, 688,
713 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ(π β 1)) < (πβ((π β 1) + 1))) |
715 | 635 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π) β π β β) |
716 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π) β 1 β β) |
717 | 715, 716 | npcand 11572 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β ((π β 1) + 1) = π) |
718 | 717 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β π = ((π β 1) + 1)) |
719 | 718 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β (πβπ) = (πβ((π β 1) + 1))) |
720 | 719 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...π) β (πβ((π β 1) + 1)) = (πβπ)) |
721 | 720 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ((π β 1) + 1)) = (πβπ)) |
722 | 714, 721 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ(π β 1)) < (πβπ)) |
723 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβπ) = (πΈβπ)) |
724 | 722, 723 | breqtrd 5174 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πβ(π β 1)) < (πΈβπ)) |
725 | 624 | leidd 11777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΈβπ) β€ (πΈβπ)) |
726 | 725 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β€ (πΈβπ)) |
727 | 641 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) = (πβπ)) |
728 | 726, 727 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β€ (πβπ)) |
729 | 728 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β€ (πβπ)) |
730 | 696, 700,
703, 724, 729 | eliocd 44207 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β ((πβ(π β 1))(,](πβπ))) |
731 | 719 | oveq2d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β ((πβ(π β 1))(,](πβπ)) = ((πβ(π β 1))(,](πβ((π β 1) + 1)))) |
732 | 731 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β ((πβ(π β 1))(,](πβπ)) = ((πβ(π β 1))(,](πβ((π β 1) + 1)))) |
733 | 730, 732 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β (πΈβπ) β ((πβ(π β 1))(,](πβ((π β 1) + 1)))) |
734 | 708, 710 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β 1) β ((πβπ)(,](πβ(π + 1))) = ((πβ(π β 1))(,](πβ((π β 1) + 1)))) |
735 | 734 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β 1) β ((πΈβπ) β ((πβπ)(,](πβ(π + 1))) β (πΈβπ) β ((πβ(π β 1))(,](πβ((π β 1) + 1))))) |
736 | 735 | rspcev 3613 |
. . . . . . . . . . . . . . 15
β’ (((π β 1) β (0..^π) β§ (πΈβπ) β ((πβ(π β 1))(,](πβ((π β 1) + 1)))) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
737 | 688, 733,
736 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β§ (πβπ) = (πΈβπ)) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
738 | 737 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ π β (0...π)) β ((πβπ) = (πΈβπ) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
739 | 738 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β§ π β (0...π)) β ((πβπ) = (πΈβπ) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
740 | 739 | rexlimdva 3156 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β (βπ β (0...π)(πβπ) = (πΈβπ) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
741 | 633, 740 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ (πΈβπ) β ran π) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
742 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β π β β) |
743 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β π:(0...π)βΆβ) |
744 | | iocssicc 13411 |
. . . . . . . . . . . . . . 15
β’ (π΄(,]π΅) β (π΄[,]π΅) |
745 | 646 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ = (πβ0)) |
746 | 645 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πβπ) = π΅) |
747 | 746 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ = (πβπ)) |
748 | 745, 747 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄[,]π΅) = ((πβ0)[,](πβπ))) |
749 | 744, 748 | sseqtrid 4034 |
. . . . . . . . . . . . . 14
β’ (π β (π΄(,]π΅) β ((πβ0)[,](πβπ))) |
750 | 749 | sselda 3982 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β (πΈβπ) β ((πβ0)[,](πβπ))) |
751 | 750 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β (πΈβπ) β ((πβ0)[,](πβπ))) |
752 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β Β¬ (πΈβπ) β ran π) |
753 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
754 | 753 | breq1d 5158 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ) < (πΈβπ) β (πβπ) < (πΈβπ))) |
755 | 754 | cbvrabv 3443 |
. . . . . . . . . . . . 13
β’ {π β (0..^π) β£ (πβπ) < (πΈβπ)} = {π β (0..^π) β£ (πβπ) < (πΈβπ)} |
756 | 755 | supeq1i 9439 |
. . . . . . . . . . . 12
β’
sup({π β
(0..^π) β£ (πβπ) < (πΈβπ)}, β, < ) = sup({π β (0..^π) β£ (πβπ) < (πΈβπ)}, β, < ) |
757 | 742, 743,
751, 752, 756 | fourierdlem25 44835 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,)(πβ(π + 1)))) |
758 | | ioossioc 44192 |
. . . . . . . . . . . . . 14
β’ ((πβπ)(,)(πβ(π + 1))) β ((πβπ)(,](πβ(π + 1))) |
759 | 758 | sseli 3978 |
. . . . . . . . . . . . 13
β’ ((πΈβπ) β ((πβπ)(,)(πβ(π + 1))) β (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
760 | 759 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β§ π β (0..^π)) β ((πΈβπ) β ((πβπ)(,)(πβ(π + 1))) β (πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
761 | 760 | reximdva 3169 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β (βπ β (0..^π)(πΈβπ) β ((πβπ)(,)(πβ(π + 1))) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
762 | 757, 761 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ (πΈβπ) β (π΄(,]π΅)) β§ Β¬ (πΈβπ) β ran π) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
763 | 741, 762 | pm2.61dan 812 |
. . . . . . . . 9
β’ ((π β§ (πΈβπ) β (π΄(,]π΅)) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
764 | 623, 763 | mpdan 686 |
. . . . . . . 8
β’ (π β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
765 | | fveq2 6889 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
766 | | oveq1 7413 |
. . . . . . . . . . . 12
β’ (π = π β (π + 1) = (π + 1)) |
767 | 766 | fveq2d 6893 |
. . . . . . . . . . 11
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
768 | 765, 767 | oveq12d 7424 |
. . . . . . . . . 10
β’ (π = π β ((πβπ)(,](πβ(π + 1))) = ((πβπ)(,](πβ(π + 1)))) |
769 | 768 | eleq2d 2820 |
. . . . . . . . 9
β’ (π = π β ((πΈβπ) β ((πβπ)(,](πβ(π + 1))) β (πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
770 | 769 | cbvrexvw 3236 |
. . . . . . . 8
β’
(βπ β
(0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
771 | 764, 770 | sylib 217 |
. . . . . . 7
β’ (π β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
772 | 771 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΈβπ) β π΅) β βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
773 | | elfzonn0 13674 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β β0) |
774 | | 1nn0 12485 |
. . . . . . . . . . . . . . 15
β’ 1 β
β0 |
775 | 774 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β 1 β
β0) |
776 | 773, 775 | nn0addcld 12533 |
. . . . . . . . . . . . 13
β’ (π β (0..^π) β (π + 1) β
β0) |
777 | 776, 42 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β (π + 1) β
(β€β₯β0)) |
778 | 777 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0..^π) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β
(β€β₯β0)) |
779 | 778 | 3ad2antl2 1187 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β
(β€β₯β0)) |
780 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β π β β€) |
781 | 780 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π β β€) |
782 | 773 | nn0red 12530 |
. . . . . . . . . . . . . 14
β’ (π β (0..^π) β π β β) |
783 | 782 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β (0..^π) β§ (πΈβπ) = (πβ(π + 1))) β π β β) |
784 | 783 | 3ad2antl2 1187 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π β β) |
785 | | 1red 11212 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β 1 β
β) |
786 | 784, 785 | readdcld 11240 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β β) |
787 | 781 | zred 12663 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π β β) |
788 | | elfzop1le2 13642 |
. . . . . . . . . . . . 13
β’ (π β (0..^π) β (π + 1) β€ π) |
789 | 788 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β (0..^π) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β€ π) |
790 | 789 | 3ad2antl2 1187 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β€ π) |
791 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πΈβπ) = (πβ(π + 1))) |
792 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
793 | 792 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (πβ(π + 1)) = (πβπ)) |
794 | 793 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πβ(π + 1)) = (πβπ)) |
795 | 746 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πβπ) = π΅) |
796 | 791, 794,
795 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πΈβπ) = π΅) |
797 | 796 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πΈβπ) = π΅) |
798 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β (πΈβπ) β π΅) |
799 | 798 | neneqd 2946 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β§ π = (π + 1)) β Β¬ (πΈβπ) = π΅) |
800 | 797, 799 | pm2.65da 816 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β Β¬ π = (π + 1)) |
801 | 800 | neqned 2948 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β π β (π + 1)) |
802 | 801 | 3ad2antl1 1186 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π β (π + 1)) |
803 | 786, 787,
790, 802 | leneltd 11365 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) < π) |
804 | | elfzo2 13632 |
. . . . . . . . . 10
β’ ((π + 1) β (0..^π) β ((π + 1) β (β€β₯β0)
β§ π β β€
β§ (π + 1) < π)) |
805 | 779, 781,
803, 804 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (π + 1) β (0..^π)) |
806 | 40 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
807 | | fzofzp1 13726 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β (π + 1) β (0...π)) |
808 | 807 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
809 | 806, 808 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
810 | 809 | rexrd 11261 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
811 | 810 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ (πΈβπ) β π΅) β§ π β (0..^π)) β (πβ(π + 1)) β
β*) |
812 | 811 | 3adant3 1133 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
813 | 812 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β
β*) |
814 | | simpl1l 1225 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π) |
815 | 814, 40 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β π:(0...π)βΆβ) |
816 | | fzofzp1 13726 |
. . . . . . . . . . . . 13
β’ ((π + 1) β (0..^π) β ((π + 1) + 1) β (0...π)) |
817 | 805, 816 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β ((π + 1) + 1) β (0...π)) |
818 | 815, 817 | ffvelcdmd 7085 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πβ((π + 1) + 1)) β β) |
819 | 818 | rexrd 11261 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πβ((π + 1) + 1)) β
β*) |
820 | 624 | rexrd 11261 |
. . . . . . . . . . . 12
β’ (π β (πΈβπ) β
β*) |
821 | 820 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β
β*) |
822 | 821 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β
β*) |
823 | 809 | leidd 11777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β€ (πβ(π + 1))) |
824 | 823 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β€ (πβ(π + 1))) |
825 | | id 22 |
. . . . . . . . . . . . . . 15
β’ ((πΈβπ) = (πβ(π + 1)) β (πΈβπ) = (πβ(π + 1))) |
826 | 825 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ ((πΈβπ) = (πβ(π + 1)) β (πβ(π + 1)) = (πΈβπ)) |
827 | 826 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) = (πΈβπ)) |
828 | 824, 827 | breqtrd 5174 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β€ (πΈβπ)) |
829 | 828 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β€ (πΈβπ)) |
830 | 829 | 3adantl3 1169 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β€ (πΈβπ)) |
831 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) = (πβ(π + 1))) |
832 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (π + 1) β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) = (πβ(π + 1))) |
833 | | ovex 7439 |
. . . . . . . . . . . . . 14
β’ (π + 1) β V |
834 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π β (0..^π) β (π + 1) β (0..^π))) |
835 | 834 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((π β§ π β (0..^π)) β (π β§ (π + 1) β (0..^π)))) |
836 | | fveq2 6889 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
837 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
838 | 837 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πβ(π + 1)) = (πβ((π + 1) + 1))) |
839 | 836, 838 | breq12d 5161 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((πβπ) < (πβ(π + 1)) β (πβ(π + 1)) < (πβ((π + 1) + 1)))) |
840 | 835, 839 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ (π + 1) β (0..^π)) β (πβ(π + 1)) < (πβ((π + 1) + 1))))) |
841 | 833, 840,
70 | vtocl 3550 |
. . . . . . . . . . . . 13
β’ ((π β§ (π + 1) β (0..^π)) β (πβ(π + 1)) < (πβ((π + 1) + 1))) |
842 | 841 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π + 1) β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) < (πβ((π + 1) + 1))) |
843 | 832, 842 | eqbrtrd 5170 |
. . . . . . . . . . 11
β’ (((π β§ (π + 1) β (0..^π)) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) < (πβ((π + 1) + 1))) |
844 | 814, 805,
831, 843 | syl21anc 837 |
. . . . . . . . . 10
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) < (πβ((π + 1) + 1))) |
845 | 813, 819,
822, 830, 844 | elicod 13371 |
. . . . . . . . 9
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β ((πβ(π + 1))[,)(πβ((π + 1) + 1)))) |
846 | 836, 838 | oveq12d 7424 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((πβπ)[,)(πβ(π + 1))) = ((πβ(π + 1))[,)(πβ((π + 1) + 1)))) |
847 | 846 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β (πΈβπ) β ((πβ(π + 1))[,)(πβ((π + 1) + 1))))) |
848 | 847 | rspcev 3613 |
. . . . . . . . 9
β’ (((π + 1) β (0..^π) β§ (πΈβπ) β ((πβ(π + 1))[,)(πβ((π + 1) + 1)))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
849 | 805, 845,
848 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ (πΈβπ) = (πβ(π + 1))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
850 | | simpl2 1193 |
. . . . . . . . 9
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β π β (0..^π)) |
851 | | id 22 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
852 | 851 | 3adant1r 1178 |
. . . . . . . . . 10
β’ (((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1))))) |
853 | | elfzofz 13645 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β π β (0...π)) |
854 | 853 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
855 | 806, 854 | ffvelcdmd 7085 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
856 | 855 | rexrd 11261 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (πβπ) β
β*) |
857 | 856 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβπ) β
β*) |
858 | 857 | 3adantl3 1169 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβπ) β
β*) |
859 | 810 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β
β*) |
860 | 859 | 3adantl3 1169 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β
β*) |
861 | 820 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β
β*) |
862 | 861 | 3ad2antl1 1186 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β
β*) |
863 | 855 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβπ) β β) |
864 | 624 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πΈβπ) β β) |
865 | 856 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβπ) β
β*) |
866 | 810 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβ(π + 1)) β
β*) |
867 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) |
868 | | iocgtlb 44202 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§
(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβπ) < (πΈβπ)) |
869 | 865, 866,
867, 868 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβπ) < (πΈβπ)) |
870 | 863, 864,
869 | ltled 11359 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πβπ) β€ (πΈβπ)) |
871 | 870 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβπ) β€ (πΈβπ)) |
872 | 864 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β β) |
873 | 809 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β β) |
874 | 873 | 3adantl3 1169 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β β) |
875 | | iocleub 44203 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β β* β§ (πβ(π + 1)) β β* β§
(πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πΈβπ) β€ (πβ(π + 1))) |
876 | 865, 866,
867, 875 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β (πΈβπ) β€ (πβ(π + 1))) |
877 | 876 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β€ (πβ(π + 1))) |
878 | | neqne 2949 |
. . . . . . . . . . . . . 14
β’ (Β¬
(πΈβπ) = (πβ(π + 1)) β (πΈβπ) β (πβ(π + 1))) |
879 | 878 | necomd 2997 |
. . . . . . . . . . . . 13
β’ (Β¬
(πΈβπ) = (πβ(π + 1)) β (πβ(π + 1)) β (πΈβπ)) |
880 | 879 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πβ(π + 1)) β (πΈβπ)) |
881 | 872, 874,
877, 880 | leneltd 11365 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) < (πβ(π + 1))) |
882 | 858, 860,
862, 871, 881 | elicod 13371 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
883 | 852, 882 | sylan 581 |
. . . . . . . . 9
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
884 | 765, 767 | oveq12d 7424 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ)[,)(πβ(π + 1))) = ((πβπ)[,)(πβ(π + 1)))) |
885 | 884 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = π β ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β (πΈβπ) β ((πβπ)[,)(πβ(π + 1))))) |
886 | 885 | rspcev 3613 |
. . . . . . . . 9
β’ ((π β (0..^π) β§ (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
887 | 850, 883,
886 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β§ Β¬ (πΈβπ) = (πβ(π + 1))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
888 | 849, 887 | pm2.61dan 812 |
. . . . . . 7
β’ (((π β§ (πΈβπ) β π΅) β§ π β (0..^π) β§ (πΈβπ) β ((πβπ)(,](πβ(π + 1)))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
889 | 888 | rexlimdv3a 3160 |
. . . . . 6
β’ ((π β§ (πΈβπ) β π΅) β (βπ β (0..^π)(πΈβπ) β ((πβπ)(,](πβ(π + 1))) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1))))) |
890 | 772, 889 | mpd 15 |
. . . . 5
β’ ((π β§ (πΈβπ) β π΅) β βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
891 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) β (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) |
892 | | oveq1 7413 |
. . . . . . . . . . . . 13
β’ (π = (ββ((π΅ β π) / π)) β (π Β· π) = ((ββ((π΅ β π) / π)) Β· π)) |
893 | 892 | oveq2d 7422 |
. . . . . . . . . . . 12
β’ (π = (ββ((π΅ β π) / π)) β (π + (π Β· π)) = (π + ((ββ((π΅ β π) / π)) Β· π))) |
894 | 893 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = (ββ((π΅ β π) / π)) β ((πΈβπ) = (π + (π Β· π)) β (πΈβπ) = (π + ((ββ((π΅ β π) / π)) Β· π)))) |
895 | 894 | rspcev 3613 |
. . . . . . . . . 10
β’
(((ββ((π΅
β π) / π)) β β€ β§ (πΈβπ) = (π + ((ββ((π΅ β π) / π)) Β· π))) β βπ β β€ (πΈβπ) = (π + (π Β· π))) |
896 | 96, 104, 895 | syl2anc 585 |
. . . . . . . . 9
β’ (π β βπ β β€ (πΈβπ) = (π + (π Β· π))) |
897 | 896 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) β βπ β β€ (πΈβπ) = (π + (π Β· π))) |
898 | | r19.42v 3191 |
. . . . . . . 8
β’
(βπ β
β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))) β ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ βπ β β€ (πΈβπ) = (π + (π Β· π)))) |
899 | 891, 897,
898 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ (πΈβπ) β π΅) β§ (πΈβπ) β ((πβπ)[,)(πβ(π + 1)))) β βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π)))) |
900 | 899 | ex 414 |
. . . . . 6
β’ ((π β§ (πΈβπ) β π΅) β ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))))) |
901 | 900 | reximdv 3171 |
. . . . 5
β’ ((π β§ (πΈβπ) β π΅) β (βπ β (0..^π)(πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))))) |
902 | 890, 901 | mpd 15 |
. . . 4
β’ ((π β§ (πΈβπ) β π΅) β βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π)))) |
903 | 626, 902 | jca 513 |
. . 3
β’ ((π β§ (πΈβπ) β π΅) β (π β§ βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))))) |
904 | | eleq1 2822 |
. . . . . . . 8
β’ (π¦ = (πΈβπ) β (π¦ β ((πβπ)[,)(πβ(π + 1))) β (πΈβπ) β ((πβπ)[,)(πβ(π + 1))))) |
905 | | eqeq1 2737 |
. . . . . . . 8
β’ (π¦ = (πΈβπ) β (π¦ = (π + (π Β· π)) β (πΈβπ) = (π + (π Β· π)))) |
906 | 904, 905 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = (πΈβπ) β ((π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))))) |
907 | 906 | 2rexbidv 3220 |
. . . . . 6
β’ (π¦ = (πΈβπ) β (βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π))) β βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π))))) |
908 | 907 | anbi2d 630 |
. . . . 5
β’ (π¦ = (πΈβπ) β ((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β (π β§ βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π)))))) |
909 | 908 | imbi1d 342 |
. . . 4
β’ (π¦ = (πΈβπ) β (((π β§ βπ β (0..^π)βπ β β€ (π¦ β ((πβπ)[,)(πβ(π + 1))) β§ π¦ = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) β ((π β§ βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
))) |
910 | 909, 611 | vtoclg 3557 |
. . 3
β’ ((πΈβπ) β β β ((π β§ βπ β (0..^π)βπ β β€ ((πΈβπ) β ((πβπ)[,)(πβ(π + 1))) β§ (πΈβπ) = (π + (π Β· π)))) β ((πΉ βΎ (π(,)+β)) limβ π) β
β
)) |
911 | 625, 903,
910 | sylc 65 |
. 2
β’ ((π β§ (πΈβπ) β π΅) β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |
912 | 613, 911 | pm2.61dane 3030 |
1
β’ (π β ((πΉ βΎ (π(,)+β)) limβ π) β β
) |