binomcxplemfrat

Description: Lemma for binomcxp . binomcxplemrat implies that when C is not a nonnegative integer, the absolute value of the ratio ( ( F( k + 1 ) ) / ( Fk ) ) converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
	binomcxp.b	$⊢ φ \to B \in ℝ$
	binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
	binomcxp.c	$⊢ φ \to C \in ℂ$
	binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
Assertion	binomcxplemfrat	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \|\frac{F (k + 1)}{F (k)}\|) ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
2		binomcxp.b	$⊢ φ \to B \in ℝ$
3		binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
4		binomcxp.c	$⊢ φ \to C \in ℂ$
5		binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
6	4	adantr	$⊢ (φ \land k \in ℕ_{0}) \to C \in ℂ$
7		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
8	6 7	bccp1k	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} (k + 1) = (C C_{𝑐} k) (\frac{C - k}{k + 1})$
9	5	a1i	$⊢ (φ \land k \in ℕ_{0}) \to F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
10		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = k + 1) \to j = k + 1$
11	10	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k + 1) \to C C_{𝑐} j = C C_{𝑐} (k + 1)$
12		1nn0	$⊢ 1 \in ℕ_{0}$
13	12	a1i	$⊢ (φ \land k \in ℕ_{0}) \to 1 \in ℕ_{0}$
14	7 13	nn0addcld	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
15		ovexd	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} (k + 1) \in V$
16	9 11 14 15	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) = C C_{𝑐} (k + 1)$
17		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to j = k$
18	17	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to C C_{𝑐} j = C C_{𝑐} k$
19		ovexd	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} k \in V$
20	9 18 7 19	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
21	20	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to F (k) (\frac{C - k}{k + 1}) = (C C_{𝑐} k) (\frac{C - k}{k + 1})$
22	8 16 21	3eqtr4d	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) = F (k) (\frac{C - k}{k + 1})$
23	22	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k + 1) = F (k) (\frac{C - k}{k + 1})$
24	23	eqcomd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) (\frac{C - k}{k + 1}) = F (k + 1)$
25	6 7	bcccl	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
26	20 25	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℂ$
27	26	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) \in ℂ$
28	6	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C \in ℂ$
29		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
30	29	nn0cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℂ$
31	28 30	subcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C - k \in ℂ$
32		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to 1 \in ℂ$
33	30 32	addcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k + 1 \in ℂ$
34		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
35	34	nnne0d	$⊢ k \in ℕ_{0} \to k + 1 \neq 0$
36	35	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to k + 1 \neq 0$
37	31 33 36	divcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{C - k}{k + 1} \in ℂ$
38	27 37	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) (\frac{C - k}{k + 1}) \in ℂ$
39	23 38	eqeltrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k + 1) \in ℂ$
40	20	adantlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
41		elfznn0	$⊢ C \in (0 \dots k - 1) \to C \in ℕ_{0}$
42	41	con3i	$⊢ \neg C \in ℕ_{0} \to \neg C \in (0 \dots k - 1)$
43	42	ad2antlr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \neg C \in (0 \dots k - 1)$
44	28 29	bcc0	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k = 0 \leftrightarrow C \in (0 \dots k - 1))$
45	44	necon3abid	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (C C_{𝑐} k \neq 0 \leftrightarrow \neg C \in (0 \dots k - 1))$
46	43 45	mpbird	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to C C_{𝑐} k \neq 0$
47	40 46	eqnetrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) \neq 0$
48	39 27 37 47	divmuld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to (\frac{F (k + 1)}{F (k)} = \frac{C - k}{k + 1} \leftrightarrow F (k) (\frac{C - k}{k + 1}) = F (k + 1))$
49	24 48	mpbird	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{F (k + 1)}{F (k)} = \frac{C - k}{k + 1}$
50	49	fveq2d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land k \in ℕ_{0}) \to \|\frac{F (k + 1)}{F (k)}\| = \|\frac{C - k}{k + 1}\|$
51	50	mpteq2dva	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \|\frac{F (k + 1)}{F (k)}\|) = (k \in ℕ_{0} ⟼ \|\frac{C - k}{k + 1}\|)$
52	1 2 3 4	binomcxplemrat	$⊢ φ \to (k \in ℕ_{0} ⟼ \|\frac{C - k}{k + 1}\|) ⇝ 1$
53	52	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \|\frac{C - k}{k + 1}\|) ⇝ 1$
54	51 53	eqbrtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ \|\frac{F (k + 1)}{F (k)}\|) ⇝ 1$

Metamath Proof Explorer

Theorem binomcxplemfrat

Proof