Description: Distribution of square over division. (Contributed by NM, 20-Aug-2001)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqval.1 | |
|
sqmul.2 | |
||
sqdiv.3 | |
||
Assertion | sqdivi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqval.1 | |
|
2 | sqmul.2 | |
|
3 | sqdiv.3 | |
|
4 | 1 2 1 2 3 3 | divmuldivi | |
5 | 1 2 3 | divcli | |
6 | 5 | sqvali | |
7 | 1 | sqvali | |
8 | 2 | sqvali | |
9 | 7 8 | oveq12i | |
10 | 4 6 9 | 3eqtr4i | |