Step |
Hyp |
Ref |
Expression |
1 |
|
rmyluc |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ( ๐ + 1 ) ) = ( ( 2 ยท ( ( ๐ด Yrm ๐ ) ยท ๐ด ) ) โ ( ๐ด Yrm ( ๐ โ 1 ) ) ) ) |
2 |
|
frmy |
โข Yrm : ( ( โคโฅ โ 2 ) ร โค ) โถ โค |
3 |
2
|
fovcl |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ๐ ) โ โค ) |
4 |
3
|
zcnd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ๐ ) โ โ ) |
5 |
|
eluzelcn |
โข ( ๐ด โ ( โคโฅ โ 2 ) โ ๐ด โ โ ) |
6 |
5
|
adantr |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ๐ด โ โ ) |
7 |
4 6
|
mulcomd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( ๐ด Yrm ๐ ) ยท ๐ด ) = ( ๐ด ยท ( ๐ด Yrm ๐ ) ) ) |
8 |
7
|
oveq2d |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( 2 ยท ( ( ๐ด Yrm ๐ ) ยท ๐ด ) ) = ( 2 ยท ( ๐ด ยท ( ๐ด Yrm ๐ ) ) ) ) |
9 |
|
2cnd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ 2 โ โ ) |
10 |
9 6 4
|
mulassd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐ ) ) = ( 2 ยท ( ๐ด ยท ( ๐ด Yrm ๐ ) ) ) ) |
11 |
8 10
|
eqtr4d |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( 2 ยท ( ( ๐ด Yrm ๐ ) ยท ๐ด ) ) = ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐ ) ) ) |
12 |
11
|
oveq1d |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( 2 ยท ( ( ๐ด Yrm ๐ ) ยท ๐ด ) ) โ ( ๐ด Yrm ( ๐ โ 1 ) ) ) = ( ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐ ) ) โ ( ๐ด Yrm ( ๐ โ 1 ) ) ) ) |
13 |
1 12
|
eqtrd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ( ๐ + 1 ) ) = ( ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐ ) ) โ ( ๐ด Yrm ( ๐ โ 1 ) ) ) ) |