Metamath Proof Explorer

Theorem lincmb01cmp

Description: A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion lincmb01cmp 
|- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> T e. ( 0 [,] 1 ) )
2 0red 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> 0 e. RR )
3 1red 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> 1 e. RR )
4 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
5 4 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
6 5 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> T e. RR )
7 difrp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
8 7 biimp3a 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ )
9 8 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( B - A ) e. RR+ )
10 eqid 
 |-  ( 0 x. ( B - A ) ) = ( 0 x. ( B - A ) )
11 eqid 
 |-  ( 1 x. ( B - A ) ) = ( 1 x. ( B - A ) )
12 10 11 iccdil 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( T e. RR /\ ( B - A ) e. RR+ ) ) -> ( T e. ( 0 [,] 1 ) <-> ( T x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
13 2 3 6 9 12 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T e. ( 0 [,] 1 ) <-> ( T x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
14 1 13 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) )
15 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> B e. RR )
16 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> A e. RR )
17 15 16 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( B - A ) e. RR )
18 17 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( B - A ) e. CC )
19 18 mul02d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( 0 x. ( B - A ) ) = 0 )
20 18 mullidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( 1 x. ( B - A ) ) = ( B - A ) )
21 19 20 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) = ( 0 [,] ( B - A ) ) )
22 14 21 eleqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. ( B - A ) ) e. ( 0 [,] ( B - A ) ) )
23 6 17 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. ( B - A ) ) e. RR )
24 eqid 
 |-  ( 0 + A ) = ( 0 + A )
25 eqid 
 |-  ( ( B - A ) + A ) = ( ( B - A ) + A )
26 24 25 iccshftr 
 |-  ( ( ( 0 e. RR /\ ( B - A ) e. RR ) /\ ( ( T x. ( B - A ) ) e. RR /\ A e. RR ) ) -> ( ( T x. ( B - A ) ) e. ( 0 [,] ( B - A ) ) <-> ( ( T x. ( B - A ) ) + A ) e. ( ( 0 + A ) [,] ( ( B - A ) + A ) ) ) )
27 2 17 23 16 26 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( T x. ( B - A ) ) e. ( 0 [,] ( B - A ) ) <-> ( ( T x. ( B - A ) ) + A ) e. ( ( 0 + A ) [,] ( ( B - A ) + A ) ) ) )
28 22 27 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( T x. ( B - A ) ) + A ) e. ( ( 0 + A ) [,] ( ( B - A ) + A ) ) )
29 6 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> T e. CC )
30 15 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> B e. CC )
31 29 30 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. B ) e. CC )
32 16 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> A e. CC )
33 29 32 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. A ) e. CC )
34 31 33 32 subadd23d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( T x. B ) - ( T x. A ) ) + A ) = ( ( T x. B ) + ( A - ( T x. A ) ) ) )
35 29 30 32 subdid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( T x. ( B - A ) ) = ( ( T x. B ) - ( T x. A ) ) )
36 35 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( T x. ( B - A ) ) + A ) = ( ( ( T x. B ) - ( T x. A ) ) + A ) )
37 1re 
 |-  1 e. RR
38 resubcl 
 |-  ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
39 37 6 38 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( 1 - T ) e. RR )
40 39 16 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 1 - T ) x. A ) e. RR )
41 40 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 1 - T ) x. A ) e. CC )
42 41 31 addcomd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) = ( ( T x. B ) + ( ( 1 - T ) x. A ) ) )
43 1cnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> 1 e. CC )
44 43 29 32 subdird 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 1 - T ) x. A ) = ( ( 1 x. A ) - ( T x. A ) ) )
45 32 mullidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( 1 x. A ) = A )
46 45 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 1 x. A ) - ( T x. A ) ) = ( A - ( T x. A ) ) )
47 44 46 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 1 - T ) x. A ) = ( A - ( T x. A ) ) )
48 47 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( T x. B ) + ( ( 1 - T ) x. A ) ) = ( ( T x. B ) + ( A - ( T x. A ) ) ) )
49 42 48 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) = ( ( T x. B ) + ( A - ( T x. A ) ) ) )
50 34 36 49 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( T x. ( B - A ) ) + A ) = ( ( ( 1 - T ) x. A ) + ( T x. B ) ) )
51 32 addlidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( 0 + A ) = A )
52 30 32 npcand 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( B - A ) + A ) = B )
53 51 52 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( 0 + A ) [,] ( ( B - A ) + A ) ) = ( A [,] B ) )
54 28 50 53 3eltr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) ) -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) )