Theorem fourierdlem15 37861

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

Hypotheses

Ref	Expression
fourierdlem15.1	|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem15.2	|- ( ph -> M e. NN )
fourierdlem15.3	|- ( ph -> Q e. ( P ` M ) )

Assertion

Ref	Expression
fourierdlem15	|- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )

Distinct variable groups:   A, i, m, p   B, i, m, p   i, M, m, p   Q, i, p   ph, i

Allowed substitution hints:   ph( m, p)   P( i, m, p)   Q( m)

Proof of Theorem fourierdlem15

Dummy variable j is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem15.3	. . . . . 6 |- ( ph -> Q e. ( P ` M ) )
2		fourierdlem15.2	. . . . . . 7 |- ( ph -> M e. NN )
3		fourierdlem15.1	. . . . . . . 8 |- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4	3	fourierdlem2 37848	. . . . . . 7 |- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
5	2, 4	syl 17	. . . . . 6 |- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
6	1, 5	mpbid 213	. . . . 5 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
7	6	simpld 460	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		reex 9574	. . . . . 6 |- RR e. _V
9	8	a1i 11	. . . . 5 |- ( ph -> RR e. _V )
10		ovex 6270	. . . . . 6 |- ( 0 ... M ) e. _V
11	10	a1i 11	. . . . 5 |- ( ph -> ( 0 ... M ) e. _V )
12	9, 11	elmapd 7434	. . . 4 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
13	7, 12	mpbid 213	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
14		ffn 5682	. . 3 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
15	13, 14	syl 17	. 2 |- ( ph -> Q Fn ( 0 ... M ) )
16	6	simprd 464	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
17	16	simpld 460	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
18	17	simpld 460	. . . . . . 7 |- ( ph -> ( Q ` 0 ) = A )
19		nnnn0 10820	. . . . . . . . . . 11 |- ( M e. NN -> M e. NN0 )
20		nn0uz 11137	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
21	19, 20	syl6eleq 2510	. . . . . . . . . 10 |- ( M e. NN -> M e. ( ZZ>= ` 0 ) )
22	2, 21	syl 17	. . . . . . . . 9 |- ( ph -> M e. ( ZZ>= ` 0 ) )
23		eluzfz1 11750	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
24	22, 23	syl 17	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
25	13, 24	ffvelrnd 5975	. . . . . . 7 |- ( ph -> ( Q ` 0 ) e. RR )
26	18, 25	eqeltrrd 2501	. . . . . 6 |- ( ph -> A e. RR )
27	26	adantr 466	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A e. RR )
28	17	simprd 464	. . . . . . 7 |- ( ph -> ( Q ` M ) = B )
29		eluzfz2 11751	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
30	22, 29	syl 17	. . . . . . . 8 |- ( ph -> M e. ( 0 ... M ) )
31	13, 30	ffvelrnd 5975	. . . . . . 7 |- ( ph -> ( Q ` M ) e. RR )
32	28, 31	eqeltrrd 2501	. . . . . 6 |- ( ph -> B e. RR )
33	32	adantr 466	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> B e. RR )
34	13	ffvelrnda 5974	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
35	18	eqcomd 2428	. . . . . . 7 |- ( ph -> A = ( Q ` 0 ) )
36	35	adantr 466	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A = ( Q ` 0 ) )
37		elfzuz 11740	. . . . . . . 8 |- ( i e. ( 0 ... M ) -> i e. ( ZZ>= ` 0 ) )
38	37	adantl 467	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( ZZ>= ` 0 ) )
39	13	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> Q : ( 0 ... M ) --> RR )
40		elfzle1 11746	. . . . . . . . . . 11 |- ( j e. ( 0 ... i ) -> 0 <_ j )
41	40	adantl 467	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 <_ j )
42		elfzelz 11744	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... i ) -> j e. ZZ )
43	42	zred 10984	. . . . . . . . . . . 12 |- ( j e. ( 0 ... i ) -> j e. RR )
44	43	adantl 467	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. RR )
45		elfzelz 11744	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> i e. ZZ )
46	45	zred 10984	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> i e. RR )
47	46	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i e. RR )
48		elfzel2 11742	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> M e. ZZ )
49	48	zred 10984	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> M e. RR )
50	49	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. RR )
51		elfzle2 11747	. . . . . . . . . . . 12 |- ( j e. ( 0 ... i ) -> j <_ i )
52	51	adantl 467	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ i )
53		elfzle2 11747	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> i <_ M )
54	53	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i <_ M )
55	44, 47, 50, 52, 54	letrd 9736	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ M )
56	42	adantl 467	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ZZ )
57		0zd 10893	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 e. ZZ )
58	48	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. ZZ )
59		elfz 11734	. . . . . . . . . . 11 |- ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
60	56, 57, 58, 59	syl3anc 1264	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
61	41, 55, 60	mpbir2and 930	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
62	61	adantll 718	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
63	39, 62	ffvelrnd 5975	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> ( Q ` j ) e. RR )
64		simpll 758	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ph )
65		elfzle1 11746	. . . . . . . . . . 11 |- ( j e. ( 0 ... ( i - 1 ) ) -> 0 <_ j )
66	65	adantl 467	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 <_ j )
67		elfzelz 11744	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... ( i - 1 ) ) -> j e. ZZ )
68	67	zred 10984	. . . . . . . . . . . 12 |- ( j e. ( 0 ... ( i - 1 ) ) -> j e. RR )
69	68	adantl 467	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. RR )
70	46	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i e. RR )
71	49	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. RR )
72		peano2rem 9885	. . . . . . . . . . . . 13 |- ( i e. RR -> ( i - 1 ) e. RR )
73	70, 72	syl 17	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR )
74		elfzle2 11747	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
75	74	adantl 467	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
76	70	ltm1d 10483	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
77	69, 73, 70, 75, 76	lelttrd 9737	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < i )
78	53	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i <_ M )
79	69, 70, 71, 77, 78	ltletrd 9739	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < M )
80	67	adantl 467	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ZZ )
81		0zd 10893	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 e. ZZ )
82	48	adantr 466	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. ZZ )
83		elfzo 11866	. . . . . . . . . . 11 |- ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
84	80, 81, 82, 83	syl3anc 1264	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
85	66, 79, 84	mpbir2and 930	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0..^ M ) )
86	85	adantll 718	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0..^ M ) )
87	13	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
88		elfzofz 11879	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) -> j e. ( 0 ... M ) )
89	88	adantl 467	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> j e. ( 0 ... M ) )
90	87, 89	ffvelrnd 5975	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) e. RR )
91		fzofzp1 11951	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
92	91	adantl 467	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
93	87, 92	ffvelrnd 5975	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
94		eleq1 2488	. . . . . . . . . . . 12 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
95	94	anbi2d 708	. . . . . . . . . . 11 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
96		fveq2 5818	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
97		oveq1 6249	. . . . . . . . . . . . 13 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
98	97	fveq2d 5822	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
99	96, 98	breq12d 4372	. . . . . . . . . . 11 |- ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
100	95, 99	imbi12d 321	. . . . . . . . . 10 |- ( i = j -> ( ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) ) )
101	16	simprd 464	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
102	101	r19.21bi 2728	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
103	100, 102	chvarv 2073	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
104	90, 93, 103	ltled 9727	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
105	64, 86, 104	syl2anc 665	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
106	38, 63, 105	monoord 12186	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` 0 ) <_ ( Q ` i ) )
107	36, 106	eqbrtrd 4380	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A <_ ( Q ` i ) )
108		elfzuz3 11741	. . . . . . . 8 |- ( i e. ( 0 ... M ) -> M e. ( ZZ>= ` i ) )
109	108	adantl 467	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> M e. ( ZZ>= ` i ) )
110	13	ad2antrr 730	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> Q : ( 0 ... M ) --> RR )
111		fz0fzelfz0 11840	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
112	111	adantll 718	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
113	110, 112	ffvelrnd 5975	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> ( Q ` j ) e. RR )
114	13	ad2antrr 730	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
115		0red 9588	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. RR )
116	46	adantr 466	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i e. RR )
117		elfzelz 11744	. . . . . . . . . . . . . 14 |- ( j e. ( i ... ( M - 1 ) ) -> j e. ZZ )
118	117	zred 10984	. . . . . . . . . . . . 13 |- ( j e. ( i ... ( M - 1 ) ) -> j e. RR )
119	118	adantl 467	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
120		elfzle1 11746	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> 0 <_ i )
121	120	adantr 466	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ i )
122		elfzle1 11746	. . . . . . . . . . . . 13 |- ( j e. ( i ... ( M - 1 ) ) -> i <_ j )
123	122	adantl 467	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i <_ j )
124	115, 116, 119, 121, 123	letrd 9736	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
125	124	adantll 718	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
126	118	adantl 467	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
127	2	nnred 10568	. . . . . . . . . . . . 13 |- ( ph -> M e. RR )
128	127	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. RR )
129		1red 9602	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
130	128, 129	resubcld 9991	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) e. RR )
131		elfzle2 11747	. . . . . . . . . . . . . 14 |- ( j e. ( i ... ( M - 1 ) ) -> j <_ ( M - 1 ) )
132	131	adantl 467	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ ( M - 1 ) )
133	128	ltm1d 10483	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) < M )
134	126, 130, 128, 132, 133	lelttrd 9737	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
135	126, 128, 134	ltled 9727	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
136	135	adantlr 719	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
137	117	adantl 467	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ZZ )
138		0zd 10893	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. ZZ )
139	48	ad2antlr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> M e. ZZ )
140	137, 138, 139, 59	syl3anc 1264	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
141	125, 136, 140	mpbir2and 930	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ... M ) )
142	114, 141	ffvelrnd 5975	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) e. RR )
143	118	adantl 467	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
144		1red 9602	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
145		0le1 10081	. . . . . . . . . . . 12 |- 0 <_ 1
146	145	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ 1 )
147	143, 144, 125, 146	addge0d 10133	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ ( j + 1 ) )
148	126, 130, 129, 132	leadd1dd 10171	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ ( ( M - 1 ) + 1 ) )
149	2	nncnd 10569	. . . . . . . . . . . . . 14 |- ( ph -> M e. CC )
150	149	adantr 466	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. CC )
151		1cnd 9603	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. CC )
152	150, 151	npcand 9934	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
153	148, 152	breqtrd 4384	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
154	153	adantlr 719	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
155	137	peano2zd 10987	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ZZ )
156		elfz 11734	. . . . . . . . . . 11 |- ( ( ( j + 1 ) e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( ( j + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( j + 1 ) /\ ( j + 1 ) <_ M ) ) )
157	155, 138, 139, 156	syl3anc 1264	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( j + 1 ) e. ( 0 ... M ) <-> ( 0 <_ ( j + 1 ) /\ ( j + 1 ) <_ M ) ) )
158	147, 154, 157	mpbir2and 930	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ( 0 ... M ) )
159	114, 158	ffvelrnd 5975	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
160		simpll 758	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ph )
161	134	adantlr 719	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
162	137, 138, 139, 83	syl3anc 1264	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
163	125, 161, 162	mpbir2and 930	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0..^ M ) )
164	160, 163, 103	syl2anc 665	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
165	142, 159, 164	ltled 9727	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
166	109, 113, 165	monoord 12186	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` M ) )
167	28	adantr 466	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` M ) = B )
168	166, 167	breqtrd 4384	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ B )
169	27, 33, 34, 107, 168	eliccd 37487	. . . 4 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( A [,] B ) )
170	169	ralrimiva 2773	. . 3 |- ( ph -> A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) )
171		fnfvrnss 6003	. . 3 |- ( ( Q Fn ( 0 ... M ) /\ A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) ) -> ran Q C_ ( A [,] B ) )
172	15, 170, 171	syl2anc 665	. 2 |- ( ph -> ran Q C_ ( A [,] B ) )
173		df-f 5541	. 2 |- ( Q : ( 0 ... M ) --> ( A [,] B ) <-> ( Q Fn ( 0 ... M ) /\ ran Q C_ ( A [,] B ) ) )
174	15, 172, 173	sylanbrc 668	1 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   A.wral 2708   {crab 2712   _Vcvv 3016   C_ wss 3372   class class class wbr 4359   |-> cmpt 4418   ran crn 4790   Fn wfn 5532   -->wf 5533   ` cfv 5537  (class class class)co 6242   ^m cmap 7420   CCcc 9481   RRcr 9482   0cc0 9483   1c1 9484   + caddc 9486   < clt 9619   <_ cle 9620   - cmin 9804   NNcn 10553   NN0cn0 10813   ZZcz 10881   ZZ>=cuz 11103   [,]cicc 11582   ...cfz 11728  ..^cfzo 11859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-er 7311  df-map 7422  df-en 7518  df-dom 7519  df-sdom 7520  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-n0 10814  df-z 10882  df-uz 11104  df-icc 11586  df-fz 11729  df-fzo 11860

This theorem is referenced by:  fourierdlem38  37885  fourierdlem50  37897  fourierdlem54  37901  fourierdlem63  37910  fourierdlem65  37912  fourierdlem69  37916  fourierdlem70  37917  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem79  37926  fourierdlem81  37928  fourierdlem84  37931  fourierdlem85  37932  fourierdlem88  37935  fourierdlem89  37936  fourierdlem90  37937  fourierdlem91  37938  fourierdlem92  37939  fourierdlem93  37940  fourierdlem100  37947  fourierdlem101  37948  fourierdlem103  37950  fourierdlem104  37951  fourierdlem107  37954  fourierdlem111  37958  fourierdlem112  37959  fourierdlem113  37960