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

Metamath Proof Explorer

Theorem fourierdlem12

Proof