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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climrec.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climrec.3 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
climrec.4 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
climrec.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
climrec.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
climrec.7 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
Assertion climrec ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climrec.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climrec.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climrec.3 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
4 climrec.4 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
5 climrec.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
6 climrec.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
7 climrec.7 ⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
8 climcl ⊢ ( 𝐺 ⇝ 𝐴 → 𝐴 ∈ ℂ )
9 3 8 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10 4 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = 0 )
11 c0ex ⊢ 0 ∈ V
12 11 elsn2 ⊢ ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 )
13 10 12 sylnibr ⊢ ( 𝜑 → ¬ 𝐴 ∈ { 0 } )
14 9 13 eldifd ⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
15 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑤 = 𝑧 ) → 𝑤 = 𝑧 )
17 16 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑤 = 𝑧 ) → ( 1 / 𝑤 ) = ( 1 / 𝑧 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
19 18 eldifad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ∈ ℂ )
20 eldifsni ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ≠ 0 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ≠ 0 )
22 19 21 reccld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑧 ) ∈ ℂ )
23 15 17 18 22 fvmptd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
24 23 22 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) ∈ ℂ )
25 eqid ⊢ ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝑥 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝑥 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝑥 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝑥 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) )
26 25 reccn2 ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) )
27 14 26 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) )
28 eqidd ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
29 simpr ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 = 𝑧 ) → 𝑤 = 𝑧 )
30 29 oveq2d ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 = 𝑧 ) → ( 1 / 𝑤 ) = ( 1 / 𝑧 ) )
31 id ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
32 eldifi ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ∈ ℂ )
33 32 20 reccld ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑧 ) ∈ ℂ )
34 28 30 31 33 fvmptd ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
35 34 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
36 eqidd ⊢ ( 𝜑 → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = 𝐴 ) → 𝑤 = 𝐴 )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ 𝑤 = 𝐴 ) → ( 1 / 𝑤 ) = ( 1 / 𝐴 ) )
39 9 4 reccld ⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℂ )
40 36 38 14 39 fvmptd ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
41 40 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
42 35 41 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) = ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) )
43 42 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) )
44 31 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
45 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 )
46 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) )
47 44 45 46 mp2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 )
48 43 47 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 )
49 48 exp41 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) ) )
50 49 ralimdv2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) → ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) )
51 50 reximdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) )
52 27 51 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) )
53 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
54 oveq2 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑘 ) → ( 1 / 𝑤 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 = ( 𝐺 ‘ 𝑘 ) ) → ( 1 / 𝑤 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
56 5 eldifad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
57 eldifsni ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
58 5 57 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
59 56 58 reccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
60 53 55 5 59 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
61 6 60 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ ( 𝐺 ‘ 𝑘 ) ) )
62 1 2 14 24 3 7 52 5 61 climcn1 ⊢ ( 𝜑 → 𝐻 ⇝ ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) )
63 62 40 breqtrd ⊢ ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )