Theorem ax5seglem7 27303

Description: Lemma for ax5seg 27306. 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 13937	. . . 4 ⊢ ((𝐶 − 𝐷)↑2) = (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2))
4	3	oveq2i 7286	. . 3 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = (𝑇 · (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2)))
5		ax5seglem7.2	. . . 4 ⊢ 𝑇 ∈ ℂ
6	1	sqcli 13898	. . . . 5 ⊢ (𝐶↑2) ∈ ℂ
7		2cn 12048	. . . . . 6 ⊢ 2 ∈ ℂ
8	1, 2	mulcli 10982	. . . . . 6 ⊢ (𝐶 · 𝐷) ∈ ℂ
9	7, 8	mulcli 10982	. . . . 5 ⊢ (2 · (𝐶 · 𝐷)) ∈ ℂ
10	6, 9	subcli 11297	. . . 4 ⊢ ((𝐶↑2) − (2 · (𝐶 · 𝐷))) ∈ ℂ
11	2	sqcli 13898	. . . 4 ⊢ (𝐷↑2) ∈ ℂ
12	5, 10, 11	adddii 10987	. . 3 ⊢ (𝑇 · (((𝐶↑2) − (2 · (𝐶 · 𝐷))) + (𝐷↑2))) = ((𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
13	5, 6, 9	subdii 11424	. . . 4 ⊢ (𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) = ((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷))))
14	13	oveq1i 7285	. . 3 ⊢ ((𝑇 · ((𝐶↑2) − (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
15	4, 12, 14	3eqtri 2770	. 2 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
16		ax-1cn 10929	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
17	16, 5	subcli 11297	. . . . . . . . . 10 ⊢ (1 − 𝑇) ∈ ℂ
18		ax5seglem7.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ ℂ
19	17, 18	mulcli 10982	. . . . . . . . 9 ⊢ ((1 − 𝑇) · 𝐴) ∈ ℂ
20	19	sqcli 13898	. . . . . . . 8 ⊢ (((1 − 𝑇) · 𝐴)↑2) ∈ ℂ
21	5, 1	mulcli 10982	. . . . . . . . . . 11 ⊢ (𝑇 · 𝐶) ∈ ℂ
22	21, 2	subcli 11297	. . . . . . . . . 10 ⊢ ((𝑇 · 𝐶) − 𝐷) ∈ ℂ
23	19, 22	mulcli 10982	. . . . . . . . 9 ⊢ (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) ∈ ℂ
24	7, 23	mulcli 10982	. . . . . . . 8 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) ∈ ℂ
25	20, 24	addcli 10981	. . . . . . 7 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) ∈ ℂ
26	21	sqcli 13898	. . . . . . . 8 ⊢ ((𝑇 · 𝐶)↑2) ∈ ℂ
27	26, 11	addcli 10981	. . . . . . 7 ⊢ (((𝑇 · 𝐶)↑2) + (𝐷↑2)) ∈ ℂ
28	25, 27	addcli 10981	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) ∈ ℂ
29	21, 2	mulcli 10982	. . . . . . 7 ⊢ ((𝑇 · 𝐶) · 𝐷) ∈ ℂ
30	7, 29	mulcli 10982	. . . . . 6 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) ∈ ℂ
31	5, 6	mulcli 10982	. . . . . . 7 ⊢ (𝑇 · (𝐶↑2)) ∈ ℂ
32	5, 11	mulcli 10982	. . . . . . 7 ⊢ (𝑇 · (𝐷↑2)) ∈ ℂ
33	31, 32	addcli 10981	. . . . . 6 ⊢ ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ
34		subadd23 11233	. . . . . 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 1460	. . . . 5 ⊢ (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) + ((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2)))) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))))
36	35	oveq1i 7285	. . . 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 13928	. . . . . . 7 ⊢ ((((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))↑2) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2))
38	19, 21, 2	addsubassi 11312	. . . . . . . 8 ⊢ ((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷) = (((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))
39	38	oveq1i 7285	. . . . . . 7 ⊢ (((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) = ((((1 − 𝑇) · 𝐴) + ((𝑇 · 𝐶) − 𝐷))↑2)
40	25, 27, 30	addsubassi 11312	. . . . . . . 8 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))))
41	21, 2	binom2subi 13937	. . . . . . . . . 10 ⊢ (((𝑇 · 𝐶) − 𝐷)↑2) = ((((𝑇 · 𝐶)↑2) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (𝐷↑2))
42	26, 11, 30	addsubi 11313	. . . . . . . . . 10 ⊢ ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))) = ((((𝑇 · 𝐶)↑2) − (2 · ((𝑇 · 𝐶) · 𝐷))) + (𝐷↑2))
43	41, 42	eqtr4i 2769	. . . . . . . . 9 ⊢ (((𝑇 · 𝐶) − 𝐷)↑2) = ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷)))
44	43	oveq2i 7286	. . . . . . . 8 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2)) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((((𝑇 · 𝐶)↑2) + (𝐷↑2)) − (2 · ((𝑇 · 𝐶) · 𝐷))))
45	40, 44	eqtr4i 2769	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶) − 𝐷)↑2))
46	37, 39, 45	3eqtr4i 2776	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) = ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷)))
47	18, 1	binom2subi 13937	. . . . . . . . . . . 12 ⊢ ((𝐴 − 𝐶)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2))
48	47	oveq2i 7286	. . . . . . . . . . 11 ⊢ (𝑇 · ((𝐴 − 𝐶)↑2)) = (𝑇 · (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2)))
49	18	sqcli 13898	. . . . . . . . . . . . 13 ⊢ (𝐴↑2) ∈ ℂ
50	18, 1	mulcli 10982	. . . . . . . . . . . . . 14 ⊢ (𝐴 · 𝐶) ∈ ℂ
51	7, 50	mulcli 10982	. . . . . . . . . . . . 13 ⊢ (2 · (𝐴 · 𝐶)) ∈ ℂ
52	49, 51	subcli 11297	. . . . . . . . . . . 12 ⊢ ((𝐴↑2) − (2 · (𝐴 · 𝐶))) ∈ ℂ
53	5, 52, 6	adddii 10987	. . . . . . . . . . 11 ⊢ (𝑇 · (((𝐴↑2) − (2 · (𝐴 · 𝐶))) + (𝐶↑2))) = ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2)))
54	48, 53	eqtri 2766	. . . . . . . . . 10 ⊢ (𝑇 · ((𝐴 − 𝐶)↑2)) = ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2)))
55	18, 2	binom2subi 13937	. . . . . . . . . 10 ⊢ ((𝐴 − 𝐷)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2))
56	54, 55	oveq12i 7287	. . . . . . . . 9 ⊢ ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2))) − (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2)))
57	5, 52	mulcli 10982	. . . . . . . . . 10 ⊢ (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) ∈ ℂ
58	18, 2	mulcli 10982	. . . . . . . . . . . 12 ⊢ (𝐴 · 𝐷) ∈ ℂ
59	7, 58	mulcli 10982	. . . . . . . . . . 11 ⊢ (2 · (𝐴 · 𝐷)) ∈ ℂ
60	49, 59	subcli 11297	. . . . . . . . . 10 ⊢ ((𝐴↑2) − (2 · (𝐴 · 𝐷))) ∈ ℂ
61	57, 31, 60, 11	addsub4i 11317	. . . . . . . . 9 ⊢ (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) + (𝑇 · (𝐶↑2))) − (((𝐴↑2) − (2 · (𝐴 · 𝐷))) + (𝐷↑2))) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))
62	56, 61	eqtri 2766	. . . . . . . 8 ⊢ ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)) = (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))
63	62	oveq2i 7286	. . . . . . 7 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))) = ((1 − 𝑇) · (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
64	57, 60	subcli 11297	. . . . . . . 8 ⊢ ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) ∈ ℂ
65	31, 11	subcli 11297	. . . . . . . 8 ⊢ ((𝑇 · (𝐶↑2)) − (𝐷↑2)) ∈ ℂ
66	17, 64, 65	adddii 10987	. . . . . . 7 ⊢ ((1 − 𝑇) · (((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) + ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
67	16, 5, 65	subdiri 11425	. . . . . . . . . 10 ⊢ ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) − (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))))
68	65	mulid2i 10980	. . . . . . . . . . 11 ⊢ (1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((𝑇 · (𝐶↑2)) − (𝐷↑2))
69	5, 31, 11	subdii 11424	. . . . . . . . . . 11 ⊢ (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))
70	68, 69	oveq12i 7287	. . . . . . . . . 10 ⊢ ((1 · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) − (𝑇 · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2))))
71	5, 31	mulcli 10982	. . . . . . . . . . . 12 ⊢ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ
72		subsub3 11253	. . . . . . . . . . . 12 ⊢ ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) ∈ ℂ ∧ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ ∧ (𝑇 · (𝐷↑2)) ∈ ℂ) → (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2)))))
73	65, 71, 32, 72	mp3an 1460	. . . . . . . . . . 11 ⊢ (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2))))
74	31, 32, 11	addsubi 11313	. . . . . . . . . . . 12 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) = (((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2)))
75	74	oveq1i 7285	. . . . . . . . . . 11 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = ((((𝑇 · (𝐶↑2)) − (𝐷↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (𝑇 · (𝐶↑2))))
76		subsub4 11254	. . . . . . . . . . . 12 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) ∈ ℂ ∧ (𝐷↑2) ∈ ℂ ∧ (𝑇 · (𝑇 · (𝐶↑2))) ∈ ℂ) → ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
77	33, 11, 71, 76	mp3an 1460	. . . . . . . . . . 11 ⊢ ((((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝐷↑2)) − (𝑇 · (𝑇 · (𝐶↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
78	73, 75, 77	3eqtr2i 2772	. . . . . . . . . 10 ⊢ (((𝑇 · (𝐶↑2)) − (𝐷↑2)) − ((𝑇 · (𝑇 · (𝐶↑2))) − (𝑇 · (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
79	67, 70, 78	3eqtri 2770	. . . . . . . . 9 ⊢ ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))
80	79	oveq2i 7286	. . . . . . . 8 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
81	17, 64	mulcli 10982	. . . . . . . . 9 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) ∈ ℂ
82	11, 71	addcli 10981	. . . . . . . . 9 ⊢ ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) ∈ ℂ
83		addsub12 11234	. . . . . . . . 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 1460	. . . . . . . 8 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
85	80, 84	eqtri 2766	. . . . . . 7 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) + ((1 − 𝑇) · ((𝑇 · (𝐶↑2)) − (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
86	63, 66, 85	3eqtri 2770	. . . . . 6 ⊢ ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))))
87	46, 86	oveq12i 7287	. . . . 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 11297	. . . . . 6 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) ∈ ℂ
89	81, 82	subcli 11297	. . . . . 6 ⊢ (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2))))) ∈ ℂ
90	88, 33, 89	addassi 10985	. . . . 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 2769	. . . 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 11297	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) ∈ ℂ
93	28, 89, 92	add32i 11198	. . . 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 2776	. . 3 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = (((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) + (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))))
95		subsub2 11249	. . . . . 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 1460	. . . . 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 10985	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2)))
98	25, 26	addcomi 11166	. . . . . . . . . 10 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) = (((𝑇 · 𝐶)↑2) + ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))))
99	5, 1	sqmuli 13901	. . . . . . . . . . . 12 ⊢ ((𝑇 · 𝐶)↑2) = ((𝑇↑2) · (𝐶↑2))
100	5	sqvali 13897	. . . . . . . . . . . . 13 ⊢ (𝑇↑2) = (𝑇 · 𝑇)
101	100	oveq1i 7285	. . . . . . . . . . . 12 ⊢ ((𝑇↑2) · (𝐶↑2)) = ((𝑇 · 𝑇) · (𝐶↑2))
102	5, 5, 6	mulassi 10986	. . . . . . . . . . . 12 ⊢ ((𝑇 · 𝑇) · (𝐶↑2)) = (𝑇 · (𝑇 · (𝐶↑2)))
103	99, 101, 102	3eqtri 2770	. . . . . . . . . . 11 ⊢ ((𝑇 · 𝐶)↑2) = (𝑇 · (𝑇 · (𝐶↑2)))
104	17, 18	sqmuli 13901	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · 𝐴)↑2) = (((1 − 𝑇)↑2) · (𝐴↑2))
105	17	sqvali 13897	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 𝑇)↑2) = ((1 − 𝑇) · (1 − 𝑇))
106	105	oveq1i 7285	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇)↑2) · (𝐴↑2)) = (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2))
107	17, 17, 49	mulassi 10986	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2)) = ((1 − 𝑇) · ((1 − 𝑇) · (𝐴↑2)))
108	16, 5, 49	subdiri 11425	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 − 𝑇) · (𝐴↑2)) = ((1 · (𝐴↑2)) − (𝑇 · (𝐴↑2)))
109	49	mulid2i 10980	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 · (𝐴↑2)) = (𝐴↑2)
110	109	oveq1i 7285	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 · (𝐴↑2)) − (𝑇 · (𝐴↑2))) = ((𝐴↑2) − (𝑇 · (𝐴↑2)))
111	108, 110	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((1 − 𝑇) · (𝐴↑2)) = ((𝐴↑2) − (𝑇 · (𝐴↑2)))
112	111	oveq2i 7286	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 𝑇) · ((1 − 𝑇) · (𝐴↑2))) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
113	107, 112	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · (1 − 𝑇)) · (𝐴↑2)) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
114	104, 106, 113	3eqtri 2770	. . . . . . . . . . . . . 14 ⊢ (((1 − 𝑇) · 𝐴)↑2) = ((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2))))
115	7, 19, 22	mul12i 11170	. . . . . . . . . . . . . . 15 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) = (((1 − 𝑇) · 𝐴) · (2 · ((𝑇 · 𝐶) − 𝐷)))
116	7, 22	mulcli 10982	. . . . . . . . . . . . . . . 16 ⊢ (2 · ((𝑇 · 𝐶) − 𝐷)) ∈ ℂ
117	17, 18, 116	mulassi 10986	. . . . . . . . . . . . . . 15 ⊢ (((1 − 𝑇) · 𝐴) · (2 · ((𝑇 · 𝐶) − 𝐷))) = ((1 − 𝑇) · (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷))))
118	18, 7	mulcomi 10983	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (2 · 𝐴)
119	118	oveq1i 7285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) · ((𝑇 · 𝐶) − 𝐷)) = ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷))
120	18, 7, 22	mulassi 10986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) · ((𝑇 · 𝐶) − 𝐷)) = (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))
121	119, 120	eqtr3i 2768	. . . . . . . . . . . . . . . . 17 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))
122	7, 18	mulcli 10982	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 · 𝐴) ∈ ℂ
123	122, 21, 2	subdii 11424	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = (((2 · 𝐴) · (𝑇 · 𝐶)) − ((2 · 𝐴) · 𝐷))
124	122, 5, 1	mul12i 11170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝐴) · (𝑇 · 𝐶)) = (𝑇 · ((2 · 𝐴) · 𝐶))
125	7, 18, 1	mulassi 10986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 𝐴) · 𝐶) = (2 · (𝐴 · 𝐶))
126	125	oveq2i 7286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑇 · ((2 · 𝐴) · 𝐶)) = (𝑇 · (2 · (𝐴 · 𝐶)))
127	124, 126	eqtri 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝐴) · (𝑇 · 𝐶)) = (𝑇 · (2 · (𝐴 · 𝐶)))
128	7, 18, 2	mulassi 10986	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝐴) · 𝐷) = (2 · (𝐴 · 𝐷))
129	127, 128	oveq12i 7287	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 · 𝐴) · (𝑇 · 𝐶)) − ((2 · 𝐴) · 𝐷)) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
130	123, 129	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((2 · 𝐴) · ((𝑇 · 𝐶) − 𝐷)) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
131	121, 130	eqtr3i 2768	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷))) = ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))
132	131	oveq2i 7286	. . . . . . . . . . . . . . 15 ⊢ ((1 − 𝑇) · (𝐴 · (2 · ((𝑇 · 𝐶) − 𝐷)))) = ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
133	115, 117, 132	3eqtri 2770	. . . . . . . . . . . . . 14 ⊢ (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))) = ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
134	114, 133	oveq12i 7287	. . . . . . . . . . . . 13 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = (((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2)))) + ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))))
135	5, 49	mulcli 10982	. . . . . . . . . . . . . . 15 ⊢ (𝑇 · (𝐴↑2)) ∈ ℂ
136	49, 135	subcli 11297	. . . . . . . . . . . . . 14 ⊢ ((𝐴↑2) − (𝑇 · (𝐴↑2))) ∈ ℂ
137	5, 51	mulcli 10982	. . . . . . . . . . . . . . 15 ⊢ (𝑇 · (2 · (𝐴 · 𝐶))) ∈ ℂ
138	137, 59	subcli 11297	. . . . . . . . . . . . . 14 ⊢ ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))) ∈ ℂ
139	17, 136, 138	adddii 10987	. . . . . . . . . . . . 13 ⊢ ((1 − 𝑇) · (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))) = (((1 − 𝑇) · ((𝐴↑2) − (𝑇 · (𝐴↑2)))) + ((1 − 𝑇) · ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))))
140	5, 49, 51	subdii 11424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) = ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))
141	140	oveq2i 7286	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))))
142	140, 57	eqeltrri 2836	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))) ∈ ℂ
143		sub32 11255	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴↑2) ∈ ℂ ∧ ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))) ∈ ℂ ∧ (2 · (𝐴 · 𝐷)) ∈ ℂ) → (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))))
144	49, 142, 59, 143	mp3an 1460	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶)))))
145	141, 144	eqtr4i 2769	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷)))
146		subsub 11251	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝑇 · (𝐴↑2)) ∈ ℂ ∧ (𝑇 · (2 · (𝐴 · 𝐶))) ∈ ℂ) → ((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))))
147	49, 135, 137, 146	mp3an 1460	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶))))
148	147	oveq1i 7285	. . . . . . . . . . . . . . 15 ⊢ (((𝐴↑2) − ((𝑇 · (𝐴↑2)) − (𝑇 · (2 · (𝐴 · 𝐶))))) − (2 · (𝐴 · 𝐷))) = ((((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))) − (2 · (𝐴 · 𝐷)))
149	136, 137, 59	addsubassi 11312	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴↑2) − (𝑇 · (𝐴↑2))) + (𝑇 · (2 · (𝐴 · 𝐶)))) − (2 · (𝐴 · 𝐷))) = (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))
150	145, 148, 149	3eqtrri 2771	. . . . . . . . . . . . . 14 ⊢ (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷)))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))))
151	150	oveq2i 7286	. . . . . . . . . . . . 13 ⊢ ((1 − 𝑇) · (((𝐴↑2) − (𝑇 · (𝐴↑2))) + ((𝑇 · (2 · (𝐴 · 𝐶))) − (2 · (𝐴 · 𝐷))))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
152	134, 139, 151	3eqtr2i 2772	. . . . . . . . . . . 12 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
153	57, 60	negsubdi2i 11307	. . . . . . . . . . . . 13 ⊢ -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))) = (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))))
154	153	oveq2i 7286	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) · -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) = ((1 − 𝑇) · (((𝐴↑2) − (2 · (𝐴 · 𝐷))) − (𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶))))))
155	17, 64	mulneg2i 11422	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) · -((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) = -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))
156	152, 154, 155	3eqtr2i 2772	. . . . . . . . . . 11 ⊢ ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) = -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))
157	103, 156	oveq12i 7287	. . . . . . . . . 10 ⊢ (((𝑇 · 𝐶)↑2) + ((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷))))) = ((𝑇 · (𝑇 · (𝐶↑2))) + -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
158	71, 81	negsubi 11299	. . . . . . . . . 10 ⊢ ((𝑇 · (𝑇 · (𝐶↑2))) + -((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) = ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
159	98, 157, 158	3eqtri 2770	. . . . . . . . 9 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) = ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
160	159	oveq2i 7286	. . . . . . . 8 ⊢ ((𝐷↑2) + (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2))) = ((𝐷↑2) + ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))))
161	25, 26	addcli 10981	. . . . . . . . 9 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) ∈ ℂ
162	161, 11	addcomi 11166	. . . . . . . 8 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = ((𝐷↑2) + (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)))
163	11, 71, 81	addsubassi 11312	. . . . . . . 8 ⊢ (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) = ((𝐷↑2) + ((𝑇 · (𝑇 · (𝐶↑2))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))))
164	160, 162, 163	3eqtr4i 2776	. . . . . . 7 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + ((𝑇 · 𝐶)↑2)) + (𝐷↑2)) = (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
165	97, 164	eqtr3i 2768	. . . . . 6 ⊢ (((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) = (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))
166	82, 81	subcli 11297	. . . . . . 7 ⊢ (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷)))))) ∈ ℂ
167	28, 166	subeq0i 11301	. . . . . 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 230	. . . . 5 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) − (((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))) − ((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))))) = 0
169	96, 168	eqtr3i 2768	. . . 4 ⊢ ((((((1 − 𝑇) · 𝐴)↑2) + (2 · (((1 − 𝑇) · 𝐴) · ((𝑇 · 𝐶) − 𝐷)))) + (((𝑇 · 𝐶)↑2) + (𝐷↑2))) + (((1 − 𝑇) · ((𝑇 · ((𝐴↑2) − (2 · (𝐴 · 𝐶)))) − ((𝐴↑2) − (2 · (𝐴 · 𝐷))))) − ((𝐷↑2) + (𝑇 · (𝑇 · (𝐶↑2)))))) = 0
170	5, 1, 2	mulassi 10986	. . . . . . . 8 ⊢ ((𝑇 · 𝐶) · 𝐷) = (𝑇 · (𝐶 · 𝐷))
171	170	oveq2i 7286	. . . . . . 7 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) = (2 · (𝑇 · (𝐶 · 𝐷)))
172	7, 5, 8	mul12i 11170	. . . . . . 7 ⊢ (2 · (𝑇 · (𝐶 · 𝐷))) = (𝑇 · (2 · (𝐶 · 𝐷)))
173	171, 172	eqtri 2766	. . . . . 6 ⊢ (2 · ((𝑇 · 𝐶) · 𝐷)) = (𝑇 · (2 · (𝐶 · 𝐷)))
174	173	oveq2i 7286	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (2 · (𝐶 · 𝐷))))
175	5, 9	mulcli 10982	. . . . . 6 ⊢ (𝑇 · (2 · (𝐶 · 𝐷))) ∈ ℂ
176	31, 32, 175	addsubi 11313	. . . . 5 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (𝑇 · (2 · (𝐶 · 𝐷)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
177	174, 176	eqtri 2766	. . . 4 ⊢ (((𝑇 · (𝐶↑2)) + (𝑇 · (𝐷↑2))) − (2 · ((𝑇 · 𝐶) · 𝐷))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
178	169, 177	oveq12i 7287	. . 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 11297	. . . . 5 ⊢ ((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) ∈ ℂ
180	179, 32	addcli 10981	. . . 4 ⊢ (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2))) ∈ ℂ
181	180	addid2i 11163	. . 3 ⊢ (0 + (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
182	94, 178, 181	3eqtri 2770	. 2 ⊢ ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2)))) = (((𝑇 · (𝐶↑2)) − (𝑇 · (2 · (𝐶 · 𝐷)))) + (𝑇 · (𝐷↑2)))
183	15, 182	eqtr4i 2769	1 ⊢ (𝑇 · ((𝐶 − 𝐷)↑2)) = ((((((1 − 𝑇) · 𝐴) + (𝑇 · 𝐶)) − 𝐷)↑2) + ((1 − 𝑇) · ((𝑇 · ((𝐴 − 𝐶)↑2)) − ((𝐴 − 𝐷)↑2))))

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   − cmin 11205  -cneg 11206  2c2 12028  ↑cexp 13782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-n0 12234  df-z 12320  df-uz 12583  df-seq 13722  df-exp 13783

This theorem is referenced by:  ax5seglem8  27304