fourierdlem12

Description: A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem12.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem12.2	$⊢ φ \to M \in ℕ$
	fourierdlem12.3	$⊢ φ \to Q \in P (M)$
	fourierdlem12.4	$⊢ φ \to X \in ran Q$
Assertion	fourierdlem12	$⊢ (φ \land i \in (0 ..^M)) \to \neg X \in (Q (i), Q (i + 1))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem12.1	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem12.2	$⊢ φ \to M \in ℕ$
3		fourierdlem12.3	$⊢ φ \to Q \in P (M)$
4		fourierdlem12.4	$⊢ φ \to X \in ran Q$
5	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
6	2 5	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
7	3 6	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
8	7	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
9		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
10		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
11	8 9 10	3syl	$⊢ φ \to Q Fn (0 \dots M)$
12		fvelrnb	$⊢ Q Fn (0 \dots M) \to (X \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = X)$
13	11 12	syl	$⊢ φ \to (X \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = X)$
14	4 13	mpbid	$⊢ φ \to \exists j \in (0 \dots M) Q (j) = X$
15	14	adantr	$⊢ (φ \land i \in (0 ..^M)) \to \exists j \in (0 \dots M) Q (j) = X$
16	8 9	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
17	16	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
18		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
19	18	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
20	17 19	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
21	20	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land i < j) \to Q (i + 1) \in ℝ$
22	21	3ad2antl1	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to Q (i + 1) \in ℝ$
23		frn	$⊢ Q : (0 \dots M) ⟶ ℝ \to ran Q \subseteq ℝ$
24	16 23	syl	$⊢ φ \to ran Q \subseteq ℝ$
25	24 4	sseldd	$⊢ φ \to X \in ℝ$
26	25	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land i < j) \to X \in ℝ$
27	26	3ad2antl1	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to X \in ℝ$
28	17	ffvelrnda	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \to Q (j) \in ℝ$
29	28	3adant3	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \to Q (j) \in ℝ$
30	29	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to Q (j) \in ℝ$
31		simpr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to i < j$
32		elfzoelz	$⊢ i \in (0 ..^M) \to i \in ℤ$
33	32	ad2antrr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to i \in ℤ$
34		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
35	34	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to j \in ℤ$
36		zltp1le	$⊢ (i \in ℤ \land j \in ℤ) \to (i < j \leftrightarrow i + 1 \leq j)$
37	33 35 36	syl2anc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to (i < j \leftrightarrow i + 1 \leq j)$
38	31 37	mpbid	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to i + 1 \leq j$
39	33	peano2zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to i + 1 \in ℤ$
40		eluz	$⊢ (i + 1 \in ℤ \land j \in ℤ) \to (j \in ℤ_{\geq (i + 1)} \leftrightarrow i + 1 \leq j)$
41	39 35 40	syl2anc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to (j \in ℤ_{\geq (i + 1)} \leftrightarrow i + 1 \leq j)$
42	38 41	mpbird	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land i < j) \to j \in ℤ_{\geq (i + 1)}$
43	42	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \to j \in ℤ_{\geq (i + 1)}$
44	17	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to Q : (0 \dots M) ⟶ ℝ$
45		0red	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to 0 \in ℝ$
46		elfzelz	$⊢ w \in (i + 1 \dots j) \to w \in ℤ$
47	46	zred	$⊢ w \in (i + 1 \dots j) \to w \in ℝ$
48	47	adantl	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to w \in ℝ$
49	32	peano2zd	$⊢ i \in (0 ..^M) \to i + 1 \in ℤ$
50	49	zred	$⊢ i \in (0 ..^M) \to i + 1 \in ℝ$
51	50	adantr	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to i + 1 \in ℝ$
52	32	zred	$⊢ i \in (0 ..^M) \to i \in ℝ$
53	52	adantr	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to i \in ℝ$
54		elfzole1	$⊢ i \in (0 ..^M) \to 0 \leq i$
55	54	adantr	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to 0 \leq i$
56	53	ltp1d	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to i < i + 1$
57	45 53 51 55 56	lelttrd	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to 0 < i + 1$
58		elfzle1	$⊢ w \in (i + 1 \dots j) \to i + 1 \leq w$
59	58	adantl	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to i + 1 \leq w$
60	45 51 48 57 59	ltletrd	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to 0 < w$
61	45 48 60	ltled	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j)) \to 0 \leq w$
62	61	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to 0 \leq w$
63	47	adantl	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to w \in ℝ$
64	34	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
65	64	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to j \in ℝ$
66		elfzel2	$⊢ j \in (0 \dots M) \to M \in ℤ$
67	66	zred	$⊢ j \in (0 \dots M) \to M \in ℝ$
68	67	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to M \in ℝ$
69		elfzle2	$⊢ w \in (i + 1 \dots j) \to w \leq j$
70	69	adantl	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to w \leq j$
71		elfzle2	$⊢ j \in (0 \dots M) \to j \leq M$
72	71	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to j \leq M$
73	63 65 68 70 72	letrd	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j)) \to w \leq M$
74	73	adantll	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to w \leq M$
75	46	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to w \in ℤ$
76		0zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to 0 \in ℤ$
77	66	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to M \in ℤ$
78		elfz	$⊢ (w \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (w \in (0 \dots M) \leftrightarrow (0 \leq w \land w \leq M))$
79	75 76 77 78	syl3anc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to (w \in (0 \dots M) \leftrightarrow (0 \leq w \land w \leq M))$
80	62 74 79	mpbir2and	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to w \in (0 \dots M)$
81	80	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to w \in (0 \dots M)$
82	44 81	ffvelrnd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j)) \to Q (w) \in ℝ$
83	82	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j)) \to Q (w) \in ℝ$
84		simp-4l	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to φ$
85		0red	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j - 1)) \to 0 \in ℝ$
86		elfzelz	$⊢ w \in (i + 1 \dots j - 1) \to w \in ℤ$
87	86	zred	$⊢ w \in (i + 1 \dots j - 1) \to w \in ℝ$
88	87	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j - 1)) \to w \in ℝ$
89		0red	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to 0 \in ℝ$
90	50	adantr	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to i + 1 \in ℝ$
91	87	adantl	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to w \in ℝ$
92		0red	$⊢ i \in (0 ..^M) \to 0 \in ℝ$
93	52	ltp1d	$⊢ i \in (0 ..^M) \to i < i + 1$
94	92 52 50 54 93	lelttrd	$⊢ i \in (0 ..^M) \to 0 < i + 1$
95	94	adantr	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to 0 < i + 1$
96		elfzle1	$⊢ w \in (i + 1 \dots j - 1) \to i + 1 \leq w$
97	96	adantl	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to i + 1 \leq w$
98	89 90 91 95 97	ltletrd	$⊢ (i \in (0 ..^M) \land w \in (i + 1 \dots j - 1)) \to 0 < w$
99	98	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j - 1)) \to 0 < w$
100	85 88 99	ltled	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j - 1)) \to 0 \leq w$
101	100	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (i + 1 \dots j - 1)) \to 0 \leq w$
102	101	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to 0 \leq w$
103	87	adantl	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to w \in ℝ$
104		peano2rem	$⊢ j \in ℝ \to j - 1 \in ℝ$
105	64 104	syl	$⊢ j \in (0 \dots M) \to j - 1 \in ℝ$
106	105	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to j - 1 \in ℝ$
107	67	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to M \in ℝ$
108		elfzle2	$⊢ w \in (i + 1 \dots j - 1) \to w \leq j - 1$
109	108	adantl	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to w \leq j - 1$
110		zlem1lt	$⊢ (j \in ℤ \land M \in ℤ) \to (j \leq M \leftrightarrow j - 1 < M)$
111	34 66 110	syl2anc	$⊢ j \in (0 \dots M) \to (j \leq M \leftrightarrow j - 1 < M)$
112	71 111	mpbid	$⊢ j \in (0 \dots M) \to j - 1 < M$
113	112	adantr	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to j - 1 < M$
114	103 106 107 109 113	lelttrd	$⊢ (j \in (0 \dots M) \land w \in (i + 1 \dots j - 1)) \to w < M$
115	114	adantlr	$⊢ ((j \in (0 \dots M) \land i < j) \land w \in (i + 1 \dots j - 1)) \to w < M$
116	115	adantlll	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to w < M$
117	86	adantl	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to w \in ℤ$
118		0zd	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to 0 \in ℤ$
119	66	ad3antlr	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to M \in ℤ$
120		elfzo	$⊢ (w \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (w \in (0 ..^M) \leftrightarrow (0 \leq w \land w < M))$
121	117 118 119 120	syl3anc	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to (w \in (0 ..^M) \leftrightarrow (0 \leq w \land w < M))$
122	102 116 121	mpbir2and	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to w \in (0 ..^M)$
123	16	adantr	$⊢ (φ \land w \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
124		elfzofz	$⊢ w \in (0 ..^M) \to w \in (0 \dots M)$
125	124	adantl	$⊢ (φ \land w \in (0 ..^M)) \to w \in (0 \dots M)$
126	123 125	ffvelrnd	$⊢ (φ \land w \in (0 ..^M)) \to Q (w) \in ℝ$
127		fzofzp1	$⊢ w \in (0 ..^M) \to w + 1 \in (0 \dots M)$
128	127	adantl	$⊢ (φ \land w \in (0 ..^M)) \to w + 1 \in (0 \dots M)$
129	123 128	ffvelrnd	$⊢ (φ \land w \in (0 ..^M)) \to Q (w + 1) \in ℝ$
130		eleq1w	$⊢ i = w \to (i \in (0 ..^M) \leftrightarrow w \in (0 ..^M))$
131	130	anbi2d	$⊢ i = w \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land w \in (0 ..^M)))$
132		fveq2	$⊢ i = w \to Q (i) = Q (w)$
133		oveq1	$⊢ i = w \to i + 1 = w + 1$
134	133	fveq2d	$⊢ i = w \to Q (i + 1) = Q (w + 1)$
135	132 134	breq12d	$⊢ i = w \to (Q (i) < Q (i + 1) \leftrightarrow Q (w) < Q (w + 1))$
136	131 135	imbi12d	$⊢ i = w \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land w \in (0 ..^M)) \to Q (w) < Q (w + 1)))$
137	7	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
138	137	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
139	136 138	chvarvv	$⊢ (φ \land w \in (0 ..^M)) \to Q (w) < Q (w + 1)$
140	126 129 139	ltled	$⊢ (φ \land w \in (0 ..^M)) \to Q (w) \leq Q (w + 1)$
141	84 122 140	syl2anc	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \land w \in (i + 1 \dots j - 1)) \to Q (w) \leq Q (w + 1)$
142	43 83 141	monoord	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land i < j) \to Q (i + 1) \leq Q (j)$
143	142	3adantl3	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to Q (i + 1) \leq Q (j)$
144	16	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ$
145	144	3adant3	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = X) \to Q (j) \in ℝ$
146		simp3	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = X) \to Q (j) = X$
147	145 146	eqled	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = X) \to Q (j) \leq X$
148	147	3adant1r	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \to Q (j) \leq X$
149	148	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to Q (j) \leq X$
150	22 30 27 143 149	letrd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to Q (i + 1) \leq X$
151	22 27 150	lensymd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to \neg X < Q (i + 1)$
152	151	intnand	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land i < j) \to \neg (Q (i) < X \land X < Q (i + 1))$
153	64	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land \neg i < j) \to j \in ℝ$
154	52	ad3antlr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land \neg i < j) \to i \in ℝ$
155		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land \neg i < j) \to \neg i < j$
156	153 154 155	nltled	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land \neg i < j) \to j \leq i$
157	156	3adantl3	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land \neg i < j) \to j \leq i$
158		eqcom	$⊢ Q (j) = X \leftrightarrow X = Q (j)$
159	158	biimpi	$⊢ Q (j) = X \to X = Q (j)$
160	159	adantr	$⊢ (Q (j) = X \land j \leq i) \to X = Q (j)$
161	160	3ad2antl3	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to X = Q (j)$
162	34	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to j \in ℤ$
163	32	ad2antrr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ$
164		simpr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to j \leq i$
165		eluz2	$⊢ i \in ℤ_{\geq j} \leftrightarrow (j \in ℤ \land i \in ℤ \land j \leq i)$
166	162 163 164 165	syl3anbrc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ_{\geq j}$
167	166	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ_{\geq j}$
168	17	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to Q : (0 \dots M) ⟶ ℝ$
169		0zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to 0 \in ℤ$
170	66	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to M \in ℤ$
171		elfzelz	$⊢ w \in (j \dots i) \to w \in ℤ$
172	171	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \in ℤ$
173	169 170 172	3jca	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to (0 \in ℤ \land M \in ℤ \land w \in ℤ)$
174		0red	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \in ℝ$
175	64	adantr	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to j \in ℝ$
176	171	zred	$⊢ w \in (j \dots i) \to w \in ℝ$
177	176	adantl	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to w \in ℝ$
178		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
179	178	adantr	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \leq j$
180		elfzle1	$⊢ w \in (j \dots i) \to j \leq w$
181	180	adantl	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to j \leq w$
182	174 175 177 179 181	letrd	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \leq w$
183	182	adantll	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to 0 \leq w$
184	176	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \in ℝ$
185		elfzoel2	$⊢ i \in (0 ..^M) \to M \in ℤ$
186	185	zred	$⊢ i \in (0 ..^M) \to M \in ℝ$
187	186	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to M \in ℝ$
188	52	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to i \in ℝ$
189		elfzle2	$⊢ w \in (j \dots i) \to w \leq i$
190	189	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \leq i$
191		elfzolt2	$⊢ i \in (0 ..^M) \to i < M$
192	191	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to i < M$
193	184 188 187 190 192	lelttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w < M$
194	184 187 193	ltled	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \leq M$
195	194	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \leq M$
196	173 183 195	jca32	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to ((0 \in ℤ \land M \in ℤ \land w \in ℤ) \land (0 \leq w \land w \leq M))$
197	196	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to ((0 \in ℤ \land M \in ℤ \land w \in ℤ) \land (0 \leq w \land w \leq M))$
198		elfz2	$⊢ w \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land w \in ℤ) \land (0 \leq w \land w \leq M))$
199	197 198	sylibr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \in (0 \dots M)$
200	168 199	ffvelrnd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to Q (w) \in ℝ$
201	200	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \land w \in (j \dots i)) \to Q (w) \in ℝ$
202		simplll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to φ$
203		0red	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \in ℝ$
204	64	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to j \in ℝ$
205		elfzelz	$⊢ w \in (j \dots i - 1) \to w \in ℤ$
206	205	zred	$⊢ w \in (j \dots i - 1) \to w \in ℝ$
207	206	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in ℝ$
208	178	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \leq j$
209		elfzle1	$⊢ w \in (j \dots i - 1) \to j \leq w$
210	209	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to j \leq w$
211	203 204 207 208 210	letrd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \leq w$
212	206	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w \in ℝ$
213	52	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i \in ℝ$
214	186	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to M \in ℝ$
215		peano2rem	$⊢ i \in ℝ \to i - 1 \in ℝ$
216	213 215	syl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i - 1 \in ℝ$
217		elfzle2	$⊢ w \in (j \dots i - 1) \to w \leq i - 1$
218	217	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w \leq i - 1$
219	213	ltm1d	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i - 1 < i$
220	212 216 213 218 219	lelttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w < i$
221	191	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i < M$
222	212 213 214 220 221	lttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w < M$
223	222	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w < M$
224	205	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in ℤ$
225		0zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \in ℤ$
226	185	ad2antrr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to M \in ℤ$
227	224 225 226 120	syl3anc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to (w \in (0 ..^M) \leftrightarrow (0 \leq w \land w < M))$
228	211 223 227	mpbir2and	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in (0 ..^M)$
229	228	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in (0 ..^M)$
230	202 229 140	syl2anc	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to Q (w) \leq Q (w + 1)$
231	230	adantlr	$⊢ ((((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \land w \in (j \dots i - 1)) \to Q (w) \leq Q (w + 1)$
232	167 201 231	monoord	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \to Q (j) \leq Q (i)$
233	232	3adantl3	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to Q (j) \leq Q (i)$
234	161 233	eqbrtrd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to X \leq Q (i)$
235	25	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
236		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
237	236	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
238	17 237	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
239	235 238	lenltd	$⊢ (φ \land i \in (0 ..^M)) \to (X \leq Q (i) \leftrightarrow \neg Q (i) < X)$
240	239	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land j \leq i) \to (X \leq Q (i) \leftrightarrow \neg Q (i) < X)$
241	240	3ad2antl1	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to (X \leq Q (i) \leftrightarrow \neg Q (i) < X)$
242	234 241	mpbid	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to \neg Q (i) < X$
243	157 242	syldan	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land \neg i < j) \to \neg Q (i) < X$
244	243	intnanrd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land \neg i < j) \to \neg (Q (i) < X \land X < Q (i + 1))$
245	152 244	pm2.61dan	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \to \neg (Q (i) < X \land X < Q (i + 1))$
246	245	intnand	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \to \neg ((Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (Q (i) < X \land X < Q (i + 1)))$
247		elioo3g	$⊢ X \in (Q (i), Q (i + 1)) \leftrightarrow ((Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land X \in ℝ^{*}) \land (Q (i) < X \land X < Q (i + 1)))$
248	246 247	sylnibr	$⊢ ((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \to \neg X \in (Q (i), Q (i + 1))$
249	248	rexlimdv3a	$⊢ (φ \land i \in (0 ..^M)) \to (\exists j \in (0 \dots M) Q (j) = X \to \neg X \in (Q (i), Q (i + 1)))$
250	15 249	mpd	$⊢ (φ \land i \in (0 ..^M)) \to \neg X \in (Q (i), Q (i + 1))$

Metamath Proof Explorer

Theorem fourierdlem12

Proof