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

Proof

Step Hyp Ref Expression
1 iccss2 ⊢ C ∈ A B ∧ D ∈ A B → C D ⊆ A B
2 1 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → C D ⊆ A B
3 2 3adantr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → C D ⊆ A B
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C < D → C D ⊆ A B
5 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
6 5 sselda ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B → C ∈ ℝ
7 6 adantrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → C ∈ ℝ
8 5 sselda ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B → D ∈ ℝ
9 8 adantrl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → D ∈ ℝ
10 7 9 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → C ∈ ℝ ∧ D ∈ ℝ
11 10 3adantr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → C ∈ ℝ ∧ D ∈ ℝ
12 simpr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → T ∈ 0 1
13 11 12 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → C ∈ ℝ ∧ D ∈ ℝ ∧ T ∈ 0 1
14 lincmb01cmp ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ C < D ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ C D
15 14 ex ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ C < D → T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ C D
16 15 3expa ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ C < D → T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ C D
17 16 imp ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ C < D ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ C D
18 17 an32s ⊢ C ∈ ℝ ∧ D ∈ ℝ ∧ T ∈ 0 1 ∧ C < D → 1 − T ⁢ C + T ⁢ D ∈ C D
19 13 18 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C < D → 1 − T ⁢ C + T ⁢ D ∈ C D
20 4 19 sseldd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C < D → 1 − T ⁢ C + T ⁢ D ∈ A B
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 ⊢ 0 1 ⊆ ℝ
24 23 sseli ⊢ T ∈ 0 1 → T ∈ ℝ
25 24 recnd ⊢ T ∈ 0 1 → T ∈ ℂ
26 25 ad2antll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B ∧ T ∈ 0 1 → T ∈ ℂ
27 8 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B → D ∈ ℂ
28 27 adantrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B ∧ T ∈ 0 1 → 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 mulid2 ⊢ 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 ∈ A B ∧ T ∈ 0 1 → 1 − T ⁢ D + T ⁢ D = D
44 43 3adantr1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → 1 − T ⁢ D + T ⁢ D = D
45 22 44 sylan9eqr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C = D → 1 − T ⁢ C + T ⁢ D = D
46 simplr2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C = D → D ∈ A B
47 45 46 eqeltrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ C = D → 1 − T ⁢ C + T ⁢ D ∈ A B
48 iccss2 ⊢ D ∈ A B ∧ C ∈ A B → D C ⊆ A B
49 48 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ D ∈ A B ∧ C ∈ A B → D C ⊆ A B
50 49 ancom2s ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → D C ⊆ A B
51 50 3adantr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → D C ⊆ A B
52 51 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ D < C → D C ⊆ A B
53 9 7 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → D ∈ ℝ ∧ C ∈ ℝ
54 53 3adantr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → D ∈ ℝ ∧ C ∈ ℝ
55 54 12 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → D ∈ ℝ ∧ C ∈ ℝ ∧ T ∈ 0 1
56 iirev ⊢ T ∈ 0 1 → 1 − T ∈ 0 1
57 23 56 sselid ⊢ T ∈ 0 1 → 1 − T ∈ ℝ
58 57 recnd ⊢ T ∈ 0 1 → 1 − T ∈ ℂ
59 recn ⊢ C ∈ ℝ → C ∈ ℂ
60 mulcl ⊢ 1 − T ∈ ℂ ∧ C ∈ ℂ → 1 − T ⁢ C ∈ ℂ
61 58 59 60 syl2anr ⊢ C ∈ ℝ ∧ T ∈ 0 1 → 1 − T ⁢ C ∈ ℂ
62 61 adantll ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ T ∈ 0 1 → 1 − T ⁢ C ∈ ℂ
63 recn ⊢ D ∈ ℝ → D ∈ ℂ
64 mulcl ⊢ T ∈ ℂ ∧ D ∈ ℂ → T ⁢ D ∈ ℂ
65 25 63 64 syl2anr ⊢ D ∈ ℝ ∧ T ∈ 0 1 → T ⁢ D ∈ ℂ
66 65 adantlr ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ T ∈ 0 1 → T ⁢ D ∈ ℂ
67 62 66 addcomd ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D = T ⁢ D + 1 − T ⁢ C
68 67 3adantl3 ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → 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 ∈ 0 1 → T ⁢ D + 1 − T ⁢ C = 1 − 1 − T ⁢ D + 1 − T ⁢ C
75 74 adantl ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → T ⁢ D + 1 − T ⁢ C = 1 − 1 − T ⁢ D + 1 − T ⁢ C
76 68 75 eqtrd ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D = 1 − 1 − T ⁢ D + 1 − T ⁢ C
77 lincmb01cmp ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ 1 − T ∈ 0 1 → 1 − 1 − T ⁢ D + 1 − T ⁢ C ∈ D C
78 56 77 sylan2 ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → 1 − 1 − T ⁢ D + 1 − T ⁢ C ∈ D C
79 76 78 eqeltrd ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ D C
80 79 ex ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C → T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ D C
81 80 3expa ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C → T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ D C
82 81 imp ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ D < C ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ D C
83 82 an32s ⊢ D ∈ ℝ ∧ C ∈ ℝ ∧ T ∈ 0 1 ∧ D < C → 1 − T ⁢ C + T ⁢ D ∈ D C
84 55 83 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ D < C → 1 − T ⁢ C + T ⁢ D ∈ D C
85 52 84 sseldd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 ∧ D < C → 1 − T ⁢ C + T ⁢ D ∈ A B
86 7 9 lttri4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B → C < D ∨ C = D ∨ D < C
87 86 3adantr3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → C < D ∨ C = D ∨ D < C
88 20 47 85 87 mpjao3dan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ A B
89 88 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ → C ∈ A B ∧ D ∈ A B ∧ T ∈ 0 1 → 1 − T ⁢ C + T ⁢ D ∈ A B