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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
2 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 0 ∈ ℝ )
3 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ )
4 elicc01 ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1 ) )
5 4 simp1bi ⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
6 5 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝑇 ∈ ℝ )
7 difrp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) )
8 7 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ+ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ+ )
10 eqid ⊢ ( 0 · ( 𝐵 − 𝐴 ) ) = ( 0 · ( 𝐵 − 𝐴 ) )
11 eqid ⊢ ( 1 · ( 𝐵 − 𝐴 ) ) = ( 1 · ( 𝐵 − 𝐴 ) )
12 10 11 iccdil ⊢ ( ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ ( 𝐵 − 𝐴 ) ∈ ℝ+ ) ) → ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) ) )
13 2 3 6 9 12 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) ) )
14 1 13 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) )
15 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝐵 ∈ ℝ )
16 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝐴 ∈ ℝ )
17 15 16 resubcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
18 17 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
19 18 mul02d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 0 · ( 𝐵 − 𝐴 ) ) = 0 )
20 18 mulid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 𝐵 − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
21 19 20 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 0 · ( 𝐵 − 𝐴 ) ) [,] ( 1 · ( 𝐵 − 𝐴 ) ) ) = ( 0 [,] ( 𝐵 − 𝐴 ) ) )
22 14 21 eleqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] ( 𝐵 − 𝐴 ) ) )
23 6 17 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ℝ )
24 eqid ⊢ ( 0 + 𝐴 ) = ( 0 + 𝐴 )
25 eqid ⊢ ( ( 𝐵 − 𝐴 ) + 𝐴 ) = ( ( 𝐵 − 𝐴 ) + 𝐴 )
26 24 25 iccshftr ⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝐵 − 𝐴 ) ∈ ℝ ) ∧ ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ) → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] ( 𝐵 − 𝐴 ) ) ↔ ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) ∈ ( ( 0 + 𝐴 ) [,] ( ( 𝐵 − 𝐴 ) + 𝐴 ) ) ) )
27 2 17 23 16 26 syl22anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ( 0 [,] ( 𝐵 − 𝐴 ) ) ↔ ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) ∈ ( ( 0 + 𝐴 ) [,] ( ( 𝐵 − 𝐴 ) + 𝐴 ) ) ) )
28 22 27 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) ∈ ( ( 0 + 𝐴 ) [,] ( ( 𝐵 − 𝐴 ) + 𝐴 ) ) )
29 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝑇 ∈ ℂ )
30 15 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝐵 ∈ ℂ )
31 29 30 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · 𝐵 ) ∈ ℂ )
32 16 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 𝐴 ∈ ℂ )
33 29 32 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · 𝐴 ) ∈ ℂ )
34 31 33 32 subadd23d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝑇 · 𝐵 ) − ( 𝑇 · 𝐴 ) ) + 𝐴 ) = ( ( 𝑇 · 𝐵 ) + ( 𝐴 − ( 𝑇 · 𝐴 ) ) ) )
35 29 30 32 subdid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 𝑇 · ( 𝐵 − 𝐴 ) ) = ( ( 𝑇 · 𝐵 ) − ( 𝑇 · 𝐴 ) ) )
36 35 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = ( ( ( 𝑇 · 𝐵 ) − ( 𝑇 · 𝐴 ) ) + 𝐴 ) )
37 1re ⊢ 1 ∈ ℝ
38 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
39 37 6 38 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑇 ) ∈ ℝ )
40 39 16 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐴 ) ∈ ℝ )
41 40 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐴 ) ∈ ℂ )
42 41 31 addcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( 𝑇 · 𝐵 ) + ( ( 1 − 𝑇 ) · 𝐴 ) ) )
43 1cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℂ )
44 43 29 32 subdird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐴 ) = ( ( 1 · 𝐴 ) − ( 𝑇 · 𝐴 ) ) )
45 32 mulid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 1 · 𝐴 ) = 𝐴 )
46 45 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 · 𝐴 ) − ( 𝑇 · 𝐴 ) ) = ( 𝐴 − ( 𝑇 · 𝐴 ) ) )
47 44 46 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑇 ) · 𝐴 ) = ( 𝐴 − ( 𝑇 · 𝐴 ) ) )
48 47 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · 𝐵 ) + ( ( 1 − 𝑇 ) · 𝐴 ) ) = ( ( 𝑇 · 𝐵 ) + ( 𝐴 − ( 𝑇 · 𝐴 ) ) ) )
49 42 48 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) = ( ( 𝑇 · 𝐵 ) + ( 𝐴 − ( 𝑇 · 𝐴 ) ) ) )
50 34 36 49 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + 𝐴 ) = ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) )
51 32 addid2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 0 + 𝐴 ) = 𝐴 )
52 30 32 npcand ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = 𝐵 )
53 51 52 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 0 + 𝐴 ) [,] ( ( 𝐵 − 𝐴 ) + 𝐴 ) ) = ( 𝐴 [,] 𝐵 ) )
54 28 50 53 3eltr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )