fourierdlem1

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

	Ref	Expression
Hypotheses	fourierdlem1.a	$⊢ φ \to A \in ℝ^{*}$
	fourierdlem1.b	$⊢ φ \to B \in ℝ^{*}$
	fourierdlem1.q	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
	fourierdlem1.i	$⊢ φ \to I \in (0 ..^M)$
	fourierdlem1.x	$⊢ φ \to X \in [Q (I), Q (I + 1)]$
Assertion	fourierdlem1	$⊢ φ \to X \in [A, B]$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem1.a	$⊢ φ \to A \in ℝ^{*}$
2		fourierdlem1.b	$⊢ φ \to B \in ℝ^{*}$
3		fourierdlem1.q	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
4		fourierdlem1.i	$⊢ φ \to I \in (0 ..^M)$
5		fourierdlem1.x	$⊢ φ \to X \in [Q (I), Q (I + 1)]$
6		iccssxr	$⊢ [Q (I), Q (I + 1)] \subseteq ℝ^{*}$
7	6 5	sselid	$⊢ φ \to X \in ℝ^{*}$
8		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
9		elfzofz	$⊢ I \in (0 ..^M) \to I \in (0 \dots M)$
10	4 9	syl	$⊢ φ \to I \in (0 \dots M)$
11	3 10	ffvelrnd	$⊢ φ \to Q (I) \in [A, B]$
12	8 11	sselid	$⊢ φ \to Q (I) \in ℝ^{*}$
13		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (I) \in [A, B]) \to A \leq Q (I)$
14	1 2 11 13	syl3anc	$⊢ φ \to A \leq Q (I)$
15		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
16	4 15	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
17	3 16	ffvelrnd	$⊢ φ \to Q (I + 1) \in [A, B]$
18	8 17	sselid	$⊢ φ \to Q (I + 1) \in ℝ^{*}$
19		elicc4	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land X \in ℝ^{*}) \to (X \in [Q (I), Q (I + 1)] \leftrightarrow (Q (I) \leq X \land X \leq Q (I + 1)))$
20	12 18 7 19	syl3anc	$⊢ φ \to (X \in [Q (I), Q (I + 1)] \leftrightarrow (Q (I) \leq X \land X \leq Q (I + 1)))$
21	5 20	mpbid	$⊢ φ \to (Q (I) \leq X \land X \leq Q (I + 1))$
22	21	simpld	$⊢ φ \to Q (I) \leq X$
23	1 12 7 14 22	xrletrd	$⊢ φ \to A \leq X$
24		iccleub	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land X \in [Q (I), Q (I + 1)]) \to X \leq Q (I + 1)$
25	12 18 5 24	syl3anc	$⊢ φ \to X \leq Q (I + 1)$
26		elicc4	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (I + 1) \in ℝ^{*}) \to (Q (I + 1) \in [A, B] \leftrightarrow (A \leq Q (I + 1) \land Q (I + 1) \leq B))$
27	1 2 18 26	syl3anc	$⊢ φ \to (Q (I + 1) \in [A, B] \leftrightarrow (A \leq Q (I + 1) \land Q (I + 1) \leq B))$
28	17 27	mpbid	$⊢ φ \to (A \leq Q (I + 1) \land Q (I + 1) \leq B)$
29	28	simprd	$⊢ φ \to Q (I + 1) \leq B$
30	7 18 2 25 29	xrletrd	$⊢ φ \to X \leq B$
31		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (X \in [A, B] \leftrightarrow (X \in ℝ^{*} \land A \leq X \land X \leq B))$
32	1 2 31	syl2anc	$⊢ φ \to (X \in [A, B] \leftrightarrow (X \in ℝ^{*} \land A \leq X \land X \leq B))$
33	7 23 30 32	mpbir3and	$⊢ φ \to X \in [A, B]$

Metamath Proof Explorer

Theorem fourierdlem1

Proof