Metamath Proof Explorer

Theorem binomcxplemrat

Description: Lemma for binomcxp . As k increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion binomcxplemrat ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ⇝ 1 )

Proof

Step Hyp Ref Expression
1 binomcxp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 binomcxp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 binomcxp.lt ⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4 binomcxp.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
7 peano2cn ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 + 1 ) ∈ ℂ )
8 4 7 syl ⊢ ( 𝜑 → ( 𝐶 + 1 ) ∈ ℂ )
9 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
10 nn0ex ⊢ ℕ0 ∈ V
11 10 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∈ V
12 11 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∈ V )
13 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) )
14 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → 𝑘 = 𝑥 )
15 14 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → ( 𝑘 + 1 ) = ( 𝑥 + 1 ) )
16 15 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) = ( ( 𝐶 + 1 ) / ( 𝑥 + 1 ) ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
18 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) / ( 𝑥 + 1 ) ) ∈ V )
19 13 16 17 18 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝐶 + 1 ) / ( 𝑥 + 1 ) ) )
20 5 6 8 9 12 19 divcnvshft ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ⇝ 0 )
21 ovexd ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∘f − ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) ∈ V )
22 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
23 1cnd ⊢ ( 𝑘 ∈ ℕ0 → 1 ∈ ℂ )
24 22 23 addcld ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℂ )
25 nn0p1nn ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
26 25 nnne0d ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ≠ 0 )
27 24 26 dividd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) = 1 )
28 27 mpteq2ia ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ 1 )
29 fconstmpt ⊢ ( ℕ0 × { 1 } ) = ( 𝑘 ∈ ℕ0 ↦ 1 )
30 28 29 eqtr4i ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( ℕ0 × { 1 } )
31 ax-1cn ⊢ 1 ∈ ℂ
32 0z ⊢ 0 ∈ ℤ
33 5 eqimss2i ⊢ ( ℤ≥ ‘ 0 ) ⊆ ℕ0
34 33 10 climconst2 ⊢ ( ( 1 ∈ ℂ ∧ 0 ∈ ℤ ) → ( ℕ0 × { 1 } ) ⇝ 1 )
35 31 32 34 mp2an ⊢ ( ℕ0 × { 1 } ) ⇝ 1
36 30 35 eqbrtri ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ⇝ 1
37 36 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ⇝ 1 )
38 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
39 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → 1 ∈ ℂ )
40 38 39 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝐶 + 1 ) ∈ ℂ )
41 17 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℂ )
42 41 39 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 + 1 ) ∈ ℂ )
43 nn0p1nn ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 1 ) ∈ ℕ )
44 43 nnne0d ⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 + 1 ) ≠ 0 )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 + 1 ) ≠ 0 )
46 40 42 45 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) / ( 𝑥 + 1 ) ) ∈ ℂ )
47 19 46 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ∈ ℂ )
48 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) )
49 15 15 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) = ( ( 𝑥 + 1 ) / ( 𝑥 + 1 ) ) )
50 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 + 1 ) / ( 𝑥 + 1 ) ) ∈ V )
51 48 49 17 50 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 + 1 ) / ( 𝑥 + 1 ) ) )
52 42 42 45 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 + 1 ) / ( 𝑥 + 1 ) ) ∈ ℂ )
53 51 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ∈ ℂ )
54 ovex ⊢ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ∈ V
55 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) )
56 54 55 fnmpti ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) Fn ℕ0
57 56 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) Fn ℕ0 )
58 ovex ⊢ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ∈ V
59 eqid ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) )
60 58 59 fnmpti ⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) Fn ℕ0
61 60 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) Fn ℕ0 )
62 10 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
63 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
64 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) )
65 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) )
66 57 61 62 62 63 64 65 ofval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∘f − ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) − ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ) )
67 5 6 20 21 37 47 53 66 climsub ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∘f − ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) ⇝ ( 0 − 1 ) )
68 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ∈ V )
69 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ∈ V )
70 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) )
71 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) )
72 62 68 69 70 71 offval2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∘f − ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) − ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) )
73 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 + 1 ) ∈ ℂ )
74 24 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℂ )
75 26 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ≠ 0 )
76 73 74 74 75 divsubdird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 + 1 ) − ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) = ( ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) − ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) )
77 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
78 22 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
79 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
80 77 78 79 pnpcan2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) − ( 𝑘 + 1 ) ) = ( 𝐶 − 𝑘 ) )
81 80 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 + 1 ) − ( 𝑘 + 1 ) ) / ( 𝑘 + 1 ) ) = ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) )
82 76 81 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) − ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) = ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) )
83 82 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) − ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
84 72 83 eqtrd ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 + 1 ) / ( 𝑘 + 1 ) ) ) ∘f − ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) / ( 𝑘 + 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
85 df-neg ⊢ - 1 = ( 0 − 1 )
86 85 eqcomi ⊢ ( 0 − 1 ) = - 1
87 86 a1i ⊢ ( 𝜑 → ( 0 − 1 ) = - 1 )
88 67 84 87 3brtr3d ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ⇝ - 1 )
89 10 mptex ⊢ ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ∈ V
90 89 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ∈ V )
91 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
92 oveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝐶 − 𝑘 ) = ( 𝐶 − 𝑥 ) )
93 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 + 1 ) = ( 𝑥 + 1 ) )
94 92 93 oveq12d ⊢ ( 𝑘 = 𝑥 → ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) = ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) )
95 94 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) = ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) )
96 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ∈ V )
97 91 95 17 96 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) = ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) )
98 38 41 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝐶 − 𝑥 ) ∈ ℂ )
99 98 42 45 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ∈ ℂ )
100 97 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ∈ ℂ )
101 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) )
102 94 fveq2d ⊢ ( 𝑘 = 𝑥 → ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( abs ‘ ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ) )
103 102 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) ∧ 𝑘 = 𝑥 ) → ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( abs ‘ ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ) )
104 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ) ∈ V )
105 101 103 17 104 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ‘ 𝑥 ) = ( abs ‘ ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ) )
106 97 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( ( 𝐶 − 𝑥 ) / ( 𝑥 + 1 ) ) ) )
107 105 106 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ‘ 𝑥 ) = ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ‘ 𝑥 ) ) )
108 5 88 90 6 100 107 climabs ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ⇝ ( abs ‘ - 1 ) )
109 31 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
110 abs1 ⊢ ( abs ‘ 1 ) = 1
111 109 110 eqtri ⊢ ( abs ‘ - 1 ) = 1
112 108 111 breqtrdi ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ⇝ 1 )