Theorem reccn2 15639

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

Hypothesis

Ref	Expression
reccn2.t	⊢ 𝑇 = (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2))

Assertion

Ref	Expression
reccn2	⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))

Distinct variable groups:   𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑦,𝑇,𝑧

Proof of Theorem reccn2

Step	Hyp	Ref	Expression
1		reccn2.t	. . 3 ⊢ 𝑇 = (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2))
2		1rp 13057	. . . . 5 ⊢ 1 ∈ ℝ+
3		simpl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → 𝐴 ∈ (ℂ ∖ {0}))
4		eldifsn 4811	. . . . . . . 8 ⊢ (𝐴 ∈ (ℂ ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
5	3, 4	sylib 218	. . . . . . 7 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
6		absrpcl 15333	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ+)
7	5, 6	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (abs‘𝐴) ∈ ℝ+)
8		rpmulcl 13076	. . . . . 6 ⊢ (((abs‘𝐴) ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
9	7, 8	sylancom 587	. . . . 5 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
10		ifcl 4593	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ+)
11	2, 9, 10	sylancr 586	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ+)
12	7	rphalfcld 13107	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) / 2) ∈ ℝ+)
13	11, 12	rpmulcld 13111	. . 3 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ∈ ℝ+)
14	1, 13	eqeltrid 2842	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → 𝑇 ∈ ℝ+)
15	5	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
16	15	simpld 494	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐴 ∈ ℂ)
17		simprl 770	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ (ℂ ∖ {0}))
18		eldifsn 4811	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↔ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
19	17, 18	sylib 218	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
20	19	simpld 494	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ ℂ)
21	16, 20	mulcld 11306	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ∈ ℂ)
22		mulne0 11928	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → (𝐴 · 𝑧) ≠ 0)
23	15, 19, 22	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ≠ 0)
24	16, 20, 21, 23	divsubdird 12105	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))))
25	16	mulridd 11303	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 1) = 𝐴)
26	25	oveq1d 7460	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (𝐴 / (𝐴 · 𝑧)))
27		1cnd 11281	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℂ)
28		divcan5 11992	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
29	27, 19, 15, 28	syl3anc 1371	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
30	26, 29	eqtr3d 2776	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 / (𝐴 · 𝑧)) = (1 / 𝑧))
31	20	mulridd 11303	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 1) = 𝑧)
32	20, 16	mulcomd 11307	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 𝐴) = (𝐴 · 𝑧))
33	31, 32	oveq12d 7463	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (𝑧 / (𝐴 · 𝑧)))
34		divcan5 11992	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
35	27, 15, 19, 34	syl3anc 1371	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
36	33, 35	eqtr3d 2776	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 / (𝐴 · 𝑧)) = (1 / 𝐴))
37	30, 36	oveq12d 7463	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))) = ((1 / 𝑧) − (1 / 𝐴)))
38	24, 37	eqtrd 2774	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((1 / 𝑧) − (1 / 𝐴)))
39	38	fveq2d 6923	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = (abs‘((1 / 𝑧) − (1 / 𝐴))))
40	16, 20	subcld 11643	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 − 𝑧) ∈ ℂ)
41	40, 21, 23	absdivd 15500	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
42	39, 41	eqtr3d 2776	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
43	16, 20	abssubd 15498	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) = (abs‘(𝑧 − 𝐴)))
44	20, 16	subcld 11643	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 − 𝐴) ∈ ℂ)
45	44	abscld 15481	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
46	43, 45	eqeltrd 2838	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) ∈ ℝ)
47	14	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ+)
48	47	rpred 13095	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ)
49	21	abscld 15481	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ)
50		rpre 13061	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ)
51	50	ad2antlr 726	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℝ)
52	49, 51	remulcld 11316	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) ∈ ℝ)
53		simprr 772	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) < 𝑇)
54	43, 53	eqbrtrd 5191	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < 𝑇)
55	9	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
56	55	rpred 13095	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ)
57	12	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ+)
58	57	rpred 13095	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ)
59	56, 58	remulcld 11316	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) ∈ ℝ)
60		1re 11286	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
61		min2 13248	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵))
62	60, 56, 61	sylancr 586	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵))
63	11	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ+)
64	63	rpred 13095	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ)
65	64, 56, 57	lemul1d 13138	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵) ↔ (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2))))
66	62, 65	mpbid 232	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)))
67	1, 66	eqbrtrid 5204	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)))
68	20	abscld 15481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℝ)
69	16	abscld 15481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℝ)
70	69	recnd 11314	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℂ)
71	70	2halvesd 12535	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) = (abs‘𝐴))
72	69, 68	resubcld 11714	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ∈ ℝ)
73	16, 20	abs2difd 15502	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ≤ (abs‘(𝐴 − 𝑧)))
74		min1 13247	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1)
75	60, 56, 74	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1)
76		1red 11287	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℝ)
77	64, 76, 57	lemul1d 13138	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (1 · ((abs‘𝐴) / 2))))
78	75, 77	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (1 · ((abs‘𝐴) / 2)))
79	1, 78	eqbrtrid 5204	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (1 · ((abs‘𝐴) / 2)))
80	58	recnd 11314	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℂ)
81	80	mullidd 11304	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (1 · ((abs‘𝐴) / 2)) = ((abs‘𝐴) / 2))
82	79, 81	breqtrd 5195	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ ((abs‘𝐴) / 2))
83	46, 48, 58, 54, 82	ltletrd 11446	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘𝐴) / 2))
84	72, 46, 58, 73, 83	lelttrd 11444	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) < ((abs‘𝐴) / 2))
85	69, 68, 58	ltsubadd2d 11884	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) − (abs‘𝑧)) < ((abs‘𝐴) / 2) ↔ (abs‘𝐴) < ((abs‘𝑧) + ((abs‘𝐴) / 2))))
86	84, 85	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) < ((abs‘𝑧) + ((abs‘𝐴) / 2)))
87	71, 86	eqbrtrd 5191	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) < ((abs‘𝑧) + ((abs‘𝐴) / 2)))
88	58, 68, 58	ltadd1d 11879	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) < (abs‘𝑧) ↔ (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) < ((abs‘𝑧) + ((abs‘𝐴) / 2))))
89	87, 88	mpbird 257	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) < (abs‘𝑧))
90	58, 68, 55, 89	ltmul2dd 13151	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
91	16, 20	absmuld 15499	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) = ((abs‘𝐴) · (abs‘𝑧)))
92	91	oveq1d 7460	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · (abs‘𝑧)) · 𝐵))
93	68	recnd 11314	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℂ)
94	51	recnd 11314	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℂ)
95	70, 93, 94	mul32d 11496	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · (abs‘𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
96	92, 95	eqtrd 2774	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
97	90, 96	breqtrrd 5197	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
98	48, 59, 52, 67, 97	lelttrd 11444	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 < ((abs‘(𝐴 · 𝑧)) · 𝐵))
99	46, 48, 52, 54, 98	lttrd 11447	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
100	21, 23	absrpcld 15493	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ+)
101	46, 51, 100	ltdivmuld 13146	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵 ↔ (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵)))
102	99, 101	mpbird 257	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵)
103	42, 102	eqbrtrd 5191	. . . 4 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)
104	103	expr 456	. . 3 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ 𝑧 ∈ (ℂ ∖ {0})) → ((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
105	104	ralrimiva 3148	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
106		breq2 5173	. . 3 ⊢ (𝑦 = 𝑇 → ((abs‘(𝑧 − 𝐴)) < 𝑦 ↔ (abs‘(𝑧 − 𝐴)) < 𝑇))
107	106	rspceaimv 3637	. 2 ⊢ ((𝑇 ∈ ℝ+ ∧ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
108	14, 105, 107	syl2anc 583	1 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2103   ≠ wne 2942  ∀wral 3063  ∃wrex 3072   ∖ cdif 3967  ifcif 4548  {csn 4648   class class class wbr 5169  ‘cfv 6572  (class class class)co 7445  ℂcc 11178  ℝcr 11179  0cc0 11180  1c1 11181   + caddc 11183   · cmul 11185   < clt 11320   ≤ cle 11321   − cmin 11516   / cdiv 11943  2c2 12344  ℝ⁺crp 13053  abscabs 15279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766  ax-cnex 11236  ax-resscn 11237  ax-1cn 11238  ax-icn 11239  ax-addcl 11240  ax-addrcl 11241  ax-mulcl 11242  ax-mulrcl 11243  ax-mulcom 11244  ax-addass 11245  ax-mulass 11246  ax-distr 11247  ax-i2m1 11248  ax-1ne0 11249  ax-1rid 11250  ax-rnegex 11251  ax-rrecex 11252  ax-cnre 11253  ax-pre-lttri 11254  ax-pre-lttrn 11255  ax-pre-ltadd 11256  ax-pre-mulgt0 11257  ax-pre-sup 11258

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-pred 6331  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-riota 7401  df-ov 7448  df-oprab 7449  df-mpo 7450  df-om 7900  df-2nd 8027  df-frecs 8318  df-wrecs 8349  df-recs 8423  df-rdg 8462  df-er 8759  df-en 9000  df-dom 9001  df-sdom 9002  df-sup 9507  df-pnf 11322  df-mnf 11323  df-xr 11324  df-ltxr 11325  df-le 11326  df-sub 11518  df-neg 11519  df-div 11944  df-nn 12290  df-2 12352  df-3 12353  df-n0 12550  df-z 12636  df-uz 12900  df-rp 13054  df-seq 14049  df-exp 14109  df-cj 15144  df-re 15145  df-im 15146  df-sqrt 15280  df-abs 15281

This theorem is referenced by:  rlimdiv  15690  divcnOLD  24902  divcn  24904  climrec  45458