fourierdlem8

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

Step	Hyp	Ref	Expression
1		fourierdlem8.a	$⊢ φ \to A \in ℝ^{*}$
2		fourierdlem8.b	$⊢ φ \to B \in ℝ^{*}$
3		fourierdlem8.q	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
4		fourierdlem8.i	$⊢ φ \to I \in (0 ..^M)$
5	1	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to A \in ℝ^{*}$
6	2	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to B \in ℝ^{*}$
7	3	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to Q : (0 \dots M) ⟶ [A, B]$
8	4	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to I \in (0 ..^M)$
9		simpr	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to x \in [Q (I), Q (I + 1)]$
10	5 6 7 8 9	fourierdlem1	$⊢ (φ \land x \in [Q (I), Q (I + 1)]) \to x \in [A, B]$
11	10	ralrimiva	$⊢ φ \to \forall x \in [Q (I), Q (I + 1)] x \in [A, B]$
12		dfss3	$⊢ [Q (I), Q (I + 1)] \subseteq [A, B] \leftrightarrow \forall x \in [Q (I), Q (I + 1)] x \in [A, B]$
13	11 12	sylibr	$⊢ φ \to [Q (I), Q (I + 1)] \subseteq [A, B]$

Metamath Proof Explorer