Metamath Proof Explorer


Theorem sqmul

Description: Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008)

Ref Expression
Assertion sqmul A B A B 2 = A 2 B 2

Proof

Step Hyp Ref Expression
1 2nn0 2 0
2 mulexp A B 2 0 A B 2 = A 2 B 2
3 1 2 mp3an3 A B A B 2 = A 2 B 2