Metamath Proof Explorer


Theorem fourierdlem37

Description: I is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem37.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem37.m φ M
fourierdlem37.q φ Q P M
fourierdlem37.t T = B A
fourierdlem37.e E = x x + B x T T
fourierdlem37.l L = y A B if y = B A y
fourierdlem37.i I = x sup i 0 ..^ M | Q i L E x <
Assertion fourierdlem37 φ I : 0 ..^ M x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x

Proof

Step Hyp Ref Expression
1 fourierdlem37.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
2 fourierdlem37.m φ M
3 fourierdlem37.q φ Q P M
4 fourierdlem37.t T = B A
5 fourierdlem37.e E = x x + B x T T
6 fourierdlem37.l L = y A B if y = B A y
7 fourierdlem37.i I = x sup i 0 ..^ M | Q i L E x <
8 ssrab2 i 0 ..^ M | Q i L E x 0 ..^ M
9 ltso < Or
10 9 a1i φ x < Or
11 fzfi 0 M Fin
12 fzossfz 0 ..^ M 0 M
13 8 12 sstri i 0 ..^ M | Q i L E x 0 M
14 ssfi 0 M Fin i 0 ..^ M | Q i L E x 0 M i 0 ..^ M | Q i L E x Fin
15 11 13 14 mp2an i 0 ..^ M | Q i L E x Fin
16 15 a1i φ x i 0 ..^ M | Q i L E x Fin
17 0zd φ 0
18 2 nnzd φ M
19 2 nngt0d φ 0 < M
20 fzolb 0 0 ..^ M 0 M 0 < M
21 17 18 19 20 syl3anbrc φ 0 0 ..^ M
22 21 adantr φ x 0 0 ..^ M
23 1 fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
24 2 23 syl φ Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
25 3 24 mpbid φ Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
26 25 simprd φ Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
27 26 simplld φ Q 0 = A
28 1 2 3 fourierdlem11 φ A B A < B
29 28 simp1d φ A
30 27 29 eqeltrd φ Q 0
31 30 27 eqled φ Q 0 A
32 31 ad2antrr φ x E x = B Q 0 A
33 iftrue E x = B if E x = B A E x = A
34 33 eqcomd E x = B A = if E x = B A E x
35 34 adantl φ x E x = B A = if E x = B A E x
36 32 35 breqtrd φ x E x = B Q 0 if E x = B A E x
37 30 adantr φ x Q 0
38 29 adantr φ x A
39 38 rexrd φ x A *
40 28 simp2d φ B
41 40 adantr φ x B
42 iocssre A * B A B
43 39 41 42 syl2anc φ x A B
44 28 simp3d φ A < B
45 29 40 44 4 5 fourierdlem4 φ E : A B
46 45 ffvelrnda φ x E x A B
47 43 46 sseldd φ x E x
48 27 adantr φ x Q 0 = A
49 elioc2 A * B E x A B E x A < E x E x B
50 39 41 49 syl2anc φ x E x A B E x A < E x E x B
51 46 50 mpbid φ x E x A < E x E x B
52 51 simp2d φ x A < E x
53 48 52 eqbrtrd φ x Q 0 < E x
54 37 47 53 ltled φ x Q 0 E x
55 54 adantr φ x ¬ E x = B Q 0 E x
56 iffalse ¬ E x = B if E x = B A E x = E x
57 56 eqcomd ¬ E x = B E x = if E x = B A E x
58 57 adantl φ x ¬ E x = B E x = if E x = B A E x
59 55 58 breqtrd φ x ¬ E x = B Q 0 if E x = B A E x
60 36 59 pm2.61dan φ x Q 0 if E x = B A E x
61 6 a1i φ x L = y A B if y = B A y
62 eqeq1 y = E x y = B E x = B
63 id y = E x y = E x
64 62 63 ifbieq2d y = E x if y = B A y = if E x = B A E x
65 64 adantl φ x y = E x if y = B A y = if E x = B A E x
66 38 47 ifcld φ x if E x = B A E x
67 61 65 46 66 fvmptd φ x L E x = if E x = B A E x
68 60 67 breqtrrd φ x Q 0 L E x
69 fveq2 i = 0 Q i = Q 0
70 69 breq1d i = 0 Q i L E x Q 0 L E x
71 70 elrab 0 i 0 ..^ M | Q i L E x 0 0 ..^ M Q 0 L E x
72 22 68 71 sylanbrc φ x 0 i 0 ..^ M | Q i L E x
73 72 ne0d φ x i 0 ..^ M | Q i L E x
74 fzssz 0 M
75 12 74 sstri 0 ..^ M
76 zssre
77 75 76 sstri 0 ..^ M
78 8 77 sstri i 0 ..^ M | Q i L E x
79 78 a1i φ x i 0 ..^ M | Q i L E x
80 fisupcl < Or i 0 ..^ M | Q i L E x Fin i 0 ..^ M | Q i L E x i 0 ..^ M | Q i L E x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
81 10 16 73 79 80 syl13anc φ x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
82 8 81 sseldi φ x sup i 0 ..^ M | Q i L E x < 0 ..^ M
83 82 7 fmptd φ I : 0 ..^ M
84 81 ex φ x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x
85 83 84 jca φ I : 0 ..^ M x sup i 0 ..^ M | Q i L E x < i 0 ..^ M | Q i L E x