scvxcvx - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > scvxcvx		Structured version Visualization version GIF version

Theorem scvxcvx 27318

Description: A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)

**Hypotheses**
Ref	Expression
scvxcvx.1	⊢ (𝜑 → 𝐷 ⊆ ℝ)
scvxcvx.2	⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
scvxcvx.3	⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
scvxcvx.4	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))

**Assertion**
Ref	Expression
scvxcvx	⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))

Distinct variable groups: 𝑎,𝑏,𝑡,𝑥,𝑦,𝐷 𝜑,𝑎,𝑏,𝑡,𝑥,𝑦 𝑋,𝑎,𝑏,𝑡,𝑥,𝑦 𝑌,𝑎,𝑏,𝑡,𝑥,𝑦 𝑡,𝐹,𝑥,𝑦 𝑡,𝑇 Allowed substitution hints: 𝑇(𝑥, 𝑦, 𝑎, 𝑏) 𝐹(𝑎, 𝑏)

**Proof of Theorem scvxcvx**
Step	Hyp	Ref	Expression
1		scvxcvx.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
2	1	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3		simpr1 1213	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ 𝐷)
4	2, 3	sseldd 3909	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
5	4	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6		simpr2 1214	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ 𝐷)
7	2, 6	sseldd 3909	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
8	7	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
9	5, 8	lttri4d 11454	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋))
10		oveq1 7427	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11		oveq2 7428	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
12	11	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
13	10, 12	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
14	13	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15		oveq1 7427	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑡 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
16	11	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
17	15, 16	oveq12d 7438	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
18	14, 17	breq12d 5115	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
19	3	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 ∈ 𝐷)
20	6	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌 ∈ 𝐷)
21	19, 20	jca 521	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷))
22		simprr 785	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24		breq1 5105	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 < 𝑦 ↔ 𝑋 < 𝑦))
25		oveq2 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
26	25	fvoveq1d 7442	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
28	27	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑋)))
29	28	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))
30	26, 29	breq12d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
31	30	ralbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
32	31	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
33	24, 32	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
34		breq2 5106	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 < 𝑦 ↔ 𝑋 < 𝑌))
35		oveq2 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
36	35	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
37	36	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
39	38	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑌)))
40	39	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
41	37, 40	breq12d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
42	41	ralbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
43	42	imbi2d 343	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))
44	34, 43	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))))
45		scvxcvx.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
46	45	3expia 1139	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
47	46	ralrimiv 3153	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
48	47	expcom 419	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
49	48	3expia 1139	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
50	33, 44, 49	vtocl2ga 3537	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))
51	21, 22, 23, 50	syl3c 67	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
52		simprl 783	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
53	18, 51, 52	rspcdva 3577	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
54	53	orcd 887	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
55	54	expr 462	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
56		unitssre 13633	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
57		simpr3 1215	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
58	56, 57	sselid 3906	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
59	58	recnd 11340	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60		ax-1cn 11261	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
61		pncan3 11568	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
62	59, 60, 61	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
63	62	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64		subcl 11559	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
65	60, 59, 64	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
66	7	recnd 11340	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
67	59, 65, 66	adddird 11337	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
68	66	mullidd 11330	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
69	63, 67, 68	3eqtr3d 2803	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
70	69	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹‘𝑌))
71	62	oveq1d 7435	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
72		scvxcvx.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
73	72	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
74	73, 6	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℝ)
75	74	recnd 11340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℂ)
76	59, 65, 75	adddird 11337	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
77	75	mullidd 11330	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑌)) = (𝐹‘𝑌))
78	71, 76, 77	3eqtr3d 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))) = (𝐹‘𝑌))
79	70, 78	eqtr4d 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
80	79	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
81		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
82	81	fvoveq1d 7442	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑋 = 𝑌 → (𝐹‘𝑋) = (𝐹‘𝑌))
84	83	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑌)))
85	84	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
86	82, 85	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
87	80, 86	syl5ibrcom 250	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
88		olc 882	. . . . . . 7 ⊢ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
89	87, 88	syl6 36	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
90		oveq1 7427	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
92	91	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
93	90, 92	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
94	93	fveq2d 6889	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95		oveq1 7427	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
96	91	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹‘𝑋)) = ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))
97	95, 96	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
98	94, 97	breq12d 5115	. . . . . . . . . 10 ⊢ (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))))
99	6	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 ∈ 𝐷)
100	3	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋 ∈ 𝐷)
101	99, 100	jca 521	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷))
102		simprr 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103		simpll 779	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104		breq1 5105	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝑥 < 𝑦 ↔ 𝑌 < 𝑦))
105		oveq2 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106	105	fvoveq1d 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
108	107	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑌)))
109	108	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))
110	106, 109	breq12d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
111	110	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
112	111	imbi2d 343	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
113	104, 112	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
114		breq2 5106	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑋))
115		oveq2 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116	115	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117	116	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
119	118	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑋)))
120	119	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
121	117, 120	breq12d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
122	121	ralbidv 3185	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
123	122	imbi2d 343	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
124	114, 123	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))))
125	113, 124, 49	vtocl2ga 3537	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
126	101, 102, 103, 125	syl3c 67	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
127		1re 11311	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
128		elioore 13509	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129		resubcl 11625	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130	127, 128, 129	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131		eliooord 13539	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ∧ 𝑇 < 1))
132	131	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133		posdif 11812	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134	128, 127, 133	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135	132, 134	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136	131	simpld 500	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137		ltsubpos 11811	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138	128, 127, 137	sylancl 598	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139	136, 138	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140		0xr 11359	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ^*
141		1xr 11371	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
142		elioo2 13520	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143	140, 141, 142	mp2an 705	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144	130, 135, 139, 143	syl3anbrc 1362	. . . . . . . . . . 11 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145	144	ad2antrl 741	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
146	98, 126, 145	rspcdva 3577	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
147	127, 58, 129	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148	147, 7	remulcld 11342	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149	148	recnd 11340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
150	58, 4	remulcld 11342	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151	150	recnd 11340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152		nncan 11590	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
153	60, 59, 152	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154	153	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155	154	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156	149, 151, 155	comraddd 11527	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157	156	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158	157	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159	147, 74	remulcld 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℝ)
160	159	recnd 11340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℂ)
161	73, 3	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℝ)
162	58, 161	remulcld 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℝ)
163	162	recnd 11340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℂ)
164	153	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
165	164	oveq2d 7436	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋))))
166	160, 163, 165	comraddd 11527	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
167	166	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
168	146, 158, 167	3brtr3d 5135	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
169	168	orcd 887	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
170	169	expr 462	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
171	55, 89, 170	3jaod 1456	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
172	9, 171	mpd 16	. . . 4 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
173	172	ex 418	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
174		elpri 4604	. . . 4 ⊢ (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
175	75	addlidd 11514	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + (𝐹‘𝑌)) = (𝐹‘𝑌))
176	161	recnd 11340	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℂ)
177	176	mul02d 11511	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑋)) = 0)
178	177, 77	oveq12d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))) = (0 + (𝐹‘𝑌)))
179	4	recnd 11340	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180	179	mul02d 11511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181	180, 68	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
182	66	addlidd 11514	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183	181, 182	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184	183	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹‘𝑌))
185	175, 178, 184	3eqtr4rd 2806	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
186		oveq1 7427	. . . . . . . . 9 ⊢ (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188		1m0e1 12465	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
189	187, 188	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
190	189	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191	186, 190	oveq12d 7438	. . . . . . . 8 ⊢ (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192	191	fveq2d 6889	. . . . . . 7 ⊢ (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193		oveq1 7427	. . . . . . . 8 ⊢ (𝑇 = 0 → (𝑇 · (𝐹‘𝑋)) = (0 · (𝐹‘𝑋)))
194	189	oveq1d 7435	. . . . . . . 8 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
195	193, 194	oveq12d 7438	. . . . . . 7 ⊢ (𝑇 = 0 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
196	192, 195	eqeq12d 2776	. . . . . 6 ⊢ (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))))
197	185, 196	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
198	176	addridd 11513	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘𝑋) + 0) = (𝐹‘𝑋))
199	176	mullidd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑋)) = (𝐹‘𝑋))
200	75	mul02d 11511	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑌)) = 0)
201	199, 200	oveq12d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))) = ((𝐹‘𝑋) + 0))
202	179	mullidd 11330	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
203	66	mul02d 11511	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204	202, 203	oveq12d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205	179	addridd 11513	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206	204, 205	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207	206	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹‘𝑋))
208	198, 201, 207	3eqtr4rd 2806	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
209		oveq1 7427	. . . . . . . . 9 ⊢ (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211		1m1e0 12418	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
212	210, 211	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑇 = 1 → (1 − 𝑇) = 0)
213	212	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214	209, 213	oveq12d 7438	. . . . . . . 8 ⊢ (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215	214	fveq2d 6889	. . . . . . 7 ⊢ (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216		oveq1 7427	. . . . . . . 8 ⊢ (𝑇 = 1 → (𝑇 · (𝐹‘𝑋)) = (1 · (𝐹‘𝑋)))
217	212	oveq1d 7435	. . . . . . . 8 ⊢ (𝑇 = 1 → ((1 − 𝑇) · (𝐹‘𝑌)) = (0 · (𝐹‘𝑌)))
218	216, 217	oveq12d 7438	. . . . . . 7 ⊢ (𝑇 = 1 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
219	215, 218	eqeq12d 2776	. . . . . 6 ⊢ (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌)))))
220	208, 219	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
221	197, 220	jaod 873	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
222	174, 221, 88	syl56 37	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
223		0le1 11842	. . . . . 6 ⊢ 0 ≤ 1
224		prunioo 13615	. . . . . 6 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225	140, 141, 223, 224	mp3an 1490	. . . . 5 ⊢ ((0(,)1) ∪ {0, 1}) = (0[,]1)
226	57, 225	eleqtrrdi 2871	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227		elun 4152	. . . 4 ⊢ (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
228	226, 227	sylib 221	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
229	173, 222, 228	mpjaod 874	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
230		scvxcvx.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
231	1, 230	cvxcl 27317	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
232	73, 231	ffvelcdmd 7085	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233	162, 159	readdcld 11341	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∈ ℝ)
234	232, 233	leloed 11456	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
235	229, 234	mpbird 260	1 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ⊆ wss 3895 ∪ cun 4149 {cpr 4586 class class class wbr 5102 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 + caddc 11206 · cmul 11208 ℝ^*cxr 11345 < clt 11346 ≤ cle 11347 − cmin 11544 (,)cioo 13479 [,]cicc 13482

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-er 8720 df-en 8977 df-dom 8978 df-sdom 8979 df-sup 9437 df-inf 9438 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-n0 12610 df-z 12697 df-uz 12969 df-q 13079 df-rp 13124 df-ioo 13483 df-ico 13485 df-icc 13486

This theorem is used by: amgmlem 27322 amgmwlem 51155

W3C validator