Theorem 2itscplem1

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

	Ref	Expression
Hypotheses	2itscp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	2itscp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	2itscp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	2itscp.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	2itscp.d	⊢ 𝐷 = ( 𝑋 − 𝐴 )
	2itscp.e	⊢ 𝐸 = ( 𝐵 − 𝑌 )
Assertion	2itscplem1	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2itscp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		2itscp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		2itscp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4		2itscp.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5		2itscp.d	⊢ 𝐷 = ( 𝑋 − 𝐴 )
6		2itscp.e	⊢ 𝐸 = ( 𝐵 − 𝑌 )
7	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
8	4	recnd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
9	7 8	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℂ )
10	6 9	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
11	10	sqcld	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
12	7	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
13	11 12	mulcld	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
14	3	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
15	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16	14 15	subcld	⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
17	5 16	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
18	17	sqcld	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
19	15	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
20	18 19	mulcld	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
21		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
22	17 15	mulcld	⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℂ )
23	10 7	mulcld	⊢ ( 𝜑 → ( 𝐸 · 𝐵 ) ∈ ℂ )
24	22 23	mulcld	⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ∈ ℂ )
25	21 24	mulcld	⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ∈ ℂ )
26	13 20 25	addsubassd	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) )
27	20 25	subcld	⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ∈ ℂ )
28	13 27	addcomd	⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) = ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
29	17 15	sqmuld	⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) ↑ 2 ) = ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
30	29	eqcomd	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( ( 𝐷 · 𝐴 ) ↑ 2 ) )
31	30	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( 𝐷 · 𝐴 ) ↑ 2 ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
32	10 7	sqmuld	⊢ ( 𝜑 → ( ( 𝐸 · 𝐵 ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
33	32	eqcomd	⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝐸 · 𝐵 ) ↑ 2 ) )
34	31 33	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) = ( ( ( ( 𝐷 · 𝐴 ) ↑ 2 ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 · 𝐵 ) ↑ 2 ) ) )
35	26 28 34	3eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( ( 𝐷 · 𝐴 ) ↑ 2 ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 · 𝐵 ) ↑ 2 ) ) )
36		binom2sub	⊢ ( ( ( 𝐷 · 𝐴 ) ∈ ℂ ∧ ( 𝐸 · 𝐵 ) ∈ ℂ ) → ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) = ( ( ( ( 𝐷 · 𝐴 ) ↑ 2 ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 · 𝐵 ) ↑ 2 ) ) )
37	22 23 36	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) = ( ( ( ( 𝐷 · 𝐴 ) ↑ 2 ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 · 𝐵 ) ↑ 2 ) ) )
38	35 37	eqtr4d	⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( 𝐷 · 𝐴 ) − ( 𝐸 · 𝐵 ) ) ↑ 2 ) )