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 46562

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 26032	. . . . . . . 8 ⊢ dom (ℝ D 𝐹) ⊆ ℝ
2		id 23	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom 𝐺)
3		fperdvper.g	. . . . . . . . . 10 ⊢ 𝐺 = (ℝ D 𝐹)
4	3	dmeqi 5897	. . . . . . . . 9 ⊢ dom 𝐺 = dom (ℝ D 𝐹)
5	2, 4	eleqtrdi 2879	. . . . . . . 8 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ dom (ℝ D 𝐹))
6	1, 5	sselid 3943	. . . . . . 7 ⊢ (𝑥 ∈ dom 𝐺 → 𝑥 ∈ ℝ)
7	6	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℝ)
8		fperdvper.t	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑇 ∈ ℝ)
10	7, 9	readdcld 11240	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℝ)
11		reopn 45937	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		retop 24889	. . . . . . . 8 ⊢ (topGen‘ran (,)) ∈ Top
13		ssidd 3968	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℝ)
14		uniretop 24890	. . . . . . . . 9 ⊢ ℝ = ∪ (topGen‘ran (,))
15	14	isopn3 23194	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ℝ ⊆ ℝ) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
16	12, 13, 15	sylancr 598	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∈ (topGen‘ran (,)) ↔ ((int‘(topGen‘ran (,)))‘ℝ) = ℝ))
17	11, 16	mpbii 236	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((int‘(topGen‘ran (,)))‘ℝ) = ℝ)
18	17	eqcomd 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ = ((int‘(topGen‘ran (,)))‘ℝ))
19	10, 18	eleqtrd 2871	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ))
20	5	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ dom (ℝ D 𝐹))
21	3	fveq1i 6885	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) = ((ℝ D 𝐹)‘𝑥)
22	21	eqcomi 2778	. . . . . . . . 9 ⊢ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥)
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))
24		dvf 26037	. . . . . . . . . . . 12 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
25		ffun 6711	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
26	24, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (ℝ D 𝐹)
27	26	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → Fun (ℝ D 𝐹))
28		funbrfv2b 6941	. . . . . . . . . 10 ⊢ (Fun (ℝ D 𝐹) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
29	27, 28	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
30	29	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘𝑥) = (𝐺‘𝑥))))
31	20, 23, 30	mpbir2and 725	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥(ℝ D 𝐹)(𝐺‘𝑥))
32		tgioo4 24933	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
33		eqid 2769	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
34		eqid 2769	. . . . . . . 8 ⊢ (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))
35		ax-resscn 11159	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ℝ ⊆ ℂ)
37		fperdvper.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
38	37	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐹:ℝ⟶ℂ)
39	32, 33, 34, 36, 38, 13	eldv 26028	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥(ℝ D 𝐹)(𝐺‘𝑥) ↔ (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))))
40	31, 39	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥)))
41	40	simprd 500	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥))
42		eqidd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
43		fveq2 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑑 → (𝐹‘𝑦) = (𝐹‘𝑑))
44	43	oveq1d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))))
45		oveq1 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 − (𝑥 + 𝑇)) = (𝑑 − (𝑥 + 𝑇)))
46	44, 45	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))))
47		eldifi 4093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℝ)
48	47	recnd 11239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ∈ ℂ)
49	48	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
50	8	recnd 11239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ ℂ)
51	50	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
52	49, 51	npcand 11575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) + 𝑇) = 𝑑)
53	52	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 = ((𝑑 − 𝑇) + 𝑇))
54	53	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
55		ovex 7446	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 − 𝑇) ∈ V
56	47	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
57	8	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
58	56, 57	resubcld 11644	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
59	58	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → (𝑑 − 𝑇) ∈ ℝ))
60	59	imdistani 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ))
61		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝑥 ∈ ℝ ↔ (𝑑 − 𝑇) ∈ ℝ))
62	61	anbi2d 641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ)))
63		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘((𝑑 − 𝑇) + 𝑇)))
64		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑑 − 𝑇) → (𝐹‘𝑥) = (𝐹‘(𝑑 − 𝑇)))
65	63, 64	eqeq12d 2785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑑 − 𝑇) → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
66	62, 65	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝑑 − 𝑇) → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))))
67		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
68	66, 67	vtoclg 3531	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑑 − 𝑇) ∈ V → ((𝜑 ∧ (𝑑 − 𝑇) ∈ ℝ) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇))))
69	55, 60, 68	mpsyl 69	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘((𝑑 − 𝑇) + 𝑇)) = (𝐹‘(𝑑 − 𝑇)))
70	54, 69	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
71	70	adantlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑑) = (𝐹‘(𝑑 − 𝑇)))
72		simpll 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝜑)
73	6	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℝ)
74	72, 73, 67	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
75	71, 74	oveq12d 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
76	48	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℂ)
77	72, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℂ)
78	7	recnd 11239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝑥 ∈ ℂ)
79	78	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑥 ∈ ℂ)
80	76, 77, 79	subsub4d 11602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑇 + 𝑥)))
81	77, 79	addcomd 11414	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑇 + 𝑥) = (𝑥 + 𝑇))
82	81	oveq2d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑇 + 𝑥)) = (𝑑 − (𝑥 + 𝑇)))
83	80, 82	eqtr2d 2805	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − (𝑥 + 𝑇)) = ((𝑑 − 𝑇) − 𝑥))
84	75, 83	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑑) − (𝐹‘(𝑥 + 𝑇))) / (𝑑 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
85	46, 84	sylan9eqr 2826	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = 𝑑) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
86		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
87	37	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝐹:ℝ⟶ℂ)
88	87, 58	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
89	88	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘(𝑑 − 𝑇)) ∈ ℂ)
90	38, 7	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐹‘𝑥) ∈ ℂ)
91	90	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝐹‘𝑥) ∈ ℂ)
92	89, 91	subcld 11571	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) ∈ ℂ)
93	76, 77	subcld 11571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℂ)
94	93, 79	subcld 11571	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ∈ ℂ)
95		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑑 − 𝑇) = 𝑥)
96	48	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ∈ ℂ)
97	77	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑇 ∈ ℂ)
98	79	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑥 ∈ ℂ)
99	96, 97, 98	subadd2d 11590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ((𝑑 − 𝑇) = 𝑥 ↔ (𝑥 + 𝑇) = 𝑑))
100	95, 99	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → (𝑥 + 𝑇) = 𝑑)
101	100	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 = (𝑥 + 𝑇))
102		eldifsni 4762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) → 𝑑 ≠ (𝑥 + 𝑇))
103	102	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → 𝑑 ≠ (𝑥 + 𝑇))
104	103	neneqd 2969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 − 𝑇) = 𝑥) → ¬ 𝑑 = (𝑥 + 𝑇))
105	101, 104	pm2.65da 828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) = 𝑥)
106	105	neqned 2971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ≠ 𝑥)
107	93, 79, 106	subne0d 11580	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) ≠ 0)
108	92, 94, 107	divcld 11993	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) ∈ ℂ)
109	42, 85, 86, 108	fvmptd 7000	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
110	109	fvoveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
111	110	ad4ant13 763	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) = (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)))
112		neeq1 3026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → (𝑐 ≠ 𝑥 ↔ (𝑑 − 𝑇) ≠ 𝑥))
113		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑑 − 𝑇) → (abs‘(𝑐 − 𝑥)) = (abs‘((𝑑 − 𝑇) − 𝑥)))
114	113	breq1d 5123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑑 − 𝑇) → ((abs‘(𝑐 − 𝑥)) < 𝑏 ↔ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
115	112, 114	anbi12d 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑑 − 𝑇) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ↔ ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)))
116	115	imbrov2fvoveq 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑑 − 𝑇) → (((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)))
117		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
118	47	ad2antlr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑑 ∈ ℝ)
119	8	ad4antr 744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → 𝑇 ∈ ℝ)
120	118, 119	resubcld 11644	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ ℝ)
121		elsni 4611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 − 𝑇) ∈ {𝑥} → (𝑑 − 𝑇) = 𝑥)
122	105, 121	nsyl 141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
123	122	ad4ant13 763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ¬ (𝑑 − 𝑇) ∈ {𝑥})
124	120, 123	eldifd 3924	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
125	116, 117, 124	rspcdva 3591	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
126		eqidd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
127		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → 𝑦 = (𝑑 − 𝑇))
128	127	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝐹‘𝑦) = (𝐹‘(𝑑 − 𝑇)))
129	128	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)))
130	127	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (𝑦 − 𝑥) = ((𝑑 − 𝑇) − 𝑥))
131	129, 130	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ 𝑦 = (𝑑 − 𝑇)) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
132	47	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑑 ∈ ℝ)
133	72, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → 𝑇 ∈ ℝ)
134	132, 133	resubcld 11644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ ℝ)
135	134, 122	eldifd 3924	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (𝑑 − 𝑇) ∈ (ℝ ∖ {𝑥}))
136	126, 131, 135, 108	fvmptd 7000	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) = (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)))
137	136	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
138	137	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) = ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)))
139	138	fvoveq1d 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)))
140	106	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (𝑑 − 𝑇) ≠ 𝑥)
141	83	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
142	141	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) − 𝑥) = (𝑑 − (𝑥 + 𝑇)))
143	142	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) = (abs‘(𝑑 − (𝑥 + 𝑇))))
144		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)
145	143, 144	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏)
146	140, 145	jca 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
147	146	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → ((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏))
148		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎))
149	147, 148	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)
150	139, 149	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ∧ (((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
151	150	ex 417	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
152	151	adantllr 731	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → ((((𝑑 − 𝑇) ≠ 𝑥 ∧ (abs‘((𝑑 − 𝑇) − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘(𝑑 − 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎))
153	125, 152	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
154	153	adantrl 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘((((𝐹‘(𝑑 − 𝑇)) − (𝐹‘𝑥)) / ((𝑑 − 𝑇) − 𝑥)) − 𝑤)) < 𝑎)
155	111, 154	eqbrtrd 5137	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) ∧ (𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)
156	155	ex 417	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ∧ 𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
157	156	ralrimiva 3163	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
158		eqidd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))))
159		fveq2 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐))
160	159	oveq1d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑐) − (𝐹‘𝑥)))
161		oveq1 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 − 𝑥) = (𝑐 − 𝑥))
162	160, 161	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
163	162	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ (ℝ ∖ {𝑥}) ∧ 𝑦 = 𝑐) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
164		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ (ℝ ∖ {𝑥}))
165		ovexd 7448	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) ∈ V)
166	158, 163, 164, 165	fvmptd 7000	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) = (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)))
167	166	fvoveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
168	167	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) = (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)))
169		simpll 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝜑)
170		eldifi 4093	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℝ)
171	170	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℝ)
172		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ ℝ ↔ 𝑐 ∈ ℝ))
173	172	anbi2d 641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑐 ∈ ℝ)))
174		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑐 + 𝑇)))
175		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑐 → (𝐹‘𝑥) = (𝐹‘𝑐))
176	174, 175	eqeq12d 2785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑐 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐)))
177	173, 176	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑐 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))))
178	177, 67	chvarvv 2016	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘(𝑐 + 𝑇)) = (𝐹‘𝑐))
179	178	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ ℝ) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
180	169, 171, 179	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑐) = (𝐹‘(𝑐 + 𝑇)))
181	6	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℝ)
182	169, 181, 67	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
183	182	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝐹‘𝑥) = (𝐹‘(𝑥 + 𝑇)))
184	180, 183	oveq12d 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝐹‘𝑐) − (𝐹‘𝑥)) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
185	171	recnd 11239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ∈ ℂ)
186	78	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑥 ∈ ℂ)
187	169, 50	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℂ)
188	185, 186, 187	pnpcan2d 11609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
189	188	eqcomd 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 − 𝑥) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
190	184, 189	oveq12d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
191	190	fvoveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
192	191	ad4ant13 763	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) = (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)))
193		neeq1 3026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → (𝑑 ≠ (𝑥 + 𝑇) ↔ (𝑐 + 𝑇) ≠ (𝑥 + 𝑇)))
194		fvoveq1 7436	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = (𝑐 + 𝑇) → (abs‘(𝑑 − (𝑥 + 𝑇))) = (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))))
195	194	breq1d 5123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = (𝑐 + 𝑇) → ((abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏 ↔ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
196	193, 195	anbi12d 643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑐 + 𝑇) → ((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) ↔ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)))
197	196	imbrov2fvoveq 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑐 + 𝑇) → (((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎) ↔ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)))
198		simpllr 787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))
199	170	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℝ)
200	8	ad4antr 744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℝ)
201	199, 200	readdcld 11240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ ℝ)
202		eldifsni 4762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ≠ 𝑥)
203	202	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑐 ≠ 𝑥)
204	185, 186, 187, 203	addneintr2d 11420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
205	204	ad4ant13 763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
206		nelsn 4637	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
207	205, 206	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
208	201, 207	eldifd 3924	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
209	197, 198, 208	rspcdva 3591	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
210		eqidd 2770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))))
211		fveq2 6884	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑐 + 𝑇)))
212	211	oveq1d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))))
213		oveq1 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = (𝑐 + 𝑇) → (𝑦 − (𝑥 + 𝑇)) = ((𝑐 + 𝑇) − (𝑥 + 𝑇)))
214	212, 213	oveq12d 7431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = (𝑐 + 𝑇) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
215	214	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ 𝑦 = (𝑐 + 𝑇)) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
216	169, 8	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → 𝑇 ∈ ℝ)
217	171, 216	readdcld 11240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ ℝ)
218	204, 206	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ¬ (𝑐 + 𝑇) ∈ {(𝑥 + 𝑇)})
219	217, 218	eldifd 3924	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (𝑐 + 𝑇) ∈ (ℝ ∖ {(𝑥 + 𝑇)}))
220		ovexd 7448	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) ∈ V)
221	210, 215, 219, 220	fvmptd 7000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) = (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))))
222	221	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
223	222	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)))
224	223	fvoveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) = (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)))
225	204	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (𝑐 + 𝑇) ≠ (𝑥 + 𝑇))
226	170	recnd 11239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ (ℝ ∖ {𝑥}) → 𝑐 ∈ ℂ)
227	226	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑐 ∈ ℂ)
228	186	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑥 ∈ ℂ)
229	187	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → 𝑇 ∈ ℂ)
230	227, 228, 229	pnpcan2d 11609	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) − (𝑥 + 𝑇)) = (𝑐 − 𝑥))
231	230	fveq2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) = (abs‘(𝑐 − 𝑥)))
232		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(𝑐 − 𝑥)) < 𝑏)
233	231, 232	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏)
234	225, 233	jca 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
235	234	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → ((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏))
236		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎))
237	235, 236	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)
238	224, 237	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) ∧ (((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎)) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
239	238	ex 417	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
240	239	adantllr 731	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → ((((𝑐 + 𝑇) ≠ (𝑥 + 𝑇) ∧ (abs‘((𝑐 + 𝑇) − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘(𝑐 + 𝑇)) − 𝑤)) < 𝑎) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎))
241	209, 240	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘(𝑐 + 𝑇)) − (𝐹‘(𝑥 + 𝑇))) / ((𝑐 + 𝑇) − (𝑥 + 𝑇))) − 𝑤)) < 𝑎)
242	192, 241	eqbrtrd 5137	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
243	242	adantrl 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘((((𝐹‘𝑐) − (𝐹‘𝑥)) / (𝑐 − 𝑥)) − 𝑤)) < 𝑎)
244	168, 243	eqbrtrd 5137	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) ∧ (𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏)) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)
245	244	ex 417	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) ∧ 𝑐 ∈ (ℝ ∖ {𝑥})) → ((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
246	245	ralrimiva 3163	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)) → ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))
247	157, 246	impbida 812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
248	247	rexbidv 3195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
249	248	ralbidv 3194	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎) ↔ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎)))
250	249	anbi2d 641	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
251	38, 36, 7	dvlem 26026	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {𝑥})) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ)
252	251	fmpttd 7113	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))):(ℝ ∖ {𝑥})⟶ℂ)
253	36	ssdifssd 4109	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {𝑥}) ⊆ ℂ)
254	252, 253, 78	ellimc3 26009	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ (ℝ ∖ {𝑥})((𝑐 ≠ 𝑥 ∧ (abs‘(𝑐 − 𝑥)) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)))‘𝑐) − 𝑤)) < 𝑎))))
255	38, 36, 10	dvlem 26026	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐺) ∧ 𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)})) → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) ∈ ℂ)
256	255	fmpttd 7113	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))):(ℝ ∖ {(𝑥 + 𝑇)})⟶ℂ)
257	36	ssdifssd 4109	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (ℝ ∖ {(𝑥 + 𝑇)}) ⊆ ℂ)
258	10	recnd 11239	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇) ∈ ℂ)
259	256, 257, 258	ellimc3 26009	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) ↔ (𝑤 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑑 ∈ (ℝ ∖ {(𝑥 + 𝑇)})((𝑑 ≠ (𝑥 + 𝑇) ∧ (abs‘(𝑑 − (𝑥 + 𝑇))) < 𝑏) → (abs‘(((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))))‘𝑑) − 𝑤)) < 𝑎))))
260	250, 254, 259	3bitr4d 314	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) ↔ 𝑤 ∈ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))))
261	260	eqrdv 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
262		fveq2 6884	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
263	262	oveq1d 7428	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) = ((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))))
264		oveq1 7420	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 − (𝑥 + 𝑇)) = (𝑧 − (𝑥 + 𝑇)))
265	263, 264	oveq12d 7431	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇))) = (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
266	265	cbvmptv 5219	. . . . . . 7 ⊢ (𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
267	266	oveq1i 7423	. . . . . 6 ⊢ ((𝑦 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑦) − (𝐹‘(𝑥 + 𝑇))) / (𝑦 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇))
268	261, 267	eqtrdi 2820	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑦 ∈ (ℝ ∖ {𝑥}) ↦ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) lim_ℂ 𝑥) = ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
269	41, 268	eleqtrd 2871	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))
270		eqid 2769	. . . . . 6 ⊢ (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) = (𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇))))
271	35	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
272		ssidd 3968	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
273	32, 33, 270, 271, 37, 272	eldv 26028	. . . . 5 ⊢ (𝜑 → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
274	273	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥) ↔ ((𝑥 + 𝑇) ∈ ((int‘(topGen‘ran (,)))‘ℝ) ∧ (𝐺‘𝑥) ∈ ((𝑧 ∈ (ℝ ∖ {(𝑥 + 𝑇)}) ↦ (((𝐹‘𝑧) − (𝐹‘(𝑥 + 𝑇))) / (𝑧 − (𝑥 + 𝑇)))) lim_ℂ (𝑥 + 𝑇)))))
275	19, 269, 274	mpbir2and 725	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥))
276	3	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → 𝐺 = (ℝ D 𝐹))
277	276	breqd 5124	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → ((𝑥 + 𝑇)𝐺(𝐺‘𝑥) ↔ (𝑥 + 𝑇)(ℝ D 𝐹)(𝐺‘𝑥)))
278	275, 277	mpbird 260	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝑥 + 𝑇)𝐺(𝐺‘𝑥))
279	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐺 = (ℝ D 𝐹))
280	279	funeqd 6561	. . . . 5 ⊢ (𝜑 → (Fun 𝐺 ↔ Fun (ℝ D 𝐹)))
281	27, 280	mpbird 260	. . . 4 ⊢ (𝜑 → Fun 𝐺)
282	281	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → Fun 𝐺)
283		funbrfv2b 6941	. . 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

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∖ cdif 3910 ⊆ wss 3913 {csn 4594 class class class wbr 5113 ↦ cmpt 5196 dom cdm 5664 ran crn 5665 Fun wfun 6533 ⟶wf 6535 ‘cfv 6539 (class class class)co 7413 ℂcc 11100 ℝcr 11101 + caddc 11105 < clt 11245 − cmin 11443 / cdiv 11873 ℝ⁺crp 13018 (,)cioo 13374 abscabs 15287 TopOpenctopn 17476 topGenctg 17492 ℂ_fldccnfld 21493 Topctop 23021 intcnt 23145 lim_ℂ climc 25992 D cdv 25993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5273 ax-pow 5339 ax-pr 5407 ax-un 7735 ax-cnex 11158 ax-resscn 11159 ax-1cn 11160 ax-icn 11161 ax-addcl 11162 ax-addrcl 11163 ax-mulcl 11164 ax-mulrcl 11165 ax-mulcom 11166 ax-addass 11167 ax-mulass 11168 ax-distr 11169 ax-i2m1 11170 ax-1ne0 11171 ax-1rid 11172 ax-rnegex 11173 ax-rrecex 11174 ax-cnre 11175 ax-pre-lttri 11176 ax-pre-lttrn 11177 ax-pre-ltadd 11178 ax-pre-mulgt0 11179 ax-pre-sup 11180

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5559 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-er 8696 df-map 8828 df-pm 8829 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fi 9373 df-sup 9404 df-inf 9405 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11445 df-neg 11446 df-div 11874 df-nn 12236 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12865 df-q 12975 df-rp 13019 df-xneg 13139 df-xadd 13140 df-xmul 13141 df-ioo 13378 df-icc 13381 df-fz 13538 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-struct 17209 df-slot 17244 df-ndx 17256 df-base 17272 df-plusg 17325 df-mulr 17326 df-starv 17327 df-tset 17331 df-ple 17332 df-ds 17334 df-unif 17335 df-rest 17477 df-topn 17478 df-topgen 17498 df-psmet 21485 df-xmet 21486 df-met 21487 df-bl 21488 df-mopn 21489 df-fbas 21490 df-fg 21491 df-cnfld 21494 df-top 23022 df-topon 23039 df-topsp 23061 df-bases 23074 df-cld 23147 df-ntr 23148 df-cls 23149 df-nei 23226 df-lp 23264 df-perf 23265 df-cnp 23356 df-haus 23443 df-fil 23974 df-fm 24066 df-flim 24067 df-flf 24068 df-xms 24448 df-ms 24449 df-limc 25996 df-dv 25997

This theorem is referenced by: fourierdlem94 46843 fourierdlem97 46846 fourierdlem113 46862

W3C validator