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∈01→1−T⁢A+T⁢B∈AB

Proof

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