Step | Hyp | Ref
| Expression |
1 | | negcl 11406 |
. . . . . . 7
โข (๐ โ โ โ -๐ โ
โ) |
2 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0)
โ -๐ โ
โ) |
3 | | elfznn 13476 |
. . . . . . . 8
โข (๐ โ (1...๐) โ ๐ โ โ) |
4 | | nnm1nn0 12459 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
5 | 3, 4 | syl 17 |
. . . . . . 7
โข (๐ โ (1...๐) โ (๐ โ 1) โ
โ0) |
6 | 5 | nn0cnd 12480 |
. . . . . 6
โข (๐ โ (1...๐) โ (๐ โ 1) โ โ) |
7 | | subcl 11405 |
. . . . . 6
โข ((-๐ โ โ โง (๐ โ 1) โ โ)
โ (-๐ โ (๐ โ 1)) โ
โ) |
8 | 2, 6, 7 | syl2an 597 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ (-๐ โ (๐ โ 1)) โ โ) |
9 | 8 | mulm1d 11612 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ (-1 ยท (-๐ โ (๐ โ 1))) = -(-๐ โ (๐ โ 1))) |
10 | | simpll 766 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ ๐ โ โ) |
11 | 6 | adantl 483 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ (๐ โ 1) โ โ) |
12 | 10, 11 | negdi2d 11531 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ -(๐ + (๐ โ 1)) = (-๐ โ (๐ โ 1))) |
13 | 12 | negeqd 11400 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ --(๐ + (๐ โ 1)) = -(-๐ โ (๐ โ 1))) |
14 | | simpl 484 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ) |
15 | | addcl 11138 |
. . . . . 6
โข ((๐ โ โ โง (๐ โ 1) โ โ)
โ (๐ + (๐ โ 1)) โ
โ) |
16 | 14, 6, 15 | syl2an 597 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ (๐ + (๐ โ 1)) โ โ) |
17 | 16 | negnegd 11508 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ --(๐ + (๐ โ 1)) = (๐ + (๐ โ 1))) |
18 | 9, 13, 17 | 3eqtr2rd 2780 |
. . 3
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ (๐ + (๐ โ 1)) = (-1 ยท (-๐ โ (๐ โ 1)))) |
19 | 18 | prodeq2dv 15811 |
. 2
โข ((๐ โ โ โง ๐ โ โ0)
โ โ๐ โ
(1...๐)(๐ + (๐ โ 1)) = โ๐ โ (1...๐)(-1 ยท (-๐ โ (๐ โ 1)))) |
20 | | risefacval2 15898 |
. 2
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ RiseFac ๐) = โ๐ โ (1...๐)(๐ + (๐ โ 1))) |
21 | | fzfi 13883 |
. . . . . . 7
โข
(1...๐) โ
Fin |
22 | | neg1cn 12272 |
. . . . . . 7
โข -1 โ
โ |
23 | | fprodconst 15866 |
. . . . . . 7
โข
(((1...๐) โ Fin
โง -1 โ โ) โ โ๐ โ (1...๐)-1 = (-1โ(โฏโ(1...๐)))) |
24 | 21, 22, 23 | mp2an 691 |
. . . . . 6
โข
โ๐ โ
(1...๐)-1 =
(-1โ(โฏโ(1...๐))) |
25 | | hashfz1 14252 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
26 | 25 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ0
โ (-1โ(โฏโ(1...๐))) = (-1โ๐)) |
27 | 24, 26 | eqtr2id 2786 |
. . . . 5
โข (๐ โ โ0
โ (-1โ๐) =
โ๐ โ (1...๐)-1) |
28 | 27 | adantl 483 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (-1โ๐) =
โ๐ โ (1...๐)-1) |
29 | | fallfacval2 15899 |
. . . . 5
โข ((-๐ โ โ โง ๐ โ โ0)
โ (-๐ FallFac ๐) = โ๐ โ (1...๐)(-๐ โ (๐ โ 1))) |
30 | 1, 29 | sylan 581 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (-๐ FallFac ๐) = โ๐ โ (1...๐)(-๐ โ (๐ โ 1))) |
31 | 28, 30 | oveq12d 7376 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ ((-1โ๐)
ยท (-๐ FallFac ๐)) = (โ๐ โ (1...๐)-1 ยท โ๐ โ (1...๐)(-๐ โ (๐ โ 1)))) |
32 | | fzfid 13884 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (1...๐) โ
Fin) |
33 | 22 | a1i 11 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ โ (1...๐)) โ -1 โ
โ) |
34 | 32, 33, 8 | fprodmul 15848 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ โ๐ โ
(1...๐)(-1 ยท (-๐ โ (๐ โ 1))) = (โ๐ โ (1...๐)-1 ยท โ๐ โ (1...๐)(-๐ โ (๐ โ 1)))) |
35 | 31, 34 | eqtr4d 2776 |
. 2
โข ((๐ โ โ โง ๐ โ โ0)
โ ((-1โ๐)
ยท (-๐ FallFac ๐)) = โ๐ โ (1...๐)(-1 ยท (-๐ โ (๐ โ 1)))) |
36 | 19, 20, 35 | 3eqtr4d 2783 |
1
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ RiseFac ๐) = ((-1โ๐) ยท (-๐ FallFac ๐))) |