reccn2

Description: The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014) (Revised by Mario Carneiro, 22-Sep-2014)

		Ref	Expression
	Hypothesis	reccn2.t	$⊢ T = if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2})$
	Assertion	reccn2	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)$

Proof

Step	Hyp	Ref	Expression
1		reccn2.t	$⊢ T = if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2})$
2		1rp	$⊢ 1 \in ℝ^{+}$
3		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
4	3	birani	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to (A \in ℂ \land A \neq 0)$
5		absrpcl	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ^{+}$
6	4 5	syl	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \|A\| \in ℝ^{+}$
7		rpmulcl	$⊢ (\|A\| \in ℝ^{+} \land B \in ℝ^{+}) \to \|A\| B \in ℝ^{+}$
8	6 7	sylancom	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \|A\| B \in ℝ^{+}$
9		ifcl	$⊢ (1 \in ℝ^{+} \land \|A\| B \in ℝ^{+}) \to if (1 \leq \|A\| B, 1, \|A\| B) \in ℝ^{+}$
10	2 8 9	sylancr	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to if (1 \leq \|A\| B, 1, \|A\| B) \in ℝ^{+}$
11	6	rphalfcld	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \frac{\|A\|}{2} \in ℝ^{+}$
12	10 11	rpmulcld	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2}) \in ℝ^{+}$
13	1 12	eqeltrid	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to T \in ℝ^{+}$
14	4	adantr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (A \in ℂ \land A \neq 0)$
15	14	simpld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to A \in ℂ$
16		simprl	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to z \in (ℂ ∖ \{0\})$
17		eldifsn	$⊢ z \in (ℂ ∖ \{0\}) \leftrightarrow (z \in ℂ \land z \neq 0)$
18	16 17	sylib	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (z \in ℂ \land z \neq 0)$
19	18	simpld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to z \in ℂ$
20	15 19	mulcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to A z \in ℂ$
21		mulne0	$⊢ ((A \in ℂ \land A \neq 0) \land (z \in ℂ \land z \neq 0)) \to A z \neq 0$
22	14 18 21	syl2anc	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to A z \neq 0$
23	15 19 20 22	divsubdird	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{A - z}{A z} = (\frac{A}{A z}) - (\frac{z}{A z})$
24	15	mulridd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to A \cdot 1 = A$
25	24	oveq1d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{A \cdot 1}{A z} = \frac{A}{A z}$
26		1cnd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to 1 \in ℂ$
27		divcan5	$⊢ (1 \in ℂ \land (z \in ℂ \land z \neq 0) \land (A \in ℂ \land A \neq 0)) \to \frac{A \cdot 1}{A z} = \frac{1}{z}$
28	26 18 14 27	syl3anc	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{A \cdot 1}{A z} = \frac{1}{z}$
29	25 28	eqtr3d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{A}{A z} = \frac{1}{z}$
30	19	mulridd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to z \cdot 1 = z$
31	19 15	mulcomd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to z A = A z$
32	30 31	oveq12d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{z \cdot 1}{z A} = \frac{z}{A z}$
33		divcan5	$⊢ (1 \in ℂ \land (A \in ℂ \land A \neq 0) \land (z \in ℂ \land z \neq 0)) \to \frac{z \cdot 1}{z A} = \frac{1}{A}$
34	26 14 18 33	syl3anc	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{z \cdot 1}{z A} = \frac{1}{A}$
35	32 34	eqtr3d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{z}{A z} = \frac{1}{A}$
36	29 35	oveq12d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\frac{A}{A z}) - (\frac{z}{A z}) = (\frac{1}{z}) - (\frac{1}{A})$
37	23 36	eqtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{A - z}{A z} = (\frac{1}{z}) - (\frac{1}{A})$
38	37	fveq2d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|\frac{A - z}{A z}\| = \|(\frac{1}{z}) - (\frac{1}{A})\|$
39	15 19	subcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to A - z \in ℂ$
40	39 20 22	absdivd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|\frac{A - z}{A z}\| = \frac{\|A - z\|}{\|A z\|}$
41	38 40	eqtr3d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|(\frac{1}{z}) - (\frac{1}{A})\| = \frac{\|A - z\|}{\|A z\|}$
42	15 19	abssubd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A - z\| = \|z - A\|$
43	19 15	subcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to z - A \in ℂ$
44	43	abscld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|z - A\| \in ℝ$
45	42 44	eqeltrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A - z\| \in ℝ$
46	13	adantr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T \in ℝ^{+}$
47	46	rpred	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T \in ℝ$
48	20	abscld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| \in ℝ$
49		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
50	49	ad2antlr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to B \in ℝ$
51	48 50	remulcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| B \in ℝ$
52		simprr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|z - A\| < T$
53	42 52	eqbrtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A - z\| < T$
54	8	adantr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| B \in ℝ^{+}$
55	54	rpred	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| B \in ℝ$
56	11	adantr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{\|A\|}{2} \in ℝ^{+}$
57	56	rpred	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{\|A\|}{2} \in ℝ$
58	55 57	remulcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| B (\frac{\|A\|}{2}) \in ℝ$
59		1re	$⊢ 1 \in ℝ$
60		min2	$⊢ (1 \in ℝ \land \|A\| B \in ℝ) \to if (1 \leq \|A\| B, 1, \|A\| B) \leq \|A\| B$
61	59 55 60	sylancr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) \leq \|A\| B$
62	10	adantr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) \in ℝ^{+}$
63	62	rpred	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) \in ℝ$
64	63 55 56	lemul1d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (if (1 \leq \|A\| B, 1, \|A\| B) \leq \|A\| B \leftrightarrow if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2}) \leq \|A\| B (\frac{\|A\|}{2}))$
65	61 64	mpbid	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2}) \leq \|A\| B (\frac{\|A\|}{2})$
66	1 65	eqbrtrid	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T \leq \|A\| B (\frac{\|A\|}{2})$
67	19	abscld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|z\| \in ℝ$
68	15	abscld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| \in ℝ$
69	68	recnd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| \in ℂ$
70	69	2halvesd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\frac{\|A\|}{2}) + (\frac{\|A\|}{2}) = \|A\|$
71	68 67	resubcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| - \|z\| \in ℝ$
72	15 19	abs2difd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| - \|z\| \leq \|A - z\|$
73		min1	$⊢ (1 \in ℝ \land \|A\| B \in ℝ) \to if (1 \leq \|A\| B, 1, \|A\| B) \leq 1$
74	59 55 73	sylancr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) \leq 1$
75		1red	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to 1 \in ℝ$
76	63 75 56	lemul1d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (if (1 \leq \|A\| B, 1, \|A\| B) \leq 1 \leftrightarrow if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2}) \leq 1 (\frac{\|A\|}{2}))$
77	74 76	mpbid	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to if (1 \leq \|A\| B, 1, \|A\| B) (\frac{\|A\|}{2}) \leq 1 (\frac{\|A\|}{2})$
78	1 77	eqbrtrid	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T \leq 1 (\frac{\|A\|}{2})$
79	57	recnd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{\|A\|}{2} \in ℂ$
80	79	mullidd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to 1 (\frac{\|A\|}{2}) = \frac{\|A\|}{2}$
81	78 80	breqtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T \leq \frac{\|A\|}{2}$
82	45 47 57 53 81	ltletrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A - z\| < \frac{\|A\|}{2}$
83	71 45 57 72 82	lelttrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| - \|z\| < \frac{\|A\|}{2}$
84	68 67 57	ltsubadd2d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\|A\| - \|z\| < \frac{\|A\|}{2} \leftrightarrow \|A\| < \|z\| + (\frac{\|A\|}{2}))$
85	83 84	mpbid	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| < \|z\| + (\frac{\|A\|}{2})$
86	70 85	eqbrtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\frac{\|A\|}{2}) + (\frac{\|A\|}{2}) < \|z\| + (\frac{\|A\|}{2})$
87	57 67 57	ltadd1d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\frac{\|A\|}{2} < \|z\| \leftrightarrow (\frac{\|A\|}{2}) + (\frac{\|A\|}{2}) < \|z\| + (\frac{\|A\|}{2}))$
88	86 87	mpbird	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{\|A\|}{2} < \|z\|$
89	57 67 54 88	ltmul2dd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| B (\frac{\|A\|}{2}) < \|A\| B \|z\|$
90	15 19	absmuld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| = \|A\| \|z\|$
91	90	oveq1d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| B = \|A\| \|z\| B$
92	67	recnd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|z\| \in ℂ$
93	50	recnd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to B \in ℂ$
94	69 92 93	mul32d	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| \|z\| B = \|A\| B \|z\|$
95	91 94	eqtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| B = \|A\| B \|z\|$
96	89 95	breqtrrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A\| B (\frac{\|A\|}{2}) < \|A z\| B$
97	47 58 51 66 96	lelttrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to T < \|A z\| B$
98	45 47 51 53 97	lttrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A - z\| < \|A z\| B$
99	20 22	absrpcld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|A z\| \in ℝ^{+}$
100	45 50 99	ltdivmuld	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to (\frac{\|A - z\|}{\|A z\|} < B \leftrightarrow \|A - z\| < \|A z\| B)$
101	98 100	mpbird	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \frac{\|A - z\|}{\|A z\|} < B$
102	41 101	eqbrtrd	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \land \|z - A\| < T)) \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B$
103	102	expr	$⊢ ((A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \land z \in (ℂ ∖ \{0\})) \to (\|z - A\| < T \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)$
104	103	ralrimiva	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < T \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)$
105		breq2	$⊢ y = T \to (\|z - A\| < y \leftrightarrow \|z - A\| < T)$
106	105	rspceaimv	$⊢ (T \in ℝ^{+} \land \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < T \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)$
107	13 104 106	syl2anc	$⊢ (A \in (ℂ ∖ \{0\}) \land B \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < B)$

Metamath Proof Explorer

Theorem reccn2

Proof