Metamath Proof Explorer


Theorem 2itscplem2

Description: Lemma 2 for 2itscp . (Contributed by AV, 4-Mar-2023)

Ref Expression
Hypotheses 2itscp.a φ A
2itscp.b φ B
2itscp.x φ X
2itscp.y φ Y
2itscp.d D = X A
2itscp.e E = B Y
2itscp.c C = D B + E A
Assertion 2itscplem2 φ C 2 = D 2 B 2 + 2 D A E B + E 2 A 2

Proof

Step Hyp Ref Expression
1 2itscp.a φ A
2 2itscp.b φ B
3 2itscp.x φ X
4 2itscp.y φ Y
5 2itscp.d D = X A
6 2itscp.e E = B Y
7 2itscp.c C = D B + E A
8 7 oveq1i C 2 = D B + E A 2
9 8 a1i φ C 2 = D B + E A 2
10 3 recnd φ X
11 1 recnd φ A
12 10 11 subcld φ X A
13 5 12 eqeltrid φ D
14 2 recnd φ B
15 13 14 mulcld φ D B
16 4 recnd φ Y
17 14 16 subcld φ B Y
18 6 17 eqeltrid φ E
19 18 11 mulcld φ E A
20 binom2 D B E A D B + E A 2 = D B 2 + 2 D B E A + E A 2
21 15 19 20 syl2anc φ D B + E A 2 = D B 2 + 2 D B E A + E A 2
22 13 14 sqmuld φ D B 2 = D 2 B 2
23 mul4r D B E A D B E A = D A E B
24 13 14 18 11 23 syl22anc φ D B E A = D A E B
25 24 oveq2d φ 2 D B E A = 2 D A E B
26 22 25 oveq12d φ D B 2 + 2 D B E A = D 2 B 2 + 2 D A E B
27 18 11 sqmuld φ E A 2 = E 2 A 2
28 26 27 oveq12d φ D B 2 + 2 D B E A + E A 2 = D 2 B 2 + 2 D A E B + E 2 A 2
29 9 21 28 3eqtrd φ C 2 = D 2 B 2 + 2 D A E B + E 2 A 2