Theorem fourierdlem15 37254

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 37241	. . . . . . 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 210	. . . . 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 457	. . . 4 |- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
8		reex 9533	. . . . . 6 |- RR e. _V
9	8	a1i 11	. . . . 5 |- ( ph -> RR e. _V )
10		ovex 6262	. . . . . 6 |- ( 0 ... M ) e. _V
11	10	a1i 11	. . . . 5 |- ( ph -> ( 0 ... M ) e. _V )
12	9, 11	elmapd 7391	. . . 4 |- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) <-> Q : ( 0 ... M ) --> RR ) )
13	7, 12	mpbid 210	. . 3 |- ( ph -> Q : ( 0 ... M ) --> RR )
14		ffn 5670	. . 3 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
15	13, 14	syl 17	. 2 |- ( ph -> Q Fn ( 0 ... M ) )
16	6	simprd 461	. . . . . . . . 9 |- ( ph -> ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
17	16	simpld 457	. . . . . . . 8 |- ( ph -> ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) )
18	17	simpld 457	. . . . . . 7 |- ( ph -> ( Q ` 0 ) = A )
19		nnnn0 10763	. . . . . . . . . . 11 |- ( M e. NN -> M e. NN0 )
20		nn0uz 11079	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
21	19, 20	syl6eleq 2500	. . . . . . . . . 10 |- ( M e. NN -> M e. ( ZZ>= ` 0 ) )
22	2, 21	syl 17	. . . . . . . . 9 |- ( ph -> M e. ( ZZ>= ` 0 ) )
23		eluzfz1 11664	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
24	22, 23	syl 17	. . . . . . . 8 |- ( ph -> 0 e. ( 0 ... M ) )
25	13, 24	ffvelrnd 5966	. . . . . . 7 |- ( ph -> ( Q ` 0 ) e. RR )
26	18, 25	eqeltrrd 2491	. . . . . 6 |- ( ph -> A e. RR )
27	26	adantr 463	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A e. RR )
28	17	simprd 461	. . . . . . 7 |- ( ph -> ( Q ` M ) = B )
29		eluzfz2 11665	. . . . . . . . 9 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
30	22, 29	syl 17	. . . . . . . 8 |- ( ph -> M e. ( 0 ... M ) )
31	13, 30	ffvelrnd 5966	. . . . . . 7 |- ( ph -> ( Q ` M ) e. RR )
32	28, 31	eqeltrrd 2491	. . . . . 6 |- ( ph -> B e. RR )
33	32	adantr 463	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> B e. RR )
34	13	ffvelrnda 5965	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. RR )
35	18	eqcomd 2410	. . . . . . 7 |- ( ph -> A = ( Q ` 0 ) )
36	35	adantr 463	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A = ( Q ` 0 ) )
37		elfzuz 11655	. . . . . . . 8 |- ( i e. ( 0 ... M ) -> i e. ( ZZ>= ` 0 ) )
38	37	adantl 464	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> i e. ( ZZ>= ` 0 ) )
39	13	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> Q : ( 0 ... M ) --> RR )
40		elfzle1 11660	. . . . . . . . . . 11 |- ( j e. ( 0 ... i ) -> 0 <_ j )
41	40	adantl 464	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 <_ j )
42		elfzelz 11659	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... i ) -> j e. ZZ )
43	42	zred 10928	. . . . . . . . . . . 12 |- ( j e. ( 0 ... i ) -> j e. RR )
44	43	adantl 464	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. RR )
45		elfzelz 11659	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> i e. ZZ )
46	45	zred 10928	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> i e. RR )
47	46	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i e. RR )
48		elfzel2 11657	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> M e. ZZ )
49	48	zred 10928	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> M e. RR )
50	49	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. RR )
51		elfzle2 11661	. . . . . . . . . . . 12 |- ( j e. ( 0 ... i ) -> j <_ i )
52	51	adantl 464	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ i )
53		elfzle2 11661	. . . . . . . . . . . 12 |- ( i e. ( 0 ... M ) -> i <_ M )
54	53	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> i <_ M )
55	44, 47, 50, 52, 54	letrd 9693	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j <_ M )
56	42	adantl 464	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ZZ )
57		0zd 10837	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> 0 e. ZZ )
58	48	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> M e. ZZ )
59		elfz 11649	. . . . . . . . . . 11 |- ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
60	56, 57, 58, 59	syl3anc 1230	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
61	41, 55, 60	mpbir2and 923	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
62	61	adantll 712	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> j e. ( 0 ... M ) )
63	39, 62	ffvelrnd 5966	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... i ) ) -> ( Q ` j ) e. RR )
64		simpll 752	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ph )
65		elfzle1 11660	. . . . . . . . . . 11 |- ( j e. ( 0 ... ( i - 1 ) ) -> 0 <_ j )
66	65	adantl 464	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 <_ j )
67		elfzelz 11659	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... ( i - 1 ) ) -> j e. ZZ )
68	67	zred 10928	. . . . . . . . . . . 12 |- ( j e. ( 0 ... ( i - 1 ) ) -> j e. RR )
69	68	adantl 464	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. RR )
70	46	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i e. RR )
71	49	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. RR )
72		peano2rem 9842	. . . . . . . . . . . . 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 11661	. . . . . . . . . . . . 13 |- ( j e. ( 0 ... ( i - 1 ) ) -> j <_ ( i - 1 ) )
75	74	adantl 464	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j <_ ( i - 1 ) )
76	70	ltm1d 10438	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( i - 1 ) < i )
77	69, 73, 70, 75, 76	lelttrd 9694	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < i )
78	53	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> i <_ M )
79	69, 70, 71, 77, 78	ltletrd 9696	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j < M )
80	67	adantl 464	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ZZ )
81		0zd 10837	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> 0 e. ZZ )
82	48	adantr 463	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> M e. ZZ )
83		elfzo 11774	. . . . . . . . . . 11 |- ( ( j e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
84	80, 81, 82, 83	syl3anc 1230	. . . . . . . . . 10 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
85	66, 79, 84	mpbir2and 923	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0..^ M ) )
86	85	adantll 712	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> j e. ( 0..^ M ) )
87	13	adantr 463	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> Q : ( 0 ... M ) --> RR )
88		elfzofz 11787	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) -> j e. ( 0 ... M ) )
89	88	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> j e. ( 0 ... M ) )
90	87, 89	ffvelrnd 5966	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) e. RR )
91		fzofzp1 11859	. . . . . . . . . . 11 |- ( j e. ( 0..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
92	91	adantl 464	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
93	87, 92	ffvelrnd 5966	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` ( j + 1 ) ) e. RR )
94		eleq1 2474	. . . . . . . . . . . 12 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
95	94	anbi2d 702	. . . . . . . . . . 11 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
96		fveq2 5805	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
97		oveq1 6241	. . . . . . . . . . . . 13 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
98	97	fveq2d 5809	. . . . . . . . . . . 12 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
99	96, 98	breq12d 4407	. . . . . . . . . . 11 |- ( i = j -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` j ) < ( Q ` ( j + 1 ) ) ) )
100	95, 99	imbi12d 318	. . . . . . . . . 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 461	. . . . . . . . . . 11 |- ( ph -> A. i e. ( 0..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
102	101	r19.21bi 2772	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
103	100, 102	chvarv 2041	. . . . . . . . 9 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
104	90, 93, 103	ltled 9685	. . . . . . . 8 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
105	64, 86, 104	syl2anc 659	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( 0 ... ( i - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
106	38, 63, 105	monoord 12091	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` 0 ) <_ ( Q ` i ) )
107	36, 106	eqbrtrd 4414	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> A <_ ( Q ` i ) )
108		elfzuz3 11656	. . . . . . . 8 |- ( i e. ( 0 ... M ) -> M e. ( ZZ>= ` i ) )
109	108	adantl 464	. . . . . . 7 |- ( ( ph /\ i e. ( 0 ... M ) ) -> M e. ( ZZ>= ` i ) )
110	13	ad2antrr 724	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> Q : ( 0 ... M ) --> RR )
111		fz0fzelfz0 11752	. . . . . . . . 9 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
112	111	adantll 712	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> j e. ( 0 ... M ) )
113	110, 112	ffvelrnd 5966	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... M ) ) -> ( Q ` j ) e. RR )
114	13	ad2antrr 724	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> Q : ( 0 ... M ) --> RR )
115		0red 9547	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. RR )
116	46	adantr 463	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i e. RR )
117		elfzelz 11659	. . . . . . . . . . . . . 14 |- ( j e. ( i ... ( M - 1 ) ) -> j e. ZZ )
118	117	zred 10928	. . . . . . . . . . . . 13 |- ( j e. ( i ... ( M - 1 ) ) -> j e. RR )
119	118	adantl 464	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
120		elfzle1 11660	. . . . . . . . . . . . 13 |- ( i e. ( 0 ... M ) -> 0 <_ i )
121	120	adantr 463	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ i )
122		elfzle1 11660	. . . . . . . . . . . . 13 |- ( j e. ( i ... ( M - 1 ) ) -> i <_ j )
123	122	adantl 464	. . . . . . . . . . . 12 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> i <_ j )
124	115, 116, 119, 121, 123	letrd 9693	. . . . . . . . . . 11 |- ( ( i e. ( 0 ... M ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
125	124	adantll 712	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ j )
126	118	adantl 464	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
127	2	nnred 10511	. . . . . . . . . . . . 13 |- ( ph -> M e. RR )
128	127	adantr 463	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. RR )
129		1red 9561	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
130	128, 129	resubcld 9948	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) e. RR )
131		elfzle2 11661	. . . . . . . . . . . . . 14 |- ( j e. ( i ... ( M - 1 ) ) -> j <_ ( M - 1 ) )
132	131	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ ( M - 1 ) )
133	128	ltm1d 10438	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( M - 1 ) < M )
134	126, 130, 128, 132, 133	lelttrd 9694	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
135	126, 128, 134	ltled 9685	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
136	135	adantlr 713	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j <_ M )
137	117	adantl 464	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ZZ )
138		0zd 10837	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 e. ZZ )
139	48	ad2antlr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> M e. ZZ )
140	137, 138, 139, 59	syl3anc 1230	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0 ... M ) <-> ( 0 <_ j /\ j <_ M ) ) )
141	125, 136, 140	mpbir2and 923	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0 ... M ) )
142	114, 141	ffvelrnd 5966	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) e. RR )
143	118	adantl 464	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. RR )
144		1red 9561	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. RR )
145		0le1 10036	. . . . . . . . . . . 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 10088	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> 0 <_ ( j + 1 ) )
148	126, 130, 129, 132	leadd1dd 10126	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ ( ( M - 1 ) + 1 ) )
149	2	nncnd 10512	. . . . . . . . . . . . . 14 |- ( ph -> M e. CC )
150	149	adantr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> M e. CC )
151		1cnd 9562	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> 1 e. CC )
152	150, 151	npcand 9891	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( ( M - 1 ) + 1 ) = M )
153	148, 152	breqtrd 4418	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
154	153	adantlr 713	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) <_ M )
155	137	peano2zd 10931	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ZZ )
156		elfz 11649	. . . . . . . . . . 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 1230	. . . . . . . . . 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 923	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j + 1 ) e. ( 0 ... M ) )
159	114, 158	ffvelrnd 5966	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` ( j + 1 ) ) e. RR )
160		simpll 752	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ph )
161	134	adantlr 713	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j < M )
162	137, 138, 139, 83	syl3anc 1230	. . . . . . . . . 10 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( j e. ( 0..^ M ) <-> ( 0 <_ j /\ j < M ) ) )
163	125, 161, 162	mpbir2and 923	. . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> j e. ( 0..^ M ) )
164	160, 163, 103	syl2anc 659	. . . . . . . 8 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) < ( Q ` ( j + 1 ) ) )
165	142, 159, 164	ltled 9685	. . . . . . 7 |- ( ( ( ph /\ i e. ( 0 ... M ) ) /\ j e. ( i ... ( M - 1 ) ) ) -> ( Q ` j ) <_ ( Q ` ( j + 1 ) ) )
166	109, 113, 165	monoord 12091	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ ( Q ` M ) )
167	28	adantr 463	. . . . . 6 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` M ) = B )
168	166, 167	breqtrd 4418	. . . . 5 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) <_ B )
169	27, 33, 34, 107, 168	eliccd 36888	. . . 4 |- ( ( ph /\ i e. ( 0 ... M ) ) -> ( Q ` i ) e. ( A [,] B ) )
170	169	ralrimiva 2817	. . 3 |- ( ph -> A. i e. ( 0 ... M ) ( Q ` i ) e. ( A [,] B ) )
171		fnfvrnss 5994	. . 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 659	. 2 |- ( ph -> ran Q C_ ( A [,] B ) )
173		df-f 5529	. 2 |- ( Q : ( 0 ... M ) --> ( A [,] B ) <-> ( Q Fn ( 0 ... M ) /\ ran Q C_ ( A [,] B ) ) )
174	15, 172, 173	sylanbrc 662	1 |- ( ph -> Q : ( 0 ... M ) --> ( A [,] B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   A.wral 2753   {crab 2757   _Vcvv 3058   C_ wss 3413   class class class wbr 4394   |-> cmpt 4452   ran crn 4943   Fn wfn 5520   -->wf 5521   ` cfv 5525  (class class class)co 6234   ^m cmap 7377   CCcc 9440   RRcr 9441   0cc0 9442   1c1 9443   + caddc 9445   < clt 9578   <_ cle 9579   - cmin 9761   NNcn 10496   NN0cn0 10756   ZZcz 10825   ZZ>=cuz 11045   [,]cicc 11503   ...cfz 11643  ..^cfzo 11767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6530  ax-cnex 9498  ax-resscn 9499  ax-1cn 9500  ax-icn 9501  ax-addcl 9502  ax-addrcl 9503  ax-mulcl 9504  ax-mulrcl 9505  ax-mulcom 9506  ax-addass 9507  ax-mulass 9508  ax-distr 9509  ax-i2m1 9510  ax-1ne0 9511  ax-1rid 9512  ax-rnegex 9513  ax-rrecex 9514  ax-cnre 9515  ax-pre-lttri 9516  ax-pre-lttrn 9517  ax-pre-ltadd 9518  ax-pre-mulgt0 9519

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 4824  df-on 4825  df-lim 4826  df-suc 4827  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-riota 6196  df-ov 6237  df-oprab 6238  df-mpt2 6239  df-om 6639  df-1st 6738  df-2nd 6739  df-recs 6999  df-rdg 7033  df-er 7268  df-map 7379  df-en 7475  df-dom 7476  df-sdom 7477  df-pnf 9580  df-mnf 9581  df-xr 9582  df-ltxr 9583  df-le 9584  df-sub 9763  df-neg 9764  df-nn 10497  df-n0 10757  df-z 10826  df-uz 11046  df-icc 11507  df-fz 11644  df-fzo 11768

This theorem is referenced by:  fourierdlem38  37277  fourierdlem50  37289  fourierdlem54  37293  fourierdlem63  37302  fourierdlem65  37304  fourierdlem69  37308  fourierdlem70  37309  fourierdlem74  37313  fourierdlem75  37314  fourierdlem76  37315  fourierdlem79  37318  fourierdlem81  37320  fourierdlem84  37323  fourierdlem85  37324  fourierdlem88  37327  fourierdlem89  37328  fourierdlem90  37329  fourierdlem91  37330  fourierdlem92  37331  fourierdlem93  37332  fourierdlem100  37339  fourierdlem101  37340  fourierdlem103  37342  fourierdlem104  37343  fourierdlem107  37346  fourierdlem111  37350  fourierdlem112  37351  fourierdlem113  37352