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 46873

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 26202	. . . . . . . 8 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
2		id 23	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom 𝐺)
3		fperdvper.g	. . . . . . . . . 10 ⊢ 𝐺 = (ℝ D 𝐹)
4	3	dmeqi 5886	. . . . . . . . 9 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
5	2, 4	eleqtrdi 2871	. . . . . . . 8 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom (ℝ D 𝐹))
6	1, 5	sselid 3929	. . . . . . 7 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ ℝ)
7	6	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
8		fperdvper.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑇 ∈ ℝ)
10	7, 9	readdcld 11319	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
11		reopn 46248	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		retop 25060	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Top
13		ssidd 3954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℝ)
14		uniretop 25061	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	isopn3 23364	. . . . . . . 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 2767	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ = ((int‘(topGen‘ran (,)))‘ℝ))
19	10, 18	eleqtrd 2863	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ))
20	5	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom (ℝ D 𝐹))
21	3	fveq1i 6878	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) = ((ℝ D 𝐹)‘𝑥)
22	21	eqcomi 2770	. . . . . . . . 9 ⊢ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥)
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))
24		dvf 26207	. . . . . . . . . . . 12 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
25		ffun 6704	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (ℝ D 𝐹)
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (ℝ D 𝐹))
28		funbrfv2b 6934	. . . . . . . . . 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 25104	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
33		eqid 2761	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
34		eqid 2761	. . . . . . . 8 ⊢ (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))
35		ax-resscn 11238	. . . . . . . . 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 26198	. . . . . . 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 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
43		fveq2 6877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑑 → (𝐹‘𝑦) = (𝐹‘𝑑))
44	43	oveq1d 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))))
45		oveq1 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 − (𝑥 + 𝑇)) = (𝑑 − (𝑥 + 𝑇)))
46	44, 45	oveq12d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))))
47		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℝ)
48	47	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℂ)
49	48	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
50	8	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
51	50	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
52	49, 51	npcand 11654	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) + 𝑇) = 𝑑)
53	52	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 = ((𝑑 − 𝑇) + 𝑇))
54	53	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
55		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 − 𝑇) ∈ V
56	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
57	8	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
58	56, 57	resubcld 11725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
59	58	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → (𝑑 − 𝑇) ∈ ℝ))
60	59	imdistani 579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ))
61		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝑥 ∈ ℝ ↔ (𝑑 − 𝑇) ∈ ℝ))
62	61	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ)))
63		fvoveq1 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
64		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑑 − 𝑇)))
65	63, 64	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
66	62, 65	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑑 − 𝑇) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))))
67		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
68	66, 67	vtoclg 3518	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑 − 𝑇) ∈ V → ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
69	55, 60, 68	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))
70	54, 69	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
76	48	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
77	72, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
78	7	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℂ)
79	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℂ)
80	76, 77, 79	subsub4d 11681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑇 + 𝑥)))
81	77, 79	addcomd 11493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑇 + 𝑥) = (𝑥 + 𝑇))
82	81	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑇 + 𝑥)) = (𝑑 − (𝑥 + 𝑇)))
83	80, 82	eqtr2d 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑥 + 𝑇)) = ((𝑑 − 𝑇) − 𝑥))
84	75, 83	oveq12d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
85	46, 84	sylan9eqr 2818	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = 𝑑) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
86		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
87	37	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝐹:ℝ⟶ℂ)
88	87, 58	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
89	88	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
90	38, 7	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐹‘𝑥) ∈ ℂ)
91	90	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑥) ∈ ℂ)
92	89, 91	subcld 11650	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) ∈ ℂ)
93	76, 77	subcld 11650	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℂ)
94	93, 79	subcld 11650	. . . . . . . . . . . . . . . . . . 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 11669	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ((𝑑 − 𝑇) = 𝑥 ↔ (𝑥 + 𝑇) = 𝑑))
100	95, 99	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑥 + 𝑇) = 𝑑)
101	100	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 = (𝑥 + 𝑇))
102		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ≠ (𝑥 + 𝑇))
103	102	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ≠ (𝑥 + 𝑇))
104	103	neneqd 2961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ¬ 𝑑 = (𝑥 + 𝑇))
105	101, 104	pm2.65da 829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) = 𝑥)
106	105	neqned 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ≠ 𝑥)
107	93, 79, 106	subne0d 11660	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ≠ 0)
108	92, 94, 107	divcld 12074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) ∈ ℂ)
109	42, 85, 86, 108	fvmptd 6993	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
110	109	fvoveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
111	110	ad4ant13 764	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
112		neeq1 3018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → (𝑐 ≠ 𝑥 ↔ (𝑑 − 𝑇) ≠ 𝑥))
113		fvoveq1 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑑 − 𝑇) → (abs‘(𝑐 − 𝑥)) = (abs‘((𝑑 − 𝑇) − 𝑥)))
114	113	breq1d 5113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → ((abs‘(𝑐 − 𝑥)) < 𝑏 ↔ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
115	112, 114	anbi12d 644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑑 − 𝑇) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ↔ ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)))
116	115	imbrov2fvoveq 7437	. . . . . . . . . . . . . . . . . 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 11725	. . . . . . . . . . . . . . . . . . 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 3910	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
125	116, 117, 124	rspcdva 3578	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
126		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
127		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → 𝑦 = (𝑑 − 𝑇))
128	127	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝐹‘𝑦) = (𝐹‘(𝑑 − 𝑇)))
129	128	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
130	127	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝑦 − 𝑥) = ((𝑑 − 𝑇) − 𝑥))
131	129, 130	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
132	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
133	72, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
134	132, 133	resubcld 11725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
135	134, 122	eldifd 3910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
136	126, 131, 135, 108	fvmptd 6993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
137	136	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
138	137	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
139	138	fvoveq1d 7434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)))
140	106	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ≠ 𝑥)
141	83	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
142	141	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
143	142	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) = (abs‘(𝑑 − (𝑥 + 𝑇))))
144		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)
145	143, 144	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)
156	155	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
157	156	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
158		eqidd 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
159		fveq2 6877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
160	159	oveq1d 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑐) − (𝐹‘𝑥)))
161		oveq1 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 − 𝑥) = (𝑐 − 𝑥))
162	160, 161	oveq12d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
163	162	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ (ℝ ∖ {𝑥}) ∧ 𝑦 = 𝑐) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
164		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ (ℝ ∖ {𝑥}))
165		ovexd 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) ∈ V)
166	158, 163, 164, 165	fvmptd 6993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
167	166	fvoveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
168	167	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
169		simpll 779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝜑)
170		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℝ)
171	170	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℝ)
172		eleq1 2849	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ ℝ ↔ 𝑐 ∈ ℝ))
173	172	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑐 ∈ ℝ)))
174		fvoveq1 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑐 + 𝑇)))
175		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
176	174, 175	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐)))
177	173, 176	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑐 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))))
178	177, 67	chvarvv 2022	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))
179	178	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑥) = (𝐹‘(𝑥 + 𝑇)))
184	180, 183	oveq12d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝐹‘𝑐) − (𝐹‘𝑥)) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
185	171	recnd 11318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℂ)
186	78	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℂ)
187	169, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℂ)
188	185, 186, 187	pnpcan2d 11688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
189	188	eqcomd 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 − 𝑥) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
190	184, 189	oveq12d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
191	190	fvoveq1d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
192	191	ad4ant13 764	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
193		neeq1 3018	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → (𝑑 ≠ (𝑥 + 𝑇) ↔ (𝑐 + 𝑇) ≠ (𝑥 + 𝑇)))
194		fvoveq1 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑐 + 𝑇) → (abs‘(𝑑 − (𝑥 + 𝑇))) = (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))))
195	194	breq1d 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → ((abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏 ↔ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
196	193, 195	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑐 + 𝑇) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ↔ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)))
197	196	imbrov2fvoveq 7437	. . . . . . . . . . . . . . . . . . 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 11319	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ ℝ)
202		eldifsni 4753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ≠ 𝑥)
203	202	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ≠ 𝑥)
204	185, 186, 187, 203	addneintr2d 11499	. . . . . . . . . . . . . . . . . . . . . 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 3910	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
209	197, 198, 208	rspcdva 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
210		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
211		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑐 + 𝑇)))
212	211	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
213		oveq1 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝑦 − (𝑥 + 𝑇)) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
214	212, 213	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑐 + 𝑇) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
215	214	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ 𝑦 = (𝑐 + 𝑇)) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
216	169, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℝ)
217	171, 216	readdcld 11319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ ℝ)
218	204, 206	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
219	217, 218	eldifd 3910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
220		ovexd 7447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) ∈ V)
221	210, 215, 219, 220	fvmptd 6993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
222	221	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
223	222	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
224	223	fvoveq1d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)))
225	204	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
226	170	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
231	230	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) = (abs‘(𝑐 − 𝑥)))
232		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(𝑐 − 𝑥)) < 𝑏)
233	231, 232	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . . . . . . . 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 5127	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
243	242	adantrl 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
244	168, 243	eqbrtrd 5127	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)
245	244	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
246	245	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
247	157, 246	impbida 813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
248	247	rexbidv 3187	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
249	248	ralbidv 3186	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
250	249	anbi2d 642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
251	38, 36, 7	dvlem 26196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
252	251	fmpttd 7107	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))):(ℝ ∖ {𝑥})⟶ℂ)
253	36	ssdifssd 4094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {𝑥}) ⊆ ℂ)
254	252, 253, 78	ellimc3 26179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))))
255	38, 36, 10	dvlem 26196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) ∈ ℂ)
256	255	fmpttd 7107	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))):(ℝ ∖ {(𝑥 + 𝑇)})⟶ℂ)
257	36	ssdifssd 4094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {(𝑥 + 𝑇)}) ⊆ ℂ)
258	10	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℂ)
259	256, 257, 258	ellimc3 26179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
260	250, 254, 259	3bitr4d 314	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ 𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))))
261	260	eqrdv 2759	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
262		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
263	262	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))))
264		oveq1 7419	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 − (𝑥 + 𝑇)) = (𝑧 − (𝑥 + 𝑇)))
265	263, 264	oveq12d 7430	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
266	265	cbvmptv 5209	. . . . . . 7 ⊢ (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
267	266	oveq1i 7422	. . . . . 6 ⊢ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))
268	261, 267	eqtrdi 2812	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
269	41, 268	eleqtrd 2863	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
270		eqid 2761	. . . . . 6 ⊢ (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
271	35	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
272		ssidd 3954	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
273	32, 33, 270, 271, 37, 272	eldv 26198	. . . . 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 5114	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥)))
278	275, 277	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)𝐺(𝐺‘𝑥))
279	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = (ℝ D 𝐹))
280	279	funeqd 6553	. . . . 5 ⊢ (𝜑 → (Fun 𝐺 ↔ Fun (ℝ D 𝐹)))
281	27, 280	mpbird 260	. . . 4 ⊢ (𝜑 → Fun 𝐺)
282	281	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → Fun 𝐺)
283		funbrfv2b 6934	. . 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 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∖ cdif 3896 ⊆ wss 3899 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ran crn 5652 Fun wfun 6525 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 ℝcr 11180 + caddc 11184 < clt 11324 − cmin 11522 / cdiv 11954 ℝ⁺crp 13101 (,)cioo 13457 abscabs 15381 TopOpenctopn 17572 topGenctg 17588 ℂ_fldccnfld 21658 Topctop 23191 intcnt 23315 lim_ℂ climc 26162 D cdv 26163

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-map 8833 df-pm 8834 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-z 12675 df-dec 12796 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-icc 13464 df-fz 13621 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-struct 17305 df-slot 17340 df-ndx 17352 df-base 17368 df-plusg 17421 df-mulr 17422 df-starv 17423 df-tset 17427 df-ple 17428 df-ds 17430 df-unif 17431 df-rest 17573 df-topn 17574 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-fbas 21655 df-fg 21656 df-cnfld 21659 df-top 23192 df-topon 23209 df-topsp 23231 df-bases 23244 df-cld 23317 df-ntr 23318 df-cls 23319 df-nei 23396 df-lp 23434 df-perf 23435 df-cnp 23526 df-haus 23613 df-fil 24145 df-fm 24237 df-flim 24238 df-flf 24239 df-xms 24619 df-ms 24620 df-limc 26166 df-dv 26167

This theorem is used by: fourierdlem94 47154 fourierdlem97 47157 fourierdlem113 47173

W3C validator