Metamath Proof Explorer


Theorem fourierdlem38

Description: The function F is continuous on every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem38.cn φ F : dom F cn
fourierdlem38.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
fourierdlem38.m φ M
fourierdlem38.q φ Q P M
fourierdlem38.h H = A π π dom F
fourierdlem38.ranq φ ran Q = H
Assertion fourierdlem38 φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn

Proof

Step Hyp Ref Expression
1 fourierdlem38.cn φ F : dom F cn
2 fourierdlem38.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
3 fourierdlem38.m φ M
4 fourierdlem38.q φ Q P M
5 fourierdlem38.h H = A π π dom F
6 fourierdlem38.ranq φ ran Q = H
7 simplr φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F x Q i Q i + 1
8 simplll φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F φ
9 ioossicc Q i Q i + 1 Q i Q i + 1
10 pire π
11 10 renegcli π
12 11 rexri π *
13 12 a1i φ i 0 ..^ M π *
14 10 rexri π *
15 14 a1i φ i 0 ..^ M π *
16 2 3 4 fourierdlem15 φ Q : 0 M π π
17 16 adantr φ i 0 ..^ M Q : 0 M π π
18 simpr φ i 0 ..^ M i 0 ..^ M
19 13 15 17 18 fourierdlem8 φ i 0 ..^ M Q i Q i + 1 π π
20 9 19 sstrid φ i 0 ..^ M Q i Q i + 1 π π
21 20 sselda φ i 0 ..^ M x Q i Q i + 1 x π π
22 21 adantr φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F x π π
23 simpr φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F ¬ x dom F
24 simpllr φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F i 0 ..^ M
25 3 3ad2ant1 φ x π π ¬ x dom F M
26 4 3ad2ant1 φ x π π ¬ x dom F Q P M
27 simp2 φ x π π ¬ x dom F x π π
28 simp3 φ x π π ¬ x dom F ¬ x dom F
29 27 28 eldifd φ x π π ¬ x dom F x π π dom F
30 elun2 x π π dom F x A π π dom F
31 29 30 syl φ x π π ¬ x dom F x A π π dom F
32 6 5 eqtr2di φ A π π dom F = ran Q
33 32 3ad2ant1 φ x π π ¬ x dom F A π π dom F = ran Q
34 31 33 eleqtrd φ x π π ¬ x dom F x ran Q
35 2 25 26 34 fourierdlem12 φ x π π ¬ x dom F i 0 ..^ M ¬ x Q i Q i + 1
36 8 22 23 24 35 syl31anc φ i 0 ..^ M x Q i Q i + 1 ¬ x dom F ¬ x Q i Q i + 1
37 7 36 condan φ i 0 ..^ M x Q i Q i + 1 x dom F
38 37 ralrimiva φ i 0 ..^ M x Q i Q i + 1 x dom F
39 dfss3 Q i Q i + 1 dom F x Q i Q i + 1 x dom F
40 38 39 sylibr φ i 0 ..^ M Q i Q i + 1 dom F
41 1 adantr φ i 0 ..^ M F : dom F cn
42 rescncf Q i Q i + 1 dom F F : dom F cn F Q i Q i + 1 : Q i Q i + 1 cn
43 40 41 42 sylc φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn