Theorem binomcxplemrat 44926

Description: Lemma for binomcxp 44933. As 𝑘 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.)

Hypotheses

Ref	Expression
binomcxp.a	⊢ (𝜑 → 𝐴 ∈ ℝ+)
binomcxp.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
binomcxp.lt	⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴))
binomcxp.c	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
binomcxplemrat	⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ 1)

Distinct variable groups:   𝜑,𝑘   𝐶,𝑘

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Proof of Theorem binomcxplemrat

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 12877	. . 3 ⊢ ℕ0 = (ℤ≥‘0)
2		0zd 12580	. . . . 5 ⊢ (𝜑 → 0 ∈ ℤ)
3		binomcxp.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		peano2cn 11355	. . . . . . 7 ⊢ (𝐶 ∈ ℂ → (𝐶 + 1) ∈ ℂ)
5	3, 4	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐶 + 1) ∈ ℂ)
6		1zzd 12602	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
7		nn0ex 12487	. . . . . . . 8 ⊢ ℕ0 ∈ V
8	7	mptex 7207	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∈ V
9	8	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∈ V)
10		eqidd 2763	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))))
11		simpr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → 𝑘 = 𝑥)
12	11	oveq1d 7411	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (𝑘 + 1) = (𝑥 + 1))
13	12	oveq2d 7412	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 + 1) / (𝑘 + 1)) = ((𝐶 + 1) / (𝑥 + 1)))
14		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℕ0)
15		ovexd 7431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ V)
16	10, 13, 14, 15	fvmptd 6983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝐶 + 1) / (𝑥 + 1)))
17	1, 2, 5, 6, 9, 16	divcnvshft 15885	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ⇝ 0)
18		ovexd 7431	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) ∈ V)
19		nn0cn 12491	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ)
20		1cnd 11175	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → 1 ∈ ℂ)
21	19, 20	addcld 11201	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℂ)
22		nn0p1nn 12520	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ)
23	22	nnne0d 12263	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ≠ 0)
24	21, 23	dividd 11965	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → ((𝑘 + 1) / (𝑘 + 1)) = 1)
25	24	mpteq2ia 5195	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ 1)
26		fconstmpt 5709	. . . . . . . 8 ⊢ (ℕ0 × {1}) = (𝑘 ∈ ℕ0 ↦ 1)
27	25, 26	eqtr4i 2788	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (ℕ0 × {1})
28		ax-1cn 11131	. . . . . . . 8 ⊢ 1 ∈ ℂ
29		0z 12579	. . . . . . . 8 ⊢ 0 ∈ ℤ
30	1	eqimss2i 3997	. . . . . . . . 9 ⊢ (ℤ≥‘0) ⊆ ℕ0
31	30, 7	climconst2 15575	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ 0 ∈ ℤ) → (ℕ0 × {1}) ⇝ 1)
32	28, 29, 31	mp2an 702	. . . . . . 7 ⊢ (ℕ0 × {1}) ⇝ 1
33	27, 32	eqbrtri 5121	. . . . . 6 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝ 1
34	33	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) ⇝ 1)
35	3	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝐶 ∈ ℂ)
36		1cnd 11175	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 1 ∈ ℂ)
37	35, 36	addcld 11201	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 + 1) ∈ ℂ)
38	14	nn0cnd 12544	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈ ℂ)
39	38, 36	addcld 11201	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ∈ ℂ)
40		nn0p1nn 12520	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ0 → (𝑥 + 1) ∈ ℕ)
41	40	nnne0d 12263	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ0 → (𝑥 + 1) ≠ 0)
42	41	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑥 + 1) ≠ 0)
43	37, 39, 42	divcld 11967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 + 1) / (𝑥 + 1)) ∈ ℂ)
44	16, 43	eqeltrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ)
45		eqidd 2763	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))))
46	12, 12	oveq12d 7414	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝑘 + 1) / (𝑘 + 1)) = ((𝑥 + 1) / (𝑥 + 1)))
47		ovexd 7431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ V)
48	45, 46, 14, 47	fvmptd 6983	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑥 + 1) / (𝑥 + 1)))
49	39, 39, 42	divcld 11967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑥 + 1) / (𝑥 + 1)) ∈ ℂ)
50	48, 49	eqeltrd 2862	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) ∈ ℂ)
51		ovex 7429	. . . . . . . 8 ⊢ ((𝐶 + 1) / (𝑘 + 1)) ∈ V
52		eqid 2762	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))
53	51, 52	fnmpti 6664	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) Fn ℕ0
54	53	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) Fn ℕ0)
55		ovex 7429	. . . . . . . 8 ⊢ ((𝑘 + 1) / (𝑘 + 1)) ∈ V
56		eqid 2762	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))
57	55, 56	fnmpti 6664	. . . . . . 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 4178	. . . . . 6 ⊢ (ℕ0 ∩ ℕ0) = ℕ0
61		eqidd 2763	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1)))‘𝑥))
62		eqidd 2763	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥) = ((𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))‘𝑥))
63	54, 58, 59, 59, 60, 61, 62	ofval 7671	. . . . 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 15661	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) ⇝ (0 − 1))
65		ovexd 7431	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) / (𝑘 + 1)) ∈ V)
66		ovexd 7431	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + 1)) ∈ V)
67		eqidd 2763	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))))
68		eqidd 2763	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1))))
69	59, 65, 66, 67, 68	offval2 7680	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))))
70	5	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶 + 1) ∈ ℂ)
71	21	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
72	23	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ≠ 0)
73	70, 71, 71, 72	divsubdird 12006	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))))
74	3	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
75	19	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
76		1cnd 11175	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℂ)
77	74, 75, 76	pnpcan2d 11580	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐶 + 1) − (𝑘 + 1)) = (𝐶 − 𝑘))
78	77	oveq1d 7411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) − (𝑘 + 1)) / (𝑘 + 1)) = ((𝐶 − 𝑘) / (𝑘 + 1)))
79	73, 78	eqtr3d 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1))) = ((𝐶 − 𝑘) / (𝑘 + 1)))
80	79	mpteq2dva 5193	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (((𝐶 + 1) / (𝑘 + 1)) − ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))))
81	69, 80	eqtrd 2797	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ ((𝐶 + 1) / (𝑘 + 1))) ∘f − (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))))
82		df-neg 11417	. . . . . 6 ⊢ -1 = (0 − 1)
83	82	eqcomi 2771	. . . . 5 ⊢ (0 − 1) = -1
84	83	a1i 11	. . . 4 ⊢ (𝜑 → (0 − 1) = -1)
85	64, 81, 84	3brtr3d 5131	. . 3 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))) ⇝ -1)
86	7	mptex 7207	. . . 4 ⊢ (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ∈ V
87	86	a1i 11	. . 3 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ∈ V)
88		eqidd 2763	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))) = (𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1))))
89		oveq2 7404	. . . . . . 7 ⊢ (𝑘 = 𝑥 → (𝐶 − 𝑘) = (𝐶 − 𝑥))
90		oveq1 7403	. . . . . . 7 ⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1))
91	89, 90	oveq12d 7414	. . . . . 6 ⊢ (𝑘 = 𝑥 → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1)))
92	91	adantl 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → ((𝐶 − 𝑘) / (𝑘 + 1)) = ((𝐶 − 𝑥) / (𝑥 + 1)))
93		ovexd 7431	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ V)
94	88, 92, 14, 93	fvmptd 6983	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) = ((𝐶 − 𝑥) / (𝑥 + 1)))
95	35, 38	subcld 11542	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐶 − 𝑥) ∈ ℂ)
96	95, 39, 42	divcld 11967	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝐶 − 𝑥) / (𝑥 + 1)) ∈ ℂ)
97	94, 96	eqeltrd 2862	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥) ∈ ℂ)
98		eqidd 2763	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))))
99	91	fveq2d 6871	. . . . . 6 ⊢ (𝑘 = 𝑥 → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1))))
100	99	adantl 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℕ0) ∧ 𝑘 = 𝑥) → (abs‘((𝐶 − 𝑘) / (𝑘 + 1))) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1))))
101		fvexd 6882	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (abs‘((𝐶 − 𝑥) / (𝑥 + 1))) ∈ V)
102	98, 100, 14, 101	fvmptd 6983	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1))))
103	94	fveq2d 6871	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (abs‘((𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥)) = (abs‘((𝐶 − 𝑥) / (𝑥 + 1))))
104	102, 103	eqtr4d 2800	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1))))‘𝑥) = (abs‘((𝑘 ∈ ℕ0 ↦ ((𝐶 − 𝑘) / (𝑘 + 1)))‘𝑥)))
105	1, 85, 87, 2, 97, 104	climabs 15631	. 2 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ (abs‘-1))
106	28	absnegi 15428	. . 3 ⊢ (abs‘-1) = (abs‘1)
107		abs1 15324	. . 3 ⊢ (abs‘1) = 1
108	106, 107	eqtri 2785	. 2 ⊢ (abs‘-1) = 1
109	105, 108	breqtrdi 5141	1 ⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) ⇝ 1)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  Vcvv 3454  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   × cxp 5645   Fn wfn 6516  ‘cfv 6521  (class class class)co 7396   ∘_f cof 7658  ℂcc 11071  ℝcr 11072  0cc0 11073  1c1 11074   + caddc 11076   < clt 11216   − cmin 11414  -cneg 11415   / cdiv 11844  ℕ₀cn0 12481  ℤcz 12568  ℤ_≥cuz 12839  ℝ⁺crp 12993  abscabs 15261   ⇝ cli 15511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150  ax-pre-sup 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7660  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-sup 9388  df-inf 9389  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-div 11845  df-nn 12211  df-2 12280  df-3 12281  df-n0 12482  df-z 12569  df-uz 12840  df-rp 12994  df-fl 13802  df-seq 14015  df-exp 14075  df-shft 15080  df-cj 15126  df-re 15127  df-im 15128  df-sqrt 15262  df-abs 15263  df-clim 15515  df-rlim 15516

This theorem is referenced by:  binomcxplemfrat  44927