Step | Hyp | Ref
| Expression |
1 | | nn0cn 12428 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
2 | 1 | 2timesd 12401 |
. . . . . . 7
โข (๐ โ โ0
โ (2 ยท ๐) =
(๐ + ๐)) |
3 | 2 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ0
โ (-1โ(2 ยท ๐)) = (-1โ(๐ + ๐))) |
4 | | nn0z 12529 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
5 | | m1expeven 14021 |
. . . . . . 7
โข (๐ โ โค โ
(-1โ(2 ยท ๐)) =
1) |
6 | 4, 5 | syl 17 |
. . . . . 6
โข (๐ โ โ0
โ (-1โ(2 ยท ๐)) = 1) |
7 | | neg1cn 12272 |
. . . . . . . 8
โข -1 โ
โ |
8 | | expadd 14016 |
. . . . . . . 8
โข ((-1
โ โ โง ๐
โ โ0 โง ๐ โ โ0) โ
(-1โ(๐ + ๐)) = ((-1โ๐) ยท (-1โ๐))) |
9 | 7, 8 | mp3an1 1449 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (-1โ(๐ + ๐)) = ((-1โ๐) ยท (-1โ๐))) |
10 | 9 | anidms 568 |
. . . . . 6
โข (๐ โ โ0
โ (-1โ(๐ + ๐)) = ((-1โ๐) ยท (-1โ๐))) |
11 | 3, 6, 10 | 3eqtr3rd 2782 |
. . . . 5
โข (๐ โ โ0
โ ((-1โ๐)
ยท (-1โ๐)) =
1) |
12 | 11 | adantl 483 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ ((-1โ๐)
ยท (-1โ๐)) =
1) |
13 | | negneg 11456 |
. . . . . 6
โข (๐ โ โ โ --๐ = ๐) |
14 | 13 | adantr 482 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ --๐ = ๐) |
15 | 14 | oveq1d 7373 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (--๐ FallFac ๐) = (๐ FallFac ๐)) |
16 | 12, 15 | oveq12d 7376 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (((-1โ๐)
ยท (-1โ๐))
ยท (--๐ FallFac ๐)) = (1 ยท (๐ FallFac ๐))) |
17 | | expcl 13991 |
. . . . . 6
โข ((-1
โ โ โง ๐
โ โ0) โ (-1โ๐) โ โ) |
18 | 7, 17 | mpan 689 |
. . . . 5
โข (๐ โ โ0
โ (-1โ๐) โ
โ) |
19 | 18 | adantl 483 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (-1โ๐) โ
โ) |
20 | | negcl 11406 |
. . . . . 6
โข (๐ โ โ โ -๐ โ
โ) |
21 | 20 | negcld 11504 |
. . . . 5
โข (๐ โ โ โ --๐ โ
โ) |
22 | | fallfaccl 15904 |
. . . . 5
โข ((--๐ โ โ โง ๐ โ โ0)
โ (--๐ FallFac ๐) โ
โ) |
23 | 21, 22 | sylan 581 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (--๐ FallFac ๐) โ
โ) |
24 | 19, 19, 23 | mulassd 11183 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (((-1โ๐)
ยท (-1โ๐))
ยท (--๐ FallFac ๐)) = ((-1โ๐) ยท ((-1โ๐) ยท (--๐ FallFac ๐)))) |
25 | | fallfaccl 15904 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ FallFac ๐) โ
โ) |
26 | 25 | mulid2d 11178 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (1 ยท (๐
FallFac ๐)) = (๐ FallFac ๐)) |
27 | 16, 24, 26 | 3eqtr3rd 2782 |
. 2
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ FallFac ๐) = ((-1โ๐) ยท ((-1โ๐) ยท (--๐ FallFac ๐)))) |
28 | | risefallfac 15912 |
. . . 4
โข ((-๐ โ โ โง ๐ โ โ0)
โ (-๐ RiseFac ๐) = ((-1โ๐) ยท (--๐ FallFac ๐))) |
29 | 20, 28 | sylan 581 |
. . 3
โข ((๐ โ โ โง ๐ โ โ0)
โ (-๐ RiseFac ๐) = ((-1โ๐) ยท (--๐ FallFac ๐))) |
30 | 29 | oveq2d 7374 |
. 2
โข ((๐ โ โ โง ๐ โ โ0)
โ ((-1โ๐)
ยท (-๐ RiseFac ๐)) = ((-1โ๐) ยท ((-1โ๐) ยท (--๐ FallFac ๐)))) |
31 | 27, 30 | eqtr4d 2776 |
1
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ FallFac ๐) = ((-1โ๐) ยท (-๐ RiseFac ๐))) |