Theorem icccvx

Description: A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	icccvx	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iccss2	⊢ ( ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 [,] 𝐵 ) )
2	1	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 [,] 𝐵 ) )
3	2	3adantr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 [,] 𝐵 ) )
4	3	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 < 𝐷 ) → ( 𝐶 [,] 𝐷 ) ⊆ ( 𝐴 [,] 𝐵 ) )
5		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
6	5	sselda	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℝ )
7	6	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐶 ∈ ℝ )
8	5	sselda	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐷 ∈ ℝ )
9	8	adantrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐷 ∈ ℝ )
10	7 9	jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) )
11	10	3adantr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) )
12		simpr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
13	11 12	jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) )
14		lincmb01cmp	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
15	14	ex	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐶 < 𝐷 ) → ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) ) )
16	15	3expa	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝐶 < 𝐷 ) → ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) ) )
17	16	imp	⊢ ( ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝐶 < 𝐷 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
18	17	an32s	⊢ ( ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ∧ 𝐶 < 𝐷 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
19	13 18	sylan	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 < 𝐷 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
20	4 19	sseldd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 < 𝐷 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
21		oveq2	⊢ ( 𝐶 = 𝐷 → ( ( 1 − 𝑇 ) · 𝐶 ) = ( ( 1 − 𝑇 ) · 𝐷 ) )
22	21	oveq1d	⊢ ( 𝐶 = 𝐷 → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) = ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) )
23		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
24	23	sseli	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
25	24	recnd	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℂ )
26	25	ad2antll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
27	8	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐷 ∈ ℂ )
28	27	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝐷 ∈ ℂ )
29		ax-1cn	⊢ 1 ∈ ℂ
30		npcan	⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( ( 1 − 𝑇 ) + 𝑇 ) = 1 )
31	29 30	mpan	⊢ ( 𝑇 ∈ ℂ → ( ( 1 − 𝑇 ) + 𝑇 ) = 1 )
32	31	adantr	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 1 − 𝑇 ) + 𝑇 ) = 1 )
33	32	oveq1d	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) + 𝑇 ) · 𝐷 ) = ( 1 · 𝐷 ) )
34		subcl	⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − 𝑇 ) ∈ ℂ )
35	29 34	mpan	⊢ ( 𝑇 ∈ ℂ → ( 1 − 𝑇 ) ∈ ℂ )
36	35	ancri	⊢ ( 𝑇 ∈ ℂ → ( ( 1 − 𝑇 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) )
37		adddir	⊢ ( ( ( 1 − 𝑇 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) + 𝑇 ) · 𝐷 ) = ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) )
38	37	3expa	⊢ ( ( ( ( 1 − 𝑇 ) ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ 𝐷 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) + 𝑇 ) · 𝐷 ) = ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) )
39	36 38	sylan	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) + 𝑇 ) · 𝐷 ) = ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) )
40		mullid	⊢ ( 𝐷 ∈ ℂ → ( 1 · 𝐷 ) = 𝐷 )
41	40	adantl	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 1 · 𝐷 ) = 𝐷 )
42	33 39 41	3eqtr3d	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) = 𝐷 )
43	26 28 42	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) = 𝐷 )
44	43	3adantr1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · 𝐷 ) + ( 𝑇 · 𝐷 ) ) = 𝐷 )
45	22 44	sylan9eqr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 = 𝐷 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) = 𝐷 )
46		simplr2	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 = 𝐷 ) → 𝐷 ∈ ( 𝐴 [,] 𝐵 ) )
47	45 46	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐶 = 𝐷 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
48		iccss2	⊢ ( ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐷 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐵 ) )
49	48	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐷 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐵 ) )
50	49	ancom2s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐷 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐵 ) )
51	50	3adantr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐷 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐵 ) )
52	51	adantr	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐷 < 𝐶 ) → ( 𝐷 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐵 ) )
53	9 7	jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
54	53	3adantr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
55	54 12	jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) )
56		iirev	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
57	23 56	sselid	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ℝ )
58	57	recnd	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ℂ )
59		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
60		mulcl	⊢ ( ( ( 1 − 𝑇 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 1 − 𝑇 ) · 𝐶 ) ∈ ℂ )
61	58 59 60	syl2anr	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐶 ) ∈ ℂ )
62	61	adantll	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐶 ) ∈ ℂ )
63		recn	⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ ℂ )
64		mulcl	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝑇 · 𝐷 ) ∈ ℂ )
65	25 63 64	syl2anr	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · 𝐷 ) ∈ ℂ )
66	65	adantlr	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · 𝐷 ) ∈ ℂ )
67	62 66	addcomd	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) = ( ( 𝑇 · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
68	67	3adantl3	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) = ( ( 𝑇 · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
69		nncan	⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
70	29 69	mpan	⊢ ( 𝑇 ∈ ℂ → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
71	70	eqcomd	⊢ ( 𝑇 ∈ ℂ → 𝑇 = ( 1 − ( 1 − 𝑇 ) ) )
72	71	oveq1d	⊢ ( 𝑇 ∈ ℂ → ( 𝑇 · 𝐷 ) = ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) )
73	72	oveq1d	⊢ ( 𝑇 ∈ ℂ → ( ( 𝑇 · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) = ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
74	25 73	syl	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( 𝑇 · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) = ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
75	74	adantl	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) = ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
76	68 75	eqtrd	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) = ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) )
77		lincmb01cmp	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
78	56 77	sylan2	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝐷 ) + ( ( 1 − 𝑇 ) · 𝐶 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
79	76 78	eqeltrd	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
80	79	ex	⊢ ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 < 𝐶 ) → ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) ) )
81	80	3expa	⊢ ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐷 < 𝐶 ) → ( 𝑇 ∈ ( 0 [,] 1 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) ) )
82	81	imp	⊢ ( ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐷 < 𝐶 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
83	82	an32s	⊢ ( ( ( ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ∧ 𝐷 < 𝐶 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
84	55 83	sylan	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐷 < 𝐶 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐷 [,] 𝐶 ) )
85	52 84	sseldd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝐷 < 𝐶 ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
86	7 9	lttri4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐶 < 𝐷 ∨ 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) )
87	86	3adantr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝐶 < 𝐷 ∨ 𝐶 = 𝐷 ∨ 𝐷 < 𝐶 ) )
88	20 47 85 87	mpjao3dan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
89	88	ex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )