Theorem 2itscplem2

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

	Ref	Expression
Hypotheses	2itscp.a	$$⊢\phi \to A\in ℝ$$
	2itscp.b	$$⊢\phi \to B\in ℝ$$
	2itscp.x	$$⊢\phi \to X\in ℝ$$
	2itscp.y	$$⊢\phi \to Y\in ℝ$$
	2itscp.d	$$⊢D=X-A$$
	2itscp.e	$$⊢E=B-Y$$
	2itscp.c	$$⊢C=DB+EA$$
Assertion	2itscplem2	$$⊢\phi \to C^2=D^2{B}^2+2DAEB+E^2{A}^2$$

Proof

Step	Hyp	Ref	Expression
1		2itscp.a	$$⊢\phi \to A\in ℝ$$
2		2itscp.b	$$⊢\phi \to B\in ℝ$$
3		2itscp.x	$$⊢\phi \to X\in ℝ$$
4		2itscp.y	$$⊢\phi \to Y\in ℝ$$
5		2itscp.d	$$⊢D=X-A$$
6		2itscp.e	$$⊢E=B-Y$$
7		2itscp.c	$$⊢C=DB+EA$$
8	7	oveq1i	$$⊢C^2={\left(DB+EA\right)}^2$$
9	8	a1i	$$⊢\phi \to C^2={\left(DB+EA\right)}^2$$
10	3	recnd	$$⊢\phi \to X\in ℂ$$
11	1	recnd	$$⊢\phi \to A\in ℂ$$
12	10 11	subcld	$$⊢\phi \to X-A\in ℂ$$
13	5 12	eqeltrid	$$⊢\phi \to D\in ℂ$$
14	2	recnd	$$⊢\phi \to B\in ℂ$$
15	13 14	mulcld	$$⊢\phi \to DB\in ℂ$$
16	4	recnd	$$⊢\phi \to Y\in ℂ$$
17	14 16	subcld	$$⊢\phi \to B-Y\in ℂ$$
18	6 17	eqeltrid	$$⊢\phi \to E\in ℂ$$
19	18 11	mulcld	$$⊢\phi \to EA\in ℂ$$
20		binom2	$$⊢\left(DB\in ℂ\wedge EA\in ℂ\right)\to {\left(DB+EA\right)}^2={DB}^2+2DBEA+{EA}^2$$
21	15 19 20	syl2anc	$$⊢\phi \to {\left(DB+EA\right)}^2={DB}^2+2DBEA+{EA}^2$$
22	13 14	sqmuld	$$⊢\phi \to {DB}^2=D^2{B}^2$$
23		mul4r	$$⊢\left(\left(D\in ℂ\wedge B\in ℂ\right)\wedge \left(E\in ℂ\wedge A\in ℂ\right)\right)\to DBEA=DAEB$$
24	13 14 18 11 23	syl22anc	$$⊢\phi \to DBEA=DAEB$$
25	24	oveq2d	$$⊢\phi \to 2DBEA=2DAEB$$
26	22 25	oveq12d	$$⊢\phi \to {DB}^2+2DBEA=D^2{B}^2+2DAEB$$
27	18 11	sqmuld	$$⊢\phi \to {EA}^2=E^2{A}^2$$
28	26 27	oveq12d	$$⊢\phi \to {DB}^2+2DBEA+{EA}^2=D^2{B}^2+2DAEB+E^2{A}^2$$
29	9 21 28	3eqtrd	$$⊢\phi \to C^2=D^2{B}^2+2DAEB+E^2{A}^2$$