Theorem reccn2 15548

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 12985	. . . . 5 ⊢ 1 ∈ ℝ+
3		simpl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → 𝐴 ∈ (ℂ ∖ {0}))
4		eldifsn 4790	. . . . . . . 8 ⊢ (𝐴 ∈ (ℂ ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
5	3, 4	sylib 217	. . . . . . 7 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
6		absrpcl 15242	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ+)
7	5, 6	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (abs‘𝐴) ∈ ℝ+)
8		rpmulcl 13004	. . . . . 6 ⊢ (((abs‘𝐴) ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
9	7, 8	sylancom 587	. . . . 5 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
10		ifcl 4573	. . . . 5 ⊢ ((1 ∈ ℝ+ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ+) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ+)
11	2, 9, 10	sylancr 586	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ+)
12	7	rphalfcld 13035	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ((abs‘𝐴) / 2) ∈ ℝ+)
13	11, 12	rpmulcld 13039	. . 3 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ∈ ℝ+)
14	1, 13	eqeltrid 2836	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → 𝑇 ∈ ℝ+)
15	5	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
16	15	simpld 494	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐴 ∈ ℂ)
17		simprl 768	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ (ℂ ∖ {0}))
18		eldifsn 4790	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↔ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
19	17, 18	sylib 217	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
20	19	simpld 494	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ ℂ)
21	16, 20	mulcld 11241	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ∈ ℂ)
22		mulne0 11863	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → (𝐴 · 𝑧) ≠ 0)
23	15, 19, 22	syl2anc 583	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ≠ 0)
24	16, 20, 21, 23	divsubdird 12036	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))))
25	16	mulridd 11238	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 1) = 𝐴)
26	25	oveq1d 7427	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (𝐴 / (𝐴 · 𝑧)))
27		1cnd 11216	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℂ)
28		divcan5 11923	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
29	27, 19, 15, 28	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
30	26, 29	eqtr3d 2773	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 / (𝐴 · 𝑧)) = (1 / 𝑧))
31	20	mulridd 11238	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 1) = 𝑧)
32	20, 16	mulcomd 11242	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 𝐴) = (𝐴 · 𝑧))
33	31, 32	oveq12d 7430	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (𝑧 / (𝐴 · 𝑧)))
34		divcan5 11923	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
35	27, 15, 19, 34	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
36	33, 35	eqtr3d 2773	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 / (𝐴 · 𝑧)) = (1 / 𝐴))
37	30, 36	oveq12d 7430	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))) = ((1 / 𝑧) − (1 / 𝐴)))
38	24, 37	eqtrd 2771	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((1 / 𝑧) − (1 / 𝐴)))
39	38	fveq2d 6895	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = (abs‘((1 / 𝑧) − (1 / 𝐴))))
40	16, 20	subcld 11578	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 − 𝑧) ∈ ℂ)
41	40, 21, 23	absdivd 15409	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
42	39, 41	eqtr3d 2773	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
43	16, 20	abssubd 15407	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) = (abs‘(𝑧 − 𝐴)))
44	20, 16	subcld 11578	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 − 𝐴) ∈ ℂ)
45	44	abscld 15390	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
46	43, 45	eqeltrd 2832	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) ∈ ℝ)
47	14	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ+)
48	47	rpred 13023	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ)
49	21	abscld 15390	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ)
50		rpre 12989	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ)
51	50	ad2antlr 724	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℝ)
52	49, 51	remulcld 11251	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) ∈ ℝ)
53		simprr 770	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) < 𝑇)
54	43, 53	eqbrtrd 5170	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < 𝑇)
55	9	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ+)
56	55	rpred 13023	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ)
57	12	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ+)
58	57	rpred 13023	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ)
59	56, 58	remulcld 11251	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) ∈ ℝ)
60		1re 11221	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
61		min2 13176	. . . . . . . . . . 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 13023	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ)
65	64, 56, 57	lemul1d 13066	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵) ↔ (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2))))
66	62, 65	mpbid 231	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)))
67	1, 66	eqbrtrid 5183	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)))
68	20	abscld 15390	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℝ)
69	16	abscld 15390	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℝ)
70	69	recnd 11249	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℂ)
71	70	2halvesd 12465	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) = (abs‘𝐴))
72	69, 68	resubcld 11649	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ∈ ℝ)
73	16, 20	abs2difd 15411	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ≤ (abs‘(𝐴 − 𝑧)))
74		min1 13175	. . . . . . . . . . . . . . . . . . 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 11222	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℝ)
77	64, 76, 57	lemul1d 13066	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1 ↔ (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (1 · ((abs‘𝐴) / 2))))
78	75, 77	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ≤ (1 · ((abs‘𝐴) / 2)))
79	1, 78	eqbrtrid 5183	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (1 · ((abs‘𝐴) / 2)))
80	58	recnd 11249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℂ)
81	80	mullidd 11239	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (1 · ((abs‘𝐴) / 2)) = ((abs‘𝐴) / 2))
82	79, 81	breqtrd 5174	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ ((abs‘𝐴) / 2))
83	46, 48, 58, 54, 82	ltletrd 11381	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘𝐴) / 2))
84	72, 46, 58, 73, 83	lelttrd 11379	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) < ((abs‘𝐴) / 2))
85	69, 68, 58	ltsubadd2d 11819	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) − (abs‘𝑧)) < ((abs‘𝐴) / 2) ↔ (abs‘𝐴) < ((abs‘𝑧) + ((abs‘𝐴) / 2))))
86	84, 85	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) < ((abs‘𝑧) + ((abs‘𝐴) / 2)))
87	71, 86	eqbrtrd 5170	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) < ((abs‘𝑧) + ((abs‘𝐴) / 2)))
88	58, 68, 58	ltadd1d 11814	. . . . . . . . . . 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 13079	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
91	16, 20	absmuld 15408	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) = ((abs‘𝐴) · (abs‘𝑧)))
92	91	oveq1d 7427	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · (abs‘𝑧)) · 𝐵))
93	68	recnd 11249	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℂ)
94	51	recnd 11249	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℂ)
95	70, 93, 94	mul32d 11431	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · (abs‘𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
96	92, 95	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
97	90, 96	breqtrrd 5176	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
98	48, 59, 52, 67, 97	lelttrd 11379	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 < ((abs‘(𝐴 · 𝑧)) · 𝐵))
99	46, 48, 52, 54, 98	lttrd 11382	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
100	21, 23	absrpcld 15402	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ+)
101	46, 51, 100	ltdivmuld 13074	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵 ↔ (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵)))
102	99, 101	mpbird 257	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵)
103	42, 102	eqbrtrd 5170	. . . 4 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)
104	103	expr 456	. . 3 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) ∧ 𝑧 ∈ (ℂ ∖ {0})) → ((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
105	104	ralrimiva 3145	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ+) → ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
106		breq2 5152	. . 3 ⊢ (𝑦 = 𝑇 → ((abs‘(𝑧 − 𝐴)) < 𝑦 ↔ (abs‘(𝑧 − 𝐴)) < 𝑇))
107	106	rspceaimv 3617	. 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 1540   ∈ wcel 2105   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ∖ cdif 3945  ifcif 4528  {csn 4628   class class class wbr 5148  ‘cfv 6543  (class class class)co 7412  ℂcc 11114  ℝcr 11115  0cc0 11116  1c1 11117   + caddc 11119   · cmul 11121   < clt 11255   ≤ cle 11256   − cmin 11451   / cdiv 11878  2c2 12274  ℝ⁺crp 12981  abscabs 15188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-sup 9443  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-n0 12480  df-z 12566  df-uz 12830  df-rp 12982  df-seq 13974  df-exp 14035  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190

This theorem is referenced by:  rlimdiv  15599  divcnOLD  24617  divcn  24619  climrec  44630