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	sselid	$⊢ φ \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	ffvelcdmd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \in ℝ$
55	24 54	ffvelcdmd	$⊢ (φ \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	ffvelcdmd	$⊢ (φ \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	ffvelcdmd	$⊢ (φ \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	ffvelcdmd	$⊢ (φ \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	mullidd	$⊢ φ \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	bilanri	$⊢ (((φ \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)$
223	221 222	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)$
224	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)$
225	222 224	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)$
226	223 225	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))$
227	226	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))$
228		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))$
229		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)$
230		elfzelz	$⊢ i \in (0 \dots N) \to i \in ℤ$
231	230	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 ℤ$
232	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 ℤ$
233		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to S (j) < S (i)$
234	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\})$
235	53	ad2antrr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to j \in (0 \dots N)$
236		simplr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to i \in (0 \dots N)$
237		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))$
238	234 235 236 237	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))$
239	233 238	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (j) < S (i)) \to j < i$
240	239	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$
241		simpr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to S (i) < S (j + 1)$
242	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\})$
243		simplr	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to i \in (0 \dots N)$
244	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)$
245		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))$
246	242 243 244 245	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))$
247	241 246	mpbird	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 \dots N)) \land S (i) < S (j + 1)) \to i < j + 1$
248	247	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$
249		btwnnz	$⊢ (j \in ℤ \land j < i \land i < j + 1) \to \neg i \in ℤ$
250	232 240 248 249	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 ℤ$
251	231 250	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))$
252	228 229 251	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))$
253	227 252	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$
254	253	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$
255	254	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$
256	220 255	condan	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) \leq S (j) + T$
257	62	rexrd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) \in ℝ^{*}$
258	85	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to T \in ℝ$
259	62 258	readdcld	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j) + T \in ℝ$
260		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))$
261	257 259 260	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))$
262	67 77 256 261	mpbir3and	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) \in (S (j), S (j) + T]$
263	57 60 61 2 10 62 63 262	fourierdlem26	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) = A + S (j + 1) - S (j)$
264	263	oveq1d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to E (S (j + 1)) - A = A + (S (j + 1) - S (j)) - A$
265	57	recnd	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A \in ℂ$
266	66	recnd	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) \in ℂ$
267	266 139	subcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) - S (j) \in ℂ$
268	267	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to S (j + 1) - S (j) \in ℂ$
269	265 268	pncan2d	$⊢ ((φ \land j \in (0 ..^N)) \land E (S (j)) = B) \to A + (S (j + 1) - S (j)) - A = S (j + 1) - S (j)$
270	59 264 269	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)$
271	11	a1i	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L = (y \in (A, B] ⟼ if (y = B, A, y))$
272		eqcom	$⊢ y = E (S (j)) \leftrightarrow E (S (j)) = y$
273	272	bilani	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to E (S (j)) = y$
274		neqne	$⊢ \neg E (S (j)) = B \to E (S (j)) \neq B$
275	274	adantr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to E (S (j)) \neq B$
276	273 275	eqnetrrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y \neq B$
277	276	neneqd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to \neg y = B$
278	277	iffalsed	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = y$
279		simpr	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to y = E (S (j))$
280	278 279	eqtrd	$⊢ (\neg E (S (j)) = B \land y = E (S (j))) \to if (y = B, A, y) = E (S (j))$
281	280	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))$
282	55	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in (A, B]$
283	271 281 282 282	fvmptd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to L (E (S (j))) = E (S (j))$
284	283	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))$
285		id	$⊢ x = S (j + 1) \to x = S (j + 1)$
286		oveq2	$⊢ x = S (j + 1) \to B - x = B - S (j + 1)$
287	286	oveq1d	$⊢ x = S (j + 1) \to \frac{B - x}{T} = \frac{B - S (j + 1)}{T}$
288	287	fveq2d	$⊢ x = S (j + 1) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋$
289	288	oveq1d	$⊢ x = S (j + 1) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (j + 1)}{T}⌋ T$
290	285 289	oveq12d	$⊢ x = S (j + 1) \to x + ⌊\frac{B - x}{T}⌋ T = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T$
291	290	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$
292	129 66	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j + 1) \in ℝ$
293	292 102	rerpdivcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} \in ℝ$
294	293	flcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℤ$
295	294	zred	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ$
296	295 86	remulcld	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ T \in ℝ$
297	66 296	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T \in ℝ$
298	121 291 66 297	fvmptd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) = S (j + 1) + ⌊\frac{B - S (j + 1)}{T}⌋ T$
299	298 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)$
300	299	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)$
301		flle	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j + 1)}{T}$
302	293 301	syl	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j + 1)}{T}$
303	54 66 76	ltled	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j + 1)$
304	54 66 129 303	lesub2dd	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j + 1) \leq B - S (j)$
305	292 130 102 304	lediv1dd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} \leq \frac{B - S (j)}{T}$
306	295 293 131 302 305	letrd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ \leq \frac{B - S (j)}{T}$
307	306	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}$
308	295	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 ℝ$
309		1red	$⊢ ((φ \land j \in (0 ..^N)) \land \neg \frac{B - S (j)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1) \to 1 \in ℝ$
310	308 309	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 ℝ$
311	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 ℝ$
312		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$
313	310 311 312	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}$
314	313	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}$
315	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\}$
316	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 ℝ$
317	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 ℝ$
318	136 135	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in ℝ$
319	129 318	resubcld	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) \in ℝ$
320	54 319	readdcld	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) \in ℝ$
321	12 320	eqeltrid	$⊢ (φ \land j \in (0 ..^N)) \to Z \in ℝ$
322	321	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 ℝ$
323	20	rexrd	$⊢ φ \to A \in ℝ^{*}$
324	323	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ^{*}$
325		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))$
326	324 129 325	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))$
327	55 326	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to (E (S (j)) \in ℝ \land A < E (S (j)) \land E (S (j)) \leq B)$
328	327	simp3d	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \leq B$
329	129 318	subge0d	$⊢ (φ \land j \in (0 ..^N)) \to (0 \leq B - E (S (j)) \leftrightarrow E (S (j)) \leq B)$
330	328 329	mpbird	$⊢ (φ \land j \in (0 ..^N)) \to 0 \leq B - E (S (j))$
331	54 319	addge01d	$⊢ (φ \land j \in (0 ..^N)) \to (0 \leq B - E (S (j)) \leftrightarrow S (j) \leq S (j) + B - E (S (j)))$
332	330 331	mpbid	$⊢ (φ \land j \in (0 ..^N)) \to S (j) \leq S (j) + B - E (S (j))$
333	89 54 320 97 332	letrd	$⊢ (φ \land j \in (0 ..^N)) \to C \leq S (j) + B - E (S (j))$
334	333 12	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to C \leq Z$
335	334	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$
336	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 ℝ$
337	293	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 ℝ$
338		reflcl	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ$
339		peano2re	$⊢ ⌊\frac{B - S (j + 1)}{T}⌋ \in ℝ \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℝ$
340	337 338 339	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 ℝ$
341	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 ℝ$
342	341 322	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 ℝ$
343	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 ℝ^{+}$
344	342 343	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 ℝ$
345		flltp1	$⊢ \frac{B - S (j + 1)}{T} \in ℝ \to \frac{B - S (j + 1)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
346	293 345	syl	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j + 1)}{T} < ⌊\frac{B - S (j + 1)}{T}⌋ + 1$
347	346	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$
348	294	peano2zd	$⊢ (φ \land j \in (0 ..^N)) \to ⌊\frac{B - S (j + 1)}{T}⌋ + 1 \in ℤ$
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}⌋ + 1 \in ℤ$
350	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 ℝ$
351		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}$
352	319 102	rerpdivcld	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} \in ℝ$
353	352	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 ℝ$
354	20	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ$
355	327	simp2d	$⊢ (φ \land j \in (0 ..^N)) \to A < E (S (j))$
356	354 318 129 355	ltsub2dd	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) < B - A$
357	356 2	breqtrrdi	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) < T$
358	319 86 102 357	ltdiv1dd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} < \frac{T}{T}$
359	144 145	dividd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{T}{T} = 1$
360	358 359	breqtrd	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - E (S (j))}{T} < 1$
361	360	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$
362	130	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j) \in ℂ$
363	319	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) \in ℂ$
364	362 363 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})$
365	364	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}$
366	129	recnd	$⊢ (φ \land j \in (0 ..^N)) \to B \in ℂ$
367	318	recnd	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) \in ℂ$
368	366 139 367	nnncan1d	$⊢ (φ \land j \in (0 ..^N)) \to B - S (j) - (B - E (S (j))) = E (S (j)) - S (j)$
369	368	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - S (j) - (B - E (S (j)))}{T} = \frac{E (S (j)) - S (j)}{T}$
370	365 369	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}$
371	370 148	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) \in ℤ$
372	371	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 ℤ$
373	349 350 351 353 361 372	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})$
374	12	a1i	$⊢ (φ \land j \in (0 ..^N)) \to Z = S (j) + B - E (S (j))$
375	374	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to B - Z = B - (S (j) + B - E (S (j)))$
376	139 366 367	addsub12d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B + S (j) - E (S (j))$
377	366 367 139	subsub2d	$⊢ (φ \land j \in (0 ..^N)) \to B - (E (S (j)) - S (j)) = B + S (j) - E (S (j))$
378	376 377	eqtr4d	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B - (E (S (j)) - S (j))$
379	378	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to B - (S (j) + B - E (S (j))) = B - (B - (E (S (j)) - S (j)))$
380	367 139	subcld	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j)) - S (j) \in ℂ$
381	366 380	nncand	$⊢ (φ \land j \in (0 ..^N)) \to B - (B - (E (S (j)) - S (j))) = E (S (j)) - S (j)$
382	375 379 381	3eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to B - Z = E (S (j)) - S (j)$
383	382	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to \frac{B - Z}{T} = \frac{E (S (j)) - S (j)}{T}$
384	369 365 383	3eqtr4d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{B - S (j)}{T}) - (\frac{B - E (S (j))}{T}) = \frac{B - Z}{T}$
385	384	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}$
386	373 385	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}$
387	337 340 344 347 386	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}$
388	292	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 ℝ$
389	388 342 343	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})$
390	387 389	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$
391	322 336 341	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)$
392	390 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 Z < S (j + 1)$
393	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$
394	322 336 317 392 393	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$
395	322 317 394	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$
396	316 317 322 335 395	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]$
397	33	a1i	$⊢ (φ \land j \in (0 ..^N)) \to B - A = T$
398	397	oveq2d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) (B - A) = (\frac{E (S (j)) - S (j)}{T}) T$
399	380 144 145	divcan1d	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) T = E (S (j)) - S (j)$
400	398 399	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{E (S (j)) - S (j)}{T}) (B - A) = E (S (j)) - S (j)$
401	374 400	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))$
402	139 363	addcomd	$⊢ (φ \land j \in (0 ..^N)) \to S (j) + B - E (S (j)) = B - E (S (j)) + S (j)$
403	402	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))$
404	363 139 367	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))$
405	366 367	npcand	$⊢ (φ \land j \in (0 ..^N)) \to B - E (S (j)) + E (S (j)) = B$
406	404 405	eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to (B - E (S (j))) + S (j) + (E (S (j)) - S (j)) = B$
407	401 403 406	3eqtrd	$⊢ (φ \land j \in (0 ..^N)) \to Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) = B$
408	200	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B \in ran Q$
409	407 408	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to Z + (\frac{E (S (j)) - S (j)}{T}) (B - A) \in ran Q$
410		oveq1	$⊢ k = \frac{E (S (j)) - S (j)}{T} \to k (B - A) = (\frac{E (S (j)) - S (j)}{T}) (B - A)$
411	410	oveq2d	$⊢ k = \frac{E (S (j)) - S (j)}{T} \to Z + k (B - A) = Z + (\frac{E (S (j)) - S (j)}{T}) (B - A)$
412	411	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)$
413	412	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$
414	148 409 413	syl2anc	$⊢ (φ \land j \in (0 ..^N)) \to \exists k \in ℤ Z + k (B - A) \in ran Q$
415	414	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$
416		oveq1	$⊢ y = Z \to y + k (B - A) = Z + k (B - A)$
417	416	eleq1d	$⊢ y = Z \to (y + k (B - A) \in ran Q \leftrightarrow Z + k (B - A) \in ran Q)$
418	417	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)$
419	418	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)$
420	396 415 419	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\}$
421		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\})$
422	420 421	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\})$
423		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)$
424	315 422 423	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)$
425	54	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) \in ℝ$
426	319	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B - E (S (j)) \in ℝ$
427	318	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \in ℝ$
428	21	ad2antrr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \in ℝ$
429	328	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) \leq B$
430	274	necomd	$⊢ \neg E (S (j)) = B \to B \neq E (S (j))$
431	430	adantl	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B \neq E (S (j))$
432	427 428 429 431	leneltd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to E (S (j)) < B$
433	427 428	posdifd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to (E (S (j)) < B \leftrightarrow 0 < B - E (S (j)))$
434	432 433	mpbid	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to 0 < B - E (S (j))$
435	426 434	elrpd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to B - E (S (j)) \in ℝ^{+}$
436	425 435	ltaddrpd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) < S (j) + B - E (S (j))$
437	436 12	breqtrrdi	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) < Z$
438	437	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$
439		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)$
440	438 439	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)$
441	392	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)$
442	439 441	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)$
443	440 442	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))$
444	443	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)))$
445	444	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)))$
446	424 445	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))$
447	314 446	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))$
448	251	nrexdv	$⊢ (φ \land j \in (0 ..^N)) \to \neg \exists i \in (0 \dots N) (S (j) < S (i) \land S (i) < S (j + 1))$
449	448	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))$
450	447 449	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$
451	307 450	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)$
452	131	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to \frac{B - S (j)}{T} \in ℝ$
453	294	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ \in ℤ$
454		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))$
455	452 453 454	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))$
456	451 455	mpbird	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j)}{T}⌋ = ⌊\frac{B - S (j + 1)}{T}⌋$
457	456	eqcomd	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j + 1)}{T}⌋ = ⌊\frac{B - S (j)}{T}⌋$
458	457	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$
459	458	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$
460	459	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)$
461	266	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j + 1) \in ℂ$
462	139	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to S (j) \in ℂ$
463	140	adantr	$⊢ ((φ \land j \in (0 ..^N)) \land \neg E (S (j)) = B) \to ⌊\frac{B - S (j)}{T}⌋ T \in ℂ$
464	461 462 463	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)$
465	460 464	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)$
466	284 300 465	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)$
467	270 466	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