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 e. RR /\ B e. RR ) -> ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. C ) + ( T x. D ) ) e. ( A [,] B ) ) )

Proof

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