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	birani	$⊢ (Q (j) = X \land j \leq i) \to X = Q (j)$
157	156	3ad2antl3	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M) \land Q (j) = X) \land j \leq i) \to X = Q (j)$
158	33	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to j \in ℤ$
159	31	ad2antrr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ$
160		simpr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to j \leq i$
161		eluz2	$⊢ i \in ℤ_{\geq j} \leftrightarrow (j \in ℤ \land i \in ℤ \land j \leq i)$
162	158 159 160 161	syl3anbrc	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ_{\geq j}$
163	162	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \to i \in ℤ_{\geq j}$
164	16	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to Q : (0 \dots M) ⟶ ℝ$
165		0zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to 0 \in ℤ$
166	45	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to M \in ℤ$
167		elfzelz	$⊢ w \in (j \dots i) \to w \in ℤ$
168	167	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \in ℤ$
169	165 166 168	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 ℤ)$
170		0red	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \in ℝ$
171	67	adantr	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to j \in ℝ$
172	167	zred	$⊢ w \in (j \dots i) \to w \in ℝ$
173	172	adantl	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to w \in ℝ$
174		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
175	174	adantr	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \leq j$
176		elfzle1	$⊢ w \in (j \dots i) \to j \leq w$
177	176	adantl	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to j \leq w$
178	170 171 173 175 177	letrd	$⊢ (j \in (0 \dots M) \land w \in (j \dots i)) \to 0 \leq w$
179	178	adantll	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to 0 \leq w$
180	172	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \in ℝ$
181		elfzoel2	$⊢ i \in (0 ..^M) \to M \in ℤ$
182	181	zred	$⊢ i \in (0 ..^M) \to M \in ℝ$
183	182	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to M \in ℝ$
184	55	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to i \in ℝ$
185		elfzle2	$⊢ w \in (j \dots i) \to w \leq i$
186	185	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \leq i$
187		elfzolt2	$⊢ i \in (0 ..^M) \to i < M$
188	187	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to i < M$
189	180 184 183 186 188	lelttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w < M$
190	180 183 189	ltled	$⊢ (i \in (0 ..^M) \land w \in (j \dots i)) \to w \leq M$
191	190	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \leq M$
192	169 179 191	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))$
193	192	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))$
194		elfz2	$⊢ w \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land w \in ℤ) \land (0 \leq w \land w \leq M))$
195	193 194	sylibr	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to w \in (0 \dots M)$
196	164 195	ffvelcdmd	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i)) \to Q (w) \in ℝ$
197	196	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 ℝ$
198		simplll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to φ$
199		0red	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \in ℝ$
200	67	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to j \in ℝ$
201		elfzelz	$⊢ w \in (j \dots i - 1) \to w \in ℤ$
202	201	zred	$⊢ w \in (j \dots i - 1) \to w \in ℝ$
203	202	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in ℝ$
204	174	ad2antlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \leq j$
205		elfzle1	$⊢ w \in (j \dots i - 1) \to j \leq w$
206	205	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to j \leq w$
207	199 200 203 204 206	letrd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \leq w$
208	202	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w \in ℝ$
209	55	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i \in ℝ$
210	182	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to M \in ℝ$
211		peano2rem	$⊢ i \in ℝ \to i - 1 \in ℝ$
212	209 211	syl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i - 1 \in ℝ$
213		elfzle2	$⊢ w \in (j \dots i - 1) \to w \leq i - 1$
214	213	adantl	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w \leq i - 1$
215	209	ltm1d	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i - 1 < i$
216	208 212 209 214 215	lelttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w < i$
217	187	adantr	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to i < M$
218	208 209 210 216 217	lttrd	$⊢ (i \in (0 ..^M) \land w \in (j \dots i - 1)) \to w < M$
219	218	adantlr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w < M$
220	201	adantl	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in ℤ$
221		0zd	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to 0 \in ℤ$
222	181	ad2antrr	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to M \in ℤ$
223	220 221 222 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))$
224	207 219 223	mpbir2and	$⊢ ((i \in (0 ..^M) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in (0 ..^M)$
225	224	adantlll	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land w \in (j \dots i - 1)) \to w \in (0 ..^M)$
226	198 225 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)$
227	226	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)$
228	163 197 227	monoord	$⊢ (((φ \land i \in (0 ..^M)) \land j \in (0 \dots M)) \land j \leq i) \to Q (j) \leq Q (i)$
229	228	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)$
230	157 229	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)$
231	24	adantr	$⊢ (φ \land i \in (0 ..^M)) \to X \in ℝ$
232		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
233	232	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
234	16 233	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
235	231 234	lenltd	$⊢ (φ \land i \in (0 ..^M)) \to (X \leq Q (i) \leftrightarrow \neg Q (i) < X)$
236	235	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land j \leq i) \to (X \leq Q (i) \leftrightarrow \neg Q (i) < X)$
237	236	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)$
238	230 237	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$
239	154 238	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$
240	239	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))$
241	149 240	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))$
242	241	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)))$
243		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)))$
244	242 243	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))$
245	244	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)))$
246	14 245	mpd	$⊢ (φ \land i \in (0 ..^M)) \to \neg X \in (Q (i), Q (i + 1))$

Metamath Proof Explorer

Theorem fourierdlem12

Proof