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 ⊢A∈ℝ∧B∈ℝ→C∈AB∧D∈AB∧T∈01→1−T⁢C+T⁢D∈AB

Proof

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