# Metamath Proof Explorer

## Theorem climrec

Description: Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climrec.1 $⊢ Z = ℤ ≥ M$
climrec.2 $⊢ φ → M ∈ ℤ$
climrec.3 $⊢ φ → G ⇝ A$
climrec.4 $⊢ φ → A ≠ 0$
climrec.5 $⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ ∖ 0$
climrec.6 $⊢ φ ∧ k ∈ Z → H ⁡ k = 1 G ⁡ k$
climrec.7 $⊢ φ → H ∈ W$
Assertion climrec $⊢ φ → H ⇝ 1 A$

### Proof

Step Hyp Ref Expression
1 climrec.1 $⊢ Z = ℤ ≥ M$
2 climrec.2 $⊢ φ → M ∈ ℤ$
3 climrec.3 $⊢ φ → G ⇝ A$
4 climrec.4 $⊢ φ → A ≠ 0$
5 climrec.5 $⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ ∖ 0$
6 climrec.6 $⊢ φ ∧ k ∈ Z → H ⁡ k = 1 G ⁡ k$
7 climrec.7 $⊢ φ → H ∈ W$
8 climcl $⊢ G ⇝ A → A ∈ ℂ$
9 3 8 syl $⊢ φ → A ∈ ℂ$
10 4 neneqd $⊢ φ → ¬ A = 0$
11 c0ex $⊢ 0 ∈ V$
12 11 elsn2 $⊢ A ∈ 0 ↔ A = 0$
13 10 12 sylnibr $⊢ φ → ¬ A ∈ 0$
14 9 13 eldifd $⊢ φ → A ∈ ℂ ∖ 0$
15 eqidd $⊢ φ ∧ z ∈ ℂ ∖ 0 → w ∈ ℂ ∖ 0 ⟼ 1 w = w ∈ ℂ ∖ 0 ⟼ 1 w$
16 simpr $⊢ φ ∧ z ∈ ℂ ∖ 0 ∧ w = z → w = z$
17 16 oveq2d $⊢ φ ∧ z ∈ ℂ ∖ 0 ∧ w = z → 1 w = 1 z$
18 simpr $⊢ φ ∧ z ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0$
19 18 eldifad $⊢ φ ∧ z ∈ ℂ ∖ 0 → z ∈ ℂ$
20 eldifsni $⊢ z ∈ ℂ ∖ 0 → z ≠ 0$
21 20 adantl $⊢ φ ∧ z ∈ ℂ ∖ 0 → z ≠ 0$
22 19 21 reccld $⊢ φ ∧ z ∈ ℂ ∖ 0 → 1 z ∈ ℂ$
23 15 17 18 22 fvmptd $⊢ φ ∧ z ∈ ℂ ∖ 0 → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z = 1 z$
24 23 22 eqeltrd $⊢ φ ∧ z ∈ ℂ ∖ 0 → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z ∈ ℂ$
25 eqid $⊢ if 1 ≤ A ⁢ x 1 A ⁢ x ⁢ A 2 = if 1 ≤ A ⁢ x 1 A ⁢ x ⁢ A 2$
26 25 reccn2 $⊢ A ∈ ℂ ∖ 0 ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ ∖ 0 z − A < y → 1 z − 1 A < x$
27 14 26 sylan $⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ ∖ 0 z − A < y → 1 z − 1 A < x$
28 eqidd $⊢ z ∈ ℂ ∖ 0 → w ∈ ℂ ∖ 0 ⟼ 1 w = w ∈ ℂ ∖ 0 ⟼ 1 w$
29 simpr $⊢ z ∈ ℂ ∖ 0 ∧ w = z → w = z$
30 29 oveq2d $⊢ z ∈ ℂ ∖ 0 ∧ w = z → 1 w = 1 z$
31 id $⊢ z ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0$
32 eldifi $⊢ z ∈ ℂ ∖ 0 → z ∈ ℂ$
33 32 20 reccld $⊢ z ∈ ℂ ∖ 0 → 1 z ∈ ℂ$
34 28 30 31 33 fvmptd $⊢ z ∈ ℂ ∖ 0 → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z = 1 z$
35 34 ad2antlr $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z = 1 z$
36 eqidd $⊢ φ → w ∈ ℂ ∖ 0 ⟼ 1 w = w ∈ ℂ ∖ 0 ⟼ 1 w$
37 simpr $⊢ φ ∧ w = A → w = A$
38 37 oveq2d $⊢ φ ∧ w = A → 1 w = 1 A$
39 9 4 reccld $⊢ φ → 1 A ∈ ℂ$
40 36 38 14 39 fvmptd $⊢ φ → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A = 1 A$
41 40 ad4antr $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A = 1 A$
42 35 41 oveq12d $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A = 1 z − 1 A$
43 42 fveq2d $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A = 1 z − 1 A$
44 31 ad2antlr $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → z ∈ ℂ ∖ 0$
45 simpr $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → z − A < y$
46 simpllr $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x$
47 44 45 46 mp2d $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → 1 z − 1 A < x$
48 43 47 eqbrtrd $⊢ φ ∧ x ∈ ℝ + ∧ z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x ∧ z ∈ ℂ ∖ 0 ∧ z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A < x$
49 48 exp41 $⊢ φ ∧ x ∈ ℝ + → z ∈ ℂ ∖ 0 → z − A < y → 1 z − 1 A < x → z ∈ ℂ ∖ 0 → z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A < x$
50 49 ralimdv2 $⊢ φ ∧ x ∈ ℝ + → ∀ z ∈ ℂ ∖ 0 z − A < y → 1 z − 1 A < x → ∀ z ∈ ℂ ∖ 0 z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A < x$
51 50 reximdv $⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ ∖ 0 z − A < y → 1 z − 1 A < x → ∃ y ∈ ℝ + ∀ z ∈ ℂ ∖ 0 z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A < x$
52 27 51 mpd $⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ ∖ 0 z − A < y → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ z − w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A < x$
53 eqidd $⊢ φ ∧ k ∈ Z → w ∈ ℂ ∖ 0 ⟼ 1 w = w ∈ ℂ ∖ 0 ⟼ 1 w$
54 oveq2 $⊢ w = G ⁡ k → 1 w = 1 G ⁡ k$
55 54 adantl $⊢ φ ∧ k ∈ Z ∧ w = G ⁡ k → 1 w = 1 G ⁡ k$
56 5 eldifad $⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℂ$
57 eldifsni $⊢ G ⁡ k ∈ ℂ ∖ 0 → G ⁡ k ≠ 0$
58 5 57 syl $⊢ φ ∧ k ∈ Z → G ⁡ k ≠ 0$
59 56 58 reccld $⊢ φ ∧ k ∈ Z → 1 G ⁡ k ∈ ℂ$
60 53 55 5 59 fvmptd $⊢ φ ∧ k ∈ Z → w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ G ⁡ k = 1 G ⁡ k$
61 6 60 eqtr4d $⊢ φ ∧ k ∈ Z → H ⁡ k = w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ G ⁡ k$
62 1 2 14 24 3 7 52 5 61 climcn1 $⊢ φ → H ⇝ w ∈ ℂ ∖ 0 ⟼ 1 w ⁡ A$
63 62 40 breqtrd $⊢ φ → H ⇝ 1 A$