Step |
Hyp |
Ref |
Expression |
1 |
|
fprodreclf.kph |
โข โฒ ๐ ๐ |
2 |
|
fprodcl.a |
โข ( ๐ โ ๐ด โ Fin ) |
3 |
|
fprodrecl.b |
โข ( ( ๐ โง ๐ โ ๐ด ) โ ๐ต โ โ ) |
4 |
|
ax-resscn |
โข โ โ โ |
5 |
4
|
a1i |
โข ( ๐ โ โ โ โ ) |
6 |
|
remulcl |
โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ๐ฅ ยท ๐ฆ ) โ โ ) |
7 |
6
|
adantl |
โข ( ( ๐ โง ( ๐ฅ โ โ โง ๐ฆ โ โ ) ) โ ( ๐ฅ ยท ๐ฆ ) โ โ ) |
8 |
|
1red |
โข ( ๐ โ 1 โ โ ) |
9 |
1 5 7 2 3 8
|
fprodcllemf |
โข ( ๐ โ โ ๐ โ ๐ด ๐ต โ โ ) |