fperdvper - Mathbox for Glauco Siliprandi

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

Theorem fperdvper 45915

Description: The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fperdvper.f	⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
fperdvper.t	⊢ (𝜑 → 𝑇 ∈ ℝ)
fperdvper.fper	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fperdvper.g	⊢ 𝐺 = (ℝ D 𝐹)

**Assertion**
Ref	Expression
fperdvper	⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))

Distinct variable groups: 𝑥,𝐹 𝑥,𝑇 𝜑,𝑥 Allowed substitution hint: 𝐺(𝑥)

Proof of Theorem fperdvper Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvbsss 25860	. . . . . . . 8 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
2		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom 𝐺)
3		fperdvper.g	. . . . . . . . . 10 ⊢ 𝐺 = (ℝ D 𝐹)
4	3	dmeqi 5889	. . . . . . . . 9 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
5	2, 4	eleqtrdi 2845	. . . . . . . 8 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom (ℝ D 𝐹))
6	1, 5	sselid 3961	. . . . . . 7 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ ℝ)
7	6	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
8		fperdvper.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑇 ∈ ℝ)
10	7, 9	readdcld 11269	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
11		reopn 45285	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		retop 24705	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Top
13		ssidd 3987	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℝ)
14		uniretop 24706	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	isopn3 23009	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ℝ ⊆ ℝ) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
16	12, 13, 15	sylancr 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
17	11, 16	mpbii 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((int‘(topGen‘ran (,)))‘ℝ) = ℝ)
18	17	eqcomd 2742	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ = ((int‘(topGen‘ran (,)))‘ℝ))
19	10, 18	eleqtrd 2837	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ))
20	5	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom (ℝ D 𝐹))
21	3	fveq1i 6882	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) = ((ℝ D 𝐹)‘𝑥)
22	21	eqcomi 2745	. . . . . . . . 9 ⊢ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥)
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))
24		dvf 25865	. . . . . . . . . . . 12 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
25		ffun 6714	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (ℝ D 𝐹)
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (ℝ D 𝐹))
28		funbrfv2b 6941	. . . . . . . . . 10 ⊢ (Fun (ℝ D 𝐹) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
30	29	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
31	20, 23, 30	mpbir2and 713	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥(ℝ D 𝐹)(𝐺‘𝑥))
32		tgioo4 24749	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
33		eqid 2736	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
34		eqid 2736	. . . . . . . 8 ⊢ (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))
35		ax-resscn 11191	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℂ)
37		fperdvper.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
38	37	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐹:ℝ⟶ℂ)
39	32, 33, 34, 36, 38, 13	eldv 25856	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))))
40	31, 39	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥)))
41	40	simprd 495	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))
42		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
43		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑑 → (𝐹‘𝑦) = (𝐹‘𝑑))
44	43	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))))
45		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 − (𝑥 + 𝑇)) = (𝑑 − (𝑥 + 𝑇)))
46	44, 45	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))))
47		eldifi 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℝ)
48	47	recnd 11268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℂ)
49	48	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
50	8	recnd 11268	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
51	50	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
52	49, 51	npcand 11603	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) + 𝑇) = 𝑑)
53	52	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 = ((𝑑 − 𝑇) + 𝑇))
54	53	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
55		ovex 7443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 − 𝑇) ∈ V
56	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
57	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
58	56, 57	resubcld 11670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
59	58	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → (𝑑 − 𝑇) ∈ ℝ))
60	59	imdistani 568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ))
61		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝑥 ∈ ℝ ↔ (𝑑 − 𝑇) ∈ ℝ))
62	61	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ)))
63		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
64		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑑 − 𝑇)))
65	63, 64	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
66	62, 65	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑑 − 𝑇) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))))
67		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
68	66, 67	vtoclg 3538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑 − 𝑇) ∈ V → ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
69	55, 60, 68	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))
70	54, 69	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
71	70	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
72		simpll 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝜑)
73	6	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℝ)
74	72, 73, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
75	71, 74	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
76	48	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
77	72, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
78	7	recnd 11268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℂ)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℂ)
80	76, 77, 79	subsub4d 11630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑇 + 𝑥)))
81	77, 79	addcomd 11442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑇 + 𝑥) = (𝑥 + 𝑇))
82	81	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑇 + 𝑥)) = (𝑑 − (𝑥 + 𝑇)))
83	80, 82	eqtr2d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑥 + 𝑇)) = ((𝑑 − 𝑇) − 𝑥))
84	75, 83	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
85	46, 84	sylan9eqr 2793	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = 𝑑) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
86		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
87	37	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝐹:ℝ⟶ℂ)
88	87, 58	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
89	88	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
90	38, 7	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐹‘𝑥) ∈ ℂ)
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑥) ∈ ℂ)
92	89, 91	subcld 11599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) ∈ ℂ)
93	76, 77	subcld 11599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℂ)
94	93, 79	subcld 11599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ∈ ℂ)
95		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑑 − 𝑇) = 𝑥)
96	48	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ∈ ℂ)
97	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑇 ∈ ℂ)
98	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑥 ∈ ℂ)
99	96, 97, 98	subadd2d 11618	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ((𝑑 − 𝑇) = 𝑥 ↔ (𝑥 + 𝑇) = 𝑑))
100	95, 99	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑥 + 𝑇) = 𝑑)
101	100	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 = (𝑥 + 𝑇))
102		eldifsni 4771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ≠ (𝑥 + 𝑇))
103	102	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ≠ (𝑥 + 𝑇))
104	103	neneqd 2938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ¬ 𝑑 = (𝑥 + 𝑇))
105	101, 104	pm2.65da 816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) = 𝑥)
106	105	neqned 2940	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ≠ 𝑥)
107	93, 79, 106	subne0d 11608	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ≠ 0)
108	92, 94, 107	divcld 12022	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) ∈ ℂ)
109	42, 85, 86, 108	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
110	109	fvoveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
111	110	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
112		neeq1 2995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → (𝑐 ≠ 𝑥 ↔ (𝑑 − 𝑇) ≠ 𝑥))
113		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑑 − 𝑇) → (abs‘(𝑐 − 𝑥)) = (abs‘((𝑑 − 𝑇) − 𝑥)))
114	113	breq1d 5134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → ((abs‘(𝑐 − 𝑥)) < 𝑏 ↔ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
115	112, 114	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑑 − 𝑇) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ↔ ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)))
116	115	imbrov2fvoveq 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑑 − 𝑇) → (((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)))
117		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
118	47	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑑 ∈ ℝ)
119	8	ad4antr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑇 ∈ ℝ)
120	118, 119	resubcld 11670	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ ℝ)
121		elsni 4623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 − 𝑇) ∈ {𝑥} → (𝑑 − 𝑇) = 𝑥)
122	105, 121	nsyl 140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
123	122	ad4ant13 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
124	120, 123	eldifd 3942	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
125	116, 117, 124	rspcdva 3607	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
126		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
127		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → 𝑦 = (𝑑 − 𝑇))
128	127	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝐹‘𝑦) = (𝐹‘(𝑑 − 𝑇)))
129	128	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
130	127	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝑦 − 𝑥) = ((𝑑 − 𝑇) − 𝑥))
131	129, 130	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
132	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
133	72, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
134	132, 133	resubcld 11670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
135	134, 122	eldifd 3942	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
136	126, 131, 135, 108	fvmptd 6998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
137	136	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
138	137	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
139	138	fvoveq1d 7432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)))
140	106	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ≠ 𝑥)
141	83	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
142	141	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
143	142	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) = (abs‘(𝑑 − (𝑥 + 𝑇))))
144		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)
145	143, 144	eqbrtrd 5146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)
146	140, 145	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
147	146	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
148		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
149	147, 148	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)
150	139, 149	eqbrtrd 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
151	150	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
152	151	adantllr 719	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
153	125, 152	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
154	153	adantrl 716	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
155	111, 154	eqbrtrd 5146	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)
156	155	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
157	156	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
158		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
159		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
160	159	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑐) − (𝐹‘𝑥)))
161		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 − 𝑥) = (𝑐 − 𝑥))
162	160, 161	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
163	162	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ (ℝ ∖ {𝑥}) ∧ 𝑦 = 𝑐) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
164		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ (ℝ ∖ {𝑥}))
165		ovexd 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) ∈ V)
166	158, 163, 164, 165	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
167	166	fvoveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
168	167	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
169		simpll 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝜑)
170		eldifi 4111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℝ)
171	170	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℝ)
172		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ ℝ ↔ 𝑐 ∈ ℝ))
173	172	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑐 ∈ ℝ)))
174		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑐 + 𝑇)))
175		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
176	174, 175	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐)))
177	173, 176	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑐 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))))
178	177, 67	chvarvv 1989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))
179	178	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
180	169, 171, 179	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
181	6	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℝ)
182	169, 181, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
183	182	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑥) = (𝐹‘(𝑥 + 𝑇)))
184	180, 183	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝐹‘𝑐) − (𝐹‘𝑥)) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
185	171	recnd 11268	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℂ)
186	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℂ)
187	169, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℂ)
188	185, 186, 187	pnpcan2d 11637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
189	188	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 − 𝑥) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
190	184, 189	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
191	190	fvoveq1d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
192	191	ad4ant13 751	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
193		neeq1 2995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → (𝑑 ≠ (𝑥 + 𝑇) ↔ (𝑐 + 𝑇) ≠ (𝑥 + 𝑇)))
194		fvoveq1 7433	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑐 + 𝑇) → (abs‘(𝑑 − (𝑥 + 𝑇))) = (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))))
195	194	breq1d 5134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → ((abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏 ↔ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
196	193, 195	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑐 + 𝑇) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ↔ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)))
197	196	imbrov2fvoveq 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑐 + 𝑇) → (((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎) ↔ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)))
198		simpllr 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
199	170	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℝ)
200	8	ad4antr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℝ)
201	199, 200	readdcld 11269	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ ℝ)
202		eldifsni 4771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ≠ 𝑥)
203	202	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ≠ 𝑥)
204	185, 186, 187, 203	addneintr2d 11448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
205	204	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
206		nelsn 4647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
207	205, 206	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
208	201, 207	eldifd 3942	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
209	197, 198, 208	rspcdva 3607	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
210		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
211		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑐 + 𝑇)))
212	211	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
213		oveq1 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝑦 − (𝑥 + 𝑇)) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
214	212, 213	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑐 + 𝑇) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
215	214	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ 𝑦 = (𝑐 + 𝑇)) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
216	169, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℝ)
217	171, 216	readdcld 11269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ ℝ)
218	204, 206	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
219	217, 218	eldifd 3942	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
220		ovexd 7445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) ∈ V)
221	210, 215, 219, 220	fvmptd 6998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
222	221	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
223	222	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
224	223	fvoveq1d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)))
225	204	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
226	170	recnd 11268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℂ)
227	226	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℂ)
228	186	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑥 ∈ ℂ)
229	187	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℂ)
230	227, 228, 229	pnpcan2d 11637	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
231	230	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) = (abs‘(𝑐 − 𝑥)))
232		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(𝑐 − 𝑥)) < 𝑏)
233	231, 232	eqbrtrd 5146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)
234	225, 233	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
235	234	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
236		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
237	235, 236	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)
238	224, 237	eqbrtrd 5146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
239	238	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
240	239	adantllr 719	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
241	209, 240	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
242	192, 241	eqbrtrd 5146	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
243	242	adantrl 716	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
244	168, 243	eqbrtrd 5146	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)
245	244	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
246	245	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
247	157, 246	impbida 800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
248	247	rexbidv 3165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
249	248	ralbidv 3164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
250	249	anbi2d 630	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
251	38, 36, 7	dvlem 25854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
252	251	fmpttd 7110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))):(ℝ ∖ {𝑥})⟶ℂ)
253	36	ssdifssd 4127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {𝑥}) ⊆ ℂ)
254	252, 253, 78	ellimc3 25837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))))
255	38, 36, 10	dvlem 25854	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) ∈ ℂ)
256	255	fmpttd 7110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))):(ℝ ∖ {(𝑥 + 𝑇)})⟶ℂ)
257	36	ssdifssd 4127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {(𝑥 + 𝑇)}) ⊆ ℂ)
258	10	recnd 11268	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℂ)
259	256, 257, 258	ellimc3 25837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
260	250, 254, 259	3bitr4d 311	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ 𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))))
261	260	eqrdv 2734	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
262		fveq2 6881	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
263	262	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))))
264		oveq1 7417	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 − (𝑥 + 𝑇)) = (𝑧 − (𝑥 + 𝑇)))
265	263, 264	oveq12d 7428	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
266	265	cbvmptv 5230	. . . . . . 7 ⊢ (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
267	266	oveq1i 7420	. . . . . 6 ⊢ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))
268	261, 267	eqtrdi 2787	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
269	41, 268	eleqtrd 2837	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
270		eqid 2736	. . . . . 6 ⊢ (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
271	35	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
272		ssidd 3987	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
273	32, 33, 270, 271, 37, 272	eldv 25856	. . . . 5 ⊢ (𝜑 → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
274	273	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
275	19, 269, 274	mpbir2and 713	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥))
276	3	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐺 = (ℝ D 𝐹))
277	276	breqd 5135	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥)))
278	275, 277	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)𝐺(𝐺‘𝑥))
279	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = (ℝ D 𝐹))
280	279	funeqd 6563	. . . . 5 ⊢ (𝜑 → (Fun 𝐺 ↔ Fun (ℝ D 𝐹)))
281	27, 280	mpbird 257	. . . 4 ⊢ (𝜑 → Fun 𝐺)
282	281	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → Fun 𝐺)
283		funbrfv2b 6941	. . 3 ⊢ (Fun 𝐺 → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))))
284	282, 283	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))))
285	278, 284	mpbid 232	1 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 Vcvv 3464 ∖ cdif 3928 ⊆ wss 3931 {csn 4606 class class class wbr 5124 ↦ cmpt 5206 dom cdm 5659 ran crn 5660 Fun wfun 6530 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 + caddc 11137 < clt 11274 − cmin 11471 / cdiv 11899 ℝ⁺crp 13013 (,)cioo 13367 abscabs 15258 TopOpenctopn 17440 topGenctg 17456 ℂ_fldccnfld 21320 Topctop 22836 intcnt 22960 lim_ℂ climc 25820 D cdv 25821

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-map 8847 df-pm 8848 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9428 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-icc 13374 df-fz 13530 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-struct 17171 df-slot 17206 df-ndx 17218 df-base 17234 df-plusg 17289 df-mulr 17290 df-starv 17291 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-rest 17441 df-topn 17442 df-topgen 17462 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-fbas 21317 df-fg 21318 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-lp 23079 df-perf 23080 df-cnp 23171 df-haus 23258 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-xms 24264 df-ms 24265 df-limc 25824 df-dv 25825

This theorem is referenced by: fourierdlem94 46196 fourierdlem97 46199 fourierdlem113 46215

W3C validator