Metamath Proof Explorer


Theorem fourierdlem99

Description: limit for F at the upper bound of an interval for the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem99.f φ F :
fourierdlem99.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem99.t T = B A
fourierdlem99.m φ M
fourierdlem99.q φ Q P M
fourierdlem99.fper φ x F x + T = F x
fourierdlem99.qcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem99.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem99.c φ C
fourierdlem99.d φ D C +∞
fourierdlem99.j φ J 0 ..^ C D y C D | k y + k T ran Q 1
fourierdlem99.v V = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
Assertion fourierdlem99 φ if v v + B v T T V J + 1 = Q y sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < V J + 1 i 0 ..^ M L y sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < V J F v v + B v T T V J + 1 F V J V J + 1 lim V J + 1

Proof

Step Hyp Ref Expression
1 fourierdlem99.f φ F :
2 fourierdlem99.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
3 fourierdlem99.t T = B A
4 fourierdlem99.m φ M
5 fourierdlem99.q φ Q P M
6 fourierdlem99.fper φ x F x + T = F x
7 fourierdlem99.qcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
8 fourierdlem99.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
9 fourierdlem99.c φ C
10 fourierdlem99.d φ D C +∞
11 fourierdlem99.j φ J 0 ..^ C D y C D | k y + k T ran Q 1
12 fourierdlem99.v V = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
13 ax-resscn
14 13 a1i φ
15 1 14 fssd φ F :
16 eqid m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
17 oveq1 z = y z + l T = y + l T
18 17 eleq1d z = y z + l T ran Q y + l T ran Q
19 18 rexbidv z = y l z + l T ran Q l y + l T ran Q
20 19 cbvrabv z C D | l z + l T ran Q = y C D | l y + l T ran Q
21 20 uneq2i C D z C D | l z + l T ran Q = C D y C D | l y + l T ran Q
22 21 eqcomi C D y C D | l y + l T ran Q = C D z C D | l z + l T ran Q
23 oveq1 k = l k T = l T
24 23 oveq2d k = l y + k T = y + l T
25 24 eleq1d k = l y + k T ran Q y + l T ran Q
26 25 cbvrexvw k y + k T ran Q l y + l T ran Q
27 26 a1i y C D k y + k T ran Q l y + l T ran Q
28 27 rabbiia y C D | k y + k T ran Q = y C D | l y + l T ran Q
29 28 uneq2i C D y C D | k y + k T ran Q = C D y C D | l y + l T ran Q
30 29 fveq2i C D y C D | k y + k T ran Q = C D y C D | l y + l T ran Q
31 30 oveq1i C D y C D | k y + k T ran Q 1 = C D y C D | l y + l T ran Q 1
32 oveq1 l = h l T = h T
33 32 oveq2d l = h y + l T = y + h T
34 33 eleq1d l = h y + l T ran Q y + h T ran Q
35 34 cbvrexvw l y + l T ran Q h y + h T ran Q
36 35 a1i y C D l y + l T ran Q h y + h T ran Q
37 36 rabbiia y C D | l y + l T ran Q = y C D | h y + h T ran Q
38 37 uneq2i C D y C D | l y + l T ran Q = C D y C D | h y + h T ran Q
39 isoeq5 C D y C D | l y + l T ran Q = C D y C D | h y + h T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
40 38 39 ax-mp g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
41 40 iotabii ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
42 isoeq1 f = g f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
43 42 cbviotavw ι f | f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
44 41 43 12 3eqtr4ri V = ι f | f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
45 id v = x v = x
46 oveq2 v = x B v = B x
47 46 oveq1d v = x B v T = B x T
48 47 fveq2d v = x B v T = B x T
49 48 oveq1d v = x B v T T = B x T T
50 45 49 oveq12d v = x v + B v T T = x + B x T T
51 50 cbvmptv v v + B v T T = x x + B x T T
52 eqeq1 u = z u = B z = B
53 id u = z u = z
54 52 53 ifbieq2d u = z if u = B A u = if z = B A z
55 54 cbvmptv u A B if u = B A u = z A B if z = B A z
56 eqid V J + 1 v v + B v T T V J + 1 = V J + 1 v v + B v T T V J + 1
57 fveq2 j = i Q j = Q i
58 57 breq1d j = i Q j u A B if u = B A u v v + B v T T y Q i u A B if u = B A u v v + B v T T y
59 58 cbvrabv j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y = i 0 ..^ M | Q i u A B if u = B A u v v + B v T T y
60 fveq2 y = x v v + B v T T y = v v + B v T T x
61 60 fveq2d y = x u A B if u = B A u v v + B v T T y = u A B if u = B A u v v + B v T T x
62 61 breq2d y = x Q i u A B if u = B A u v v + B v T T y Q i u A B if u = B A u v v + B v T T x
63 62 rabbidv y = x i 0 ..^ M | Q i u A B if u = B A u v v + B v T T y = i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x
64 59 63 syl5eq y = x j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y = i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x
65 64 supeq1d y = x sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < = sup i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x <
66 65 cbvmptv y sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < = x sup i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x <
67 eqid i 0 ..^ M L = i 0 ..^ M L
68 2 3 4 5 15 6 7 8 9 10 16 22 31 44 51 55 11 56 66 67 fourierdlem91 φ if v v + B v T T V J + 1 = Q y sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < V J + 1 i 0 ..^ M L y sup j 0 ..^ M | Q j u A B if u = B A u v v + B v T T y < V J F v v + B v T T V J + 1 F V J V J + 1 lim V J + 1