Metamath Proof Explorer


Theorem sqdivzi

Description: Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013)

Ref Expression
Hypotheses sqdivzi.1 A
sqdivzi.2 B
Assertion sqdivzi B0AB2=A2B2

Proof

Step Hyp Ref Expression
1 sqdivzi.1 A
2 sqdivzi.2 B
3 oveq2 B=ifB0B1AB=AifB0B1
4 3 oveq1d B=ifB0B1AB2=AifB0B12
5 oveq1 B=ifB0B1B2=ifB0B12
6 5 oveq2d B=ifB0B1A2B2=A2ifB0B12
7 4 6 eqeq12d B=ifB0B1AB2=A2B2AifB0B12=A2ifB0B12
8 ax-1cn 1
9 2 8 ifcli ifB0B1
10 elimne0 ifB0B10
11 1 9 10 sqdivi AifB0B12=A2ifB0B12
12 7 11 dedth B0AB2=A2B2