Theorem cn1lem

Description: A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Hypotheses	cn1lem.1	$$⊢F:ℂ⟶ℂ$$
	cn1lem.2	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|F\left(z\right)-F\left(A\right)\right|\le \left|z-A\right|$$
Assertion	cn1lem	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		cn1lem.1	$$⊢F:ℂ⟶ℂ$$
2		cn1lem.2	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|F\left(z\right)-F\left(A\right)\right|\le \left|z-A\right|$$
3		simpr	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x\in {ℝ}^{+}$$
4		simpr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to z\in ℂ$$
5		simpll	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to A\in ℂ$$
6	4 5 2	syl2anc	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to \left|F\left(z\right)-F\left(A\right)\right|\le \left|z-A\right|$$
7	1	ffvelrni	$$⊢z\in ℂ\to F\left(z\right)\in ℂ$$
8	4 7	syl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to F\left(z\right)\in ℂ$$
9	1	ffvelrni	$$⊢A\in ℂ\to F\left(A\right)\in ℂ$$
10	5 9	syl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to F\left(A\right)\in ℂ$$
11	8 10	subcld	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to F\left(z\right)-F\left(A\right)\in ℂ$$
12	11	abscld	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to \left|F\left(z\right)-F\left(A\right)\right|\in ℝ$$
13	4 5	subcld	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to z-A\in ℂ$$
14	13	abscld	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to \left|z-A\right|\in ℝ$$
15		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
16	15	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to x\in ℝ$$
17		lelttr	$$⊢\left(\left|F\left(z\right)-F\left(A\right)\right|\in ℝ\wedge \left|z-A\right|\in ℝ\wedge x\in ℝ\right)\to \left(\left(\left|F\left(z\right)-F\left(A\right)\right|\le \left|z-A\right|\wedge \left|z-A\right|<x\right)\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
18	12 14 16 17	syl3anc	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to \left(\left(\left|F\left(z\right)-F\left(A\right)\right|\le \left|z-A\right|\wedge \left|z-A\right|<x\right)\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
19	6 18	mpand	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge z\in ℂ\right)\to \left(\left|z-A\right|<x\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
20	19	ralrimiva	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \forall z\in ℂ\left(\left|z-A\right|<x\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
21		breq2	$$⊢y=x\to \left(\left|z-A\right|<y\leftrightarrow \left|z-A\right|<x\right)$$
22	21	rspceaimv	$$⊢\left(x\in {ℝ}^{+}\wedge \forall z\in ℂ\left(\left|z-A\right|<x\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$
23	3 20 22	syl2anc	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|F\left(z\right)-F\left(A\right)\right|<x\right)$$