Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11266 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | binomcxp.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | | peano2cn 10087 |
. . . . . . 7
⊢ (𝐶 ∈ ℂ → (𝐶 + 1) ∈
ℂ) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐶 + 1) ∈ ℂ) |
6 | | 1zzd 11285 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
7 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
8 | 7 | mptex 6390 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) ∈
V |
9 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∈ V) |
10 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))) |
11 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥) |
12 | 11 | oveq1d 6564 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (𝑘 + 1) = (𝑥 + 1)) |
13 | 12 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 + 1) / (𝑘 + 1)) = ((𝐶 + 1) / (𝑥 + 1))) |
14 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
15 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐶 + 1) / (𝑥 + 1)) ∈ V |
16 | 15 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ V) |
17 | 10, 13, 14, 16 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝐶 + 1) / (𝑥 + 1))) |
18 | 1, 2, 5, 6, 9, 17 | divcnvshft 14426 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ⇝ 0) |
19 | | ovex 6577 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))
∘𝑓 − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) ∈ V |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘𝑓 −
(𝑘 ∈
ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) ∈ V) |
21 | | nn0cn 11179 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
22 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 1 ∈ ℂ) |
23 | 21, 22 | addcld 9938 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℂ) |
24 | | nn0p1nn 11209 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
25 | 24 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ≠
0) |
26 | 23, 25 | dividd 10678 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ ((𝑘 + 1) / (𝑘 + 1)) = 1) |
27 | 26 | mpteq2ia 4668 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦
1) |
28 | | fconstmpt 5085 |
. . . . . . . 8
⊢
(ℕ0 × {1}) = (𝑘 ∈ ℕ0 ↦
1) |
29 | 27, 28 | eqtr4i 2635 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (ℕ0
× {1}) |
30 | | ax-1cn 9873 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
31 | | 0z 11265 |
. . . . . . . 8
⊢ 0 ∈
ℤ |
32 | 1 | eqimss2i 3623 |
. . . . . . . . 9
⊢
(ℤ≥‘0) ⊆
ℕ0 |
33 | 32, 7 | climconst2 14127 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 0 ∈ ℤ) → (ℕ0 × {1})
⇝ 1) |
34 | 30, 31, 33 | mp2an 704 |
. . . . . . 7
⊢
(ℕ0 × {1}) ⇝ 1 |
35 | 29, 34 | eqbrtri 4604 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝
1 |
36 | 35 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝ 1) |
37 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝐶 ∈
ℂ) |
38 | | 1cnd 9935 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 1 ∈
ℂ) |
39 | 37, 38 | addcld 9938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 + 1) ∈
ℂ) |
40 | 14 | nn0cnd 11230 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℂ) |
41 | 40, 38 | addcld 9938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ∈
ℂ) |
42 | | nn0p1nn 11209 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0
→ (𝑥 + 1) ∈
ℕ) |
43 | 42 | nnne0d 10942 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0
→ (𝑥 + 1) ≠
0) |
44 | 43 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ≠ 0) |
45 | 39, 41, 44 | divcld 10680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ ℂ) |
46 | 17, 45 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ) |
47 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) |
48 | 12, 12 | oveq12d 6567 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝑘 + 1) / (𝑘 + 1)) = ((𝑥 + 1) / (𝑥 + 1))) |
49 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑥 + 1) / (𝑥 + 1)) ∈ V |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ V) |
51 | 47, 48, 14, 50 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑥 + 1) / (𝑥 + 1))) |
52 | 41, 41, 44 | divcld 10680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ ℂ) |
53 | 51, 52 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ) |
54 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝐶 + 1) / (𝑘 + 1)) ∈ V |
55 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) |
56 | 54, 55 | fnmpti 5935 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1))) Fn
ℕ0 |
57 | 56 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) Fn
ℕ0) |
58 | | ovex 6577 |
. . . . . . . 8
⊢ ((𝑘 + 1) / (𝑘 + 1)) ∈ V |
59 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) |
60 | 58, 59 | fnmpti 5935 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1))) Fn
ℕ0 |
61 | 60 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) Fn
ℕ0) |
62 | 7 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ0 ∈
V) |
63 | | inidm 3784 |
. . . . . 6
⊢
(ℕ0 ∩ ℕ0) =
ℕ0 |
64 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥)) |
65 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥)) |
66 | 57, 61, 62, 62, 63, 64, 65 | ofval 6804 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ ((𝐶 + 1) / (𝑘 + 1)))
∘𝑓 − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))))‘𝑥) = (((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) − ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥))) |
67 | 1, 2, 18, 20, 36, 46, 53, 66 | climsub 14212 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘𝑓 −
(𝑘 ∈
ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) ⇝ (0 −
1)) |
68 | 54 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) / (𝑘 + 1)) ∈ V) |
69 | 58 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + 1)) ∈ V) |
70 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))) |
71 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) |
72 | 62, 68, 69, 70, 71 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘𝑓 −
(𝑘 ∈
ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))))) |
73 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶 + 1) ∈
ℂ) |
74 | 23 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℂ) |
75 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ≠ 0) |
76 | 73, 74, 74, 75 | divsubdird 10719 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))) |
77 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) |
78 | 21 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) |
79 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℂ) |
80 | 77, 78, 79 | pnpcan2d 10309 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) − (𝑘 + 1)) = (𝐶 − 𝑘)) |
81 | 80 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = ((𝐶 − 𝑘) / (𝑘 + 1))) |
82 | 76, 81 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))) = ((𝐶 − 𝑘) / (𝑘 + 1))) |
83 | 82 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) |
84 | 72, 83 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘𝑓 −
(𝑘 ∈
ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) |
85 | | df-neg 10148 |
. . . . . 6
⊢ -1 = (0
− 1) |
86 | 85 | eqcomi 2619 |
. . . . 5
⊢ (0
− 1) = -1 |
87 | 86 | a1i 11 |
. . . 4
⊢ (𝜑 → (0 − 1) =
-1) |
88 | 67, 84, 87 | 3brtr3d 4614 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))) ⇝ -1) |
89 | 7 | mptex 6390 |
. . . 4
⊢ (𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1)))) ∈
V |
90 | 89 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ∈ V) |
91 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))) |
92 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → (𝐶 − 𝑘) = (𝐶 − 𝑥)) |
93 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) |
94 | 92, 93 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑥 → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1))) |
95 | 94 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1))) |
96 | | ovex 6577 |
. . . . . 6
⊢ ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ V |
97 | 96 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ V) |
98 | 91, 95, 14, 97 | fvmptd 6197 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) = ((𝐶 − 𝑥) / (𝑥 + 1))) |
99 | 37, 40 | subcld 10271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 − 𝑥) ∈ ℂ) |
100 | 99, 41, 44 | divcld 10680 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ ℂ) |
101 | 98, 100 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) ∈ ℂ) |
102 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1))))) |
103 | 94 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑥 → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) |
104 | 103 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) |
105 | | fvex 6113 |
. . . . . 6
⊢
(abs‘((𝐶
− 𝑥) / (𝑥 + 1))) ∈
V |
106 | 105 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(abs‘((𝐶 −
𝑥) / (𝑥 + 1))) ∈ V) |
107 | 102, 104,
14, 106 | fvmptd 6197 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) |
108 | 98 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) →
(abs‘((𝑘 ∈
ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥)) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1)))) |
109 | 107, 108 | eqtr4d 2647 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝑘 ∈ ℕ0
↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥))) |
110 | 1, 88, 90, 2, 101, 109 | climabs 14182 |
. 2
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ⇝
(abs‘-1)) |
111 | 30 | absnegi 13987 |
. . 3
⊢
(abs‘-1) = (abs‘1) |
112 | | abs1 13885 |
. . 3
⊢
(abs‘1) = 1 |
113 | 111, 112 | eqtri 2632 |
. 2
⊢
(abs‘-1) = 1 |
114 | 110, 113 | syl6breq 4624 |
1
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ⇝ 1) |