# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({C}\in \left[{A},{B}\right]\wedge {D}\in \left[{A},{B}\right]\wedge {T}\in \left[0,1\right]\right)\to \left(1-{T}\right){C}+{T}{D}\in \left[{A},{B}\right]\right)$

### Proof

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