Metamath Proof Explorer
Description: Distribution of squaring over multiplication. (Contributed by NM, 3-Sep-1999)
|
|
Ref |
Expression |
|
Hypotheses |
sqval.1 |
โข ๐ด โ โ |
|
|
sqmul.2 |
โข ๐ต โ โ |
|
Assertion |
sqmuli |
โข ( ( ๐ด ยท ๐ต ) โ 2 ) = ( ( ๐ด โ 2 ) ยท ( ๐ต โ 2 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sqval.1 |
โข ๐ด โ โ |
2 |
|
sqmul.2 |
โข ๐ต โ โ |
3 |
|
sqmul |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ๐ด ยท ๐ต ) โ 2 ) = ( ( ๐ด โ 2 ) ยท ( ๐ต โ 2 ) ) ) |
4 |
1 2 3
|
mp2an |
โข ( ( ๐ด ยท ๐ต ) โ 2 ) = ( ( ๐ด โ 2 ) ยท ( ๐ต โ 2 ) ) |