Metamath Proof Explorer


Theorem sqabsadd

Description: Square of absolute value of sum. Proposition 10-3.7(g) of Gleason p. 133. (Contributed by NM, 21-Jan-2007)

Ref Expression
Assertion sqabsadd A B A + B 2 = A 2 + B 2 + 2 A B

Proof

Step Hyp Ref Expression
1 cjadd A B A + B = A + B
2 1 oveq2d A B A + B A + B = A + B A + B
3 cjcl A A
4 cjcl B B
5 3 4 anim12i A B A B
6 muladd A B A B A + B A + B = A A + B B + A B + A B
7 5 6 mpdan A B A + B A + B = A A + B B + A B + A B
8 2 7 eqtrd A B A + B A + B = A A + B B + A B + A B
9 addcl A B A + B
10 absvalsq A + B A + B 2 = A + B A + B
11 9 10 syl A B A + B 2 = A + B A + B
12 absvalsq A A 2 = A A
13 absvalsq B B 2 = B B
14 mulcom B B B B = B B
15 4 14 mpdan B B B = B B
16 13 15 eqtrd B B 2 = B B
17 12 16 oveqan12d A B A 2 + B 2 = A A + B B
18 mulcl A B A B
19 4 18 sylan2 A B A B
20 19 addcjd A B A B + A B = 2 A B
21 cjmul A B A B = A B
22 4 21 sylan2 A B A B = A B
23 cjcj B B = B
24 23 adantl A B B = B
25 24 oveq2d A B A B = A B
26 22 25 eqtrd A B A B = A B
27 26 oveq2d A B A B + A B = A B + A B
28 20 27 eqtr3d A B 2 A B = A B + A B
29 17 28 oveq12d A B A 2 + B 2 + 2 A B = A A + B B + A B + A B
30 8 11 29 3eqtr4d A B A + B 2 = A 2 + B 2 + 2 A B