fourierdlem65

Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem65.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))\})$
2		fourierdlem65.t	$⊢ T = B - A$
3		fourierdlem65.m	$⊢ φ \to M \in ℕ$
4		fourierdlem65.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem65.c	$⊢ φ \to C \in ℝ$
6		fourierdlem65.d	$⊢ φ \to D \in (C, +∞)$
7		fourierdlem65.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))\})$
8		fourierdlem65.n	$⊢ N = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
9		fourierdlem65.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
10		fourierdlem65.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
11		fourierdlem65.l	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
12		fourierdlem65.z	$⊢ Z = S (j) + B - E (S (j))$
13	11	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
14		simpr	$⊢ (E (S (j)) = B \land y = E (S (j))) \to y = E (S (j))$
15		simpl	$⊢ (E (S (j)) = B \land y = E (S (j))) \to E (S (j)) = B$
16	14 15	eqtrd	$⊢ (E (S (j)) = B \land y = E (S (j))) \to y = B$
17	16	iftrued	$⊢ (E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = A$
18	17	adantll	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land y = E (S (j))) \to if (y = B, A, y) = A$
19	1 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
20	19	simp1d	$⊢ φ \to A \in ℝ$
21	19	simp2d	$⊢ φ \to B \in ℝ$
22	19	simp3d	$⊢ φ \to A < B$
23	20 21 22 2 10	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
24	23	adantr	$⊢ (φ \land j \in (0 ..^N)) \to E : ℝ ⟶ (A, B]$
25		ioossre	$⊢ (C, +∞) \subseteq ℝ$
26	25 6	sseldi	$⊢ φ \to D \in ℝ$
27	5	rexrd	$⊢ φ \to C \in ℝ^{*}$
28		pnfxr	$⊢ +∞ \in ℝ^{*}$
29	28	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
30		ioogtlb	$⊢ (C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in (C, +∞)) \to C < D$
31	27 29 6 30	syl3anc	$⊢ φ \to C < D$
32		id	$⊢ y = x \to y = x$
33	2	eqcomi	$⊢ B - A = T$
34	33	oveq2i	$⊢ k (B - A) = k T$
35	34	a1i	$⊢ y = x \to k (B - A) = k T$
36	32 35	oveq12d	$⊢ y = x \to y + k (B - A) = x + k T$
37	36	eleq1d	$⊢ y = x \to (y + k (B - A) \in ran Q \leftrightarrow x + k T \in ran Q)$
38	37	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k (B - A) \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
39	38	cbvrabv	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
40	39	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
41	2 1 3 4 5 26 31 7 40 8 9	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
42	41	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
43	42	simprd	$⊢ φ \to S \in O (N)$
44	42	simpld	$⊢ φ \to N \in ℕ$
45	7	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))))$
46	44 45	syl	$⊢ φ \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))))$
47	43 46	mpbid	$⊢ φ \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)))$
48	47	simpld	$⊢ φ \to S \in (ℝ^{(0 \dots N)})$
49		elmapi	$⊢ S \in (ℝ^{(0 \dots N)}) \to S : (0 \dots N) ⟶ ℝ$
50	48 49	syl	$⊢ φ \to S : (0 \dots N) ⟶ ℝ$
51	50	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S : (0 \dots N) ⟶ ℝ$
52		elfzofz	$⊢ j \in (0 ..^N) \to j \in (0 \dots N)$
53	52	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 \dots N)$
54	51 53	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℝ$
55	24 54	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in (A, B]$
56	55	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j)) \in (A, B]$
57	20	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A \in ℝ$
58	13 18 56 57	fvmptd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to L (E (S (j))) = A$
59	58	oveq2d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) - L (E (S (j))) = E (S (j + 1)) - A$
60	21	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to B \in ℝ$
61	22	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A < B$
62	54	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) \in ℝ$
63		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j)) = B$
64		fzofzp1	$⊢ j \in (0 ..^N) \to j + 1 \in (0 \dots N)$
65	64	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j + 1 \in (0 \dots N)$
66	51 65	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℝ$
67	66	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) \in ℝ$
68		elfzoelz	$⊢ j \in (0 ..^N) \to j \in ℤ$
69	68	zred	$⊢ j \in (0 ..^N) \to j \in ℝ$
70	69	adantl	$⊢ (φ \land j \in (0 ..^N)) \to j \in ℝ$
71	70	ltp1d	$⊢ (φ \land j \in (0 ..^N)) \to j < j + 1$
72	41	simprd	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
73	72	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
74		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}) \land (j \in (0 \dots N) \land j + 1 \in (0 \dots N))) \to (j < j + 1 \leftrightarrow S (j) < S (j + 1))$
75	73 53 65 74	syl12anc	$⊢ (φ \land j \in (0 ..^N)) \to (j < j + 1 \leftrightarrow S (j) < S (j + 1))$
76	71 75	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j + 1)$
77	76	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) < S (j + 1)$
78		isof1o	$⊢ S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}) \to S : (0 \dots N) \underset{1-1 onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
79		f1ofo	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \to S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
80	72 78 79	3syl	$⊢ φ \to S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
81	80	ad3antrrr	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
82	5	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to C \in ℝ$
83	26	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to D \in ℝ$
84	21 20	resubcld	$⊢ φ \to B - A \in ℝ$
85	2 84	eqeltrid	$⊢ φ \to T \in ℝ$
86	85	adantr	$⊢ (φ \land j \in (0 ..^N)) \to T \in ℝ$
87	54 86	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + T \in ℝ$
88	87	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \in ℝ$
89	5	adantr	$⊢ (φ \land j \in (0 ..^N)) \to C \in ℝ$
90	7 44 43	fourierdlem15	$⊢ φ \to S : (0 \dots N) ⟶ [C, D]$
91	90	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S : (0 \dots N) ⟶ [C, D]$
92	91 53	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in [C, D]$
93	26	adantr	$⊢ (φ \land j \in (0 ..^N)) \to D \in ℝ$
94		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (S (j) \in [C, D] \leftrightarrow (S (j) \in ℝ \land C \leq S (j) \land S (j) \leq D))$
95	89 93 94	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (S (j) \in [C, D] \leftrightarrow (S (j) \in ℝ \land C \leq S (j) \land S (j) \leq D))$
96	92 95	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (S (j) \in ℝ \land C \leq S (j) \land S (j) \leq D)$
97	96	simp2d	$⊢ (φ \land j \in (0 ..^N)) \to C \leq S (j)$
98	20 21	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
99	22 98	mpbid	$⊢ φ \to 0 < B - A$
100	99 2	breqtrrdi	$⊢ φ \to 0 < T$
101	85 100	elrpd	$⊢ φ \to T \in ℝ^{+}$
102	101	adantr	$⊢ (φ \land j \in (0 ..^N)) \to T \in ℝ^{+}$
103	54 102	ltaddrpd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) < S (j) + T$
104	89 54 87 97 103	lelttrd	$⊢ (φ \land j \in (0 ..^N)) \to C < S (j) + T$
105	89 87 104	ltled	$⊢ (φ \land j \in (0 ..^N)) \to C \leq S (j) + T$
106	105	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to C \leq S (j) + T$
107	66	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j + 1) \in ℝ$
108		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to \neg S (j + 1) \leq S (j) + T$
109	88 107	ltnled	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to (S (j) + T < S (j + 1) \leftrightarrow \neg S (j + 1) \leq S (j) + T)$
110	108 109	mpbird	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T < S (j + 1)$
111	91 65	ffvelrnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in [C, D]$
112		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (S (j + 1) \in [C, D] \leftrightarrow (S (j + 1) \in ℝ \land C \leq S (j + 1) \land S (j + 1) \leq D))$
113	89 93 112	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to (S (j + 1) \in [C, D] \leftrightarrow (S (j + 1) \in ℝ \land C \leq S (j + 1) \land S (j + 1) \leq D))$
114	111 113	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (S (j + 1) \in ℝ \land C \leq S (j + 1) \land S (j + 1) \leq D)$
115	114	simp3d	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \leq D$
116	115	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j + 1) \leq D$
117	88 107 83 110 116	ltletrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T < D$
118	88 83 117	ltled	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \leq D$
119	82 83 88 106 118	eliccd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \in [C, D]$
120	119	adantlr	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \in [C, D]$
121	10	a1i	$⊢ (φ \land j \in (0 ..^N)) \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
122		id	$⊢ x = S (j) \to x = S (j)$
123		oveq2	$⊢ x = S (j) \to B - x = B - S (j)$
124	123	oveq1d	$⊢ x = S (j) \to \frac{B - x}{T} = \frac{B - S (j)}{T}$
125	124	fveq2d	$⊢ x = S (j) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (j)}{T}⌋$
126	125	oveq1d	$⊢ x = S (j) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (j)}{T}⌋ T$
127	122 126	oveq12d	$⊢ x = S (j) \to x + ⌊\frac{B - x}{T}⌋ T = S (j) + ⌊\frac{B - S (j)}{T}⌋ T$
128	127	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land x = S (j)) \to x + ⌊\frac{B - x}{T}⌋ T = S (j) + ⌊\frac{B - S (j)}{T}⌋ T$
129	21	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B \in ℝ$
130	129 54	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j) \in ℝ$
131	130 102	rerpdivcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j)}{T} \in ℝ$
132	131	flcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j)}{T}⌋ \in ℤ$
133	132	zred	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j)}{T}⌋ \in ℝ$
134	133 86	remulcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j)}{T}⌋ T \in ℝ$
135	54 134	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + ⌊\frac{B - S (j)}{T}⌋ T \in ℝ$
136	121 128 54 135	fvmptd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) = S (j) + ⌊\frac{B - S (j)}{T}⌋ T$
137	136	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) - S (j) = S (j) + ⌊\frac{B - S (j)}{T}⌋ T - S (j)$
138	137	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{E (S (j)) - S (j)}{T} = \frac{S (j) + ⌊\frac{B - S (j)}{T}⌋ T - S (j)}{T}$
139	54	recnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℂ$
140	134	recnd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j)}{T}⌋ T \in ℂ$
141	139 140	pncan2d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + ⌊\frac{B - S (j)}{T}⌋ T - S (j) = ⌊\frac{B - S (j)}{T}⌋ T$
142	141	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{S (j) + ⌊\frac{B - S (j)}{T}⌋ T - S (j)}{T} = \frac{⌊\frac{B - S (j)}{T}⌋ T}{T}$
143	133	recnd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j)}{T}⌋ \in ℂ$
144	86	recnd	$⊢ (φ \land j \in (0 ..^N)) \to T \in ℂ$
145	102	rpne0d	$⊢ (φ \land j \in (0 ..^N)) \to T \neq 0$
146	143 144 145	divcan4d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{⌊\frac{B - S (j)}{T}⌋ T}{T} = ⌊\frac{B - S (j)}{T}⌋$
147	138 142 146	3eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{E (S (j)) - S (j)}{T} = ⌊\frac{B - S (j)}{T}⌋$
148	147 132	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{E (S (j)) - S (j)}{T} \in ℤ$
149		peano2zm	$⊢ \frac{E (S (j)) - S (j)}{T} \in ℤ \to (\frac{E (S (j)) - S (j)}{T}) - 1 \in ℤ$
150	148 149	syl	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) - 1 \in ℤ$
151	150	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to (\frac{E (S (j)) - S (j)}{T}) - 1 \in ℤ$
152	33	oveq2i	$⊢ ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) = ((\frac{E (S (j)) - S (j)}{T}) - 1) T$
153	152	oveq2i	$⊢ S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T$
154	153	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T$
155	136	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j)) = S (j) + ⌊\frac{B - S (j)}{T}⌋ T$
156		oveq1	$⊢ E (S (j)) = B \to E (S (j)) - S (j) = B - S (j)$
157	156	eqcomd	$⊢ E (S (j)) = B \to B - S (j) = E (S (j)) - S (j)$
158	157	oveq1d	$⊢ E (S (j)) = B \to \frac{B - S (j)}{T} = \frac{E (S (j)) - S (j)}{T}$
159	158	fveq2d	$⊢ E (S (j)) = B \to ⌊\frac{B - S (j)}{T}⌋ = ⌊\frac{E (S (j)) - S (j)}{T}⌋$
160	159	oveq1d	$⊢ E (S (j)) = B \to ⌊\frac{B - S (j)}{T}⌋ T = ⌊\frac{E (S (j)) - S (j)}{T}⌋ T$
161	160	oveq2d	$⊢ E (S (j)) = B \to S (j) + ⌊\frac{B - S (j)}{T}⌋ T = S (j) + ⌊\frac{E (S (j)) - S (j)}{T}⌋ T$
162	161	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + ⌊\frac{B - S (j)}{T}⌋ T = S (j) + ⌊\frac{E (S (j)) - S (j)}{T}⌋ T$
163	147 143	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{E (S (j)) - S (j)}{T} \in ℂ$
164		1cnd	$⊢ (φ \land j \in (0 ..^N)) \to 1 \in ℂ$
165	163 164 144	subdird	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{E (S (j)) - S (j)}{T}) - 1) T = (\frac{E (S (j)) - S (j)}{T}) T - 1 T$
166	85	recnd	$⊢ φ \to T \in ℂ$
167	166	mulid2d	$⊢ φ \to 1 T = T$
168	167	oveq2d	$⊢ φ \to (\frac{E (S (j)) - S (j)}{T}) T - 1 T = (\frac{E (S (j)) - S (j)}{T}) T - T$
169	168	adantr	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) T - 1 T = (\frac{E (S (j)) - S (j)}{T}) T - T$
170	165 169	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{E (S (j)) - S (j)}{T}) - 1) T = (\frac{E (S (j)) - S (j)}{T}) T - T$
171	170	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) T - T)$
172	163 144	mulcld	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) T \in ℂ$
173	139 144 172	ppncand	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) T - T) = S (j) + (\frac{E (S (j)) - S (j)}{T}) T$
174		flid	$⊢ \frac{E (S (j)) - S (j)}{T} \in ℤ \to ⌊\frac{E (S (j)) - S (j)}{T}⌋ = \frac{E (S (j)) - S (j)}{T}$
175	148 174	syl	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{E (S (j)) - S (j)}{T}⌋ = \frac{E (S (j)) - S (j)}{T}$
176	175	eqcomd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{E (S (j)) - S (j)}{T} = ⌊\frac{E (S (j)) - S (j)}{T}⌋$
177	176	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) T = ⌊\frac{E (S (j)) - S (j)}{T}⌋ T$
178	177	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + (\frac{E (S (j)) - S (j)}{T}) T = S (j) + ⌊\frac{E (S (j)) - S (j)}{T}⌋ T$
179	171 173 178	3eqtrrd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + ⌊\frac{E (S (j)) - S (j)}{T}⌋ T = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T$
180	179	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + ⌊\frac{E (S (j)) - S (j)}{T}⌋ T = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T$
181	155 162 180	3eqtrrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) T = E (S (j))$
182	154 181 63	3eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) = B$
183	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
184	3 183	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))))$
185	4 184	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)))$
186	185	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
187	186	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
188	187	simprd	$⊢ φ \to Q (M) = B$
189	188	eqcomd	$⊢ φ \to B = Q (M)$
190	1 3 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
191		ffn	$⊢ Q : (0 \dots M) ⟶ [A, B] \to Q Fn (0 \dots M)$
192	190 191	syl	$⊢ φ \to Q Fn (0 \dots M)$
193	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
194		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
195	193 194	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
196		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
197	195 196	syl	$⊢ φ \to M \in (0 \dots M)$
198		fnfvelrn	$⊢ (Q Fn (0 \dots M) \land M \in (0 \dots M)) \to Q (M) \in ran Q$
199	192 197 198	syl2anc	$⊢ φ \to Q (M) \in ran Q$
200	189 199	eqeltrd	$⊢ φ \to B \in ran Q$
201	200	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to B \in ran Q$
202	182 201	eqeltrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) \in ran Q$
203	202	adantr	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) \in ran Q$
204		oveq1	$⊢ k = (\frac{E (S (j)) - S (j)}{T}) - 1 \to k (B - A) = ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A)$
205	204	oveq2d	$⊢ k = (\frac{E (S (j)) - S (j)}{T}) - 1 \to S (j) + T + k (B - A) = S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A)$
206	205	eleq1d	$⊢ k = (\frac{E (S (j)) - S (j)}{T}) - 1 \to (S (j) + T + k (B - A) \in ran Q \leftrightarrow S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) \in ran Q)$
207	206	rspcev	$⊢ ((\frac{E (S (j)) - S (j)}{T}) - 1 \in ℤ \land S (j) + T + ((\frac{E (S (j)) - S (j)}{T}) - 1) (B - A) \in ran Q) \to \exists k \in ℤ S (j) + T + k (B - A) \in ran Q$
208	151 203 207	syl2anc	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to \exists k \in ℤ S (j) + T + k (B - A) \in ran Q$
209		oveq1	$⊢ y = S (j) + T \to y + k (B - A) = S (j) + T + k (B - A)$
210	209	eleq1d	$⊢ y = S (j) + T \to (y + k (B - A) \in ran Q \leftrightarrow S (j) + T + k (B - A) \in ran Q)$
211	210	rexbidv	$⊢ y = S (j) + T \to (\exists k \in ℤ y + k (B - A) \in ran Q \leftrightarrow \exists k \in ℤ S (j) + T + k (B - A) \in ran Q)$
212	211	elrab	$⊢ S (j) + T \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \leftrightarrow (S (j) + T \in [C, D] \land \exists k \in ℤ S (j) + T + k (B - A) \in ran Q)$
213	120 208 212	sylanbrc	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
214		elun2	$⊢ S (j) + T \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \to S (j) + T \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
215	213 214	syl	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to S (j) + T \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
216		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \land S (j) + T \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})) \to \exists i \in (0 \dots N) S (j) + T = S (i)$
217	81 215 216	syl2anc	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to \exists i \in (0 \dots N) S (j) + T = S (i)$
218		eqcom	$⊢ S (j) + T = S (i) \leftrightarrow S (i) = S (j) + T$
219	218	rexbii	$⊢ \exists i \in (0 \dots N) S (j) + T = S (i) \leftrightarrow \exists i \in (0 \dots N) S (i) = S (j) + T$
220	217 219	sylib	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to \exists i \in (0 \dots N) S (i) = S (j) + T$
221	103	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to S (j) < S (j) + T$
222	218	biimpri	$⊢ S (i) = S (j) + T \to S (j) + T = S (i)$
223	222	adantl	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to S (j) + T = S (i)$
224	221 223	breqtrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to S (j) < S (i)$
225	110	adantr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to S (j) + T < S (j + 1)$
226	223 225	eqbrtrrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to S (i) < S (j + 1)$
227	224 226	jca	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land S (i) = S (j) + T) \to (S (j) < S (i) \land S (i) < S (j + 1))$
228	227	adantlr	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land i \in (0 \dots N)) \land S (i) = S (j) + T) \to (S (j) < S (i) \land S (i) < S (j + 1))$
229		simplll	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land i \in (0 \dots N)) \land S (i) = S (j) + T) \to (φ \land j \in (0 ..^N))$
230		simplr	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land i \in (0 \dots N)) \land S (i) = S (j) + T) \to i \in (0 \dots N)$
231		elfzelz	$⊢ i \in (0 \dots N) \to i \in ℤ$
232	231	ad2antlr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land (S (j) < S (i) \land S (i) < S (j + 1))) \to i \in ℤ$
233	68	ad3antlr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land (S (j) < S (i) \land S (i) < S (j + 1))) \to j \in ℤ$
234		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to S (j) < S (i)$
235	73	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
236	53	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to j \in (0 \dots N)$
237		simplr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to i \in (0 \dots N)$
238		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}) \land (j \in (0 \dots N) \land i \in (0 \dots N))) \to (j < i \leftrightarrow S (j) < S (i))$
239	235 236 237 238	syl12anc	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to (j < i \leftrightarrow S (j) < S (i))$
240	234 239	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to j < i$
241	240	adantrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land (S (j) < S (i) \land S (i) < S (j + 1))) \to j < i$
242		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to S (i) < S (j + 1)$
243	73	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
244		simplr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to i \in (0 \dots N)$
245	65	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to j + 1 \in (0 \dots N)$
246		isorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}) \land (i \in (0 \dots N) \land j + 1 \in (0 \dots N))) \to (i < j + 1 \leftrightarrow S (i) < S (j + 1))$
247	243 244 245 246	syl12anc	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to (i < j + 1 \leftrightarrow S (i) < S (j + 1))$
248	242 247	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to i < j + 1$
249	248	adantrl	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land (S (j) < S (i) \land S (i) < S (j + 1))) \to i < j + 1$
250		btwnnz	$⊢ (j \in ℤ \land j < i \land i < j + 1) \to \neg i \in ℤ$
251	233 241 249 250	syl3anc	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land (S (j) < S (i) \land S (i) < S (j + 1))) \to \neg i \in ℤ$
252	232 251	pm2.65da	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \to \neg (S (j) < S (i) \land S (i) < S (j + 1))$
253	229 230 252	syl2anc	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land i \in (0 \dots N)) \land S (i) = S (j) + T) \to \neg (S (j) < S (i) \land S (i) < S (j + 1))$
254	228 253	pm2.65da	$⊢ (((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \land i \in (0 \dots N)) \to \neg S (i) = S (j) + T$
255	254	nrexdv	$⊢ ((φ \land j \in (0 ..^N)) \land \neg S (j + 1) \leq S (j) + T) \to \neg \exists i \in (0 \dots N) S (i) = S (j) + T$
256	255	adantlr	$⊢ (((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \land \neg S (j + 1) \leq S (j) + T) \to \neg \exists i \in (0 \dots N) S (i) = S (j) + T$
257	220 256	condan	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) \leq S (j) + T$
258	62	rexrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) \in ℝ^{*}$
259	85	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to T \in ℝ$
260	62 259	readdcld	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T \in ℝ$
261		elioc2	$⊢ (S (j) \in ℝ^{*} \land S (j) + T \in ℝ) \to (S (j + 1) \in (S (j), S (j) + T] \leftrightarrow (S (j + 1) \in ℝ \land S (j) < S (j + 1) \land S (j + 1) \leq S (j) + T))$
262	258 260 261	syl2anc	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to (S (j + 1) \in (S (j), S (j) + T] \leftrightarrow (S (j + 1) \in ℝ \land S (j) < S (j + 1) \land S (j + 1) \leq S (j) + T))$
263	67 77 257 262	mpbir3and	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) \in (S (j), S (j) + T]$
264	57 60 61 2 10 62 63 263	fourierdlem26	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) = A + S (j + 1) - S (j)$
265	264	oveq1d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) - A = A + (S (j + 1) - S (j)) - A$
266	57	recnd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A \in ℂ$
267	66	recnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℂ$
268	267 139	subcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) - S (j) \in ℂ$
269	268	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) - S (j) \in ℂ$
270	266 269	pncan2d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A + (S (j + 1) - S (j)) - A = S (j + 1) - S (j)$
271	59 265 270	3eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j)$
272	11	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
273		eqcom	$⊢ y = E (S (j)) \leftrightarrow E (S (j)) = y$
274	273	biimpi	$⊢ y = E (S (j)) \to E (S (j)) = y$
275	274	adantl	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to E (S (j)) = y$
276		neqne	$⊢ \neg E (S (j)) = B \to E (S (j)) \neq B$
277	276	adantr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to E (S (j)) \neq B$
278	275 277	eqnetrrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y \neq B$
279	278	neneqd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to \neg y = B$
280	279	iffalsed	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = y$
281		simpr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y = E (S (j))$
282	280 281	eqtrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = E (S (j))$
283	282	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))$
284	55	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in (A, B]$
285	272 283 284 284	fvmptd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L (E (S (j))) = E (S (j))$
286	285	oveq2d	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j + 1)) - L (E (S (j))) = E (S (j + 1)) - E (S (j))$
287		id	$⊢ x = S (j + 1) \to x = S (j + 1)$
288		oveq2	$⊢ x = S (j + 1) \to B - x = B - S (j + 1)$
289	288	oveq1d	$⊢ x = S (j + 1) \to \frac{B - x}{T} = \frac{B - S (j + 1)}{T}$
290	289	fveq2d	$⊢ x = S (j + 1) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋$
291	290	oveq1d	$⊢ x = S (j + 1) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (j + 1)}{T}⌋ T$
292	287 291	oveq12d	$⊢ x = S (j + 1) \to x + ⌊\frac{B - x}{T}⌋ T = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T$
293	292	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land x = S (j + 1)) \to x + ⌊\frac{B - x}{T}⌋ T = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T$
294	129 66	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j + 1) \in ℝ$
295	294 102	rerpdivcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} \in ℝ$
296	295	flcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℤ$
297	296	zred	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ$
298	297 86	remulcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ T \in ℝ$
299	66 298	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T \in ℝ$
300	121 293 66 299	fvmptd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T$
301	300 136	oveq12d	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) - E (S (j)) = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T)$
302	301	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j + 1)) - E (S (j)) = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T)$
303		flle	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j + 1)}{T}$
304	295 303	syl	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j + 1)}{T}$
305	54 66 76	ltled	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j + 1)$
306	54 66 129 305	lesub2dd	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j + 1) \leq B - S (j)$
307	294 130 102 306	lediv1dd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} \leq \frac{B - S (j)}{T}$
308	297 295 131 304 307	letrd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T}$
309	308	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T}$
310	297	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ$
311		1red	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to 1 \in ℝ$
312	310 311	readdcld	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℝ$
313	131	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to \frac{B - S (j)}{T} \in ℝ$
314		simpr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
315	312 313 314	nltled	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}$
316	315	adantlr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}$
317	80	ad3antrrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
318	89	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to C \in ℝ$
319	93	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to D \in ℝ$
320	136 135	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in ℝ$
321	129 320	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) \in ℝ$
322	54 321	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) \in ℝ$
323	12 322	eqeltrid	$⊢ (φ \land j \in (0 ..^N)) \to Z \in ℝ$
324	323	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z \in ℝ$
325	20	rexrd	$⊢ φ \to A \in ℝ^{*}$
326	325	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ^{*}$
327		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))$
328	326 129 327	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))$
329	55 328	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (E (S (j)) \in ℝ \land A < E (S (j)) \land E (S (j)) \leq B)$
330	329	simp3d	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \leq B$
331	129 320	subge0d	$⊢ (φ \land j \in (0 ..^N)) \to (0 \leq B - E (S (j)) \leftrightarrow E (S (j)) \leq B)$
332	330 331	mpbird	$⊢ (φ \land j \in (0 ..^N)) \to 0 \leq B - E (S (j))$
333	54 321	addge01d	$⊢ (φ \land j \in (0 ..^N)) \to (0 \leq B - E (S (j)) \leftrightarrow S (j) \leq S (j) + B - E (S (j)))$
334	332 333	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j) + B - E (S (j))$
335	89 54 322 97 334	letrd	$⊢ (φ \land j \in (0 ..^N)) \to C \leq S (j) + B - E (S (j))$
336	335 12	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to C \leq Z$
337	336	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to C \leq Z$
338	66	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to S (j + 1) \in ℝ$
339	295	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - S (j + 1)}{T} \in ℝ$
340		reflcl	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ$
341		peano2re	$⊢ ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℝ$
342	339 340 341	3syl	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℝ$
343	129	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to B \in ℝ$
344	343 324	resubcld	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to B - Z \in ℝ$
345	102	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to T \in ℝ^{+}$
346	344 345	rerpdivcld	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - Z}{T} \in ℝ$
347		flltp1	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to \frac{B - S (j + 1)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
348	295 347	syl	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
349	348	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - S (j + 1)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
350	296	peano2zd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℤ$
351	350	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℤ$
352	131	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - S (j)}{T} \in ℝ$
353		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}$
354	321 102	rerpdivcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} \in ℝ$
355	354	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - E (S (j))}{T} \in ℝ$
356	20	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ$
357	329	simp2d	$⊢ (φ \land j \in (0 ..^N)) \to A < E (S (j))$
358	356 320 129 357	ltsub2dd	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) < B - A$
359	358 2	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) < T$
360	321 86 102 359	ltdiv1dd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} < \frac{T}{T}$
361	144 145	dividd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{T}{T} = 1$
362	360 361	breqtrd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} < 1$
363	362	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - E (S (j))}{T} < 1$
364	130	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j) \in ℂ$
365	321	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) \in ℂ$
366	364 365 144 145	divsubdird	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j) - (B - E (S (j)))}{T} = (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T})$
367	366	eqcomd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) = \frac{B - S (j) - (B - E (S (j)))}{T}$
368	129	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B \in ℂ$
369	320	recnd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in ℂ$
370	368 139 369	nnncan1d	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j) - (B - E (S (j))) = E (S (j)) - S (j)$
371	370	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j) - (B - E (S (j)))}{T} = \frac{E (S (j)) - S (j)}{T}$
372	367 371	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) = \frac{E (S (j)) - S (j)}{T}$
373	372 148	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) \in ℤ$
374	373	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) \in ℤ$
375	351 352 353 355 363 374	zltlesub	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T})$
376	12	a1i	$⊢ (φ \land j \in (0 ..^N)) \to Z = S (j) + B - E (S (j))$
377	376	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to B - Z = B - (S (j) + B - E (S (j)))$
378	139 368 369	addsub12d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B + S (j) - E (S (j))$
379	368 369 139	subsub2d	$⊢ (φ \land j \in (0 ..^N)) \to B - (E (S (j)) - S (j)) = B + S (j) - E (S (j))$
380	378 379	eqtr4d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B - (E (S (j)) - S (j))$
381	380	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to B - (S (j) + B - E (S (j))) = B - (B - (E (S (j)) - S (j)))$
382	369 139	subcld	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) - S (j) \in ℂ$
383	368 382	nncand	$⊢ (φ \land j \in (0 ..^N)) \to B - (B - (E (S (j)) - S (j))) = E (S (j)) - S (j)$
384	377 381 383	3eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to B - Z = E (S (j)) - S (j)$
385	384	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - Z}{T} = \frac{E (S (j)) - S (j)}{T}$
386	371 367 385	3eqtr4d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) = \frac{B - Z}{T}$
387	386	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) = \frac{B - Z}{T}$
388	375 387	breqtrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - Z}{T}$
389	339 342 346 349 388	ltletrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \frac{B - S (j + 1)}{T} < \frac{B - Z}{T}$
390	294	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to B - S (j + 1) \in ℝ$
391	390 344 345	ltdiv1d	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (B - S (j + 1) < B - Z \leftrightarrow \frac{B - S (j + 1)}{T} < \frac{B - Z}{T})$
392	389 391	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to B - S (j + 1) < B - Z$
393	324 338 343	ltsub2d	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (Z < S (j + 1) \leftrightarrow B - S (j + 1) < B - Z)$
394	392 393	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z < S (j + 1)$
395	115	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to S (j + 1) \leq D$
396	324 338 319 394 395	ltletrd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z < D$
397	324 319 396	ltled	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z \leq D$
398	318 319 324 337 397	eliccd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z \in [C, D]$
399	33	a1i	$⊢ (φ \land j \in (0 ..^N)) \to B - A = T$
400	399	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) (B - A) = (\frac{E (S (j)) - S (j)}{T}) T$
401	382 144 145	divcan1d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) T = E (S (j)) - S (j)$
402	400 401	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) (B - A) = E (S (j)) - S (j)$
403	376 402	oveq12d	$⊢ (φ \land j \in (0 ..^N)) \to Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) = S (j) + (B - E (S (j))) + (E (S (j)) - S (j))$
404	139 365	addcomd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B - E (S (j)) + S (j)$
405	404	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + (B - E (S (j))) + (E (S (j)) - S (j)) = (B - E (S (j))) + S (j) + (E (S (j)) - S (j))$
406	365 139 369	ppncand	$⊢ (φ \land j \in (0 ..^N)) \to (B - E (S (j))) + S (j) + (E (S (j)) - S (j)) = B - E (S (j)) + E (S (j))$
407	368 369	npcand	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) + E (S (j)) = B$
408	406 407	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (B - E (S (j))) + S (j) + (E (S (j)) - S (j)) = B$
409	403 405 408	3eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) = B$
410	200	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B \in ran Q$
411	409 410	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) \in ran Q$
412		oveq1	$⊢ k = \frac{E (S (j)) - S (j)}{T} \to k (B - A) = (\frac{E (S (j)) - S (j)}{T}) (B - A)$
413	412	oveq2d	$⊢ k = \frac{E (S (j)) - S (j)}{T} \to Z + k (B - A) = Z + (\frac{E (S (j)) - S (j)}{T}) (B - A)$
414	413	eleq1d	$⊢ k = \frac{E (S (j)) - S (j)}{T} \to (Z + k (B - A) \in ran Q \leftrightarrow Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) \in ran Q)$
415	414	rspcev	$⊢ (\frac{E (S (j)) - S (j)}{T} \in ℤ \land Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) \in ran Q) \to \exists k \in ℤ Z + k (B - A) \in ran Q$
416	148 411 415	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to \exists k \in ℤ Z + k (B - A) \in ran Q$
417	416	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \exists k \in ℤ Z + k (B - A) \in ran Q$
418		oveq1	$⊢ y = Z \to y + k (B - A) = Z + k (B - A)$
419	418	eleq1d	$⊢ y = Z \to (y + k (B - A) \in ran Q \leftrightarrow Z + k (B - A) \in ran Q)$
420	419	rexbidv	$⊢ y = Z \to (\exists k \in ℤ y + k (B - A) \in ran Q \leftrightarrow \exists k \in ℤ Z + k (B - A) \in ran Q)$
421	420	elrab	$⊢ Z \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \leftrightarrow (Z \in [C, D] \land \exists k \in ℤ Z + k (B - A) \in ran Q)$
422	398 417 421	sylanbrc	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
423		elun2	$⊢ Z \in \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \to Z \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
424	422 423	syl	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to Z \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
425		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \land Z \in (\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})) \to \exists i \in (0 \dots N) Z = S (i)$
426	317 424 425	syl2anc	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \exists i \in (0 \dots N) Z = S (i)$
427	54	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) \in ℝ$
428	321	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B - E (S (j)) \in ℝ$
429	320	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in ℝ$
430	21	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \in ℝ$
431	330	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \leq B$
432	276	necomd	$⊢ \neg E (S (j)) = B \to B \neq E (S (j))$
433	432	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \neq E (S (j))$
434	429 430 431 433	leneltd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) < B$
435	429 430	posdifd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to (E (S (j)) < B \leftrightarrow 0 < B - E (S (j)))$
436	434 435	mpbid	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to 0 < B - E (S (j))$
437	428 436	elrpd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B - E (S (j)) \in ℝ^{+}$
438	427 437	ltaddrpd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) < S (j) + B - E (S (j))$
439	438 12	breqtrrdi	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) < Z$
440	439	ad2antrr	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to S (j) < Z$
441		simpr	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to Z = S (i)$
442	440 441	breqtrd	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to S (j) < S (i)$
443	394	adantr	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to Z < S (j + 1)$
444	441 443	eqbrtrrd	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to S (i) < S (j + 1)$
445	442 444	jca	$⊢ ((((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \land Z = S (i)) \to (S (j) < S (i) \land S (i) < S (j + 1))$
446	445	ex	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (Z = S (i) \to (S (j) < S (i) \land S (i) < S (j + 1)))$
447	446	reximdv	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to (\exists i \in (0 \dots N) Z = S (i) \to \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1)))$
448	426 447	mpd	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \leq \frac{B - S (j)}{T}) \to \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1))$
449	316 448	syldan	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1))$
450	252	nrexdv	$⊢ (φ \land j \in (0 ..^N)) \to \neg \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1))$
451	450	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to \neg \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1))$
452	449 451	condan	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
453	309 452	jca	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to (⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T} \land \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1)$
454	131	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to \frac{B - S (j)}{T} \in ℝ$
455	296	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℤ$
456		flbi	$⊢ (\frac{B - S (j)}{T} \in ℝ \land ⌊\frac{B - S (j + 1)}{T}⌋ \in ℤ) \to (⌊\frac{B - S (j)}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋ \leftrightarrow (⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T} \land \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1))$
457	454 455 456	syl2anc	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to (⌊\frac{B - S (j)}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋ \leftrightarrow (⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T} \land \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1))$
458	453 457	mpbird	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j)}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋$
459	458	eqcomd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ = ⌊\frac{B - S (j)}{T}⌋$
460	459	oveq1d	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ T = ⌊\frac{B - S (j)}{T}⌋ T$
461	460	oveq2d	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T = S (j + 1) + ⌊\frac{B - S (j)}{T}⌋ T$
462	461	oveq1d	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T) = S (j + 1) + ⌊\frac{B - S (j)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T)$
463	267	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) \in ℂ$
464	139	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) \in ℂ$
465	140	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j)}{T}⌋ T \in ℂ$
466	463 464 465	pnpcan2d	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) + ⌊\frac{B - S (j)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T) = S (j + 1) - S (j)$
467	462 466	eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T - (S (j) + ⌊\frac{B - S (j)}{T}⌋ T) = S (j + 1) - S (j)$
468	286 302 467	3eqtrd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j)$
469	271 468	pm2.61dan	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j)$

Metamath Proof Explorer

Theorem fourierdlem65

Proof