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

Metamath Proof Explorer

Theorem fourierdlem12

Proof