This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem8

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem8.a 
 |-  ( ph -> A e. RR* )
2 fourierdlem8.b 
 |-  ( ph -> B e. RR* )
3 fourierdlem8.q 
 |-  ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )
4 fourierdlem8.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 3 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) ) -> Q : ( 0 ... M ) --> ( A [,] B ) )
8 4 adantr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) ) -> I e. ( 0 ..^ M ) )
9 simpr 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) ) -> x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) )
10 5 6 7 8 9 fourierdlem1 
 |-  ( ( ph /\ x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) ) -> x e. ( A [,] B ) )
11 10 ralrimiva 
 |-  ( ph -> A. x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) x e. ( A [,] B ) )
12 dfss3 
 |-  ( ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) C_ ( A [,] B ) <-> A. x e. ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) x e. ( A [,] B ) )
13 11 12 sylibr 
 |-  ( ph -> ( ( Q ` I ) [,] ( Q ` ( I + 1 ) ) ) C_ ( A [,] B ) )