Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqdivzi.1 | |
|
sqdivzi.2 | |
||
Assertion | sqdivzi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqdivzi.1 | |
|
2 | sqdivzi.2 | |
|
3 | oveq2 | |
|
4 | 3 | oveq1d | |
5 | oveq1 | |
|
6 | 5 | oveq2d | |
7 | 4 6 | eqeq12d | |
8 | ax-1cn | |
|
9 | 2 8 | ifcli | |
10 | elimne0 | |
|
11 | 1 9 10 | sqdivi | |
12 | 7 11 | dedth | |