Theorem ax5seglem7 28862

Description: Lemma for ax5seg 28865. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.)

Hypotheses

Ref	Expression
ax5seglem7.1	⊢ 𝐴 ∈ ℂ
ax5seglem7.2	⊢ 𝑇 ∈ ℂ
ax5seglem7.3	⊢ 𝐶 ∈ ℂ
ax5seglem7.4	⊢ 𝐷 ∈ ℂ

Assertion

Ref	Expression
ax5seglem7	⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))))

Proof of Theorem ax5seglem7

Step	Hyp	Ref	Expression
1		ax5seglem7.3	. . . . 5 ⊢ 𝐶 ∈ ℂ
2		ax5seglem7.4	. . . . 5 ⊢ 𝐷 ∈ ℂ
3	1, 2	binom2subi 14187	. . . 4 ⊢ ((𝐶 − 𝐷)↑2) = (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2))
4	3	oveq2i 7398	. . 3 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = (𝑇 · (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2)))
5		ax5seglem7.2	. . . 4 ⊢ 𝑇 ∈ ℂ
6	1	sqcli 14146	. . . . 5 ⊢ (𝐶↑2) ∈ ℂ
7		2cn 12261	. . . . . 6 ⊢ 2 ∈ ℂ
8	1, 2	mulcli 11181	. . . . . 6 ⊢ (𝐶 · 𝐷) ∈ ℂ
9	7, 8	mulcli 11181	. . . . 5 ⊢ (2 · (𝐶 · 𝐷)) ∈ ℂ
10	6, 9	subcli 11498	. . . 4 ⊢ ((𝐶↑2) − (2 · (𝐶 · 𝐷))) ∈ ℂ
11	2	sqcli 14146	. . . 4 ⊢ (𝐷↑2) ∈ ℂ
12	5, 10, 11	adddii 11186	. . 3 ⊢ (𝑇 · (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2))) = ((𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
13	5, 6, 9	subdii 11627	. . . 4 ⊢ (𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) = ((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷))))
14	13	oveq1i 7397	. . 3 ⊢ ((𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
15	4, 12, 14	3eqtri 2756	. 2 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
16		ax-1cn 11126	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
17	16, 5	subcli 11498	. . . . . . . . . 10 ⊢ (1 − 𝑇) ∈ ℂ
18		ax5seglem7.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ ℂ
19	17, 18	mulcli 11181	. . . . . . . . 9 ⊢ ((1 − 𝑇) · 𝐴) ∈ ℂ
20	19	sqcli 14146	. . . . . . . 8 ⊢ (((1 − 𝑇) · 𝐴)↑2) ∈ ℂ
21	5, 1	mulcli 11181	. . . . . . . . . . 11 ⊢ (𝑇 · 𝐶) ∈ ℂ
22	21, 2	subcli 11498	. . . . . . . . . 10 ⊢ ((𝑇 · 𝐶) − 𝐷) ∈ ℂ
23	19, 22	mulcli 11181	. . . . . . . . 9 ⊢ (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) ∈ ℂ
24	7, 23	mulcli 11181	. . . . . . . 8 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) ∈ ℂ
25	20, 24	addcli 11180	. . . . . . 7 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) ∈ ℂ
26	21	sqcli 14146	. . . . . . . 8 ⊢ ((𝑇 · 𝐶)↑2) ∈ ℂ
27	26, 11	addcli 11180	. . . . . . 7 ⊢ (((𝑇 · 𝐶)↑2) + (𝐷↑2)) ∈ ℂ
28	25, 27	addcli 11180	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) ∈ ℂ
29	21, 2	mulcli 11181	. . . . . . 7 ⊢ ((𝑇 · 𝐶) · 𝐷) ∈ ℂ
30	7, 29	mulcli 11181	. . . . . 6 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) ∈ ℂ
31	5, 6	mulcli 11181	. . . . . . 7 ⊢ (𝑇 · (𝐶↑2)) ∈ ℂ
32	5, 11	mulcli 11181	. . . . . . 7 ⊢ (𝑇 · (𝐷↑2)) ∈ ℂ
33	31, 32	addcli 11180	. . . . . 6 ⊢ ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ
34		subadd23 11433	. . . . . 6 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) ∈ ℂ ∧ (2 · ((𝑇 · 𝐶) · 𝐷)) ∈ ℂ ∧ ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ) → (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))))
35	28, 30, 33, 34	mp3an 1463	. . . . 5 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))))
36	35	oveq1i 7397	. . . 4 ⊢ ((((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
37	19, 22	binom2i 14177	. . . . . . 7 ⊢ ((((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))↑2) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2))
38	19, 21, 2	addsubassi 11513	. . . . . . . 8 ⊢ ((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷) = (((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))
39	38	oveq1i 7397	. . . . . . 7 ⊢ (((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) = ((((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))↑2)
40	25, 27, 30	addsubassi 11513	. . . . . . . 8 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))))
41	21, 2	binom2subi 14187	. . . . . . . . . 10 ⊢ (((𝑇 · 𝐶) − 𝐷)↑2) = ((((𝑇 · 𝐶)↑2) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (𝐷↑2))
42	26, 11, 30	addsubi 11514	. . . . . . . . . 10 ⊢ ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))) = ((((𝑇 · 𝐶)↑2) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (𝐷↑2))
43	41, 42	eqtr4i 2755	. . . . . . . . 9 ⊢ (((𝑇 · 𝐶) − 𝐷)↑2) = ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷)))
44	43	oveq2i 7398	. . . . . . . 8 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2)) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))))
45	40, 44	eqtr4i 2755	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2))
46	37, 39, 45	3eqtr4i 2762	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))
47	18, 1	binom2subi 14187	. . . . . . . . . . . 12 ⊢ ((𝐴 − 𝐶)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2))
48	47	oveq2i 7398	. . . . . . . . . . 11 ⊢ (𝑇 · ((𝐴 − 𝐶)↑2)) = (𝑇 · (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)))
49	18	sqcli 14146	. . . . . . . . . . . . 13 ⊢ (𝐴↑2) ∈ ℂ
50	18, 1	mulcli 11181	. . . . . . . . . . . . . 14 ⊢ (𝐴 · 𝐶) ∈ ℂ
51	7, 50	mulcli 11181	. . . . . . . . . . . . 13 ⊢ (2 · (𝐴 · 𝐶)) ∈ ℂ
52	49, 51	subcli 11498	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) − (2 · (𝐴 · 𝐶))) ∈ ℂ
53	5, 52, 6	adddii 11186	. . . . . . . . . . 11 ⊢ (𝑇 · (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2))) = ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2)))
54	48, 53	eqtri 2752	. . . . . . . . . 10 ⊢ (𝑇 · ((𝐴 − 𝐶)↑2)) = ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2)))
55	18, 2	binom2subi 14187	. . . . . . . . . 10 ⊢ ((𝐴 − 𝐷)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2))
56	54, 55	oveq12i 7399	. . . . . . . . 9 ⊢ ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2))) − (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2)))
57	5, 52	mulcli 11181	. . . . . . . . . 10 ⊢ (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) ∈ ℂ
58	18, 2	mulcli 11181	. . . . . . . . . . . 12 ⊢ (𝐴 · 𝐷) ∈ ℂ
59	7, 58	mulcli 11181	. . . . . . . . . . 11 ⊢ (2 · (𝐴 · 𝐷)) ∈ ℂ
60	49, 59	subcli 11498	. . . . . . . . . 10 ⊢ ((𝐴↑2) − (2 · (𝐴 · 𝐷))) ∈ ℂ
61	57, 31, 60, 11	addsub4i 11518	. . . . . . . . 9 ⊢ (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2))) − (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2))) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))
62	56, 61	eqtri 2752	. . . . . . . 8 ⊢ ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))
63	62	oveq2i 7398	. . . . . . 7 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))) = ((1 − 𝑇) · (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
64	57, 60	subcli 11498	. . . . . . . 8 ⊢ ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) ∈ ℂ
65	31, 11	subcli 11498	. . . . . . . 8 ⊢ ((𝑇 · (𝐶↑2)) − (𝐷↑2)) ∈ ℂ
66	17, 64, 65	adddii 11186	. . . . . . 7 ⊢ ((1 − 𝑇) · (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
67	16, 5, 65	subdiri 11628	. . . . . . . . . 10 ⊢ ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) − (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
68	65	mullidi 11179	. . . . . . . . . . 11 ⊢ (1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((𝑇 · (𝐶↑2)) − (𝐷↑2))
69	5, 31, 11	subdii 11627	. . . . . . . . . . 11 ⊢ (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))
70	68, 69	oveq12i 7399	. . . . . . . . . 10 ⊢ ((1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) − (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2))))
71	5, 31	mulcli 11181	. . . . . . . . . . . 12 ⊢ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ
72		subsub3 11454	. . . . . . . . . . . 12 ⊢ ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) ∈ ℂ ∧ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ ∧ (𝑇 · (𝐷↑2)) ∈ ℂ) → (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2)))))
73	65, 71, 32, 72	mp3an 1463	. . . . . . . . . . 11 ⊢ (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2))))
74	31, 32, 11	addsubi 11514	. . . . . . . . . . . 12 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) = (((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2)))
75	74	oveq1i 7397	. . . . . . . . . . 11 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2))))
76		subsub4 11455	. . . . . . . . . . . 12 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ ∧ (𝐷↑2) ∈ ℂ ∧ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ) → ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
77	33, 11, 71, 76	mp3an 1463	. . . . . . . . . . 11 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
78	73, 75, 77	3eqtr2i 2758	. . . . . . . . . 10 ⊢ (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
79	67, 70, 78	3eqtri 2756	. . . . . . . . 9 ⊢ ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
80	79	oveq2i 7398	. . . . . . . 8 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
81	17, 64	mulcli 11181	. . . . . . . . 9 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) ∈ ℂ
82	11, 71	addcli 11180	. . . . . . . . 9 ⊢ ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) ∈ ℂ
83		addsub12 11434	. . . . . . . . 9 ⊢ ((((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) ∈ ℂ ∧ ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ ∧ ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) ∈ ℂ) → (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))))
84	81, 33, 82, 83	mp3an 1463	. . . . . . . 8 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
85	80, 84	eqtri 2752	. . . . . . 7 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
86	63, 66, 85	3eqtri 2756	. . . . . 6 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
87	46, 86	oveq12i 7399	. . . . 5 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))))
88	28, 30	subcli 11498	. . . . . 6 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) ∈ ℂ
89	81, 82	subcli 11498	. . . . . 6 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))) ∈ ℂ
90	88, 33, 89	addassi 11184	. . . . 5 ⊢ ((((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))))
91	87, 90	eqtr4i 2755	. . . 4 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = ((((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
92	33, 30	subcli 11498	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) ∈ ℂ
93	28, 89, 92	add32i 11398	. . . 4 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
94	36, 91, 93	3eqtr4i 2762	. . 3 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))))
95		subsub2 11450	. . . . . 6 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) ∈ ℂ ∧ ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) ∈ ℂ ∧ ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) ∈ ℂ) → ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))))
96	28, 82, 81, 95	mp3an 1463	. . . . 5 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
97	25, 26, 11	addassi 11184	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2)))
98	25, 26	addcomi 11365	. . . . . . . . . 10 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) = (((𝑇 · 𝐶)↑2) + ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))))
99	5, 1	sqmuli 14149	. . . . . . . . . . . 12 ⊢ ((𝑇 · 𝐶)↑2) = ((𝑇↑2) · (𝐶↑2))
100	5	sqvali 14145	. . . . . . . . . . . . 13 ⊢ (𝑇↑2) = (𝑇 · 𝑇)
101	100	oveq1i 7397	. . . . . . . . . . . 12 ⊢ ((𝑇↑2) · (𝐶↑2)) = ((𝑇 · 𝑇) · (𝐶↑2))
102	5, 5, 6	mulassi 11185	. . . . . . . . . . . 12 ⊢ ((𝑇 · 𝑇) · (𝐶↑2)) = (𝑇 · (𝑇 · (𝐶↑2)))
103	99, 101, 102	3eqtri 2756	. . . . . . . . . . 11 ⊢ ((𝑇 · 𝐶)↑2) = (𝑇 · (𝑇 · (𝐶↑2)))
104	17, 18	sqmuli 14149	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · 𝐴)↑2) = (((1 − 𝑇)↑2) · (𝐴↑2))
105	17	sqvali 14145	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 𝑇)↑2) = ((1 − 𝑇) · (1 − 𝑇))
106	105	oveq1i 7397	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇)↑2) · (𝐴↑2)) = (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2))
107	17, 17, 49	mulassi 11185	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2)) = ((1 − 𝑇) · ((1 − 𝑇) · (𝐴↑2)))
108	16, 5, 49	subdiri 11628	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 − 𝑇) · (𝐴↑2)) = ((1 · (𝐴↑2)) − (𝑇 · (𝐴↑2)))
109	49	mullidi 11179	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 · (𝐴↑2)) = (𝐴↑2)
110	109	oveq1i 7397	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 · (𝐴↑2)) − (𝑇 · (𝐴↑2))) = ((𝐴↑2) − (𝑇 · (𝐴↑2)))
111	108, 110	eqtri 2752	. . . . . . . . . . . . . . . . 17 ⊢ ((1 − 𝑇) · (𝐴↑2)) = ((𝐴↑2) − (𝑇 · (𝐴↑2)))
112	111	oveq2i 7398	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 𝑇) · ((1 − 𝑇) · (𝐴↑2))) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
113	107, 112	eqtri 2752	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2)) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
114	104, 106, 113	3eqtri 2756	. . . . . . . . . . . . . 14 ⊢ (((1 − 𝑇) · 𝐴)↑2) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
115	7, 19, 22	mul12i 11369	. . . . . . . . . . . . . . 15 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) = (((1 − 𝑇) · 𝐴) · (2 · ((𝑇 · 𝐶) − 𝐷)))
116	7, 22	mulcli 11181	. . . . . . . . . . . . . . . 16 ⊢ (2 · ((𝑇 · 𝐶) − 𝐷)) ∈ ℂ
117	17, 18, 116	mulassi 11185	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · 𝐴) · (2 · ((𝑇 · 𝐶) − 𝐷))) = ((1 − 𝑇) · (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷))))
118	18, 7	mulcomi 11182	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (2 · 𝐴)
119	118	oveq1i 7397	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) · ((𝑇 · 𝐶) − 𝐷)) = ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷))
120	18, 7, 22	mulassi 11185	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) · ((𝑇 · 𝐶) − 𝐷)) = (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))
121	119, 120	eqtr3i 2754	. . . . . . . . . . . . . . . . 17 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))
122	7, 18	mulcli 11181	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 𝐴) ∈ ℂ
123	122, 21, 2	subdii 11627	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = (((2 · 𝐴) · (𝑇 · 𝐶)) − ((2 · 𝐴) · 𝐷))
124	122, 5, 1	mul12i 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝐴) · (𝑇 · 𝐶)) = (𝑇 · ((2 · 𝐴) · 𝐶))
125	7, 18, 1	mulassi 11185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 𝐴) · 𝐶) = (2 · (𝐴 · 𝐶))
126	125	oveq2i 7398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 · ((2 · 𝐴) · 𝐶)) = (𝑇 · (2 · (𝐴 · 𝐶)))
127	124, 126	eqtri 2752	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝐴) · (𝑇 · 𝐶)) = (𝑇 · (2 · (𝐴 · 𝐶)))
128	7, 18, 2	mulassi 11185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝐴) · 𝐷) = (2 · (𝐴 · 𝐷))
129	127, 128	oveq12i 7399	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝐴) · (𝑇 · 𝐶)) − ((2 · 𝐴) · 𝐷)) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
130	123, 129	eqtri 2752	. . . . . . . . . . . . . . . . 17 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
131	121, 130	eqtr3i 2754	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷))) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
132	131	oveq2i 7398	. . . . . . . . . . . . . . 15 ⊢ ((1 − 𝑇) · (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))) = ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
133	115, 117, 132	3eqtri 2756	. . . . . . . . . . . . . 14 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) = ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
134	114, 133	oveq12i 7399	. . . . . . . . . . . . 13 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = (((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2)))) + ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))))
135	5, 49	mulcli 11181	. . . . . . . . . . . . . . 15 ⊢ (𝑇 · (𝐴↑2)) ∈ ℂ
136	49, 135	subcli 11498	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑2) − (𝑇 · (𝐴↑2))) ∈ ℂ
137	5, 51	mulcli 11181	. . . . . . . . . . . . . . 15 ⊢ (𝑇 · (2 · (𝐴 · 𝐶))) ∈ ℂ
138	137, 59	subcli 11498	. . . . . . . . . . . . . 14 ⊢ ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))) ∈ ℂ
139	17, 136, 138	adddii 11186	. . . . . . . . . . . . 13 ⊢ ((1 − 𝑇) · (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))) = (((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2)))) + ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))))
140	5, 49, 51	subdii 11627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) = ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))
141	140	oveq2i 7398	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))))
142	140, 57	eqeltrri 2825	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))) ∈ ℂ
143		sub32 11456	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴↑2) ∈ ℂ ∧ ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))) ∈ ℂ ∧ (2 · (𝐴 · 𝐷)) ∈ ℂ) → (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))))
144	49, 142, 59, 143	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))))
145	141, 144	eqtr4i 2755	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷)))
146		subsub 11452	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝑇 · (𝐴↑2)) ∈ ℂ ∧ (𝑇 · (2 · (𝐴 · 𝐶))) ∈ ℂ) → ((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))))
147	49, 135, 137, 146	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶))))
148	147	oveq1i 7397	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = ((((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))) − (2 · (𝐴 · 𝐷)))
149	136, 137, 59	addsubassi 11513	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
150	145, 148, 149	3eqtrri 2757	. . . . . . . . . . . . . 14 ⊢ (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))))
151	150	oveq2i 7398	. . . . . . . . . . . . 13 ⊢ ((1 − 𝑇) · (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
152	134, 139, 151	3eqtr2i 2758	. . . . . . . . . . . 12 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
153	57, 60	negsubdi2i 11508	. . . . . . . . . . . . 13 ⊢ -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))))
154	153	oveq2i 7398	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) · -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
155	17, 64	mulneg2i 11625	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) · -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) = -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))
156	152, 154, 155	3eqtr2i 2758	. . . . . . . . . . 11 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))
157	103, 156	oveq12i 7399	. . . . . . . . . 10 ⊢ (((𝑇 · 𝐶)↑2) + ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))))) = ((𝑇 · (𝑇 · (𝐶↑2))) + -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
158	71, 81	negsubi 11500	. . . . . . . . . 10 ⊢ ((𝑇 · (𝑇 · (𝐶↑2))) + -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) = ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
159	98, 157, 158	3eqtri 2756	. . . . . . . . 9 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) = ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
160	159	oveq2i 7398	. . . . . . . 8 ⊢ ((𝐷↑2) + (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2))) = ((𝐷↑2) + ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))))
161	25, 26	addcli 11180	. . . . . . . . 9 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) ∈ ℂ
162	161, 11	addcomi 11365	. . . . . . . 8 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = ((𝐷↑2) + (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)))
163	11, 71, 81	addsubassi 11513	. . . . . . . 8 ⊢ (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) = ((𝐷↑2) + ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))))
164	160, 162, 163	3eqtr4i 2762	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
165	97, 164	eqtr3i 2754	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) = (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
166	82, 81	subcli 11498	. . . . . . 7 ⊢ (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) ∈ ℂ
167	28, 166	subeq0i 11502	. . . . . 6 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))) = 0 ↔ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) = (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))))
168	165, 167	mpbir 231	. . . . 5 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))) = 0
169	96, 168	eqtr3i 2754	. . . 4 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = 0
170	5, 1, 2	mulassi 11185	. . . . . . . 8 ⊢ ((𝑇 · 𝐶) · 𝐷) = (𝑇 · (𝐶 · 𝐷))
171	170	oveq2i 7398	. . . . . . 7 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) = (2 · (𝑇 · (𝐶 · 𝐷)))
172	7, 5, 8	mul12i 11369	. . . . . . 7 ⊢ (2 · (𝑇 · (𝐶 · 𝐷))) = (𝑇 · (2 · (𝐶 · 𝐷)))
173	171, 172	eqtri 2752	. . . . . 6 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) = (𝑇 · (2 · (𝐶 · 𝐷)))
174	173	oveq2i 7398	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (2 · (𝐶 · 𝐷))))
175	5, 9	mulcli 11181	. . . . . 6 ⊢ (𝑇 · (2 · (𝐶 · 𝐷))) ∈ ℂ
176	31, 32, 175	addsubi 11514	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (2 · (𝐶 · 𝐷)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
177	174, 176	eqtri 2752	. . . 4 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
178	169, 177	oveq12i 7399	. . 3 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))) = (0 + (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2))))
179	31, 175	subcli 11498	. . . . 5 ⊢ ((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) ∈ ℂ
180	179, 32	addcli 11180	. . . 4 ⊢ (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2))) ∈ ℂ
181	180	addlidi 11362	. . 3 ⊢ (0 + (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
182	94, 178, 181	3eqtri 2756	. 2 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
183	15, 182	eqtr4i 2755	1 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))))

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073   − cmin 11405  -cneg 11406  2c2 12241  ↑cexp 14026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-n0 12443  df-z 12530  df-uz 12794  df-seq 13967  df-exp 14027

This theorem is referenced by:  ax5seglem8  28863