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	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 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	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 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	addlidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( 0 + 𝐴 ) = 𝐴 )
52	30 32	npcand	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = 𝐵 )
53	51 52	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( 0 + 𝐴 ) [,] ( ( 𝐵 − 𝐴 ) + 𝐴 ) ) = ( 𝐴 [,] 𝐵 ) )
54	28 50 53	3eltr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝐴 ) + ( 𝑇 · 𝐵 ) ) ∈ ( 𝐴 [,] 𝐵 ) )