fourierdlem15

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem15.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem15.2	$⊢ φ \to M \in ℕ$
	fourierdlem15.3	$⊢ φ \to Q \in P (M)$
Assertion	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem15.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem15.2	$⊢ φ \to M \in ℕ$
3		fourierdlem15.3	$⊢ φ \to Q \in P (M)$
4	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
5	2 4	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
6	3 5	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
7	6	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
8		reex	$⊢ ℝ \in V$
9	8	a1i	$⊢ φ \to ℝ \in V$
10		ovex	$⊢ (0 \dots M) \in V$
11	10	a1i	$⊢ φ \to (0 \dots M) \in V$
12	9 11	elmapd	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \leftrightarrow Q : (0 \dots M) ⟶ ℝ)$
13	7 12	mpbid	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
14		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
15	13 14	syl	$⊢ φ \to Q Fn (0 \dots M)$
16	6	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
17	16	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
18	17	simpld	$⊢ φ \to Q (0) = A$
19		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
20		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
21	19 20	eleqtrdi	$⊢ M \in ℕ \to M \in ℤ_{\geq 0}$
22	2 21	syl	$⊢ φ \to M \in ℤ_{\geq 0}$
23		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
24	22 23	syl	$⊢ φ \to 0 \in (0 \dots M)$
25	13 24	ffvelrnd	$⊢ φ \to Q (0) \in ℝ$
26	18 25	eqeltrrd	$⊢ φ \to A \in ℝ$
27	26	adantr	$⊢ (φ \land i \in (0 \dots M)) \to A \in ℝ$
28	17	simprd	$⊢ φ \to Q (M) = B$
29		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
30	22 29	syl	$⊢ φ \to M \in (0 \dots M)$
31	13 30	ffvelrnd	$⊢ φ \to Q (M) \in ℝ$
32	28 31	eqeltrrd	$⊢ φ \to B \in ℝ$
33	32	adantr	$⊢ (φ \land i \in (0 \dots M)) \to B \in ℝ$
34	13	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
35	18	eqcomd	$⊢ φ \to A = Q (0)$
36	35	adantr	$⊢ (φ \land i \in (0 \dots M)) \to A = Q (0)$
37		elfzuz	$⊢ i \in (0 \dots M) \to i \in ℤ_{\geq 0}$
38	37	adantl	$⊢ (φ \land i \in (0 \dots M)) \to i \in ℤ_{\geq 0}$
39	13	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i)) \to Q : (0 \dots M) ⟶ ℝ$
40		elfzle1	$⊢ j \in (0 \dots i) \to 0 \leq j$
41	40	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to 0 \leq j$
42		elfzelz	$⊢ j \in (0 \dots i) \to j \in ℤ$
43	42	zred	$⊢ j \in (0 \dots i) \to j \in ℝ$
44	43	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \in ℝ$
45		elfzelz	$⊢ i \in (0 \dots M) \to i \in ℤ$
46	45	zred	$⊢ i \in (0 \dots M) \to i \in ℝ$
47	46	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to i \in ℝ$
48		elfzel2	$⊢ i \in (0 \dots M) \to M \in ℤ$
49	48	zred	$⊢ i \in (0 \dots M) \to M \in ℝ$
50	49	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to M \in ℝ$
51		elfzle2	$⊢ j \in (0 \dots i) \to j \leq i$
52	51	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \leq i$
53		elfzle2	$⊢ i \in (0 \dots M) \to i \leq M$
54	53	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to i \leq M$
55	44 47 50 52 54	letrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \leq M$
56	42	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \in ℤ$
57		0zd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to 0 \in ℤ$
58	48	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to M \in ℤ$
59		elfz	$⊢ (j \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (j \in (0 \dots M) \leftrightarrow (0 \leq j \land j \leq M))$
60	56 57 58 59	syl3anc	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to (j \in (0 \dots M) \leftrightarrow (0 \leq j \land j \leq M))$
61	41 55 60	mpbir2and	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \in (0 \dots M)$
62	61	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i)) \to j \in (0 \dots M)$
63	39 62	ffvelrnd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i)) \to Q (j) \in ℝ$
64		simpll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to φ$
65		elfzle1	$⊢ j \in (0 \dots i - 1) \to 0 \leq j$
66	65	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to 0 \leq j$
67		elfzelz	$⊢ j \in (0 \dots i - 1) \to j \in ℤ$
68	67	zred	$⊢ j \in (0 \dots i - 1) \to j \in ℝ$
69	68	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in ℝ$
70	46	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i \in ℝ$
71	49	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to M \in ℝ$
72		peano2rem	$⊢ i \in ℝ \to i - 1 \in ℝ$
73	70 72	syl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i - 1 \in ℝ$
74		elfzle2	$⊢ j \in (0 \dots i - 1) \to j \leq i - 1$
75	74	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \leq i - 1$
76	70	ltm1d	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i - 1 < i$
77	69 73 70 75 76	lelttrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j < i$
78	53	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i \leq M$
79	69 70 71 77 78	ltletrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j < M$
80	67	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in ℤ$
81		0zd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to 0 \in ℤ$
82	48	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to M \in ℤ$
83		elfzo	$⊢ (j \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (j \in (0 ..^M) \leftrightarrow (0 \leq j \land j < M))$
84	80 81 82 83	syl3anc	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to (j \in (0 ..^M) \leftrightarrow (0 \leq j \land j < M))$
85	66 79 84	mpbir2and	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in (0 ..^M)$
86	85	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to j \in (0 ..^M)$
87	13	adantr	$⊢ (φ \land j \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
88		elfzofz	$⊢ j \in (0 ..^M) \to j \in (0 \dots M)$
89	88	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j \in (0 \dots M)$
90	87 89	ffvelrnd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \in ℝ$
91		fzofzp1	$⊢ j \in (0 ..^M) \to j + 1 \in (0 \dots M)$
92	91	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j + 1 \in (0 \dots M)$
93	87 92	ffvelrnd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ$
94		eleq1w	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
95	94	anbi2d	$⊢ i = j \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j \in (0 ..^M)))$
96		fveq2	$⊢ i = j \to Q (i) = Q (j)$
97		oveq1	$⊢ i = j \to i + 1 = j + 1$
98	97	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
99	96 98	breq12d	$⊢ i = j \to (Q (i) < Q (i + 1) \leftrightarrow Q (j) < Q (j + 1))$
100	95 99	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land j \in (0 ..^M)) \to Q (j) < Q (j + 1)))$
101	16	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
102	101	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
103	100 102	chvarvv	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) < Q (j + 1)$
104	90 93 103	ltled	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \leq Q (j + 1)$
105	64 86 104	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to Q (j) \leq Q (j + 1)$
106	38 63 105	monoord	$⊢ (φ \land i \in (0 \dots M)) \to Q (0) \leq Q (i)$
107	36 106	eqbrtrd	$⊢ (φ \land i \in (0 \dots M)) \to A \leq Q (i)$
108		elfzuz3	$⊢ i \in (0 \dots M) \to M \in ℤ_{\geq i}$
109	108	adantl	$⊢ (φ \land i \in (0 \dots M)) \to M \in ℤ_{\geq i}$
110	13	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to Q : (0 \dots M) ⟶ ℝ$
111		fz0fzelfz0	$⊢ (i \in (0 \dots M) \land j \in (i \dots M)) \to j \in (0 \dots M)$
112	111	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to j \in (0 \dots M)$
113	110 112	ffvelrnd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to Q (j) \in ℝ$
114	13	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q : (0 \dots M) ⟶ ℝ$
115		0red	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \in ℝ$
116	46	adantr	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to i \in ℝ$
117		elfzelz	$⊢ j \in (i \dots M - 1) \to j \in ℤ$
118	117	zred	$⊢ j \in (i \dots M - 1) \to j \in ℝ$
119	118	adantl	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to j \in ℝ$
120		elfzle1	$⊢ i \in (0 \dots M) \to 0 \leq i$
121	120	adantr	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \leq i$
122		elfzle1	$⊢ j \in (i \dots M - 1) \to i \leq j$
123	122	adantl	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to i \leq j$
124	115 116 119 121 123	letrd	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \leq j$
125	124	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq j$
126	118	adantl	$⊢ (φ \land j \in (i \dots M - 1)) \to j \in ℝ$
127	2	nnred	$⊢ φ \to M \in ℝ$
128	127	adantr	$⊢ (φ \land j \in (i \dots M - 1)) \to M \in ℝ$
129		1red	$⊢ (φ \land j \in (i \dots M - 1)) \to 1 \in ℝ$
130	128 129	resubcld	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 \in ℝ$
131		elfzle2	$⊢ j \in (i \dots M - 1) \to j \leq M - 1$
132	131	adantl	$⊢ (φ \land j \in (i \dots M - 1)) \to j \leq M - 1$
133	128	ltm1d	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 < M$
134	126 130 128 132 133	lelttrd	$⊢ (φ \land j \in (i \dots M - 1)) \to j < M$
135	126 128 134	ltled	$⊢ (φ \land j \in (i \dots M - 1)) \to j \leq M$
136	135	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \leq M$
137	117	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in ℤ$
138		0zd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \in ℤ$
139	48	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to M \in ℤ$
140	137 138 139 59	syl3anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to (j \in (0 \dots M) \leftrightarrow (0 \leq j \land j \leq M))$
141	125 136 140	mpbir2and	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in (0 \dots M)$
142	114 141	ffvelrnd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) \in ℝ$
143	118	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in ℝ$
144		1red	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 1 \in ℝ$
145		0le1	$⊢ 0 \leq 1$
146	145	a1i	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq 1$
147	143 144 125 146	addge0d	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq j + 1$
148	126 130 129 132	leadd1dd	$⊢ (φ \land j \in (i \dots M - 1)) \to j + 1 \leq M - 1 + 1$
149	2	nncnd	$⊢ φ \to M \in ℂ$
150	149	adantr	$⊢ (φ \land j \in (i \dots M - 1)) \to M \in ℂ$
151		1cnd	$⊢ (φ \land j \in (i \dots M - 1)) \to 1 \in ℂ$
152	150 151	npcand	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 + 1 = M$
153	148 152	breqtrd	$⊢ (φ \land j \in (i \dots M - 1)) \to j + 1 \leq M$
154	153	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \leq M$
155	137	peano2zd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \in ℤ$
156		elfz	$⊢ (j + 1 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (j + 1 \in (0 \dots M) \leftrightarrow (0 \leq j + 1 \land j + 1 \leq M))$
157	155 138 139 156	syl3anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to (j + 1 \in (0 \dots M) \leftrightarrow (0 \leq j + 1 \land j + 1 \leq M))$
158	147 154 157	mpbir2and	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \in (0 \dots M)$
159	114 158	ffvelrnd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j + 1) \in ℝ$
160		simpll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to φ$
161	134	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j < M$
162	137 138 139 83	syl3anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to (j \in (0 ..^M) \leftrightarrow (0 \leq j \land j < M))$
163	125 161 162	mpbir2and	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in (0 ..^M)$
164	160 163 103	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) < Q (j + 1)$
165	142 159 164	ltled	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) \leq Q (j + 1)$
166	109 113 165	monoord	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq Q (M)$
167	28	adantr	$⊢ (φ \land i \in (0 \dots M)) \to Q (M) = B$
168	166 167	breqtrd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq B$
169	27 33 34 107 168	eliccd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in [A, B]$
170	169	ralrimiva	$⊢ φ \to \forall i \in (0 \dots M) Q (i) \in [A, B]$
171		fnfvrnss	$⊢ (Q Fn (0 \dots M) \land \forall i \in (0 \dots M) Q (i) \in [A, B]) \to ran Q \subseteq [A, B]$
172	15 170 171	syl2anc	$⊢ φ \to ran Q \subseteq [A, B]$
173		df-f	$⊢ Q : (0 \dots M) ⟶ [A, B] \leftrightarrow (Q Fn (0 \dots M) \land ran Q \subseteq [A, B])$
174	15 172 173	sylanbrc	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$

Metamath Proof Explorer

Theorem fourierdlem15

Proof