fourierdlem68 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem68 43715

Description: The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem68.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem68.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem68.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem68.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem68.altb	⊢ (𝜑 → 𝐴 < 𝐵)
fourierdlem68.ab	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem68.n0	⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem68.fdv	⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
fourierdlem68.d	⊢ (𝜑 → 𝐷 ∈ ℝ)
fourierdlem68.fbd	⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷)
fourierdlem68.e	⊢ (𝜑 → 𝐸 ∈ ℝ)
fourierdlem68.fdvbd	⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
fourierdlem68.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem68.o	⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))

**Assertion**
Ref	Expression
fourierdlem68	⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))

Distinct variable groups: 𝐴,𝑏,𝑠 𝑡,𝐴,𝑠 𝐵,𝑏,𝑠 𝑡,𝐵 𝐶,𝑏,𝑠 𝐷,𝑏,𝑠 𝑡,𝐷 𝐸,𝑏,𝑠 𝑡,𝐸 𝐹,𝑏,𝑠 𝑡,𝐹 𝑋,𝑏,𝑠 𝑡,𝑋 𝜑,𝑏,𝑠 𝜑,𝑡 Allowed substitution hints: 𝐶(𝑡) 𝑂(𝑡,𝑠,𝑏)

Proof of Theorem fourierdlem68 Dummy variable 𝑐 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem68.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem68.xre	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ ℝ)
3		fourierdlem68.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		fourierdlem68.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		fourierdlem68.fdv	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
6		ioossicc 13165	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
7		fourierdlem68.ab	. . . . . . 7 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
8	6, 7	sstrid 3932	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
9		fourierdlem68.n0	. . . . . . 7 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
10	6	sseli 3917	. . . . . . 7 ⊢ (0 ∈ (𝐴(,)𝐵) → 0 ∈ (𝐴[,]𝐵))
11	9, 10	nsyl 140	. . . . . 6 ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))
12		fourierdlem68.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℝ)
13		fourierdlem68.o	. . . . . 6 ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
14	1, 2, 3, 4, 5, 8, 11, 12, 13	fourierdlem57 43704	. . . . 5 ⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
15	14	simpli 484	. . . 4 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
16	15	simpld 495	. . 3 ⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
17	16	fdmd 6611	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
18		eqid 2738	. . . . . 6 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2))))
19		fourierdlem68.altb	. . . . . . 7 ⊢ (𝜑 → 𝐴 < 𝐵)
20	3, 4, 19	ltled 11123	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
21		2re 12047	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
22	21	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ)
23	3, 4	iccssred 13166	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
24	23	sselda 3921	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ)
25	24	rehalfcld 12220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ)
26	25	resincld 15852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ)
27	22, 26	remulcld 11005	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ ℝ)
28		2cnd 12051	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
29	26	recnd 11003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ)
30		2ne0 12077	. . . . . . . . . . 11 ⊢ 2 ≠ 0
31	30	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
32	7	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π))
33		eqcom 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 0 ↔ 0 = 𝑡)
34	33	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → 0 = 𝑡)
35	34	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡)
36		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵))
37	35, 36	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
38	37	adantll 711	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
39	9	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
40	38, 39	pm2.65da 814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0)
41	40	neqned 2950	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0)
42		fourierdlem44 43692	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ (-π[,]π) ∧ 𝑡 ≠ 0) → (sin‘(𝑡 / 2)) ≠ 0)
43	32, 41, 42	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0)
44	28, 29, 31, 43	mulne0d 11627	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0)
45		eldifsn 4720	. . . . . . . . 9 ⊢ ((2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}) ↔ ((2 · (sin‘(𝑡 / 2))) ∈ ℝ ∧ (2 · (sin‘(𝑡 / 2))) ≠ 0))
46	27, 44, 45	sylanbrc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ (ℝ ∖ {0}))
47	46, 18	fmptd 6988	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0}))
48		difss 4066	. . . . . . . . . 10 ⊢ (ℝ ∖ {0}) ⊆ ℝ
49		ax-resscn 10928	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
50	48, 49	sstri 3930	. . . . . . . . 9 ⊢ (ℝ ∖ {0}) ⊆ ℂ
51	50	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ ∖ {0}) ⊆ ℂ)
52	23, 49	sstrdi 3933	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
53		2cnd 12051	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
54		ssid 3943	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
55	54	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℂ ⊆ ℂ)
56	52, 53, 55	constcncfg 43413	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ))
57		sincn 25603	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
58	57	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
59	52, 55	idcncfg 43414	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
60		eldifsn 4720	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
61	28, 31, 60	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖ {0}))
62		eqid 2738	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2)
63	61, 62	fmptd 6988	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0}))
64		difssd 4067	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
65		cncffvrn 24061	. . . . . . . . . . . . 13 ⊢ (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
66	64, 56, 65	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0})))
67	63, 66	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
68	59, 67	divcncf 24611	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
69	58, 68	cncfmpt1f 24077	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
70	56, 69	mulcncf 24610	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
71		cncffvrn 24061	. . . . . . . 8 ⊢ (((ℝ ∖ {0}) ⊆ ℂ ∧ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
72	51, 70, 71	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})) ↔ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0})))
73	47, 72	mpbird 256	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})))
74	18, 3, 4, 20, 73	cncficcgt0 43429	. . . . 5 ⊢ (𝜑 → ∃𝑐 ∈ ℝ⁺ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))))
75		reelprrecn 10963	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
76	75	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ℝ ∈ {ℝ, ℂ})
77	1	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
78	2	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
79		elioore 13109	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
80	79	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
81	78, 80	readdcld 11004	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
82	77, 81	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
83	12	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
84	82, 83	resubcld 11403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
85	84	recnd 11003	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
86	85	3ad2antl1 1184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
87	75	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
88	82	recnd 11003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
89	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
90	2, 3	readdcld 11004	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
91	90	rexrd 11025	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ^*)
92	91	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ^*)
93	2, 4	readdcld 11004	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
94	93	rexrd 11025	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ^*)
95	94	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ^*)
96	3	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
97	96	rexrd 11025	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
98	4	rexrd 11025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
99	98	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
100		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
101		ioogtlb 43033	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
102	97, 99, 100, 101	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
103	96, 80, 78, 102	ltadd2dd 11134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
104	4	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
105		iooltub 43048	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
106	97, 99, 100, 105	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
107	80, 104, 78, 106	ltadd2dd 11134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
108	92, 95, 81, 103, 107	eliood 43036	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
109	89, 108	ffvelrnd 6962	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
110		eqid 2738	. . . . . . . . . . 11 ⊢ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
111	1, 2, 3, 4, 110, 5	fourierdlem28 43676	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
112	83	recnd 11003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
113		0red 10978	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
114		iooretop 23929	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
115		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
116	115	tgioo2 23966	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
117	114, 116	eleqtri 2837	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
119	12	recnd 11003	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
120	87, 118, 119	dvmptconst 43456	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
121	87, 88, 109, 111, 112, 113, 120	dvmptsub 25131	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
122	109	recnd 11003	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
123	122	subid1d 11321	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
124	123	mpteq2dva 5174	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
125	121, 124	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
126	125	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
127	122	3ad2antl1 1184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
128		2cnd 12051	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ)
129	79	recnd 11003	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ)
130	129	halfcld 12218	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ)
131	130	sincld 15839	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ)
132	128, 131	mulcld 10995	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
133	132	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
134		fourierdlem68.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℝ)
135	134	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝐸 ∈ ℝ)
136		1re 10975	. . . . . . . . 9 ⊢ 1 ∈ ℝ
137	21, 136	remulcli 10991	. . . . . . . 8 ⊢ (2 · 1) ∈ ℝ
138	137	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (2 · 1) ∈ ℝ)
139		1red 10976	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 1 ∈ ℝ)
140		fourierdlem68.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℝ)
141	119	abscld 15148	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
142	140, 141	readdcld 11004	. . . . . . . 8 ⊢ (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ)
143	142	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
144		simpl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝜑)
145	144, 108	jca 512	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
146		eleq1 2826	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
147	146	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑋 + 𝑠) → ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))))
148		fveq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
149	148	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
150	149	breq1d 5084	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
151	147, 150	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)))
152		fourierdlem68.fdvbd	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
153	151, 152	vtoclg 3505	. . . . . . . . 9 ⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
154	81, 145, 153	sylc 65	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
155	154	3ad2antl1 1184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
156	128, 131	absmuld 15166	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) = ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))))
157		0le2 12075	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
158		absid 15008	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
159	21, 157, 158	mp2an 689	. . . . . . . . . . 11 ⊢ (abs‘2) = 2
160	159	oveq1i 7285	. . . . . . . . . 10 ⊢ ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 · (abs‘(sin‘(𝑠 / 2))))
161	131	abscld 15148	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈ ℝ)
162		1red 10976	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ)
163	21	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ)
164	157	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2)
165	79	rehalfcld 12220	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ)
166		abssinbd 42834	. . . . . . . . . . . 12 ⊢ ((𝑠 / 2) ∈ ℝ → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
167	165, 166	syl 17	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
168	161, 162, 163, 164, 167	lemul2ad 11915	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
169	160, 168	eqbrtrid 5109	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
170	156, 169	eqbrtrd 5096	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
171	170	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
172		abscosbd 42817	. . . . . . . . 9 ⊢ ((𝑠 / 2) ∈ ℝ → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
173	100, 165, 172	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
174	173	3ad2antl1 1184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
175	85	abscld 15148	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
176	88	abscld 15148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ)
177	112	abscld 15148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ)
178	176, 177	readdcld 11004	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ)
179	140	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ)
180	179, 177	readdcld 11004	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
181	88, 112	abs2dif2d 15170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)))
182		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝑋 + 𝑠) → (𝐹‘𝑡) = (𝐹‘(𝑋 + 𝑠)))
183	182	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹‘𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠))))
184	183	breq1d 5084	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹‘𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
185	147, 184	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)))
186		fourierdlem68.fbd	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷)
187	185, 186	vtoclg 3505	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
188	108, 145, 187	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)
189	176, 179, 177, 188	leadd1dd 11589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶)))
190	175, 178, 180, 181, 189	letrd 11132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
191	190	3ad2antl1 1184	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
192	14	simpri 486	. . . . . . . 8 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
193	192	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
194	130	coscld 15840	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
195	194	adantl 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
196		simp2 1136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝑐 ∈ ℝ⁺)
197		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2))
198	197	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2)))
199	198	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 · (sin‘(𝑠 / 2))))
200	199	fveq2d 6778	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (abs‘(2 · (sin‘(𝑡 / 2)))) = (abs‘(2 · (sin‘(𝑠 / 2)))))
201	200	breq2d 5086	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
202	201	cbvralvw 3383	. . . . . . . . 9 ⊢ (∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
203		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑠𝜑
204		nfra1 3144	. . . . . . . . . . 11 ⊢ Ⅎ𝑠∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))
205	203, 204	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
206		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
207	6, 100	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
208	207	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
209		rspa 3132	. . . . . . . . . . . 12 ⊢ ((∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))) ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
210	206, 208, 209	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
211	210	ex 413	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
212	205, 211	ralrimi 3141	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
213	202, 212	sylan2b 594	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
214	213	3adant2 1130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
215		eqid 2738	. . . . . . 7 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
216	76, 86, 126, 127, 133, 135, 138, 139, 143, 155, 171, 174, 191, 193, 195, 196, 214, 215	dvdivbd 43464	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
217	216	rexlimdv3a 3215	. . . . 5 ⊢ (𝜑 → (∃𝑐 ∈ ℝ⁺ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
218	74, 217	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
219		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑠ℝ
220		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑠 D
221		nfmpt1 5182	. . . . . . . . . 10 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
222	13, 221	nfcxfr 2905	. . . . . . . . 9 ⊢ Ⅎ𝑠𝑂
223	219, 220, 222	nfov 7305	. . . . . . . 8 ⊢ Ⅎ𝑠(ℝ D 𝑂)
224	223	nfdm 5860	. . . . . . 7 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
225		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑠(𝐴(,)𝐵)
226	224, 225	raleqf 3332	. . . . . 6 ⊢ (dom (ℝ D 𝑂) = (𝐴(,)𝐵) → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
227	17, 226	syl 17	. . . . 5 ⊢ (𝜑 → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
228	227	rexbidv 3226	. . . 4 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
229	218, 228	mpbird 256	. . 3 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
230	13	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
231	230	oveq2d 7291	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
232	231	fveq1d 6776	. . . . . 6 ⊢ (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))
233	232	fveq2d 6778	. . . . 5 ⊢ (𝜑 → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)))
234	233	breq1d 5084	. . . 4 ⊢ (𝜑 → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
235	234	rexralbidv 3230	. . 3 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
236	229, 235	mpbird 256	. 2 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
237	17, 236	jca 512	1 ⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 ∖ cdif 3884 ⊆ wss 3887 {csn 4561 {cpr 4563 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ran crn 5590 ↾ cres 5591 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 -cneg 11206 / cdiv 11632 2c2 12028 ℝ⁺crp 12730 (,)cioo 13079 [,]cicc 13082 ↑cexp 13782 abscabs 14945 sincsin 15773 cosccos 15774 πcpi 15776 ↾_t crest 17131 TopOpenctopn 17132 topGenctg 17148 ℂ_fldccnfld 20597 –cn→ccncf 24039 D cdv 25027

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-er 8498 df-map 8617 df-pm 8618 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-fac 13988 df-bc 14017 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398 df-ef 15777 df-sin 15779 df-cos 15780 df-pi 15782 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-hom 16986 df-cco 16987 df-rest 17133 df-topn 17134 df-0g 17152 df-gsum 17153 df-topgen 17154 df-pt 17155 df-prds 17158 df-xrs 17213 df-qtop 17218 df-imas 17219 df-xps 17221 df-mre 17295 df-mrc 17296 df-acs 17298 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-submnd 18431 df-mulg 18701 df-cntz 18923 df-cmn 19388 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-t1 22465 df-haus 22466 df-cmp 22538 df-tx 22713 df-hmeo 22906 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-xms 23473 df-ms 23474 df-tms 23475 df-cncf 24041 df-limc 25030 df-dv 25031

This theorem is referenced by: fourierdlem80 43727

W3C validator