fourierdlem20

Description: Every interval in the partition S is included in an interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem20.m	$⊢ φ \to M \in ℕ$
	fourierdlem20.a	$⊢ φ \to A \in ℝ$
	fourierdlem20.b	$⊢ φ \to B \in ℝ$
	fourierdlem20.aleb	$⊢ φ \to A \leq B$
	fourierdlem20.q	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
	fourierdlem20.q0	$⊢ φ \to Q (0) \leq A$
	fourierdlem20.qm	$⊢ φ \to B \leq Q (M)$
	fourierdlem20.j	$⊢ φ \to J \in (0 ..^N)$
	fourierdlem20.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
	fourierdlem20.s	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), T)$
	fourierdlem20.i	$⊢ I = sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <)$
Assertion	fourierdlem20	$⊢ φ \to \exists i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem20.m	$⊢ φ \to M \in ℕ$
2		fourierdlem20.a	$⊢ φ \to A \in ℝ$
3		fourierdlem20.b	$⊢ φ \to B \in ℝ$
4		fourierdlem20.aleb	$⊢ φ \to A \leq B$
5		fourierdlem20.q	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
6		fourierdlem20.q0	$⊢ φ \to Q (0) \leq A$
7		fourierdlem20.qm	$⊢ φ \to B \leq Q (M)$
8		fourierdlem20.j	$⊢ φ \to J \in (0 ..^N)$
9		fourierdlem20.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
10		fourierdlem20.s	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), T)$
11		fourierdlem20.i	$⊢ I = sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <)$
12		ssrab2	$⊢ \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq (0 ..^M)$
13		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
14		fzssz	$⊢ (0 \dots M) \subseteq ℤ$
15	13 14	sstri	$⊢ (0 ..^M) \subseteq ℤ$
16	12 15	sstri	$⊢ \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℤ$
17	16	a1i	$⊢ φ \to \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℤ$
18		0z	$⊢ 0 \in ℤ$
19		0le0	$⊢ 0 \leq 0$
20		eluz2	$⊢ 0 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land 0 \in ℤ \land 0 \leq 0)$
21	18 18 19 20	mpbir3an	$⊢ 0 \in ℤ_{\geq 0}$
22	21	a1i	$⊢ φ \to 0 \in ℤ_{\geq 0}$
23	1	nnzd	$⊢ φ \to M \in ℤ$
24	1	nngt0d	$⊢ φ \to 0 < M$
25		elfzo2	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ_{\geq 0} \land M \in ℤ \land 0 < M)$
26	22 23 24 25	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
27	13 26	sselid	$⊢ φ \to 0 \in (0 \dots M)$
28	5 27	ffvelcdmd	$⊢ φ \to Q (0) \in ℝ$
29	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
30	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
31		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
32	29 30 4 31	syl3anc	$⊢ φ \to A \in [A, B]$
33		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
34	29 30 4 33	syl3anc	$⊢ φ \to B \in [A, B]$
35	32 34	jca	$⊢ φ \to (A \in [A, B] \land B \in [A, B])$
36		prssg	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \in [A, B] \land B \in [A, B]) \leftrightarrow \{A, B\} \subseteq [A, B])$
37	29 30 36	syl2anc	$⊢ φ \to ((A \in [A, B] \land B \in [A, B]) \leftrightarrow \{A, B\} \subseteq [A, B])$
38	35 37	mpbid	$⊢ φ \to \{A, B\} \subseteq [A, B]$
39		inss2	$⊢ ran Q \cap (A, B) \subseteq (A, B)$
40		ioossicc	$⊢ (A, B) \subseteq [A, B]$
41	39 40	sstri	$⊢ ran Q \cap (A, B) \subseteq [A, B]$
42	41	a1i	$⊢ φ \to ran Q \cap (A, B) \subseteq [A, B]$
43	38 42	unssd	$⊢ φ \to \{A, B\} \cup (ran Q \cap (A, B)) \subseteq [A, B]$
44	9 43	eqsstrid	$⊢ φ \to T \subseteq [A, B]$
45	2 3	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
46	44 45	sstrd	$⊢ φ \to T \subseteq ℝ$
47		isof1o	$⊢ S {Isom}_{<, <} ((0 \dots N), T) \to S : (0 \dots N) \underset{1-1 onto}{⟶} T$
48		f1of	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} T \to S : (0 \dots N) ⟶ T$
49	10 47 48	3syl	$⊢ φ \to S : (0 \dots N) ⟶ T$
50		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
51	8 50	syl	$⊢ φ \to J \in (0 \dots N)$
52	49 51	ffvelcdmd	$⊢ φ \to S (J) \in T$
53	46 52	sseldd	$⊢ φ \to S (J) \in ℝ$
54	44 52	sseldd	$⊢ φ \to S (J) \in [A, B]$
55		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land S (J) \in [A, B]) \to A \leq S (J)$
56	29 30 54 55	syl3anc	$⊢ φ \to A \leq S (J)$
57	28 2 53 6 56	letrd	$⊢ φ \to Q (0) \leq S (J)$
58		fveq2	$⊢ k = 0 \to Q (k) = Q (0)$
59	58	breq1d	$⊢ k = 0 \to (Q (k) \leq S (J) \leftrightarrow Q (0) \leq S (J))$
60	59	elrab	$⊢ 0 \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) \leq S (J))$
61	26 57 60	sylanbrc	$⊢ φ \to 0 \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
62	61	ne0d	$⊢ φ \to \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \neq \emptyset$
63	1	nnred	$⊢ φ \to M \in ℝ$
64	12	sseli	$⊢ j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \to j \in (0 ..^M)$
65		elfzo0le	$⊢ j \in (0 ..^M) \to j \leq M$
66	64 65	syl	$⊢ j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \to j \leq M$
67	66	adantl	$⊢ (φ \land j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}) \to j \leq M$
68	67	ralrimiva	$⊢ φ \to \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq M$
69		breq2	$⊢ x = M \to (j \leq x \leftrightarrow j \leq M)$
70	69	ralbidv	$⊢ x = M \to (\forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x \leftrightarrow \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq M)$
71	70	rspcev	$⊢ (M \in ℝ \land \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq M) \to \exists x \in ℝ \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x$
72	63 68 71	syl2anc	$⊢ φ \to \exists x \in ℝ \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x$
73		suprzcl	$⊢ (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℤ \land \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \neq \emptyset \land \exists x \in ℝ \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x) \to sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <) \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
74	17 62 72 73	syl3anc	$⊢ φ \to sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <) \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
75	12 74	sselid	$⊢ φ \to sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <) \in (0 ..^M)$
76	11 75	eqeltrid	$⊢ φ \to I \in (0 ..^M)$
77	13 76	sselid	$⊢ φ \to I \in (0 \dots M)$
78	5 77	ffvelcdmd	$⊢ φ \to Q (I) \in ℝ$
79	78	rexrd	$⊢ φ \to Q (I) \in ℝ^{*}$
80		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
81	76 80	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
82	5 81	ffvelcdmd	$⊢ φ \to Q (I + 1) \in ℝ$
83	82	rexrd	$⊢ φ \to Q (I + 1) \in ℝ^{*}$
84	11 74	eqeltrid	$⊢ φ \to I \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
85		nfrab1	$⊢ \underline{Ⅎ} k \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
86		nfcv	$⊢ \underline{Ⅎ} k ℝ$
87		nfcv	$⊢ \underline{Ⅎ} k <$
88	85 86 87	nfsup	$⊢ \underline{Ⅎ} k sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <)$
89	11 88	nfcxfr	$⊢ \underline{Ⅎ} k I$
90		nfcv	$⊢ \underline{Ⅎ} k (0 ..^M)$
91		nfcv	$⊢ \underline{Ⅎ} k Q$
92	91 89	nffv	$⊢ \underline{Ⅎ} k Q (I)$
93		nfcv	$⊢ \underline{Ⅎ} k \leq$
94		nfcv	$⊢ \underline{Ⅎ} k S (J)$
95	92 93 94	nfbr	$⊢ Ⅎ k Q (I) \leq S (J)$
96		fveq2	$⊢ k = I \to Q (k) = Q (I)$
97	96	breq1d	$⊢ k = I \to (Q (k) \leq S (J) \leftrightarrow Q (I) \leq S (J))$
98	89 90 95 97	elrabf	$⊢ I \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \leftrightarrow (I \in (0 ..^M) \land Q (I) \leq S (J))$
99	84 98	sylib	$⊢ φ \to (I \in (0 ..^M) \land Q (I) \leq S (J))$
100	99	simprd	$⊢ φ \to Q (I) \leq S (J)$
101		simpr	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to \neg S (J + 1) \leq Q (I + 1)$
102	83	adantr	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to Q (I + 1) \in ℝ^{*}$
103		iccssxr	$⊢ [A, B] \subseteq ℝ^{*}$
104	44 103	sstrdi	$⊢ φ \to T \subseteq ℝ^{*}$
105		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
106	8 105	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
107	49 106	ffvelcdmd	$⊢ φ \to S (J + 1) \in T$
108	104 107	sseldd	$⊢ φ \to S (J + 1) \in ℝ^{*}$
109	108	adantr	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to S (J + 1) \in ℝ^{*}$
110		xrltnle	$⊢ (Q (I + 1) \in ℝ^{} \land S (J + 1) \in ℝ^{}) \to (Q (I + 1) < S (J + 1) \leftrightarrow \neg S (J + 1) \leq Q (I + 1))$
111	102 109 110	syl2anc	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to (Q (I + 1) < S (J + 1) \leftrightarrow \neg S (J + 1) \leq Q (I + 1))$
112	101 111	mpbird	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to Q (I + 1) < S (J + 1)$
113		fzssz	$⊢ (0 \dots N) \subseteq ℤ$
114		f1ofo	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} T \to S : (0 \dots N) \underset{onto}{⟶} T$
115	10 47 114	3syl	$⊢ φ \to S : (0 \dots N) \underset{onto}{⟶} T$
116	115	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to S : (0 \dots N) \underset{onto}{⟶} T$
117		ffun	$⊢ Q : (0 \dots M) ⟶ ℝ \to Fun Q$
118	5 117	syl	$⊢ φ \to Fun Q$
119	5	fdmd	$⊢ φ \to dom Q = (0 \dots M)$
120	119	eqcomd	$⊢ φ \to (0 \dots M) = dom Q$
121	81 120	eleqtrd	$⊢ φ \to I + 1 \in dom Q$
122		fvelrn	$⊢ (Fun Q \land I + 1 \in dom Q) \to Q (I + 1) \in ran Q$
123	118 121 122	syl2anc	$⊢ φ \to Q (I + 1) \in ran Q$
124	123	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in ran Q$
125	29	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to A \in ℝ^{*}$
126	30	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to B \in ℝ^{*}$
127	82	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in ℝ$
128	45 54	sseldd	$⊢ φ \to S (J) \in ℝ$
129	14	sseli	$⊢ I \in (0 \dots M) \to I \in ℤ$
130		zre	$⊢ I \in ℤ \to I \in ℝ$
131	77 129 130	3syl	$⊢ φ \to I \in ℝ$
132	131	adantr	$⊢ (φ \land \neg S (J) < Q (I + 1)) \to I \in ℝ$
133	132	ltp1d	$⊢ (φ \land \neg S (J) < Q (I + 1)) \to I < I + 1$
134	133	adantlr	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to I < I + 1$
135		simplr	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to Q (I + 1) \in ℝ$
136	128	ad2antrr	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to S (J) \in ℝ$
137		simpr	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to \neg S (J) < Q (I + 1)$
138	135 136 137	nltled	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to Q (I + 1) \leq S (J)$
139	131	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I \in ℝ$
140		1red	$⊢ (φ \land Q (I + 1) \leq S (J)) \to 1 \in ℝ$
141	139 140	readdcld	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I + 1 \in ℝ$
142		elfzoelz	$⊢ j \in (0 ..^M) \to j \in ℤ$
143	142	zred	$⊢ j \in (0 ..^M) \to j \in ℝ$
144	143	ssriv	$⊢ (0 ..^M) \subseteq ℝ$
145	12 144	sstri	$⊢ \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℝ$
146	145	a1i	$⊢ (φ \land Q (I + 1) \leq S (J)) \to \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℝ$
147	62	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \neq \emptyset$
148	72	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to \exists x \in ℝ \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x$
149	82	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to Q (I + 1) \in ℝ$
150	128	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to S (J) \in ℝ$
151	3	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to B \in ℝ$
152		simpr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to Q (I + 1) \leq S (J)$
153	46 107	sseldd	$⊢ φ \to S (J + 1) \in ℝ$
154	153	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to S (J + 1) \in ℝ$
155		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
156		zre	$⊢ J \in ℤ \to J \in ℝ$
157	8 155 156	3syl	$⊢ φ \to J \in ℝ$
158	157	ltp1d	$⊢ φ \to J < J + 1$
159		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), T) \land (J \in (0 \dots N) \land J + 1 \in (0 \dots N))) \to (J < J + 1 \leftrightarrow S (J) < S (J + 1))$
160	10 51 106 159	syl12anc	$⊢ φ \to (J < J + 1 \leftrightarrow S (J) < S (J + 1))$
161	158 160	mpbid	$⊢ φ \to S (J) < S (J + 1)$
162	161	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to S (J) < S (J + 1)$
163	44 107	sseldd	$⊢ φ \to S (J + 1) \in [A, B]$
164		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land S (J + 1) \in [A, B]) \to S (J + 1) \leq B$
165	29 30 163 164	syl3anc	$⊢ φ \to S (J + 1) \leq B$
166	165	adantr	$⊢ (φ \land Q (I + 1) \leq S (J)) \to S (J + 1) \leq B$
167	150 154 151 162 166	ltletrd	$⊢ (φ \land Q (I + 1) \leq S (J)) \to S (J) < B$
168	149 150 151 152 167	lelttrd	$⊢ (φ \land Q (I + 1) \leq S (J)) \to Q (I + 1) < B$
169	168	adantr	$⊢ ((φ \land Q (I + 1) \leq S (J)) \land \neg I + 1 \in (0 ..^M)) \to Q (I + 1) < B$
170	3	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to B \in ℝ$
171	82	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to Q (I + 1) \in ℝ$
172	7	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to B \leq Q (M)$
173	23	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to M \in ℤ$
174	81	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to I + 1 \in (0 \dots M)$
175		fzval3	$⊢ M \in ℤ \to (0 \dots M) = (0 ..^M + 1)$
176	23 175	syl	$⊢ φ \to (0 \dots M) = (0 ..^M + 1)$
177	176	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to (0 \dots M) = (0 ..^M + 1)$
178	174 177	eleqtrd	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to I + 1 \in (0 ..^M + 1)$
179		simpr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to \neg I + 1 \in (0 ..^M)$
180	178 179	jca	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to (I + 1 \in (0 ..^M + 1) \land \neg I + 1 \in (0 ..^M))$
181		elfzonelfzo	$⊢ M \in ℤ \to ((I + 1 \in (0 ..^M + 1) \land \neg I + 1 \in (0 ..^M)) \to I + 1 \in (M ..^M + 1))$
182	173 180 181	sylc	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to I + 1 \in (M ..^M + 1)$
183		fzval3	$⊢ M \in ℤ \to (M \dots M) = (M ..^M + 1)$
184	23 183	syl	$⊢ φ \to (M \dots M) = (M ..^M + 1)$
185	184	eqcomd	$⊢ φ \to (M ..^M + 1) = (M \dots M)$
186	185	adantr	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to (M ..^M + 1) = (M \dots M)$
187	182 186	eleqtrd	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to I + 1 \in (M \dots M)$
188		elfz1eq	$⊢ I + 1 \in (M \dots M) \to I + 1 = M$
189	187 188	syl	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to I + 1 = M$
190	189	eqcomd	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to M = I + 1$
191	190	fveq2d	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to Q (M) = Q (I + 1)$
192	172 191	breqtrd	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to B \leq Q (I + 1)$
193	170 171 192	lensymd	$⊢ (φ \land \neg I + 1 \in (0 ..^M)) \to \neg Q (I + 1) < B$
194	193	adantlr	$⊢ ((φ \land Q (I + 1) \leq S (J)) \land \neg I + 1 \in (0 ..^M)) \to \neg Q (I + 1) < B$
195	169 194	condan	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I + 1 \in (0 ..^M)$
196		nfcv	$⊢ \underline{Ⅎ} k +$
197		nfcv	$⊢ \underline{Ⅎ} k 1$
198	89 196 197	nfov	$⊢ \underline{Ⅎ} k (I + 1)$
199	91 198	nffv	$⊢ \underline{Ⅎ} k Q (I + 1)$
200	199 93 94	nfbr	$⊢ Ⅎ k Q (I + 1) \leq S (J)$
201		fveq2	$⊢ k = I + 1 \to Q (k) = Q (I + 1)$
202	201	breq1d	$⊢ k = I + 1 \to (Q (k) \leq S (J) \leftrightarrow Q (I + 1) \leq S (J))$
203	198 90 200 202	elrabf	$⊢ I + 1 \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \leftrightarrow (I + 1 \in (0 ..^M) \land Q (I + 1) \leq S (J))$
204	195 152 203	sylanbrc	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I + 1 \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}$
205		suprub	$⊢ ((\{k \in (0 ..^M) \| Q (k) \leq S (J)\} \subseteq ℝ \land \{k \in (0 ..^M) \| Q (k) \leq S (J)\} \neq \emptyset \land \exists x \in ℝ \forall j \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\} j \leq x) \land I + 1 \in \{k \in (0 ..^M) \| Q (k) \leq S (J)\}) \to I + 1 \leq sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <)$
206	146 147 148 204 205	syl31anc	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I + 1 \leq sup (\{k \in (0 ..^M) \| Q (k) \leq S (J)\} ℝ <)$
207	206 11	breqtrrdi	$⊢ (φ \land Q (I + 1) \leq S (J)) \to I + 1 \leq I$
208	141 139 207	lensymd	$⊢ (φ \land Q (I + 1) \leq S (J)) \to \neg I < I + 1$
209	208	adantlr	$⊢ ((φ \land Q (I + 1) \in ℝ) \land Q (I + 1) \leq S (J)) \to \neg I < I + 1$
210	138 209	syldan	$⊢ ((φ \land Q (I + 1) \in ℝ) \land \neg S (J) < Q (I + 1)) \to \neg I < I + 1$
211	134 210	condan	$⊢ (φ \land Q (I + 1) \in ℝ) \to S (J) < Q (I + 1)$
212	82 211	mpdan	$⊢ φ \to S (J) < Q (I + 1)$
213	2 128 82 56 212	lelttrd	$⊢ φ \to A < Q (I + 1)$
214	213	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to A < Q (I + 1)$
215	153	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to S (J + 1) \in ℝ$
216	3	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to B \in ℝ$
217		simpr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) < S (J + 1)$
218	165	adantr	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to S (J + 1) \leq B$
219	127 215 216 217 218	ltletrd	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) < B$
220	125 126 127 214 219	eliood	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in (A, B)$
221	124 220	elind	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in (ran Q \cap (A, B))$
222		elun2	$⊢ Q (I + 1) \in (ran Q \cap (A, B)) \to Q (I + 1) \in (\{A, B\} \cup (ran Q \cap (A, B)))$
223	221 222	syl	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in (\{A, B\} \cup (ran Q \cap (A, B)))$
224	223 9	eleqtrrdi	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to Q (I + 1) \in T$
225		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} T \land Q (I + 1) \in T) \to \exists j \in (0 \dots N) Q (I + 1) = S (j)$
226	116 224 225	syl2anc	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to \exists j \in (0 \dots N) Q (I + 1) = S (j)$
227	212	adantr	$⊢ (φ \land Q (I + 1) = S (j)) \to S (J) < Q (I + 1)$
228		simpr	$⊢ (φ \land Q (I + 1) = S (j)) \to Q (I + 1) = S (j)$
229	227 228	breqtrd	$⊢ (φ \land Q (I + 1) = S (j)) \to S (J) < S (j)$
230	229	adantlr	$⊢ ((φ \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to S (J) < S (j)$
231	10	ad2antrr	$⊢ ((φ \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to S {Isom}_{<, <} ((0 \dots N), T)$
232	51	anim1i	$⊢ (φ \land j \in (0 \dots N)) \to (J \in (0 \dots N) \land j \in (0 \dots N))$
233	232	adantr	$⊢ ((φ \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to (J \in (0 \dots N) \land j \in (0 \dots N))$
234		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), T) \land (J \in (0 \dots N) \land j \in (0 \dots N))) \to (J < j \leftrightarrow S (J) < S (j))$
235	231 233 234	syl2anc	$⊢ ((φ \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to (J < j \leftrightarrow S (J) < S (j))$
236	230 235	mpbird	$⊢ ((φ \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to J < j$
237	236	adantllr	$⊢ (((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to J < j$
238		eqcom	$⊢ Q (I + 1) = S (j) \leftrightarrow S (j) = Q (I + 1)$
239	238	bilani	$⊢ (Q (I + 1) < S (J + 1) \land Q (I + 1) = S (j)) \to S (j) = Q (I + 1)$
240		simpl	$⊢ (Q (I + 1) < S (J + 1) \land Q (I + 1) = S (j)) \to Q (I + 1) < S (J + 1)$
241	239 240	eqbrtrd	$⊢ (Q (I + 1) < S (J + 1) \land Q (I + 1) = S (j)) \to S (j) < S (J + 1)$
242	241	adantll	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land Q (I + 1) = S (j)) \to S (j) < S (J + 1)$
243	242	adantlr	$⊢ (((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to S (j) < S (J + 1)$
244	10	ad2antrr	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \to S {Isom}_{<, <} ((0 \dots N), T)$
245		simpr	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \to j \in (0 \dots N)$
246	106	ad2antrr	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \to J + 1 \in (0 \dots N)$
247		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), T) \land (j \in (0 \dots N) \land J + 1 \in (0 \dots N))) \to (j < J + 1 \leftrightarrow S (j) < S (J + 1))$
248	244 245 246 247	syl12anc	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \to (j < J + 1 \leftrightarrow S (j) < S (J + 1))$
249	248	adantr	$⊢ (((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to (j < J + 1 \leftrightarrow S (j) < S (J + 1))$
250	243 249	mpbird	$⊢ (((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to j < J + 1$
251	237 250	jca	$⊢ (((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \land Q (I + 1) = S (j)) \to (J < j \land j < J + 1)$
252	251	ex	$⊢ ((φ \land Q (I + 1) < S (J + 1)) \land j \in (0 \dots N)) \to (Q (I + 1) = S (j) \to (J < j \land j < J + 1))$
253	252	reximdva	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to (\exists j \in (0 \dots N) Q (I + 1) = S (j) \to \exists j \in (0 \dots N) (J < j \land j < J + 1))$
254	226 253	mpd	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to \exists j \in (0 \dots N) (J < j \land j < J + 1)$
255		ssrexv	$⊢ (0 \dots N) \subseteq ℤ \to (\exists j \in (0 \dots N) (J < j \land j < J + 1) \to \exists j \in ℤ (J < j \land j < J + 1))$
256	113 254 255	mpsyl	$⊢ (φ \land Q (I + 1) < S (J + 1)) \to \exists j \in ℤ (J < j \land j < J + 1)$
257	112 256	syldan	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to \exists j \in ℤ (J < j \land j < J + 1)$
258		simplr	$⊢ ((φ \land j \in ℤ) \land (J < j \land j < J + 1)) \to j \in ℤ$
259	8 155	syl	$⊢ φ \to J \in ℤ$
260	259	ad2antrr	$⊢ ((φ \land j \in ℤ) \land (J < j \land j < J + 1)) \to J \in ℤ$
261		simprl	$⊢ ((φ \land j \in ℤ) \land (J < j \land j < J + 1)) \to J < j$
262		simprr	$⊢ ((φ \land j \in ℤ) \land (J < j \land j < J + 1)) \to j < J + 1$
263		btwnnz	$⊢ (J \in ℤ \land J < j \land j < J + 1) \to \neg j \in ℤ$
264	260 261 262 263	syl3anc	$⊢ ((φ \land j \in ℤ) \land (J < j \land j < J + 1)) \to \neg j \in ℤ$
265	258 264	pm2.65da	$⊢ (φ \land j \in ℤ) \to \neg (J < j \land j < J + 1)$
266	265	nrexdv	$⊢ φ \to \neg \exists j \in ℤ (J < j \land j < J + 1)$
267	266	adantr	$⊢ (φ \land \neg S (J + 1) \leq Q (I + 1)) \to \neg \exists j \in ℤ (J < j \land j < J + 1)$
268	257 267	condan	$⊢ φ \to S (J + 1) \leq Q (I + 1)$
269		ioossioo	$⊢ ((Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{}) \land (Q (I) \leq S (J) \land S (J + 1) \leq Q (I + 1))) \to (S (J), S (J + 1)) \subseteq (Q (I), Q (I + 1))$
270	79 83 100 268 269	syl22anc	$⊢ φ \to (S (J), S (J + 1)) \subseteq (Q (I), Q (I + 1))$
271		fveq2	$⊢ i = I \to Q (i) = Q (I)$
272		oveq1	$⊢ i = I \to i + 1 = I + 1$
273	272	fveq2d	$⊢ i = I \to Q (i + 1) = Q (I + 1)$
274	271 273	oveq12d	$⊢ i = I \to (Q (i), Q (i + 1)) = (Q (I), Q (I + 1))$
275	274	sseq2d	$⊢ i = I \to ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \leftrightarrow (S (J), S (J + 1)) \subseteq (Q (I), Q (I + 1)))$
276	275	rspcev	$⊢ (I \in (0 ..^M) \land (S (J), S (J + 1)) \subseteq (Q (I), Q (I + 1))) \to \exists i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
277	76 270 276	syl2anc	$⊢ φ \to \exists i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$

Metamath Proof Explorer

Theorem fourierdlem20

Proof