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	$⊢ φ \to A \in ℝ^{*}$
	fourierdlem27.b	$⊢ φ \to B \in ℝ^{*}$
	fourierdlem27.q	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
	fourierdlem27.i	$⊢ φ \to I \in (0 ..^M)$
Assertion	fourierdlem27	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (A, B)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem27.a	$⊢ φ \to A \in ℝ^{*}$
2		fourierdlem27.b	$⊢ φ \to B \in ℝ^{*}$
3		fourierdlem27.q	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
4		fourierdlem27.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		elioore	$⊢ x \in (Q (I), Q (I + 1)) \to x \in ℝ$
8	7	adantl	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in ℝ$
9		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
10		elfzofz	$⊢ I \in (0 ..^M) \to I \in (0 \dots M)$
11	4 10	syl	$⊢ φ \to I \in (0 \dots M)$
12	3 11	ffvelrnd	$⊢ φ \to Q (I) \in [A, B]$
13	9 12	sseldi	$⊢ φ \to Q (I) \in ℝ^{*}$
14	13	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to Q (I) \in ℝ^{*}$
15	8	rexrd	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in ℝ^{*}$
16		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (I) \in [A, B]) \to A \leq Q (I)$
17	1 2 12 16	syl3anc	$⊢ φ \to A \leq Q (I)$
18	17	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to A \leq Q (I)$
19		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
20	4 19	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
21	3 20	ffvelrnd	$⊢ φ \to Q (I + 1) \in [A, B]$
22	9 21	sseldi	$⊢ φ \to Q (I + 1) \in ℝ^{*}$
23	22	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to Q (I + 1) \in ℝ^{*}$
24		simpr	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in (Q (I), Q (I + 1))$
25		ioogtlb	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in (Q (I), Q (I + 1))) \to Q (I) < x$
26	14 23 24 25	syl3anc	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to Q (I) < x$
27	5 14 15 18 26	xrlelttrd	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to A < x$
28		iooltub	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in (Q (I), Q (I + 1))) \to x < Q (I + 1)$
29	14 23 24 28	syl3anc	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x < Q (I + 1)$
30		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (I + 1) \in [A, B]) \to Q (I + 1) \leq B$
31	1 2 21 30	syl3anc	$⊢ φ \to Q (I + 1) \leq B$
32	31	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to Q (I + 1) \leq B$
33	15 23 6 29 32	xrltletrd	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x < B$
34	5 6 8 27 33	eliood	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in (A, B)$
35	34	ralrimiva	$⊢ φ \to \forall x \in (Q (I), Q (I + 1)) x \in (A, B)$
36		dfss3	$⊢ (Q (I), Q (I + 1)) \subseteq (A, B) \leftrightarrow \forall x \in (Q (I), Q (I + 1)) x \in (A, B)$
37	35 36	sylibr	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (A, B)$

Metamath Proof Explorer

Theorem fourierdlem27

Proof