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