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 46159

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 25859	. . . . . . . 8 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
2		id 22	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom 𝐺)
3		fperdvper.g	. . . . . . . . . 10 ⊢ 𝐺 = (ℝ D 𝐹)
4	3	dmeqi 5853	. . . . . . . . 9 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
5	2, 4	eleqtrdi 2846	. . . . . . . 8 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom (ℝ D 𝐹))
6	1, 5	sselid 3931	. . . . . . 7 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ ℝ)
7	6	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
8		fperdvper.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑇 ∈ ℝ)
10	7, 9	readdcld 11161	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
11		reopn 45533	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		retop 24705	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Top
13		ssidd 3957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℝ)
14		uniretop 24706	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	isopn3 23010	. . . . . . . 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 2838	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ))
20	5	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom (ℝ D 𝐹))
21	3	fveq1i 6835	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) = ((ℝ D 𝐹)‘𝑥)
22	21	eqcomi 2745	. . . . . . . . 9 ⊢ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥)
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))
24		dvf 25864	. . . . . . . . . . . 12 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
25		ffun 6665	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (ℝ D 𝐹)
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (ℝ D 𝐹))
28		funbrfv2b 6891	. . . . . . . . . 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 11083	. . . . . . . . 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 25855	. . . . . . 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 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑑 → (𝐹‘𝑦) = (𝐹‘𝑑))
44	43	oveq1d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))))
45		oveq1 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 − (𝑥 + 𝑇)) = (𝑑 − (𝑥 + 𝑇)))
46	44, 45	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))))
47		eldifi 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℝ)
48	47	recnd 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℂ)
49	48	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
50	8	recnd 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
51	50	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
52	49, 51	npcand 11496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) + 𝑇) = 𝑑)
53	52	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 = ((𝑑 − 𝑇) + 𝑇))
54	53	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
55		ovex 7391	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 − 𝑇) ∈ V
56	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
57	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
58	56, 57	resubcld 11565	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
59	58	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → (𝑑 − 𝑇) ∈ ℝ))
60	59	imdistani 568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ))
61		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝑥 ∈ ℝ ↔ (𝑑 − 𝑇) ∈ ℝ))
62	61	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ)))
63		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
64		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑑 − 𝑇)))
65	63, 64	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
66	62, 65	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑑 − 𝑇) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))))
67		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
68	66, 67	vtoclg 3511	. . . . . . . . . . . . . . . . . . . . . . . 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 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
76	48	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
77	72, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
78	7	recnd 11160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℂ)
79	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℂ)
80	76, 77, 79	subsub4d 11523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑇 + 𝑥)))
81	77, 79	addcomd 11335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑇 + 𝑥) = (𝑥 + 𝑇))
82	81	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑇 + 𝑥)) = (𝑑 − (𝑥 + 𝑇)))
83	80, 82	eqtr2d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑥 + 𝑇)) = ((𝑑 − 𝑇) − 𝑥))
84	75, 83	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
85	46, 84	sylan9eqr 2793	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = 𝑑) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
86		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
87	37	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝐹:ℝ⟶ℂ)
88	87, 58	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
89	88	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
90	38, 7	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐹‘𝑥) ∈ ℂ)
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑥) ∈ ℂ)
92	89, 91	subcld 11492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) ∈ ℂ)
93	76, 77	subcld 11492	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℂ)
94	93, 79	subcld 11492	. . . . . . . . . . . . . . . . . . 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 11511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ((𝑑 − 𝑇) = 𝑥 ↔ (𝑥 + 𝑇) = 𝑑))
100	95, 99	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑥 + 𝑇) = 𝑑)
101	100	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 = (𝑥 + 𝑇))
102		eldifsni 4746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ≠ (𝑥 + 𝑇))
103	102	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ≠ (𝑥 + 𝑇))
104	103	neneqd 2937	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ¬ 𝑑 = (𝑥 + 𝑇))
105	101, 104	pm2.65da 816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) = 𝑥)
106	105	neqned 2939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ≠ 𝑥)
107	93, 79, 106	subne0d 11501	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ≠ 0)
108	92, 94, 107	divcld 11917	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) ∈ ℂ)
109	42, 85, 86, 108	fvmptd 6948	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
110	109	fvoveq1d 7380	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
111	110	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
112		neeq1 2994	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → (𝑐 ≠ 𝑥 ↔ (𝑑 − 𝑇) ≠ 𝑥))
113		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑑 − 𝑇) → (abs‘(𝑐 − 𝑥)) = (abs‘((𝑑 − 𝑇) − 𝑥)))
114	113	breq1d 5108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → ((abs‘(𝑐 − 𝑥)) < 𝑏 ↔ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
115	112, 114	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑑 − 𝑇) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ↔ ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)))
116	115	imbrov2fvoveq 7383	. . . . . . . . . . . . . . . . . 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 11565	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ ℝ)
121		elsni 4597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 − 𝑇) ∈ {𝑥} → (𝑑 − 𝑇) = 𝑥)
122	105, 121	nsyl 140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
123	122	ad4ant13 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
124	120, 123	eldifd 3912	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
125	116, 117, 124	rspcdva 3577	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
126		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
127		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → 𝑦 = (𝑑 − 𝑇))
128	127	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝐹‘𝑦) = (𝐹‘(𝑑 − 𝑇)))
129	128	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
130	127	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝑦 − 𝑥) = ((𝑑 − 𝑇) − 𝑥))
131	129, 130	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
132	47	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
133	72, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
134	132, 133	resubcld 11565	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
135	134, 122	eldifd 3912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
136	126, 131, 135, 108	fvmptd 6948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
137	136	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
138	137	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
139	138	fvoveq1d 7380	. . . . . . . . . . . . . . . . . . . 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 6838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) = (abs‘(𝑑 − (𝑥 + 𝑇))))
144		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)
145	143, 144	eqbrtrd 5120	. . . . . . . . . . . . . . . . . . . . . . 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 5120	. . . . . . . . . . . . . . . . . . 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 5120	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)
156	155	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
157	156	ralrimiva 3128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
158		eqidd 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
159		fveq2 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
160	159	oveq1d 7373	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑐) − (𝐹‘𝑥)))
161		oveq1 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 − 𝑥) = (𝑐 − 𝑥))
162	160, 161	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
163	162	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ (ℝ ∖ {𝑥}) ∧ 𝑦 = 𝑐) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
164		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ (ℝ ∖ {𝑥}))
165		ovexd 7393	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) ∈ V)
166	158, 163, 164, 165	fvmptd 6948	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
167	166	fvoveq1d 7380	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
168	167	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
169		simpll 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝜑)
170		eldifi 4083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℝ)
171	170	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℝ)
172		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ ℝ ↔ 𝑐 ∈ ℝ))
173	172	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑐 ∈ ℝ)))
174		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑐 + 𝑇)))
175		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
176	174, 175	eqeq12d 2752	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐)))
177	173, 176	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑐 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))))
178	177, 67	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . . . 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 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝐹‘𝑐) − (𝐹‘𝑥)) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
185	171	recnd 11160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℂ)
186	78	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℂ)
187	169, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℂ)
188	185, 186, 187	pnpcan2d 11530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
189	188	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 − 𝑥) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
190	184, 189	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
191	190	fvoveq1d 7380	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
192	191	ad4ant13 751	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
193		neeq1 2994	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → (𝑑 ≠ (𝑥 + 𝑇) ↔ (𝑐 + 𝑇) ≠ (𝑥 + 𝑇)))
194		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑐 + 𝑇) → (abs‘(𝑑 − (𝑥 + 𝑇))) = (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))))
195	194	breq1d 5108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → ((abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏 ↔ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
196	193, 195	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑐 + 𝑇) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ↔ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)))
197	196	imbrov2fvoveq 7383	. . . . . . . . . . . . . . . . . . 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 11161	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ ℝ)
202		eldifsni 4746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ≠ 𝑥)
203	202	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ≠ 𝑥)
204	185, 186, 187, 203	addneintr2d 11341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
205	204	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
206		nelsn 4623	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
207	205, 206	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
208	201, 207	eldifd 3912	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
209	197, 198, 208	rspcdva 3577	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
210		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
211		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑐 + 𝑇)))
212	211	oveq1d 7373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
213		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝑦 − (𝑥 + 𝑇)) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
214	212, 213	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑐 + 𝑇) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
215	214	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ 𝑦 = (𝑐 + 𝑇)) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
216	169, 8	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℝ)
217	171, 216	readdcld 11161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ ℝ)
218	204, 206	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
219	217, 218	eldifd 3912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
220		ovexd 7393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) ∈ V)
221	210, 215, 219, 220	fvmptd 6948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
222	221	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
223	222	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
224	223	fvoveq1d 7380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)))
225	204	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
226	170	recnd 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11530	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
231	230	fveq2d 6838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) = (abs‘(𝑐 − 𝑥)))
232		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(𝑐 − 𝑥)) < 𝑏)
233	231, 232	eqbrtrd 5120	. . . . . . . . . . . . . . . . . . . . . . . 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 5120	. . . . . . . . . . . . . . . . . . . 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 5120	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
243	242	adantrl 716	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
244	168, 243	eqbrtrd 5120	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)
245	244	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
246	245	ralrimiva 3128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
247	157, 246	impbida 800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
248	247	rexbidv 3160	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
249	248	ralbidv 3159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
250	249	anbi2d 630	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
251	38, 36, 7	dvlem 25853	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
252	251	fmpttd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))):(ℝ ∖ {𝑥})⟶ℂ)
253	36	ssdifssd 4099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {𝑥}) ⊆ ℂ)
254	252, 253, 78	ellimc3 25836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))))
255	38, 36, 10	dvlem 25853	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) ∈ ℂ)
256	255	fmpttd 7060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))):(ℝ ∖ {(𝑥 + 𝑇)})⟶ℂ)
257	36	ssdifssd 4099	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {(𝑥 + 𝑇)}) ⊆ ℂ)
258	10	recnd 11160	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℂ)
259	256, 257, 258	ellimc3 25836	. . . . . . . 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 6834	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
263	262	oveq1d 7373	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))))
264		oveq1 7365	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 − (𝑥 + 𝑇)) = (𝑧 − (𝑥 + 𝑇)))
265	263, 264	oveq12d 7376	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
266	265	cbvmptv 5202	. . . . . . 7 ⊢ (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
267	266	oveq1i 7368	. . . . . 6 ⊢ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))
268	261, 267	eqtrdi 2787	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
269	41, 268	eleqtrd 2838	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
270		eqid 2736	. . . . . 6 ⊢ (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
271	35	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
272		ssidd 3957	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
273	32, 33, 270, 271, 37, 272	eldv 25855	. . . . 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 5109	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥)))
278	275, 277	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)𝐺(𝐺‘𝑥))
279	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = (ℝ D 𝐹))
280	279	funeqd 6514	. . . . 5 ⊢ (𝜑 → (Fun 𝐺 ↔ Fun (ℝ D 𝐹)))
281	27, 280	mpbird 257	. . . 4 ⊢ (𝜑 → Fun 𝐺)
282	281	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → Fun 𝐺)
283		funbrfv2b 6891	. . 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 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∖ cdif 3898 ⊆ wss 3901 {csn 4580 class class class wbr 5098 ↦ cmpt 5179 dom cdm 5624 ran crn 5625 Fun wfun 6486 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ℂcc 11024 ℝcr 11025 + caddc 11029 < clt 11166 − cmin 11364 / cdiv 11794 ℝ⁺crp 12905 (,)cioo 13261 abscabs 15157 TopOpenctopn 17341 topGenctg 17357 ℂ_fldccnfld 21309 Topctop 22837 intcnt 22961 lim_ℂ climc 25819 D cdv 25820

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9314 df-sup 9345 df-inf 9346 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-icc 13268 df-fz 13424 df-seq 13925 df-exp 13985 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-struct 17074 df-slot 17109 df-ndx 17121 df-base 17137 df-plusg 17190 df-mulr 17191 df-starv 17192 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-rest 17342 df-topn 17343 df-topgen 17363 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-fbas 21306 df-fg 21307 df-cnfld 21310 df-top 22838 df-topon 22855 df-topsp 22877 df-bases 22890 df-cld 22963 df-ntr 22964 df-cls 22965 df-nei 23042 df-lp 23080 df-perf 23081 df-cnp 23172 df-haus 23259 df-fil 23790 df-fm 23882 df-flim 23883 df-flf 23884 df-xms 24264 df-ms 24265 df-limc 25823 df-dv 25824

This theorem is referenced by: fourierdlem94 46440 fourierdlem97 46443 fourierdlem113 46459

W3C validator