Metamath Proof Explorer

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 − 𝑇 ) · 𝐶 ) + ( 𝑇 · 𝐷 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )