Step |
Hyp |
Ref |
Expression |
1 |
|
divccncf.1 |
โข ๐น = ( ๐ฅ โ โ โฆ ( ๐ฅ / ๐ด ) ) |
2 |
|
divrec2 |
โข ( ( ๐ฅ โ โ โง ๐ด โ โ โง ๐ด โ 0 ) โ ( ๐ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐ฅ ) ) |
3 |
2
|
3expb |
โข ( ( ๐ฅ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐ฅ ) ) |
4 |
3
|
ancoms |
โข ( ( ( ๐ด โ โ โง ๐ด โ 0 ) โง ๐ฅ โ โ ) โ ( ๐ฅ / ๐ด ) = ( ( 1 / ๐ด ) ยท ๐ฅ ) ) |
5 |
4
|
mpteq2dva |
โข ( ( ๐ด โ โ โง ๐ด โ 0 ) โ ( ๐ฅ โ โ โฆ ( ๐ฅ / ๐ด ) ) = ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) ) |
6 |
1 5
|
eqtrid |
โข ( ( ๐ด โ โ โง ๐ด โ 0 ) โ ๐น = ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) ) |
7 |
|
reccl |
โข ( ( ๐ด โ โ โง ๐ด โ 0 ) โ ( 1 / ๐ด ) โ โ ) |
8 |
|
eqid |
โข ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) = ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) |
9 |
8
|
mulc1cncf |
โข ( ( 1 / ๐ด ) โ โ โ ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) โ ( โ โcnโ โ ) ) |
10 |
7 9
|
syl |
โข ( ( ๐ด โ โ โง ๐ด โ 0 ) โ ( ๐ฅ โ โ โฆ ( ( 1 / ๐ด ) ยท ๐ฅ ) ) โ ( โ โcnโ โ ) ) |
11 |
6 10
|
eqeltrd |
โข ( ( ๐ด โ โ โง ๐ด โ 0 ) โ ๐น โ ( โ โcnโ โ ) ) |