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

Proof

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