Metamath Proof Explorer

Theorem 2itscplem3

Description: Lemma D 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 ⊢ 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) )
2itscp.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
2itscplem3.q ⊢ 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
2itscplem3.s ⊢ 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion 2itscplem3 ( 𝜑 → 𝑆 = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 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 2itscp.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
9 2itscplem3.q ⊢ 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) )
10 2itscplem3.s ⊢ 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
11 10 a1i ⊢ ( 𝜑 → 𝑆 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) )
12 9 a1i ⊢ ( 𝜑 → 𝑄 = ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
13 12 oveq2d ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) · 𝑄 ) = ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
14 8 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
15 14 sqcld ⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) ∈ ℂ )
16 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
17 4 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
18 16 17 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℂ )
19 6 18 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
20 19 sqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
21 3 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
22 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
23 21 22 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐴 ) ∈ ℂ )
24 5 23 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
25 24 sqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
26 20 25 addcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
27 15 26 mulcomd ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) · ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) )
28 20 25 15 adddird ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
29 13 27 28 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) · 𝑄 ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
30 1 2 3 4 5 6 7 2itscplem2 ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
31 29 30 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ) )
32 20 15 mulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
33 25 15 mulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
34 32 33 addcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
35 16 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
36 25 35 mulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
37 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
38 24 22 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝐴 ) ∈ ℂ )
39 19 16 mulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐵 ) ∈ ℂ )
40 38 39 mulcld ⊢ ( 𝜑 → ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ∈ ℂ )
41 37 40 mulcld ⊢ ( 𝜑 → ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ∈ ℂ )
42 34 36 41 subsub4d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) )
43 42 eqcomd ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) = ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
44 43 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
45 34 36 subcld ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
46 22 sqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
47 20 46 mulcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ∈ ℂ )
48 45 41 47 sub32d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
49 44 48 eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
50 36 41 addcld ⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ∈ ℂ )
51 34 50 47 subsub4d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ) )
52 32 33 36 addsubassd ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) )
53 25 15 35 subdid ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
54 53 eqcomd ⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
55 54 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
56 52 55 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
57 56 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
58 15 35 subcld ⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
59 25 58 mulcld ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ∈ ℂ )
60 32 59 47 addsubd ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
61 20 15 46 subdid ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
62 61 eqcomd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) )
63 62 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
64 57 60 63 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
65 64 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) − ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
66 49 51 65 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) − ( ( ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) + ( ( 𝐸 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) ) = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )
67 11 31 66 3eqtrd ⊢ ( 𝜑 → 𝑆 = ( ( ( ( 𝐸 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐴 ↑ 2 ) ) ) + ( ( 𝐷 ↑ 2 ) · ( ( 𝑅 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) − ( 2 · ( ( 𝐷 · 𝐴 ) · ( 𝐸 · 𝐵 ) ) ) ) )