Step | Hyp | Ref
| Expression |
1 | | elfz3nn0 13541 |
. . . . 5
โข (๐พ โ (0...๐) โ ๐ โ
โ0) |
2 | | facp1 14184 |
. . . . 5
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐พ โ (0...๐) โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
4 | | fznn0sub 13479 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ (๐ โ ๐พ) โ
โ0) |
5 | | facp1 14184 |
. . . . . . . 8
โข ((๐ โ ๐พ) โ โ0 โ
(!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
6 | 4, 5 | syl 17 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (!โ((๐ โ ๐พ) + 1)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
7 | 1 | nn0cnd 12480 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐ โ โ) |
8 | | 1cnd 11155 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ 1 โ โ) |
9 | | elfznn0 13540 |
. . . . . . . . . 10
โข (๐พ โ (0...๐) โ ๐พ โ
โ0) |
10 | 9 | nn0cnd 12480 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐พ โ โ) |
11 | 7, 8, 10 | addsubd 11538 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) = ((๐ โ ๐พ) + 1)) |
12 | 11 | fveq2d 6847 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (!โ((๐ + 1) โ ๐พ)) = (!โ((๐ โ ๐พ) + 1))) |
13 | 11 | oveq2d 7374 |
. . . . . . 7
โข (๐พ โ (0...๐) โ ((!โ(๐ โ ๐พ)) ยท ((๐ + 1) โ ๐พ)) = ((!โ(๐ โ ๐พ)) ยท ((๐ โ ๐พ) + 1))) |
14 | 6, 12, 13 | 3eqtr4d 2783 |
. . . . . 6
โข (๐พ โ (0...๐) โ (!โ((๐ + 1) โ ๐พ)) = ((!โ(๐ โ ๐พ)) ยท ((๐ + 1) โ ๐พ))) |
15 | 14 | oveq1d 7373 |
. . . . 5
โข (๐พ โ (0...๐) โ ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ)) = (((!โ(๐ โ ๐พ)) ยท ((๐ + 1) โ ๐พ)) ยท (!โ๐พ))) |
16 | 4 | faccld 14190 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
17 | 16 | nncnd 12174 |
. . . . . 6
โข (๐พ โ (0...๐) โ (!โ(๐ โ ๐พ)) โ โ) |
18 | | nn0p1nn 12457 |
. . . . . . . . 9
โข ((๐ โ ๐พ) โ โ0 โ ((๐ โ ๐พ) + 1) โ โ) |
19 | 4, 18 | syl 17 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ ((๐ โ ๐พ) + 1) โ โ) |
20 | 11, 19 | eqeltrd 2834 |
. . . . . . 7
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ โ) |
21 | 20 | nncnd 12174 |
. . . . . 6
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ โ) |
22 | 9 | faccld 14190 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (!โ๐พ) โ โ) |
23 | 22 | nncnd 12174 |
. . . . . 6
โข (๐พ โ (0...๐) โ (!โ๐พ) โ โ) |
24 | 17, 21, 23 | mul32d 11370 |
. . . . 5
โข (๐พ โ (0...๐) โ (((!โ(๐ โ ๐พ)) ยท ((๐ + 1) โ ๐พ)) ยท (!โ๐พ)) = (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ + 1) โ ๐พ))) |
25 | 15, 24 | eqtrd 2773 |
. . . 4
โข (๐พ โ (0...๐) โ ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ)) = (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ + 1) โ ๐พ))) |
26 | 3, 25 | oveq12d 7376 |
. . 3
โข (๐พ โ (0...๐) โ ((!โ(๐ + 1)) / ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ))) = (((!โ๐) ยท (๐ + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ + 1) โ ๐พ)))) |
27 | 1 | faccld 14190 |
. . . . 5
โข (๐พ โ (0...๐) โ (!โ๐) โ โ) |
28 | 27 | nncnd 12174 |
. . . 4
โข (๐พ โ (0...๐) โ (!โ๐) โ โ) |
29 | | nn0p1nn 12457 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
30 | 1, 29 | syl 17 |
. . . . 5
โข (๐พ โ (0...๐) โ (๐ + 1) โ โ) |
31 | 30 | nncnd 12174 |
. . . 4
โข (๐พ โ (0...๐) โ (๐ + 1) โ โ) |
32 | 16, 22 | nnmulcld 12211 |
. . . . 5
โข (๐พ โ (0...๐) โ ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ) |
33 | | nncn 12166 |
. . . . . 6
โข
(((!โ(๐
โ ๐พ)) ยท
(!โ๐พ)) โ โ
โ ((!โ(๐ โ
๐พ)) ยท (!โ๐พ)) โ
โ) |
34 | | nnne0 12192 |
. . . . . 6
โข
(((!โ(๐
โ ๐พ)) ยท
(!โ๐พ)) โ โ
โ ((!โ(๐ โ
๐พ)) ยท (!โ๐พ)) โ 0) |
35 | 33, 34 | jca 513 |
. . . . 5
โข
(((!โ(๐
โ ๐พ)) ยท
(!โ๐พ)) โ โ
โ (((!โ(๐
โ ๐พ)) ยท
(!โ๐พ)) โ โ
โง ((!โ(๐ โ
๐พ)) ยท (!โ๐พ)) โ 0)) |
36 | 32, 35 | syl 17 |
. . . 4
โข (๐พ โ (0...๐) โ (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ โง ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ 0)) |
37 | 20 | nnne0d 12208 |
. . . . 5
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ 0) |
38 | 21, 37 | jca 513 |
. . . 4
โข (๐พ โ (0...๐) โ (((๐ + 1) โ ๐พ) โ โ โง ((๐ + 1) โ ๐พ) โ 0)) |
39 | | divmuldiv 11860 |
. . . 4
โข
((((!โ๐)
โ โ โง (๐ +
1) โ โ) โง ((((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ โ โง ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) โ 0) โง (((๐ + 1) โ ๐พ) โ โ โง ((๐ + 1) โ ๐พ) โ 0))) โ (((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) = (((!โ๐) ยท (๐ + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ + 1) โ ๐พ)))) |
40 | 28, 31, 36, 38, 39 | syl22anc 838 |
. . 3
โข (๐พ โ (0...๐) โ (((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) = (((!โ๐) ยท (๐ + 1)) / (((!โ(๐ โ ๐พ)) ยท (!โ๐พ)) ยท ((๐ + 1) โ ๐พ)))) |
41 | 26, 40 | eqtr4d 2776 |
. 2
โข (๐พ โ (0...๐) โ ((!โ(๐ + 1)) / ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ))) = (((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) |
42 | | fzelp1 13499 |
. . 3
โข (๐พ โ (0...๐) โ ๐พ โ (0...(๐ + 1))) |
43 | | bcval2 14211 |
. . 3
โข (๐พ โ (0...(๐ + 1)) โ ((๐ + 1)C๐พ) = ((!โ(๐ + 1)) / ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ)))) |
44 | 42, 43 | syl 17 |
. 2
โข (๐พ โ (0...๐) โ ((๐ + 1)C๐พ) = ((!โ(๐ + 1)) / ((!โ((๐ + 1) โ ๐พ)) ยท (!โ๐พ)))) |
45 | | bcval2 14211 |
. . 3
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
46 | 45 | oveq1d 7373 |
. 2
โข (๐พ โ (0...๐) โ ((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) = (((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) |
47 | 41, 44, 46 | 3eqtr4d 2783 |
1
โข (๐พ โ (0...๐) โ ((๐ + 1)C๐พ) = ((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) |