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 40388

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	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem65.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem65.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem65.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem65.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem65.d	⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
fourierdlem65.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (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 477	. . . . . . . 8 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
4		simpl 473	. . . . . . . 8 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
5	3, 4	eqtrd 2656	. . . . . . 7 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = 𝐵)
6	5	iftrued 4094	. . . . . 6 ⊢ (((𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
7	6	adantll 750	. . . . 5 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
8		fourierdlem65.p	. . . . . . . . . . 11 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
9		fourierdlem65.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ)
10		fourierdlem65.q	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
11	8, 9, 10	fourierdlem11 40335	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
12	11	simp1d 1073	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
13	11	simp2d 1074	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	11	simp3d 1075	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 𝐵)
15		fourierdlem65.t	. . . . . . . . 9 ⊢ 𝑇 = (𝐵 − 𝐴)
16		fourierdlem65.e	. . . . . . . . 9 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
17	12, 13, 14, 15, 16	fourierdlem4 40328	. . . . . . . 8 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
18	17	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
19		fourierdlem65.c	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 ∈ ℝ)
20		ioossre 12235	. . . . . . . . . . . . . . . 16 ⊢ (𝐶(,)+∞) ⊆ ℝ
21		fourierdlem65.d	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
22	20, 21	sseldi 3601	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ ℝ)
23	19	rexrd 10089	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ^*)
24		pnfxr 10092	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
25	24	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
26		ioogtlb 39717	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ (𝐶(,)+∞)) → 𝐶 < 𝐷)
27	23, 25, 21, 26	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 < 𝐷)
28		fourierdlem65.o	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
29		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
30	15	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 − 𝐴) = 𝑇
31	30	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇)
32	31	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇))
33	29, 32	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (𝑥 + (𝑘 · 𝑇)))
34	33	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
35	34	rexbidv 3052	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
36	35	cbvrabv 3199	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
37	36	uneq2i 3764	. . . . . . . . . . . . . . 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 40377	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
41	40	simpld 475	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
42	41	simprd 479	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
43	41	simpld 475	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
44	28	fourierdlem2 40326	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
45	43, 44	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
46	42, 45	mpbid 222	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
47	46	simpld 475	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)))
48		elmapi 7879	. . . . . . . . . 10 ⊢ (𝑆 ∈ (ℝ ↑_𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
49	47, 48	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
50	49	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
51		elfzofz 12485	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
52	51	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
53	50, 52	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
54	18, 53	ffvelrnd 6360	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
55	54	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
56	12	ad2antrr 762	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
57	2, 7, 55, 56	fvmptd 6288	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴)
58	57	oveq2d 6666	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴))
59	13	ad2antrr 762	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
60	14	ad2antrr 762	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵)
61	53	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
62		simpr 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
63		fzofzp1 12565	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
64	63	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
65	50, 64	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
66	65	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
67		elfzoelz 12470	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
68	67	zred 11482	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
69	68	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℝ)
70	69	ltp1d 10954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
71	40	simprd 479	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
72	71	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
73		isorel 6576	. . . . . . . . 9 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
74	72, 52, 64, 73	syl12anc 1324	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
75	70, 74	mpbid 222	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
76	75	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
77		isof1o 6573	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → 𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
78		f1ofo 6144	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
79	71, 77, 78	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
80	79	ad3antrrr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
81	19	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐶 ∈ ℝ)
82	22	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐷 ∈ ℝ)
83	13, 12	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
84	15, 83	syl5eqel 2705	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℝ)
85	84	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
86	53, 85	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
87	86	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
88	19	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
89	28, 43, 42	fourierdlem15 40339	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
90	89	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
91	90, 52	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ (𝐶[,]𝐷))
92	22	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ)
93		elicc2 12238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷)))
94	88, 92, 93	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷)))
95	91, 94	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) ≤ 𝐷))
96	95	simp2d 1074	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ (𝑆‘𝑗))
97	12, 13	posdifd 10614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
98	14, 97	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
99	98, 15	syl6breqr 4695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 𝑇)
100	84, 99	elrpd 11869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
101	100	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ⁺)
102	53, 101	ltaddrpd 11905	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + 𝑇))
103	88, 53, 86, 96, 102	lelttrd 10195	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 < ((𝑆‘𝑗) + 𝑇))
104	88, 86, 103	ltled 10185	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆‘𝑗) + 𝑇))
105	104	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → 𝐶 ≤ ((𝑆‘𝑗) + 𝑇))
106	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
107		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))
108	87, 106	ltnled 10184	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)) ↔ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)))
109	107, 108	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
110	90, 64	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷))
111		elicc2 12238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
112	88, 92, 111	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷)))
113	110, 112	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ 𝐷))
114	113	simp3d 1075	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
115	114	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
116	87, 106, 82, 109, 115	ltletrd 10197	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < 𝐷)
117	87, 82, 116	ltled 10185	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ≤ 𝐷)
118	81, 82, 87, 105, 117	eliccd 39726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
119	118	adantlr 751	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷))
120	16	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘𝑗) → 𝑥 = (𝑆‘𝑗))
122		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝑆‘𝑗) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘𝑗)))
123	122	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = (𝑆‘𝑗) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘𝑗)) / 𝑇))
124	123	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑆‘𝑗) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
125	124	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘𝑗) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
126	121, 125	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘𝑗) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
127	126	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
128	13	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
129	128, 53	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘𝑗)) ∈ ℝ)
130	129, 101	rerpdivcld 11903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
131	130	flcld 12599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℤ)
132	131	zred 11482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℝ)
133	132, 85	remulcld 10070	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℝ)
134	53, 133	readdcld 10069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) ∈ ℝ)
135	120, 127, 53, 134	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
136	135	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) = (((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)))
137	136	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = ((((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) / 𝑇))
138	53	recnd 10068	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ)
139	133	recnd 10068	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
140	138, 139	pncan2d 10394	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
141	140	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − (𝑆‘𝑗)) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) / 𝑇))
142	132	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∈ ℂ)
143	85	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℂ)
144	101	rpne0d 11877	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ≠ 0)
145	142, 143, 144	divcan4d 10807	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
146	137, 141, 145	3eqtrd 2660	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
147	146, 131	eqeltrd 2701	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ)
148		peano2zm 11420	. . . . . . . . . . . . . 14 ⊢ ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
149	147, 148	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
150	149	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ)
151	30	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)
152	151	oveq2i 6661	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇))
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
154	135	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
155		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) = (𝐵 − (𝑆‘𝑗)))
156	155	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐵 − (𝑆‘𝑗)) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
157	156	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝐵 − (𝑆‘𝑗)) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
158	157	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)))
159	158	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) = ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
160	159	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
161	160	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
162	146, 142	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℂ)
163		1cnd 10056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℂ)
164	162, 163, 143	subdird 10487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)))
165	84	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 ∈ ℂ)
166	165	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝑇) = 𝑇)
167	166	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
168	167	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − (1 · 𝑇)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
169	164, 168	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇))
170	169	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇)))
171	162, 143	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) ∈ ℂ)
172	138, 143, 171	ppncand 10432	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) − 𝑇)) = ((𝑆‘𝑗) + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇)))
173		flid 12609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ → (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
174	147, 173	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
175	174	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) = (⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)))
176	175	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) = ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
177	176	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇)) = ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
178	170, 172, 177	3eqtrrd 2661	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
179	178	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + ((⌊‘(((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)))
180	154, 161, 179	3eqtrrd 2661	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · 𝑇)) = (𝐸‘(𝑆‘𝑗)))
181	153, 180, 62	3eqtrd 2660	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) = 𝐵)
182	8	fourierdlem2 40326	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
183	9, 182	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
184	10, 183	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
185	184	simprd 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
186	185	simpld 475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
187	186	simprd 479	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)
188	187	eqcomd 2628	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 = (𝑄‘𝑀))
189	8, 9, 10	fourierdlem15 40339	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
190		ffn 6045	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄:(0...𝑀)⟶(𝐴[,]𝐵) → 𝑄 Fn (0...𝑀))
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
192	9	nnnn0d 11351	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
193		nn0uz 11722	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
194	192, 193	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
195		eluzfz2 12349	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
196	194, 195	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
197		fnfvelrn 6356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑄 Fn (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)) → (𝑄‘𝑀) ∈ ran 𝑄)
198	191, 196, 197	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
199	188, 198	eqeltrd 2701	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ran 𝑄)
200	199	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ran 𝑄)
201	181, 200	eqeltrd 2701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄)
202	201	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄)
203		oveq1 6657	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → (𝑘 · (𝐵 − 𝐴)) = (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴)))
204	203	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))))
205	204	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑘 = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) → ((((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄))
206	205	rspcev 3309	. . . . . . . . . . . 12 ⊢ ((((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) ∈ ℤ ∧ (((𝑆‘𝑗) + 𝑇) + (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) − 1) · (𝐵 − 𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
207	150, 202, 206	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
208		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))))
209	208	eleq1d 2686	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
210	209	rexbidv 3052	. . . . . . . . . . . 12 ⊢ (𝑦 = ((𝑆‘𝑗) + 𝑇) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
211	210	elrab 3363	. . . . . . . . . . 11 ⊢ (((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} ↔ (((𝑆‘𝑗) + 𝑇) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑆‘𝑗) + 𝑇) + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
212	119, 207, 211	sylanbrc 698	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
213		elun2 3781	. . . . . . . . . 10 ⊢ (((𝑆‘𝑗) + 𝑇) ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} → ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
214	212, 213	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
215		foelrn 6378	. . . . . . . . 9 ⊢ ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) ∧ ((𝑆‘𝑗) + 𝑇) ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
216	80, 214, 215	syl2anc 693	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
217		eqcom 2629	. . . . . . . . 9 ⊢ (((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖) ↔ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
218	217	rexbii 3041	. . . . . . . 8 ⊢ (∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖) ↔ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
219	216, 218	sylib 208	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
220	102	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + 𝑇))
221	217	biimpri 218	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇) → ((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
222	221	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) = (𝑆‘𝑖))
223	220, 222	breqtrd 4679	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑗) < (𝑆‘𝑖))
224	109	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) + 𝑇) < (𝑆‘(𝑗 + 1)))
225	222, 224	eqbrtrrd 4677	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
226	223, 225	jca 554	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
227	226	adantlr 751	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
228		simplll 798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
229		simplr 792	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → 𝑖 ∈ (0...𝑁))
230		elfzelz 12342	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑁) → 𝑖 ∈ ℤ)
231	230	ad2antlr 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 ∈ ℤ)
232	67	ad3antlr 767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 ∈ ℤ)
233		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → (𝑆‘𝑗) < (𝑆‘𝑖))
234	72	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
235	52	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑗 ∈ (0...𝑁))
236		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑖 ∈ (0...𝑁))
237		isorel 6576	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑗 ∈ (0...𝑁) ∧ 𝑖 ∈ (0...𝑁))) → (𝑗 < 𝑖 ↔ (𝑆‘𝑗) < (𝑆‘𝑖)))
238	234, 235, 236, 237	syl12anc 1324	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → (𝑗 < 𝑖 ↔ (𝑆‘𝑗) < (𝑆‘𝑖)))
239	233, 238	mpbird 247	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘𝑖)) → 𝑗 < 𝑖)
240	239	adantrr 753	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑗 < 𝑖)
241		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
242	72	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
243		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 ∈ (0...𝑁))
244	64	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑗 + 1) ∈ (0...𝑁))
245		isorel 6576	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) ∧ (𝑖 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑖 < (𝑗 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
246	242, 243, 244, 245	syl12anc 1324	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → (𝑖 < (𝑗 + 1) ↔ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
247	241, 246	mpbird 247	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))) → 𝑖 < (𝑗 + 1))
248	247	adantrl 752	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → 𝑖 < (𝑗 + 1))
249		btwnnz 11453	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℤ ∧ 𝑗 < 𝑖 ∧ 𝑖 < (𝑗 + 1)) → ¬ 𝑖 ∈ ℤ)
250	232, 240, 248, 249	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) ∧ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))) → ¬ 𝑖 ∈ ℤ)
251	231, 250	pm2.65da 600	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
252	228, 229, 251	syl2anc 693	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) ∧ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇)) → ¬ ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
253	227, 252	pm2.65da 600	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) ∧ 𝑖 ∈ (0...𝑁)) → ¬ (𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
254	253	nrexdv 3001	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
255	254	adantlr 751	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇)) → ¬ ∃𝑖 ∈ (0...𝑁)(𝑆‘𝑖) = ((𝑆‘𝑗) + 𝑇))
256	219, 255	condan 835	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))
257	61	rexrd 10089	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ^*)
258	84	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑇 ∈ ℝ)
259	61, 258	readdcld 10069	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
260		elioc2 12236	. . . . . . 7 ⊢ (((𝑆‘𝑗) ∈ ℝ^* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))))
261	257, 259, 260	syl2anc 693	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ ((𝑆‘(𝑗 + 1)) ∈ ℝ ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ∧ (𝑆‘(𝑗 + 1)) ≤ ((𝑆‘𝑗) + 𝑇))))
262	66, 76, 256, 261	mpbir3and 1245	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
263	56, 59, 60, 15, 16, 61, 62, 262	fourierdlem26 40350	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))))
264	263	oveq1d 6665	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − 𝐴) = ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) − 𝐴))
265	56	recnd 10068	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℂ)
266	65	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
267	266, 138	subcld 10392	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℂ)
268	267	adantr 481	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℂ)
269	265, 268	pncan2d 10394	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐴 + ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) − 𝐴) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
270	58, 264, 269	3eqtrd 2660	. 2 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
271	1	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
272		eqcom 2629	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝐸‘(𝑆‘𝑗)) ↔ (𝐸‘(𝑆‘𝑗)) = 𝑦)
273	272	biimpi 206	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐸‘(𝑆‘𝑗)) → (𝐸‘(𝑆‘𝑗)) = 𝑦)
274	273	adantl 482	. . . . . . . . . 10 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) = 𝑦)
275		neqne 2802	. . . . . . . . . . 11 ⊢ (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
276	275	adantr 481	. . . . . . . . . 10 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
277	274, 276	eqnetrrd 2862	. . . . . . . . 9 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵)
278	277	neneqd 2799	. . . . . . . 8 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵)
279	278	iffalsed 4097	. . . . . . 7 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
280		simpr 477	. . . . . . 7 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
281	279, 280	eqtrd 2656	. . . . . 6 ⊢ ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
282	281	adantll 750	. . . . 5 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
283	54	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
284	271, 282, 283, 283	fvmptd 6288	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗)))
285	284	oveq2d 6666	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))))
286		id 22	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → 𝑥 = (𝑆‘(𝑗 + 1)))
287		oveq2 6658	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝑗 + 1))))
288	287	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
289	288	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
290	289	oveq1d 6665	. . . . . . . 8 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇))
291	286, 290	oveq12d 6668	. . . . . . 7 ⊢ (𝑥 = (𝑆‘(𝑗 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
292	291	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘(𝑗 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
293	128, 65	resubcld 10458	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
294	293, 101	rerpdivcld 11903	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
295	294	flcld 12599	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
296	295	zred 11482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
297	296, 85	remulcld 10070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
298	65, 297	readdcld 10069	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
299	120, 292, 65, 298	fvmptd 6288	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)))
300	299, 135	oveq12d 6668	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
301	300	adantr 481	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐸‘(𝑆‘𝑗))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
302		flle 12600	. . . . . . . . . . . . 13 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
303	294, 302	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇))
304	53, 65, 75	ltled 10185	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘(𝑗 + 1)))
305	53, 65, 128, 304	lesub2dd 10644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘(𝑗 + 1))) ≤ (𝐵 − (𝑆‘𝑗)))
306	293, 129, 101, 305	lediv1dd 11930	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
307	296, 294, 130, 303, 306	letrd 10194	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
308	307	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
309	296	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
310		1red 10055	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → 1 ∈ ℝ)
311	309, 310	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
312	130	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
313		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
314	311, 312, 313	nltled 10187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
315	314	adantlr 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
316	79	ad3antrrr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
317	88	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐶 ∈ ℝ)
318	92	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐷 ∈ ℝ)
319		fourierdlem65.z	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
320	135, 134	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
321	128, 320	resubcld 10458	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ)
322	53, 321	readdcld 10069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) ∈ ℝ)
323	319, 322	syl5eqel 2705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
324	323	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ ℝ)
325	12	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
326	325	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ^*)
327		elioc2 12236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
328	326, 128, 327	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
329	54, 328	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
330	329	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
331	128, 320	subge0d 10617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))) ↔ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
332	330, 331	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))))
333	53, 321	addge01d 10615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (0 ≤ (𝐵 − (𝐸‘(𝑆‘𝑗))) ↔ (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))))
334	332, 333	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
335	88, 53, 322, 96, 334	letrd 10194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
336	335, 319	syl6breqr 4695	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ≤ 𝑍)
337	336	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐶 ≤ 𝑍)
338	65	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
339	294	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ)
340		reflcl 12597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ)
341		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℝ → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
342	339, 340, 341	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℝ)
343	128	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝐵 ∈ ℝ)
344	343, 324	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − 𝑍) ∈ ℝ)
345	101	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑇 ∈ ℝ⁺)
346	344, 345	rerpdivcld 11903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − 𝑍) / 𝑇) ∈ ℝ)
347		flltp1 12601	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) ∈ ℝ → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
348	294, 347	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
349	348	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
350	295	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
351	350	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ∈ ℤ)
352	130	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
353		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇))
354	321, 101	rerpdivcld 11903	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) ∈ ℝ)
355	354	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) ∈ ℝ)
356	12	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
357	329	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < (𝐸‘(𝑆‘𝑗)))
358	356, 320, 128, 357	ltsub2dd 10640	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) < (𝐵 − 𝐴))
359	358, 15	syl6breqr 4695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) < 𝑇)
360	321, 85, 101, 359	ltdiv1dd 11929	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < (𝑇 / 𝑇))
361	143, 144	dividd 10799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑇 / 𝑇) = 1)
362	360, 361	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < 1)
363	362	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇) < 1)
364	129	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝑆‘𝑗)) ∈ ℂ)
365	321	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℂ)
366	364, 365, 143, 144	divsubdird 10840	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇) = (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)))
367	366	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇))
368	128	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℂ)
369	320	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ ℂ)
370	368, 138, 369	nnncan1d 10426	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
371	370	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) − (𝐵 − (𝐸‘(𝑆‘𝑗)))) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
372	367, 371	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
373	372, 147	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) ∈ ℤ)
374	373	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) ∈ ℤ)
375	351, 352, 353, 355, 363, 374	zltlesub 39497	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)))
376	319	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
377	376	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝑍) = (𝐵 − ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))))
378	138, 368, 369	addsub12d 10415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = (𝐵 + ((𝑆‘𝑗) − (𝐸‘(𝑆‘𝑗)))))
379	368, 369, 138	subsub2d 10421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = (𝐵 + ((𝑆‘𝑗) − (𝐸‘(𝑆‘𝑗)))))
380	378, 379	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
381	380	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))) = (𝐵 − (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))))
382	369, 138	subcld 10392	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) ∈ ℂ)
383	368, 382	nncand 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − (𝐵 − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
384	377, 381, 383	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝑍) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
385	384	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − 𝑍) / 𝑇) = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇))
386	371, 367, 385	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = ((𝐵 − 𝑍) / 𝑇))
387	386	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (((𝐵 − (𝑆‘𝑗)) / 𝑇) − ((𝐵 − (𝐸‘(𝑆‘𝑗))) / 𝑇)) = ((𝐵 − 𝑍) / 𝑇))
388	375, 387	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − 𝑍) / 𝑇))
389	339, 342, 346, 349, 388	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵 − 𝑍) / 𝑇))
390	293	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) ∈ ℝ)
391	390, 344, 345	ltdiv1d 11917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ((𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍) ↔ ((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇) < ((𝐵 − 𝑍) / 𝑇)))
392	389, 391	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍))
393	324, 338, 343	ltsub2d 10637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑍 < (𝑆‘(𝑗 + 1)) ↔ (𝐵 − (𝑆‘(𝑗 + 1))) < (𝐵 − 𝑍)))
394	392, 393	mpbird 247	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 < (𝑆‘(𝑗 + 1)))
395	114	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑆‘(𝑗 + 1)) ≤ 𝐷)
396	324, 338, 318, 394, 395	ltletrd 10197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 < 𝐷)
397	324, 318, 396	ltled 10185	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ≤ 𝐷)
398	317, 318, 324, 337, 397	eliccd 39726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ (𝐶[,]𝐷))
399	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐵 − 𝐴) = 𝑇)
400	399	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)) = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇))
401	382, 143, 144	divcan1d 10802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · 𝑇) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
402	400, 401	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)) = ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
403	376, 402	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) = (((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
404	138, 365	addcomd 10238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)))
405	404	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))))
406	365, 138, 369	ppncand 10432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝐸‘(𝑆‘𝑗))))
407	368, 369	npcand 10396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝐸‘(𝑆‘𝑗))) = 𝐵)
408	406, 407	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝐵 − (𝐸‘(𝑆‘𝑗))) + (𝑆‘𝑗)) + ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = 𝐵)
409	403, 405, 408	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) = 𝐵)
410	199	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ran 𝑄)
411	409, 410	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄)
412		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → (𝑘 · (𝐵 − 𝐴)) = ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴)))
413	412	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → (𝑍 + (𝑘 · (𝐵 − 𝐴))) = (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))))
414	413	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) → ((𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄))
415	414	rspcev 3309	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) ∈ ℤ ∧ (𝑍 + ((((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)) / 𝑇) · (𝐵 − 𝐴))) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
416	147, 411, 415	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
417	416	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
418		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑍 → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (𝑍 + (𝑘 · (𝐵 − 𝐴))))
419	418	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑍 → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
420	419	rexbidv 3052	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑍 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
421	420	elrab 3363	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} ↔ (𝑍 ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (𝑍 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄))
422	398, 417, 421	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
423		elun2 3781	. . . . . . . . . . . . . . 15 ⊢ (𝑍 ∈ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
424	422, 423	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
425		foelrn 6378	. . . . . . . . . . . . . 14 ⊢ ((𝑆:(0...𝑁)–onto→({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) ∧ 𝑍 ∈ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖))
426	316, 424, 425	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖))
427	53	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
428	321	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ)
429	320	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
430	13	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
431	330	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
432	275	necomd 2849	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
433	432	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
434	429, 430, 431, 433	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
435	429, 430	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘𝑗)) < 𝐵 ↔ 0 < (𝐵 − (𝐸‘(𝑆‘𝑗)))))
436	434, 435	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 0 < (𝐵 − (𝐸‘(𝑆‘𝑗))))
437	428, 436	elrpd 11869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐵 − (𝐸‘(𝑆‘𝑗))) ∈ ℝ⁺)
438	427, 437	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))))
439	438, 319	syl6breqr 4695	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) < 𝑍)
440	439	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑗) < 𝑍)
441		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → 𝑍 = (𝑆‘𝑖))
442	440, 441	breqtrd 4679	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑗) < (𝑆‘𝑖))
443	394	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → 𝑍 < (𝑆‘(𝑗 + 1)))
444	441, 443	eqbrtrrd 4677	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))
445	442, 444	jca 554	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) ∧ 𝑍 = (𝑆‘𝑖)) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
446	445	ex 450	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (𝑍 = (𝑆‘𝑖) → ((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))))
447	446	reximdv 3016	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → (∃𝑖 ∈ (0...𝑁)𝑍 = (𝑆‘𝑖) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1)))))
448	426, 447	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
449	315, 448	syldan 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
450	251	nrexdv 3001	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
451	450	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)) → ¬ ∃𝑖 ∈ (0...𝑁)((𝑆‘𝑗) < (𝑆‘𝑖) ∧ (𝑆‘𝑖) < (𝑆‘(𝑗 + 1))))
452	449, 451	condan 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))
453	308, 452	jca 554	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1)))
454	130	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ)
455	295	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ)
456		flbi 12617	. . . . . . . . . 10 ⊢ ((((𝐵 − (𝑆‘𝑗)) / 𝑇) ∈ ℝ ∧ (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ∈ ℤ) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
457	454, 455, 456	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ↔ ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) ≤ ((𝐵 − (𝑆‘𝑗)) / 𝑇) ∧ ((𝐵 − (𝑆‘𝑗)) / 𝑇) < ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) + 1))))
458	453, 457	mpbird 247	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)))
459	458	eqcomd 2628	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)))
460	459	oveq1d 6665	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))
461	460	oveq2d 6666	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) = ((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)))
462	461	oveq1d 6665	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))))
463	266	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
464	138	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℂ)
465	139	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇) ∈ ℂ)
466	463, 464, 465	pnpcan2d 10430	. . . 4 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
467	462, 466	eqtrd 2656	. . 3 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (((𝑆‘(𝑗 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝑗 + 1))) / 𝑇)) · 𝑇)) − ((𝑆‘𝑗) + ((⌊‘((𝐵 − (𝑆‘𝑗)) / 𝑇)) · 𝑇))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
468	285, 301, 467	3eqtrd 2660	. 2 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
469	270, 468	pm2.61dan 832	1 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 ∪ cun 3572 ifcif 4086 {cpr 4179 class class class wbr 4653 ↦ cmpt 4729 ran crn 5115 ℩cio 5849 Fn wfn 5883 ⟶wf 5884 –onto→wfo 5886 –1-1-onto→wf1o 5887 ‘cfv 5888 Isom wiso 5889 (class class class)co 6650 ↑_𝑚 cmap 7857 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 (,]cioc 12176 [,]cicc 12178 ...cfz 12326 ..^cfzo 12465 ⌊cfl 12591 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-cmp 21190

This theorem is referenced by: fourierdlem89 40412 fourierdlem90 40413 fourierdlem91 40414

W3C validator