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