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	258 260 262	3jca	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to (0 \in ℤ \land M \in ℤ \land i \in ℤ)$
264		0red	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \in ℝ$
265	261	zred	$⊢ i \in (l + 1 \dots h) \to i \in ℝ$
266	265	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \in ℝ$
267	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l \in ℝ$
268		elfzole1	$⊢ l \in (0 ..^M) \to 0 \leq l$
269	268	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \leq l$
270	267 243	syl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l + 1 \in ℝ$
271	267	ltp1d	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l < l + 1$
272		elfzle1	$⊢ i \in (l + 1 \dots h) \to l + 1 \leq i$
273	272	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l + 1 \leq i$
274	267 270 266 271 273	ltletrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to l < i$
275	264 267 266 269 274	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 < i$
276	264 266 275	ltled	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h)) \to 0 \leq i$
277	276	adantll	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to 0 \leq i$
278	265	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \in ℝ$
279	259	zred	$⊢ h \in (0 ..^M) \to M \in ℝ$
280	279	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to M \in ℝ$
281	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to h \in ℝ$
282		elfzle2	$⊢ i \in (l + 1 \dots h) \to i \leq h$
283	282	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \leq h$
284		elfzolt2	$⊢ h \in (0 ..^M) \to h < M$
285	284	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to h < M$
286	278 281 280 283 285	lelttrd	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i < M$
287	278 280 286	ltled	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h)) \to i \leq M$
288	287	adantlr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \leq M$
289	263 277 288	jca32	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to ((0 \in ℤ \land M \in ℤ \land i \in ℤ) \land (0 \leq i \land i \leq M))$
290		elfz2	$⊢ i \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land i \in ℤ) \land (0 \leq i \land i \leq M))$
291	289 290	sylibr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \in (0 \dots M)$
292	291	adantlll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to i \in (0 \dots M)$
293	257 292 26	syl2anc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h)) \to V (i) \in ℝ$
294	293	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 ℝ$
295		simplll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to φ$
296		0zd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \in ℤ$
297		elfzelz	$⊢ i \in (l + 1 \dots h - 1) \to i \in ℤ$
298	297	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ$
299		0red	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \in ℝ$
300	298	zred	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℝ$
301	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l \in ℝ$
302	268	adantr	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \leq l$
303	301 243	syl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l + 1 \in ℝ$
304	301	ltp1d	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l < l + 1$
305		elfzle1	$⊢ i \in (l + 1 \dots h - 1) \to l + 1 \leq i$
306	305	adantl	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l + 1 \leq i$
307	301 303 300 304 306	ltletrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to l < i$
308	299 301 300 302 307	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 < i$
309	299 300 308	ltled	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to 0 \leq i$
310		eluz2	$⊢ i \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land i \in ℤ \land 0 \leq i)$
311	296 298 309 310	syl3anbrc	$⊢ (l \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ_{\geq 0}$
312	311	adantll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i \in ℤ_{\geq 0}$
313		elfzoel2	$⊢ l \in (0 ..^M) \to M \in ℤ$
314	313	ad2antlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to M \in ℤ$
315	297	zred	$⊢ i \in (l + 1 \dots h - 1) \to i \in ℝ$
316	315	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \in ℝ$
317		peano2rem	$⊢ h \in ℝ \to h - 1 \in ℝ$
318	246 317	syl	$⊢ h \in (0 ..^M) \to h - 1 \in ℝ$
319	318	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to h - 1 \in ℝ$
320	279	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to M \in ℝ$
321		elfzle2	$⊢ i \in (l + 1 \dots h - 1) \to i \leq h - 1$
322	321	adantl	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i \leq h - 1$
323	246	ltm1d	$⊢ h \in (0 ..^M) \to h - 1 < h$
324	318 246 279 323 284	lttrd	$⊢ h \in (0 ..^M) \to h - 1 < M$
325	324	adantr	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to h - 1 < M$
326	316 319 320 322 325	lelttrd	$⊢ (h \in (0 ..^M) \land i \in (l + 1 \dots h - 1)) \to i < M$
327	326	adantll	$⊢ ((φ \land h \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i < M$
328	327	adantlr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i < M$
329		elfzo2	$⊢ i \in (0 ..^M) \leftrightarrow (i \in ℤ_{\geq 0} \land M \in ℤ \land i < M)$
330	312 314 328 329	syl3anbrc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (l + 1 \dots h - 1)) \to i \in (0 ..^M)$
331	169 26	sylan2	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \in ℝ$
332	47	simprd	$⊢ φ \to \forall i \in (0 ..^M) V (i) < V (i + 1)$
333	332	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to V (i) < V (i + 1)$
334	331 190 333	ltled	$⊢ (φ \land i \in (0 ..^M)) \to V (i) \leq V (i + 1)$
335	295 330 334	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)$
336	335	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)$
337	256 294 336	monoord	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land l + 1 \leq h) \to V (l + 1) \leq V (h)$
338	249 337	syldan	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to V (l + 1) \leq V (h)$
339	236 241 338	lensymd	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land \neg h < l + 1) \to \neg V (h) < V (l + 1)$
340	339	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)$
341	230 340	condan	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to h < l + 1$
342		zleltp1	$⊢ (h \in ℤ \land l \in ℤ) \to (h \leq l \leftrightarrow h < l + 1)$
343	227 229 342	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)$
344	341 343	mpbird	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to h \leq l$
345		eluz2	$⊢ l \in ℤ_{\geq h} \leftrightarrow (h \in ℤ \land l \in ℤ \land h \leq l)$
346	227 229 344 345	syl3anbrc	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to l \in ℤ_{\geq h}$
347	25	ad3antrrr	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to V : (0 \dots M) ⟶ ℝ$
348		0zd	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to 0 \in ℤ$
349	259	ad2antrr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to M \in ℤ$
350		elfzelz	$⊢ i \in (h \dots l) \to i \in ℤ$
351	350	adantl	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in ℤ$
352	348 349 351	3jca	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to (0 \in ℤ \land M \in ℤ \land i \in ℤ)$
353		0red	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \in ℝ$
354	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to h \in ℝ$
355	350	zred	$⊢ i \in (h \dots l) \to i \in ℝ$
356	355	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to i \in ℝ$
357		elfzole1	$⊢ h \in (0 ..^M) \to 0 \leq h$
358	357	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \leq h$
359		elfzle1	$⊢ i \in (h \dots l) \to h \leq i$
360	359	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to h \leq i$
361	353 354 356 358 360	letrd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l)) \to 0 \leq i$
362	361	adantlr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to 0 \leq i$
363	355	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \in ℝ$
364	313	zred	$⊢ l \in (0 ..^M) \to M \in ℝ$
365	364	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to M \in ℝ$
366	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to l \in ℝ$
367		elfzle2	$⊢ i \in (h \dots l) \to i \leq l$
368	367	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \leq l$
369		elfzolt2	$⊢ l \in (0 ..^M) \to l < M$
370	369	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to l < M$
371	363 366 365 368 370	lelttrd	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i < M$
372	363 365 371	ltled	$⊢ (l \in (0 ..^M) \land i \in (h \dots l)) \to i \leq M$
373	372	adantll	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \leq M$
374	352 362 373	jca32	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to ((0 \in ℤ \land M \in ℤ \land i \in ℤ) \land (0 \leq i \land i \leq M))$
375	374 290	sylibr	$⊢ ((h \in (0 ..^M) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in (0 \dots M)$
376	375	adantlll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to i \in (0 \dots M)$
377	347 376	ffvelrnd	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l)) \to V (i) \in ℝ$
378	377	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 ℝ$
379		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 φ$
380		0zd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \in ℤ$
381		elfzelz	$⊢ i \in (h \dots l - 1) \to i \in ℤ$
382	381	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℤ$
383		0red	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \in ℝ$
384	246	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to h \in ℝ$
385	382	zred	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℝ$
386	357	adantr	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \leq h$
387		elfzle1	$⊢ i \in (h \dots l - 1) \to h \leq i$
388	387	adantl	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to h \leq i$
389	383 384 385 386 388	letrd	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to 0 \leq i$
390	380 382 389 310	syl3anbrc	$⊢ (h \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℤ_{\geq 0}$
391	390	adantll	$⊢ ((φ \land h \in (0 ..^M)) \land i \in (h \dots l - 1)) \to i \in ℤ_{\geq 0}$
392	391	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}$
393	313	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 ℤ$
394	381	zred	$⊢ i \in (h \dots l - 1) \to i \in ℝ$
395	394	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \in ℝ$
396	242	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to l \in ℝ$
397	364	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to M \in ℝ$
398		elfzle2	$⊢ i \in (h \dots l - 1) \to i \leq l - 1$
399	398	adantl	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i \leq l - 1$
400		zltlem1	$⊢ (i \in ℤ \land l \in ℤ) \to (i < l \leftrightarrow i \leq l - 1)$
401	381 228 400	syl2anr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to (i < l \leftrightarrow i \leq l - 1)$
402	399 401	mpbird	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i < l$
403	369	adantr	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to l < M$
404	395 396 397 402 403	lttrd	$⊢ (l \in (0 ..^M) \land i \in (h \dots l - 1)) \to i < M$
405	404	adantll	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land i \in (h \dots l - 1)) \to i < M$
406	405	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$
407	392 393 406 329	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)$
408	379 407 334	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)$
409	346 378 408	monoord	$⊢ (((φ \land h \in (0 ..^M)) \land l \in (0 ..^M)) \land V (h) < V (l + 1)) \to V (h) \leq V (l)$
410	225 409	chvarvv	$⊢ (((φ \land k \in (0 ..^M)) \land l \in (0 ..^M)) \land V (k) < V (l + 1)) \to V (k) \leq V (l)$
411	217 410	chvarvv	$⊢ (((φ \land k \in (0 ..^M)) \land i \in (0 ..^M)) \land V (k) < V (i + 1)) \to V (k) \leq V (i)$
412	110 112 208 411	syl21anc	$⊢ χ \to V (k) \leq V (i)$
413	107 112	jca	$⊢ χ \to (φ \land i \in (0 ..^M))$
414	110 149	syl	$⊢ χ \to Q (k + 1) \in ℝ$
415	179	simpld	$⊢ χ \to Q (i) \leq S (J)$
416	176 143 138 415 164	lelttrd	$⊢ χ \to Q (i) < S (J + 1)$
417	166	simprd	$⊢ χ \to S (J + 1) \leq Q (k + 1)$
418	176 138 414 416 417	ltletrd	$⊢ χ \to Q (i) < Q (k + 1)$
419	176 414 118 418	ltadd2dd	$⊢ χ \to X + Q (i) < X + Q (k + 1)$
420	175	oveq2d	$⊢ χ \to X + Q (i) = X + V (i) - X$
421	107 172 26	syl2anc	$⊢ χ \to V (i) \in ℝ$
422	421	recnd	$⊢ χ \to V (i) \in ℂ$
423	184 422	pncan3d	$⊢ χ \to X + V (i) - X = V (i)$
424	420 423	eqtr2d	$⊢ χ \to V (i) = X + Q (i)$
425	9	a1i	$⊢ (φ \land k \in (0 ..^M)) \to Q = (i \in (0 \dots M) ⟼ V (i) - X)$
426		fveq2	$⊢ i = k + 1 \to V (i) = V (k + 1)$
427	426	oveq1d	$⊢ i = k + 1 \to V (i) - X = V (k + 1) - X$
428	427	adantl	$⊢ ((φ \land k \in (0 ..^M)) \land i = k + 1) \to V (i) - X = V (k + 1) - X$
429	25	adantr	$⊢ (φ \land k \in (0 ..^M)) \to V : (0 \dots M) ⟶ ℝ$
430	429 148	ffvelrnd	$⊢ (φ \land k \in (0 ..^M)) \to V (k + 1) \in ℝ$
431	1	adantr	$⊢ (φ \land k \in (0 ..^M)) \to X \in ℝ$
432	430 431	resubcld	$⊢ (φ \land k \in (0 ..^M)) \to V (k + 1) - X \in ℝ$
433	425 428 148 432	fvmptd	$⊢ (φ \land k \in (0 ..^M)) \to Q (k + 1) = V (k + 1) - X$
434	107 109 433	syl2anc	$⊢ χ \to Q (k + 1) = V (k + 1) - X$
435	434	oveq2d	$⊢ χ \to X + Q (k + 1) = X + V (k + 1) - X$
436	110 430	syl	$⊢ χ \to V (k + 1) \in ℝ$
437	436	recnd	$⊢ χ \to V (k + 1) \in ℂ$
438	184 437	pncan3d	$⊢ χ \to X + V (k + 1) - X = V (k + 1)$
439	435 438	eqtr2d	$⊢ χ \to V (k + 1) = X + Q (k + 1)$
440	419 424 439	3brtr4d	$⊢ χ \to V (i) < V (k + 1)$
441		eleq1w	$⊢ l = k \to (l \in (0 ..^M) \leftrightarrow k \in (0 ..^M))$
442	441	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)))$
443		oveq1	$⊢ l = k \to l + 1 = k + 1$
444	443	fveq2d	$⊢ l = k \to V (l + 1) = V (k + 1)$
445	444	breq2d	$⊢ l = k \to (V (i) < V (l + 1) \leftrightarrow V (i) < V (k + 1))$
446	442 445	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)))$
447		fveq2	$⊢ l = k \to V (l) = V (k)$
448	447	breq2d	$⊢ l = k \to (V (i) \leq V (l) \leftrightarrow V (i) \leq V (k))$
449	446 448	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)))$
450		eleq1w	$⊢ h = i \to (h \in (0 ..^M) \leftrightarrow i \in (0 ..^M))$
451	450	anbi2d	$⊢ h = i \to ((φ \land h \in (0 ..^M)) \leftrightarrow (φ \land i \in (0 ..^M)))$
452	451	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)))$
453		fveq2	$⊢ h = i \to V (h) = V (i)$
454	453	breq1d	$⊢ h = i \to (V (h) < V (l + 1) \leftrightarrow V (i) < V (l + 1))$
455	452 454	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)))$
456	453	breq1d	$⊢ h = i \to (V (h) \leq V (l) \leftrightarrow V (i) \leq V (l))$
457	455 456	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)))$
458	457 409	chvarvv	$⊢ (((φ \land i \in (0 ..^M)) \land l \in (0 ..^M)) \land V (i) < V (l + 1)) \to V (i) \leq V (l)$
459	449 458	chvarvv	$⊢ (((φ \land i \in (0 ..^M)) \land k \in (0 ..^M)) \land V (i) < V (k + 1)) \to V (i) \leq V (k)$
460	413 109 440 459	syl21anc	$⊢ χ \to V (i) \leq V (k)$
461	117 421	letri3d	$⊢ χ \to (V (k) = V (i) \leftrightarrow (V (k) \leq V (i) \land V (i) \leq V (k)))$
462	412 460 461	mpbir2and	$⊢ χ \to V (k) = V (i)$
463	2 3 4	fourierdlem34	$⊢ φ \to V : (0 \dots M) \underset{1-1}{⟶} ℝ$
464	107 463	syl	$⊢ χ \to V : (0 \dots M) \underset{1-1}{⟶} ℝ$
465		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)$
466	464 115 172 465	syl12anc	$⊢ χ \to (V (k) = V (i) \leftrightarrow k = i)$
467	462 466	mpbid	$⊢ χ \to k = i$
468	15 467	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$
469	468	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)$
470		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))$
471		fveq2	$⊢ k = i \to Q (k) = Q (i)$
472		oveq1	$⊢ k = i \to k + 1 = i + 1$
473	472	fveq2d	$⊢ k = i \to Q (k + 1) = Q (i + 1)$
474	471 473	oveq12d	$⊢ k = i \to (Q (k), Q (k + 1)) = (Q (i), Q (i + 1))$
475	474	eqcomd	$⊢ k = i \to (Q (i), Q (i + 1)) = (Q (k), Q (k + 1))$
476	475	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))$
477	470 476	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))$
478	477	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)))$
479	478	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)))$
480	469 479	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)$
481	480	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)$
482	481	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))$
483	482	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))$
484	104 483	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)$
485		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)$
486	484 485	sylibr	$⊢ φ \to \exists! k \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (k), Q (k + 1))$
487		fveq2	$⊢ i = k \to Q (i) = Q (k)$
488		oveq1	$⊢ i = k \to i + 1 = k + 1$
489	488	fveq2d	$⊢ i = k \to Q (i + 1) = Q (k + 1)$
490	487 489	oveq12d	$⊢ i = k \to (Q (i), Q (i + 1)) = (Q (k), Q (k + 1))$
491	490	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)))$
492	491	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))$
493	486 492	sylibr	$⊢ φ \to \exists! i \in (0 ..^M) (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))$
494		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)$
495	493 494	syl	$⊢ φ \to (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) \in (0 ..^M)$
496	14 495	eqeltrid	$⊢ φ \to U \in (0 ..^M)$
497	14	eqcomi	$⊢ (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U$
498	497	a1i	$⊢ φ \to (ι i \in (0 ..^M) \| (S (J), S (J + 1)) \subseteq (Q (i), Q (i + 1))) = U$
499		fveq2	$⊢ i = U \to Q (i) = Q (U)$
500		oveq1	$⊢ i = U \to i + 1 = U + 1$
501	500	fveq2d	$⊢ i = U \to Q (i + 1) = Q (U + 1)$
502	499 501	oveq12d	$⊢ i = U \to (Q (i), Q (i + 1)) = (Q (U), Q (U + 1))$
503	502	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)))$
504	503	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)$
505	496 493 504	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)$
506	498 505	mpbird	$⊢ φ \to (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1))$
507	496 506	jca	$⊢ φ \to (U \in (0 ..^M) \land (S (J), S (J + 1)) \subseteq (Q (U), Q (U + 1)))$

Metamath Proof Explorer

Theorem fourierdlem50

Proof