Metamath Proof Explorer

Theorem 2itscplem2

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

Ref Expression
Hypotheses 2itscp.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2itscp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2itscp.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2itscp.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
2itscp.d ⊢ 𝐷 = ( 𝑋 − 𝐴 )
2itscp.e ⊢ 𝐸 = ( 𝐵 − 𝑌 )
2itscp.c ⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
Assertion 2itscplem2 ( 𝜑 → ( 𝐶 ↑ 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 2itscp.c ⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
8 7 oveq1i ⊢ ( 𝐶 ↑ 2 ) = ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 )
9 8 a1i ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) )
10 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
11 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
12 10 11 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
13 5 12 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
14 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
15 13 14 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐵 ) ∈ ℂ )
16 4 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
17 14 16 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℂ )
18 6 17 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
19 18 11 mulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐴 ) ∈ ℂ )
20 binom2 ⊢ ( ( ( 𝐷 · 𝐵 ) ∈ ℂ ∧ ( 𝐸 · 𝐴 ) ∈ ℂ ) → ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) = ( ( ( ( 𝐷 · 𝐵 ) ↑ 2 ) + ( 2 · ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) ) ) + ( ( 𝐸 · 𝐴 ) ↑ 2 ) ) )
21 15 19 20 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) = ( ( ( ( 𝐷 · 𝐵 ) ↑ 2 ) + ( 2 · ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) ) ) + ( ( 𝐸 · 𝐴 ) ↑ 2 ) ) )
22 13 14 sqmuld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐵 ) ↑ 2 ) = ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
23 mul4r ⊢ ( ( ( 𝐷 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐸 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ) → ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) )
24 13 14 18 11 23 syl22anc ⊢ ( 𝜑 → ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) = ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) )
25 24 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) ) = ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) )
26 22 25 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐷 · 𝐵 ) ↑ 2 ) + ( 2 · ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) ) ) = ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
27 18 11 sqmuld ⊢ ( 𝜑 → ( ( 𝐸 · 𝐴 ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
28 26 27 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐷 · 𝐵 ) ↑ 2 ) + ( 2 · ( ( 𝐷 · 𝐵 ) · ( 𝐸 · 𝐴 ) ) ) ) + ( ( 𝐸 · 𝐴 ) ↑ 2 ) ) = ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
29 9 21 28 3eqtrd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )