Metamath Proof Explorer

Theorem fourierdlem27

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

Ref Expression
Hypotheses fourierdlem27.a 
|- ( ph -> A e. RR* )
fourierdlem27.b 
|- ( ph -> B e. RR* )
fourierdlem27.q 
|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
fourierdlem27.i 
|- ( ph -> I e. ( 0 ..^ M ) )
Assertion fourierdlem27 
|- ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( A (,) B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem27.a 
 |-  ( ph -> A e. RR* )
2 fourierdlem27.b 
 |-  ( ph -> B e. RR* )
3 fourierdlem27.q 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
4 fourierdlem27.i 
 |-  ( ph -> I e. ( 0 ..^ M ) )
5 1 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> A e. RR* )
6 2 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> B e. RR* )
7 elioore 
 |-  ( x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) -> x e. RR )
8 7 adantl 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. RR )
9 iccssxr 
 |-  ( A [,] B ) C_ RR*
10 elfzofz 
 |-  ( I e. ( 0 ..^ M ) -> I e. ( 0 ... M ) )
11 4 10 syl 
 |-  ( ph -> I e. ( 0 ... M ) )
12 3 11 ffvelcdmd 
 |-  ( ph -> ( Q ` I ) e. ( A [,] B ) )
13 9 12 sselid 
 |-  ( ph -> ( Q ` I ) e. RR* )
14 13 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) e. RR* )
15 8 rexrd 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. RR* )
16 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` I ) e. ( A [,] B ) ) -> A <_ ( Q ` I ) )
17 1 2 12 16 syl3anc 
 |-  ( ph -> A <_ ( Q ` I ) )
18 17 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> A <_ ( Q ` I ) )
19 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
20 4 19 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
21 3 20 ffvelcdmd 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. ( A [,] B ) )
22 9 21 sselid 
 |-  ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
23 22 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) e. RR* )
24 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
25 ioogtlb 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < x )
26 14 23 24 25 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` I ) < x )
27 5 14 15 18 26 xrlelttrd 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> A < x )
28 iooltub 
 |-  ( ( ( Q ` I ) e. RR* /\ ( Q ` ( I + 1 ) ) e. RR* /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x < ( Q ` ( I + 1 ) ) )
29 14 23 24 28 syl3anc 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x < ( Q ` ( I + 1 ) ) )
30 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( Q ` ( I + 1 ) ) e. ( A [,] B ) ) -> ( Q ` ( I + 1 ) ) <_ B )
31 1 2 21 30 syl3anc 
 |-  ( ph -> ( Q ` ( I + 1 ) ) <_ B )
32 31 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> ( Q ` ( I + 1 ) ) <_ B )
33 15 23 6 29 32 xrltletrd 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x < B )
34 5 6 8 27 33 eliood 
 |-  ( ( ph /\ x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> x e. ( A (,) B ) )
35 34 ralrimiva 
 |-  ( ph -> A. x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) x e. ( A (,) B ) )
36 dfss3 
 |-  ( ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( A (,) B ) <-> A. x e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) x e. ( A (,) B ) )
37 35 36 sylibr 
 |-  ( ph -> ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) C_ ( A (,) B ) )