Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	binomcxp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	binomcxp.lt	⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
	binomcxp.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	binomcxplem.f	⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
Assertion	binomcxplemfrat	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) ) ⇝ 1 )

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		binomcxp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		binomcxp.lt	⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4		binomcxp.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		binomcxplem.f	⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
8	6 7	bccp1k	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 ( 𝑘 + 1 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
9	5	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
10		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( 𝑘 + 1 ) ) → 𝑗 = ( 𝑘 + 1 ) )
11	10	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = ( 𝑘 + 1 ) ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 ( 𝑘 + 1 ) ) )
12		1nn0	⊢ 1 ∈ ℕ0
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℕ0 )
14	7 13	nn0addcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
15		ovexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 ( 𝑘 + 1 ) ) ∈ V )
16	9 11 14 15	fvmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐶 C𝑐 ( 𝑘 + 1 ) ) )
17		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
18	17	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 𝑘 ) )
19		ovexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ V )
20	9 18 7 19	fvmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
21	20	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
22	8 16 21	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
23	22	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
24	23	eqcomd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
25	6 7	bcccl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
26	20 25	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
27	26	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
28	6	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
29		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
30	29	nn0cnd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
31	28 30	subcld	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 − 𝑘 ) ∈ ℂ )
32		1cnd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
33	30 32	addcld	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℂ )
34		nn0p1nn	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
35	34	nnne0d	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ≠ 0 )
36	35	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ≠ 0 )
37	31 33 36	divcld	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ∈ ℂ )
38	27 37	mulcld	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ∈ ℂ )
39	23 38	eqeltrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
40	20	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
41		elfznn0	⊢ ( 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) → 𝐶 ∈ ℕ0 )
42	41	con3i	⊢ ( ¬ 𝐶 ∈ ℕ0 → ¬ 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) )
43	42	ad2antlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ¬ 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) )
44	28 29	bcc0	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) ) )
45	44	necon3abid	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) ≠ 0 ↔ ¬ 𝐶 ∈ ( 0 ... ( 𝑘 − 1 ) ) ) )
46	43 45	mpbird	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ≠ 0 )
47	40 46	eqnetrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
48	39 27 37 47	divmuld	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) · ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
49	24 48	mpbird	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) )
50	49	fveq2d	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) )
51	50	mpteq2dva	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) )
52	1 2 3 4	binomcxplemrat	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ⇝ 1 )
53	52	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐶 − 𝑘 ) / ( 𝑘 + 1 ) ) ) ) ⇝ 1 )
54	51 53	eqbrtrd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) ) ⇝ 1 )