fourierdlem25

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)

	Ref	Expression
Hypotheses	fourierdlem25.m	$⊢ φ \to M \in ℕ$
	fourierdlem25.qf	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
	fourierdlem25.cel	$⊢ φ \to C \in [Q (0), Q (M)]$
	fourierdlem25.cnel	$⊢ φ \to \neg C \in ran Q$
	fourierdlem25.i	$⊢ I = sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <)$
Assertion	fourierdlem25	$⊢ φ \to \exists j \in (0 ..^M) C \in (Q (j), Q (j + 1))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem25.m	$⊢ φ \to M \in ℕ$
2		fourierdlem25.qf	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
3		fourierdlem25.cel	$⊢ φ \to C \in [Q (0), Q (M)]$
4		fourierdlem25.cnel	$⊢ φ \to \neg C \in ran Q$
5		fourierdlem25.i	$⊢ I = sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <)$
6		ssrab2	$⊢ \{k \in (0 ..^M) \| Q (k) < C\} \subseteq (0 ..^M)$
7		ltso	$⊢ < Or ℝ$
8	7	a1i	$⊢ φ \to < Or ℝ$
9		fzofi	$⊢ (0 ..^M) \in Fin$
10		ssfi	$⊢ ((0 ..^M) \in Fin \land \{k \in (0 ..^M) \| Q (k) < C\} \subseteq (0 ..^M)) \to \{k \in (0 ..^M) \| Q (k) < C\} \in Fin$
11	9 6 10	mp2an	$⊢ \{k \in (0 ..^M) \| Q (k) < C\} \in Fin$
12	11	a1i	$⊢ φ \to \{k \in (0 ..^M) \| Q (k) < C\} \in Fin$
13		0zd	$⊢ φ \to 0 \in ℤ$
14	1	nnzd	$⊢ φ \to M \in ℤ$
15	1	nngt0d	$⊢ φ \to 0 < M$
16		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
17	13 14 15 16	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
18		elfzofz	$⊢ 0 \in (0 ..^M) \to 0 \in (0 \dots M)$
19	17 18	syl	$⊢ φ \to 0 \in (0 \dots M)$
20	2 19	ffvelrnd	$⊢ φ \to Q (0) \in ℝ$
21	1	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
22		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
23	21 22	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
24		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
25	23 24	syl	$⊢ φ \to M \in (0 \dots M)$
26	2 25	ffvelrnd	$⊢ φ \to Q (M) \in ℝ$
27	20 26	iccssred	$⊢ φ \to [Q (0), Q (M)] \subseteq ℝ$
28	27 3	sseldd	$⊢ φ \to C \in ℝ$
29	20	rexrd	$⊢ φ \to Q (0) \in ℝ^{*}$
30	26	rexrd	$⊢ φ \to Q (M) \in ℝ^{*}$
31		iccgelb	$⊢ (Q (0) \in ℝ^{} \land Q (M) \in ℝ^{} \land C \in [Q (0), Q (M)]) \to Q (0) \leq C$
32	29 30 3 31	syl3anc	$⊢ φ \to Q (0) \leq C$
33		simpr	$⊢ (φ \land C = Q (0)) \to C = Q (0)$
34	2	ffnd	$⊢ φ \to Q Fn (0 \dots M)$
35	34	adantr	$⊢ (φ \land C = Q (0)) \to Q Fn (0 \dots M)$
36	19	adantr	$⊢ (φ \land C = Q (0)) \to 0 \in (0 \dots M)$
37		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land 0 \in (0 \dots M)) \to Q (0) \in ran Q$
38	35 36 37	syl2anc	$⊢ (φ \land C = Q (0)) \to Q (0) \in ran Q$
39	33 38	eqeltrd	$⊢ (φ \land C = Q (0)) \to C \in ran Q$
40	4 39	mtand	$⊢ φ \to \neg C = Q (0)$
41	40	neqned	$⊢ φ \to C \neq Q (0)$
42	20 28 32 41	leneltd	$⊢ φ \to Q (0) < C$
43		fveq2	$⊢ k = 0 \to Q (k) = Q (0)$
44	43	breq1d	$⊢ k = 0 \to (Q (k) < C \leftrightarrow Q (0) < C)$
45	44	elrab	$⊢ 0 \in \{k \in (0 ..^M) \| Q (k) < C\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) < C)$
46	17 42 45	sylanbrc	$⊢ φ \to 0 \in \{k \in (0 ..^M) \| Q (k) < C\}$
47	46	ne0d	$⊢ φ \to \{k \in (0 ..^M) \| Q (k) < C\} \neq \emptyset$
48		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
49		fzssz	$⊢ (0 \dots M) \subseteq ℤ$
50		zssre	$⊢ ℤ \subseteq ℝ$
51	49 50	sstri	$⊢ (0 \dots M) \subseteq ℝ$
52	48 51	sstri	$⊢ (0 ..^M) \subseteq ℝ$
53	6 52	sstri	$⊢ \{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℝ$
54	53	a1i	$⊢ φ \to \{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℝ$
55		fisupcl	$⊢ (< Or ℝ \land (\{k \in (0 ..^M) \| Q (k) < C\} \in Fin \land \{k \in (0 ..^M) \| Q (k) < C\} \neq \emptyset \land \{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℝ)) \to sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <) \in \{k \in (0 ..^M) \| Q (k) < C\}$
56	8 12 47 54 55	syl13anc	$⊢ φ \to sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <) \in \{k \in (0 ..^M) \| Q (k) < C\}$
57	6 56	sselid	$⊢ φ \to sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <) \in (0 ..^M)$
58	5 57	eqeltrid	$⊢ φ \to I \in (0 ..^M)$
59	48 58	sselid	$⊢ φ \to I \in (0 \dots M)$
60	2 59	ffvelrnd	$⊢ φ \to Q (I) \in ℝ$
61	60	rexrd	$⊢ φ \to Q (I) \in ℝ^{*}$
62		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
63	58 62	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
64	2 63	ffvelrnd	$⊢ φ \to Q (I + 1) \in ℝ$
65	64	rexrd	$⊢ φ \to Q (I + 1) \in ℝ^{*}$
66	5 56	eqeltrid	$⊢ φ \to I \in \{k \in (0 ..^M) \| Q (k) < C\}$
67		fveq2	$⊢ k = I \to Q (k) = Q (I)$
68	67	breq1d	$⊢ k = I \to (Q (k) < C \leftrightarrow Q (I) < C)$
69	68	elrab	$⊢ I \in \{k \in (0 ..^M) \| Q (k) < C\} \leftrightarrow (I \in (0 ..^M) \land Q (I) < C)$
70	66 69	sylib	$⊢ φ \to (I \in (0 ..^M) \land Q (I) < C)$
71	70	simprd	$⊢ φ \to Q (I) < C$
72	52 58	sselid	$⊢ φ \to I \in ℝ$
73		ltp1	$⊢ I \in ℝ \to I < I + 1$
74		id	$⊢ I \in ℝ \to I \in ℝ$
75		peano2re	$⊢ I \in ℝ \to I + 1 \in ℝ$
76	74 75	ltnled	$⊢ I \in ℝ \to (I < I + 1 \leftrightarrow \neg I + 1 \leq I)$
77	73 76	mpbid	$⊢ I \in ℝ \to \neg I + 1 \leq I$
78	72 77	syl	$⊢ φ \to \neg I + 1 \leq I$
79	48 49	sstri	$⊢ (0 ..^M) \subseteq ℤ$
80	6 79	sstri	$⊢ \{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℤ$
81	80	a1i	$⊢ (φ \land Q (I + 1) < C) \to \{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℤ$
82		elrabi	$⊢ h \in \{k \in (0 ..^M) \| Q (k) < C\} \to h \in (0 ..^M)$
83		elfzo0le	$⊢ h \in (0 ..^M) \to h \leq M$
84	82 83	syl	$⊢ h \in \{k \in (0 ..^M) \| Q (k) < C\} \to h \leq M$
85	84	adantl	$⊢ (φ \land h \in \{k \in (0 ..^M) \| Q (k) < C\}) \to h \leq M$
86	85	ralrimiva	$⊢ φ \to \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq M$
87		breq2	$⊢ m = M \to (h \leq m \leftrightarrow h \leq M)$
88	87	ralbidv	$⊢ m = M \to (\forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq m \leftrightarrow \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq M)$
89	88	rspcev	$⊢ (M \in ℤ \land \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq M) \to \exists m \in ℤ \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq m$
90	14 86 89	syl2anc	$⊢ φ \to \exists m \in ℤ \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq m$
91	90	adantr	$⊢ (φ \land Q (I + 1) < C) \to \exists m \in ℤ \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq m$
92		elfzuz	$⊢ I + 1 \in (0 \dots M) \to I + 1 \in ℤ_{\geq 0}$
93	63 92	syl	$⊢ φ \to I + 1 \in ℤ_{\geq 0}$
94	93	adantr	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \in ℤ_{\geq 0}$
95	14	adantr	$⊢ (φ \land Q (I + 1) < C) \to M \in ℤ$
96	51 63	sselid	$⊢ φ \to I + 1 \in ℝ$
97	96	adantr	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \in ℝ$
98	95	zred	$⊢ (φ \land Q (I + 1) < C) \to M \in ℝ$
99		elfzle2	$⊢ I + 1 \in (0 \dots M) \to I + 1 \leq M$
100	63 99	syl	$⊢ φ \to I + 1 \leq M$
101	100	adantr	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \leq M$
102		simpr	$⊢ (φ \land Q (I + 1) < C) \to Q (I + 1) < C$
103	64	adantr	$⊢ (φ \land Q (I + 1) < C) \to Q (I + 1) \in ℝ$
104	28	adantr	$⊢ (φ \land Q (I + 1) < C) \to C \in ℝ$
105	103 104	ltnled	$⊢ (φ \land Q (I + 1) < C) \to (Q (I + 1) < C \leftrightarrow \neg C \leq Q (I + 1))$
106	102 105	mpbid	$⊢ (φ \land Q (I + 1) < C) \to \neg C \leq Q (I + 1)$
107		iccleub	$⊢ (Q (0) \in ℝ^{} \land Q (M) \in ℝ^{} \land C \in [Q (0), Q (M)]) \to C \leq Q (M)$
108	29 30 3 107	syl3anc	$⊢ φ \to C \leq Q (M)$
109	108	adantr	$⊢ (φ \land M = I + 1) \to C \leq Q (M)$
110		fveq2	$⊢ M = I + 1 \to Q (M) = Q (I + 1)$
111	110	adantl	$⊢ (φ \land M = I + 1) \to Q (M) = Q (I + 1)$
112	109 111	breqtrd	$⊢ (φ \land M = I + 1) \to C \leq Q (I + 1)$
113	112	adantlr	$⊢ ((φ \land Q (I + 1) < C) \land M = I + 1) \to C \leq Q (I + 1)$
114	106 113	mtand	$⊢ (φ \land Q (I + 1) < C) \to \neg M = I + 1$
115	114	neqned	$⊢ (φ \land Q (I + 1) < C) \to M \neq I + 1$
116	97 98 101 115	leneltd	$⊢ (φ \land Q (I + 1) < C) \to I + 1 < M$
117		elfzo2	$⊢ I + 1 \in (0 ..^M) \leftrightarrow (I + 1 \in ℤ_{\geq 0} \land M \in ℤ \land I + 1 < M)$
118	94 95 116 117	syl3anbrc	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \in (0 ..^M)$
119		fveq2	$⊢ k = I + 1 \to Q (k) = Q (I + 1)$
120	119	breq1d	$⊢ k = I + 1 \to (Q (k) < C \leftrightarrow Q (I + 1) < C)$
121	120	elrab	$⊢ I + 1 \in \{k \in (0 ..^M) \| Q (k) < C\} \leftrightarrow (I + 1 \in (0 ..^M) \land Q (I + 1) < C)$
122	118 102 121	sylanbrc	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \in \{k \in (0 ..^M) \| Q (k) < C\}$
123		suprzub	$⊢ (\{k \in (0 ..^M) \| Q (k) < C\} \subseteq ℤ \land \exists m \in ℤ \forall h \in \{k \in (0 ..^M) \| Q (k) < C\} h \leq m \land I + 1 \in \{k \in (0 ..^M) \| Q (k) < C\}) \to I + 1 \leq sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <)$
124	81 91 122 123	syl3anc	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \leq sup (\{k \in (0 ..^M) \| Q (k) < C\} ℝ <)$
125	124 5	breqtrrdi	$⊢ (φ \land Q (I + 1) < C) \to I + 1 \leq I$
126	78 125	mtand	$⊢ φ \to \neg Q (I + 1) < C$
127		eqcom	$⊢ Q (I + 1) = C \leftrightarrow C = Q (I + 1)$
128	127	biimpi	$⊢ Q (I + 1) = C \to C = Q (I + 1)$
129	128	adantl	$⊢ (φ \land Q (I + 1) = C) \to C = Q (I + 1)$
130	34	adantr	$⊢ (φ \land Q (I + 1) = C) \to Q Fn (0 \dots M)$
131	63	adantr	$⊢ (φ \land Q (I + 1) = C) \to I + 1 \in (0 \dots M)$
132		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land I + 1 \in (0 \dots M)) \to Q (I + 1) \in ran Q$
133	130 131 132	syl2anc	$⊢ (φ \land Q (I + 1) = C) \to Q (I + 1) \in ran Q$
134	129 133	eqeltrd	$⊢ (φ \land Q (I + 1) = C) \to C \in ran Q$
135	4 134	mtand	$⊢ φ \to \neg Q (I + 1) = C$
136	126 135	jca	$⊢ φ \to (\neg Q (I + 1) < C \land \neg Q (I + 1) = C)$
137		pm4.56	$⊢ (\neg Q (I + 1) < C \land \neg Q (I + 1) = C) \leftrightarrow \neg (Q (I + 1) < C \lor Q (I + 1) = C)$
138	136 137	sylib	$⊢ φ \to \neg (Q (I + 1) < C \lor Q (I + 1) = C)$
139	64 28	leloed	$⊢ φ \to (Q (I + 1) \leq C \leftrightarrow (Q (I + 1) < C \lor Q (I + 1) = C))$
140	138 139	mtbird	$⊢ φ \to \neg Q (I + 1) \leq C$
141	28 64	ltnled	$⊢ φ \to (C < Q (I + 1) \leftrightarrow \neg Q (I + 1) \leq C)$
142	140 141	mpbird	$⊢ φ \to C < Q (I + 1)$
143	61 65 28 71 142	eliood	$⊢ φ \to C \in (Q (I), Q (I + 1))$
144		fveq2	$⊢ j = I \to Q (j) = Q (I)$
145		oveq1	$⊢ j = I \to j + 1 = I + 1$
146	145	fveq2d	$⊢ j = I \to Q (j + 1) = Q (I + 1)$
147	144 146	oveq12d	$⊢ j = I \to (Q (j), Q (j + 1)) = (Q (I), Q (I + 1))$
148	147	eleq2d	$⊢ j = I \to (C \in (Q (j), Q (j + 1)) \leftrightarrow C \in (Q (I), Q (I + 1)))$
149	148	rspcev	$⊢ (I \in (0 ..^M) \land C \in (Q (I), Q (I + 1))) \to \exists j \in (0 ..^M) C \in (Q (j), Q (j + 1))$
150	58 143 149	syl2anc	$⊢ φ \to \exists j \in (0 ..^M) C \in (Q (j), Q (j + 1))$

Metamath Proof Explorer

Theorem fourierdlem25

Proof