Step |
Hyp |
Ref |
Expression |
1 |
|
risefallfaccllem.1 |
โข ๐ โ โ |
2 |
|
risefallfaccllem.2 |
โข 1 โ ๐ |
3 |
|
risefallfaccllem.3 |
โข ( ( ๐ฅ โ ๐ โง ๐ฆ โ ๐ ) โ ( ๐ฅ ยท ๐ฆ ) โ ๐ ) |
4 |
|
fallfaccllem.4 |
โข ( ( ๐ด โ ๐ โง ๐ โ โ0 ) โ ( ๐ด โ ๐ ) โ ๐ ) |
5 |
1
|
sseli |
โข ( ๐ด โ ๐ โ ๐ด โ โ ) |
6 |
|
fallfacval |
โข ( ( ๐ด โ โ โง ๐ โ โ0 ) โ ( ๐ด FallFac ๐ ) = โ ๐ โ ( 0 ... ( ๐ โ 1 ) ) ( ๐ด โ ๐ ) ) |
7 |
5 6
|
sylan |
โข ( ( ๐ด โ ๐ โง ๐ โ โ0 ) โ ( ๐ด FallFac ๐ ) = โ ๐ โ ( 0 ... ( ๐ โ 1 ) ) ( ๐ด โ ๐ ) ) |
8 |
1
|
a1i |
โข ( ๐ด โ ๐ โ ๐ โ โ ) |
9 |
3
|
adantl |
โข ( ( ๐ด โ ๐ โง ( ๐ฅ โ ๐ โง ๐ฆ โ ๐ ) ) โ ( ๐ฅ ยท ๐ฆ ) โ ๐ ) |
10 |
|
fzfid |
โข ( ๐ด โ ๐ โ ( 0 ... ( ๐ โ 1 ) ) โ Fin ) |
11 |
|
elfznn0 |
โข ( ๐ โ ( 0 ... ( ๐ โ 1 ) ) โ ๐ โ โ0 ) |
12 |
11 4
|
sylan2 |
โข ( ( ๐ด โ ๐ โง ๐ โ ( 0 ... ( ๐ โ 1 ) ) ) โ ( ๐ด โ ๐ ) โ ๐ ) |
13 |
2
|
a1i |
โข ( ๐ด โ ๐ โ 1 โ ๐ ) |
14 |
8 9 10 12 13
|
fprodcllem |
โข ( ๐ด โ ๐ โ โ ๐ โ ( 0 ... ( ๐ โ 1 ) ) ( ๐ด โ ๐ ) โ ๐ ) |
15 |
14
|
adantr |
โข ( ( ๐ด โ ๐ โง ๐ โ โ0 ) โ โ ๐ โ ( 0 ... ( ๐ โ 1 ) ) ( ๐ด โ ๐ ) โ ๐ ) |
16 |
7 15
|
eqeltrd |
โข ( ( ๐ด โ ๐ โง ๐ โ โ0 ) โ ( ๐ด FallFac ๐ ) โ ๐ ) |