Metamath Proof Explorer

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 ) )