Theorem fourierdlem25 31723

Description: If C is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem25.m	|- ( ph -> M e. NN )
fourierdlem25.qf	|- ( ph -> Q : ( 0 ... M ) --> RR )
fourierdlem25.cel	|- ( ph -> C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
fourierdlem25.cnel	|- ( ph -> -. C e. ran Q )
fourierdlem25.i	|- I = sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < )

Assertion

Ref	Expression
fourierdlem25	|- ( ph -> E. j e. ( 0..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )

Distinct variable groups:   C, k   C, j   j, I   k, I   k, M   j, M   Q, k   Q, j

Allowed substitution hints:   ph( j, k)

Proof of Theorem fourierdlem25

Dummy variables h m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem25.i	. . 3 |- I = sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < )
2		ssrab2 3590	. . . . 5 |- { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ( 0..^ M )
3	2	a1i 11	. . . 4 |- ( ph -> { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ( 0..^ M ) )
4		ltso 9675	. . . . . 6 |- < Or RR
5	4	a1i 11	. . . . 5 |- ( ph -> < Or RR )
6		fzofi 12062	. . . . . . 7 |- ( 0..^ M ) e. Fin
7		ssfi 7750	. . . . . . 7 |- ( ( ( 0..^ M ) e. Fin /\ { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ( 0..^ M ) ) -> { k e. ( 0..^ M ) | ( Q ` k ) < C } e. Fin )
8	6, 2, 7	mp2an 672	. . . . . 6 |- { k e. ( 0..^ M ) | ( Q ` k ) < C } e. Fin
9	8	a1i 11	. . . . 5 |- ( ph -> { k e. ( 0..^ M ) | ( Q ` k ) < C } e. Fin )
10		0z 10885	. . . . . . . . . . 11 |- 0 e. ZZ
11	10	a1i 11	. . . . . . . . . 10 |- ( ph -> 0 e. ZZ )
12		fourierdlem25.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
13	12	nnzd 10975	. . . . . . . . . 10 |- ( ph -> M e. ZZ )
14	12	nngt0d 10589	. . . . . . . . . 10 |- ( ph -> 0 < M )
15	11, 13, 14	3jca 1176	. . . . . . . . 9 |- ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
16		fzolb 11812	. . . . . . . . 9 |- ( 0 e. ( 0..^ M ) <-> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
17	15, 16	sylibr 212	. . . . . . . 8 |- ( ph -> 0 e. ( 0..^ M ) )
18		fourierdlem25.qf	. . . . . . . . . 10 |- ( ph -> Q : ( 0 ... M ) --> RR )
19		elfzofz 11821	. . . . . . . . . . 11 |- ( 0 e. ( 0..^ M ) -> 0 e. ( 0 ... M ) )
20	17, 19	syl 16	. . . . . . . . . 10 |- ( ph -> 0 e. ( 0 ... M ) )
21	18, 20	ffvelrnd 6032	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) e. RR )
22	12	nnnn0d 10862	. . . . . . . . . . . . . 14 |- ( ph -> M e. NN0 )
23		nn0uz 11126	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` 0 )
24	22, 23	syl6eleq 2565	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 0 ) )
25		eluzfz2 11704	. . . . . . . . . . . . 13 |- ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
26	24, 25	syl 16	. . . . . . . . . . . 12 |- ( ph -> M e. ( 0 ... M ) )
27	18, 26	ffvelrnd 6032	. . . . . . . . . . 11 |- ( ph -> ( Q ` M ) e. RR )
28	21, 27	iccssred 31394	. . . . . . . . . 10 |- ( ph -> ( ( Q ` 0 ) [,] ( Q ` M ) ) C_ RR )
29		fourierdlem25.cel	. . . . . . . . . 10 |- ( ph -> C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) )
30	28, 29	sseldd 3510	. . . . . . . . 9 |- ( ph -> C e. RR )
31	21	rexrd 9653	. . . . . . . . . 10 |- ( ph -> ( Q ` 0 ) e. RR* )
32	27	rexrd 9653	. . . . . . . . . 10 |- ( ph -> ( Q ` M ) e. RR* )
33		iccgelb 11591	. . . . . . . . . 10 |- ( ( ( Q ` 0 ) e. RR* /\ ( Q ` M ) e. RR* /\ C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> ( Q ` 0 ) <_ C )
34	31, 32, 29, 33	syl3anc 1228	. . . . . . . . 9 |- ( ph -> ( Q ` 0 ) <_ C )
35		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ C = ( Q ` 0 ) ) -> C = ( Q ` 0 ) )
36		ffn 5736	. . . . . . . . . . . . . . 15 |- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) )
37	18, 36	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> Q Fn ( 0 ... M ) )
38	37	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ C = ( Q ` 0 ) ) -> Q Fn ( 0 ... M ) )
39	20	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ C = ( Q ` 0 ) ) -> 0 e. ( 0 ... M ) )
40		fnfvelrn 6028	. . . . . . . . . . . . 13 |- ( ( Q Fn ( 0 ... M ) /\ 0 e. ( 0 ... M ) ) -> ( Q ` 0 ) e. ran Q )
41	38, 39, 40	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ C = ( Q ` 0 ) ) -> ( Q ` 0 ) e. ran Q )
42	35, 41	eqeltrd 2555	. . . . . . . . . . 11 |- ( ( ph /\ C = ( Q ` 0 ) ) -> C e. ran Q )
43		fourierdlem25.cnel	. . . . . . . . . . . 12 |- ( ph -> -. C e. ran Q )
44	43	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ C = ( Q ` 0 ) ) -> -. C e. ran Q )
45	42, 44	pm2.65da 576	. . . . . . . . . 10 |- ( ph -> -. C = ( Q ` 0 ) )
46	45	neqned 2670	. . . . . . . . 9 |- ( ph -> C =/= ( Q ` 0 ) )
47	21, 30, 34, 46	leneltd 31362	. . . . . . . 8 |- ( ph -> ( Q ` 0 ) < C )
48	17, 47	jca 532	. . . . . . 7 |- ( ph -> ( 0 e. ( 0..^ M ) /\ ( Q ` 0 ) < C ) )
49		fveq2 5871	. . . . . . . . 9 |- ( k = 0 -> ( Q ` k ) = ( Q ` 0 ) )
50	49	breq1d 4462	. . . . . . . 8 |- ( k = 0 -> ( ( Q ` k ) < C <-> ( Q ` 0 ) < C ) )
51	50	elrab 3266	. . . . . . 7 |- ( 0 e. { k e. ( 0..^ M ) | ( Q ` k ) < C } <-> ( 0 e. ( 0..^ M ) /\ ( Q ` 0 ) < C ) )
52	48, 51	sylibr 212	. . . . . 6 |- ( ph -> 0 e. { k e. ( 0..^ M ) | ( Q ` k ) < C } )
53		ne0i 3796	. . . . . 6 |- ( 0 e. { k e. ( 0..^ M ) | ( Q ` k ) < C } -> { k e. ( 0..^ M ) | ( Q ` k ) < C } =/= (/) )
54	52, 53	syl 16	. . . . 5 |- ( ph -> { k e. ( 0..^ M ) | ( Q ` k ) < C } =/= (/) )
55		fzossfz 11824	. . . . . . . 8 |- ( 0..^ M ) C_ ( 0 ... M )
56		fzssz 31334	. . . . . . . . 9 |- ( 0 ... M ) C_ ZZ
57		zssre 10881	. . . . . . . . 9 |- ZZ C_ RR
58	56, 57	sstri 3518	. . . . . . . 8 |- ( 0 ... M ) C_ RR
59	55, 58	sstri 3518	. . . . . . 7 |- ( 0..^ M ) C_ RR
60	2, 59	sstri 3518	. . . . . 6 |- { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ RR
61	60	a1i 11	. . . . 5 |- ( ph -> { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ RR )
62		fisupcl 7937	. . . . 5 |- ( ( < Or RR /\ ( { k e. ( 0..^ M ) | ( Q ` k ) < C } e. Fin /\ { k e. ( 0..^ M ) | ( Q ` k ) < C } =/= (/) /\ { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ RR ) ) -> sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) e. { k e. ( 0..^ M ) | ( Q ` k ) < C } )
63	5, 9, 54, 61, 62	syl13anc 1230	. . . 4 |- ( ph -> sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) e. { k e. ( 0..^ M ) | ( Q ` k ) < C } )
64	3, 63	sseldd 3510	. . 3 |- ( ph -> sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) e. ( 0..^ M ) )
65	1, 64	syl5eqel 2559	. 2 |- ( ph -> I e. ( 0..^ M ) )
66	55, 65	sseldi 3507	. . . . 5 |- ( ph -> I e. ( 0 ... M ) )
67	18, 66	ffvelrnd 6032	. . . 4 |- ( ph -> ( Q ` I ) e. RR )
68	67	rexrd 9653	. . 3 |- ( ph -> ( Q ` I ) e. RR* )
69		fzofzp1 11887	. . . . . 6 |- ( I e. ( 0..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
70	65, 69	syl 16	. . . . 5 |- ( ph -> ( I + 1 ) e. ( 0 ... M ) )
71	18, 70	ffvelrnd 6032	. . . 4 |- ( ph -> ( Q ` ( I + 1 ) ) e. RR )
72	71	rexrd 9653	. . 3 |- ( ph -> ( Q ` ( I + 1 ) ) e. RR* )
73	1, 63	syl5eqel 2559	. . . . 5 |- ( ph -> I e. { k e. ( 0..^ M ) | ( Q ` k ) < C } )
74		fveq2 5871	. . . . . . 7 |- ( k = I -> ( Q ` k ) = ( Q ` I ) )
75	74	breq1d 4462	. . . . . 6 |- ( k = I -> ( ( Q ` k ) < C <-> ( Q ` I ) < C ) )
76	75	elrab 3266	. . . . 5 |- ( I e. { k e. ( 0..^ M ) | ( Q ` k ) < C } <-> ( I e. ( 0..^ M ) /\ ( Q ` I ) < C ) )
77	73, 76	sylib 196	. . . 4 |- ( ph -> ( I e. ( 0..^ M ) /\ ( Q ` I ) < C ) )
78	77	simprd 463	. . 3 |- ( ph -> ( Q ` I ) < C )
79	55, 56	sstri 3518	. . . . . . . . . . . 12 |- ( 0..^ M ) C_ ZZ
80	2, 79	sstri 3518	. . . . . . . . . . 11 |- { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ZZ
81	80	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ZZ )
82	2	sseli 3505	. . . . . . . . . . . . . . 15 |- ( h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } -> h e. ( 0..^ M ) )
83	59	sseli 3505	. . . . . . . . . . . . . . . 16 |- ( h e. ( 0..^ M ) -> h e. RR )
84		elfzoel2 11806	. . . . . . . . . . . . . . . . 17 |- ( h e. ( 0..^ M ) -> M e. ZZ )
85	57	sseli 3505	. . . . . . . . . . . . . . . . 17 |- ( M e. ZZ -> M e. RR )
86	84, 85	syl 16	. . . . . . . . . . . . . . . 16 |- ( h e. ( 0..^ M ) -> M e. RR )
87		elfzolt2 11815	. . . . . . . . . . . . . . . 16 |- ( h e. ( 0..^ M ) -> h < M )
88	83, 86, 87	ltled 9742	. . . . . . . . . . . . . . 15 |- ( h e. ( 0..^ M ) -> h <_ M )
89	82, 88	syl 16	. . . . . . . . . . . . . 14 |- ( h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } -> h <_ M )
90	89	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } ) -> h <_ M )
91	90	ralrimiva 2881	. . . . . . . . . . . 12 |- ( ph -> A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ M )
92		breq2 4456	. . . . . . . . . . . . . 14 |- ( m = M -> ( h <_ m <-> h <_ M ) )
93	92	ralbidv 2906	. . . . . . . . . . . . 13 |- ( m = M -> ( A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ m <-> A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ M ) )
94	93	rspcev 3219	. . . . . . . . . . . 12 |- ( ( M e. ZZ /\ A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ M ) -> E. m e. ZZ A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ m )
95	13, 91, 94	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> E. m e. ZZ A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ m )
96	95	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> E. m e. ZZ A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ m )
97		elfzuz 11694	. . . . . . . . . . . . . . . 16 |- ( ( I + 1 ) e. ( 0 ... M ) -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
98	70, 97	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
99	98	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. ( ZZ>= ` 0 ) )
100	13	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M e. ZZ )
101	58, 70	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> ( I + 1 ) e. RR )
102	101	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. RR )
103	100, 85	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M e. RR )
104		elfzle2 11700	. . . . . . . . . . . . . . . . 17 |- ( ( I + 1 ) e. ( 0 ... M ) -> ( I + 1 ) <_ M )
105	70, 104	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( I + 1 ) <_ M )
106	105	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ M )
107		iccleub 11590	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( Q ` 0 ) e. RR* /\ ( Q ` M ) e. RR* /\ C e. ( ( Q ` 0 ) [,] ( Q ` M ) ) ) -> C <_ ( Q ` M ) )
108	31, 32, 29, 107	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> C <_ ( Q ` M ) )
109	108	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ M = ( I + 1 ) ) -> C <_ ( Q ` M ) )
110		fveq2 5871	. . . . . . . . . . . . . . . . . . . 20 |- ( M = ( I + 1 ) -> ( Q ` M ) = ( Q ` ( I + 1 ) ) )
111	110	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ M = ( I + 1 ) ) -> ( Q ` M ) = ( Q ` ( I + 1 ) ) )
112	109, 111	breqtrd 4476	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ M = ( I + 1 ) ) -> C <_ ( Q ` ( I + 1 ) ) )
113	112	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) /\ M = ( I + 1 ) ) -> C <_ ( Q ` ( I + 1 ) ) )
114		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( Q ` ( I + 1 ) ) < C )
115	71	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( Q ` ( I + 1 ) ) e. RR )
116	30	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> C e. RR )
117	115, 116	ltnled 9741	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( ( Q ` ( I + 1 ) ) < C <-> -. C <_ ( Q ` ( I + 1 ) ) ) )
118	114, 117	mpbid 210	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> -. C <_ ( Q ` ( I + 1 ) ) )
119	118	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) /\ M = ( I + 1 ) ) -> -. C <_ ( Q ` ( I + 1 ) ) )
120	113, 119	pm2.65da 576	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> -. M = ( I + 1 ) )
121	120	neqned 2670	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> M =/= ( I + 1 ) )
122	102, 103, 106, 121	leneltd 31362	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) < M )
123	99, 100, 122	3jca 1176	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( ( I + 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( I + 1 ) < M ) )
124		elfzo2 11810	. . . . . . . . . . . . 13 |- ( ( I + 1 ) e. ( 0..^ M ) <-> ( ( I + 1 ) e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ ( I + 1 ) < M ) )
125	123, 124	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. ( 0..^ M ) )
126	125, 114	jca 532	. . . . . . . . . . 11 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( ( I + 1 ) e. ( 0..^ M ) /\ ( Q ` ( I + 1 ) ) < C ) )
127		fveq2 5871	. . . . . . . . . . . . 13 |- ( k = ( I + 1 ) -> ( Q ` k ) = ( Q ` ( I + 1 ) ) )
128	127	breq1d 4462	. . . . . . . . . . . 12 |- ( k = ( I + 1 ) -> ( ( Q ` k ) < C <-> ( Q ` ( I + 1 ) ) < C ) )
129	128	elrab 3266	. . . . . . . . . . 11 |- ( ( I + 1 ) e. { k e. ( 0..^ M ) | ( Q ` k ) < C } <-> ( ( I + 1 ) e. ( 0..^ M ) /\ ( Q ` ( I + 1 ) ) < C ) )
130	126, 129	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) e. { k e. ( 0..^ M ) | ( Q ` k ) < C } )
131		suprzub 11183	. . . . . . . . . 10 |- ( ( { k e. ( 0..^ M ) | ( Q ` k ) < C } C_ ZZ /\ E. m e. ZZ A. h e. { k e. ( 0..^ M ) | ( Q ` k ) < C } h <_ m /\ ( I + 1 ) e. { k e. ( 0..^ M ) | ( Q ` k ) < C } ) -> ( I + 1 ) <_ sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) )
132	81, 96, 130, 131	syl3anc 1228	. . . . . . . . 9 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) )
133	1	eqcomi 2480	. . . . . . . . . 10 |- sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) = I
134	133	a1i 11	. . . . . . . . 9 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> sup ( { k e. ( 0..^ M ) | ( Q ` k ) < C } , RR , < ) = I )
135	132, 134	breqtrd 4476	. . . . . . . 8 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> ( I + 1 ) <_ I )
136	59, 65	sseldi 3507	. . . . . . . . . 10 |- ( ph -> I e. RR )
137		ltp1 10390	. . . . . . . . . . 11 |- ( I e. RR -> I < ( I + 1 ) )
138		id 22	. . . . . . . . . . . 12 |- ( I e. RR -> I e. RR )
139		peano2re 9762	. . . . . . . . . . . 12 |- ( I e. RR -> ( I + 1 ) e. RR )
140	138, 139	ltnled 9741	. . . . . . . . . . 11 |- ( I e. RR -> ( I < ( I + 1 ) <-> -. ( I + 1 ) <_ I ) )
141	137, 140	mpbid 210	. . . . . . . . . 10 |- ( I e. RR -> -. ( I + 1 ) <_ I )
142	136, 141	syl 16	. . . . . . . . 9 |- ( ph -> -. ( I + 1 ) <_ I )
143	142	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` ( I + 1 ) ) < C ) -> -. ( I + 1 ) <_ I )
144	135, 143	pm2.65da 576	. . . . . . 7 |- ( ph -> -. ( Q ` ( I + 1 ) ) < C )
145		eqcom 2476	. . . . . . . . . . 11 |- ( ( Q ` ( I + 1 ) ) = C <-> C = ( Q ` ( I + 1 ) ) )
146	145	biimpi 194	. . . . . . . . . 10 |- ( ( Q ` ( I + 1 ) ) = C -> C = ( Q ` ( I + 1 ) ) )
147	146	adantl 466	. . . . . . . . 9 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> C = ( Q ` ( I + 1 ) ) )
148	37	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> Q Fn ( 0 ... M ) )
149	70	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> ( I + 1 ) e. ( 0 ... M ) )
150		fnfvelrn 6028	. . . . . . . . . 10 |- ( ( Q Fn ( 0 ... M ) /\ ( I + 1 ) e. ( 0 ... M ) ) -> ( Q ` ( I + 1 ) ) e. ran Q )
151	148, 149, 150	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> ( Q ` ( I + 1 ) ) e. ran Q )
152	147, 151	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> C e. ran Q )
153	43	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( Q ` ( I + 1 ) ) = C ) -> -. C e. ran Q )
154	152, 153	pm2.65da 576	. . . . . . 7 |- ( ph -> -. ( Q ` ( I + 1 ) ) = C )
155	144, 154	jca 532	. . . . . 6 |- ( ph -> ( -. ( Q ` ( I + 1 ) ) < C /\ -. ( Q ` ( I + 1 ) ) = C ) )
156		pm4.56 495	. . . . . 6 |- ( ( -. ( Q ` ( I + 1 ) ) < C /\ -. ( Q ` ( I + 1 ) ) = C ) <-> -. ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) )
157	155, 156	sylib 196	. . . . 5 |- ( ph -> -. ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) )
158		leloe 9681	. . . . . 6 |- ( ( ( Q ` ( I + 1 ) ) e. RR /\ C e. RR ) -> ( ( Q ` ( I + 1 ) ) <_ C <-> ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) ) )
159	71, 30, 158	syl2anc 661	. . . . 5 |- ( ph -> ( ( Q ` ( I + 1 ) ) <_ C <-> ( ( Q ` ( I + 1 ) ) < C \/ ( Q ` ( I + 1 ) ) = C ) ) )
160	157, 159	mtbird 301	. . . 4 |- ( ph -> -. ( Q ` ( I + 1 ) ) <_ C )
161	30, 71	ltnled 9741	. . . 4 |- ( ph -> ( C < ( Q ` ( I + 1 ) ) <-> -. ( Q ` ( I + 1 ) ) <_ C ) )
162	160, 161	mpbird 232	. . 3 |- ( ph -> C < ( Q ` ( I + 1 ) ) )
163	68, 72, 30, 78, 162	eliood 31386	. 2 |- ( ph -> C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
164		fveq2 5871	. . . . 5 |- ( j = I -> ( Q ` j ) = ( Q ` I ) )
165		oveq1 6301	. . . . . 6 |- ( j = I -> ( j + 1 ) = ( I + 1 ) )
166	165	fveq2d 5875	. . . . 5 |- ( j = I -> ( Q ` ( j + 1 ) ) = ( Q ` ( I + 1 ) ) )
167	164, 166	oveq12d 6312	. . . 4 |- ( j = I -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) )
168	167	eleq2d 2537	. . 3 |- ( j = I -> ( C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) <-> C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) )
169	168	rspcev 3219	. 2 |- ( ( I e. ( 0..^ M ) /\ C e. ( ( Q ` I ) (,) ( Q ` ( I + 1 ) ) ) ) -> E. j e. ( 0..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
170	65, 163, 169	syl2anc 661	1 |- ( ph -> E. j e. ( 0..^ M ) C e. ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2817   E.wrex 2818   {crab 2821   C_ wss 3481   (/)c0 3790   class class class wbr 4452   Or wor 4804   ran crn 5005   Fn wfn 5588   -->wf 5589   ` cfv 5593  (class class class)co 6294   Fincfn 7526   supcsup 7910   RRcr 9501   0cc0 9502   1c1 9503   + caddc 9505   RR*cxr 9637   < clt 9638   <_ cle 9639   NNcn 10546   NN0cn0 10805   ZZcz 10874   ZZ>=cuz 11092   (,)cioo 11539   [,]cicc 11542   ...cfz 11682  ..^cfzo 11802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6586  ax-cnex 9558  ax-resscn 9559  ax-1cn 9560  ax-icn 9561  ax-addcl 9562  ax-addrcl 9563  ax-mulcl 9564  ax-mulrcl 9565  ax-mulcom 9566  ax-addass 9567  ax-mulass 9568  ax-distr 9569  ax-i2m1 9570  ax-1ne0 9571  ax-1rid 9572  ax-rnegex 9573  ax-rrecex 9574  ax-cnre 9575  ax-pre-lttri 9576  ax-pre-lttrn 9577  ax-pre-ltadd 9578  ax-pre-mulgt0 9579

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4251  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6255  df-ov 6297  df-oprab 6298  df-mpt2 6299  df-om 6695  df-1st 6794  df-2nd 6795  df-recs 7052  df-rdg 7086  df-1o 7140  df-er 7321  df-en 7527  df-dom 7528  df-sdom 7529  df-fin 7530  df-sup 7911  df-pnf 9640  df-mnf 9641  df-xr 9642  df-ltxr 9643  df-le 9644  df-sub 9817  df-neg 9818  df-nn 10547  df-n0 10806  df-z 10875  df-uz 11093  df-ioo 11543  df-icc 11546  df-fz 11683  df-fzo 11803

This theorem is referenced by:  fourierdlem41  31739  fourierdlem48  31746  fourierdlem49  31747  fourierdlem70  31768  fourierdlem71  31769  fourierdlem103  31801  fourierdlem104  31802