Metamath Proof Explorer

Theorem ax5seglem8

Description: Lemma for ax5seg . Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 . (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem8 ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 1 − 𝑇 ) · 𝐴 ) = ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) )
2 1 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) = ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) )
3 2 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) = ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) )
4 3 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) )
5 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝐴 − 𝐶 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) )
6 5 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝐴 − 𝐶 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) )
7 6 oveq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) = ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) )
8 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( 𝐴 − 𝐷 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) )
9 8 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝐴 − 𝐷 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) )
10 7 9 oveq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) = ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) )
11 10 oveq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) = ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) )
12 4 11 oveq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) )
13 12 eqeq2d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) ↔ ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ) )
14 oveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) )
15 oveq2 ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( 1 − 𝑇 ) = ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) )
16 15 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) = ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) )
17 oveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( 𝑇 · 𝐶 ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) )
18 16 17 oveq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) = ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) )
19 18 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) = ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) )
20 19 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) )
21 oveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) )
22 21 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) )
23 15 22 oveq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) = ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) )
24 20 23 oveq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) )
25 14 24 eqeq12d ⊢ ( 𝑇 = if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) → ( ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ↔ ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ) )
26 oveq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( 𝐶 − 𝐷 ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) )
27 26 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( 𝐶 − 𝐷 ) ↑ 2 ) = ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) )
28 27 oveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) ) )
29 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) )
30 29 oveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) = ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) )
31 30 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) = ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) )
32 31 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) )
33 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) )
34 33 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) )
35 34 oveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) )
36 35 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) )
37 36 oveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) = ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) )
38 32 37 oveq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) )
39 28 38 eqeq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) → ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐶 ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ↔ ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ) )
40 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) = ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) )
41 40 oveq1d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) = ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) )
42 41 oveq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) )
43 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) = ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) )
44 43 oveq1d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) = ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) )
45 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) = ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) )
46 45 oveq1d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) = ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) )
47 46 oveq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) )
48 47 oveq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) = ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) ) )
49 44 48 oveq12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) ) ) )
50 42 49 eqeq12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) → ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − 𝐷 ) ↑ 2 ) ) ) ) ↔ ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) ) ) ) )
51 0cn ⊢ 0 ∈ ℂ
52 51 elimel ⊢ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ∈ ℂ
53 51 elimel ⊢ if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ∈ ℂ
54 51 elimel ⊢ if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ∈ ℂ
55 51 elimel ⊢ if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ∈ ℂ
56 52 53 54 55 ax5seglem7 ⊢ ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) + ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) + ( ( 1 − if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) ) · ( ( if ( 𝑇 ∈ ℂ , 𝑇 , 0 ) · ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐶 ∈ ℂ , 𝐶 , 0 ) ) ↑ 2 ) ) − ( ( if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) − if ( 𝐷 ∈ ℂ , 𝐷 , 0 ) ) ↑ 2 ) ) ) )
57 13 25 39 50 56 dedth4h ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( 𝑇 · ( ( 𝐶 − 𝐷 ) ↑ 2 ) ) = ( ( ( ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐶 ) ) − 𝐷 ) ↑ 2 ) + ( ( 1 − 𝑇 ) · ( ( 𝑇 · ( ( 𝐴 − 𝐶 ) ↑ 2 ) ) − ( ( 𝐴 − 𝐷 ) ↑ 2 ) ) ) ) )