Step | Hyp | Ref
| Expression |
1 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...๐ด) โ (((๐ด โ ๐) + 1)...๐ด) โ Fin) |
2 | | elfzelz 13447 |
. . . . . . 7
โข (๐ โ (((๐ด โ ๐) + 1)...๐ด) โ ๐ โ โค) |
3 | 2 | zcnd 12613 |
. . . . . 6
โข (๐ โ (((๐ด โ ๐) + 1)...๐ด) โ ๐ โ โ) |
4 | 3 | adantl 483 |
. . . . 5
โข ((๐ โ (0...๐ด) โง ๐ โ (((๐ด โ ๐) + 1)...๐ด)) โ ๐ โ โ) |
5 | 1, 4 | fprodcl 15840 |
. . . 4
โข (๐ โ (0...๐ด) โ โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐ โ โ) |
6 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...๐ด) โ (1...(๐ด โ ๐)) โ Fin) |
7 | | elfznn 13476 |
. . . . . . 7
โข (๐ โ (1...(๐ด โ ๐)) โ ๐ โ โ) |
8 | 7 | adantl 483 |
. . . . . 6
โข ((๐ โ (0...๐ด) โง ๐ โ (1...(๐ด โ ๐))) โ ๐ โ โ) |
9 | 8 | nncnd 12174 |
. . . . 5
โข ((๐ โ (0...๐ด) โง ๐ โ (1...(๐ด โ ๐))) โ ๐ โ โ) |
10 | 6, 9 | fprodcl 15840 |
. . . 4
โข (๐ โ (0...๐ด) โ โ๐ โ (1...(๐ด โ ๐))๐ โ โ) |
11 | 8 | nnne0d 12208 |
. . . . 5
โข ((๐ โ (0...๐ด) โง ๐ โ (1...(๐ด โ ๐))) โ ๐ โ 0) |
12 | 6, 9, 11 | fprodn0 15867 |
. . . 4
โข (๐ โ (0...๐ด) โ โ๐ โ (1...(๐ด โ ๐))๐ โ 0) |
13 | 5, 10, 12 | divcan3d 11941 |
. . 3
โข (๐ โ (0...๐ด) โ ((โ๐ โ (1...(๐ด โ ๐))๐ ยท โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐) / โ๐ โ (1...(๐ด โ ๐))๐) = โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐) |
14 | | fznn0sub 13479 |
. . . . . . . 8
โข (๐ โ (0...๐ด) โ (๐ด โ ๐) โ
โ0) |
15 | 14 | nn0red 12479 |
. . . . . . 7
โข (๐ โ (0...๐ด) โ (๐ด โ ๐) โ โ) |
16 | 15 | ltp1d 12090 |
. . . . . 6
โข (๐ โ (0...๐ด) โ (๐ด โ ๐) < ((๐ด โ ๐) + 1)) |
17 | | fzdisj 13474 |
. . . . . 6
โข ((๐ด โ ๐) < ((๐ด โ ๐) + 1) โ ((1...(๐ด โ ๐)) โฉ (((๐ด โ ๐) + 1)...๐ด)) = โ
) |
18 | 16, 17 | syl 17 |
. . . . 5
โข (๐ โ (0...๐ด) โ ((1...(๐ด โ ๐)) โฉ (((๐ด โ ๐) + 1)...๐ด)) = โ
) |
19 | | nn0p1nn 12457 |
. . . . . . . 8
โข ((๐ด โ ๐) โ โ0 โ ((๐ด โ ๐) + 1) โ โ) |
20 | 14, 19 | syl 17 |
. . . . . . 7
โข (๐ โ (0...๐ด) โ ((๐ด โ ๐) + 1) โ โ) |
21 | | nnuz 12811 |
. . . . . . 7
โข โ =
(โคโฅโ1) |
22 | 20, 21 | eleqtrdi 2844 |
. . . . . 6
โข (๐ โ (0...๐ด) โ ((๐ด โ ๐) + 1) โ
(โคโฅโ1)) |
23 | 14 | nn0zd 12530 |
. . . . . . 7
โข (๐ โ (0...๐ด) โ (๐ด โ ๐) โ โค) |
24 | | elfzel2 13445 |
. . . . . . 7
โข (๐ โ (0...๐ด) โ ๐ด โ โค) |
25 | | elfzle1 13450 |
. . . . . . . 8
โข (๐ โ (0...๐ด) โ 0 โค ๐) |
26 | 24 | zred 12612 |
. . . . . . . . 9
โข (๐ โ (0...๐ด) โ ๐ด โ โ) |
27 | | elfzelz 13447 |
. . . . . . . . . 10
โข (๐ โ (0...๐ด) โ ๐ โ โค) |
28 | 27 | zred 12612 |
. . . . . . . . 9
โข (๐ โ (0...๐ด) โ ๐ โ โ) |
29 | 26, 28 | subge02d 11752 |
. . . . . . . 8
โข (๐ โ (0...๐ด) โ (0 โค ๐ โ (๐ด โ ๐) โค ๐ด)) |
30 | 25, 29 | mpbid 231 |
. . . . . . 7
โข (๐ โ (0...๐ด) โ (๐ด โ ๐) โค ๐ด) |
31 | | eluz2 12774 |
. . . . . . 7
โข (๐ด โ
(โคโฅโ(๐ด โ ๐)) โ ((๐ด โ ๐) โ โค โง ๐ด โ โค โง (๐ด โ ๐) โค ๐ด)) |
32 | 23, 24, 30, 31 | syl3anbrc 1344 |
. . . . . 6
โข (๐ โ (0...๐ด) โ ๐ด โ (โคโฅโ(๐ด โ ๐))) |
33 | | fzsplit2 13472 |
. . . . . 6
โข ((((๐ด โ ๐) + 1) โ
(โคโฅโ1) โง ๐ด โ (โคโฅโ(๐ด โ ๐))) โ (1...๐ด) = ((1...(๐ด โ ๐)) โช (((๐ด โ ๐) + 1)...๐ด))) |
34 | 22, 32, 33 | syl2anc 585 |
. . . . 5
โข (๐ โ (0...๐ด) โ (1...๐ด) = ((1...(๐ด โ ๐)) โช (((๐ด โ ๐) + 1)...๐ด))) |
35 | | fzfid 13884 |
. . . . 5
โข (๐ โ (0...๐ด) โ (1...๐ด) โ Fin) |
36 | | elfznn 13476 |
. . . . . . 7
โข (๐ โ (1...๐ด) โ ๐ โ โ) |
37 | 36 | nncnd 12174 |
. . . . . 6
โข (๐ โ (1...๐ด) โ ๐ โ โ) |
38 | 37 | adantl 483 |
. . . . 5
โข ((๐ โ (0...๐ด) โง ๐ โ (1...๐ด)) โ ๐ โ โ) |
39 | 18, 34, 35, 38 | fprodsplit 15854 |
. . . 4
โข (๐ โ (0...๐ด) โ โ๐ โ (1...๐ด)๐ = (โ๐ โ (1...(๐ด โ ๐))๐ ยท โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐)) |
40 | 39 | oveq1d 7373 |
. . 3
โข (๐ โ (0...๐ด) โ (โ๐ โ (1...๐ด)๐ / โ๐ โ (1...(๐ด โ ๐))๐) = ((โ๐ โ (1...(๐ด โ ๐))๐ ยท โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐) / โ๐ โ (1...(๐ด โ ๐))๐)) |
41 | 24 | zcnd 12613 |
. . . . . 6
โข (๐ โ (0...๐ด) โ ๐ด โ โ) |
42 | 27 | zcnd 12613 |
. . . . . 6
โข (๐ โ (0...๐ด) โ ๐ โ โ) |
43 | | 1cnd 11155 |
. . . . . 6
โข (๐ โ (0...๐ด) โ 1 โ โ) |
44 | 41, 42, 43 | subsubd 11545 |
. . . . 5
โข (๐ โ (0...๐ด) โ (๐ด โ (๐ โ 1)) = ((๐ด โ ๐) + 1)) |
45 | 44 | oveq1d 7373 |
. . . 4
โข (๐ โ (0...๐ด) โ ((๐ด โ (๐ โ 1))...๐ด) = (((๐ด โ ๐) + 1)...๐ด)) |
46 | 45 | prodeq1d 15809 |
. . 3
โข (๐ โ (0...๐ด) โ โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐ = โ๐ โ (((๐ด โ ๐) + 1)...๐ด)๐) |
47 | 13, 40, 46 | 3eqtr4rd 2784 |
. 2
โข (๐ โ (0...๐ด) โ โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐ = (โ๐ โ (1...๐ด)๐ / โ๐ โ (1...(๐ด โ ๐))๐)) |
48 | | fallfacval3 15900 |
. 2
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐) |
49 | | elfz3nn0 13541 |
. . . 4
โข (๐ โ (0...๐ด) โ ๐ด โ
โ0) |
50 | | fprodfac 15861 |
. . . 4
โข (๐ด โ โ0
โ (!โ๐ด) =
โ๐ โ (1...๐ด)๐) |
51 | 49, 50 | syl 17 |
. . 3
โข (๐ โ (0...๐ด) โ (!โ๐ด) = โ๐ โ (1...๐ด)๐) |
52 | | fprodfac 15861 |
. . . 4
โข ((๐ด โ ๐) โ โ0 โ
(!โ(๐ด โ ๐)) = โ๐ โ (1...(๐ด โ ๐))๐) |
53 | 14, 52 | syl 17 |
. . 3
โข (๐ โ (0...๐ด) โ (!โ(๐ด โ ๐)) = โ๐ โ (1...(๐ด โ ๐))๐) |
54 | 51, 53 | oveq12d 7376 |
. 2
โข (๐ โ (0...๐ด) โ ((!โ๐ด) / (!โ(๐ด โ ๐))) = (โ๐ โ (1...๐ด)๐ / โ๐ โ (1...(๐ด โ ๐))๐)) |
55 | 47, 48, 54 | 3eqtr4d 2783 |
1
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = ((!โ๐ด) / (!โ(๐ด โ ๐)))) |