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	$$⊢\phi \to A\in {ℝ}^{+}$$
	binomcxp.b	$$⊢\phi \to B\in ℝ$$
	binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
	binomcxp.c	$$⊢\phi \to C\in ℂ$$
Assertion	binomcxplemrat	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)⇝1$$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$$⊢\phi \to A\in {ℝ}^{+}$$
2		binomcxp.b	$$⊢\phi \to B\in ℝ$$
3		binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
4		binomcxp.c	$$⊢\phi \to C\in ℂ$$
5		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
6		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
7		peano2cn	$$⊢C\in ℂ\to C+1\in ℂ$$
8	4 7	syl	$$⊢\phi \to C+1\in ℂ$$
9		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
10		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
11	10	mptex	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\in \mathrm{V}$$
13		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)$$
14		simpr	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to k=x$$
15	14	oveq1d	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to k+1=x+1$$
16	15	oveq2d	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to \frac{C+1}{k+1}=\frac{C+1}{x+1}$$
17		simpr	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to x\in {\mathbb{N}}_0$$
18		ovexd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{C+1}{x+1}\in \mathrm{V}$$
19	13 16 17 18	fvmptd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\left(x\right)=\frac{C+1}{x+1}$$
20	5 6 8 9 12 19	divcnvshft	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)⇝0$$
21		ovexd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right){-}_f\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\in \mathrm{V}$$
22		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
23		1cnd	$$⊢k\in {\mathbb{N}}_0\to 1\in ℂ$$
24	22 23	addcld	$$⊢k\in {\mathbb{N}}_0\to k+1\in ℂ$$
25		nn0p1nn	$$⊢k\in {\mathbb{N}}_0\to k+1\in \mathbb{N}$$
26	25	nnne0d	$$⊢k\in {\mathbb{N}}_0\to k+1\ne 0$$
27	24 26	dividd	$$⊢k\in {\mathbb{N}}_0\to \frac{k+1}{k+1}=1$$
28	27	mpteq2ia	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼1\right)$$
29		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{1\right\}=\left(k\in {\mathbb{N}}_0⟼1\right)$$
30	28 29	eqtr4i	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)={\mathbb{N}}_0\times \left\{1\right\}$$
31		ax-1cn	$$⊢1\in ℂ$$
32		0z	$$⊢0\in \mathbb{Z}$$
33	5	eqimss2i	$$⊢{\mathbb{Z}}_{\ge 0}\subseteq {\mathbb{N}}_0$$
34	33 10	climconst2	$$⊢\left(1\in ℂ\wedge 0\in \mathbb{Z}\right)\to \left({\mathbb{N}}_0\times \left\{1\right\}\right)⇝1$$
35	31 32 34	mp2an	$$⊢\left({\mathbb{N}}_0\times \left\{1\right\}\right)⇝1$$
36	30 35	eqbrtri	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)⇝1$$
37	36	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)⇝1$$
38	4	adantr	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to C\in ℂ$$
39		1cnd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
40	38 39	addcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to C+1\in ℂ$$
41	17	nn0cnd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to x\in ℂ$$
42	41 39	addcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to x+1\in ℂ$$
43		nn0p1nn	$$⊢x\in {\mathbb{N}}_0\to x+1\in \mathbb{N}$$
44	43	nnne0d	$$⊢x\in {\mathbb{N}}_0\to x+1\ne 0$$
45	44	adantl	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to x+1\ne 0$$
46	40 42 45	divcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{C+1}{x+1}\in ℂ$$
47	19 46	eqeltrd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\left(x\right)\in ℂ$$
48		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)$$
49	15 15	oveq12d	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to \frac{k+1}{k+1}=\frac{x+1}{x+1}$$
50		ovexd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{x+1}{x+1}\in \mathrm{V}$$
51	48 49 17 50	fvmptd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\left(x\right)=\frac{x+1}{x+1}$$
52	42 42 45	divcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{x+1}{x+1}\in ℂ$$
53	51 52	eqeltrd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\left(x\right)\in ℂ$$
54		ovex	$$⊢\frac{C+1}{k+1}\in \mathrm{V}$$
55		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)$$
56	54 55	fnmpti	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)Fn{\mathbb{N}}_0$$
57	56	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)Fn{\mathbb{N}}_0$$
58		ovex	$$⊢\frac{k+1}{k+1}\in \mathrm{V}$$
59		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)$$
60	58 59	fnmpti	$$⊢\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)Fn{\mathbb{N}}_0$$
61	60	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)Fn{\mathbb{N}}_0$$
62	10	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
63		inidm	$$⊢{\mathbb{N}}_0\cap {\mathbb{N}}_0={\mathbb{N}}_0$$
64		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\left(x\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\left(x\right)$$
65		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\left(x\right)=\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\left(x\right)$$
66	57 61 62 62 63 64 65	ofval	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right){-}_f\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\right)\left(x\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)\left(x\right)-\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\left(x\right)$$
67	5 6 20 21 37 47 53 66	climsub	$$⊢\phi \to \left(\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right){-}_f\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)\right)⇝\left(0-1\right)$$
68		ovexd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{C+1}{k+1}\in \mathrm{V}$$
69		ovexd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{k+1}{k+1}\in \mathrm{V}$$
70		eqidd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right)$$
71		eqidd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)$$
72	62 68 69 70 71	offval2	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right){-}_f\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\left(\frac{C+1}{k+1}\right)-\left(\frac{k+1}{k+1}\right)\right)$$
73	8	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to C+1\in ℂ$$
74	24	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k+1\in ℂ$$
75	26	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k+1\ne 0$$
76	73 74 74 75	divsubdird	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{C+1-\left(k+1\right)}{k+1}=\left(\frac{C+1}{k+1}\right)-\left(\frac{k+1}{k+1}\right)$$
77	4	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to C\in ℂ$$
78	22	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in ℂ$$
79		1cnd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
80	77 78 79	pnpcan2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to C+1-\left(k+1\right)=C-k$$
81	80	oveq1d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{C+1-\left(k+1\right)}{k+1}=\frac{C-k}{k+1}$$
82	76 81	eqtr3d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\frac{C+1}{k+1}\right)-\left(\frac{k+1}{k+1}\right)=\frac{C-k}{k+1}$$
83	82	mpteq2dva	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\left(\frac{C+1}{k+1}\right)-\left(\frac{k+1}{k+1}\right)\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)$$
84	72 83	eqtrd	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C+1}{k+1}\right){-}_f\left(k\in {\mathbb{N}}_0⟼\frac{k+1}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)$$
85		df-neg	$$⊢-1=0-1$$
86	85	eqcomi	$$⊢0-1=-1$$
87	86	a1i	$$⊢\phi \to 0-1=-1$$
88	67 84 87	3brtr3d	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)⇝-1$$
89	10	mptex	$$⊢\left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)\in \mathrm{V}$$
90	89	a1i	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)\in \mathrm{V}$$
91		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)=\left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)$$
92		oveq2	$$⊢k=x\to C-k=C-x$$
93		oveq1	$$⊢k=x\to k+1=x+1$$
94	92 93	oveq12d	$$⊢k=x\to \frac{C-k}{k+1}=\frac{C-x}{x+1}$$
95	94	adantl	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to \frac{C-k}{k+1}=\frac{C-x}{x+1}$$
96		ovexd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{C-x}{x+1}\in \mathrm{V}$$
97	91 95 17 96	fvmptd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)\left(x\right)=\frac{C-x}{x+1}$$
98	38 41	subcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to C-x\in ℂ$$
99	98 42 45	divcld	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \frac{C-x}{x+1}\in ℂ$$
100	97 99	eqeltrd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)\left(x\right)\in ℂ$$
101		eqidd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)=\left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)$$
102	94	fveq2d	$$⊢k=x\to \left|\frac{C-k}{k+1}\right|=\left|\frac{C-x}{x+1}\right|$$
103	102	adantl	$$⊢\left(\left(\phi \wedge x\in {\mathbb{N}}_0\right)\wedge k=x\right)\to \left|\frac{C-k}{k+1}\right|=\left|\frac{C-x}{x+1}\right|$$
104		fvexd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left|\frac{C-x}{x+1}\right|\in \mathrm{V}$$
105	101 103 17 104	fvmptd	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)\left(x\right)=\left|\frac{C-x}{x+1}\right|$$
106	97	fveq2d	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left|\left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)\left(x\right)\right|=\left|\frac{C-x}{x+1}\right|$$
107	105 106	eqtr4d	$$⊢\left(\phi \wedge x\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)\left(x\right)=\left|\left(k\in {\mathbb{N}}_0⟼\frac{C-k}{k+1}\right)\left(x\right)\right|$$
108	5 88 90 6 100 107	climabs	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)⇝\left|-1\right|$$
109	31	absnegi	$$⊢\left|-1\right|=\left|1\right|$$
110		abs1	$$⊢\left|1\right|=1$$
111	109 110	eqtri	$$⊢\left|-1\right|=1$$
112	108 111	breqtrdi	$$⊢\phi \to \left(k\in {\mathbb{N}}_0⟼\left|\frac{C-k}{k+1}\right|\right)⇝1$$