Metamath Proof Explorer


Theorem sqdivi

Description: Distribution of square over division. (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypotheses sqval.1 A
sqmul.2 B
sqdiv.3 B0
Assertion sqdivi AB2=A2B2

Proof

Step Hyp Ref Expression
1 sqval.1 A
2 sqmul.2 B
3 sqdiv.3 B0
4 1 2 1 2 3 3 divmuldivi ABAB=AABB
5 1 2 3 divcli AB
6 5 sqvali AB2=ABAB
7 1 sqvali A2=AA
8 2 sqvali B2=BB
9 7 8 oveq12i A2B2=AABB
10 4 6 9 3eqtr4i AB2=A2B2