fourierdlem50

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem50.xre	$⊢ φ \to X \in ℝ$
	fourierdlem50.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem50.m	$⊢ φ \to M \in ℕ$
	fourierdlem50.v	$⊢ φ \to V \in P (M)$
	fourierdlem50.a	$⊢ φ \to A \in ℝ$
	fourierdlem50.b	$⊢ φ \to B \in ℝ$
	fourierdlem50.altb	$⊢ φ \to A < B$
	fourierdlem50.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
	fourierdlem50.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem50.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
	fourierdlem50.n	$⊢ N = \|T\| - 1$
	fourierdlem50.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
	fourierdlem50.j	$⊢ φ \to J \in (0 ..^N)$
	fourierdlem50.u	$⊢ U = (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)))$
	fourierdlem50.ch	$⊢ χ \leftrightarrow ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
Assertion	fourierdlem50	$⊢ φ \to (U \in (0 ..^M) \land (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem50.xre	$⊢ φ \to X \in ℝ$
2		fourierdlem50.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
3		fourierdlem50.m	$⊢ φ \to M \in ℕ$
4		fourierdlem50.v	$⊢ φ \to V \in P (M)$
5		fourierdlem50.a	$⊢ φ \to A \in ℝ$
6		fourierdlem50.b	$⊢ φ \to B \in ℝ$
7		fourierdlem50.altb	$⊢ φ \to A < B$
8		fourierdlem50.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
9		fourierdlem50.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
10		fourierdlem50.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
11		fourierdlem50.n	$⊢ N = \|T\| - 1$
12		fourierdlem50.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
13		fourierdlem50.j	$⊢ φ \to J \in (0 ..^N)$
14		fourierdlem50.u	$⊢ U = (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)))$
15		fourierdlem50.ch	$⊢ χ \leftrightarrow ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
16	5 6 7	ltled	$⊢ φ \to A \leq B$
17	2 3 4	fourierdlem15	$⊢ φ \to V : (0 \dots M) ⟶ [- π + X, π + X]$
18		pire	$⊢ π \in ℝ$
19	18	renegcli	$⊢ - π \in ℝ$
20	19	a1i	$⊢ φ \to - π \in ℝ$
21	20 1	readdcld	$⊢ φ \to - π + X \in ℝ$
22	18	a1i	$⊢ φ \to π \in ℝ$
23	22 1	readdcld	$⊢ φ \to π + X \in ℝ$
24	21 23	iccssred	$⊢ φ \to [- π + X, π + X] \subseteq ℝ$
25	17 24	fssd	$⊢ φ \to V : (0 \dots M) ⟶ ℝ$
26	25	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to V (i) \in ℝ$
27	1	adantr	$⊢ (φ \land i \in (0 \dots M)) \to X \in ℝ$
28	26 27	resubcld	$⊢ (φ \land i \in (0 \dots M)) \to V (i) - X \in ℝ$
29	28 9	fmptd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
30	9	a1i	$⊢ φ \to Q = (i \in (0 \dots M) ⟼ V (i) - X)$
31		fveq2	$⊢ i = 0 \to V (i) = V (0)$
32	31	oveq1d	$⊢ i = 0 \to V (i) - X = V (0) - X$
33	32	adantl	$⊢ (φ \land i = 0) \to V (i) - X = V (0) - X$
34		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
35	34	a1i	$⊢ φ \to ℕ \subseteq ℕ_{0}$
36		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
37	35 36	sseqtrdi	$⊢ φ \to ℕ \subseteq ℤ_{\geq 0}$
38	37 3	sseldd	$⊢ φ \to M \in ℤ_{\geq 0}$
39		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
40	38 39	syl	$⊢ φ \to 0 \in (0 \dots M)$
41	25 40	ffvelrnd	$⊢ φ \to V (0) \in ℝ$
42	41 1	resubcld	$⊢ φ \to V (0) - X \in ℝ$
43	30 33 40 42	fvmptd	$⊢ φ \to Q (0) = V (0) - X$
44	2	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
45	3 44	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
46	4 45	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
47	46	simprd	$⊢ φ \to ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))$
48	47	simpld	$⊢ φ \to (V (0) = - π + X \land V (M) = π + X)$
49	48	simpld	$⊢ φ \to V (0) = - π + X$
50	49	oveq1d	$⊢ φ \to V (0) - X = (- π) + X - X$
51	20	recnd	$⊢ φ \to - π \in ℂ$
52	1	recnd	$⊢ φ \to X \in ℂ$
53	51 52	pncand	$⊢ φ \to (- π) + X - X = - π$
54	43 50 53	3eqtrd	$⊢ φ \to Q (0) = - π$
55	20	rexrd	$⊢ φ \to - π \in ℝ^{*}$
56	22	rexrd	$⊢ φ \to π \in ℝ^{*}$
57	5	leidd	$⊢ φ \to A \leq A$
58	5 6 5 57 16	eliccd	$⊢ φ \to A \in [A, B]$
59	8 58	sseldd	$⊢ φ \to A \in [- π, π]$
60		iccgelb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in [- π, π]) \to - π \leq A$
61	55 56 59 60	syl3anc	$⊢ φ \to - π \leq A$
62	54 61	eqbrtrd	$⊢ φ \to Q (0) \leq A$
63	6	leidd	$⊢ φ \to B \leq B$
64	5 6 6 16 63	eliccd	$⊢ φ \to B \in [A, B]$
65	8 64	sseldd	$⊢ φ \to B \in [- π, π]$
66		iccleub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land B \in [- π, π]) \to B \leq π$
67	55 56 65 66	syl3anc	$⊢ φ \to B \leq π$
68		fveq2	$⊢ i = M \to V (i) = V (M)$
69	68	oveq1d	$⊢ i = M \to V (i) - X = V (M) - X$
70	69	adantl	$⊢ (φ \land i = M) \to V (i) - X = V (M) - X$
71		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
72	38 71	syl	$⊢ φ \to M \in (0 \dots M)$
73	25 72	ffvelrnd	$⊢ φ \to V (M) \in ℝ$
74	73 1	resubcld	$⊢ φ \to V (M) - X \in ℝ$
75	30 70 72 74	fvmptd	$⊢ φ \to Q (M) = V (M) - X$
76	48	simprd	$⊢ φ \to V (M) = π + X$
77	76	oveq1d	$⊢ φ \to V (M) - X = π + X - X$
78	22	recnd	$⊢ φ \to π \in ℂ$
79	78 52	pncand	$⊢ φ \to π + X - X = π$
80	75 77 79	3eqtrrd	$⊢ φ \to π = Q (M)$
81	67 80	breqtrd	$⊢ φ \to B \leq Q (M)$
82		prfi	$⊢ \{A, B\} \in Fin$
83	82	a1i	$⊢ φ \to \{A, B\} \in Fin$
84		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
85	9	rnmptfi	$⊢ (0 \dots M) \in Fin \to ran Q \in Fin$
86	84 85	syl	$⊢ φ \to ran Q \in Fin$
87		infi	$⊢ ran Q \in Fin \to ran Q \cap (A, B) \in Fin$
88	86 87	syl	$⊢ φ \to ran Q \cap (A, B) \in Fin$
89		unfi	$⊢ (\{A, B\} \in Fin \land ran Q \cap (A, B) \in Fin) \to \{A, B\} \cup (ran Q \cap (A, B)) \in Fin$
90	83 88 89	syl2anc	$⊢ φ \to \{A, B\} \cup (ran Q \cap (A, B)) \in Fin$
91	10 90	eqeltrid	$⊢ φ \to T \in Fin$
92	5 6	jca	$⊢ φ \to (A \in ℝ \land B \in ℝ)$
93		prssg	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \in ℝ \land B \in ℝ) \leftrightarrow \{A, B\} \subseteq ℝ)$
94	5 6 93	syl2anc	$⊢ φ \to ((A \in ℝ \land B \in ℝ) \leftrightarrow \{A, B\} \subseteq ℝ)$
95	92 94	mpbid	$⊢ φ \to \{A, B\} \subseteq ℝ$
96		inss2	$⊢ ran Q \cap (A, B) \subseteq (A, B)$
97		ioossre	$⊢ (A, B) \subseteq ℝ$
98	96 97	sstri	$⊢ ran Q \cap (A, B) \subseteq ℝ$
99	98	a1i	$⊢ φ \to ran Q \cap (A, B) \subseteq ℝ$
100	95 99	unssd	$⊢ φ \to \{A, B\} \cup (ran Q \cap (A, B)) \subseteq ℝ$
101	10 100	eqsstrid	$⊢ φ \to T \subseteq ℝ$
102	91 101 12 11	fourierdlem36	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), T)$
103		eqid	$⊢ sup (\{x \in (0 ..^M) \| Q (x) \leq S (J)\} ℝ <) = sup (\{x \in (0 ..^M) \| Q (x) \leq S (J)\} ℝ <)$
104	3 5 6 16 29 62 81 13 10 102 103	fourierdlem20	$⊢ φ \to \exists i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
105	15	biimpi	$⊢ χ \to ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
106		simp-4l	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to φ$
107	105 106	syl	$⊢ χ \to φ$
108		simplr	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to k \in (0 ..^M)$
109	105 108	syl	$⊢ χ \to k \in (0 ..^M)$
110	107 109	jca	$⊢ χ \to (φ \land k \in (0 ..^M))$
111		simp-4r	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to i \in (0 ..^M)$
112	105 111	syl	$⊢ χ \to i \in (0 ..^M)$
113		elfzofz	$⊢ k \in (0 ..^M) \to k \in (0 \dots M)$
114	113	ad2antlr	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to k \in (0 \dots M)$
115	105 114	syl	$⊢ χ \to k \in (0 \dots M)$
116	107 25	syl	$⊢ χ \to V : (0 \dots M) ⟶ ℝ$
117	116 115	ffvelrnd	$⊢ χ \to V (k) \in ℝ$
118	107 1	syl	$⊢ χ \to X \in ℝ$
119	117 118	resubcld	$⊢ χ \to V (k) - X \in ℝ$
120		fveq2	$⊢ i = k \to V (i) = V (k)$
121	120	oveq1d	$⊢ i = k \to V (i) - X = V (k) - X$
122	121 9	fvmptg	$⊢ (k \in (0 \dots M) \land V (k) - X \in ℝ) \to Q (k) = V (k) - X$
123	115 119 122	syl2anc	$⊢ χ \to Q (k) = V (k) - X$
124	123 119	eqeltrd	$⊢ χ \to Q (k) \in ℝ$
125	29	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
126		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
127	126	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
128	125 127	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
129	107 112 128	syl2anc	$⊢ χ \to Q (i + 1) \in ℝ$
130		isof1o	$⊢ S {Isom}_{<, <} ((0 \dots N), T) \to S : (0 \dots N) \underset{1-1 onto}{⟶} T$
131	102 130	syl	$⊢ φ \to S : (0 \dots N) \underset{1-1 onto}{⟶} T$
132		f1of	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} T \to S : (0 \dots N) ⟶ T$
133	131 132	syl	$⊢ φ \to S : (0 \dots N) ⟶ T$
134		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
135	13 134	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
136	133 135	ffvelrnd	$⊢ φ \to S (J + 1) \in T$
137	101 136	sseldd	$⊢ φ \to S (J + 1) \in ℝ$
138	107 137	syl	$⊢ χ \to S (J + 1) \in ℝ$
139		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
140	13 139	syl	$⊢ φ \to J \in (0 \dots N)$
141	133 140	ffvelrnd	$⊢ φ \to S (J) \in T$
142	101 141	sseldd	$⊢ φ \to S (J) \in ℝ$
143	107 142	syl	$⊢ χ \to S (J) \in ℝ$
144	105	simprd	$⊢ χ \to (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))$
145	124	rexrd	$⊢ χ \to Q (k) \in ℝ^{*}$
146	29	adantr	$⊢ (φ \land k \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
147		fzofzp1	$⊢ k \in (0 ..^M) \to k + 1 \in (0 \dots M)$
148	147	adantl	$⊢ (φ \land k \in (0 ..^M)) \to k + 1 \in (0 \dots M)$
149	146 148	ffvelrnd	$⊢ (φ \land k \in (0 ..^M)) \to Q (k + 1) \in ℝ$
150	149	rexrd	$⊢ (φ \land k \in (0 ..^M)) \to Q (k + 1) \in ℝ^{*}$
151	110 150	syl	$⊢ χ \to Q (k + 1) \in ℝ^{*}$
152	143	rexrd	$⊢ χ \to S (J) \in ℝ^{*}$
153	138	rexrd	$⊢ χ \to S (J + 1) \in ℝ^{*}$
154		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
155	154	zred	$⊢ J \in (0 ..^N) \to J \in ℝ$
156	155	ltp1d	$⊢ J \in (0 ..^N) \to J < J + 1$
157	13 156	syl	$⊢ φ \to J < J + 1$
158		isoeq5	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B)) \to (S {Isom}_{<, <} ((0 \dots N), T) \leftrightarrow S {Isom}_{<, <} ((0 \dots N), \{A, B\} \cup (ran Q \cap (A, B))))$
159	10 158	ax-mp	$⊢ S {Isom}_{<, <} ((0 \dots N), T) \leftrightarrow S {Isom}_{<, <} ((0 \dots N), \{A, B\} \cup (ran Q \cap (A, B)))$
160	102 159	sylib	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), \{A, B\} \cup (ran Q \cap (A, B)))$
161		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), \{A, B\} \cup (ran Q \cap (A, B))) \land (J \in (0 \dots N) \land J + 1 \in (0 \dots N))) \to (J < J + 1 \leftrightarrow S (J) < S (J + 1))$
162	160 140 135 161	syl12anc	$⊢ φ \to (J < J + 1 \leftrightarrow S (J) < S (J + 1))$
163	157 162	mpbid	$⊢ φ \to S (J) < S (J + 1)$
164	107 163	syl	$⊢ χ \to S (J) < S (J + 1)$
165	145 151 152 153 164	ioossioobi	$⊢ χ \to ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow (Q (k) \leq S (J) \land S (J + 1) \leq Q (k + 1)))$
166	144 165	mpbid	$⊢ χ \to (Q (k) \leq S (J) \land S (J + 1) \leq Q (k + 1))$
167	166	simpld	$⊢ χ \to Q (k) \leq S (J)$
168	124 143 138 167 164	lelttrd	$⊢ χ \to Q (k) < S (J + 1)$
169		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
170	169	ad2antlr	$⊢ ((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \to i \in (0 \dots M)$
171	170	ad2antrr	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to i \in (0 \dots M)$
172	105 171	syl	$⊢ χ \to i \in (0 \dots M)$
173	107 172 28	syl2anc	$⊢ χ \to V (i) - X \in ℝ$
174	9	fvmpt2	$⊢ (i \in (0 \dots M) \land V (i) - X \in ℝ) \to Q (i) = V (i) - X$
175	172 173 174	syl2anc	$⊢ χ \to Q (i) = V (i) - X$
176	175 173	eqeltrd	$⊢ χ \to Q (i) \in ℝ$
177		simpllr	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
178	105 177	syl	$⊢ χ \to (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
179	176 129 143 138 164 178	fourierdlem10	$⊢ χ \to (Q (i) \leq S (J) \land S (J + 1) \leq Q (i + 1))$
180	179	simprd	$⊢ χ \to S (J + 1) \leq Q (i + 1)$
181	124 138 129 168 180	ltletrd	$⊢ χ \to Q (k) < Q (i + 1)$
182	124 129 118 181	ltadd2dd	$⊢ χ \to X + Q (k) < X + Q (i + 1)$
183	123	oveq2d	$⊢ χ \to X + Q (k) = X + V (k) - X$
184	107 52	syl	$⊢ χ \to X \in ℂ$
185	117	recnd	$⊢ χ \to V (k) \in ℂ$
186	184 185	pncan3d	$⊢ χ \to X + V (k) - X = V (k)$
187	183 186	eqtr2d	$⊢ χ \to V (k) = X + Q (k)$
188	112 126	syl	$⊢ χ \to i + 1 \in (0 \dots M)$
189	25	adantr	$⊢ (φ \land i \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
190	189 127	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to V (i + 1) \in ℝ$
191	107 112 190	syl2anc	$⊢ χ \to V (i + 1) \in ℝ$
192	191 118	resubcld	$⊢ χ \to V (i + 1) - X \in ℝ$
193	188 192	jca	$⊢ χ \to (i + 1 \in (0 \dots M) \land V (i + 1) - X \in ℝ)$
194		eleq1	$⊢ k = i + 1 \to (k \in (0 \dots M) \leftrightarrow i + 1 \in (0 \dots M))$
195		fveq2	$⊢ k = i + 1 \to V (k) = V (i + 1)$
196	195	oveq1d	$⊢ k = i + 1 \to V (k) - X = V (i + 1) - X$
197	196	eleq1d	$⊢ k = i + 1 \to (V (k) - X \in ℝ \leftrightarrow V (i + 1) - X \in ℝ)$
198	194 197	anbi12d	$⊢ k = i + 1 \to ((k \in (0 \dots M) \land V (k) - X \in ℝ) \leftrightarrow (i + 1 \in (0 \dots M) \land V (i + 1) - X \in ℝ))$
199		fveq2	$⊢ k = i + 1 \to Q (k) = Q (i + 1)$
200	199 196	eqeq12d	$⊢ k = i + 1 \to (Q (k) = V (k) - X \leftrightarrow Q (i + 1) = V (i + 1) - X)$
201	198 200	imbi12d	$⊢ k = i + 1 \to (((k \in (0 \dots M) \land V (k) - X \in ℝ) \to Q (k) = V (k) - X) \leftrightarrow ((i + 1 \in (0 \dots M) \land V (i + 1) - X \in ℝ) \to Q (i + 1) = V (i + 1) - X))$
202	201 122	vtoclg	$⊢ i + 1 \in (0 \dots M) \to ((i + 1 \in (0 \dots M) \land V (i + 1) - X \in ℝ) \to Q (i + 1) = V (i + 1) - X)$
203	188 193 202	sylc	$⊢ χ \to Q (i + 1) = V (i + 1) - X$
204	203	oveq2d	$⊢ χ \to X + Q (i + 1) = X + V (i + 1) - X$
205	191	recnd	$⊢ χ \to V (i + 1) \in ℂ$
206	184 205	pncan3d	$⊢ χ \to X + V (i + 1) - X = V (i + 1)$
207	204 206	eqtr2d	$⊢ χ \to V (i + 1) = X + Q (i + 1)$
208	182 187 207	3brtr4d	$⊢ χ \to V (k) < V (i + 1)$
209		eleq1w	$⊢ l = i \to (l \in (0 ..^M) \leftrightarrow i \in (0 ..^M))$
210	209	anbi2d	$⊢ l = i \to (((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \leftrightarrow ((φ \land k \in (0 ..^M)) \land i \in (0 ..^M)))$
211		oveq1	$⊢ l = i \to l + 1 = i + 1$
212	211	fveq2d	$⊢ l = i \to V (l + 1) = V (i + 1)$
213	212	breq2d	$⊢ l = i \to (V (k) < V (l + 1) \leftrightarrow V (k) < V (i + 1))$
214	210 213	anbi12d	$⊢ l = i \to ((((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)) \leftrightarrow (((φ \land k \in (0 ..^M)) \land i \in (0 ..^M)) \land V (k) < V (i + 1)))$
215		fveq2	$⊢ l = i \to V (l) = V (i)$
216	215	breq2d	$⊢ l = i \to (V (k) \leq V (l) \leftrightarrow V (k) \leq V (i))$
217	214 216	imbi12d	$⊢ l = i \to (((((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)) \to V (k) \leq V (l)) \leftrightarrow ((((φ \land k \in (0 ..^M)) \land i \in (0 ..^M)) \land V (k) < V (i + 1)) \to V (k) \leq V (i)))$
218		eleq1w	$⊢ h = k \to (h \in (0 ..^M) \leftrightarrow k \in (0 ..^M))$
219	218	anbi2d	$⊢ h = k \to ((φ \land h \in (0 ..^M)) \leftrightarrow (φ \land k \in (0 ..^M)))$
220	219	anbi1d	$⊢ h = k \to (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \leftrightarrow ((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)))$
221		fveq2	$⊢ h = k \to V (h) = V (k)$
222	221	breq1d	$⊢ h = k \to (V (h) < V (l + 1) \leftrightarrow V (k) < V (l + 1))$
223	220 222	anbi12d	$⊢ h = k \to ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \leftrightarrow (((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)))$
224	221	breq1d	$⊢ h = k \to (V (h) \leq V (l) \leftrightarrow V (k) \leq V (l))$
225	223 224	imbi12d	$⊢ h = k \to (((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to V (h) \leq V (l)) \leftrightarrow ((((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)) \to V (k) \leq V (l)))$
226		elfzoelz	$⊢ h \in (0 ..^M) \to h \in ℤ$
227	226	ad3antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to h \in ℤ$
228		elfzoelz	$⊢ l \in (0 ..^M) \to l \in ℤ$
229	228	ad2antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to l \in ℤ$
230		simplr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land \neg h < l + 1) \to V (h) < V (l + 1)$
231	25	adantr	$⊢ (φ \land l \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
232		fzofzp1	$⊢ l \in (0 ..^M) \to l + 1 \in (0 \dots M)$
233	232	adantl	$⊢ (φ \land l \in (0 ..^M)) \to l + 1 \in (0 \dots M)$
234	231 233	ffvelrnd	$⊢ (φ \land l \in (0 ..^M)) \to V (l + 1) \in ℝ$
235	234	adantlr	$⊢ ((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \to V (l + 1) \in ℝ$
236	235	adantr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to V (l + 1) \in ℝ$
237	25	adantr	$⊢ (φ \land h \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
238		elfzofz	$⊢ h \in (0 ..^M) \to h \in (0 \dots M)$
239	238	adantl	$⊢ (φ \land h \in (0 ..^M)) \to h \in (0 \dots M)$
240	237 239	ffvelrnd	$⊢ (φ \land h \in (0 ..^M)) \to V (h) \in ℝ$
241	240	ad2antrr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to V (h) \in ℝ$
242	228	zred	$⊢ l \in (0 ..^M) \to l \in ℝ$
243		peano2re	$⊢ l \in ℝ \to l + 1 \in ℝ$
244	242 243	syl	$⊢ l \in (0 ..^M) \to l + 1 \in ℝ$
245	244	ad2antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to l + 1 \in ℝ$
246	226	zred	$⊢ h \in (0 ..^M) \to h \in ℝ$
247	246	ad3antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to h \in ℝ$
248		simpr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to \neg h < l + 1$
249	245 247 248	nltled	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to l + 1 \leq h$
250	228	peano2zd	$⊢ l \in (0 ..^M) \to l + 1 \in ℤ$
251	250	ad2antlr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land l + 1 \leq h) \to l + 1 \in ℤ$
252	226	ad2antrr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land l + 1 \leq h) \to h \in ℤ$
253		simpr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land l + 1 \leq h) \to l + 1 \leq h$
254		eluz2	$⊢ h \in ℤ_{\geq (l + 1)} \leftrightarrow (l + 1 \in ℤ \land h \in ℤ \land l + 1 \leq h)$
255	251 252 253 254	syl3anbrc	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land l + 1 \leq h) \to h \in ℤ_{\geq (l + 1)}$
256	255	adantlll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land l + 1 \leq h) \to h \in ℤ_{\geq (l + 1)}$
257		simplll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to φ$
258		0zd	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to 0 \in ℤ$
259		elfzoel2	$⊢ h \in (0 ..^M) \to M \in ℤ$
260	259	ad2antrr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to M \in ℤ$
261		elfzelz	$⊢ i \in (l + 1 \dots h) \to i \in ℤ$
262	261	adantl	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \in ℤ$
263		0red	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \in ℝ$
264	261	zred	$⊢ i \in (l + 1 \dots h) \to i \in ℝ$
265	264	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \in ℝ$
266	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l \in ℝ$
267		elfzole1	$⊢ l \in (0 ..^M) \to 0 \leq l$
268	267	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \leq l$
269	266 243	syl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l + 1 \in ℝ$
270	266	ltp1d	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l < l + 1$
271		elfzle1	$⊢ i \in (l + 1 \dots h) \to l + 1 \leq i$
272	271	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l + 1 \leq i$
273	266 269 265 270 272	ltletrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l < i$
274	263 266 265 268 273	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 < i$
275	263 265 274	ltled	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \leq i$
276	275	adantll	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to 0 \leq i$
277	264	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \in ℝ$
278	259	zred	$⊢ h \in (0 ..^M) \to M \in ℝ$
279	278	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to M \in ℝ$
280	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to h \in ℝ$
281		elfzle2	$⊢ i \in (l + 1 \dots h) \to i \leq h$
282	281	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \leq h$
283		elfzolt2	$⊢ h \in (0 ..^M) \to h < M$
284	283	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to h < M$
285	277 280 279 282 284	lelttrd	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i < M$
286	277 279 285	ltled	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \leq M$
287	286	adantlr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \leq M$
288	258 260 262 276 287	elfzd	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \in (0 \dots M)$
289	288	adantlll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \in (0 \dots M)$
290	257 289 26	syl2anc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to V (i) \in ℝ$
291	290	adantlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land l + 1 \leq h) \land i \in (l + 1 \dots h)) \to V (i) \in ℝ$
292		simplll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to φ$
293		0zd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \in ℤ$
294		elfzelz	$⊢ i \in (l + 1 \dots h - 1) \to i \in ℤ$
295	294	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ$
296		0red	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \in ℝ$
297	295	zred	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℝ$
298	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l \in ℝ$
299	267	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \leq l$
300	298 243	syl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l + 1 \in ℝ$
301	298	ltp1d	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l < l + 1$
302		elfzle1	$⊢ i \in (l + 1 \dots h - 1) \to l + 1 \leq i$
303	302	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l + 1 \leq i$
304	298 300 297 301 303	ltletrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l < i$
305	296 298 297 299 304	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 < i$
306	296 297 305	ltled	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \leq i$
307		eluz2	$⊢ i \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land i \in ℤ \land 0 \leq i)$
308	293 295 306 307	syl3anbrc	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ_{\geq 0}$
309	308	adantll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ_{\geq 0}$
310		elfzoel2	$⊢ l \in (0 ..^M) \to M \in ℤ$
311	310	ad2antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to M \in ℤ$
312	294	zred	$⊢ i \in (l + 1 \dots h - 1) \to i \in ℝ$
313	312	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℝ$
314		peano2rem	$⊢ h \in ℝ \to h - 1 \in ℝ$
315	246 314	syl	$⊢ h \in (0 ..^M) \to h - 1 \in ℝ$
316	315	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to h - 1 \in ℝ$
317	278	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to M \in ℝ$
318		elfzle2	$⊢ i \in (l + 1 \dots h - 1) \to i \leq h - 1$
319	318	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \leq h - 1$
320	246	ltm1d	$⊢ h \in (0 ..^M) \to h - 1 < h$
321	315 246 278 320 283	lttrd	$⊢ h \in (0 ..^M) \to h - 1 < M$
322	321	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to h - 1 < M$
323	313 316 317 319 322	lelttrd	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i < M$
324	323	adantll	$⊢ ((φ \land h \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i < M$
325	324	adantlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i < M$
326		elfzo2	$⊢ i \in (0 ..^M) \leftrightarrow (i \in ℤ_{\geq 0} \land M \in ℤ \land i < M)$
327	309 311 325 326	syl3anbrc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i \in (0 ..^M)$
328	169 26	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
329	47	simprd	$⊢ φ \to \forall i \in (0 ..^M) V (i) < V (i + 1)$
330	329	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to V (i) < V (i + 1)$
331	328 190 330	ltled	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \leq V (i + 1)$
332	292 327 331	syl2anc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to V (i) \leq V (i + 1)$
333	332	adantlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land l + 1 \leq h) \land i \in (l + 1 \dots h - 1)) \to V (i) \leq V (i + 1)$
334	256 291 333	monoord	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land l + 1 \leq h) \to V (l + 1) \leq V (h)$
335	249 334	syldan	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to V (l + 1) \leq V (h)$
336	236 241 335	lensymd	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to \neg V (h) < V (l + 1)$
337	336	adantlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land \neg h < l + 1) \to \neg V (h) < V (l + 1)$
338	230 337	condan	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to h < l + 1$
339		zleltp1	$⊢ (h \in ℤ \land l \in ℤ) \to (h \leq l \leftrightarrow h < l + 1)$
340	227 229 339	syl2anc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to (h \leq l \leftrightarrow h < l + 1)$
341	338 340	mpbird	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to h \leq l$
342		eluz2	$⊢ l \in ℤ_{\geq h} \leftrightarrow (h \in ℤ \land l \in ℤ \land h \leq l)$
343	227 229 341 342	syl3anbrc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to l \in ℤ_{\geq h}$
344	25	ad3antrrr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to V : (0 \dots M) ⟶ ℝ$
345		0zd	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to 0 \in ℤ$
346	259	ad2antrr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to M \in ℤ$
347		elfzelz	$⊢ i \in (h \dots l) \to i \in ℤ$
348	347	adantl	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in ℤ$
349		0red	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \in ℝ$
350	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to h \in ℝ$
351	347	zred	$⊢ i \in (h \dots l) \to i \in ℝ$
352	351	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to i \in ℝ$
353		elfzole1	$⊢ h \in (0 ..^M) \to 0 \leq h$
354	353	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \leq h$
355		elfzle1	$⊢ i \in (h \dots l) \to h \leq i$
356	355	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to h \leq i$
357	349 350 352 354 356	letrd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \leq i$
358	357	adantlr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to 0 \leq i$
359	351	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \in ℝ$
360	310	zred	$⊢ l \in (0 ..^M) \to M \in ℝ$
361	360	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to M \in ℝ$
362	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to l \in ℝ$
363		elfzle2	$⊢ i \in (h \dots l) \to i \leq l$
364	363	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \leq l$
365		elfzolt2	$⊢ l \in (0 ..^M) \to l < M$
366	365	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to l < M$
367	359 362 361 364 366	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i < M$
368	359 361 367	ltled	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \leq M$
369	368	adantll	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \leq M$
370	345 346 348 358 369	elfzd	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in (0 \dots M)$
371	370	adantlll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in (0 \dots M)$
372	344 371	ffvelrnd	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to V (i) \in ℝ$
373	372	adantlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l)) \to V (i) \in ℝ$
374		simp-4l	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to φ$
375		0zd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \in ℤ$
376		elfzelz	$⊢ i \in (h \dots l - 1) \to i \in ℤ$
377	376	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℤ$
378		0red	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \in ℝ$
379	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to h \in ℝ$
380	377	zred	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℝ$
381	353	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \leq h$
382		elfzle1	$⊢ i \in (h \dots l - 1) \to h \leq i$
383	382	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to h \leq i$
384	378 379 380 381 383	letrd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \leq i$
385	375 377 384 307	syl3anbrc	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℤ_{\geq 0}$
386	385	adantll	$⊢ ((φ \land h \in (0 ..^M)) \land i \in (h \dots l - 1)) \to i \in ℤ_{\geq 0}$
387	386	ad4ant14	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to i \in ℤ_{\geq 0}$
388	310	ad3antlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to M \in ℤ$
389	376	zred	$⊢ i \in (h \dots l - 1) \to i \in ℝ$
390	389	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℝ$
391	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to l \in ℝ$
392	360	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to M \in ℝ$
393		elfzle2	$⊢ i \in (h \dots l - 1) \to i \leq l - 1$
394	393	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \leq l - 1$
395		zltlem1	$⊢ (i \in ℤ \land l \in ℤ) \to (i < l \leftrightarrow i \leq l - 1)$
396	376 228 395	syl2anr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to (i < l \leftrightarrow i \leq l - 1)$
397	394 396	mpbird	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i < l$
398	365	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to l < M$
399	390 391 392 397 398	lttrd	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i < M$
400	399	adantll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l - 1)) \to i < M$
401	400	adantlr	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to i < M$
402	387 388 401 326	syl3anbrc	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to i \in (0 ..^M)$
403	374 402 331	syl2anc	$⊢ ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \land i \in (h \dots l - 1)) \to V (i) \leq V (i + 1)$
404	343 373 403	monoord	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to V (h) \leq V (l)$
405	225 404	chvarvv	$⊢ (((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)) \to V (k) \leq V (l)$
406	217 405	chvarvv	$⊢ (((φ \land k \in (0 ..^M)) \land i \in (0 ..^M)) \land V (k) < V (i + 1)) \to V (k) \leq V (i)$
407	110 112 208 406	syl21anc	$⊢ χ \to V (k) \leq V (i)$
408	107 112	jca	$⊢ χ \to (φ \land i \in (0 ..^M))$
409	110 149	syl	$⊢ χ \to Q (k + 1) \in ℝ$
410	179	simpld	$⊢ χ \to Q (i) \leq S (J)$
411	176 143 138 410 164	lelttrd	$⊢ χ \to Q (i) < S (J + 1)$
412	166	simprd	$⊢ χ \to S (J + 1) \leq Q (k + 1)$
413	176 138 409 411 412	ltletrd	$⊢ χ \to Q (i) < Q (k + 1)$
414	176 409 118 413	ltadd2dd	$⊢ χ \to X + Q (i) < X + Q (k + 1)$
415	175	oveq2d	$⊢ χ \to X + Q (i) = X + V (i) - X$
416	107 172 26	syl2anc	$⊢ χ \to V (i) \in ℝ$
417	416	recnd	$⊢ χ \to V (i) \in ℂ$
418	184 417	pncan3d	$⊢ χ \to X + V (i) - X = V (i)$
419	415 418	eqtr2d	$⊢ χ \to V (i) = X + Q (i)$
420	9	a1i	$⊢ (φ \land k \in (0 ..^M)) \to Q = (i \in (0 \dots M) ⟼ V (i) - X)$
421		fveq2	$⊢ i = k + 1 \to V (i) = V (k + 1)$
422	421	oveq1d	$⊢ i = k + 1 \to V (i) - X = V (k + 1) - X$
423	422	adantl	$⊢ ((φ \land k \in (0 ..^M)) \land i = k + 1) \to V (i) - X = V (k + 1) - X$
424	25	adantr	$⊢ (φ \land k \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
425	424 148	ffvelrnd	$⊢ (φ \land k \in (0 ..^M)) \to V (k + 1) \in ℝ$
426	1	adantr	$⊢ (φ \land k \in (0 ..^M)) \to X \in ℝ$
427	425 426	resubcld	$⊢ (φ \land k \in (0 ..^M)) \to V (k + 1) - X \in ℝ$
428	420 423 148 427	fvmptd	$⊢ (φ \land k \in (0 ..^M)) \to Q (k + 1) = V (k + 1) - X$
429	107 109 428	syl2anc	$⊢ χ \to Q (k + 1) = V (k + 1) - X$
430	429	oveq2d	$⊢ χ \to X + Q (k + 1) = X + V (k + 1) - X$
431	110 425	syl	$⊢ χ \to V (k + 1) \in ℝ$
432	431	recnd	$⊢ χ \to V (k + 1) \in ℂ$
433	184 432	pncan3d	$⊢ χ \to X + V (k + 1) - X = V (k + 1)$
434	430 433	eqtr2d	$⊢ χ \to V (k + 1) = X + Q (k + 1)$
435	414 419 434	3brtr4d	$⊢ χ \to V (i) < V (k + 1)$
436		eleq1w	$⊢ l = k \to (l \in (0 ..^M) \leftrightarrow k \in (0 ..^M))$
437	436	anbi2d	$⊢ l = k \to (((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \leftrightarrow ((φ \land i \in (0 ..^M)) \land k \in (0 ..^M)))$
438		oveq1	$⊢ l = k \to l + 1 = k + 1$
439	438	fveq2d	$⊢ l = k \to V (l + 1) = V (k + 1)$
440	439	breq2d	$⊢ l = k \to (V (i) < V (l + 1) \leftrightarrow V (i) < V (k + 1))$
441	437 440	anbi12d	$⊢ l = k \to ((((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)) \leftrightarrow (((φ \land i \in (0 ..^M)) \land k \in (0 ..^M)) \land V (i) < V (k + 1)))$
442		fveq2	$⊢ l = k \to V (l) = V (k)$
443	442	breq2d	$⊢ l = k \to (V (i) \leq V (l) \leftrightarrow V (i) \leq V (k))$
444	441 443	imbi12d	$⊢ l = k \to (((((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)) \to V (i) \leq V (l)) \leftrightarrow ((((φ \land i \in (0 ..^M)) \land k \in (0 ..^M)) \land V (i) < V (k + 1)) \to V (i) \leq V (k)))$
445		eleq1w	$⊢ h = i \to (h \in (0 ..^M) \leftrightarrow i \in (0 ..^M))$
446	445	anbi2d	$⊢ h = i \to ((φ \land h \in (0 ..^M)) \leftrightarrow (φ \land i \in (0 ..^M)))$
447	446	anbi1d	$⊢ h = i \to (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \leftrightarrow ((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)))$
448		fveq2	$⊢ h = i \to V (h) = V (i)$
449	448	breq1d	$⊢ h = i \to (V (h) < V (l + 1) \leftrightarrow V (i) < V (l + 1))$
450	447 449	anbi12d	$⊢ h = i \to ((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \leftrightarrow (((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)))$
451	448	breq1d	$⊢ h = i \to (V (h) \leq V (l) \leftrightarrow V (i) \leq V (l))$
452	450 451	imbi12d	$⊢ h = i \to (((((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to V (h) \leq V (l)) \leftrightarrow ((((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)) \to V (i) \leq V (l)))$
453	452 404	chvarvv	$⊢ (((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)) \to V (i) \leq V (l)$
454	444 453	chvarvv	$⊢ (((φ \land i \in (0 ..^M)) \land k \in (0 ..^M)) \land V (i) < V (k + 1)) \to V (i) \leq V (k)$
455	408 109 435 454	syl21anc	$⊢ χ \to V (i) \leq V (k)$
456	117 416	letri3d	$⊢ χ \to (V (k) = V (i) \leftrightarrow (V (k) \leq V (i) \land V (i) \leq V (k)))$
457	407 455 456	mpbir2and	$⊢ χ \to V (k) = V (i)$
458	2 3 4	fourierdlem34	$⊢ φ \to V : (0 \dots M) \underset{1-1}{⟶} ℝ$
459	107 458	syl	$⊢ χ \to V : (0 \dots M) \underset{1-1}{⟶} ℝ$
460		f1fveq	$⊢ (V : (0 \dots M) \underset{1-1}{⟶} ℝ \land (k \in (0 \dots M) \land i \in (0 \dots M))) \to (V (k) = V (i) \leftrightarrow k = i)$
461	459 115 172 460	syl12anc	$⊢ χ \to (V (k) = V (i) \leftrightarrow k = i)$
462	457 461	mpbid	$⊢ χ \to k = i$
463	15 462	sylbir	$⊢ ((((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))) \to k = i$
464	463	ex	$⊢ (((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \to ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \to k = i)$
465		simpl	$⊢ ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \land k = i) \to (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
466		fveq2	$⊢ k = i \to Q (k) = Q (i)$
467		oveq1	$⊢ k = i \to k + 1 = i + 1$
468	467	fveq2d	$⊢ k = i \to Q (k + 1) = Q (i + 1)$
469	466 468	oveq12d	$⊢ k = i \to (Q (k), Q (k + 1)) = (Q (i), Q (i + 1))$
470	469	eqcomd	$⊢ k = i \to (Q (i), Q (i + 1)) = (Q (k), Q (k + 1))$
471	470	adantl	$⊢ ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \land k = i) \to (Q (i), Q (i + 1)) = (Q (k), Q (k + 1))$
472	465 471	sseqtrd	$⊢ ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \land k = i) \to (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))$
473	472	ex	$⊢ (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \to (k = i \to (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
474	473	ad2antlr	$⊢ (((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \to (k = i \to (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
475	464 474	impbid	$⊢ (((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \land k \in (0 ..^M)) \to ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i)$
476	475	ralrimiva	$⊢ ((φ \land i \in (0 ..^M)) \land (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \to \forall k \in (0 ..^M) ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i)$
477	476	ex	$⊢ (φ \land i \in (0 ..^M)) \to ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \to \forall k \in (0 ..^M) ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i))$
478	477	reximdva	$⊢ φ \to (\exists i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \to \exists i \in (0 ..^M) \forall k \in (0 ..^M) ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i))$
479	104 478	mpd	$⊢ φ \to \exists i \in (0 ..^M) \forall k \in (0 ..^M) ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i)$
480		reu6	$⊢ \exists! k \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow \exists i \in (0 ..^M) \forall k \in (0 ..^M) ((S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)) \leftrightarrow k = i)$
481	479 480	sylibr	$⊢ φ \to \exists! k \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))$
482		fveq2	$⊢ i = k \to Q (i) = Q (k)$
483		oveq1	$⊢ i = k \to i + 1 = k + 1$
484	483	fveq2d	$⊢ i = k \to Q (i + 1) = Q (k + 1)$
485	482 484	oveq12d	$⊢ i = k \to (Q (i), Q (i + 1)) = (Q (k), Q (k + 1))$
486	485	sseq2d	$⊢ i = k \to ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \leftrightarrow (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1)))$
487	486	cbvreuvw	$⊢ \exists! i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \leftrightarrow \exists! k \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))$
488	481 487	sylibr	$⊢ φ \to \exists! i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
489		riotacl	$⊢ \exists! i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \to (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \in (0 ..^M)$
490	488 489	syl	$⊢ φ \to (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \in (0 ..^M)$
491	14 490	eqeltrid	$⊢ φ \to U \in (0 ..^M)$
492	14	eqcomi	$⊢ (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U$
493	492	a1i	$⊢ φ \to (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U$
494		fveq2	$⊢ i = U \to Q (i) = Q (U)$
495		oveq1	$⊢ i = U \to i + 1 = U + 1$
496	495	fveq2d	$⊢ i = U \to Q (i + 1) = Q (U + 1)$
497	494 496	oveq12d	$⊢ i = U \to (Q (i), Q (i + 1)) = (Q (U), Q (U + 1))$
498	497	sseq2d	$⊢ i = U \to ((S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1)) \leftrightarrow (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)))$
499	498	riota2	$⊢ (U \in (0 ..^M) \land \exists! i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \to ((S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)) \leftrightarrow (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U)$
500	491 488 499	syl2anc	$⊢ φ \to ((S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)) \leftrightarrow (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U)$
501	493 500	mpbird	$⊢ φ \to (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1))$
502	491 501	jca	$⊢ φ \to (U \in (0 ..^M) \land (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)))$

Metamath Proof Explorer

Theorem fourierdlem50

Proof