Theorem divrcnv

Description: The sequence of reciprocals of real numbers, multiplied by the factor A , converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014)

	Ref	Expression
Assertion	divrcnv	$$⊢A\in ℂ\to \left(n\in {ℝ}^{+}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0$$

Proof

Step	Hyp	Ref	Expression
1		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
2		rerpdivcl	$$⊢\left(\left|A\right|\in ℝ\wedge x\in {ℝ}^{+}\right)\to \frac{\left|A\right|}{x}\in ℝ$$
3	1 2	sylan	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \frac{\left|A\right|}{x}\in ℝ$$
4		simpll	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to A\in ℂ$$
5		rpcn	$$⊢n\in {ℝ}^{+}\to n\in ℂ$$
6	5	ad2antrl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to n\in ℂ$$
7		rpne0	$$⊢n\in {ℝ}^{+}\to n\ne 0$$
8	7	ad2antrl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to n\ne 0$$
9	4 6 8	absdivd	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left|\frac{A}{n}\right|=\frac{\left|A\right|}{\left|n\right|}$$
10		rpre	$$⊢n\in {ℝ}^{+}\to n\in ℝ$$
11	10	ad2antrl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to n\in ℝ$$
12		rpge0	$$⊢n\in {ℝ}^{+}\to 0\le n$$
13	12	ad2antrl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to 0\le n$$
14	11 13	absidd	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left|n\right|=n$$
15	14	oveq2d	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \frac{\left|A\right|}{\left|n\right|}=\frac{\left|A\right|}{n}$$
16	9 15	eqtrd	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left|\frac{A}{n}\right|=\frac{\left|A\right|}{n}$$
17		simprr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \frac{\left|A\right|}{x}<n$$
18	4	abscld	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left|A\right|\in ℝ$$
19		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
20	19	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to x\in ℝ$$
21		rpgt0	$$⊢x\in {ℝ}^{+}\to 0<x$$
22	21	ad2antlr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to 0<x$$
23		rpgt0	$$⊢n\in {ℝ}^{+}\to 0<n$$
24	23	ad2antrl	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to 0<n$$
25		ltdiv23	$$⊢\left(\left|A\right|\in ℝ\wedge \left(x\in ℝ\wedge 0<x\right)\wedge \left(n\in ℝ\wedge 0<n\right)\right)\to \left(\frac{\left|A\right|}{x}<n\leftrightarrow \frac{\left|A\right|}{n}<x\right)$$
26	18 20 22 11 24 25	syl122anc	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left(\frac{\left|A\right|}{x}<n\leftrightarrow \frac{\left|A\right|}{n}<x\right)$$
27	17 26	mpbid	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \frac{\left|A\right|}{n}<x$$
28	16 27	eqbrtrd	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge \frac{\left|A\right|}{x}<n\right)\right)\to \left|\frac{A}{n}\right|<x$$
29	28	expr	$$⊢\left(\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\wedge n\in {ℝ}^{+}\right)\to \left(\frac{\left|A\right|}{x}<n\to \left|\frac{A}{n}\right|<x\right)$$
30	29	ralrimiva	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \forall n\in {ℝ}^{+}\left(\frac{\left|A\right|}{x}<n\to \left|\frac{A}{n}\right|<x\right)$$
31		breq1	$$⊢y=\frac{\left|A\right|}{x}\to \left(y<n\leftrightarrow \frac{\left|A\right|}{x}<n\right)$$
32	31	rspceaimv	$$⊢\left(\frac{\left|A\right|}{x}\in ℝ\wedge \forall n\in {ℝ}^{+}\left(\frac{\left|A\right|}{x}<n\to \left|\frac{A}{n}\right|<x\right)\right)\to \exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{A}{n}\right|<x\right)$$
33	3 30 32	syl2anc	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{A}{n}\right|<x\right)$$
34	33	ralrimiva	$$⊢A\in ℂ\to \forall x\in {ℝ}^{+}\exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{A}{n}\right|<x\right)$$
35		simpl	$$⊢\left(A\in ℂ\wedge n\in {ℝ}^{+}\right)\to A\in ℂ$$
36	5	adantl	$$⊢\left(A\in ℂ\wedge n\in {ℝ}^{+}\right)\to n\in ℂ$$
37	7	adantl	$$⊢\left(A\in ℂ\wedge n\in {ℝ}^{+}\right)\to n\ne 0$$
38	35 36 37	divcld	$$⊢\left(A\in ℂ\wedge n\in {ℝ}^{+}\right)\to \frac{A}{n}\in ℂ$$
39	38	ralrimiva	$$⊢A\in ℂ\to \forall n\in {ℝ}^{+}\frac{A}{n}\in ℂ$$
40		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
41	40	a1i	$$⊢A\in ℂ\to {ℝ}^{+}\subseteq ℝ$$
42	39 41	rlim0lt	$$⊢A\in ℂ\to \left(\left(n\in {ℝ}^{+}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0\leftrightarrow \forall x\in {ℝ}^{+}\exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{A}{n}\right|<x\right)\right)$$
43	34 42	mpbird	$$⊢A\in ℂ\to \left(n\in {ℝ}^{+}⟼\frac{A}{n}\right)\underset{ℝ}{⇝}0$$