Theorem 2itscplem1

Description: Lemma 1 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$$
Assertion	2itscplem1	$$⊢\phi \to E^2{B}^2+D^2{A}^2-2DAEB={\left(DA-EB\right)}^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	2	recnd	$$⊢\phi \to B\in ℂ$$
8	4	recnd	$$⊢\phi \to Y\in ℂ$$
9	7 8	subcld	$$⊢\phi \to B-Y\in ℂ$$
10	6 9	eqeltrid	$$⊢\phi \to E\in ℂ$$
11	10	sqcld	$$⊢\phi \to E^2\in ℂ$$
12	7	sqcld	$$⊢\phi \to B^2\in ℂ$$
13	11 12	mulcld	$$⊢\phi \to E^2{B}^2\in ℂ$$
14	3	recnd	$$⊢\phi \to X\in ℂ$$
15	1	recnd	$$⊢\phi \to A\in ℂ$$
16	14 15	subcld	$$⊢\phi \to X-A\in ℂ$$
17	5 16	eqeltrid	$$⊢\phi \to D\in ℂ$$
18	17	sqcld	$$⊢\phi \to D^2\in ℂ$$
19	15	sqcld	$$⊢\phi \to A^2\in ℂ$$
20	18 19	mulcld	$$⊢\phi \to D^2{A}^2\in ℂ$$
21		2cnd	$$⊢\phi \to 2\in ℂ$$
22	17 15	mulcld	$$⊢\phi \to DA\in ℂ$$
23	10 7	mulcld	$$⊢\phi \to EB\in ℂ$$
24	22 23	mulcld	$$⊢\phi \to DAEB\in ℂ$$
25	21 24	mulcld	$$⊢\phi \to 2DAEB\in ℂ$$
26	13 20 25	addsubassd	$$⊢\phi \to E^2{B}^2+D^2{A}^2-2DAEB=E^2{B}^2+D^2{A}^2-2DAEB$$
27	20 25	subcld	$$⊢\phi \to D^2{A}^2-2DAEB\in ℂ$$
28	13 27	addcomd	$$⊢\phi \to E^2{B}^2+D^2{A}^2-2DAEB=D^2{A}^2-2DAEB+E^2{B}^2$$
29	17 15	sqmuld	$$⊢\phi \to {DA}^2=D^2{A}^2$$
30	29	eqcomd	$$⊢\phi \to D^2{A}^2={DA}^2$$
31	30	oveq1d	$$⊢\phi \to D^2{A}^2-2DAEB={DA}^2-2DAEB$$
32	10 7	sqmuld	$$⊢\phi \to {EB}^2=E^2{B}^2$$
33	32	eqcomd	$$⊢\phi \to E^2{B}^2={EB}^2$$
34	31 33	oveq12d	$$⊢\phi \to D^2{A}^2-2DAEB+E^2{B}^2={DA}^2-2DAEB+{EB}^2$$
35	26 28 34	3eqtrd	$$⊢\phi \to E^2{B}^2+D^2{A}^2-2DAEB={DA}^2-2DAEB+{EB}^2$$
36		binom2sub	$$⊢\left(DA\in ℂ\wedge EB\in ℂ\right)\to {\left(DA-EB\right)}^2={DA}^2-2DAEB+{EB}^2$$
37	22 23 36	syl2anc	$$⊢\phi \to {\left(DA-EB\right)}^2={DA}^2-2DAEB+{EB}^2$$
38	35 37	eqtr4d	$$⊢\phi \to E^2{B}^2+D^2{A}^2-2DAEB={\left(DA-EB\right)}^2$$