fourierdlem65 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem65		Structured version Visualization version GIF version

Theorem fourierdlem65 46614

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

**Hypotheses**
Ref	Expression
fourierdlem65.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem65.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem65.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem65.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem65.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem65.d	⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
fourierdlem65.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem65.n	⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
fourierdlem65.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
fourierdlem65.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem65.l	⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem65.z	⊢ 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))

**Assertion**
Ref	Expression
fourierdlem65	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))

Distinct variable groups: 𝐴,𝑓,𝑘,𝑦 𝐴,𝑖,𝑥,𝑘,𝑦 𝐴,𝑚,𝑝,𝑖 𝐵,𝑓,𝑘,𝑦 𝐵,𝑖,𝑥 𝐵,𝑚,𝑝 𝐶,𝑓,𝑦 𝐶,𝑖,𝑚,𝑝 𝑥,𝐶 𝐷,𝑓,𝑦 𝐷,𝑖,𝑚,𝑝 𝑥,𝐷 𝑖,𝐸,𝑘,𝑥,𝑦 𝑖,𝑀,𝑚,𝑝 𝑓,𝑁,𝑦 𝑖,𝑁,𝑚,𝑝 𝑥,𝑁 𝑄,𝑓,𝑘,𝑦 𝑄,𝑖,𝑥 𝑄,𝑝 𝑆,𝑓,𝑘,𝑦 𝑆,𝑖,𝑥 𝑆,𝑝 𝑇,𝑖,𝑘,𝑥,𝑦 𝑖,𝑍,𝑘,𝑦 𝜑,𝑓,𝑘,𝑦 𝑖,𝑗,𝑘,𝑥,𝑦 𝜑,𝑖,𝑥 Allowed substitution hints: 𝜑(𝑗,𝑚,𝑝) 𝐴(𝑗) 𝐵(𝑗) 𝐶(𝑗,𝑘) 𝐷(𝑗,𝑘) 𝑃(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝) 𝑄(𝑗,𝑚) 𝑆(𝑗,𝑚) 𝑇(𝑓,𝑗,𝑚,𝑝) 𝐸(𝑓,𝑗,𝑚,𝑝) 𝐿(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝) 𝑀(𝑥,𝑦,𝑓,𝑗,𝑘) 𝑁(𝑗,𝑘) 𝑂(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝) 𝑍(𝑥,𝑓,𝑗,𝑚,𝑝)

**Proof of Theorem fourierdlem65**
Step	Hyp	Ref	Expression
1		fourierdlem65.l	. . . . . 6 ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
2	1	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
3		simpr 485	. . . . . . . 8 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
4		simpl 483	. . . . . . . 8 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
5	3, 4	eqtrd 2774	. . . . . . 7 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = 𝐵)
6	5	iftrued 4462	. . . . . 6 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
7	6	adantll 720	. . . . 5 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
8		fourierdlem65.p	. . . . . . . . . . 11 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
9		fourierdlem65.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10		fourierdlem65.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
11	8, 9, 10	fourierdlem11 46561	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
12	11	simp1d 1148	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
13	11	simp2d 1149	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	11	simp3d 1150	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 𝐵)
15		fourierdlem65.t	. . . . . . . . 9 ⊢ 𝑇 = (𝐵 − 𝐴)
16		fourierdlem65.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
17	12, 13, 14, 15, 16	fourierdlem4 46554	. . . . . . . 8 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
18	17	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
19		fourierdlem65.c	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ)
20		ioossre 13351	. . . . . . . . . . . . . . . 16 ⊢ (𝐶(,)+∞) ⊆ ℝ
21		fourierdlem65.d	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
22	20, 21	sselid 3913	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ)
23	19	rexrd 11186	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
24		pnfxr 11190	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
25	24	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
26		ioogtlb 45940	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
27	23, 25, 21, 26	syl3anc 1379	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 < 𝐷)
28		fourierdlem65.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
29		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
30	15	eqcomi 2748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 − 𝐴) = 𝑇
31	30	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇)
32	31	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇))
33	29, 32	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (𝑥 + (𝑘 · 𝑇)))
34	33	eleq1d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
35	34	rexbidv 3163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
36	35	cbvrabv 3401	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
37	36	uneq2i 4095	. . . . . . . . . . . . . . 15 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
38		fourierdlem65.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
39		fourierdlem65.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
40	15, 8, 9, 10, 19, 22, 27, 28, 37, 38, 39	fourierdlem54 46603	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
41	40	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
42	41	simprd 496	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
43	41	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
44	28	fourierdlem2 46552	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
45	43, 44	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
46	42, 45	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
47	46	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
48		elmapi 8786	. . . . . . . . . 10 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
49	47, 48	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
51		elfzofz 13621	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
52	51	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
53	50, 52	ffvelcdmd 7026	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
54	18, 53	ffvelcdmd 7026	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
55	54	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
56	12	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
57	2, 7, 55, 56	fvmptd 6943	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴)
58	57	oveq2d 7372	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴))
59	13	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
60	14	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵)
61	53	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
62		simpr 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
63		fzofzp1 13710	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
64	63	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
65	50, 64	ffvelcdmd 7026	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
66	65	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
67		elfzoelz 13604	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
68	67	zred 12624	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
69	68	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℝ)
70	69	ltp1d 12077	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
71	40	simprd 496	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
72	71	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
73		isorel 7270	. . . . . . . . 9 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
74	72, 52, 64, 73	syl12anc 842	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
75	70, 74	mpbid 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
76	75	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
77		isof1o 7267	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → 𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
78		f1ofo 6774	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
79	71, 77, 78	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
80	79	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
81	19	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐶 ∈ ℝ)
82	22	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐷 ∈ ℝ)
83	13, 12	resubcld 11569	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
84	15, 83	eqeltrid 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
85	84	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
86	53, 85	readdcld 11165	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
87	86	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
88	19	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
89	28, 43, 42	fourierdlem15 46565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
90	89	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
91	90, 52	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐶[,]𝐷))
92	22	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ)
93		elicc2 13355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷)))
94	88, 92, 93	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷)))
95	91, 94	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷))
96	95	simp2d 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ (𝑆‘𝑗))
97	12, 13	posdifd 11728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
98	14, 97	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
99	98, 15	breqtrrdi 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑇)
100	84, 99	elrpd 12974	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
101	100	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ⁺)
102	53, 101	ltaddrpd 13010	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + 𝑇))
103	88, 53, 86, 96, 102	lelttrd 11295	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 < ((𝑆‘𝑗) + 𝑇))
104	88, 86, 103	ltled 11285	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆‘𝑗) + 𝑇))
105	104	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐶 ≤ ((𝑆‘𝑗) + 𝑇))
106	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
107		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))
108	87, 106	ltnled 11284	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)) ↔ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)))
109	107, 108	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
110	90, 64	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷))
111		elicc2 13355	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
112	88, 92, 111	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
113	110, 112	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷))
114	113	simp3d 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
115	114	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
116	87, 106, 82, 109, 115	ltletrd 11297	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < 𝐷)
117	87, 82, 116	ltled 11285	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ≤ 𝐷)
118	81, 82, 87, 105, 117	eliccd 45949	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
119	118	adantlr 721	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
120	16	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘𝑗) → 𝑥 = (𝑆‘𝑗))
122		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑆‘𝑗) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘𝑗)))
123	122	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑆‘𝑗) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘𝑗)) / 𝑇))
124	123	fveq2d 6831	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑆‘𝑗) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
125	124	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘𝑗) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
126	121, 125	oveq12d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘𝑗) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
127	126	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
128	13	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
129	128, 53	resubcld 11569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘𝑗)) ∈ ℝ)
130	129, 101	rerpdivcld 13008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
131	130	flcld 13748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℤ)
132	131	zred 12624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℝ)
133	132, 85	remulcld 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℝ)
134	53, 133	readdcld 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) ∈ ℝ)
135	120, 127, 53, 134	fvmptd 6943	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
136	135	oveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) = (((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)))
137	136	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = ((((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) / 𝑇))
138	53	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ)
139	133	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
140	138, 139	pncan2d 11498	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
141	140	oveq1d 7371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) / 𝑇))
142	132	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℂ)
143	85	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℂ)
144	101	rpne0d 12982	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ≠ 0)
145	142, 143, 144	divcan4d 11928	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
146	137, 141, 145	3eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
147	146, 131	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ)
148		peano2zm 12561	. . . . . . . . . . . . . 14 ⊢ ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
149	147, 148	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
150	149	ad2antrr 732	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
151	30	oveq2i 7367	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)
152	151	oveq2i 7367	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
154	135	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
155		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) = (𝐵 − (𝑆‘𝑗)))
156	155	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐵 − (𝑆‘𝑗)) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
157	156	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝐵 − (𝑆‘𝑗)) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
158	157	fveq2d 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)))
159	158	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) = ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
160	159	oveq2d 7372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
161	160	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
162	146, 142	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℂ)
163		1cnd 11130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℂ)
164	162, 163, 143	subdird 11598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)))
165	84	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
166	165	mullidd 11154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
167	166	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
168	167	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
169	164, 168	eqtrd 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
170	169	oveq2d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇)))
171	162, 143	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) ∈ ℂ)
172	138, 143, 171	ppncand 11536	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇)) = ((𝑆‘𝑗) + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇)))
173		flid 13758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ → (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
174	147, 173	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
175	174	eqcomd 2745	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)))
176	175	oveq1d 7371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) = ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
177	176	oveq2d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
178	170, 172, 177	3eqtrrd 2779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
179	178	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
180	154, 161, 179	3eqtrrd 2779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)) = (𝐸‘(𝑆‘𝑗)))
181	153, 180, 62	3eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = 𝐵)
182	8	fourierdlem2 46552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
183	9, 182	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
184	10, 183	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
185	184	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
186	185	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
187	186	simprd 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
188	187	eqcomd 2745	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 = (𝑄‘𝑀))
189	8, 9, 10	fourierdlem15 46565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
190		ffn 6655	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → 𝑄 Fn (0...𝑀))
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
192	9	nnnn0d 12489	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
193		nn0uz 12817	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
194	192, 193	eleqtrdi 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
195		eluzfz2 13477	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
196	194, 195	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
197		fnfvelrn 7021	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
198	191, 196, 197	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
199	188, 198	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
200	199	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ran 𝑄)
201	181, 200	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄)
202	201	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄)
203		oveq1 7363	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → (𝑘 · (𝐵 − 𝐴)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴)))
204	203	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))))
205	204	eleq1d 2824	. . . . . . . . . . . . 13 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → ((((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄))
206	205	rspcev 3560	. . . . . . . . . . . 12 ⊢ ((((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ ∧ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
207	150, 202, 206	syl2anc 590	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
208		oveq1 7363	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))))
209	208	eleq1d 2824	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
210	209	rexbidv 3163	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
211	210	elrab 3629	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} ↔ (((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
212	119, 207, 211	sylanbrc 589	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
213		elun2 4112	. . . . . . . . . 10 ⊢ (((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} → ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
214	212, 213	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
215		foelrn 7048	. . . . . . . . 9 ⊢ ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) ∧ ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
216	80, 214, 215	syl2anc 590	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
217		eqcom 2746	. . . . . . . . 9 ⊢ (((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖) ↔ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
218	217	rexbii 3086	. . . . . . . 8 ⊢ (∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖) ↔ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
219	216, 218	sylib 219	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
220	102	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + 𝑇))
221	217	bilanri 507	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
222	220, 221	breqtrd 5098	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑗) < (𝑆‘𝑖))
223	109	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
224	221, 223	eqbrtrrd 5096	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
225	222, 224	jca 516	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
226	225	adantlr 721	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
227		simplll 780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
228		simplr 774	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → 𝑖 ∈ (0...𝑁))
229		elfzelz 13469	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑁) → 𝑖 ∈ ℤ)
230	229	ad2antlr 733	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 ∈ ℤ)
231	67	ad3antlr 737	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 ∈ ℤ)
232		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → (𝑆‘𝑗) < (𝑆‘𝑖))
233	72	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
234	52	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑗 ∈ (0...𝑁))
235		simplr 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑖 ∈ (0...𝑁))
236		isorel 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑖 ∈ (0...𝑁))) → (𝑗 < 𝑖 ↔ (𝑆‘𝑗) < (𝑆‘𝑖)))
237	233, 234, 235, 236	syl12anc 842	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → (𝑗 < 𝑖 ↔ (𝑆‘𝑗) < (𝑆‘𝑖)))
238	232, 237	mpbird 258	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑗 < 𝑖)
239	238	adantrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 < 𝑖)
240		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
241	72	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
242		simplr 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 ∈ (0...𝑁))
243	64	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑗 + 1) ∈ (0...𝑁))
244		isorel 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑖 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑖 < (𝑗 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
245	241, 242, 243, 244	syl12anc 842	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑖 < (𝑗 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
246	240, 245	mpbird 258	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 < (𝑗 + 1))
247	246	adantrl 722	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 < (𝑗 + 1))
248		btwnnz 12596	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℤ ∧ 𝑗 < 𝑖 ∧ 𝑖 < (𝑗 + 1)) → ¬ 𝑖 ∈ ℤ)
249	231, 239, 247, 248	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → ¬ 𝑖 ∈ ℤ)
250	230, 249	pm2.65da 822	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
251	227, 228, 250	syl2anc 590	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ¬ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
252	226, 251	pm2.65da 822	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
253	252	nrexdv 3134	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
254	253	adantlr 721	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
255	219, 254	condan 823	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))
256	61	rexrd 11186	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ^*)
257	84	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑇 ∈ ℝ)
258	61, 257	readdcld 11165	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
259		elioc2 13353	. . . . . . 7 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))))
260	256, 258, 259	syl2anc 590	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))))
261	66, 76, 255, 260	mpbir3and 1349	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
262	56, 59, 60, 15, 16, 61, 62, 261	fourierdlem26 46576	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))))
263	262	oveq1d 7371	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴) = ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) − 𝐴))
264	56	recnd 11164	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℂ)
265	65	recnd 11164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
266	265, 138	subcld 11496	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℂ)
267	266	adantr 481	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℂ)
268	264, 267	pncan2d 11498	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) − 𝐴) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
269	58, 263, 268	3eqtrd 2778	. 2 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
270	1	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
271		eqcom 2746	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐸‘(𝑆‘𝑗)) ↔ (𝐸‘(𝑆‘𝑗)) = 𝑦)
272	271	bilani 505	. . . . . . . . . 10 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) = 𝑦)
273		neqne 2942	. . . . . . . . . . 11 ⊢ (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
274	273	adantr 481	. . . . . . . . . 10 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
275	272, 274	eqnetrrd 3002	. . . . . . . . 9 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵)
276	275	neneqd 2939	. . . . . . . 8 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵)
277	276	iffalsed 4465	. . . . . . 7 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
278		simpr 485	. . . . . . 7 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
279	277, 278	eqtrd 2774	. . . . . 6 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
280	279	adantll 720	. . . . 5 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
281	54	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
282	270, 280, 281, 281	fvmptd 6943	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗)))
283	282	oveq2d 7372	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))))
284		id 22	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → 𝑥 = (𝑆‘(𝑗 + 1)))
285		oveq2 7364	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝑗 + 1))))
286	285	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
287	286	fveq2d 6831	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
288	287	oveq1d 7371	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇))
289	284, 288	oveq12d 7374	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
290	289	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘(𝑗 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
291	128, 65	resubcld 11569	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
292	291, 101	rerpdivcld 13008	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
293	292	flcld 13748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
294	293	zred 12624	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
295	294, 85	remulcld 11166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
296	65, 295	readdcld 11165	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
297	120, 290, 65, 296	fvmptd 6943	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
298	297, 135	oveq12d 7374	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
299	298	adantr 481	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
300		flle 13749	. . . . . . . . . . . . 13 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
301	292, 300	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
302	53, 65, 75	ltled 11285	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘(𝑗 + 1)))
303	53, 65, 128, 302	lesub2dd 11758	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ≤ (𝐵 − (𝑆‘𝑗)))
304	291, 129, 101, 303	lediv1dd 13035	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
305	294, 292, 130, 301, 304	letrd 11294	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
306	305	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
307	294	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
308		1red 11136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → 1 ∈ ℝ)
309	307, 308	readdcld 11165	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
310	130	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
311		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
312	309, 310, 311	nltled 11287	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
313	312	adantlr 721	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
314	79	ad3antrrr 736	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
315	88	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐶 ∈ ℝ)
316	92	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐷 ∈ ℝ)
317		fourierdlem65.z	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
318	135, 134	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
319	128, 318	resubcld 11569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ)
320	53, 319	readdcld 11165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) ∈ ℝ)
321	317, 320	eqeltrid 2843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
322	321	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ ℝ)
323	12	rexrd 11186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
324	323	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ^*)
325		elioc2 13353	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
326	324, 128, 325	syl2anc 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
327	54, 326	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
328	327	simp3d 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
329	128, 318	subge0d 11731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))) ↔ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
330	328, 329	mpbird 258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))))
331	53, 319	addge01d 11729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))) ↔ (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))))
332	330, 331	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
333	88, 53, 320, 96, 332	letrd 11294	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
334	333, 317	breqtrrdi 5114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ 𝑍)
335	334	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐶 ≤ 𝑍)
336	65	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
337	292	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
338		reflcl 13746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
339		peano2re 11310	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
340	337, 338, 339	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
341	128	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐵 ∈ ℝ)
342	341, 322	resubcld 11569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − 𝑍) ∈ ℝ)
343	101	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
344	342, 343	rerpdivcld 13008	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − 𝑍) / 𝑇) ∈ ℝ)
345		flltp1 13750	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
346	292, 345	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
347	346	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
348	293	peano2zd 12627	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
349	348	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
350	130	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
351		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
352	319, 101	rerpdivcld 13008	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) ∈ ℝ)
353	352	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) ∈ ℝ)
354	12	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
355	327	simp2d 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < (𝐸‘(𝑆‘𝑗)))
356	354, 318, 128, 355	ltsub2dd 11754	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) < (𝐵 − 𝐴))
357	356, 15	breqtrrdi 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) < 𝑇)
358	319, 85, 101, 357	ltdiv1dd 13034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < (𝑇 / 𝑇))
359	143, 144	dividd 11920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑇 / 𝑇) = 1)
360	358, 359	breqtrd 5098	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < 1)
361	360	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < 1)
362	129	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘𝑗)) ∈ ℂ)
363	319	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℂ)
364	362, 363, 143, 144	divsubdird 11961	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇) = (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)))
365	364	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇))
366	128	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
367	318	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ ℂ)
368	366, 138, 367	nnncan1d 11530	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
369	368	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
370	365, 369	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
371	370, 147	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) ∈ ℤ)
372	371	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) ∈ ℤ)
373	349, 350, 351, 353, 361, 372	zltlesub 45733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)))
374	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
375	374	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝑍) = (𝐵 − ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))))
376	138, 366, 367	addsub12d 11519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = (𝐵 + ((𝑆‘𝑗) − (𝐸‘(𝑆‘𝑗)))))
377	366, 367, 138	subsub2d 11525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = (𝐵 + ((𝑆‘𝑗) − (𝐸‘(𝑆‘𝑗)))))
378	376, 377	eqtr4d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
379	378	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))) = (𝐵 − (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))))
380	367, 138	subcld 11496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) ∈ ℂ)
381	366, 380	nncand 11501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
382	375, 379, 381	3eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝑍) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
383	382	oveq1d 7371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − 𝑍) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
384	369, 365, 383	3eqtr4d 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = ((𝐵 − 𝑍) / 𝑇))
385	384	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = ((𝐵 − 𝑍) / 𝑇))
386	373, 385	breqtrd 5098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − 𝑍) / 𝑇))
387	337, 340, 344, 347, 386	ltletrd 11297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵 − 𝑍) / 𝑇))
388	291	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
389	388, 342, 343	ltdiv1d 13022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍) ↔ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵 − 𝑍) / 𝑇)))
390	387, 389	mpbird 258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍))
391	322, 336, 341	ltsub2d 11751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑍 < (𝑆‘(𝑗 + 1)) ↔ (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍)))
392	390, 391	mpbird 258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 < (𝑆‘(𝑗 + 1)))
393	114	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
394	322, 336, 316, 392, 393	ltletrd 11297	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 < 𝐷)
395	322, 316, 394	ltled 11285	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ≤ 𝐷)
396	315, 316, 322, 335, 395	eliccd 45949	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ (𝐶[,]𝐷))
397	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝐴) = 𝑇)
398	397	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)) = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇))
399	380, 143, 144	divcan1d 11923	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
400	398, 399	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
401	374, 400	oveq12d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
402	138, 363	addcomd 11339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)))
403	402	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
404	363, 138, 367	ppncand 11536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝐸‘(𝑆‘𝑗))))
405	366, 367	npcand 11500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝐸‘(𝑆‘𝑗))) = 𝐵)
406	404, 405	eqtrd 2774	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = 𝐵)
407	401, 403, 406	3eqtrd 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) = 𝐵)
408	199	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ran 𝑄)
409	407, 408	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄)
410		oveq1 7363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → (𝑘 · (𝐵 − 𝐴)) = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)))
411	410	oveq2d 7372	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → (𝑍 + (𝑘 · (𝐵 − 𝐴))) = (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))))
412	411	eleq1d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → ((𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄))
413	412	rspcev 3560	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ ∧ (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
414	147, 409, 413	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
415	414	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
416		oveq1 7363	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑍 → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (𝑍 + (𝑘 · (𝐵 − 𝐴))))
417	416	eleq1d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑍 → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
418	417	rexbidv 3163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑍 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
419	418	elrab 3629	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} ↔ (𝑍 ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
420	396, 415, 419	sylanbrc 589	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
421		elun2 4112	. . . . . . . . . . . . . . 15 ⊢ (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
422	420, 421	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
423		foelrn 7048	. . . . . . . . . . . . . 14 ⊢ ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) ∧ 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖))
424	314, 422, 423	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖))
425	53	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
426	319	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ)
427	318	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
428	13	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
429	328	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
430	273	necomd 2989	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
431	430	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
432	427, 428, 429, 431	leneltd 11291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
433	427, 428	posdifd 11728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘𝑗)) < 𝐵 ↔ 0 < (𝐵 − (𝐸‘(𝑆‘𝑗)))))
434	432, 433	mpbid 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 0 < (𝐵 − (𝐸‘(𝑆‘𝑗))))
435	426, 434	elrpd 12974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ⁺)
436	425, 435	ltaddrpd 13010	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
437	436, 317	breqtrrdi 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < 𝑍)
438	437	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑗) < 𝑍)
439		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → 𝑍 = (𝑆‘𝑖))
440	438, 439	breqtrd 5098	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑗) < (𝑆‘𝑖))
441	392	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → 𝑍 < (𝑆‘(𝑗 + 1)))
442	439, 441	eqbrtrrd 5096	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
443	440, 442	jca 516	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
444	443	ex 413	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑍 = (𝑆‘𝑖) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))))
445	444	reximdv 3154	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))))
446	424, 445	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
447	313, 446	syldan 597	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
448	250	nrexdv 3134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
449	448	ad2antrr 732	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
450	447, 449	condan 823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
451	306, 450	jca 516	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)))
452	130	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
453	293	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
454		flbi 13766	. . . . . . . . . 10 ⊢ ((((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ ∧ (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
455	452, 453, 454	syl2anc 590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
456	451, 455	mpbird 258	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
457	456	eqcomd 2745	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
458	457	oveq1d 7371	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
459	458	oveq2d 7372	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
460	459	oveq1d 7371	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
461	265	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
462	138	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℂ)
463	139	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
464	461, 462, 463	pnpcan2d 11534	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
465	460, 464	eqtrd 2774	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
466	283, 299, 465	3eqtrd 2778	. 2 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
467	269, 466	pm2.61dan 818	1 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {crab 3391 ∪ cun 3881 ifcif 4454 {cpr 4557 class class class wbr 5072 ↦ cmpt 5153 ran crn 5619 ℩cio 6439 Fn wfn 6480 ⟶wf 6481 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 Isom wiso 6486 (class class class)co 7356 ↑_m cmap 8763 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 +∞cpnf 11167 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12165 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 (,)cioo 13289 (,]cioc 13290 [,]cicc 13292 ...cfz 13452 ..^cfzo 13599 ⌊cfl 13740 ♯chash 14283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8633 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-rest 17376 df-topgen 17397 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-top 22877 df-topon 22894 df-bases 22929 df-cld 23002 df-ntr 23003 df-cls 23004 df-nei 23081 df-lp 23119 df-cmp 23370

This theorem is referenced by: fourierdlem89 46638 fourierdlem90 46639 fourierdlem91 46640

W3C validator