Metamath Proof Explorer


Theorem fourierdlem1

Description: A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem1.a φ A *
fourierdlem1.b φ B *
fourierdlem1.q φ Q : 0 M A B
fourierdlem1.i φ I 0 ..^ M
fourierdlem1.x φ X Q I Q I + 1
Assertion fourierdlem1 φ X A B

Proof

Step Hyp Ref Expression
1 fourierdlem1.a φ A *
2 fourierdlem1.b φ B *
3 fourierdlem1.q φ Q : 0 M A B
4 fourierdlem1.i φ I 0 ..^ M
5 fourierdlem1.x φ X Q I Q I + 1
6 iccssxr Q I Q I + 1 *
7 6 5 sseldi φ X *
8 iccssxr A B *
9 elfzofz I 0 ..^ M I 0 M
10 4 9 syl φ I 0 M
11 3 10 ffvelrnd φ Q I A B
12 8 11 sseldi φ Q I *
13 iccgelb A * B * Q I A B A Q I
14 1 2 11 13 syl3anc φ A Q I
15 fzofzp1 I 0 ..^ M I + 1 0 M
16 4 15 syl φ I + 1 0 M
17 3 16 ffvelrnd φ Q I + 1 A B
18 8 17 sseldi φ Q I + 1 *
19 elicc4 Q I * Q I + 1 * X * X Q I Q I + 1 Q I X X Q I + 1
20 12 18 7 19 syl3anc φ X Q I Q I + 1 Q I X X Q I + 1
21 5 20 mpbid φ Q I X X Q I + 1
22 21 simpld φ Q I X
23 1 12 7 14 22 xrletrd φ A X
24 iccleub Q I * Q I + 1 * X Q I Q I + 1 X Q I + 1
25 12 18 5 24 syl3anc φ X Q I + 1
26 elicc4 A * B * Q I + 1 * Q I + 1 A B A Q I + 1 Q I + 1 B
27 1 2 18 26 syl3anc φ Q I + 1 A B A Q I + 1 Q I + 1 B
28 17 27 mpbid φ A Q I + 1 Q I + 1 B
29 28 simprd φ Q I + 1 B
30 7 18 2 25 29 xrletrd φ X B
31 elicc1 A * B * X A B X * A X X B
32 1 2 31 syl2anc φ X A B X * A X X B
33 7 23 30 32 mpbir3and φ X A B