Proof of Theorem binomcxplemfrat
Step | Hyp | Ref
| Expression |
1 | | binomcxp.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℂ) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
4 | 2, 3 | bccp1k 37562 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐(𝑘 + 1)) = ((𝐶C𝑐𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1)))) |
5 | | binomcxplem.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))) |
7 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = (𝑘 + 1)) → 𝑗 = (𝑘 + 1)) |
8 | 7 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = (𝑘 + 1)) → (𝐶C𝑐𝑗) = (𝐶C𝑐(𝑘 + 1))) |
9 | | 1nn0 11185 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 1 ∈
ℕ0) |
11 | 3, 10 | nn0addcld 11232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℕ0) |
12 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐶C𝑐(𝑘 + 1)) ∈ V |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐(𝑘 + 1)) ∈
V) |
14 | 6, 8, 11, 13 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) = (𝐶C𝑐(𝑘 + 1))) |
15 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
16 | 15 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝐶C𝑐𝑗) = (𝐶C𝑐𝑘)) |
17 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝐶C𝑐𝑘) ∈ V |
18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐𝑘) ∈ V) |
19 | 6, 16, 3, 18 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐶C𝑐𝑘)) |
20 | 19 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1))) = ((𝐶C𝑐𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1)))) |
21 | 4, 14, 20 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘(𝑘 + 1)) = ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1)))) |
22 | 21 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘(𝑘 + 1)) = ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1)))) |
23 | 22 | eqcomd 2616 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
24 | 2, 3 | bcccl 37560 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐶C𝑐𝑘) ∈
ℂ) |
25 | 19, 24 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ) |
26 | 25 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) ∈
ℂ) |
27 | 2 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝐶 ∈
ℂ) |
28 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
29 | 28 | nn0cnd 11230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) |
30 | 27, 29 | subcld 10271 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐶 − 𝑘) ∈
ℂ) |
31 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℂ) |
32 | 29, 31 | addcld 9938 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ∈
ℂ) |
33 | | nn0p1nn 11209 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
34 | 33 | nnne0d 10942 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ≠
0) |
35 | 34 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 + 1) ≠
0) |
36 | 30, 32, 35 | divcld 10680 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐶 − 𝑘) / (𝑘 + 1)) ∈ ℂ) |
37 | 26, 36 | mulcld 9939 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1))) ∈ ℂ) |
38 | 22, 37 | eqeltrd 2688 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘(𝑘 + 1)) ∈
ℂ) |
39 | 19 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) = (𝐶C𝑐𝑘)) |
40 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (0...(𝑘 − 1)) → 𝐶 ∈
ℕ0) |
41 | 40 | con3i 149 |
. . . . . . . . 9
⊢ (¬
𝐶 ∈
ℕ0 → ¬ 𝐶 ∈ (0...(𝑘 − 1))) |
42 | 41 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ¬ 𝐶 ∈
(0...(𝑘 −
1))) |
43 | 27, 28 | bcc0 37561 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐶C𝑐𝑘) = 0 ↔ 𝐶 ∈ (0...(𝑘 − 1)))) |
44 | 43 | necon3abid 2818 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐶C𝑐𝑘) ≠ 0 ↔ ¬ 𝐶 ∈ (0...(𝑘 − 1)))) |
45 | 42, 44 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐶C𝑐𝑘) ≠ 0) |
46 | 39, 45 | eqnetrd 2849 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝐹‘𝑘) ≠ 0) |
47 | 38, 26, 36, 46 | divmuld 10702 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) = ((𝐶 − 𝑘) / (𝑘 + 1)) ↔ ((𝐹‘𝑘) · ((𝐶 − 𝑘) / (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))) |
48 | 23, 47 | mpbird 246 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)) = ((𝐶 − 𝑘) / (𝑘 + 1))) |
49 | 48 | fveq2d 6107 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘))) = (abs‘((𝐶 − 𝑘) / (𝑘 + 1)))) |
50 | 49 | mpteq2dva 4672 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) = (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1))))) |
51 | | binomcxp.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
52 | | binomcxp.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
53 | | binomcxp.lt |
. . . 4
⊢ (𝜑 → (abs‘𝐵) < (abs‘𝐴)) |
54 | 51, 52, 53, 1 | binomcxplemrat 37571 |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦
(abs‘((𝐶 −
𝑘) / (𝑘 + 1)))) ⇝ 1) |
55 | 54 | adantr 480 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (abs‘((𝐶
− 𝑘) / (𝑘 + 1)))) ⇝
1) |
56 | 50, 55 | eqbrtrd 4605 |
1
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑘 ∈ ℕ0
↦ (abs‘((𝐹‘(𝑘 + 1)) / (𝐹‘𝑘)))) ⇝ 1) |