fperdvper

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

	Ref	Expression
Hypotheses	fperdvper.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fperdvper.t	$⊢ φ \to T \in ℝ$
	fperdvper.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fperdvper.g	$⊢ G = ℝ D F$
Assertion	fperdvper	$⊢ (φ \land x \in dom G) \to (x + T \in dom G \land G (x + T) = G (x))$

Proof

Step	Hyp	Ref	Expression
1		fperdvper.f	$⊢ φ \to F : ℝ ⟶ ℂ$
2		fperdvper.t	$⊢ φ \to T \in ℝ$
3		fperdvper.fper	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fperdvper.g	$⊢ G = ℝ D F$
5		dvbsss	$⊢ dom F_{ℝ}^{'} \subseteq ℝ$
6		id	$⊢ x \in dom G \to x \in dom G$
7	4	dmeqi	$⊢ dom G = dom F_{ℝ}^{'}$
8	6 7	eleqtrdi	$⊢ x \in dom G \to x \in dom F_{ℝ}^{'}$
9	5 8	sselid	$⊢ x \in dom G \to x \in ℝ$
10	9	adantl	$⊢ (φ \land x \in dom G) \to x \in ℝ$
11	2	adantr	$⊢ (φ \land x \in dom G) \to T \in ℝ$
12	10 11	readdcld	$⊢ (φ \land x \in dom G) \to x + T \in ℝ$
13		reopn	$⊢ ℝ \in topGen (ran (.))$
14		retop	$⊢ topGen (ran (.)) \in Top$
15		ssidd	$⊢ (φ \land x \in dom G) \to ℝ \subseteq ℝ$
16		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
17	16	isopn3	$⊢ (topGen (ran (.)) \in Top \land ℝ \subseteq ℝ) \to (ℝ \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (ℝ) = ℝ)$
18	14 15 17	sylancr	$⊢ (φ \land x \in dom G) \to (ℝ \in topGen (ran (.)) \leftrightarrow int (topGen (ran (.))) (ℝ) = ℝ)$
19	13 18	mpbii	$⊢ (φ \land x \in dom G) \to int (topGen (ran (.))) (ℝ) = ℝ$
20	19	eqcomd	$⊢ (φ \land x \in dom G) \to ℝ = int (topGen (ran (.))) (ℝ)$
21	12 20	eleqtrd	$⊢ (φ \land x \in dom G) \to x + T \in int (topGen (ran (.))) (ℝ)$
22	8	adantl	$⊢ (φ \land x \in dom G) \to x \in dom F_{ℝ}^{'}$
23	4	fveq1i	$⊢ G (x) = F_{ℝ}^{'} (x)$
24	23	eqcomi	$⊢ F_{ℝ}^{'} (x) = G (x)$
25	24	a1i	$⊢ (φ \land x \in dom G) \to F_{ℝ}^{'} (x) = G (x)$
26		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
27		ffun	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to Fun F_{ℝ}^{'}$
28	26 27	ax-mp	$⊢ Fun F_{ℝ}^{'}$
29	28	a1i	$⊢ φ \to Fun F_{ℝ}^{'}$
30		funbrfv2b	$⊢ Fun F_{ℝ}^{'} \to (x F_{ℝ}^{'} G (x) \leftrightarrow (x \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (x) = G (x)))$
31	29 30	syl	$⊢ φ \to (x F_{ℝ}^{'} G (x) \leftrightarrow (x \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (x) = G (x)))$
32	31	adantr	$⊢ (φ \land x \in dom G) \to (x F_{ℝ}^{'} G (x) \leftrightarrow (x \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (x) = G (x)))$
33	22 25 32	mpbir2and	$⊢ (φ \land x \in dom G) \to x F_{ℝ}^{'} G (x)$
34		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
35		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
36		eqid	$⊢ (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) = (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x})$
37		ax-resscn	$⊢ ℝ \subseteq ℂ$
38	37	a1i	$⊢ (φ \land x \in dom G) \to ℝ \subseteq ℂ$
39	1	adantr	$⊢ (φ \land x \in dom G) \to F : ℝ ⟶ ℂ$
40	34 35 36 38 39 15	eldv	$⊢ (φ \land x \in dom G) \to (x F_{ℝ}^{'} G (x) \leftrightarrow (x \in int (topGen (ran (.))) (ℝ) \land G (x) \in ((y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x)))$
41	33 40	mpbid	$⊢ (φ \land x \in dom G) \to (x \in int (topGen (ran (.))) (ℝ) \land G (x) \in ((y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x))$
42	41	simprd	$⊢ (φ \land x \in dom G) \to G (x) \in ((y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x)$
43		eqidd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) = (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)})$
44		fveq2	$⊢ y = d \to F (y) = F (d)$
45	44	oveq1d	$⊢ y = d \to F (y) - F (x + T) = F (d) - F (x + T)$
46		oveq1	$⊢ y = d \to y - (x + T) = d - (x + T)$
47	45 46	oveq12d	$⊢ y = d \to \frac{F (y) - F (x + T)}{y - (x + T)} = \frac{F (d) - F (x + T)}{d - (x + T)}$
48		eldifi	$⊢ d \in (ℝ ∖ \{x + T\}) \to d \in ℝ$
49	48	recnd	$⊢ d \in (ℝ ∖ \{x + T\}) \to d \in ℂ$
50	49	adantl	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to d \in ℂ$
51	2	recnd	$⊢ φ \to T \in ℂ$
52	51	adantr	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to T \in ℂ$
53	50 52	npcand	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to d - T + T = d$
54	53	eqcomd	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to d = d - T + T$
55	54	fveq2d	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to F (d) = F (d - T + T)$
56		ovex	$⊢ d - T \in V$
57	48	adantl	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to d \in ℝ$
58	2	adantr	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to T \in ℝ$
59	57 58	resubcld	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to d - T \in ℝ$
60	59	ex	$⊢ φ \to (d \in (ℝ ∖ \{x + T\}) \to d - T \in ℝ)$
61	60	imdistani	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to (φ \land d - T \in ℝ)$
62		eleq1	$⊢ x = d - T \to (x \in ℝ \leftrightarrow d - T \in ℝ)$
63	62	anbi2d	$⊢ x = d - T \to ((φ \land x \in ℝ) \leftrightarrow (φ \land d - T \in ℝ))$
64		fvoveq1	$⊢ x = d - T \to F (x + T) = F (d - T + T)$
65		fveq2	$⊢ x = d - T \to F (x) = F (d - T)$
66	64 65	eqeq12d	$⊢ x = d - T \to (F (x + T) = F (x) \leftrightarrow F (d - T + T) = F (d - T))$
67	63 66	imbi12d	$⊢ x = d - T \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land d - T \in ℝ) \to F (d - T + T) = F (d - T)))$
68	67 3	vtoclg	$⊢ d - T \in V \to ((φ \land d - T \in ℝ) \to F (d - T + T) = F (d - T))$
69	56 61 68	mpsyl	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to F (d - T + T) = F (d - T)$
70	55 69	eqtrd	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to F (d) = F (d - T)$
71	70	adantlr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (d) = F (d - T)$
72		simpll	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to φ$
73	9	ad2antlr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to x \in ℝ$
74	72 73 3	syl2anc	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (x + T) = F (x)$
75	71 74	oveq12d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (d) - F (x + T) = F (d - T) - F (x)$
76	49	adantl	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d \in ℂ$
77	72 51	syl	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to T \in ℂ$
78	10	recnd	$⊢ (φ \land x \in dom G) \to x \in ℂ$
79	78	adantr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to x \in ℂ$
80	76 77 79	subsub4d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T - x = d - (T + x)$
81	77 79	addcomd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to T + x = x + T$
82	81	oveq2d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - (T + x) = d - (x + T)$
83	80 82	eqtr2d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - (x + T) = d - T - x$
84	75 83	oveq12d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \frac{F (d) - F (x + T)}{d - (x + T)} = \frac{F (d - T) - F (x)}{d - T - x}$
85	47 84	sylan9eqr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d) \to \frac{F (y) - F (x + T)}{y - (x + T)} = \frac{F (d - T) - F (x)}{d - T - x}$
86		simpr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d \in (ℝ ∖ \{x + T\})$
87	1	adantr	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to F : ℝ ⟶ ℂ$
88	87 59	ffvelcdmd	$⊢ (φ \land d \in (ℝ ∖ \{x + T\})) \to F (d - T) \in ℂ$
89	88	adantlr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (d - T) \in ℂ$
90	39 10	ffvelcdmd	$⊢ (φ \land x \in dom G) \to F (x) \in ℂ$
91	90	adantr	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (x) \in ℂ$
92	89 91	subcld	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to F (d - T) - F (x) \in ℂ$
93	76 77	subcld	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T \in ℂ$
94	93 79	subcld	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T - x \in ℂ$
95		simpr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to d - T = x$
96	49	ad2antlr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to d \in ℂ$
97	77	adantr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to T \in ℂ$
98	79	adantr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to x \in ℂ$
99	96 97 98	subadd2d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to (d - T = x \leftrightarrow x + T = d)$
100	95 99	mpbid	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to x + T = d$
101	100	eqcomd	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to d = x + T$
102		eldifsni	$⊢ d \in (ℝ ∖ \{x + T\}) \to d \neq x + T$
103	102	ad2antlr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to d \neq x + T$
104	103	neneqd	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land d - T = x) \to \neg d = x + T$
105	101 104	pm2.65da	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \neg d - T = x$
106	105	neqned	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T \neq x$
107	93 79 106	subne0d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T - x \neq 0$
108	92 94 107	divcld	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \frac{F (d - T) - F (x)}{d - T - x} \in ℂ$
109	43 85 86 108	fvmptd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) = \frac{F (d - T) - F (x)}{d - T - x}$
110	109	fvoveq1d	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| = \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\|$
111	110	ad4ant13	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land (d \neq x + T \land \|d - (x + T)\| < b)) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| = \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\|$
112		neeq1	$⊢ c = d - T \to (c \neq x \leftrightarrow d - T \neq x)$
113		fvoveq1	$⊢ c = d - T \to \|c - x\| = \|d - T - x\|$
114	113	breq1d	$⊢ c = d - T \to (\|c - x\| < b \leftrightarrow \|d - T - x\| < b)$
115	112 114	anbi12d	$⊢ c = d - T \to ((c \neq x \land \|c - x\| < b) \leftrightarrow (d - T \neq x \land \|d - T - x\| < b))$
116	115	imbrov2fvoveq	$⊢ c = d - T \to (((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a) \leftrightarrow ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a))$
117		simpllr	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)$
118	48	ad2antlr	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to d \in ℝ$
119	2	ad4antr	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to T \in ℝ$
120	118 119	resubcld	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to d - T \in ℝ$
121		elsni	$⊢ d - T \in \{x\} \to d - T = x$
122	105 121	nsyl	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \neg d - T \in \{x\}$
123	122	ad4ant13	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \neg d - T \in \{x\}$
124	120 123	eldifd	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to d - T \in (ℝ ∖ \{x\})$
125	116 117 124	rspcdva	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)$
126		eqidd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) = (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x})$
127		simpr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d - T) \to y = d - T$
128	127	fveq2d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d - T) \to F (y) = F (d - T)$
129	128	oveq1d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d - T) \to F (y) - F (x) = F (d - T) - F (x)$
130	127	oveq1d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d - T) \to y - x = d - T - x$
131	129 130	oveq12d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land y = d - T) \to \frac{F (y) - F (x)}{y - x} = \frac{F (d - T) - F (x)}{d - T - x}$
132	48	adantl	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d \in ℝ$
133	72 2	syl	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to T \in ℝ$
134	132 133	resubcld	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T \in ℝ$
135	134 122	eldifd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T \in (ℝ ∖ \{x\})$
136	126 131 135 108	fvmptd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) = \frac{F (d - T) - F (x)}{d - T - x}$
137	136	eqcomd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to \frac{F (d - T) - F (x)}{d - T - x} = (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T)$
138	137	ad2antrr	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to \frac{F (d - T) - F (x)}{d - T - x} = (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T)$
139	138	fvoveq1d	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| = \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\|$
140	106	adantr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to d - T \neq x$
141	83	eqcomd	$⊢ ((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \to d - T - x = d - (x + T)$
142	141	adantr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to d - T - x = d - (x + T)$
143	142	fveq2d	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \|d - T - x\| = \|d - (x + T)\|$
144		simpr	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \|d - (x + T)\| < b$
145	143 144	eqbrtrd	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \|d - T - x\| < b$
146	140 145	jca	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to (d - T \neq x \land \|d - T - x\| < b)$
147	146	adantr	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to (d - T \neq x \land \|d - T - x\| < b)$
148		simpr	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)$
149	147 148	mpd	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a$
150	139 149	eqbrtrd	$⊢ ((((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \land ((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a)) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| < a$
151	150	ex	$⊢ (((φ \land x \in dom G) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to (((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| < a)$
152	151	adantllr	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to (((d - T \neq x \land \|d - T - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (d - T) - w\| < a) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| < a)$
153	125 152	mpd	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land \|d - (x + T)\| < b) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| < a$
154	153	adantrl	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land (d \neq x + T \land \|d - (x + T)\| < b)) \to \|(\frac{F (d - T) - F (x)}{d - T - x}) - w\| < a$
155	111 154	eqbrtrd	$⊢ ((((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \land (d \neq x + T \land \|d - (x + T)\| < b)) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a$
156	155	ex	$⊢ (((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \land d \in (ℝ ∖ \{x + T\})) \to ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)$
157	156	ralrimiva	$⊢ ((φ \land x \in dom G) \land \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \to \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)$
158		eqidd	$⊢ c \in (ℝ ∖ \{x\}) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) = (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x})$
159		fveq2	$⊢ y = c \to F (y) = F (c)$
160	159	oveq1d	$⊢ y = c \to F (y) - F (x) = F (c) - F (x)$
161		oveq1	$⊢ y = c \to y - x = c - x$
162	160 161	oveq12d	$⊢ y = c \to \frac{F (y) - F (x)}{y - x} = \frac{F (c) - F (x)}{c - x}$
163	162	adantl	$⊢ (c \in (ℝ ∖ \{x\}) \land y = c) \to \frac{F (y) - F (x)}{y - x} = \frac{F (c) - F (x)}{c - x}$
164		id	$⊢ c \in (ℝ ∖ \{x\}) \to c \in (ℝ ∖ \{x\})$
165		ovexd	$⊢ c \in (ℝ ∖ \{x\}) \to \frac{F (c) - F (x)}{c - x} \in V$
166	158 163 164 165	fvmptd	$⊢ c \in (ℝ ∖ \{x\}) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) = \frac{F (c) - F (x)}{c - x}$
167	166	fvoveq1d	$⊢ c \in (ℝ ∖ \{x\}) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| = \|(\frac{F (c) - F (x)}{c - x}) - w\|$
168	167	ad2antlr	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land (c \neq x \land \|c - x\| < b)) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| = \|(\frac{F (c) - F (x)}{c - x}) - w\|$
169		simpll	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to φ$
170		eldifi	$⊢ c \in (ℝ ∖ \{x\}) \to c \in ℝ$
171	170	adantl	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c \in ℝ$
172		eleq1	$⊢ x = c \to (x \in ℝ \leftrightarrow c \in ℝ)$
173	172	anbi2d	$⊢ x = c \to ((φ \land x \in ℝ) \leftrightarrow (φ \land c \in ℝ))$
174		fvoveq1	$⊢ x = c \to F (x + T) = F (c + T)$
175		fveq2	$⊢ x = c \to F (x) = F (c)$
176	174 175	eqeq12d	$⊢ x = c \to (F (x + T) = F (x) \leftrightarrow F (c + T) = F (c))$
177	173 176	imbi12d	$⊢ x = c \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land c \in ℝ) \to F (c + T) = F (c)))$
178	177 3	chvarvv	$⊢ (φ \land c \in ℝ) \to F (c + T) = F (c)$
179	178	eqcomd	$⊢ (φ \land c \in ℝ) \to F (c) = F (c + T)$
180	169 171 179	syl2anc	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to F (c) = F (c + T)$
181	9	ad2antlr	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to x \in ℝ$
182	169 181 3	syl2anc	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to F (x + T) = F (x)$
183	182	eqcomd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to F (x) = F (x + T)$
184	180 183	oveq12d	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to F (c) - F (x) = F (c + T) - F (x + T)$
185	171	recnd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c \in ℂ$
186	78	adantr	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to x \in ℂ$
187	169 51	syl	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to T \in ℂ$
188	185 186 187	pnpcan2d	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c + T - (x + T) = c - x$
189	188	eqcomd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c - x = c + T - (x + T)$
190	184 189	oveq12d	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to \frac{F (c) - F (x)}{c - x} = \frac{F (c + T) - F (x + T)}{c + T - (x + T)}$
191	190	fvoveq1d	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to \|(\frac{F (c) - F (x)}{c - x}) - w\| = \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\|$
192	191	ad4ant13	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|(\frac{F (c) - F (x)}{c - x}) - w\| = \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\|$
193		neeq1	$⊢ d = c + T \to (d \neq x + T \leftrightarrow c + T \neq x + T)$
194		fvoveq1	$⊢ d = c + T \to \|d - (x + T)\| = \|c + T - (x + T)\|$
195	194	breq1d	$⊢ d = c + T \to (\|d - (x + T)\| < b \leftrightarrow \|c + T - (x + T)\| < b)$
196	193 195	anbi12d	$⊢ d = c + T \to ((d \neq x + T \land \|d - (x + T)\| < b) \leftrightarrow (c + T \neq x + T \land \|c + T - (x + T)\| < b))$
197	196	imbrov2fvoveq	$⊢ d = c + T \to (((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a) \leftrightarrow ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a))$
198		simpllr	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)$
199	170	ad2antlr	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c \in ℝ$
200	2	ad4antr	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to T \in ℝ$
201	199 200	readdcld	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c + T \in ℝ$
202		eldifsni	$⊢ c \in (ℝ ∖ \{x\}) \to c \neq x$
203	202	adantl	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c \neq x$
204	185 186 187 203	addneintr2d	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c + T \neq x + T$
205	204	ad4ant13	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c + T \neq x + T$
206		nelsn	$⊢ c + T \neq x + T \to \neg c + T \in \{x + T\}$
207	205 206	syl	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \neg c + T \in \{x + T\}$
208	201 207	eldifd	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c + T \in (ℝ ∖ \{x + T\})$
209	197 198 208	rspcdva	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)$
210		eqidd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) = (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)})$
211		fveq2	$⊢ y = c + T \to F (y) = F (c + T)$
212	211	oveq1d	$⊢ y = c + T \to F (y) - F (x + T) = F (c + T) - F (x + T)$
213		oveq1	$⊢ y = c + T \to y - (x + T) = c + T - (x + T)$
214	212 213	oveq12d	$⊢ y = c + T \to \frac{F (y) - F (x + T)}{y - (x + T)} = \frac{F (c + T) - F (x + T)}{c + T - (x + T)}$
215	214	adantl	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land y = c + T) \to \frac{F (y) - F (x + T)}{y - (x + T)} = \frac{F (c + T) - F (x + T)}{c + T - (x + T)}$
216	169 2	syl	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to T \in ℝ$
217	171 216	readdcld	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c + T \in ℝ$
218	204 206	syl	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to \neg c + T \in \{x + T\}$
219	217 218	eldifd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to c + T \in (ℝ ∖ \{x + T\})$
220		ovexd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to \frac{F (c + T) - F (x + T)}{c + T - (x + T)} \in V$
221	210 215 219 220	fvmptd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) = \frac{F (c + T) - F (x + T)}{c + T - (x + T)}$
222	221	eqcomd	$⊢ ((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \to \frac{F (c + T) - F (x + T)}{c + T - (x + T)} = (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T)$
223	222	ad2antrr	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to \frac{F (c + T) - F (x + T)}{c + T - (x + T)} = (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T)$
224	223	fvoveq1d	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\| = \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\|$
225	204	adantr	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c + T \neq x + T$
226	170	recnd	$⊢ c \in (ℝ ∖ \{x\}) \to c \in ℂ$
227	226	ad2antlr	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c \in ℂ$
228	186	adantr	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to x \in ℂ$
229	187	adantr	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to T \in ℂ$
230	227 228 229	pnpcan2d	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to c + T - (x + T) = c - x$
231	230	fveq2d	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|c + T - (x + T)\| = \|c - x\|$
232		simpr	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|c - x\| < b$
233	231 232	eqbrtrd	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|c + T - (x + T)\| < b$
234	225 233	jca	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to (c + T \neq x + T \land \|c + T - (x + T)\| < b)$
235	234	adantr	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to (c + T \neq x + T \land \|c + T - (x + T)\| < b)$
236		simpr	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)$
237	235 236	mpd	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a$
238	224 237	eqbrtrd	$⊢ ((((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \land ((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a)) \to \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\| < a$
239	238	ex	$⊢ (((φ \land x \in dom G) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to (((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a) \to \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\| < a)$
240	239	adantllr	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to (((c + T \neq x + T \land \|c + T - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (c + T) - w\| < a) \to \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\| < a)$
241	209 240	mpd	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|(\frac{F (c + T) - F (x + T)}{c + T - (x + T)}) - w\| < a$
242	192 241	eqbrtrd	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land \|c - x\| < b) \to \|(\frac{F (c) - F (x)}{c - x}) - w\| < a$
243	242	adantrl	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land (c \neq x \land \|c - x\| < b)) \to \|(\frac{F (c) - F (x)}{c - x}) - w\| < a$
244	168 243	eqbrtrd	$⊢ ((((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \land (c \neq x \land \|c - x\| < b)) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a$
245	244	ex	$⊢ (((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \land c \in (ℝ ∖ \{x\})) \to ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)$
246	245	ralrimiva	$⊢ ((φ \land x \in dom G) \land \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)) \to \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)$
247	157 246	impbida	$⊢ (φ \land x \in dom G) \to (\forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a) \leftrightarrow \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a))$
248	247	rexbidv	$⊢ (φ \land x \in dom G) \to (\exists b \in ℝ^{+} \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a) \leftrightarrow \exists b \in ℝ^{+} \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a))$
249	248	ralbidv	$⊢ (φ \land x \in dom G) \to (\forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a) \leftrightarrow \forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a))$
250	249	anbi2d	$⊢ (φ \land x \in dom G) \to ((w \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)) \leftrightarrow (w \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)))$
251	39 38 10	dvlem	$⊢ ((φ \land x \in dom G) \land y \in (ℝ ∖ \{x\})) \to \frac{F (y) - F (x)}{y - x} \in ℂ$
252	251	fmpttd	$⊢ (φ \land x \in dom G) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) : ℝ ∖ \{x\} ⟶ ℂ$
253	38	ssdifssd	$⊢ (φ \land x \in dom G) \to ℝ ∖ \{x\} \subseteq ℂ$
254	252 253 78	ellimc3	$⊢ (φ \land x \in dom G) \to (w \in ((y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x) \leftrightarrow (w \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in (ℝ ∖ \{x\}) ((c \neq x \land \|c - x\| < b) \to \|(y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) (c) - w\| < a)))$
255	39 38 12	dvlem	$⊢ ((φ \land x \in dom G) \land y \in (ℝ ∖ \{x + T\})) \to \frac{F (y) - F (x + T)}{y - (x + T)} \in ℂ$
256	255	fmpttd	$⊢ (φ \land x \in dom G) \to (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) : ℝ ∖ \{x + T\} ⟶ ℂ$
257	38	ssdifssd	$⊢ (φ \land x \in dom G) \to ℝ ∖ \{x + T\} \subseteq ℂ$
258	12	recnd	$⊢ (φ \land x \in dom G) \to x + T \in ℂ$
259	256 257 258	ellimc3	$⊢ (φ \land x \in dom G) \to (w \in ((y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) {lim}_{ℂ} (x + T)) \leftrightarrow (w \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℝ^{+} \forall d \in (ℝ ∖ \{x + T\}) ((d \neq x + T \land \|d - (x + T)\| < b) \to \|(y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) (d) - w\| < a)))$
260	250 254 259	3bitr4d	$⊢ (φ \land x \in dom G) \to (w \in ((y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x) \leftrightarrow w \in ((y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) {lim}_{ℂ} (x + T)))$
261	260	eqrdv	$⊢ (φ \land x \in dom G) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x = (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) {lim}_{ℂ} (x + T)$
262		fveq2	$⊢ y = z \to F (y) = F (z)$
263	262	oveq1d	$⊢ y = z \to F (y) - F (x + T) = F (z) - F (x + T)$
264		oveq1	$⊢ y = z \to y - (x + T) = z - (x + T)$
265	263 264	oveq12d	$⊢ y = z \to \frac{F (y) - F (x + T)}{y - (x + T)} = \frac{F (z) - F (x + T)}{z - (x + T)}$
266	265	cbvmptv	$⊢ (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) = (z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)})$
267	266	oveq1i	$⊢ (y \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (y) - F (x + T)}{y - (x + T)}) {lim}_{ℂ} (x + T) = (z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) {lim}_{ℂ} (x + T)$
268	261 267	eqtrdi	$⊢ (φ \land x \in dom G) \to (y \in (ℝ ∖ \{x\}) ⟼ \frac{F (y) - F (x)}{y - x}) {lim}_{ℂ} x = (z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) {lim}_{ℂ} (x + T)$
269	42 268	eleqtrd	$⊢ (φ \land x \in dom G) \to G (x) \in ((z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) {lim}_{ℂ} (x + T))$
270		eqid	$⊢ (z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) = (z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)})$
271	37	a1i	$⊢ φ \to ℝ \subseteq ℂ$
272		ssidd	$⊢ φ \to ℝ \subseteq ℝ$
273	34 35 270 271 1 272	eldv	$⊢ φ \to ((x + T) F_{ℝ}^{'} G (x) \leftrightarrow (x + T \in int (topGen (ran (.))) (ℝ) \land G (x) \in ((z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) {lim}_{ℂ} (x + T))))$
274	273	adantr	$⊢ (φ \land x \in dom G) \to ((x + T) F_{ℝ}^{'} G (x) \leftrightarrow (x + T \in int (topGen (ran (.))) (ℝ) \land G (x) \in ((z \in (ℝ ∖ \{x + T\}) ⟼ \frac{F (z) - F (x + T)}{z - (x + T)}) {lim}_{ℂ} (x + T))))$
275	21 269 274	mpbir2and	$⊢ (φ \land x \in dom G) \to (x + T) F_{ℝ}^{'} G (x)$
276	4	a1i	$⊢ (φ \land x \in dom G) \to G = ℝ D F$
277	276	breqd	$⊢ (φ \land x \in dom G) \to ((x + T) G G (x) \leftrightarrow (x + T) F_{ℝ}^{'} G (x))$
278	275 277	mpbird	$⊢ (φ \land x \in dom G) \to (x + T) G G (x)$
279	4	a1i	$⊢ φ \to G = ℝ D F$
280	279	funeqd	$⊢ φ \to (Fun G \leftrightarrow Fun F_{ℝ}^{'})$
281	29 280	mpbird	$⊢ φ \to Fun G$
282	281	adantr	$⊢ (φ \land x \in dom G) \to Fun G$
283		funbrfv2b	$⊢ Fun G \to ((x + T) G G (x) \leftrightarrow (x + T \in dom G \land G (x + T) = G (x)))$
284	282 283	syl	$⊢ (φ \land x \in dom G) \to ((x + T) G G (x) \leftrightarrow (x + T \in dom G \land G (x + T) = G (x)))$
285	278 284	mpbid	$⊢ (φ \land x \in dom G) \to (x + T \in dom G \land G (x + T) = G (x))$

Metamath Proof Explorer

Theorem fperdvper

Proof