Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
โข ( ๐ โ โค โ ๐ โ โ ) |
2 |
1
|
adantl |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ๐ โ โ ) |
3 |
2
|
2timesd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( 2 ยท ๐ ) = ( ๐ + ๐ ) ) |
4 |
3
|
oveq2d |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ( 2 ยท ๐ ) ) = ( ๐ด Yrm ( ๐ + ๐ ) ) ) |
5 |
|
rmyadd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค โง ๐ โ โค ) โ ( ๐ด Yrm ( ๐ + ๐ ) ) = ( ( ( ๐ด Yrm ๐ ) ยท ( ๐ด Xrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) ) |
6 |
5
|
3anidm23 |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ( ๐ + ๐ ) ) = ( ( ( ๐ด Yrm ๐ ) ยท ( ๐ด Xrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) ) |
7 |
|
2cnd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ 2 โ โ ) |
8 |
|
frmx |
โข Xrm : ( ( โคโฅ โ 2 ) ร โค ) โถ โ0 |
9 |
8
|
fovcl |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Xrm ๐ ) โ โ0 ) |
10 |
9
|
nn0cnd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Xrm ๐ ) โ โ ) |
11 |
|
frmy |
โข Yrm : ( ( โคโฅ โ 2 ) ร โค ) โถ โค |
12 |
11
|
fovcl |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ๐ ) โ โค ) |
13 |
12
|
zcnd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ๐ ) โ โ ) |
14 |
7 10 13
|
mulassd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( 2 ยท ( ๐ด Xrm ๐ ) ) ยท ( ๐ด Yrm ๐ ) ) = ( 2 ยท ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) ) |
15 |
10 13
|
mulcld |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) โ โ ) |
16 |
15
|
2timesd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( 2 ยท ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) = ( ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) ) |
17 |
10 13
|
mulcomd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) = ( ( ๐ด Yrm ๐ ) ยท ( ๐ด Xrm ๐ ) ) ) |
18 |
17
|
oveq1d |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) = ( ( ( ๐ด Yrm ๐ ) ยท ( ๐ด Xrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) ) |
19 |
14 16 18
|
3eqtrrd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ( ( ๐ด Yrm ๐ ) ยท ( ๐ด Xrm ๐ ) ) + ( ( ๐ด Xrm ๐ ) ยท ( ๐ด Yrm ๐ ) ) ) = ( ( 2 ยท ( ๐ด Xrm ๐ ) ) ยท ( ๐ด Yrm ๐ ) ) ) |
20 |
4 6 19
|
3eqtrd |
โข ( ( ๐ด โ ( โคโฅ โ 2 ) โง ๐ โ โค ) โ ( ๐ด Yrm ( 2 ยท ๐ ) ) = ( ( 2 ยท ( ๐ด Xrm ๐ ) ) ยท ( ๐ด Yrm ๐ ) ) ) |