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 47134

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 26252	. . . . . . . 8 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
2		id 23	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom 𝐺)
3		fperdvper.g	. . . . . . . . . 10 ⊢ 𝐺 = (ℝ D 𝐹)
4	3	dmeqi 5893	. . . . . . . . 9 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
5	2, 4	eleqtrdi 2874	. . . . . . . 8 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom (ℝ D 𝐹))
6	1, 5	sselid 3911	. . . . . . 7 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ ℝ)
7	6	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
8		fperdvper.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑇 ∈ ℝ)
10	7, 9	readdcld 11365	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
11		reopn 46510	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		retop 25110	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Top
13		ssidd 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℝ)
14		uniretop 25111	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	isopn3 23414	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ℝ ⊆ ℝ) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
16	12, 13, 15	sylancr 599	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
17	11, 16	mpbii 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((int‘(topGen‘ran (,)))‘ℝ) = ℝ)
18	17	eqcomd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ = ((int‘(topGen‘ran (,)))‘ℝ))
19	10, 18	eleqtrd 2866	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ))
20	5	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom (ℝ D 𝐹))
21	3	fveq1i 6909	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) = ((ℝ D 𝐹)‘𝑥)
22	21	eqcomi 2772	. . . . . . . . 9 ⊢ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥)
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))
24		dvf 26257	. . . . . . . . . . . 12 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
25		ffun 6734	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (ℝ D 𝐹)
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (ℝ D 𝐹))
28		funbrfv2b 6965	. . . . . . . . . 10 ⊢ (Fun (ℝ D 𝐹) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
29	27, 28	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
30	29	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
31	20, 23, 30	mpbir2and 726	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥(ℝ D 𝐹)(𝐺‘𝑥))
32		tgioo4 25154	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
33		eqid 2763	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
34		eqid 2763	. . . . . . . 8 ⊢ (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))
35		ax-resscn 11284	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℂ)
37		fperdvper.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
38	37	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐹:ℝ⟶ℂ)
39	32, 33, 34, 36, 38, 13	eldv 26248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))))
40	31, 39	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥)))
41	40	simprd 501	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))
42		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
43		fveq2 6908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑑 → (𝐹‘𝑦) = (𝐹‘𝑑))
44	43	oveq1d 7458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))))
45		oveq1 7450	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 − (𝑥 + 𝑇)) = (𝑑 − (𝑥 + 𝑇)))
46	44, 45	oveq12d 7461	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))))
47		eldifi 4070	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℝ)
48	47	recnd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℂ)
49	48	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
50	8	recnd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
51	50	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
52	49, 51	npcand 11700	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) + 𝑇) = 𝑑)
53	52	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 = ((𝑑 − 𝑇) + 𝑇))
54	53	fveq2d 6912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
55		ovex 7476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 − 𝑇) ∈ V
56	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
57	8	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
58	56, 57	resubcld 11771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
59	58	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → (𝑑 − 𝑇) ∈ ℝ))
60	59	imdistani 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ))
61		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝑥 ∈ ℝ ↔ (𝑑 − 𝑇) ∈ ℝ))
62	61	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ)))
63		fvoveq1 7466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
64		fveq2 6908	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑑 − 𝑇)))
65	63, 64	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
66	62, 65	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑑 − 𝑇) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))))
67		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
68	66, 67	vtoclg 3521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑 − 𝑇) ∈ V → ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
69	55, 60, 68	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))
70	54, 69	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
71	70	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
72		simpll 779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝜑)
73	6	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℝ)
74	72, 73, 67	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
75	71, 74	oveq12d 7461	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
76	48	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
77	72, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
78	7	recnd 11364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℂ)
79	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℂ)
80	76, 77, 79	subsub4d 11727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑇 + 𝑥)))
81	77, 79	addcomd 11539	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑇 + 𝑥) = (𝑥 + 𝑇))
82	81	oveq2d 7459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑇 + 𝑥)) = (𝑑 − (𝑥 + 𝑇)))
83	80, 82	eqtr2d 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑥 + 𝑇)) = ((𝑑 − 𝑇) − 𝑥))
84	75, 83	oveq12d 7461	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
85	46, 84	sylan9eqr 2820	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = 𝑑) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
86		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
87	37	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝐹:ℝ⟶ℂ)
88	87, 58	ffvelcdmd 7109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
89	88	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
90	38, 7	ffvelcdmd 7109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐹‘𝑥) ∈ ℂ)
91	90	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑥) ∈ ℂ)
92	89, 91	subcld 11696	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) ∈ ℂ)
93	76, 77	subcld 11696	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℂ)
94	93, 79	subcld 11696	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ∈ ℂ)
95		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑑 − 𝑇) = 𝑥)
96	48	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ∈ ℂ)
97	77	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑇 ∈ ℂ)
98	79	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑥 ∈ ℂ)
99	96, 97, 98	subadd2d 11715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ((𝑑 − 𝑇) = 𝑥 ↔ (𝑥 + 𝑇) = 𝑑))
100	95, 99	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑥 + 𝑇) = 𝑑)
101	100	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 = (𝑥 + 𝑇))
102		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ≠ (𝑥 + 𝑇))
103	102	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ≠ (𝑥 + 𝑇))
104	103	neneqd 2964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ¬ 𝑑 = (𝑥 + 𝑇))
105	101, 104	pm2.65da 829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) = 𝑥)
106	105	neqned 2966	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ≠ 𝑥)
107	93, 79, 106	subne0d 11706	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ≠ 0)
108	92, 94, 107	divcld 12120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) ∈ ℂ)
109	42, 85, 86, 108	fvmptd 7024	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
110	109	fvoveq1d 7465	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
111	110	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
112		neeq1 3021	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → (𝑐 ≠ 𝑥 ↔ (𝑑 − 𝑇) ≠ 𝑥))
113		fvoveq1 7466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑑 − 𝑇) → (abs‘(𝑐 − 𝑥)) = (abs‘((𝑑 − 𝑇) − 𝑥)))
114	113	breq1d 5116	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → ((abs‘(𝑐 − 𝑥)) < 𝑏 ↔ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
115	112, 114	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑑 − 𝑇) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ↔ ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)))
116	115	imbrov2fvoveq 7468	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑑 − 𝑇) → (((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)))
117		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
118	47	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑑 ∈ ℝ)
119	8	ad4antr 745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑇 ∈ ℝ)
120	118, 119	resubcld 11771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ ℝ)
121		elsni 4601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 − 𝑇) ∈ {𝑥} → (𝑑 − 𝑇) = 𝑥)
122	105, 121	nsyl 141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
123	122	ad4ant13 764	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
124	120, 123	eldifd 4053	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
125	116, 117, 124	rspcdva 3581	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
126		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
127		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → 𝑦 = (𝑑 − 𝑇))
128	127	fveq2d 6912	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝐹‘𝑦) = (𝐹‘(𝑑 − 𝑇)))
129	128	oveq1d 7458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
130	127	oveq1d 7458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝑦 − 𝑥) = ((𝑑 − 𝑇) − 𝑥))
131	129, 130	oveq12d 7461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
132	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
133	72, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
134	132, 133	resubcld 11771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
135	134, 122	eldifd 4053	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
136	126, 131, 135, 108	fvmptd 7024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
137	136	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
138	137	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
139	138	fvoveq1d 7465	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)))
140	106	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ≠ 𝑥)
141	83	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
142	141	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
143	142	fveq2d 6912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) = (abs‘(𝑑 − (𝑥 + 𝑇))))
144		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)
145	143, 144	eqbrtrd 5130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)
146	140, 145	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
147	146	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
148		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
149	147, 148	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)
150	139, 149	eqbrtrd 5130	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
151	150	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
152	151	adantllr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
153	125, 152	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
154	153	adantrl 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
155	111, 154	eqbrtrd 5130	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)
156	155	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
157	156	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
158		eqidd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
159		fveq2 6908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
160	159	oveq1d 7458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑐) − (𝐹‘𝑥)))
161		oveq1 7450	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 − 𝑥) = (𝑐 − 𝑥))
162	160, 161	oveq12d 7461	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
163	162	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ (ℝ ∖ {𝑥}) ∧ 𝑦 = 𝑐) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
164		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ (ℝ ∖ {𝑥}))
165		ovexd 7478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) ∈ V)
166	158, 163, 164, 165	fvmptd 7024	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
167	166	fvoveq1d 7465	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
168	167	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
169		simpll 779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝜑)
170		eldifi 4070	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℝ)
171	170	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℝ)
172		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ ℝ ↔ 𝑐 ∈ ℝ))
173	172	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑐 ∈ ℝ)))
174		fvoveq1 7466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑐 + 𝑇)))
175		fveq2 6908	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
176	174, 175	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐)))
177	173, 176	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑐 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))))
178	177, 67	chvarvv 2024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))
179	178	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
180	169, 171, 179	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
181	6	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℝ)
182	169, 181, 67	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
183	182	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑥) = (𝐹‘(𝑥 + 𝑇)))
184	180, 183	oveq12d 7461	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝐹‘𝑐) − (𝐹‘𝑥)) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
185	171	recnd 11364	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℂ)
186	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℂ)
187	169, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℂ)
188	185, 186, 187	pnpcan2d 11734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
189	188	eqcomd 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 − 𝑥) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
190	184, 189	oveq12d 7461	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
191	190	fvoveq1d 7465	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
192	191	ad4ant13 764	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
193		neeq1 3021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → (𝑑 ≠ (𝑥 + 𝑇) ↔ (𝑐 + 𝑇) ≠ (𝑥 + 𝑇)))
194		fvoveq1 7466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑐 + 𝑇) → (abs‘(𝑑 − (𝑥 + 𝑇))) = (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))))
195	194	breq1d 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → ((abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏 ↔ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
196	193, 195	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑐 + 𝑇) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ↔ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)))
197	196	imbrov2fvoveq 7468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑐 + 𝑇) → (((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎) ↔ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)))
198		simpllr 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
199	170	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℝ)
200	8	ad4antr 745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℝ)
201	199, 200	readdcld 11365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ ℝ)
202		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ≠ 𝑥)
203	202	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ≠ 𝑥)
204	185, 186, 187, 203	addneintr2d 11545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
205	204	ad4ant13 764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
206		nelsn 4627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
207	205, 206	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
208	201, 207	eldifd 4053	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
209	197, 198, 208	rspcdva 3581	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
210		eqidd 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
211		fveq2 6908	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑐 + 𝑇)))
212	211	oveq1d 7458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
213		oveq1 7450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝑦 − (𝑥 + 𝑇)) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
214	212, 213	oveq12d 7461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑐 + 𝑇) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
215	214	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ 𝑦 = (𝑐 + 𝑇)) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
216	169, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℝ)
217	171, 216	readdcld 11365	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ ℝ)
218	204, 206	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
219	217, 218	eldifd 4053	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
220		ovexd 7478	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) ∈ V)
221	210, 215, 219, 220	fvmptd 7024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
222	221	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
223	222	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
224	223	fvoveq1d 7465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)))
225	204	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
226	170	recnd 11364	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℂ)
227	226	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℂ)
228	186	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑥 ∈ ℂ)
229	187	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℂ)
230	227, 228, 229	pnpcan2d 11734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
231	230	fveq2d 6912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) = (abs‘(𝑐 − 𝑥)))
232		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(𝑐 − 𝑥)) < 𝑏)
233	231, 232	eqbrtrd 5130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)
234	225, 233	jca 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
235	234	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
236		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
237	235, 236	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)
238	224, 237	eqbrtrd 5130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
239	238	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
240	239	adantllr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
241	209, 240	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
242	192, 241	eqbrtrd 5130	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
243	242	adantrl 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
244	168, 243	eqbrtrd 5130	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)
245	244	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
246	245	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
247	157, 246	impbida 813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
248	247	rexbidv 3190	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
249	248	ralbidv 3189	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
250	249	anbi2d 642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
251	38, 36, 7	dvlem 26246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
252	251	fmpttd 7139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))):(ℝ ∖ {𝑥})⟶ℂ)
253	36	ssdifssd 4086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {𝑥}) ⊆ ℂ)
254	252, 253, 78	ellimc3 26229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))))
255	38, 36, 10	dvlem 26246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) ∈ ℂ)
256	255	fmpttd 7139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))):(ℝ ∖ {(𝑥 + 𝑇)})⟶ℂ)
257	36	ssdifssd 4086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {(𝑥 + 𝑇)}) ⊆ ℂ)
258	10	recnd 11364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℂ)
259	256, 257, 258	ellimc3 26229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
260	250, 254, 259	3bitr4d 314	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ 𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))))
261	260	eqrdv 2761	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
262		fveq2 6908	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
263	262	oveq1d 7458	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))))
264		oveq1 7450	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 − (𝑥 + 𝑇)) = (𝑧 − (𝑥 + 𝑇)))
265	263, 264	oveq12d 7461	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
266	265	cbvmptv 5212	. . . . . . 7 ⊢ (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
267	266	oveq1i 7453	. . . . . 6 ⊢ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))
268	261, 267	eqtrdi 2814	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
269	41, 268	eleqtrd 2866	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
270		eqid 2763	. . . . . 6 ⊢ (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
271	35	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
272		ssidd 3936	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
273	32, 33, 270, 271, 37, 272	eldv 26248	. . . . 5 ⊢ (𝜑 → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
274	273	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
275	19, 269, 274	mpbir2and 726	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥))
276	3	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐺 = (ℝ D 𝐹))
277	276	breqd 5117	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥)))
278	275, 277	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)𝐺(𝐺‘𝑥))
279	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = (ℝ D 𝐹))
280	279	funeqd 6581	. . . . 5 ⊢ (𝜑 → (Fun 𝐺 ↔ Fun (ℝ D 𝐹)))
281	27, 280	mpbird 260	. . . 4 ⊢ (𝜑 → Fun 𝐺)
282	281	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → Fun 𝐺)
283		funbrfv2b 6965	. . 3 ⊢ (Fun 𝐺 → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))))
284	282, 283	syl 18	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥))))
285	278, 284	mpbid 235	1 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇) ∈ dom 𝐺 ∧ (𝐺‘(𝑥 + 𝑇)) = (𝐺‘𝑥)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 class class class wbr 5106 ↦ cmpt 5189 dom cdm 5655 ran crn 5656 Fun wfun 6552 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 ℂcc 11225 ℝcr 11226 + caddc 11230 < clt 11370 − cmin 11568 / cdiv 12000 ℝ⁺crp 13147 (,)cioo 13503 abscabs 15430 TopOpenctopn 17621 topGenctg 17637 ℂ_fldccnfld 21708 Topctop 23241 intcnt 23365 lim_ℂ climc 26212 D cdv 26213

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-er 8745 df-map 8877 df-pm 8878 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fi 9430 df-sup 9461 df-inf 9462 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-z 12721 df-dec 12842 df-uz 12993 df-q 13103 df-rp 13148 df-xneg 13268 df-xadd 13269 df-xmul 13270 df-ioo 13507 df-icc 13510 df-fz 13667 df-seq 14172 df-exp 14232 df-cj 15295 df-re 15296 df-im 15297 df-sqrt 15431 df-abs 15432 df-struct 17354 df-slot 17389 df-ndx 17401 df-base 17417 df-plusg 17470 df-mulr 17471 df-starv 17472 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-rest 17622 df-topn 17623 df-topgen 17643 df-psmet 21700 df-xmet 21701 df-met 21702 df-bl 21703 df-mopn 21704 df-fbas 21705 df-fg 21706 df-cnfld 21709 df-top 23242 df-topon 23259 df-topsp 23281 df-bases 23294 df-cld 23367 df-ntr 23368 df-cls 23369 df-nei 23446 df-lp 23484 df-perf 23485 df-cnp 23576 df-haus 23663 df-fil 24195 df-fm 24287 df-flim 24288 df-flf 24289 df-xms 24669 df-ms 24670 df-limc 26216 df-dv 26217

This theorem is used by: fourierdlem94 47415 fourierdlem97 47418 fourierdlem113 47434

W3C validator