Theorem lincmb01cmp 10238

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.)

Assertion

Ref	Expression
lincmb01cmp	⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))

Proof of Theorem lincmb01cmp

Step	Hyp	Ref	Expression
1		simpr 110	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝑇 ∈ (0[,]1))
2		0re 8179	. . . . . . 7 ⊢ 0 ∈ ℝ
3	2	a1i 9	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 0 ∈ ℝ)
4		1re 8178	. . . . . . 7 ⊢ 1 ∈ ℝ
5	4	a1i 9	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 1 ∈ ℝ)
6	2, 4	elicc2i 10174	. . . . . . . 8 ⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1))
7	6	simp1bi 1038	. . . . . . 7 ⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈ ℝ)
8	7	adantl 277	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝑇 ∈ ℝ)
9		difrp 9927	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ+))
10	9	biimp3a 1381	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → (𝐵 − 𝐴) ∈ ℝ+)
11	10	adantr 276	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝐵 − 𝐴) ∈ ℝ+)
12		eqid 2231	. . . . . . 7 ⊢ (0 · (𝐵 − 𝐴)) = (0 · (𝐵 − 𝐴))
13		eqid 2231	. . . . . . 7 ⊢ (1 · (𝐵 − 𝐴)) = (1 · (𝐵 − 𝐴))
14	12, 13	iccdil 10233	. . . . . 6 ⊢ (((0 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ+)) → (𝑇 ∈ (0[,]1) ↔ (𝑇 · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴)))))
15	3, 5, 8, 11, 14	syl22anc 1274	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 ∈ (0[,]1) ↔ (𝑇 · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴)))))
16	1, 15	mpbid 147	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · (𝐵 − 𝐴)) ∈ ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴))))
17		simpl2 1027	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝐵 ∈ ℝ)
18		simpl1 1026	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝐴 ∈ ℝ)
19	17, 18	resubcld 8560	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝐵 − 𝐴) ∈ ℝ)
20	19	recnd 8208	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝐵 − 𝐴) ∈ ℂ)
21	20	mul02d 8571	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (0 · (𝐵 − 𝐴)) = 0)
22	20	mulid2d 8198	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (1 · (𝐵 − 𝐴)) = (𝐵 − 𝐴))
23	21, 22	oveq12d 6036	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((0 · (𝐵 − 𝐴))[,](1 · (𝐵 − 𝐴))) = (0[,](𝐵 − 𝐴)))
24	16, 23	eleqtrd 2310	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · (𝐵 − 𝐴)) ∈ (0[,](𝐵 − 𝐴)))
25	8, 19	remulcld 8210	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · (𝐵 − 𝐴)) ∈ ℝ)
26		eqid 2231	. . . . 5 ⊢ (0 + 𝐴) = (0 + 𝐴)
27		eqid 2231	. . . . 5 ⊢ ((𝐵 − 𝐴) + 𝐴) = ((𝐵 − 𝐴) + 𝐴)
28	26, 27	iccshftr 10229	. . . 4 ⊢ (((0 ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ) ∧ ((𝑇 · (𝐵 − 𝐴)) ∈ ℝ ∧ 𝐴 ∈ ℝ)) → ((𝑇 · (𝐵 − 𝐴)) ∈ (0[,](𝐵 − 𝐴)) ↔ ((𝑇 · (𝐵 − 𝐴)) + 𝐴) ∈ ((0 + 𝐴)[,]((𝐵 − 𝐴) + 𝐴))))
29	3, 19, 25, 18, 28	syl22anc 1274	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝑇 · (𝐵 − 𝐴)) ∈ (0[,](𝐵 − 𝐴)) ↔ ((𝑇 · (𝐵 − 𝐴)) + 𝐴) ∈ ((0 + 𝐴)[,]((𝐵 − 𝐴) + 𝐴))))
30	24, 29	mpbid 147	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝑇 · (𝐵 − 𝐴)) + 𝐴) ∈ ((0 + 𝐴)[,]((𝐵 − 𝐴) + 𝐴)))
31	8	recnd 8208	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝑇 ∈ ℂ)
32	17	recnd 8208	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝐵 ∈ ℂ)
33	31, 32	mulcld 8200	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · 𝐵) ∈ ℂ)
34	18	recnd 8208	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
35	31, 34	mulcld 8200	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · 𝐴) ∈ ℂ)
36	33, 35, 34	subadd23d 8512	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((𝑇 · 𝐵) − (𝑇 · 𝐴)) + 𝐴) = ((𝑇 · 𝐵) + (𝐴 − (𝑇 · 𝐴))))
37	31, 32, 34	subdid 8593	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (𝑇 · (𝐵 − 𝐴)) = ((𝑇 · 𝐵) − (𝑇 · 𝐴)))
38	37	oveq1d 6033	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝑇 · (𝐵 − 𝐴)) + 𝐴) = (((𝑇 · 𝐵) − (𝑇 · 𝐴)) + 𝐴))
39		resubcl 8443	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
40	4, 8, 39	sylancr 414	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (1 − 𝑇) ∈ ℝ)
41	40, 18	remulcld 8210	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((1 − 𝑇) · 𝐴) ∈ ℝ)
42	41	recnd 8208	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((1 − 𝑇) · 𝐴) ∈ ℂ)
43	42, 33	addcomd 8330	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) = ((𝑇 · 𝐵) + ((1 − 𝑇) · 𝐴)))
44		1cnd 8195	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → 1 ∈ ℂ)
45	44, 31, 34	subdird 8594	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((1 − 𝑇) · 𝐴) = ((1 · 𝐴) − (𝑇 · 𝐴)))
46	34	mulid2d 8198	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (1 · 𝐴) = 𝐴)
47	46	oveq1d 6033	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((1 · 𝐴) − (𝑇 · 𝐴)) = (𝐴 − (𝑇 · 𝐴)))
48	45, 47	eqtrd 2264	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((1 − 𝑇) · 𝐴) = (𝐴 − (𝑇 · 𝐴)))
49	48	oveq2d 6034	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝑇 · 𝐵) + ((1 − 𝑇) · 𝐴)) = ((𝑇 · 𝐵) + (𝐴 − (𝑇 · 𝐴))))
50	43, 49	eqtrd 2264	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) = ((𝑇 · 𝐵) + (𝐴 − (𝑇 · 𝐴))))
51	36, 38, 50	3eqtr4d 2274	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝑇 · (𝐵 − 𝐴)) + 𝐴) = (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)))
52	34	addlidd 8329	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (0 + 𝐴) = 𝐴)
53	32, 34	npcand 8494	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((𝐵 − 𝐴) + 𝐴) = 𝐵)
54	52, 53	oveq12d 6036	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → ((0 + 𝐴)[,]((𝐵 − 𝐴) + 𝐴)) = (𝐴[,]𝐵))
55	30, 51, 54	3eltr3d 2314	1 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1004   ∈ wcel 2202   class class class wbr 4088  (class class class)co 6018  ℝcr 8031  0cc0 8032  1c1 8033   + caddc 8035   · cmul 8037   < clt 8214   ≤ cle 8215   − cmin 8350  ℝ⁺crp 9888  [,]cicc 10126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-mulrcl 8131  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-precex 8142  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148  ax-pre-mulgt0 8149

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-po 4393  df-iso 4394  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-rp 9889  df-icc 10130

This theorem is referenced by:  iccf1o  10239