Step | Hyp | Ref
| Expression |
1 | | binomcxplem.c |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
2 | | binomcxplem.k |
. . . . . . 7
โข (๐ โ ๐พ โ โ) |
3 | 2 | nncnd 12177 |
. . . . . 6
โข (๐ โ ๐พ โ โ) |
4 | 1, 3 | npcand 11524 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐พ) + ๐พ) = ๐ถ) |
5 | 4 | oveq1d 7376 |
. . . 4
โข (๐ โ (((๐ถ โ ๐พ) + ๐พ) ยท (๐ถ FallFac ๐พ)) = (๐ถ ยท (๐ถ FallFac ๐พ))) |
6 | 1, 3 | subcld 11520 |
. . . . 5
โข (๐ โ (๐ถ โ ๐พ) โ โ) |
7 | 2 | nnnn0d 12481 |
. . . . . 6
โข (๐ โ ๐พ โ
โ0) |
8 | | fallfaccl 15907 |
. . . . . 6
โข ((๐ถ โ โ โง ๐พ โ โ0)
โ (๐ถ FallFac ๐พ) โ
โ) |
9 | 1, 7, 8 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ถ FallFac ๐พ) โ โ) |
10 | 6, 3, 9 | adddird 11188 |
. . . 4
โข (๐ โ (((๐ถ โ ๐พ) + ๐พ) ยท (๐ถ FallFac ๐พ)) = (((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) + (๐พ ยท (๐ถ FallFac ๐พ)))) |
11 | 5, 10 | eqtr3d 2775 |
. . 3
โข (๐ โ (๐ถ ยท (๐ถ FallFac ๐พ)) = (((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) + (๐พ ยท (๐ถ FallFac ๐พ)))) |
12 | 11 | oveq1d 7376 |
. 2
โข (๐ โ ((๐ถ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) = ((((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) + (๐พ ยท (๐ถ FallFac ๐พ))) / (!โ๐พ))) |
13 | 1, 7 | bccval 42710 |
. . . 4
โข (๐ โ (๐ถC๐๐พ) = ((๐ถ FallFac ๐พ) / (!โ๐พ))) |
14 | 13 | oveq2d 7377 |
. . 3
โข (๐ โ (๐ถ ยท (๐ถC๐๐พ)) = (๐ถ ยท ((๐ถ FallFac ๐พ) / (!โ๐พ)))) |
15 | | faccl 14192 |
. . . . . 6
โข (๐พ โ โ0
โ (!โ๐พ) โ
โ) |
16 | 15 | nncnd 12177 |
. . . . 5
โข (๐พ โ โ0
โ (!โ๐พ) โ
โ) |
17 | 7, 16 | syl 17 |
. . . 4
โข (๐ โ (!โ๐พ) โ โ) |
18 | | facne0 14195 |
. . . . 5
โข (๐พ โ โ0
โ (!โ๐พ) โ
0) |
19 | 7, 18 | syl 17 |
. . . 4
โข (๐ โ (!โ๐พ) โ 0) |
20 | 1, 9, 17, 19 | divassd 11974 |
. . 3
โข (๐ โ ((๐ถ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) = (๐ถ ยท ((๐ถ FallFac ๐พ) / (!โ๐พ)))) |
21 | 14, 20 | eqtr4d 2776 |
. 2
โข (๐ โ (๐ถ ยท (๐ถC๐๐พ)) = ((๐ถ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ))) |
22 | 6, 9, 17, 19 | divassd 11974 |
. . . 4
โข (๐ โ (((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) = ((๐ถ โ ๐พ) ยท ((๐ถ FallFac ๐พ) / (!โ๐พ)))) |
23 | 22 | oveq1d 7376 |
. . 3
โข (๐ โ ((((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) + ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ))) = (((๐ถ โ ๐พ) ยท ((๐ถ FallFac ๐พ) / (!โ๐พ))) + ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)))) |
24 | 6, 9 | mulcld 11183 |
. . . 4
โข (๐ โ ((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) โ โ) |
25 | 3, 9 | mulcld 11183 |
. . . 4
โข (๐ โ (๐พ ยท (๐ถ FallFac ๐พ)) โ โ) |
26 | 24, 25, 17, 19 | divdird 11977 |
. . 3
โข (๐ โ ((((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) + (๐พ ยท (๐ถ FallFac ๐พ))) / (!โ๐พ)) = ((((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) + ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)))) |
27 | 13 | oveq2d 7377 |
. . . 4
โข (๐ โ ((๐ถ โ ๐พ) ยท (๐ถC๐๐พ)) = ((๐ถ โ ๐พ) ยท ((๐ถ FallFac ๐พ) / (!โ๐พ)))) |
28 | | nnm1nn0 12462 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ0) |
29 | 2, 28 | syl 17 |
. . . . . . 7
โข (๐ โ (๐พ โ 1) โ
โ0) |
30 | | faccl 14192 |
. . . . . . . 8
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ
โ) |
31 | 30 | nncnd 12177 |
. . . . . . 7
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ
โ) |
32 | 29, 31 | syl 17 |
. . . . . 6
โข (๐ โ (!โ(๐พ โ 1)) โ
โ) |
33 | | facne0 14195 |
. . . . . . 7
โข ((๐พ โ 1) โ
โ0 โ (!โ(๐พ โ 1)) โ 0) |
34 | 29, 33 | syl 17 |
. . . . . 6
โข (๐ โ (!โ(๐พ โ 1)) โ
0) |
35 | 2 | nnne0d 12211 |
. . . . . 6
โข (๐ โ ๐พ โ 0) |
36 | 9, 32, 3, 34, 35 | divcan5d 11965 |
. . . . 5
โข (๐ โ ((๐พ ยท (๐ถ FallFac ๐พ)) / (๐พ ยท (!โ(๐พ โ 1)))) = ((๐ถ FallFac ๐พ) / (!โ(๐พ โ 1)))) |
37 | | 1cnd 11158 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
38 | 3, 37 | npcand 11524 |
. . . . . . . 8
โข (๐ โ ((๐พ โ 1) + 1) = ๐พ) |
39 | 38 | fveq2d 6850 |
. . . . . . 7
โข (๐ โ (!โ((๐พ โ 1) + 1)) =
(!โ๐พ)) |
40 | 38 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ ((!โ(๐พ โ 1)) ยท ((๐พ โ 1) + 1)) =
((!โ(๐พ โ 1))
ยท ๐พ)) |
41 | | facp1 14187 |
. . . . . . . . 9
โข ((๐พ โ 1) โ
โ0 โ (!โ((๐พ โ 1) + 1)) = ((!โ(๐พ โ 1)) ยท ((๐พ โ 1) +
1))) |
42 | 29, 41 | syl 17 |
. . . . . . . 8
โข (๐ โ (!โ((๐พ โ 1) + 1)) =
((!โ(๐พ โ 1))
ยท ((๐พ โ 1) +
1))) |
43 | 3, 32 | mulcomd 11184 |
. . . . . . . 8
โข (๐ โ (๐พ ยท (!โ(๐พ โ 1))) = ((!โ(๐พ โ 1)) ยท ๐พ)) |
44 | 40, 42, 43 | 3eqtr4d 2783 |
. . . . . . 7
โข (๐ โ (!โ((๐พ โ 1) + 1)) = (๐พ ยท (!โ(๐พ โ 1)))) |
45 | 39, 44 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (!โ๐พ) = (๐พ ยท (!โ(๐พ โ 1)))) |
46 | 45 | oveq2d 7377 |
. . . . 5
โข (๐ โ ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)) = ((๐พ ยท (๐ถ FallFac ๐พ)) / (๐พ ยท (!โ(๐พ โ 1))))) |
47 | 3, 37 | subcld 11520 |
. . . . . . . 8
โข (๐ โ (๐พ โ 1) โ โ) |
48 | 1, 47 | subcld 11520 |
. . . . . . 7
โข (๐ โ (๐ถ โ (๐พ โ 1)) โ
โ) |
49 | | fallfaccl 15907 |
. . . . . . . 8
โข ((๐ถ โ โ โง (๐พ โ 1) โ
โ0) โ (๐ถ FallFac (๐พ โ 1)) โ
โ) |
50 | 1, 29, 49 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ถ FallFac (๐พ โ 1)) โ
โ) |
51 | 48, 50, 32, 34 | divassd 11974 |
. . . . . 6
โข (๐ โ (((๐ถ โ (๐พ โ 1)) ยท (๐ถ FallFac (๐พ โ 1))) / (!โ(๐พ โ 1))) = ((๐ถ โ (๐พ โ 1)) ยท ((๐ถ FallFac (๐พ โ 1)) / (!โ(๐พ โ 1))))) |
52 | 38 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (๐ถ FallFac ((๐พ โ 1) + 1)) = (๐ถ FallFac ๐พ)) |
53 | | fallfacp1 15921 |
. . . . . . . . . 10
โข ((๐ถ โ โ โง (๐พ โ 1) โ
โ0) โ (๐ถ FallFac ((๐พ โ 1) + 1)) = ((๐ถ FallFac (๐พ โ 1)) ยท (๐ถ โ (๐พ โ 1)))) |
54 | 1, 29, 53 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐ถ FallFac ((๐พ โ 1) + 1)) = ((๐ถ FallFac (๐พ โ 1)) ยท (๐ถ โ (๐พ โ 1)))) |
55 | 52, 54 | eqtr3d 2775 |
. . . . . . . 8
โข (๐ โ (๐ถ FallFac ๐พ) = ((๐ถ FallFac (๐พ โ 1)) ยท (๐ถ โ (๐พ โ 1)))) |
56 | 48, 50 | mulcomd 11184 |
. . . . . . . 8
โข (๐ โ ((๐ถ โ (๐พ โ 1)) ยท (๐ถ FallFac (๐พ โ 1))) = ((๐ถ FallFac (๐พ โ 1)) ยท (๐ถ โ (๐พ โ 1)))) |
57 | 55, 56 | eqtr4d 2776 |
. . . . . . 7
โข (๐ โ (๐ถ FallFac ๐พ) = ((๐ถ โ (๐พ โ 1)) ยท (๐ถ FallFac (๐พ โ 1)))) |
58 | 57 | oveq1d 7376 |
. . . . . 6
โข (๐ โ ((๐ถ FallFac ๐พ) / (!โ(๐พ โ 1))) = (((๐ถ โ (๐พ โ 1)) ยท (๐ถ FallFac (๐พ โ 1))) / (!โ(๐พ โ 1)))) |
59 | 1, 29 | bccval 42710 |
. . . . . . 7
โข (๐ โ (๐ถC๐(๐พ โ 1)) = ((๐ถ FallFac (๐พ โ 1)) / (!โ(๐พ โ 1)))) |
60 | 59 | oveq2d 7377 |
. . . . . 6
โข (๐ โ ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1))) = ((๐ถ โ (๐พ โ 1)) ยท ((๐ถ FallFac (๐พ โ 1)) / (!โ(๐พ โ 1))))) |
61 | 51, 58, 60 | 3eqtr4rd 2784 |
. . . . 5
โข (๐ โ ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1))) = ((๐ถ FallFac ๐พ) / (!โ(๐พ โ 1)))) |
62 | 36, 46, 61 | 3eqtr4rd 2784 |
. . . 4
โข (๐ โ ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1))) = ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ))) |
63 | 27, 62 | oveq12d 7379 |
. . 3
โข (๐ โ (((๐ถ โ ๐พ) ยท (๐ถC๐๐พ)) + ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1)))) = (((๐ถ โ ๐พ) ยท ((๐ถ FallFac ๐พ) / (!โ๐พ))) + ((๐พ ยท (๐ถ FallFac ๐พ)) / (!โ๐พ)))) |
64 | 23, 26, 63 | 3eqtr4rd 2784 |
. 2
โข (๐ โ (((๐ถ โ ๐พ) ยท (๐ถC๐๐พ)) + ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1)))) = ((((๐ถ โ ๐พ) ยท (๐ถ FallFac ๐พ)) + (๐พ ยท (๐ถ FallFac ๐พ))) / (!โ๐พ))) |
65 | 12, 21, 64 | 3eqtr4rd 2784 |
1
โข (๐ โ (((๐ถ โ ๐พ) ยท (๐ถC๐๐พ)) + ((๐ถ โ (๐พ โ 1)) ยท (๐ถC๐(๐พ โ 1)))) = (๐ถ ยท (๐ถC๐๐พ))) |