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 46133

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 13439	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
7		fourierdlem68.ab	. . . . . . 7 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
8	6, 7	sstrid 3968	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))
9		fourierdlem68.n0	. . . . . . 7 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
10	6	sseli 3952	. . . . . . 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 46122	. . . . 5 ⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
15	14	simpli 483	. . . 4 ⊢ (𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2)))))
16	15	simpld 494	. . 3 ⊢ (𝜑 → (ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ)
17	16	fdmd 6712	. 2 ⊢ (𝜑 → dom (ℝ D 𝑂) = (𝐴(,)𝐵))
18		eqid 2734	. . . . . 6 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) = (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2))))
19		fourierdlem68.altb	. . . . . . 7 ⊢ (𝜑 → 𝐴 < 𝐵)
20	3, 4, 19	ltled 11375	. . . . . 6 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
21		2re 12306	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
22	21	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℝ)
23	3, 4	iccssred 13440	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
24	23	sselda 3956	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ ℝ)
25	24	rehalfcld 12480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (𝑡 / 2) ∈ ℝ)
26	25	resincld 16146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℝ)
27	22, 26	remulcld 11257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ∈ ℝ)
28		2cnd 12310	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ ℂ)
29	26	recnd 11255	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ∈ ℂ)
30		2ne0 12336	. . . . . . . . . . 11 ⊢ 2 ≠ 0
31	30	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ≠ 0)
32	7	sselda 3956	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ∈ (-π[,]π))
33		eqcom 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 0 ↔ 0 = 𝑡)
34	33	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → 0 = 𝑡)
35	34	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 = 𝑡)
36		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 𝑡 ∈ (𝐴[,]𝐵))
37	35, 36	eqeltrd 2833	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ (𝐴[,]𝐵) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
38	37	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → 0 ∈ (𝐴[,]𝐵))
39	9	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) ∧ 𝑡 = 0) → ¬ 0 ∈ (𝐴[,]𝐵))
40	38, 39	pm2.65da 816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → ¬ 𝑡 = 0)
41	40	neqned 2938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 𝑡 ≠ 0)
42		fourierdlem44 46110	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ (-π[,]π) ∧ 𝑡 ≠ 0) → (sin‘(𝑡 / 2)) ≠ 0)
43	32, 41, 42	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (sin‘(𝑡 / 2)) ≠ 0)
44	28, 29, 31, 43	mulne0d 11881	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → (2 · (sin‘(𝑡 / 2))) ≠ 0)
45		eldifsn 4759	. . . . . . . . 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 7100	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))):(𝐴[,]𝐵)⟶(ℝ ∖ {0}))
48		difss 4109	. . . . . . . . . 10 ⊢ (ℝ ∖ {0}) ⊆ ℝ
49		ax-resscn 11178	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
50	48, 49	sstri 3966	. . . . . . . . 9 ⊢ (ℝ ∖ {0}) ⊆ ℂ
51	50	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (ℝ ∖ {0}) ⊆ ℂ)
52	23, 49	sstrdi 3969	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
53		2cnd 12310	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
54		ssid 3979	. . . . . . . . . . 11 ⊢ ℂ ⊆ ℂ
55	54	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℂ ⊆ ℂ)
56	52, 53, 55	constcncfg 45831	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→ℂ))
57		sincn 26391	. . . . . . . . . . 11 ⊢ sin ∈ (ℂ–cn→ℂ)
58	57	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sin ∈ (ℂ–cn→ℂ))
59	52, 55	idcncfg 45832	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ))
60		eldifsn 4759	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠ 0))
61	28, 31, 60	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴[,]𝐵)) → 2 ∈ (ℂ ∖ {0}))
62		eqid 2734	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) = (𝑡 ∈ (𝐴[,]𝐵) ↦ 2)
63	61, 62	fmptd 7100	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2):(𝐴[,]𝐵)⟶(ℂ ∖ {0}))
64		difssd 4110	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ ∖ {0}) ⊆ ℂ)
65		cncfcdm 24827	. . . . . . . . . . . . 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 257	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ 2) ∈ ((𝐴[,]𝐵)–cn→(ℂ ∖ {0})))
68	59, 67	divcncf 25385	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (𝑡 / 2)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
69	58, 68	cncfmpt1f 24843	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (sin‘(𝑡 / 2))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
70	56, 69	mulcncf 25383	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
71		cncfcdm 24827	. . . . . . . 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 257	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (𝐴[,]𝐵) ↦ (2 · (sin‘(𝑡 / 2)))) ∈ ((𝐴[,]𝐵)–cn→(ℝ ∖ {0})))
74	18, 3, 4, 20, 73	cncficcgt0 45847	. . . . 5 ⊢ (𝜑 → ∃𝑐 ∈ ℝ⁺ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))))
75		reelprrecn 11213	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
76	75	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ℝ ∈ {ℝ, ℂ})
77	1	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ)
78	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ)
79		elioore 13383	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ)
80	79	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ)
81	78, 80	readdcld 11256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ)
82	77, 81	ffvelcdmd 7071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
83	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ)
84	82, 83	resubcld 11657	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ)
85	84	recnd 11255	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
86	85	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ)
87	75	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
88	82	recnd 11255	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
89	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)
90	2, 3	readdcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ)
91	90	rexrd 11277	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ^*)
92	91	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈ ℝ^*)
93	2, 4	readdcld 11256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ)
94	93	rexrd 11277	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ^*)
95	94	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈ ℝ^*)
96	3	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ)
97	96	rexrd 11277	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ^*)
98	4	rexrd 11277	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
99	98	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ^*)
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵))
101		ioogtlb 45452	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
102	97, 99, 100, 101	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠)
103	96, 80, 78, 102	ltadd2dd 11386	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠))
104	4	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ)
105		iooltub 45467	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
106	97, 99, 100, 105	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵)
107	80, 104, 78, 106	ltadd2dd 11386	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵))
108	92, 95, 81, 103, 107	eliood 45455	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))
109	89, 108	ffvelcdmd 7071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℝ)
110		eqid 2734	. . . . . . . . . . 11 ⊢ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
111	1, 2, 3, 4, 110, 5	fourierdlem28 46094	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
112	83	recnd 11255	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ)
113		0red 11230	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
114		iooretop 24689	. . . . . . . . . . . . 13 ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,))
115		tgioo4 24729	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
116	114, 115	eleqtri 2831	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
117	116	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
118	12	recnd 11255	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℂ)
119	87, 117, 118	dvmptconst 45874	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0))
120	87, 88, 109, 111, 112, 113, 119	dvmptsub 25908	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)))
121	109	recnd 11255	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
122	121	subid1d 11575	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
123	122	mpteq2dva 5211	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) − 0)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
124	120, 123	eqtrd 2769	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
125	124	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
126	121	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) ∈ ℂ)
127		2cnd 12310	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℂ)
128	79	recnd 11255	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℂ)
129	128	halfcld 12478	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℂ)
130	129	sincld 16133	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (sin‘(𝑠 / 2)) ∈ ℂ)
131	127, 130	mulcld 11247	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
132	131	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
133		fourierdlem68.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℝ)
134	133	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝐸 ∈ ℝ)
135		1re 11227	. . . . . . . . 9 ⊢ 1 ∈ ℝ
136	21, 135	remulcli 11243	. . . . . . . 8 ⊢ (2 · 1) ∈ ℝ
137	136	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (2 · 1) ∈ ℝ)
138		1red 11228	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 1 ∈ ℝ)
139		fourierdlem68.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℝ)
140	118	abscld 15442	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
141	139, 140	readdcld 11256	. . . . . . . 8 ⊢ (𝜑 → (𝐷 + (abs‘𝐶)) ∈ ℝ)
142	141	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
143		simpl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝜑)
144	143, 108	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
145		eleq1 2821	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ↔ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))
146	145	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑋 + 𝑠) → ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) ↔ (𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))))
147		fveq2 6872	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑋 + 𝑠) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡) = ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))
148	147	fveq2d 6876	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) = (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))))
149	148	breq1d 5126	. . . . . . . . . . 11 ⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸 ↔ (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
150	146, 149	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)))
151		fourierdlem68.fdvbd	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)
152	150, 151	vtoclg 3531	. . . . . . . . 9 ⊢ ((𝑋 + 𝑠) ∈ ℝ → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸))
153	81, 144, 152	sylc 65	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
154	153	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ≤ 𝐸)
155	127, 130	absmuld 15460	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) = ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))))
156		0le2 12334	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
157		absid 15302	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
158	21, 156, 157	mp2an 692	. . . . . . . . . . 11 ⊢ (abs‘2) = 2
159	158	oveq1i 7409	. . . . . . . . . 10 ⊢ ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) = (2 · (abs‘(sin‘(𝑠 / 2))))
160	130	abscld 15442	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ∈ ℝ)
161		1red 11228	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 1 ∈ ℝ)
162	21	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 2 ∈ ℝ)
163	156	a1i 11	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → 0 ≤ 2)
164	79	rehalfcld 12480	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (𝑠 / 2) ∈ ℝ)
165		abssinbd 45251	. . . . . . . . . . . 12 ⊢ ((𝑠 / 2) ∈ ℝ → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
166	164, 165	syl 17	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(sin‘(𝑠 / 2))) ≤ 1)
167	160, 161, 162, 163, 166	lemul2ad 12174	. . . . . . . . . 10 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (2 · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
168	159, 167	eqbrtrid 5151	. . . . . . . . 9 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → ((abs‘2) · (abs‘(sin‘(𝑠 / 2)))) ≤ (2 · 1))
169	155, 168	eqbrtrd 5138	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
170	169	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(2 · (sin‘(𝑠 / 2)))) ≤ (2 · 1))
171		abscosbd 45234	. . . . . . . . 9 ⊢ ((𝑠 / 2) ∈ ℝ → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
172	100, 164, 171	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
173	172	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(cos‘(𝑠 / 2))) ≤ 1)
174	85	abscld 15442	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∈ ℝ)
175	88	abscld 15442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ∈ ℝ)
176	112	abscld 15442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘𝐶) ∈ ℝ)
177	175, 176	readdcld 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ∈ ℝ)
178	139	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐷 ∈ ℝ)
179	178, 176	readdcld 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐷 + (abs‘𝐶)) ∈ ℝ)
180	88, 112	abs2dif2d 15464	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)))
181		fveq2 6872	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (𝑋 + 𝑠) → (𝐹‘𝑡) = (𝐹‘(𝑋 + 𝑠)))
182	181	fveq2d 6876	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑋 + 𝑠) → (abs‘(𝐹‘𝑡)) = (abs‘(𝐹‘(𝑋 + 𝑠))))
183	182	breq1d 5126	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑋 + 𝑠) → ((abs‘(𝐹‘𝑡)) ≤ 𝐷 ↔ (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
184	146, 183	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑋 + 𝑠) → (((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷) ↔ ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)))
185		fourierdlem68.fbd	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷)
186	184, 185	vtoclg 3531	. . . . . . . . . . 11 ⊢ ((𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) → ((𝜑 ∧ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷))
187	108, 144, 186	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘(𝐹‘(𝑋 + 𝑠))) ≤ 𝐷)
188	175, 178, 176, 187	leadd1dd 11843	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((abs‘(𝐹‘(𝑋 + 𝑠))) + (abs‘𝐶)) ≤ (𝐷 + (abs‘𝐶)))
189	174, 177, 179, 180, 188	letrd 11384	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
190	189	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (abs‘((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ≤ (𝐷 + (abs‘𝐶)))
191	14	simpri 485	. . . . . . . 8 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2)))
192	191	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
193	129	coscld 16134	. . . . . . . 8 ⊢ (𝑠 ∈ (𝐴(,)𝐵) → (cos‘(𝑠 / 2)) ∈ ℂ)
194	193	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (cos‘(𝑠 / 2)) ∈ ℂ)
195		simp2 1137	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → 𝑐 ∈ ℝ⁺)
196		oveq1 7406	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑠 → (𝑡 / 2) = (𝑠 / 2))
197	196	fveq2d 6876	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (sin‘(𝑡 / 2)) = (sin‘(𝑠 / 2)))
198	197	oveq2d 7415	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → (2 · (sin‘(𝑡 / 2))) = (2 · (sin‘(𝑠 / 2))))
199	198	fveq2d 6876	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑠 → (abs‘(2 · (sin‘(𝑡 / 2)))) = (abs‘(2 · (sin‘(𝑠 / 2)))))
200	199	breq2d 5128	. . . . . . . . . 10 ⊢ (𝑡 = 𝑠 → (𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
201	200	cbvralvw 3218	. . . . . . . . 9 ⊢ (∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) ↔ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
202		nfv 1913	. . . . . . . . . . 11 ⊢ Ⅎ𝑠𝜑
203		nfra1 3264	. . . . . . . . . . 11 ⊢ Ⅎ𝑠∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))
204	202, 203	nfan 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑠(𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
205		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
206	6, 100	sselid 3954	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
207	206	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴[,]𝐵))
208		rspa 3229	. . . . . . . . . . . 12 ⊢ ((∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))) ∧ 𝑠 ∈ (𝐴[,]𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
209	205, 207, 208	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
210	209	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → (𝑠 ∈ (𝐴(,)𝐵) → 𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))))
211	204, 210	ralrimi 3238	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑠 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
212	201, 211	sylan2b 594	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
213	212	3adant2 1131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∀𝑠 ∈ (𝐴(,)𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑠 / 2)))))
214		eqid 2734	. . . . . . 7 ⊢ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
215	76, 86, 125, 126, 132, 134, 137, 138, 142, 154, 170, 173, 190, 192, 194, 195, 213, 214	dvdivbd 45882	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ⁺ ∧ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2))))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
216	215	rexlimdv3a 3143	. . . . 5 ⊢ (𝜑 → (∃𝑐 ∈ ℝ⁺ ∀𝑡 ∈ (𝐴[,]𝐵)𝑐 ≤ (abs‘(2 · (sin‘(𝑡 / 2)))) → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
217	74, 216	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
218		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑠ℝ
219		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑠 D
220		nfmpt1 5217	. . . . . . . . . 10 ⊢ Ⅎ𝑠(𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))
221	13, 220	nfcxfr 2895	. . . . . . . . 9 ⊢ Ⅎ𝑠𝑂
222	218, 219, 221	nfov 7429	. . . . . . . 8 ⊢ Ⅎ𝑠(ℝ D 𝑂)
223	222	nfdm 5928	. . . . . . 7 ⊢ Ⅎ𝑠dom (ℝ D 𝑂)
224		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑠(𝐴(,)𝐵)
225	223, 224	raleqf 3330	. . . . . 6 ⊢ (dom (ℝ D 𝑂) = (𝐴(,)𝐵) → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
226	17, 225	syl 17	. . . . 5 ⊢ (𝜑 → (∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
227	226	rexbidv 3162	. . . 4 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ (𝐴(,)𝐵)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
228	217, 227	mpbird 257	. . 3 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏)
229	13	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))
230	229	oveq2d 7415	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝑂) = (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))))
231	230	fveq1d 6874	. . . . . 6 ⊢ (𝜑 → ((ℝ D 𝑂)‘𝑠) = ((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠))
232	231	fveq2d 6876	. . . . 5 ⊢ (𝜑 → (abs‘((ℝ D 𝑂)‘𝑠)) = (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)))
233	232	breq1d 5126	. . . 4 ⊢ (𝜑 → ((abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ (abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
234	233	rexralbidv 3205	. . 3 ⊢ (𝜑 → (∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏 ↔ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2))))))‘𝑠)) ≤ 𝑏))
235	228, 234	mpbird 257	. 2 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏)
236	17, 235	jca 511	1 ⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ∃wrex 3059 ∖ cdif 3921 ⊆ wss 3924 {csn 4599 {cpr 4601 class class class wbr 5116 ↦ cmpt 5198 dom cdm 5651 ran crn 5652 ↾ cres 5653 ⟶wf 6523 ‘cfv 6527 (class class class)co 7399 ℂcc 11119 ℝcr 11120 0cc0 11121 1c1 11122 + caddc 11124 · cmul 11126 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 − cmin 11458 -cneg 11459 / cdiv 11886 2c2 12287 ℝ⁺crp 13000 (,)cioo 13353 [,]cicc 13356 ↑cexp 14068 abscabs 15240 sincsin 16066 cosccos 16067 πcpi 16069 ↾_t crest 17419 TopOpenctopn 17420 topGenctg 17436 ℂ_fldccnfld 21300 –cn→ccncf 24805 D cdv 25801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5246 ax-sep 5263 ax-nul 5273 ax-pow 5332 ax-pr 5399 ax-un 7723 ax-inf2 9647 ax-cnex 11177 ax-resscn 11178 ax-1cn 11179 ax-icn 11180 ax-addcl 11181 ax-addrcl 11182 ax-mulcl 11183 ax-mulrcl 11184 ax-mulcom 11185 ax-addass 11186 ax-mulass 11187 ax-distr 11188 ax-i2m1 11189 ax-1ne0 11190 ax-1rid 11191 ax-rnegex 11192 ax-rrecex 11193 ax-cnre 11194 ax-pre-lttri 11195 ax-pre-lttrn 11196 ax-pre-ltadd 11197 ax-pre-mulgt0 11198 ax-pre-sup 11199 ax-addf 11200

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3357 df-reu 3358 df-rab 3414 df-v 3459 df-sbc 3764 df-csb 3873 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-pss 3944 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-tp 4604 df-op 4606 df-uni 4881 df-int 4920 df-iun 4966 df-iin 4967 df-br 5117 df-opab 5179 df-mpt 5199 df-tr 5227 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6287 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6480 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7356 df-ov 7402 df-oprab 7403 df-mpo 7404 df-of 7665 df-om 7856 df-1st 7982 df-2nd 7983 df-supp 8154 df-frecs 8274 df-wrecs 8305 df-recs 8379 df-rdg 8418 df-1o 8474 df-2o 8475 df-er 8713 df-map 8836 df-pm 8837 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9368 df-fi 9417 df-sup 9448 df-inf 9449 df-oi 9516 df-card 9945 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11460 df-neg 11461 df-div 11887 df-nn 12233 df-2 12295 df-3 12296 df-4 12297 df-5 12298 df-6 12299 df-7 12300 df-8 12301 df-9 12302 df-n0 12494 df-z 12581 df-dec 12701 df-uz 12845 df-q 12957 df-rp 13001 df-xneg 13120 df-xadd 13121 df-xmul 13122 df-ioo 13357 df-ioc 13358 df-ico 13359 df-icc 13360 df-fz 13514 df-fzo 13661 df-fl 13798 df-mod 13876 df-seq 14009 df-exp 14069 df-fac 14280 df-bc 14309 df-hash 14337 df-shft 15073 df-cj 15105 df-re 15106 df-im 15107 df-sqrt 15241 df-abs 15242 df-limsup 15474 df-clim 15491 df-rlim 15492 df-sum 15690 df-ef 16070 df-sin 16072 df-cos 16073 df-pi 16075 df-struct 17151 df-sets 17168 df-slot 17186 df-ndx 17198 df-base 17214 df-ress 17237 df-plusg 17269 df-mulr 17270 df-starv 17271 df-sca 17272 df-vsca 17273 df-ip 17274 df-tset 17275 df-ple 17276 df-ds 17278 df-unif 17279 df-hom 17280 df-cco 17281 df-rest 17421 df-topn 17422 df-0g 17440 df-gsum 17441 df-topgen 17442 df-pt 17443 df-prds 17446 df-xrs 17501 df-qtop 17506 df-imas 17507 df-xps 17509 df-mre 17583 df-mrc 17584 df-acs 17586 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-mulg 19036 df-cntz 19285 df-cmn 19748 df-psmet 21292 df-xmet 21293 df-met 21294 df-bl 21295 df-mopn 21296 df-fbas 21297 df-fg 21298 df-cnfld 21301 df-top 22817 df-topon 22834 df-topsp 22856 df-bases 22869 df-cld 22942 df-ntr 22943 df-cls 22944 df-nei 23021 df-lp 23059 df-perf 23060 df-cn 23150 df-cnp 23151 df-t1 23237 df-haus 23238 df-cmp 23310 df-tx 23485 df-hmeo 23678 df-fil 23769 df-fm 23861 df-flim 23862 df-flf 23863 df-xms 24244 df-ms 24245 df-tms 24246 df-cncf 24807 df-limc 25804 df-dv 25805

This theorem is referenced by: fourierdlem80 46145

W3C validator