This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )