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	ffvelcdmd	$⊢ φ \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	ffvelcdmd	$⊢ φ \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	ffvelcdmda	$⊢ (φ \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		0zd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to 0 \in ℤ$
41		elfzel2	$⊢ i \in (0 \dots M) \to M \in ℤ$
42	41	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to M \in ℤ$
43		elfzelz	$⊢ 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		elfzle1	$⊢ j \in (0 \dots i) \to 0 \leq j$
46	45	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to 0 \leq j$
47	43	zred	$⊢ j \in (0 \dots i) \to j \in ℝ$
48	47	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \in ℝ$
49		elfzelz	$⊢ i \in (0 \dots M) \to i \in ℤ$
50	49	zred	$⊢ i \in (0 \dots M) \to i \in ℝ$
51	50	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to i \in ℝ$
52	41	zred	$⊢ i \in (0 \dots M) \to M \in ℝ$
53	52	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to M \in ℝ$
54		elfzle2	$⊢ j \in (0 \dots i) \to j \leq i$
55	54	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \leq i$
56		elfzle2	$⊢ i \in (0 \dots M) \to i \leq M$
57	56	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to i \leq M$
58	48 51 53 55 57	letrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \leq M$
59	40 42 44 46 58	elfzd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i)) \to j \in (0 \dots M)$
60	59	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i)) \to j \in (0 \dots M)$
61	39 60	ffvelcdmd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i)) \to Q (j) \in ℝ$
62		simpll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to φ$
63		elfzle1	$⊢ j \in (0 \dots i - 1) \to 0 \leq j$
64	63	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to 0 \leq j$
65		elfzelz	$⊢ j \in (0 \dots i - 1) \to j \in ℤ$
66	65	zred	$⊢ j \in (0 \dots i - 1) \to j \in ℝ$
67	66	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in ℝ$
68	50	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i \in ℝ$
69	52	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to M \in ℝ$
70		peano2rem	$⊢ i \in ℝ \to i - 1 \in ℝ$
71	68 70	syl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i - 1 \in ℝ$
72		elfzle2	$⊢ j \in (0 \dots i - 1) \to j \leq i - 1$
73	72	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \leq i - 1$
74	68	ltm1d	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i - 1 < i$
75	67 71 68 73 74	lelttrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j < i$
76	56	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to i \leq M$
77	67 68 69 75 76	ltletrd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j < M$
78	65	adantl	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in ℤ$
79		0zd	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to 0 \in ℤ$
80	41	adantr	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to M \in ℤ$
81		elfzo	$⊢ (j \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (j \in (0 ..^M) \leftrightarrow (0 \leq j \land j < M))$
82	78 79 80 81	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))$
83	64 77 82	mpbir2and	$⊢ (i \in (0 \dots M) \land j \in (0 \dots i - 1)) \to j \in (0 ..^M)$
84	83	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to j \in (0 ..^M)$
85	13	adantr	$⊢ (φ \land j \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
86		elfzofz	$⊢ j \in (0 ..^M) \to j \in (0 \dots M)$
87	86	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j \in (0 \dots M)$
88	85 87	ffvelcdmd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \in ℝ$
89		fzofzp1	$⊢ j \in (0 ..^M) \to j + 1 \in (0 \dots M)$
90	89	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j + 1 \in (0 \dots M)$
91	85 90	ffvelcdmd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ$
92		eleq1w	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
93	92	anbi2d	$⊢ i = j \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j \in (0 ..^M)))$
94		fveq2	$⊢ i = j \to Q (i) = Q (j)$
95		oveq1	$⊢ i = j \to i + 1 = j + 1$
96	95	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
97	94 96	breq12d	$⊢ i = j \to (Q (i) < Q (i + 1) \leftrightarrow Q (j) < Q (j + 1))$
98	93 97	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)))$
99	16	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
100	99	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
101	98 100	chvarvv	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) < Q (j + 1)$
102	88 91 101	ltled	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \leq Q (j + 1)$
103	62 84 102	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (0 \dots i - 1)) \to Q (j) \leq Q (j + 1)$
104	38 61 103	monoord	$⊢ (φ \land i \in (0 \dots M)) \to Q (0) \leq Q (i)$
105	36 104	eqbrtrd	$⊢ (φ \land i \in (0 \dots M)) \to A \leq Q (i)$
106		elfzuz3	$⊢ i \in (0 \dots M) \to M \in ℤ_{\geq i}$
107	106	adantl	$⊢ (φ \land i \in (0 \dots M)) \to M \in ℤ_{\geq i}$
108	13	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to Q : (0 \dots M) ⟶ ℝ$
109		fz0fzelfz0	$⊢ (i \in (0 \dots M) \land j \in (i \dots M)) \to j \in (0 \dots M)$
110	109	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to j \in (0 \dots M)$
111	108 110	ffvelcdmd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M)) \to Q (j) \in ℝ$
112	13	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q : (0 \dots M) ⟶ ℝ$
113		0zd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \in ℤ$
114	41	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to M \in ℤ$
115		elfzelz	$⊢ j \in (i \dots M - 1) \to j \in ℤ$
116	115	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in ℤ$
117		0red	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \in ℝ$
118	50	adantr	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to i \in ℝ$
119	115	zred	$⊢ j \in (i \dots M - 1) \to j \in ℝ$
120	119	adantl	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to j \in ℝ$
121		elfzle1	$⊢ i \in (0 \dots M) \to 0 \leq i$
122	121	adantr	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \leq i$
123		elfzle1	$⊢ j \in (i \dots M - 1) \to i \leq j$
124	123	adantl	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to i \leq j$
125	117 118 120 122 124	letrd	$⊢ (i \in (0 \dots M) \land j \in (i \dots M - 1)) \to 0 \leq j$
126	125	adantll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq j$
127	119	adantl	$⊢ (φ \land j \in (i \dots M - 1)) \to j \in ℝ$
128	2	nnred	$⊢ φ \to M \in ℝ$
129	128	adantr	$⊢ (φ \land j \in (i \dots M - 1)) \to M \in ℝ$
130		1red	$⊢ (φ \land j \in (i \dots M - 1)) \to 1 \in ℝ$
131	129 130	resubcld	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 \in ℝ$
132		elfzle2	$⊢ j \in (i \dots M - 1) \to j \leq M - 1$
133	132	adantl	$⊢ (φ \land j \in (i \dots M - 1)) \to j \leq M - 1$
134	129	ltm1d	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 < M$
135	127 131 129 133 134	lelttrd	$⊢ (φ \land j \in (i \dots M - 1)) \to j < M$
136	127 129 135	ltled	$⊢ (φ \land j \in (i \dots M - 1)) \to j \leq M$
137	136	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \leq M$
138	113 114 116 126 137	elfzd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in (0 \dots M)$
139	112 138	ffvelcdmd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) \in ℝ$
140	116	peano2zd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \in ℤ$
141	119	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in ℝ$
142		1red	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 1 \in ℝ$
143		0le1	$⊢ 0 \leq 1$
144	143	a1i	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq 1$
145	141 142 126 144	addge0d	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to 0 \leq j + 1$
146	127 131 130 133	leadd1dd	$⊢ (φ \land j \in (i \dots M - 1)) \to j + 1 \leq M - 1 + 1$
147	2	nncnd	$⊢ φ \to M \in ℂ$
148	147	adantr	$⊢ (φ \land j \in (i \dots M - 1)) \to M \in ℂ$
149		1cnd	$⊢ (φ \land j \in (i \dots M - 1)) \to 1 \in ℂ$
150	148 149	npcand	$⊢ (φ \land j \in (i \dots M - 1)) \to M - 1 + 1 = M$
151	146 150	breqtrd	$⊢ (φ \land j \in (i \dots M - 1)) \to j + 1 \leq M$
152	151	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \leq M$
153	113 114 140 145 152	elfzd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j + 1 \in (0 \dots M)$
154	112 153	ffvelcdmd	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j + 1) \in ℝ$
155		simpll	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to φ$
156	135	adantlr	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j < M$
157	116 113 114 81	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))$
158	126 156 157	mpbir2and	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to j \in (0 ..^M)$
159	155 158 101	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) < Q (j + 1)$
160	139 154 159	ltled	$⊢ ((φ \land i \in (0 \dots M)) \land j \in (i \dots M - 1)) \to Q (j) \leq Q (j + 1)$
161	107 111 160	monoord	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq Q (M)$
162	28	adantr	$⊢ (φ \land i \in (0 \dots M)) \to Q (M) = B$
163	161 162	breqtrd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq B$
164	27 33 34 105 163	eliccd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in [A, B]$
165	164	ralrimiva	$⊢ φ \to \forall i \in (0 \dots M) Q (i) \in [A, B]$
166		fnfvrnss	$⊢ (Q Fn (0 \dots M) \land \forall i \in (0 \dots M) Q (i) \in [A, B]) \to ran Q \subseteq [A, B]$
167	15 165 166	syl2anc	$⊢ φ \to ran Q \subseteq [A, B]$
168		df-f	$⊢ Q : (0 \dots M) ⟶ [A, B] \leftrightarrow (Q Fn (0 \dots M) \land ran Q \subseteq [A, B])$
169	15 167 168	sylanbrc	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$

Metamath Proof Explorer

Theorem fourierdlem15

Proof