fourierdlem79

Description: E projects every interval of the partition induced by S on H into a corresponding interval of the partition induced by Q on [ A , B ] . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem79.t	$⊢ T = B - A$
	fourierdlem79.p	$⊢ 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))\})$
	fourierdlem79.m	$⊢ φ \to M \in ℕ$
	fourierdlem79.q	$⊢ φ \to Q \in P (M)$
	fourierdlem79.c	$⊢ φ \to C \in ℝ$
	fourierdlem79.d	$⊢ φ \to D \in ℝ$
	fourierdlem79.cltd	$⊢ φ \to C < D$
	fourierdlem79.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem79.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
	fourierdlem79.n	$⊢ N = \|H\| - 1$
	fourierdlem79.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem79.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem79.l	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem79.z	$⊢ Z = S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
	fourierdlem79.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
Assertion	fourierdlem79	$⊢ (φ \land j \in (0 ..^N)) \to (L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem79.t	$⊢ T = B - A$
2		fourierdlem79.p	$⊢ 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))\})$
3		fourierdlem79.m	$⊢ φ \to M \in ℕ$
4		fourierdlem79.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem79.c	$⊢ φ \to C \in ℝ$
6		fourierdlem79.d	$⊢ φ \to D \in ℝ$
7		fourierdlem79.cltd	$⊢ φ \to C < D$
8		fourierdlem79.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
9		fourierdlem79.h	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
10		fourierdlem79.n	$⊢ N = \|H\| - 1$
11		fourierdlem79.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
12		fourierdlem79.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
13		fourierdlem79.l	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
14		fourierdlem79.z	$⊢ Z = S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
15		fourierdlem79.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
16	2	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))))$
17	3 16	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))))$
18	4 17	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)))$
19	18	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
20		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
21	19 20	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
22	21	adantr	$⊢ (φ \land j \in (0 ..^N)) \to Q : (0 \dots M) ⟶ ℝ$
23	2 3 4 1 12 13 15	fourierdlem37	$⊢ φ \to (I : ℝ ⟶ (0 ..^M) \land (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}))$
24	23	simpld	$⊢ φ \to I : ℝ ⟶ (0 ..^M)$
25		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
26	25	a1i	$⊢ φ \to (0 ..^M) \subseteq (0 \dots M)$
27	24 26	fssd	$⊢ φ \to I : ℝ ⟶ (0 \dots M)$
28	27	adantr	$⊢ (φ \land j \in (0 ..^N)) \to I : ℝ ⟶ (0 \dots M)$
29	1 2 3 4 5 6 7 8 9 10 11	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$
30	29	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
31	30	simprd	$⊢ φ \to S \in O (N)$
32	31	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S \in O (N)$
33	30	simpld	$⊢ φ \to N \in ℕ$
34	33	adantr	$⊢ (φ \land j \in (0 ..^N)) \to N \in ℕ$
35	8	fourierdlem2	$⊢ N \in ℕ \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
36	34 35	syl	$⊢ (φ \land j \in (0 ..^N)) \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
37	32 36	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1)))$
38	37	simpld	$⊢ (φ \land j \in (0 ..^N)) \to S \in (ℝ^{(0 \dots N)})$
39		elmapi	$⊢ S \in (ℝ^{(0 \dots N)}) \to S : (0 \dots N) ⟶ ℝ$
40	38 39	syl	$⊢ (φ \land j \in (0 ..^N)) \to S : (0 \dots N) ⟶ ℝ$
41		elfzofz	$⊢ j \in (0 ..^N) \to j \in (0 \dots N)$
42	41	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 \dots N)$
43	40 42	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℝ$
44	28 43	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) \in (0 \dots M)$
45	22 44	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j))) \in ℝ$
46	45	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j))) \in ℝ^{*}$
47	24	adantr	$⊢ (φ \land j \in (0 ..^N)) \to I : ℝ ⟶ (0 ..^M)$
48	47 43	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) \in (0 ..^M)$
49		fzofzp1	$⊢ I (S (j)) \in (0 ..^M) \to I (S (j)) + 1 \in (0 \dots M)$
50	48 49	syl	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) + 1 \in (0 \dots M)$
51	22 50	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j)) + 1) \in ℝ$
52	51	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j)) + 1) \in ℝ^{*}$
53	15	a1i	$⊢ (φ \land j \in (0 ..^N)) \to I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
54		fveq2	$⊢ x = S (j) \to E (x) = E (S (j))$
55	54	fveq2d	$⊢ x = S (j) \to L (E (x)) = L (E (S (j)))$
56	55	breq2d	$⊢ x = S (j) \to (Q (i) \leq L (E (x)) \leftrightarrow Q (i) \leq L (E (S (j))))$
57	56	rabbidv	$⊢ x = S (j) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} = \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}$
58	57	supeq1d	$⊢ x = S (j) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
59	58	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land x = S (j)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
60		ltso	$⊢ < Or ℝ$
61	60	supex	$⊢ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in V$
62	61	a1i	$⊢ (φ \land j \in (0 ..^N)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in V$
63	53 59 43 62	fvmptd	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
64	63	fveq2d	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j))) = Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <))$
65		simpl	$⊢ (φ \land j \in (0 ..^N)) \to φ$
66	65 43	jca	$⊢ (φ \land j \in (0 ..^N)) \to (φ \land S (j) \in ℝ)$
67		eleq1	$⊢ x = S (j) \to (x \in ℝ \leftrightarrow S (j) \in ℝ)$
68	67	anbi2d	$⊢ x = S (j) \to ((φ \land x \in ℝ) \leftrightarrow (φ \land S (j) \in ℝ))$
69	58 57	eleq12d	$⊢ x = S (j) \to (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \leftrightarrow sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\})$
70	68 69	imbi12d	$⊢ x = S (j) \to (((φ \land x \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}) \leftrightarrow ((φ \land S (j) \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}))$
71	23	simprd	$⊢ φ \to (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\})$
72	71	imp	$⊢ (φ \land x \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}$
73	70 72	vtoclg	$⊢ S (j) \in ℝ \to ((φ \land S (j) \in ℝ) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\})$
74	43 66 73	sylc	$⊢ (φ \land j \in (0 ..^N)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}$
75		nfrab1	$⊢ \underline{Ⅎ} i \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}$
76		nfcv	$⊢ \underline{Ⅎ} i ℝ$
77		nfcv	$⊢ \underline{Ⅎ} i <$
78	75 76 77	nfsup	$⊢ \underline{Ⅎ} i sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
79		nfcv	$⊢ \underline{Ⅎ} i (0 ..^M)$
80		nfcv	$⊢ \underline{Ⅎ} i Q$
81	80 78	nffv	$⊢ \underline{Ⅎ} i Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <))$
82		nfcv	$⊢ \underline{Ⅎ} i \leq$
83		nfcv	$⊢ \underline{Ⅎ} i L (E (S (j)))$
84	81 82 83	nfbr	$⊢ Ⅎ i Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)) \leq L (E (S (j)))$
85		fveq2	$⊢ i = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \to Q (i) = Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <))$
86	85	breq1d	$⊢ i = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \to (Q (i) \leq L (E (S (j))) \leftrightarrow Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)) \leq L (E (S (j))))$
87	78 79 84 86	elrabf	$⊢ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \leftrightarrow (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in (0 ..^M) \land Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)) \leq L (E (S (j))))$
88	74 87	sylib	$⊢ (φ \land j \in (0 ..^N)) \to (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in (0 ..^M) \land Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)) \leq L (E (S (j))))$
89	88	simprd	$⊢ (φ \land j \in (0 ..^N)) \to Q (sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)) \leq L (E (S (j)))$
90	64 89	eqbrtrd	$⊢ (φ \land j \in (0 ..^N)) \to Q (I (S (j))) \leq L (E (S (j)))$
91	3	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to M \in ℕ$
92	4	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to Q \in P (M)$
93	5	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to C \in ℝ$
94	6	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to D \in ℝ$
95	7	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to C < D$
96		0zd	$⊢ φ \to 0 \in ℤ$
97	3	nnzd	$⊢ φ \to M \in ℤ$
98		1zzd	$⊢ φ \to 1 \in ℤ$
99		0le1	$⊢ 0 \leq 1$
100	99	a1i	$⊢ φ \to 0 \leq 1$
101	3	nnge1d	$⊢ φ \to 1 \leq M$
102	96 97 98 100 101	elfzd	$⊢ φ \to 1 \in (0 \dots M)$
103	102	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to 1 \in (0 \dots M)$
104		simplr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to j \in (0 ..^N)$
105		fzofzp1	$⊢ j \in (0 ..^N) \to j + 1 \in (0 \dots N)$
106	105	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j + 1 \in (0 \dots N)$
107	40 106	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℝ$
108	107 43	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) - S (j) \in ℝ$
109	108	rehalfcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j + 1) - S (j)}{2} \in ℝ$
110	21 102	ffvelcdmd	$⊢ φ \to Q (1) \in ℝ$
111	2 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
112	111	simp1d	$⊢ φ \to A \in ℝ$
113	110 112	resubcld	$⊢ φ \to Q (1) - A \in ℝ$
114	113	rehalfcld	$⊢ φ \to \frac{Q (1) - A}{2} \in ℝ$
115	114	adantr	$⊢ (φ \land j \in (0 ..^N)) \to \frac{Q (1) - A}{2} \in ℝ$
116	109 115	ifcld	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \in ℝ$
117	43 116	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \in ℝ$
118	14 117	eqeltrid	$⊢ (φ \land j \in (0 ..^N)) \to Z \in ℝ$
119		2re	$⊢ 2 \in ℝ$
120	119	a1i	$⊢ (φ \land j \in (0 ..^N)) \to 2 \in ℝ$
121		elfzoelz	$⊢ j \in (0 ..^N) \to j \in ℤ$
122	121	zred	$⊢ j \in (0 ..^N) \to j \in ℝ$
123	122	ltp1d	$⊢ j \in (0 ..^N) \to j < j + 1$
124	123	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j < j + 1$
125	29	simprd	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), H)$
126	125	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S {Isom}_{<, <} ((0 \dots N), H)$
127		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), H) \land (j \in (0 \dots N) \land j + 1 \in (0 \dots N))) \to (j < j + 1 \leftrightarrow S (j) < S (j + 1))$
128	126 42 106 127	syl12anc	$⊢ (φ \land j \in (0 ..^N)) \to (j < j + 1 \leftrightarrow S (j) < S (j + 1))$
129	124 128	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j + 1)$
130	43 107	posdifd	$⊢ (φ \land j \in (0 ..^N)) \to (S (j) < S (j + 1) \leftrightarrow 0 < S (j + 1) - S (j))$
131	129 130	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to 0 < S (j + 1) - S (j)$
132		2pos	$⊢ 0 < 2$
133	132	a1i	$⊢ (φ \land j \in (0 ..^N)) \to 0 < 2$
134	108 120 131 133	divgt0d	$⊢ (φ \land j \in (0 ..^N)) \to 0 < \frac{S (j + 1) - S (j)}{2}$
135	109 134	elrpd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j + 1) - S (j)}{2} \in ℝ^{+}$
136	119	a1i	$⊢ φ \to 2 \in ℝ$
137	3	nngt0d	$⊢ φ \to 0 < M$
138		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
139	96 97 137 138	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
140		0re	$⊢ 0 \in ℝ$
141		eleq1	$⊢ i = 0 \to (i \in (0 ..^M) \leftrightarrow 0 \in (0 ..^M))$
142	141	anbi2d	$⊢ i = 0 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land 0 \in (0 ..^M)))$
143		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
144		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
145	144	fveq2d	$⊢ i = 0 \to Q (i + 1) = Q (0 + 1)$
146	143 145	breq12d	$⊢ i = 0 \to (Q (i) < Q (i + 1) \leftrightarrow Q (0) < Q (0 + 1))$
147	142 146	imbi12d	$⊢ i = 0 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)))$
148	18	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
149	148	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
150	149	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
151	147 150	vtoclg	$⊢ 0 \in ℝ \to ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1))$
152	140 151	ax-mp	$⊢ (φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)$
153	139 152	mpdan	$⊢ φ \to Q (0) < Q (0 + 1)$
154	148	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
155	154	simpld	$⊢ φ \to Q (0) = A$
156		0p1e1	$⊢ 0 + 1 = 1$
157	156	fveq2i	$⊢ Q (0 + 1) = Q (1)$
158	157	a1i	$⊢ φ \to Q (0 + 1) = Q (1)$
159	153 155 158	3brtr3d	$⊢ φ \to A < Q (1)$
160	112 110	posdifd	$⊢ φ \to (A < Q (1) \leftrightarrow 0 < Q (1) - A)$
161	159 160	mpbid	$⊢ φ \to 0 < Q (1) - A$
162	132	a1i	$⊢ φ \to 0 < 2$
163	113 136 161 162	divgt0d	$⊢ φ \to 0 < \frac{Q (1) - A}{2}$
164	114 163	elrpd	$⊢ φ \to \frac{Q (1) - A}{2} \in ℝ^{+}$
165	164	adantr	$⊢ (φ \land j \in (0 ..^N)) \to \frac{Q (1) - A}{2} \in ℝ^{+}$
166	135 165	ifcld	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \in ℝ^{+}$
167	43 166	ltaddrpd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
168	43 117 167	ltled	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
169	168 14	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq Z$
170	43 109	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + (\frac{S (j + 1) - S (j)}{2}) \in ℝ$
171		iftrue	$⊢ S (j + 1) - S (j) < Q (1) - A \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = \frac{S (j + 1) - S (j)}{2}$
172	171	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = \frac{S (j + 1) - S (j)}{2}$
173	109	leidd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j + 1) - S (j)}{2} \leq \frac{S (j + 1) - S (j)}{2}$
174	173	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to \frac{S (j + 1) - S (j)}{2} \leq \frac{S (j + 1) - S (j)}{2}$
175	172 174	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{S (j + 1) - S (j)}{2}$
176		iffalse	$⊢ \neg S (j + 1) - S (j) < Q (1) - A \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = \frac{Q (1) - A}{2}$
177	176	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = \frac{Q (1) - A}{2}$
178	113	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to Q (1) - A \in ℝ$
179	108	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to S (j + 1) - S (j) \in ℝ$
180		2rp	$⊢ 2 \in ℝ^{+}$
181	180	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to 2 \in ℝ^{+}$
182		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to \neg S (j + 1) - S (j) < Q (1) - A$
183	178 179 182	nltled	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to Q (1) - A \leq S (j + 1) - S (j)$
184	178 179 181 183	lediv1dd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to \frac{Q (1) - A}{2} \leq \frac{S (j + 1) - S (j)}{2}$
185	177 184	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{S (j + 1) - S (j)}{2}$
186	175 185	pm2.61dan	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{S (j + 1) - S (j)}{2}$
187	116 109 43 186	leadd2dd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq S (j) + (\frac{S (j + 1) - S (j)}{2})$
188	43	recnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℂ$
189	107	recnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℂ$
190	188 189	addcomd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + S (j + 1) = S (j + 1) + S (j)$
191	190	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j) + S (j + 1)}{2} = \frac{S (j + 1) + S (j)}{2}$
192	191	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{S (j) + S (j + 1)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = (\frac{S (j + 1) + S (j)}{2}) - (\frac{S (j + 1) - S (j)}{2})$
193		halfaddsub	$⊢ (S (j + 1) \in ℂ \land S (j) \in ℂ) \to ((\frac{S (j + 1) + S (j)}{2}) + (\frac{S (j + 1) - S (j)}{2}) = S (j + 1) \land (\frac{S (j + 1) + S (j)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = S (j))$
194	189 188 193	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{S (j + 1) + S (j)}{2}) + (\frac{S (j + 1) - S (j)}{2}) = S (j + 1) \land (\frac{S (j + 1) + S (j)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = S (j))$
195	194	simprd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{S (j + 1) + S (j)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = S (j)$
196	192 195	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{S (j) + S (j + 1)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = S (j)$
197	188 189	addcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + S (j + 1) \in ℂ$
198	197	halfcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j) + S (j + 1)}{2} \in ℂ$
199	109	recnd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j + 1) - S (j)}{2} \in ℂ$
200	198 199 188	subsub23d	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{S (j) + S (j + 1)}{2}) - (\frac{S (j + 1) - S (j)}{2}) = S (j) \leftrightarrow (\frac{S (j) + S (j + 1)}{2}) - S (j) = \frac{S (j + 1) - S (j)}{2})$
201	196 200	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{S (j) + S (j + 1)}{2}) - S (j) = \frac{S (j + 1) - S (j)}{2}$
202	198 188 199	subaddd	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{S (j) + S (j + 1)}{2}) - S (j) = \frac{S (j + 1) - S (j)}{2} \leftrightarrow S (j) + (\frac{S (j + 1) - S (j)}{2}) = \frac{S (j) + S (j + 1)}{2})$
203	201 202	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + (\frac{S (j + 1) - S (j)}{2}) = \frac{S (j) + S (j + 1)}{2}$
204		avglt2	$⊢ (S (j) \in ℝ \land S (j + 1) \in ℝ) \to (S (j) < S (j + 1) \leftrightarrow \frac{S (j) + S (j + 1)}{2} < S (j + 1))$
205	43 107 204	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (S (j) < S (j + 1) \leftrightarrow \frac{S (j) + S (j + 1)}{2} < S (j + 1))$
206	129 205	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j) + S (j + 1)}{2} < S (j + 1)$
207	203 206	eqbrtrd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + (\frac{S (j + 1) - S (j)}{2}) < S (j + 1)$
208	117 170 107 187 207	lelttrd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) < S (j + 1)$
209	14 208	eqbrtrid	$⊢ (φ \land j \in (0 ..^N)) \to Z < S (j + 1)$
210	107	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℝ^{*}$
211		elico2	$⊢ (S (j) \in ℝ \land S (j + 1) \in ℝ^{*}) \to (Z \in [S (j), S (j + 1)) \leftrightarrow (Z \in ℝ \land S (j) \leq Z \land Z < S (j + 1)))$
212	43 210 211	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (Z \in [S (j), S (j + 1)) \leftrightarrow (Z \in ℝ \land S (j) \leq Z \land Z < S (j + 1)))$
213	118 169 209 212	mpbir3and	$⊢ (φ \land j \in (0 ..^N)) \to Z \in [S (j), S (j + 1))$
214	213	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to Z \in [S (j), S (j + 1))$
215	112	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A \in ℝ$
216	111	simp2d	$⊢ φ \to B \in ℝ$
217	216	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to B \in ℝ$
218	111	simp3d	$⊢ φ \to A < B$
219	218	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A < B$
220	43	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) \in ℝ$
221		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j)) = B$
222	167 14	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < Z$
223	216 112	resubcld	$⊢ φ \to B - A \in ℝ$
224	1 223	eqeltrid	$⊢ φ \to T \in ℝ$
225	224	adantr	$⊢ (φ \land j \in (0 ..^N)) \to T \in ℝ$
226	109	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to \frac{S (j + 1) - S (j)}{2} \in ℝ$
227	114	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to \frac{Q (1) - A}{2} \in ℝ$
228	108	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to S (j + 1) - S (j) \in ℝ$
229	113	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to Q (1) - A \in ℝ$
230	180	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to 2 \in ℝ^{+}$
231		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to S (j + 1) - S (j) < Q (1) - A$
232	228 229 230 231	ltdiv1dd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to \frac{S (j + 1) - S (j)}{2} < \frac{Q (1) - A}{2}$
233	226 227 232	ltled	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to \frac{S (j + 1) - S (j)}{2} \leq \frac{Q (1) - A}{2}$
234	172 233	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{Q (1) - A}{2}$
235	176	adantl	$⊢ (φ \land \neg S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = \frac{Q (1) - A}{2}$
236	114	leidd	$⊢ φ \to \frac{Q (1) - A}{2} \leq \frac{Q (1) - A}{2}$
237	236	adantr	$⊢ (φ \land \neg S (j + 1) - S (j) < Q (1) - A) \to \frac{Q (1) - A}{2} \leq \frac{Q (1) - A}{2}$
238	235 237	eqbrtrd	$⊢ (φ \land \neg S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{Q (1) - A}{2}$
239	238	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{Q (1) - A}{2}$
240	234 239	pm2.61dan	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq \frac{Q (1) - A}{2}$
241	223	rehalfcld	$⊢ φ \to \frac{B - A}{2} \in ℝ$
242	180	a1i	$⊢ φ \to 2 \in ℝ^{+}$
243	112	rexrd	$⊢ φ \to A \in ℝ^{*}$
244	216	rexrd	$⊢ φ \to B \in ℝ^{*}$
245	2 3 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
246	245 102	ffvelcdmd	$⊢ φ \to Q (1) \in [A, B]$
247		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Q (1) \in [A, B]) \to Q (1) \leq B$
248	243 244 246 247	syl3anc	$⊢ φ \to Q (1) \leq B$
249	110 216 112 248	lesub1dd	$⊢ φ \to Q (1) - A \leq B - A$
250	113 223 242 249	lediv1dd	$⊢ φ \to \frac{Q (1) - A}{2} \leq \frac{B - A}{2}$
251	1	eqcomi	$⊢ B - A = T$
252	251	oveq1i	$⊢ \frac{B - A}{2} = \frac{T}{2}$
253	112 216	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
254	218 253	mpbid	$⊢ φ \to 0 < B - A$
255	254 1	breqtrrdi	$⊢ φ \to 0 < T$
256	224 255	elrpd	$⊢ φ \to T \in ℝ^{+}$
257		rphalflt	$⊢ T \in ℝ^{+} \to \frac{T}{2} < T$
258	256 257	syl	$⊢ φ \to \frac{T}{2} < T$
259	252 258	eqbrtrid	$⊢ φ \to \frac{B - A}{2} < T$
260	114 241 224 250 259	lelttrd	$⊢ φ \to \frac{Q (1) - A}{2} < T$
261	114 224 260	ltled	$⊢ φ \to \frac{Q (1) - A}{2} \leq T$
262	261	adantr	$⊢ (φ \land j \in (0 ..^N)) \to \frac{Q (1) - A}{2} \leq T$
263	116 115 225 240 262	letrd	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq T$
264	116 225 43 263	leadd2dd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \leq S (j) + T$
265	14 264	eqbrtrid	$⊢ (φ \land j \in (0 ..^N)) \to Z \leq S (j) + T$
266	43	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℝ^{*}$
267	43 225	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + T \in ℝ$
268		elioc2	$⊢ (S (j) \in ℝ^{*} \land S (j) + T \in ℝ) \to (Z \in (S (j), S (j) + T] \leftrightarrow (Z \in ℝ \land S (j) < Z \land Z \leq S (j) + T))$
269	266 267 268	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (Z \in (S (j), S (j) + T] \leftrightarrow (Z \in ℝ \land S (j) < Z \land Z \leq S (j) + T))$
270	118 222 265 269	mpbir3and	$⊢ (φ \land j \in (0 ..^N)) \to Z \in (S (j), S (j) + T]$
271	270	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to Z \in (S (j), S (j) + T]$
272	215 217 219 1 12 220 221 271	fourierdlem26	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (Z) = A + Z - S (j)$
273	14	a1i	$⊢ (φ \land j \in (0 ..^N)) \to Z = S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
274	273	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to Z - S (j) = S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) - S (j)$
275	274	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to A + Z - S (j) = A + (S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})) - S (j)$
276	275	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A + Z - S (j) = A + (S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})) - S (j)$
277	116	recnd	$⊢ (φ \land j \in (0 ..^N)) \to if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) \in ℂ$
278	188 277	pncan2d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) - S (j) = if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
279	278	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to A + (S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})) - S (j) = A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
280	279	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A + (S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})) - S (j) = A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
281	272 276 280	3eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (Z) = A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
282	171	oveq2d	$⊢ S (j + 1) - S (j) < Q (1) - A \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = A + (\frac{S (j + 1) - S (j)}{2})$
283	282	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = A + (\frac{S (j + 1) - S (j)}{2})$
284	112	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ$
285	284 109	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to A + (\frac{S (j + 1) - S (j)}{2}) \in ℝ$
286	285	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{S (j + 1) - S (j)}{2}) \in ℝ$
287	284 115	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to A + (\frac{Q (1) - A}{2}) \in ℝ$
288	287	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{Q (1) - A}{2}) \in ℝ$
289	110	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to Q (1) \in ℝ$
290	112	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A \in ℝ$
291	226 227 290 232	ltadd2dd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{S (j + 1) - S (j)}{2}) < A + (\frac{Q (1) - A}{2})$
292	110	recnd	$⊢ φ \to Q (1) \in ℂ$
293	112	recnd	$⊢ φ \to A \in ℂ$
294		halfaddsub	$⊢ (Q (1) \in ℂ \land A \in ℂ) \to ((\frac{Q (1) + A}{2}) + (\frac{Q (1) - A}{2}) = Q (1) \land (\frac{Q (1) + A}{2}) - (\frac{Q (1) - A}{2}) = A)$
295	292 293 294	syl2anc	$⊢ φ \to ((\frac{Q (1) + A}{2}) + (\frac{Q (1) - A}{2}) = Q (1) \land (\frac{Q (1) + A}{2}) - (\frac{Q (1) - A}{2}) = A)$
296	295	simprd	$⊢ φ \to (\frac{Q (1) + A}{2}) - (\frac{Q (1) - A}{2}) = A$
297	296	oveq1d	$⊢ φ \to (\frac{Q (1) + A}{2}) - (\frac{Q (1) - A}{2}) + (\frac{Q (1) - A}{2}) = A + (\frac{Q (1) - A}{2})$
298	110 112	readdcld	$⊢ φ \to Q (1) + A \in ℝ$
299	298	rehalfcld	$⊢ φ \to \frac{Q (1) + A}{2} \in ℝ$
300	299	recnd	$⊢ φ \to \frac{Q (1) + A}{2} \in ℂ$
301	114	recnd	$⊢ φ \to \frac{Q (1) - A}{2} \in ℂ$
302	300 301	npcand	$⊢ φ \to (\frac{Q (1) + A}{2}) - (\frac{Q (1) - A}{2}) + (\frac{Q (1) - A}{2}) = \frac{Q (1) + A}{2}$
303	297 302	eqtr3d	$⊢ φ \to A + (\frac{Q (1) - A}{2}) = \frac{Q (1) + A}{2}$
304	110 110	readdcld	$⊢ φ \to Q (1) + Q (1) \in ℝ$
305	112 110 110 159	ltadd2dd	$⊢ φ \to Q (1) + A < Q (1) + Q (1)$
306	298 304 242 305	ltdiv1dd	$⊢ φ \to \frac{Q (1) + A}{2} < \frac{Q (1) + Q (1)}{2}$
307	292	2timesd	$⊢ φ \to 2 Q (1) = Q (1) + Q (1)$
308	307	eqcomd	$⊢ φ \to Q (1) + Q (1) = 2 Q (1)$
309	308	oveq1d	$⊢ φ \to \frac{Q (1) + Q (1)}{2} = \frac{2 Q (1)}{2}$
310		2cnd	$⊢ φ \to 2 \in ℂ$
311		2ne0	$⊢ 2 \neq 0$
312	311	a1i	$⊢ φ \to 2 \neq 0$
313	292 310 312	divcan3d	$⊢ φ \to \frac{2 Q (1)}{2} = Q (1)$
314	309 313	eqtrd	$⊢ φ \to \frac{Q (1) + Q (1)}{2} = Q (1)$
315	306 314	breqtrd	$⊢ φ \to \frac{Q (1) + A}{2} < Q (1)$
316	303 315	eqbrtrd	$⊢ φ \to A + (\frac{Q (1) - A}{2}) < Q (1)$
317	316	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{Q (1) - A}{2}) < Q (1)$
318	286 288 289 291 317	lttrd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{S (j + 1) - S (j)}{2}) < Q (1)$
319	283 318	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land S (j + 1) - S (j) < Q (1) - A) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) < Q (1)$
320	176	oveq2d	$⊢ \neg S (j + 1) - S (j) < Q (1) - A \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = A + (\frac{Q (1) - A}{2})$
321	320	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = A + (\frac{Q (1) - A}{2})$
322	316	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to A + (\frac{Q (1) - A}{2}) < Q (1)$
323	321 322	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) - S (j) < Q (1) - A) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) < Q (1)$
324	319 323	pm2.61dan	$⊢ (φ \land j \in (0 ..^N)) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) < Q (1)$
325	324	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) < Q (1)$
326	281 325	eqbrtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (Z) < Q (1)$
327		eqid	$⊢ Q (1) - (E (Z) - Z) = Q (1) - (E (Z) - Z)$
328	1 2 91 92 93 94 95 8 9 10 11 12 103 104 214 326 327	fourierdlem63	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) \leq Q (1)$
329	15	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
330	58	adantl	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land x = S (j)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
331	61	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) \in V$
332	329 330 220 331	fvmptd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to I (S (j)) = sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
333		fveq2	$⊢ E (S (j)) = B \to L (E (S (j))) = L (B)$
334	13	a1i	$⊢ φ \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
335		iftrue	$⊢ y = B \to if (y = B, A, y) = A$
336	335	adantl	$⊢ (φ \land y = B) \to if (y = B, A, y) = A$
337		ubioc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to B \in (A, B]$
338	243 244 218 337	syl3anc	$⊢ φ \to B \in (A, B]$
339	334 336 338 112	fvmptd	$⊢ φ \to L (B) = A$
340	333 339	sylan9eqr	$⊢ (φ \land E (S (j)) = B) \to L (E (S (j))) = A$
341	340	breq2d	$⊢ (φ \land E (S (j)) = B) \to (Q (i) \leq L (E (S (j))) \leftrightarrow Q (i) \leq A)$
342	341	rabbidv	$⊢ (φ \land E (S (j)) = B) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} = \{i \in (0 ..^M) \| Q (i) \leq A\}$
343	342	supeq1d	$⊢ (φ \land E (S (j)) = B) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq A\} ℝ <)$
344	343	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) = sup (\{i \in (0 ..^M) \| Q (i) \leq A\} ℝ <)$
345		simpl	$⊢ (φ \land j \in \{i \in (0 ..^M) \| Q (i) \leq A\}) \to φ$
346		elrabi	$⊢ j \in \{i \in (0 ..^M) \| Q (i) \leq A\} \to j \in (0 ..^M)$
347	346	adantl	$⊢ (φ \land j \in \{i \in (0 ..^M) \| Q (i) \leq A\}) \to j \in (0 ..^M)$
348		fveq2	$⊢ i = j \to Q (i) = Q (j)$
349	348	breq1d	$⊢ i = j \to (Q (i) \leq A \leftrightarrow Q (j) \leq A)$
350	349	elrab	$⊢ j \in \{i \in (0 ..^M) \| Q (i) \leq A\} \leftrightarrow (j \in (0 ..^M) \land Q (j) \leq A)$
351	350	simprbi	$⊢ j \in \{i \in (0 ..^M) \| Q (i) \leq A\} \to Q (j) \leq A$
352	351	adantl	$⊢ (φ \land j \in \{i \in (0 ..^M) \| Q (i) \leq A\}) \to Q (j) \leq A$
353		simp3	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to Q (j) \leq A$
354	112	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to A \in ℝ$
355	110	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to Q (1) \in ℝ$
356	21	adantr	$⊢ (φ \land j \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
357	26	sselda	$⊢ (φ \land j \in (0 ..^M)) \to j \in (0 \dots M)$
358	356 357	ffvelcdmd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \in ℝ$
359	358	adantr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to Q (j) \in ℝ$
360	159	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to A < Q (1)$
361		1zzd	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 1 \in ℤ$
362		elfzoelz	$⊢ j \in (0 ..^M) \to j \in ℤ$
363	362	ad2antlr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to j \in ℤ$
364		1e0p1	$⊢ 1 = 0 + 1$
365		simpr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to \neg j \leq 0$
366		0red	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 0 \in ℝ$
367	363	zred	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to j \in ℝ$
368	366 367	ltnled	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to (0 < j \leftrightarrow \neg j \leq 0)$
369	365 368	mpbird	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 0 < j$
370		0zd	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 0 \in ℤ$
371		zltp1le	$⊢ (0 \in ℤ \land j \in ℤ) \to (0 < j \leftrightarrow 0 + 1 \leq j)$
372	370 363 371	syl2anc	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to (0 < j \leftrightarrow 0 + 1 \leq j)$
373	369 372	mpbid	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 0 + 1 \leq j$
374	364 373	eqbrtrid	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to 1 \leq j$
375		eluz2	$⊢ j \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land j \in ℤ \land 1 \leq j)$
376	361 363 374 375	syl3anbrc	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to j \in ℤ_{\geq 1}$
377	21	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to Q : (0 \dots M) ⟶ ℝ$
378		0zd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to 0 \in ℤ$
379	97	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to M \in ℤ$
380		elfzelz	$⊢ l \in (1 \dots j) \to l \in ℤ$
381	380	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l \in ℤ$
382		0red	$⊢ l \in (1 \dots j) \to 0 \in ℝ$
383	380	zred	$⊢ l \in (1 \dots j) \to l \in ℝ$
384		1red	$⊢ l \in (1 \dots j) \to 1 \in ℝ$
385		0lt1	$⊢ 0 < 1$
386	385	a1i	$⊢ l \in (1 \dots j) \to 0 < 1$
387		elfzle1	$⊢ l \in (1 \dots j) \to 1 \leq l$
388	382 384 383 386 387	ltletrd	$⊢ l \in (1 \dots j) \to 0 < l$
389	382 383 388	ltled	$⊢ l \in (1 \dots j) \to 0 \leq l$
390	389	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to 0 \leq l$
391	383	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l \in ℝ$
392	97	zred	$⊢ φ \to M \in ℝ$
393	392	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to M \in ℝ$
394	362	zred	$⊢ j \in (0 ..^M) \to j \in ℝ$
395	394	ad2antlr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to j \in ℝ$
396		elfzle2	$⊢ l \in (1 \dots j) \to l \leq j$
397	396	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l \leq j$
398		elfzolt2	$⊢ j \in (0 ..^M) \to j < M$
399	398	ad2antlr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to j < M$
400	391 395 393 397 399	lelttrd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l < M$
401	391 393 400	ltled	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l \leq M$
402	378 379 381 390 401	elfzd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to l \in (0 \dots M)$
403	377 402	ffvelcdmd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j)) \to Q (l) \in ℝ$
404	403	adantlr	$⊢ (((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \land l \in (1 \dots j)) \to Q (l) \in ℝ$
405	21	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to Q : (0 \dots M) ⟶ ℝ$
406		0zd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to 0 \in ℤ$
407	97	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to M \in ℤ$
408		elfzelz	$⊢ l \in (1 \dots j - 1) \to l \in ℤ$
409	408	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l \in ℤ$
410		0red	$⊢ l \in (1 \dots j - 1) \to 0 \in ℝ$
411	408	zred	$⊢ l \in (1 \dots j - 1) \to l \in ℝ$
412		1red	$⊢ l \in (1 \dots j - 1) \to 1 \in ℝ$
413	385	a1i	$⊢ l \in (1 \dots j - 1) \to 0 < 1$
414		elfzle1	$⊢ l \in (1 \dots j - 1) \to 1 \leq l$
415	410 412 411 413 414	ltletrd	$⊢ l \in (1 \dots j - 1) \to 0 < l$
416	410 411 415	ltled	$⊢ l \in (1 \dots j - 1) \to 0 \leq l$
417	416	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to 0 \leq l$
418	409	zred	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l \in ℝ$
419	392	ad2antrr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to M \in ℝ$
420	394	ad2antlr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to j \in ℝ$
421	411	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l \in ℝ$
422		peano2rem	$⊢ j \in ℝ \to j - 1 \in ℝ$
423	394 422	syl	$⊢ j \in (0 ..^M) \to j - 1 \in ℝ$
424	423	adantr	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to j - 1 \in ℝ$
425	394	adantr	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to j \in ℝ$
426		elfzle2	$⊢ l \in (1 \dots j - 1) \to l \leq j - 1$
427	426	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l \leq j - 1$
428	425	ltm1d	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to j - 1 < j$
429	421 424 425 427 428	lelttrd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l < j$
430	429	adantll	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l < j$
431	398	ad2antlr	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to j < M$
432	418 420 419 430 431	lttrd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l < M$
433	418 419 432	ltled	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l \leq M$
434	406 407 409 417 433	elfzd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l \in (0 \dots M)$
435	405 434	ffvelcdmd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to Q (l) \in ℝ$
436	409	peano2zd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 \in ℤ$
437	411 412	readdcld	$⊢ l \in (1 \dots j - 1) \to l + 1 \in ℝ$
438	411 412 415 413	addgt0d	$⊢ l \in (1 \dots j - 1) \to 0 < l + 1$
439	410 437 438	ltled	$⊢ l \in (1 \dots j - 1) \to 0 \leq l + 1$
440	439	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to 0 \leq l + 1$
441	437	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 \in ℝ$
442	437	recnd	$⊢ l \in (1 \dots j - 1) \to l + 1 \in ℂ$
443		1cnd	$⊢ l \in (1 \dots j - 1) \to 1 \in ℂ$
444	442 443	npcand	$⊢ l \in (1 \dots j - 1) \to (l + 1) - 1 + 1 = l + 1$
445	444	eqcomd	$⊢ l \in (1 \dots j - 1) \to l + 1 = (l + 1) - 1 + 1$
446	445	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l + 1 = (l + 1) - 1 + 1$
447		peano2re	$⊢ l \in ℝ \to l + 1 \in ℝ$
448		peano2rem	$⊢ l + 1 \in ℝ \to l + 1 - 1 \in ℝ$
449	421 447 448	3syl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l + 1 - 1 \in ℝ$
450		peano2re	$⊢ j - 1 \in ℝ \to j - 1 + 1 \in ℝ$
451		peano2rem	$⊢ j - 1 + 1 \in ℝ \to (j - 1) + 1 - 1 \in ℝ$
452	424 450 451	3syl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to (j - 1) + 1 - 1 \in ℝ$
453		1red	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to 1 \in ℝ$
454		elfzel2	$⊢ l \in (1 \dots j - 1) \to j - 1 \in ℤ$
455	454	zred	$⊢ l \in (1 \dots j - 1) \to j - 1 \in ℝ$
456	455 412	readdcld	$⊢ l \in (1 \dots j - 1) \to j - 1 + 1 \in ℝ$
457	411 455 412 426	leadd1dd	$⊢ l \in (1 \dots j - 1) \to l + 1 \leq j - 1 + 1$
458	437 456 412 457	lesub1dd	$⊢ l \in (1 \dots j - 1) \to l + 1 - 1 \leq (j - 1) + 1 - 1$
459	458	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l + 1 - 1 \leq (j - 1) + 1 - 1$
460	449 452 453 459	leadd1dd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to (l + 1) - 1 + 1 \leq (j - 1 + 1) - 1 + 1$
461		peano2zm	$⊢ j \in ℤ \to j - 1 \in ℤ$
462	362 461	syl	$⊢ j \in (0 ..^M) \to j - 1 \in ℤ$
463	462	peano2zd	$⊢ j \in (0 ..^M) \to j - 1 + 1 \in ℤ$
464	463	zcnd	$⊢ j \in (0 ..^M) \to j - 1 + 1 \in ℂ$
465		1cnd	$⊢ j \in (0 ..^M) \to 1 \in ℂ$
466	464 465	npcand	$⊢ j \in (0 ..^M) \to (j - 1 + 1) - 1 + 1 = j - 1 + 1$
467	394	recnd	$⊢ j \in (0 ..^M) \to j \in ℂ$
468	467 465	npcand	$⊢ j \in (0 ..^M) \to j - 1 + 1 = j$
469	466 468	eqtrd	$⊢ j \in (0 ..^M) \to (j - 1 + 1) - 1 + 1 = j$
470	469	adantr	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to (j - 1 + 1) - 1 + 1 = j$
471	460 470	breqtrd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to (l + 1) - 1 + 1 \leq j$
472	446 471	eqbrtrd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l + 1 \leq j$
473	472	adantll	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 \leq j$
474	441 420 419 473 431	lelttrd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 < M$
475	441 419 474	ltled	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 \leq M$
476	406 407 436 440 475	elfzd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l + 1 \in (0 \dots M)$
477	405 476	ffvelcdmd	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to Q (l + 1) \in ℝ$
478		simpll	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to φ$
479		0zd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to 0 \in ℤ$
480	408	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l \in ℤ$
481	416	adantl	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to 0 \leq l$
482		eluz2	$⊢ l \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land l \in ℤ \land 0 \leq l)$
483	479 480 481 482	syl3anbrc	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l \in ℤ_{\geq 0}$
484		elfzoel2	$⊢ j \in (0 ..^M) \to M \in ℤ$
485	484	adantr	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to M \in ℤ$
486	485	zred	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to M \in ℝ$
487	398	adantr	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to j < M$
488	421 425 486 429 487	lttrd	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l < M$
489		elfzo2	$⊢ l \in (0 ..^M) \leftrightarrow (l \in ℤ_{\geq 0} \land M \in ℤ \land l < M)$
490	483 485 488 489	syl3anbrc	$⊢ (j \in (0 ..^M) \land l \in (1 \dots j - 1)) \to l \in (0 ..^M)$
491	490	adantll	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to l \in (0 ..^M)$
492		eleq1	$⊢ i = l \to (i \in (0 ..^M) \leftrightarrow l \in (0 ..^M))$
493	492	anbi2d	$⊢ i = l \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land l \in (0 ..^M)))$
494		fveq2	$⊢ i = l \to Q (i) = Q (l)$
495		oveq1	$⊢ i = l \to i + 1 = l + 1$
496	495	fveq2d	$⊢ i = l \to Q (i + 1) = Q (l + 1)$
497	494 496	breq12d	$⊢ i = l \to (Q (i) < Q (i + 1) \leftrightarrow Q (l) < Q (l + 1))$
498	493 497	imbi12d	$⊢ i = l \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land l \in (0 ..^M)) \to Q (l) < Q (l + 1)))$
499	498 150	chvarvv	$⊢ (φ \land l \in (0 ..^M)) \to Q (l) < Q (l + 1)$
500	478 491 499	syl2anc	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to Q (l) < Q (l + 1)$
501	435 477 500	ltled	$⊢ ((φ \land j \in (0 ..^M)) \land l \in (1 \dots j - 1)) \to Q (l) \leq Q (l + 1)$
502	501	adantlr	$⊢ (((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \land l \in (1 \dots j - 1)) \to Q (l) \leq Q (l + 1)$
503	376 404 502	monoord	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to Q (1) \leq Q (j)$
504	354 355 359 360 503	ltletrd	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to A < Q (j)$
505	354 359	ltnled	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to (A < Q (j) \leftrightarrow \neg Q (j) \leq A)$
506	504 505	mpbid	$⊢ ((φ \land j \in (0 ..^M)) \land \neg j \leq 0) \to \neg Q (j) \leq A$
507	506	ex	$⊢ (φ \land j \in (0 ..^M)) \to (\neg j \leq 0 \to \neg Q (j) \leq A)$
508	507	3adant3	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to (\neg j \leq 0 \to \neg Q (j) \leq A)$
509	353 508	mt4d	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to j \leq 0$
510		elfzole1	$⊢ j \in (0 ..^M) \to 0 \leq j$
511	510	3ad2ant2	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to 0 \leq j$
512	394	3ad2ant2	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to j \in ℝ$
513		0red	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to 0 \in ℝ$
514	512 513	letri3d	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to (j = 0 \leftrightarrow (j \leq 0 \land 0 \leq j))$
515	509 511 514	mpbir2and	$⊢ (φ \land j \in (0 ..^M) \land Q (j) \leq A) \to j = 0$
516	345 347 352 515	syl3anc	$⊢ (φ \land j \in \{i \in (0 ..^M) \| Q (i) \leq A\}) \to j = 0$
517		velsn	$⊢ j \in \{0\} \leftrightarrow j = 0$
518	516 517	sylibr	$⊢ (φ \land j \in \{i \in (0 ..^M) \| Q (i) \leq A\}) \to j \in \{0\}$
519	518	ralrimiva	$⊢ φ \to \forall j \in \{i \in (0 ..^M) \| Q (i) \leq A\} j \in \{0\}$
520		dfss3	$⊢ \{i \in (0 ..^M) \| Q (i) \leq A\} \subseteq \{0\} \leftrightarrow \forall j \in \{i \in (0 ..^M) \| Q (i) \leq A\} j \in \{0\}$
521	519 520	sylibr	$⊢ φ \to \{i \in (0 ..^M) \| Q (i) \leq A\} \subseteq \{0\}$
522	155 112	eqeltrd	$⊢ φ \to Q (0) \in ℝ$
523	522 155	eqled	$⊢ φ \to Q (0) \leq A$
524	143	breq1d	$⊢ i = 0 \to (Q (i) \leq A \leftrightarrow Q (0) \leq A)$
525	524	elrab	$⊢ 0 \in \{i \in (0 ..^M) \| Q (i) \leq A\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) \leq A)$
526	139 523 525	sylanbrc	$⊢ φ \to 0 \in \{i \in (0 ..^M) \| Q (i) \leq A\}$
527	526	snssd	$⊢ φ \to \{0\} \subseteq \{i \in (0 ..^M) \| Q (i) \leq A\}$
528	521 527	eqssd	$⊢ φ \to \{i \in (0 ..^M) \| Q (i) \leq A\} = \{0\}$
529	528	supeq1d	$⊢ φ \to sup (\{i \in (0 ..^M) \| Q (i) \leq A\} ℝ <) = sup (\{0\} ℝ <)$
530		supsn	$⊢ (< Or ℝ \land 0 \in ℝ) \to sup (\{0\} ℝ <) = 0$
531	60 140 530	mp2an	$⊢ sup (\{0\} ℝ <) = 0$
532	531	a1i	$⊢ φ \to sup (\{0\} ℝ <) = 0$
533	529 532	eqtrd	$⊢ φ \to sup (\{i \in (0 ..^M) \| Q (i) \leq A\} ℝ <) = 0$
534	533	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to sup (\{i \in (0 ..^M) \| Q (i) \leq A\} ℝ <) = 0$
535	332 344 534	3eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to I (S (j)) = 0$
536	535	oveq1d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to I (S (j)) + 1 = 0 + 1$
537	536	fveq2d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to Q (I (S (j)) + 1) = Q (0 + 1)$
538	537 157	eqtr2di	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to Q (1) = Q (I (S (j)) + 1)$
539	328 538	breqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) \leq Q (I (S (j)) + 1)$
540	66	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to (φ \land S (j) \in ℝ)$
541		simplr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to j \in (0 ..^N)$
542	13	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
543		simpr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y = E (S (j))$
544		neqne	$⊢ \neg E (S (j)) = B \to E (S (j)) \neq B$
545	544	adantr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to E (S (j)) \neq B$
546	543 545	eqnetrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y \neq B$
547	546	neneqd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to \neg y = B$
548	547	iffalsed	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = y$
549	548 543	eqtrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = E (S (j))$
550	549	adantll	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land y = E (S (j))) \to if (y = B, A, y) = E (S (j))$
551	112 216 218 1 12	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
552	551	adantr	$⊢ (φ \land j \in (0 ..^N)) \to E : ℝ ⟶ (A, B]$
553	552 43	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in (A, B]$
554	553	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in (A, B]$
555	542 550 554 554	fvmptd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L (E (S (j))) = E (S (j))$
556	555	eqcomd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) = L (E (S (j)))$
557	112 216 218 13	fourierdlem17	$⊢ φ \to L : (A, B] ⟶ [A, B]$
558	557	adantr	$⊢ (φ \land j \in (0 ..^N)) \to L : (A, B] ⟶ [A, B]$
559	112 216	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
560	559	adantr	$⊢ (φ \land j \in (0 ..^N)) \to [A, B] \subseteq ℝ$
561	558 560	fssd	$⊢ (φ \land j \in (0 ..^N)) \to L : (A, B] ⟶ ℝ$
562	561 553	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to L (E (S (j))) \in ℝ$
563	562	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L (E (S (j))) \in ℝ$
564	556 563	eqeltrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in ℝ$
565	216	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \in ℝ$
566	243	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ^{*}$
567	216	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B \in ℝ$
568		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (E (S (j)) \in (A, B] \leftrightarrow (E (S (j)) \in ℝ \land A < E (S (j)) \land E (S (j)) \leq B))$
569	566 567 568	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (E (S (j)) \in (A, B] \leftrightarrow (E (S (j)) \in ℝ \land A < E (S (j)) \land E (S (j)) \leq B))$
570	553 569	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (E (S (j)) \in ℝ \land A < E (S (j)) \land E (S (j)) \leq B)$
571	570	simp3d	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \leq B$
572	571	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \leq B$
573	544	necomd	$⊢ \neg E (S (j)) = B \to B \neq E (S (j))$
574	573	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \neq E (S (j))$
575	564 565 572 574	leneltd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) < B$
576	575	adantr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land I (S (j)) = M - 1) \to E (S (j)) < B$
577		oveq1	$⊢ I (S (j)) = M - 1 \to I (S (j)) + 1 = M - 1 + 1$
578	3	nncnd	$⊢ φ \to M \in ℂ$
579		1cnd	$⊢ φ \to 1 \in ℂ$
580	578 579	npcand	$⊢ φ \to M - 1 + 1 = M$
581	577 580	sylan9eqr	$⊢ (φ \land I (S (j)) = M - 1) \to I (S (j)) + 1 = M$
582	581	fveq2d	$⊢ (φ \land I (S (j)) = M - 1) \to Q (I (S (j)) + 1) = Q (M)$
583	154	simprd	$⊢ φ \to Q (M) = B$
584	583	adantr	$⊢ (φ \land I (S (j)) = M - 1) \to Q (M) = B$
585	582 584	eqtr2d	$⊢ (φ \land I (S (j)) = M - 1) \to B = Q (I (S (j)) + 1)$
586	585	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land I (S (j)) = M - 1) \to B = Q (I (S (j)) + 1)$
587	586	adantlr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land I (S (j)) = M - 1) \to B = Q (I (S (j)) + 1)$
588	576 587	breqtrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land I (S (j)) = M - 1) \to E (S (j)) < Q (I (S (j)) + 1)$
589	556	adantr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg I (S (j)) = M - 1) \to E (S (j)) = L (E (S (j)))$
590		ssrab2	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq (0 ..^M)$
591		fzssz	$⊢ (0 \dots M) \subseteq ℤ$
592	25 591	sstri	$⊢ (0 ..^M) \subseteq ℤ$
593		zssre	$⊢ ℤ \subseteq ℝ$
594	592 593	sstri	$⊢ (0 ..^M) \subseteq ℝ$
595	590 594	sstri	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq ℝ$
596	595	a1i	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq ℝ$
597	57	neeq1d	$⊢ x = S (j) \to (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset \leftrightarrow \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset)$
598	68 597	imbi12d	$⊢ x = S (j) \to (((φ \land x \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset) \leftrightarrow ((φ \land S (j) \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset))$
599	139	adantr	$⊢ (φ \land x \in ℝ) \to 0 \in (0 ..^M)$
600	523	ad2antrr	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to Q (0) \leq A$
601		iftrue	$⊢ E (x) = B \to if (E (x) = B, A, E (x)) = A$
602	601	eqcomd	$⊢ E (x) = B \to A = if (E (x) = B, A, E (x))$
603	602	adantl	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to A = if (E (x) = B, A, E (x))$
604	600 603	breqtrd	$⊢ ((φ \land x \in ℝ) \land E (x) = B) \to Q (0) \leq if (E (x) = B, A, E (x))$
605	522	adantr	$⊢ (φ \land x \in ℝ) \to Q (0) \in ℝ$
606	112	adantr	$⊢ (φ \land x \in ℝ) \to A \in ℝ$
607	606	rexrd	$⊢ (φ \land x \in ℝ) \to A \in ℝ^{*}$
608	216	adantr	$⊢ (φ \land x \in ℝ) \to B \in ℝ$
609		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
610	607 608 609	syl2anc	$⊢ (φ \land x \in ℝ) \to (A, B] \subseteq ℝ$
611	551	ffvelcdmda	$⊢ (φ \land x \in ℝ) \to E (x) \in (A, B]$
612	610 611	sseldd	$⊢ (φ \land x \in ℝ) \to E (x) \in ℝ$
613	155	adantr	$⊢ (φ \land x \in ℝ) \to Q (0) = A$
614		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (E (x) \in (A, B] \leftrightarrow (E (x) \in ℝ \land A < E (x) \land E (x) \leq B))$
615	607 608 614	syl2anc	$⊢ (φ \land x \in ℝ) \to (E (x) \in (A, B] \leftrightarrow (E (x) \in ℝ \land A < E (x) \land E (x) \leq B))$
616	611 615	mpbid	$⊢ (φ \land x \in ℝ) \to (E (x) \in ℝ \land A < E (x) \land E (x) \leq B)$
617	616	simp2d	$⊢ (φ \land x \in ℝ) \to A < E (x)$
618	613 617	eqbrtrd	$⊢ (φ \land x \in ℝ) \to Q (0) < E (x)$
619	605 612 618	ltled	$⊢ (φ \land x \in ℝ) \to Q (0) \leq E (x)$
620	619	adantr	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to Q (0) \leq E (x)$
621		iffalse	$⊢ \neg E (x) = B \to if (E (x) = B, A, E (x)) = E (x)$
622	621	eqcomd	$⊢ \neg E (x) = B \to E (x) = if (E (x) = B, A, E (x))$
623	622	adantl	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to E (x) = if (E (x) = B, A, E (x))$
624	620 623	breqtrd	$⊢ ((φ \land x \in ℝ) \land \neg E (x) = B) \to Q (0) \leq if (E (x) = B, A, E (x))$
625	604 624	pm2.61dan	$⊢ (φ \land x \in ℝ) \to Q (0) \leq if (E (x) = B, A, E (x))$
626	13	a1i	$⊢ (φ \land x \in ℝ) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
627		eqeq1	$⊢ y = E (x) \to (y = B \leftrightarrow E (x) = B)$
628		id	$⊢ y = E (x) \to y = E (x)$
629	627 628	ifbieq2d	$⊢ y = E (x) \to if (y = B, A, y) = if (E (x) = B, A, E (x))$
630	629	adantl	$⊢ ((φ \land x \in ℝ) \land y = E (x)) \to if (y = B, A, y) = if (E (x) = B, A, E (x))$
631	606 612	ifcld	$⊢ (φ \land x \in ℝ) \to if (E (x) = B, A, E (x)) \in ℝ$
632	626 630 611 631	fvmptd	$⊢ (φ \land x \in ℝ) \to L (E (x)) = if (E (x) = B, A, E (x))$
633	625 632	breqtrrd	$⊢ (φ \land x \in ℝ) \to Q (0) \leq L (E (x))$
634	143	breq1d	$⊢ i = 0 \to (Q (i) \leq L (E (x)) \leftrightarrow Q (0) \leq L (E (x)))$
635	634	elrab	$⊢ 0 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \leftrightarrow (0 \in (0 ..^M) \land Q (0) \leq L (E (x)))$
636	599 633 635	sylanbrc	$⊢ (φ \land x \in ℝ) \to 0 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}$
637		ne0i	$⊢ 0 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset$
638	636 637	syl	$⊢ (φ \land x \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} \neq \emptyset$
639	598 638	vtoclg	$⊢ S (j) \in ℝ \to ((φ \land S (j) \in ℝ) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset)$
640	43 66 639	sylc	$⊢ (φ \land j \in (0 ..^N)) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset$
641	640	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset$
642	595	a1i	$⊢ (φ \land j \in (0 ..^N)) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq ℝ$
643		fzofi	$⊢ (0 ..^M) \in Fin$
644		ssfi	$⊢ ((0 ..^M) \in Fin \land \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq (0 ..^M)) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \in Fin$
645	643 590 644	mp2an	$⊢ \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \in Fin$
646	645	a1i	$⊢ (φ \land j \in (0 ..^N)) \to \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \in Fin$
647		fimaxre2	$⊢ (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq ℝ \land \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \in Fin) \to \exists x \in ℝ \forall l \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} l \leq x$
648	642 646 647	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to \exists x \in ℝ \forall l \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} l \leq x$
649	648	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to \exists x \in ℝ \forall l \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} l \leq x$
650		0red	$⊢ (φ \land j \in (0 ..^N)) \to 0 \in ℝ$
651	594 48	sselid	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) \in ℝ$
652		1red	$⊢ (φ \land j \in (0 ..^N)) \to 1 \in ℝ$
653	651 652	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) + 1 \in ℝ$
654		elfzouz	$⊢ I (S (j)) \in (0 ..^M) \to I (S (j)) \in ℤ_{\geq 0}$
655		eluzle	$⊢ I (S (j)) \in ℤ_{\geq 0} \to 0 \leq I (S (j))$
656	48 654 655	3syl	$⊢ (φ \land j \in (0 ..^N)) \to 0 \leq I (S (j))$
657	385	a1i	$⊢ (φ \land j \in (0 ..^N)) \to 0 < 1$
658	651 652 656 657	addgegt0d	$⊢ (φ \land j \in (0 ..^N)) \to 0 < I (S (j)) + 1$
659	650 653 658	ltled	$⊢ (φ \land j \in (0 ..^N)) \to 0 \leq I (S (j)) + 1$
660	659	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to 0 \leq I (S (j)) + 1$
661	651	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) \in ℝ$
662		1red	$⊢ φ \to 1 \in ℝ$
663	392 662	resubcld	$⊢ φ \to M - 1 \in ℝ$
664	663	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to M - 1 \in ℝ$
665		1red	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to 1 \in ℝ$
666		elfzolt2	$⊢ I (S (j)) \in (0 ..^M) \to I (S (j)) < M$
667	48 666	syl	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) < M$
668	44	elfzelzd	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) \in ℤ$
669	97	adantr	$⊢ (φ \land j \in (0 ..^N)) \to M \in ℤ$
670		zltlem1	$⊢ (I (S (j)) \in ℤ \land M \in ℤ) \to (I (S (j)) < M \leftrightarrow I (S (j)) \leq M - 1)$
671	668 669 670	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (I (S (j)) < M \leftrightarrow I (S (j)) \leq M - 1)$
672	667 671	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) \leq M - 1$
673	672	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) \leq M - 1$
674		neqne	$⊢ \neg I (S (j)) = M - 1 \to I (S (j)) \neq M - 1$
675	674	necomd	$⊢ \neg I (S (j)) = M - 1 \to M - 1 \neq I (S (j))$
676	675	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to M - 1 \neq I (S (j))$
677	661 664 673 676	leneltd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) < M - 1$
678	661 664 665 677	ltadd1dd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) + 1 < M - 1 + 1$
679	580	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to M - 1 + 1 = M$
680	678 679	breqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) + 1 < M$
681	50	elfzelzd	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) + 1 \in ℤ$
682	681	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) + 1 \in ℤ$
683		0zd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to 0 \in ℤ$
684	97	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to M \in ℤ$
685		elfzo	$⊢ (I (S (j)) + 1 \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (I (S (j)) + 1 \in (0 ..^M) \leftrightarrow (0 \leq I (S (j)) + 1 \land I (S (j)) + 1 < M))$
686	682 683 684 685	syl3anc	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to (I (S (j)) + 1 \in (0 ..^M) \leftrightarrow (0 \leq I (S (j)) + 1 \land I (S (j)) + 1 < M))$
687	660 680 686	mpbir2and	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to I (S (j)) + 1 \in (0 ..^M)$
688	687	adantr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to I (S (j)) + 1 \in (0 ..^M)$
689		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to Q (I (S (j)) + 1) \leq L (E (S (j)))$
690		fveq2	$⊢ i = I (S (j)) + 1 \to Q (i) = Q (I (S (j)) + 1)$
691	690	breq1d	$⊢ i = I (S (j)) + 1 \to (Q (i) \leq L (E (S (j))) \leftrightarrow Q (I (S (j)) + 1) \leq L (E (S (j))))$
692	691	elrab	$⊢ I (S (j)) + 1 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \leftrightarrow (I (S (j)) + 1 \in (0 ..^M) \land Q (I (S (j)) + 1) \leq L (E (S (j))))$
693	688 689 692	sylanbrc	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to I (S (j)) + 1 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}$
694		suprub	$⊢ ((\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \subseteq ℝ \land \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} \neq \emptyset \land \exists x \in ℝ \forall l \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} l \leq x) \land I (S (j)) + 1 \in \{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\}) \to I (S (j)) + 1 \leq sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
695	596 641 649 693 694	syl31anc	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to I (S (j)) + 1 \leq sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <)$
696	63	eqcomd	$⊢ (φ \land j \in (0 ..^N)) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) = I (S (j))$
697	696	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (S (j)))\} ℝ <) = I (S (j))$
698	695 697	breqtrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to I (S (j)) + 1 \leq I (S (j))$
699	651	ltp1d	$⊢ (φ \land j \in (0 ..^N)) \to I (S (j)) < I (S (j)) + 1$
700	651 653	ltnled	$⊢ (φ \land j \in (0 ..^N)) \to (I (S (j)) < I (S (j)) + 1 \leftrightarrow \neg I (S (j)) + 1 \leq I (S (j)))$
701	699 700	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to \neg I (S (j)) + 1 \leq I (S (j))$
702	701	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \land Q (I (S (j)) + 1) \leq L (E (S (j)))) \to \neg I (S (j)) + 1 \leq I (S (j))$
703	698 702	pm2.65da	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to \neg Q (I (S (j)) + 1) \leq L (E (S (j)))$
704	562	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to L (E (S (j))) \in ℝ$
705	51	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to Q (I (S (j)) + 1) \in ℝ$
706	704 705	ltnled	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to (L (E (S (j))) < Q (I (S (j)) + 1) \leftrightarrow \neg Q (I (S (j)) + 1) \leq L (E (S (j))))$
707	703 706	mpbird	$⊢ ((φ \land j \in (0 ..^N)) \land \neg I (S (j)) = M - 1) \to L (E (S (j))) < Q (I (S (j)) + 1)$
708	707	adantlr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg I (S (j)) = M - 1) \to L (E (S (j))) < Q (I (S (j)) + 1)$
709	589 708	eqbrtrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg I (S (j)) = M - 1) \to E (S (j)) < Q (I (S (j)) + 1)$
710	588 709	pm2.61dan	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) < Q (I (S (j)) + 1)$
711	3	3ad2ant1	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to M \in ℕ$
712	4	3ad2ant1	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to Q \in P (M)$
713	5	3ad2ant1	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to C \in ℝ$
714	6	3ad2ant1	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to D \in ℝ$
715	7	3ad2ant1	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to C < D$
716	50	3adant3	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to I (S (j)) + 1 \in (0 \dots M)$
717		simp2	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to j \in (0 ..^N)$
718	43	leidd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j)$
719		elico2	$⊢ (S (j) \in ℝ \land S (j + 1) \in ℝ^{*}) \to (S (j) \in [S (j), S (j + 1)) \leftrightarrow (S (j) \in ℝ \land S (j) \leq S (j) \land S (j) < S (j + 1)))$
720	43 210 719	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (S (j) \in [S (j), S (j + 1)) \leftrightarrow (S (j) \in ℝ \land S (j) \leq S (j) \land S (j) < S (j + 1)))$
721	43 718 129 720	mpbir3and	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in [S (j), S (j + 1))$
722	721	3adant3	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to S (j) \in [S (j), S (j + 1))$
723		simp3	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to E (S (j)) < Q (I (S (j)) + 1)$
724		eqid	$⊢ Q (I (S (j)) + 1) - (E (S (j)) - S (j)) = Q (I (S (j)) + 1) - (E (S (j)) - S (j))$
725	1 2 711 712 713 714 715 8 9 10 11 12 716 717 722 723 724	fourierdlem63	$⊢ (φ \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to E (S (j + 1)) \leq Q (I (S (j)) + 1)$
726	725	3adant1r	$⊢ ((φ \land S (j) \in ℝ) \land j \in (0 ..^N) \land E (S (j)) < Q (I (S (j)) + 1)) \to E (S (j + 1)) \leq Q (I (S (j)) + 1)$
727	540 541 710 726	syl3anc	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j + 1)) \leq Q (I (S (j)) + 1)$
728	539 727	pm2.61dan	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) \leq Q (I (S (j)) + 1)$
729		ioossioo	$⊢ ((Q (I (S (j))) \in ℝ^{} \land Q (I (S (j)) + 1) \in ℝ^{}) \land (Q (I (S (j))) \leq L (E (S (j))) \land E (S (j + 1)) \leq Q (I (S (j)) + 1))) \to (L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))$
730	46 52 90 728 729	syl22anc	$⊢ (φ \land j \in (0 ..^N)) \to (L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))$

Metamath Proof Explorer

Theorem fourierdlem79

Proof