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	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 )

Proof

Step	Hyp	Ref	Expression
1		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
2		rerpdivcl	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) / 𝑥 ) ∈ ℝ )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ( ( abs ‘ 𝐴 ) / 𝑥 ) ∈ ℝ )
4		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 𝐴 ∈ ℂ )
5		rpcn	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ )
6	5	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 𝑛 ∈ ℂ )
7		rpne0	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≠ 0 )
8	7	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 𝑛 ≠ 0 )
9	4 6 8	absdivd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( abs ‘ ( 𝐴 / 𝑛 ) ) = ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑛 ) ) )
10		rpre	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
11	10	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 𝑛 ∈ ℝ )
12		rpge0	⊢ ( 𝑛 ∈ ℝ+ → 0 ≤ 𝑛 )
13	12	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 0 ≤ 𝑛 )
14	11 13	absidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
15	14	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( ( abs ‘ 𝐴 ) / ( abs ‘ 𝑛 ) ) = ( ( abs ‘ 𝐴 ) / 𝑛 ) )
16	9 15	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( abs ‘ ( 𝐴 / 𝑛 ) ) = ( ( abs ‘ 𝐴 ) / 𝑛 ) )
17		simprr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 )
18	4	abscld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
20	19	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 𝑥 ∈ ℝ )
21		rpgt0	⊢ ( 𝑥 ∈ ℝ+ → 0 < 𝑥 )
22	21	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 0 < 𝑥 )
23		rpgt0	⊢ ( 𝑛 ∈ ℝ+ → 0 < 𝑛 )
24	23	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → 0 < 𝑛 )
25		ltdiv23	⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ↔ ( ( abs ‘ 𝐴 ) / 𝑛 ) < 𝑥 ) )
26	18 20 22 11 24 25	syl122anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ↔ ( ( abs ‘ 𝐴 ) / 𝑛 ) < 𝑥 ) )
27	17 26	mpbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( ( abs ‘ 𝐴 ) / 𝑛 ) < 𝑥 )
28	16 27	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) ) → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 )
29	28	expr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) )
30	29	ralrimiva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ℝ+ ( ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) )
31		breq1	⊢ ( 𝑦 = ( ( abs ‘ 𝐴 ) / 𝑥 ) → ( 𝑦 < 𝑛 ↔ ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 ) )
32	31	rspceaimv	⊢ ( ( ( ( abs ‘ 𝐴 ) / 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ ℝ+ ( ( ( abs ‘ 𝐴 ) / 𝑥 ) < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) )
33	3 30 32	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) )
34	33	ralrimiva	⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) )
35		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
36	5	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℂ )
37	7	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ≠ 0 )
38	35 36 37	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+ ) → ( 𝐴 / 𝑛 ) ∈ ℂ )
39	38	ralrimiva	⊢ ( 𝐴 ∈ ℂ → ∀ 𝑛 ∈ ℝ+ ( 𝐴 / 𝑛 ) ∈ ℂ )
40		rpssre	⊢ ℝ+ ⊆ ℝ
41	40	a1i	⊢ ( 𝐴 ∈ ℂ → ℝ+ ⊆ ℝ )
42	39 41	rlim0lt	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℝ+ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 𝐴 / 𝑛 ) ) < 𝑥 ) ) )
43	34 42	mpbird	⊢ ( 𝐴 ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( 𝐴 / 𝑛 ) ) ⇝𝑟 0 )