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 
|- ( ph -> A e. RR* )
fourierdlem1.b 
|- ( ph -> B e. RR* )
fourierdlem1.q 
|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
fourierdlem1.i 
|- ( ph -> I e. ( 0 ..^ M ) )
fourierdlem1.x 
|- ( ph -> X e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) )
Assertion fourierdlem1 
|- ( ph -> X e. ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem1.a 
 |-  ( ph -> A e. RR* )
2 fourierdlem1.b 
 |-  ( ph -> B e. RR* )
3 fourierdlem1.q 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
4 fourierdlem1.i 
 |-  ( ph -> I e. ( 0 ..^ M ) )
5 fourierdlem1.x 
 |-  ( ph -> X e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) )
6 iccssxr 
 |-  ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) C_ RR*
7 6 5 sselid 
 |-  ( ph -> X e. RR* )
8 iccssxr 
 |-  ( A [,] B ) C_ RR*
9 elfzofz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ( 0 ... M ) )
10 4 9 syl 
 |-  ( ph -> I e. ( 0 ... M ) )
11 3 10 ffvelrnd 
 |-  ( ph -> ( Q ` I ) e. ( A [,] B ) )
12 8 11 sselid 
 |-  ( ph -> ( Q ` I ) e. RR* )
13 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` I ) e. ( A [,] B ) ) -> A <_ ( Q ` I ) )
14 1 2 11 13 syl3anc 
 |-  ( ph -> A <_ ( Q ` I ) )
15 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
16 4 15 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
17 3 16 ffvelrnd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. ( A [,] B ) )
18 8 17 sselid 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
19 elicc4 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ X e. RR* ) -> ( X e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) <-> ( ( Q ` I ) <_ X /\ X <_ ( Q ` ( I + 1 ) ) ) ) )
20 12 18 7 19 syl3anc 
 |-  ( ph -> ( X e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) <-> ( ( Q ` I ) <_ X /\ X <_ ( Q ` ( I + 1 ) ) ) ) )
21 5 20 mpbid 
 |-  ( ph -> ( ( Q ` I ) <_ X /\ X <_ ( Q ` ( I + 1 ) ) ) )
22 21 simpld 
 |-  ( ph -> ( Q ` I ) <_ X )
23 1 12 7 14 22 xrletrd 
 |-  ( ph -> A <_ X )
24 iccleub 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ X e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) ) -> X <_ ( Q ` ( I + 1 ) ) )
25 12 18 5 24 syl3anc 
 |-  ( ph -> X <_ ( Q ` ( I + 1 ) ) )
26 elicc4 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* ) -> ( ( Q ` ( I + 1 ) ) e. ( A [,] B ) <-> ( A <_ ( Q ` ( I + 1 ) ) /\ ( Q ` ( I + 1 ) ) <_ B ) ) )
27 1 2 18 26 syl3anc 
 |-  ( ph -> ( ( Q ` ( I + 1 ) ) e. ( A [,] B ) <-> ( A <_ ( Q ` ( I + 1 ) ) /\ ( Q ` ( I + 1 ) ) <_ B ) ) )
28 17 27 mpbid 
 |-  ( ph -> ( A <_ ( Q ` ( I + 1 ) ) /\ ( Q ` ( I + 1 ) ) <_ B ) )
29 28 simprd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) <_ B )
30 7 18 2 25 29 xrletrd 
 |-  ( ph -> X <_ B )
31 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( X e. ( A [,] B ) <-> ( X e. RR* /\ A <_ X /\ X <_ B ) ) )
32 1 2 31 syl2anc 
 |-  ( ph -> ( X e. ( A [,] B ) <-> ( X e. RR* /\ A <_ X /\ X <_ B ) ) )
33 7 23 30 32 mpbir3and 
 |-  ( ph -> X e. ( A [,] B ) )