Step | Hyp | Ref
| Expression |
1 | | binomcxplem.s |
. . . 4
β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
2 | | simpl 484 |
. . . . . . . . 9
β’ ((π = π₯ β§ π β β0) β π = π₯) |
3 | 2 | oveq1d 7376 |
. . . . . . . 8
β’ ((π = π₯ β§ π β β0) β (πβπ) = (π₯βπ)) |
4 | 3 | oveq2d 7377 |
. . . . . . 7
β’ ((π = π₯ β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΉβπ) Β· (π₯βπ))) |
5 | 4 | mpteq2dva 5209 |
. . . . . 6
β’ (π = π₯ β (π β β0 β¦ ((πΉβπ) Β· (πβπ))) = (π β β0 β¦ ((πΉβπ) Β· (π₯βπ)))) |
6 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π¦ β (πΉβπ) = (πΉβπ¦)) |
7 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π¦ β (π₯βπ) = (π₯βπ¦)) |
8 | 6, 7 | oveq12d 7379 |
. . . . . . 7
β’ (π = π¦ β ((πΉβπ) Β· (π₯βπ)) = ((πΉβπ¦) Β· (π₯βπ¦))) |
9 | 8 | cbvmptv 5222 |
. . . . . 6
β’ (π β β0
β¦ ((πΉβπ) Β· (π₯βπ))) = (π¦ β β0 β¦ ((πΉβπ¦) Β· (π₯βπ¦))) |
10 | 5, 9 | eqtrdi 2789 |
. . . . 5
β’ (π = π₯ β (π β β0 β¦ ((πΉβπ) Β· (πβπ))) = (π¦ β β0 β¦ ((πΉβπ¦) Β· (π₯βπ¦)))) |
11 | 10 | cbvmptv 5222 |
. . . 4
β’ (π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ)))) = (π₯ β β β¦ (π¦ β β0 β¦ ((πΉβπ¦) Β· (π₯βπ¦)))) |
12 | 1, 11 | eqtri 2761 |
. . 3
β’ π = (π₯ β β β¦ (π¦ β β0 β¦ ((πΉβπ¦) Β· (π₯βπ¦)))) |
13 | | binomcxp.c |
. . . . . 6
β’ (π β πΆ β β) |
14 | 13 | ad2antrr 725 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β πΆ β
β) |
15 | | simpr 486 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π β
β0) |
16 | 14, 15 | bcccl 42711 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΆCππ) β β) |
17 | | binomcxplem.f |
. . . 4
β’ πΉ = (π β β0 β¦ (πΆCππ)) |
18 | 16, 17 | fmptd 7066 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β πΉ:β0βΆβ) |
19 | | binomcxplem.r |
. . 3
β’ π
= sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
20 | | fvoveq1 7384 |
. . . . . 6
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
21 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
22 | 20, 21 | oveq12d 7379 |
. . . . 5
β’ (π = π β ((πΉβ(π + 1)) / (πΉβπ)) = ((πΉβ(π + 1)) / (πΉβπ))) |
23 | 22 | fveq2d 6850 |
. . . 4
β’ (π = π β (absβ((πΉβ(π + 1)) / (πΉβπ))) = (absβ((πΉβ(π + 1)) / (πΉβπ)))) |
24 | 23 | cbvmptv 5222 |
. . 3
β’ (π β β0
β¦ (absβ((πΉβ(π + 1)) / (πΉβπ)))) = (π β β0 β¦
(absβ((πΉβ(π + 1)) / (πΉβπ)))) |
25 | | nn0uz 12813 |
. . 3
β’
β0 = (β€β₯β0) |
26 | | 0nn0 12436 |
. . . 4
β’ 0 β
β0 |
27 | 26 | a1i 11 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β 0 β
β0) |
28 | 17 | a1i 11 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β πΉ = (π β β0
β¦ (πΆCππ))) |
29 | | simpr 486 |
. . . . . 6
β’ ((((π β§ Β¬ πΆ β β0) β§ π β β0)
β§ π = π) β π = π) |
30 | 29 | oveq2d 7377 |
. . . . 5
β’ ((((π β§ Β¬ πΆ β β0) β§ π β β0)
β§ π = π) β (πΆCππ) = (πΆCππ)) |
31 | | simpr 486 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π β
β0) |
32 | | ovexd 7396 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΆCππ) β V) |
33 | 28, 30, 31, 32 | fvmptd 6959 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΉβπ) = (πΆCππ)) |
34 | | elfznn0 13543 |
. . . . . . 7
β’ (πΆ β (0...(π β 1)) β πΆ β
β0) |
35 | 34 | con3i 154 |
. . . . . 6
β’ (Β¬
πΆ β
β0 β Β¬ πΆ β (0...(π β 1))) |
36 | 35 | ad2antlr 726 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β Β¬ πΆ β
(0...(π β
1))) |
37 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β πΆ β
β) |
38 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β
β0) |
39 | 37, 38 | bcc0 42712 |
. . . . . . 7
β’ ((π β§ π β β0) β ((πΆCππ) = 0 β πΆ β (0...(π β 1)))) |
40 | 39 | necon3abid 2977 |
. . . . . 6
β’ ((π β§ π β β0) β ((πΆCππ) β 0 β Β¬ πΆ β (0...(π β 1)))) |
41 | 40 | adantlr 714 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) β 0 β Β¬ πΆ β (0...(π β 1)))) |
42 | 36, 41 | mpbird 257 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΆCππ) β 0) |
43 | 33, 42 | eqnetrd 3008 |
. . 3
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΉβπ) β 0) |
44 | | binomcxp.a |
. . . 4
β’ (π β π΄ β
β+) |
45 | | binomcxp.b |
. . . 4
β’ (π β π΅ β β) |
46 | | binomcxp.lt |
. . . 4
β’ (π β (absβπ΅) < (absβπ΄)) |
47 | 44, 45, 46, 13, 17 | binomcxplemfrat 42723 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (π β β0
β¦ (absβ((πΉβ(π + 1)) / (πΉβπ)))) β 1) |
48 | | ax-1ne0 11128 |
. . . 4
β’ 1 β
0 |
49 | 48 | a1i 11 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β 1 β
0) |
50 | 12, 18, 19, 24, 25, 27, 43, 47, 49 | radcnvrat 42686 |
. 2
β’ ((π β§ Β¬ πΆ β β0) β π
= (1 / 1)) |
51 | | 1div1e1 11853 |
. 2
β’ (1 / 1) =
1 |
52 | 50, 51 | eqtrdi 2789 |
1
β’ ((π β§ Β¬ πΆ β β0) β π
= 1) |