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