Theorem cvxcl

Description: Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Hypotheses	cvxcl.1	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	cvxcl.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
Assertion	cvxcl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		cvxcl.1	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
2		cvxcl.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
3	2	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
4	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
5		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ 𝐷 )
6		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ 𝐷 )
7		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 [,] 𝑦 ) = ( 𝑋 [,] 𝑦 ) )
8	7	sseq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑋 [,] 𝑦 ) ⊆ 𝐷 ) )
9		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 [,] 𝑦 ) = ( 𝑋 [,] 𝑌 ) )
10	9	sseq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
11	8 10	rspc2v	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
12	5 6 11	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
13	12	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 ) )
14	4 13	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 𝑋 [,] 𝑌 ) ⊆ 𝐷 )
15		ax-1cn	⊢ 1 ∈ ℂ
16		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
17		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
18	16 17	sselid	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℝ )
19	18	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑇 ∈ ℂ )
20		nncan	⊢ ( ( 1 ∈ ℂ ∧ 𝑇 ∈ ℂ ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
21	15 19 20	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − ( 1 − 𝑇 ) ) = 𝑇 )
22	21	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) = ( 𝑇 · 𝑋 ) )
23	22	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
24	23	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
25	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝐷 ⊆ ℝ )
26	25 5	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℝ )
27	26	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
28	25 6	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℝ )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
30		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
31		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → 𝑇 ∈ ( 0 [,] 1 ) )
32		iirev	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
33	31 32	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) )
34		lincmb01cmp	⊢ ( ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 < 𝑌 ) ∧ ( 1 − 𝑇 ) ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
35	27 29 30 33 34	syl31anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( ( 1 − ( 1 − 𝑇 ) ) · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
36	24 35	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑋 [,] 𝑌 ) )
37	14 36	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 < 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
38		oveq2	⊢ ( 𝑋 = 𝑌 → ( 𝑇 · 𝑋 ) = ( 𝑇 · 𝑌 ) )
39	38	oveq1d	⊢ ( 𝑋 = 𝑌 → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
40		pncan3	⊢ ( ( 𝑇 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
41	19 15 40	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 + ( 1 − 𝑇 ) ) = 1 )
42	41	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( 1 · 𝑌 ) )
43		1re	⊢ 1 ∈ ℝ
44		resubcl	⊢ ( ( 1 ∈ ℝ ∧ 𝑇 ∈ ℝ ) → ( 1 − 𝑇 ) ∈ ℝ )
45	43 18 44	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℝ )
46	45	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 − 𝑇 ) ∈ ℂ )
47	28	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑌 ∈ ℂ )
48	19 46 47	adddird	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 + ( 1 − 𝑇 ) ) · 𝑌 ) = ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) )
49	47	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 1 · 𝑌 ) = 𝑌 )
50	42 48 49	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑌 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = 𝑌 )
51	39 50	sylan9eqr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = 𝑌 )
52	6	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → 𝑌 ∈ 𝐷 )
53	51 52	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑋 = 𝑌 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
54	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 )
55		oveq1	⊢ ( 𝑥 = 𝑌 → ( 𝑥 [,] 𝑦 ) = ( 𝑌 [,] 𝑦 ) )
56	55	sseq1d	⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑌 [,] 𝑦 ) ⊆ 𝐷 ) )
57		oveq2	⊢ ( 𝑦 = 𝑋 → ( 𝑌 [,] 𝑦 ) = ( 𝑌 [,] 𝑋 ) )
58	57	sseq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑌 [,] 𝑦 ) ⊆ 𝐷 ↔ ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
59	56 58	rspc2v	⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
60	6 5 59	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
61	60	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 [,] 𝑦 ) ⊆ 𝐷 → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 ) )
62	54 61	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( 𝑌 [,] 𝑋 ) ⊆ 𝐷 )
63	26	recnd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → 𝑋 ∈ ℂ )
64	19 63	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑇 · 𝑋 ) ∈ ℂ )
65	46 47	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 1 − 𝑇 ) · 𝑌 ) ∈ ℂ )
66	64 65	addcomd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) )
67	66	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) = ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) )
68	28	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑌 ∈ ℝ )
69	26	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑋 ∈ ℝ )
70		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑌 < 𝑋 )
71		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → 𝑇 ∈ ( 0 [,] 1 ) )
72		lincmb01cmp	⊢ ( ( ( 𝑌 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑌 < 𝑋 ) ∧ 𝑇 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
73	68 69 70 71 72	syl31anc	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( ( 1 − 𝑇 ) · 𝑌 ) + ( 𝑇 · 𝑋 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
74	67 73	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ ( 𝑌 [,] 𝑋 ) )
75	62 74	sseldd	⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑌 < 𝑋 ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )
76	26 28	lttri4d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋 ) )
77	37 53 75 76	mpjao3dan	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑇 · 𝑋 ) + ( ( 1 − 𝑇 ) · 𝑌 ) ) ∈ 𝐷 )