Metamath Proof Explorer

Theorem itsclc0yqsollem1

Description: Lemma 1 for itsclc0yqsol . (Contributed by AV, 6-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
itsclc0yqsollem1.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion itsclc0yqsollem1 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) = ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
3 itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
4 itsclc0yqsollem1.d ⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
5 2 oveq1i ⊢ ( 𝑇 ↑ 2 ) = ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 )
6 2cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 2 ∈ ℂ )
7 simpl2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝐵 ∈ ℂ )
8 simpl3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝐶 ∈ ℂ )
9 7 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
10 6 9 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
11 sqneg ⊢ ( ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ → ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
12 10 11 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
13 6 9 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) )
14 sq2 ⊢ ( 2 ↑ 2 ) = 4
15 14 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 2 ↑ 2 ) = 4 )
16 7 8 sqmuld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐵 · 𝐶 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) )
17 15 16 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 2 ↑ 2 ) · ( ( 𝐵 · 𝐶 ) ↑ 2 ) ) = ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
18 12 13 17 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) ↑ 2 ) = ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
19 5 18 syl5eq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝑇 ↑ 2 ) = ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
20 1 3 oveq12i ⊢ ( 𝑄 · 𝑈 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
21 simpl1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝐴 ∈ ℂ )
22 21 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
23 7 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
24 22 23 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ )
25 8 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
26 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝑅 ∈ ℂ )
27 26 sqcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝑅 ↑ 2 ) ∈ ℂ )
28 22 27 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
29 24 25 28 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
30 22 23 25 adddird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝐶 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
31 22 23 28 adddird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
32 30 31 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) )
33 23 25 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
34 22 25 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
35 22 28 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
36 23 27 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
37 22 36 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ )
38 35 37 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ∈ ℂ )
39 34 33 addcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
40 23 22 27 mul12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
41 40 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
42 39 41 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) )
43 33 34 38 42 assraddsubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐵 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
44 29 32 43 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
45 20 44 syl5eq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝑄 · 𝑈 ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
46 45 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 4 · ( 𝑄 · 𝑈 ) ) = ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) )
47 19 46 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) = ( ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) )
48 4cn ⊢ 4 ∈ ℂ
49 48 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 4 ∈ ℂ )
50 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
51 50 sqcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
53 1 24 eqeltrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝑄 ∈ ℂ )
54 27 53 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℂ )
55 54 25 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℂ )
56 4 55 eqeltrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝐷 ∈ ℂ )
57 49 52 56 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) = ( 4 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
58 34 38 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ∈ ℂ )
59 33 33 58 subsub4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) )
60 33 subidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = 0 )
61 60 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( 0 − ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
62 0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 0 ∈ ℂ )
63 62 34 38 subsub2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 0 − ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( 0 + ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) )
64 38 34 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ )
65 64 addid2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 0 + ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
66 61 63 65 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
67 59 66 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
68 22 28 36 adddid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) )
69 22 23 27 adddird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) )
70 69 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) )
71 70 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) ) )
72 68 71 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) ) )
73 72 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
74 24 27 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ )
75 22 74 25 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) )
76 73 75 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) · ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) ) )
77 1 a1i ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
78 77 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) = ( ( 𝑅 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
79 27 24 mulcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑅 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) )
80 78 79 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) )
81 80 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) )
82 4 81 syl5eq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → 𝐷 = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) )
83 82 eqcomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) = 𝐷 )
84 83 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) · ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑅 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) · 𝐷 ) )
85 67 76 84 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) = ( ( 𝐴 ↑ 2 ) · 𝐷 ) )
86 85 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( 4 · ( ( 𝐴 ↑ 2 ) · 𝐷 ) ) )
87 33 58 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ∈ ℂ )
88 49 33 87 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) )
89 57 86 88 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 4 · ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) ) − ( 4 · ( ( ( 𝐵 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝐶 ↑ 2 ) ) − ( ( ( 𝐴 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝐵 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) ) = ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) )
90 47 89 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑅 ∈ ℂ ) → ( ( 𝑇 ↑ 2 ) − ( 4 · ( 𝑄 · 𝑈 ) ) ) = ( ( 4 · ( 𝐴 ↑ 2 ) ) · 𝐷 ) )