| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0uz 12920 | . . 3
⊢
ℕ0 = (ℤ≥‘0) | 
| 2 |  | 0zd 12625 | . . . . 5
⊢ (𝜑 → 0 ∈
ℤ) | 
| 3 |  | binomcxp.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 4 |  | peano2cn 11433 | . . . . . . 7
⊢ (𝐶 ∈ ℂ → (𝐶 + 1) ∈
ℂ) | 
| 5 | 3, 4 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐶 + 1) ∈ ℂ) | 
| 6 |  | 1zzd 12648 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) | 
| 7 |  | nn0ex 12532 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 8 | 7 | mptex 7243 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) ∈
V | 
| 9 | 8 | a1i 11 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∈ V) | 
| 10 |  | eqidd 2738 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))) | 
| 11 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥) | 
| 12 | 11 | oveq1d 7446 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (𝑘 + 1) = (𝑥 + 1)) | 
| 13 | 12 | oveq2d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 + 1) / (𝑘 + 1)) = ((𝐶 + 1) / (𝑥 + 1))) | 
| 14 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) | 
| 15 |  | ovexd 7466 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ V) | 
| 16 | 10, 13, 14, 15 | fvmptd 7023 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝐶 + 1) / (𝑥 + 1))) | 
| 17 | 1, 2, 5, 6, 9, 16 | divcnvshft 15891 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ⇝ 0) | 
| 18 |  | ovexd 7466 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))) ∈
V) | 
| 19 |  | nn0cn 12536 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 20 |  | 1cnd 11256 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℂ) | 
| 21 | 19, 20 | addcld 11280 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) | 
| 22 |  | nn0p1nn 12565 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) | 
| 23 | 22 | nnne0d 12316 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ≠
0) | 
| 24 | 21, 23 | dividd 12041 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 + 1) / (𝑘 + 1)) = 1) | 
| 25 | 24 | mpteq2ia 5245 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦
1) | 
| 26 |  | fconstmpt 5747 | . . . . . . . 8
⊢
(ℕ0 × {1}) = (𝑘 ∈ ℕ0 ↦
1) | 
| 27 | 25, 26 | eqtr4i 2768 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (ℕ0
× {1}) | 
| 28 |  | ax-1cn 11213 | . . . . . . . 8
⊢ 1 ∈
ℂ | 
| 29 |  | 0z 12624 | . . . . . . . 8
⊢ 0 ∈
ℤ | 
| 30 | 1 | eqimss2i 4045 | . . . . . . . . 9
⊢
(ℤ≥‘0) ⊆
ℕ0 | 
| 31 | 30, 7 | climconst2 15584 | . . . . . . . 8
⊢ ((1
∈ ℂ ∧ 0 ∈ ℤ) → (ℕ0 × {1})
⇝ 1) | 
| 32 | 28, 29, 31 | mp2an 692 | . . . . . . 7
⊢
(ℕ0 × {1}) ⇝ 1 | 
| 33 | 27, 32 | eqbrtri 5164 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝
1 | 
| 34 | 33 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝ 1) | 
| 35 | 3 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝐶 ∈
ℂ) | 
| 36 |  | 1cnd 11256 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 1 ∈
ℂ) | 
| 37 | 35, 36 | addcld 11280 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 + 1) ∈
ℂ) | 
| 38 | 14 | nn0cnd 12589 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℂ) | 
| 39 | 38, 36 | addcld 11280 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ∈
ℂ) | 
| 40 |  | nn0p1nn 12565 | . . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ (𝑥 + 1) ∈
ℕ) | 
| 41 | 40 | nnne0d 12316 | . . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ (𝑥 + 1) ≠
0) | 
| 42 | 41 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ≠ 0) | 
| 43 | 37, 39, 42 | divcld 12043 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ ℂ) | 
| 44 | 16, 43 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ) | 
| 45 |  | eqidd 2738 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) | 
| 46 | 12, 12 | oveq12d 7449 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝑘 + 1) / (𝑘 + 1)) = ((𝑥 + 1) / (𝑥 + 1))) | 
| 47 |  | ovexd 7466 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ V) | 
| 48 | 45, 46, 14, 47 | fvmptd 7023 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑥 + 1) / (𝑥 + 1))) | 
| 49 | 39, 39, 42 | divcld 12043 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ ℂ) | 
| 50 | 48, 49 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ) | 
| 51 |  | ovex 7464 | . . . . . . . 8
⊢ ((𝐶 + 1) / (𝑘 + 1)) ∈ V | 
| 52 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) | 
| 53 | 51, 52 | fnmpti 6711 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) Fn
ℕ0 | 
| 54 | 53 | a1i 11 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) Fn
ℕ0) | 
| 55 |  | ovex 7464 | . . . . . . . 8
⊢ ((𝑘 + 1) / (𝑘 + 1)) ∈ V | 
| 56 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) | 
| 57 | 55, 56 | fnmpti 6711 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) Fn
ℕ0 | 
| 58 | 57 | a1i 11 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) Fn
ℕ0) | 
| 59 | 7 | a1i 11 | . . . . . 6
⊢ (𝜑 → ℕ0 ∈
V) | 
| 60 |  | inidm 4227 | . . . . . 6
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 | 
| 61 |  | eqidd 2738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥)) | 
| 62 |  | eqidd 2738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥)) | 
| 63 | 54, 58, 59, 59, 60, 61, 62 | ofval 7708 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f
− (𝑘 ∈
ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))))‘𝑥) = (((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) − ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥))) | 
| 64 | 1, 2, 17, 18, 34, 44, 50, 63 | climsub 15670 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))) ⇝ (0 −
1)) | 
| 65 |  | ovexd 7466 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) / (𝑘 + 1)) ∈ V) | 
| 66 |  | ovexd 7466 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + 1)) ∈ V) | 
| 67 |  | eqidd 2738 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))) | 
| 68 |  | eqidd 2738 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) | 
| 69 | 59, 65, 66, 67, 68 | offval2 7717 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))))) | 
| 70 | 5 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶 + 1) ∈
ℂ) | 
| 71 | 21 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℂ) | 
| 72 | 23 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ≠ 0) | 
| 73 | 70, 71, 71, 72 | divsubdird 12082 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))) | 
| 74 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) | 
| 75 | 19 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) | 
| 76 |  | 1cnd 11256 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℂ) | 
| 77 | 74, 75, 76 | pnpcan2d 11658 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) − (𝑘 + 1)) = (𝐶 − 𝑘)) | 
| 78 | 77 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = ((𝐶 − 𝑘) / (𝑘 + 1))) | 
| 79 | 73, 78 | eqtr3d 2779 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))) = ((𝐶 − 𝑘) / (𝑘 + 1))) | 
| 80 | 79 | mpteq2dva 5242 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) | 
| 81 | 69, 80 | eqtrd 2777 | . . . 4
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) | 
| 82 |  | df-neg 11495 | . . . . . 6
⊢ -1 = (0
− 1) | 
| 83 | 82 | eqcomi 2746 | . . . . 5
⊢ (0
− 1) = -1 | 
| 84 | 83 | a1i 11 | . . . 4
⊢ (𝜑 → (0 − 1) =
-1) | 
| 85 | 64, 81, 84 | 3brtr3d 5174 | . . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))) ⇝ -1) | 
| 86 | 7 | mptex 7243 | . . . 4
⊢ (𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1)))) ∈
V | 
| 87 | 86 | a1i 11 | . . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ∈ V) | 
| 88 |  | eqidd 2738 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) | 
| 89 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = 𝑥 → (𝐶 − 𝑘) = (𝐶 − 𝑥)) | 
| 90 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) | 
| 91 | 89, 90 | oveq12d 7449 | . . . . . 6
⊢ (𝑘 = 𝑥 → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1))) | 
| 92 | 91 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1))) | 
| 93 |  | ovexd 7466 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ V) | 
| 94 | 88, 92, 14, 93 | fvmptd 7023 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) = ((𝐶 − 𝑥) / (𝑥 + 1))) | 
| 95 | 35, 38 | subcld 11620 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 − 𝑥) ∈ ℂ) | 
| 96 | 95, 39, 42 | divcld 12043 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ ℂ) | 
| 97 | 94, 96 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) ∈ ℂ) | 
| 98 |  | eqidd 2738 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1))))) | 
| 99 | 91 | fveq2d 6910 | . . . . . 6
⊢ (𝑘 = 𝑥 → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) | 
| 100 | 99 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) | 
| 101 |  | fvexd 6921 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(abs‘((𝐶 −
𝑥) / (𝑥 + 1))) ∈ V) | 
| 102 | 98, 100, 14, 101 | fvmptd 7023 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) | 
| 103 | 94 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(abs‘((𝑘 ∈
ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥)) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) | 
| 104 | 102, 103 | eqtr4d 2780 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥))) | 
| 105 | 1, 85, 87, 2, 97, 104 | climabs 15640 | . 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ⇝
(abs‘-1)) | 
| 106 | 28 | absnegi 15439 | . . 3
⊢
(abs‘-1) = (abs‘1) | 
| 107 |  | abs1 15336 | . . 3
⊢
(abs‘1) = 1 | 
| 108 | 106, 107 | eqtri 2765 | . 2
⊢
(abs‘-1) = 1 | 
| 109 | 105, 108 | breqtrdi 5184 | 1
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ⇝ 1) |