reccn2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > reccn2		Structured version Visualization version GIF version

Theorem reccn2 15537

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 12974	. . . . 5 ⊢ 1 ∈ ℝ⁺
3		simpl 483	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → 𝐴 ∈ (ℂ ∖ {0}))
4		eldifsn 4789	. . . . . . . 8 ⊢ (𝐴 ∈ (ℂ ∖ {0}) ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
5	3, 4	sylib 217	. . . . . . 7 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
6		absrpcl 15231	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ⁺)
7	5, 6	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → (abs‘𝐴) ∈ ℝ⁺)
8		rpmulcl 12993	. . . . . 6 ⊢ (((abs‘𝐴) ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺) → ((abs‘𝐴) · 𝐵) ∈ ℝ⁺)
9	7, 8	sylancom 588	. . . . 5 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → ((abs‘𝐴) · 𝐵) ∈ ℝ⁺)
10		ifcl 4572	. . . . 5 ⊢ ((1 ∈ ℝ⁺ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ⁺) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ⁺)
11	2, 9, 10	sylancr 587	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ⁺)
12	7	rphalfcld 13024	. . . 4 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → ((abs‘𝐴) / 2) ∈ ℝ⁺)
13	11, 12	rpmulcld 13028	. . 3 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → (if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) · ((abs‘𝐴) / 2)) ∈ ℝ⁺)
14	1, 13	eqeltrid 2837	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
15	5	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0))
16	15	simpld 495	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐴 ∈ ℂ)
17		simprl 769	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ (ℂ ∖ {0}))
18		eldifsn 4789	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↔ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
19	17, 18	sylib 217	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
20	19	simpld 495	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑧 ∈ ℂ)
21	16, 20	mulcld 11230	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ∈ ℂ)
22		mulne0 11852	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → (𝐴 · 𝑧) ≠ 0)
23	15, 19, 22	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 𝑧) ≠ 0)
24	16, 20, 21, 23	divsubdird 12025	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))))
25	16	mulridd 11227	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 · 1) = 𝐴)
26	25	oveq1d 7420	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (𝐴 / (𝐴 · 𝑧)))
27		1cnd 11205	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℂ)
28		divcan5 11912	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
29	27, 19, 15, 28	syl3anc 1371	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 · 1) / (𝐴 · 𝑧)) = (1 / 𝑧))
30	26, 29	eqtr3d 2774	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 / (𝐴 · 𝑧)) = (1 / 𝑧))
31	20	mulridd 11227	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 1) = 𝑧)
32	20, 16	mulcomd 11231	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 · 𝐴) = (𝐴 · 𝑧))
33	31, 32	oveq12d 7423	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (𝑧 / (𝐴 · 𝑧)))
34		divcan5 11912	. . . . . . . . . . 11 ⊢ ((1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
35	27, 15, 19, 34	syl3anc 1371	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝑧 · 1) / (𝑧 · 𝐴)) = (1 / 𝐴))
36	33, 35	eqtr3d 2774	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 / (𝐴 · 𝑧)) = (1 / 𝐴))
37	30, 36	oveq12d 7423	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 / (𝐴 · 𝑧)) − (𝑧 / (𝐴 · 𝑧))) = ((1 / 𝑧) − (1 / 𝐴)))
38	24, 37	eqtrd 2772	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((𝐴 − 𝑧) / (𝐴 · 𝑧)) = ((1 / 𝑧) − (1 / 𝐴)))
39	38	fveq2d 6892	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = (abs‘((1 / 𝑧) − (1 / 𝐴))))
40	16, 20	subcld 11567	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝐴 − 𝑧) ∈ ℂ)
41	40, 21, 23	absdivd 15398	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((𝐴 − 𝑧) / (𝐴 · 𝑧))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
42	39, 41	eqtr3d 2774	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) = ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))))
43	16, 20	abssubd 15396	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) = (abs‘(𝑧 − 𝐴)))
44	20, 16	subcld 11567	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (𝑧 − 𝐴) ∈ ℂ)
45	44	abscld 15379	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) ∈ ℝ)
46	43, 45	eqeltrd 2833	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) ∈ ℝ)
47	14	adantr 481	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ⁺)
48	47	rpred 13012	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ∈ ℝ)
49	21	abscld 15379	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ)
50		rpre 12978	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ⁺ → 𝐵 ∈ ℝ)
51	50	ad2antlr 725	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℝ)
52	49, 51	remulcld 11240	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) ∈ ℝ)
53		simprr 771	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝑧 − 𝐴)) < 𝑇)
54	43, 53	eqbrtrd 5169	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < 𝑇)
55	9	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ⁺)
56	55	rpred 13012	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) · 𝐵) ∈ ℝ)
57	12	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ⁺)
58	57	rpred 13012	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℝ)
59	56, 58	remulcld 11240	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) ∈ ℝ)
60		1re 11210	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
61		min2 13165	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵))
62	60, 56, 61	sylancr 587	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ ((abs‘𝐴) · 𝐵))
63	11	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ⁺)
64	63	rpred 13012	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ∈ ℝ)
65	64, 56, 57	lemul1d 13055	. . . . . . . . . 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 5182	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)))
68	20	abscld 15379	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℝ)
69	16	abscld 15379	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℝ)
70	69	recnd 11238	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝐴) ∈ ℂ)
71	70	2halvesd 12454	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) = (abs‘𝐴))
72	69, 68	resubcld 11638	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ∈ ℝ)
73	16, 20	abs2difd 15400	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) ≤ (abs‘(𝐴 − 𝑧)))
74		min1 13164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((abs‘𝐴) · 𝐵) ∈ ℝ) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1)
75	60, 56, 74	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → if(1 ≤ ((abs‘𝐴) · 𝐵), 1, ((abs‘𝐴) · 𝐵)) ≤ 1)
76		1red 11211	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 1 ∈ ℝ)
77	64, 76, 57	lemul1d 13055	. . . . . . . . . . . . . . . . . 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 5182	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ (1 · ((abs‘𝐴) / 2)))
80	58	recnd 11238	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) ∈ ℂ)
81	80	mullidd 11228	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (1 · ((abs‘𝐴) / 2)) = ((abs‘𝐴) / 2))
82	79, 81	breqtrd 5173	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 ≤ ((abs‘𝐴) / 2))
83	46, 48, 58, 54, 82	ltletrd 11370	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘𝐴) / 2))
84	72, 46, 58, 73, 83	lelttrd 11368	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) − (abs‘𝑧)) < ((abs‘𝐴) / 2))
85	69, 68, 58	ltsubadd2d 11808	. . . . . . . . . . . . 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 5169	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) < ((abs‘𝑧) + ((abs‘𝐴) / 2)))
88	58, 68, 58	ltadd1d 11803	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) / 2) < (abs‘𝑧) ↔ (((abs‘𝐴) / 2) + ((abs‘𝐴) / 2)) < ((abs‘𝑧) + ((abs‘𝐴) / 2))))
89	87, 88	mpbird 256	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘𝐴) / 2) < (abs‘𝑧))
90	58, 68, 55, 89	ltmul2dd 13068	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
91	16, 20	absmuld 15397	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) = ((abs‘𝐴) · (abs‘𝑧)))
92	91	oveq1d 7420	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · (abs‘𝑧)) · 𝐵))
93	68	recnd 11238	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘𝑧) ∈ ℂ)
94	51	recnd 11238	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝐵 ∈ ℂ)
95	70, 93, 94	mul32d 11420	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · (abs‘𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
96	92, 95	eqtrd 2772	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 · 𝑧)) · 𝐵) = (((abs‘𝐴) · 𝐵) · (abs‘𝑧)))
97	90, 96	breqtrrd 5175	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘𝐴) · 𝐵) · ((abs‘𝐴) / 2)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
98	48, 59, 52, 67, 97	lelttrd 11368	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → 𝑇 < ((abs‘(𝐴 · 𝑧)) · 𝐵))
99	46, 48, 52, 54, 98	lttrd 11371	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵))
100	21, 23	absrpcld 15391	. . . . . . 7 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘(𝐴 · 𝑧)) ∈ ℝ⁺)
101	46, 51, 100	ltdivmuld 13063	. . . . . 6 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵 ↔ (abs‘(𝐴 − 𝑧)) < ((abs‘(𝐴 · 𝑧)) · 𝐵)))
102	99, 101	mpbird 256	. . . . 5 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → ((abs‘(𝐴 − 𝑧)) / (abs‘(𝐴 · 𝑧))) < 𝐵)
103	42, 102	eqbrtrd 5169	. . . 4 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ (𝑧 ∈ (ℂ ∖ {0}) ∧ (abs‘(𝑧 − 𝐴)) < 𝑇)) → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)
104	103	expr 457	. . 3 ⊢ (((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) ∧ 𝑧 ∈ (ℂ ∖ {0})) → ((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
105	104	ralrimiva 3146	. 2 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
106		breq2 5151	. . 3 ⊢ (𝑦 = 𝑇 → ((abs‘(𝑧 − 𝐴)) < 𝑦 ↔ (abs‘(𝑧 − 𝐴)) < 𝑇))
107	106	rspceaimv 3616	. 2 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑇 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))
108	14, 105, 107	syl2anc 584	1 ⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ (ℂ ∖ {0})((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∖ cdif 3944 ifcif 4527 {csn 4627 class class class wbr 5147 ‘cfv 6540 (class class class)co 7405 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 < clt 11244 ≤ cle 11245 − cmin 11440 / cdiv 11867 2c2 12263 ℝ⁺crp 12970 abscabs 15177

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-sup 9433 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-z 12555 df-uz 12819 df-rp 12971 df-seq 13963 df-exp 14024 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179

This theorem is referenced by: rlimdiv 15588 divcn 24375 gg-divcn 35151 climrec 44305

W3C validator