Step | Hyp | Ref
| Expression |
1 | | binomcxp.c |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โ) |
2 | 1 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ๐ถ โ
โ) |
3 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
4 | 2, 3 | bccp1k 43086 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ถC๐(๐ + 1)) = ((๐ถC๐๐) ยท ((๐ถ โ ๐) / (๐ + 1)))) |
5 | | binomcxplem.f |
. . . . . . . . . 10
โข ๐น = (๐ โ โ0 โฆ (๐ถC๐๐)) |
6 | 5 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ ๐น = (๐ โ โ0 โฆ (๐ถC๐๐))) |
7 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ = (๐ + 1)) โ ๐ = (๐ + 1)) |
8 | 7 | oveq2d 7422 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ๐ = (๐ + 1)) โ (๐ถC๐๐) = (๐ถC๐(๐ + 1))) |
9 | | 1nn0 12485 |
. . . . . . . . . . 11
โข 1 โ
โ0 |
10 | 9 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ 1 โ
โ0) |
11 | 3, 10 | nn0addcld 12533 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ0) |
12 | | ovexd 7441 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐ถC๐(๐ + 1)) โ
V) |
13 | 6, 8, 11, 12 | fvmptd 7003 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐นโ(๐ + 1)) = (๐ถC๐(๐ + 1))) |
14 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ = ๐) โ ๐ = ๐) |
15 | 14 | oveq2d 7422 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ = ๐) โ (๐ถC๐๐) = (๐ถC๐๐)) |
16 | | ovexd 7441 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (๐ถC๐๐) โ V) |
17 | 6, 15, 3, 16 | fvmptd 7003 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (๐ถC๐๐)) |
18 | 17 | oveq1d 7421 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1))) = ((๐ถC๐๐) ยท ((๐ถ โ ๐) / (๐ + 1)))) |
19 | 4, 13, 18 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐นโ(๐ + 1)) = ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1)))) |
20 | 19 | adantlr 714 |
. . . . . 6
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐นโ(๐ + 1)) = ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1)))) |
21 | 20 | eqcomd 2739 |
. . . . 5
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1))) = (๐นโ(๐ + 1))) |
22 | 2, 3 | bcccl 43084 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ (๐ถC๐๐) โ
โ) |
23 | 17, 22 | eqeltrd 2834 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) โ โ) |
24 | 23 | adantlr 714 |
. . . . . . . 8
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐นโ๐) โ
โ) |
25 | 2 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ๐ถ โ
โ) |
26 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ๐ โ
โ0) |
27 | 26 | nn0cnd 12531 |
. . . . . . . . . 10
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ๐ โ
โ) |
28 | 25, 27 | subcld 11568 |
. . . . . . . . 9
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐ถ โ ๐) โ
โ) |
29 | | 1cnd 11206 |
. . . . . . . . . 10
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ 1 โ โ) |
30 | 27, 29 | addcld 11230 |
. . . . . . . . 9
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐ + 1) โ
โ) |
31 | | nn0p1nn 12508 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
32 | 31 | nnne0d 12259 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
0) |
33 | 32 | adantl 483 |
. . . . . . . . 9
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐ + 1) โ
0) |
34 | 28, 30, 33 | divcld 11987 |
. . . . . . . 8
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐ถ โ ๐) / (๐ + 1)) โ โ) |
35 | 24, 34 | mulcld 11231 |
. . . . . . 7
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1))) โ โ) |
36 | 20, 35 | eqeltrd 2834 |
. . . . . 6
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐นโ(๐ + 1)) โ
โ) |
37 | 17 | adantlr 714 |
. . . . . . 7
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐นโ๐) = (๐ถC๐๐)) |
38 | | elfznn0 13591 |
. . . . . . . . . 10
โข (๐ถ โ (0...(๐ โ 1)) โ ๐ถ โ
โ0) |
39 | 38 | con3i 154 |
. . . . . . . . 9
โข (ยฌ
๐ถ โ
โ0 โ ยฌ ๐ถ โ (0...(๐ โ 1))) |
40 | 39 | ad2antlr 726 |
. . . . . . . 8
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ยฌ ๐ถ โ
(0...(๐ โ
1))) |
41 | 25, 26 | bcc0 43085 |
. . . . . . . . 9
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐ถC๐๐) = 0 โ ๐ถ โ (0...(๐ โ 1)))) |
42 | 41 | necon3abid 2978 |
. . . . . . . 8
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐ถC๐๐) โ 0 โ ยฌ ๐ถ โ (0...(๐ โ 1)))) |
43 | 40, 42 | mpbird 257 |
. . . . . . 7
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐ถC๐๐) โ 0) |
44 | 37, 43 | eqnetrd 3009 |
. . . . . 6
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (๐นโ๐) โ 0) |
45 | 36, 24, 34, 44 | divmuld 12009 |
. . . . 5
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (((๐นโ(๐ + 1)) / (๐นโ๐)) = ((๐ถ โ ๐) / (๐ + 1)) โ ((๐นโ๐) ยท ((๐ถ โ ๐) / (๐ + 1))) = (๐นโ(๐ + 1)))) |
46 | 21, 45 | mpbird 257 |
. . . 4
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ ((๐นโ(๐ + 1)) / (๐นโ๐)) = ((๐ถ โ ๐) / (๐ + 1))) |
47 | 46 | fveq2d 6893 |
. . 3
โข (((๐ โง ยฌ ๐ถ โ โ0) โง ๐ โ โ0)
โ (absโ((๐นโ(๐ + 1)) / (๐นโ๐))) = (absโ((๐ถ โ ๐) / (๐ + 1)))) |
48 | 47 | mpteq2dva 5248 |
. 2
โข ((๐ โง ยฌ ๐ถ โ โ0) โ (๐ โ โ0
โฆ (absโ((๐นโ(๐ + 1)) / (๐นโ๐)))) = (๐ โ โ0 โฆ
(absโ((๐ถ โ
๐) / (๐ + 1))))) |
49 | | binomcxp.a |
. . . 4
โข (๐ โ ๐ด โ
โ+) |
50 | | binomcxp.b |
. . . 4
โข (๐ โ ๐ต โ โ) |
51 | | binomcxp.lt |
. . . 4
โข (๐ โ (absโ๐ต) < (absโ๐ด)) |
52 | 49, 50, 51, 1 | binomcxplemrat 43095 |
. . 3
โข (๐ โ (๐ โ โ0 โฆ
(absโ((๐ถ โ
๐) / (๐ + 1)))) โ 1) |
53 | 52 | adantr 482 |
. 2
โข ((๐ โง ยฌ ๐ถ โ โ0) โ (๐ โ โ0
โฆ (absโ((๐ถ
โ ๐) / (๐ + 1)))) โ
1) |
54 | 48, 53 | eqbrtrd 5170 |
1
โข ((๐ โง ยฌ ๐ถ โ โ0) โ (๐ โ โ0
โฆ (absโ((๐นโ(๐ + 1)) / (๐นโ๐)))) โ 1) |