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 27295

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 3932	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
5	4	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6		simpr2 1214	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ 𝐷)
7	2, 6	sseldd 3932	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
8	7	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
9	5, 8	lttri4d 11432	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋))
10		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11		oveq2 7420	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
12	11	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
13	10, 12	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
14	13	fveq2d 6881	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑡 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
16	11	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
17	15, 16	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
18	14, 17	breq12d 5116	. . . . . . . . 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 5106	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 < 𝑦 ↔ 𝑋 < 𝑦))
25		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
26	25	fvoveq1d 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27		fveq2 6877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
28	27	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑋)))
29	28	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))
30	26, 29	breq12d 5116	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
31	30	ralbidv 3186	. . . . . . . . . . . . 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 5107	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 < 𝑦 ↔ 𝑋 < 𝑌))
35		oveq2 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
36	35	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
37	36	fveq2d 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38		fveq2 6877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
39	38	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑌)))
40	39	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
41	37, 40	breq12d 5116	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
42	41	ralbidv 3186	. . . . . . . . . . . . 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 3154	. . . . . . . . . . . . 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 3538	. . . . . . . . . 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 3578	. . . . . . . 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 13611	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
57		simpr3 1215	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
58	56, 57	sselid 3929	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
59	58	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60		ax-1cn 11239	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
61		pncan3 11546	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
62	59, 60, 61	sylancl 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
63	62	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64		subcl 11537	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
65	60, 59, 64	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
66	7	recnd 11318	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
67	59, 65, 66	adddird 11315	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
68	66	mullidd 11308	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
69	63, 67, 68	3eqtr3d 2804	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
70	69	fveq2d 6881	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹‘𝑌))
71	62	oveq1d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
72		scvxcvx.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
73	72	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
74	73, 6	ffvelcdmd 7077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℝ)
75	74	recnd 11318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℂ)
76	59, 65, 75	adddird 11315	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
77	75	mullidd 11308	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑌)) = (𝐹‘𝑌))
78	71, 76, 77	3eqtr3d 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))) = (𝐹‘𝑌))
79	70, 78	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
80	79	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
81		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
82	81	fvoveq1d 7434	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83		fveq2 6877	. . . . . . . . . . 11 ⊢ (𝑋 = 𝑌 → (𝐹‘𝑋) = (𝐹‘𝑌))
84	83	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑌)))
85	84	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
86	82, 85	eqeq12d 2777	. . . . . . . 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 7419	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
92	91	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
93	90, 92	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
94	93	fveq2d 6881	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
96	91	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹‘𝑋)) = ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))
97	95, 96	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
98	94, 97	breq12d 5116	. . . . . . . . . 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 5106	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝑥 < 𝑦 ↔ 𝑌 < 𝑦))
105		oveq2 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106	105	fvoveq1d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107		fveq2 6877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
108	107	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑌)))
109	108	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))
110	106, 109	breq12d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
111	110	ralbidv 3186	. . . . . . . . . . . . . 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 5107	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑋))
115		oveq2 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116	115	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117	116	fveq2d 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118		fveq2 6877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
119	118	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑋)))
120	119	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
121	117, 120	breq12d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
122	121	ralbidv 3186	. . . . . . . . . . . . . 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 3538	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
126	101, 102, 103, 125	syl3c 67	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
127		1re 11289	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
128		elioore 13487	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129		resubcl 11603	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130	127, 128, 129	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131		eliooord 13517	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ∧ 𝑇 < 1))
132	131	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133		posdif 11790	. . . . . . . . . . . . . 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 11789	. . . . . . . . . . . . . 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 11337	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ^*
141		1xr 11349	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
142		elioo2 13498	. . . . . . . . . . . . 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 3578	. . . . . . . . 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 11320	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149	148	recnd 11318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
150	58, 4	remulcld 11320	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151	150	recnd 11318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152		nncan 11568	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
153	60, 59, 152	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154	153	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155	154	oveq2d 7428	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156	149, 151, 155	comraddd 11505	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157	156	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158	157	fveq2d 6881	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159	147, 74	remulcld 11320	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℝ)
160	159	recnd 11318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℂ)
161	73, 3	ffvelcdmd 7077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℝ)
162	58, 161	remulcld 11320	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℝ)
163	162	recnd 11318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℂ)
164	153	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
165	164	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋))))
166	160, 163, 165	comraddd 11505	. . . . . . . . . 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 5136	. . . . . . . 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 4608	. . . 4 ⊢ (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
175	75	addlidd 11492	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + (𝐹‘𝑌)) = (𝐹‘𝑌))
176	161	recnd 11318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℂ)
177	176	mul02d 11489	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑋)) = 0)
178	177, 77	oveq12d 7430	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))) = (0 + (𝐹‘𝑌)))
179	4	recnd 11318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180	179	mul02d 11489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181	180, 68	oveq12d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
182	66	addlidd 11492	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183	181, 182	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184	183	fveq2d 6881	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹‘𝑌))
185	175, 178, 184	3eqtr4rd 2807	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
186		oveq1 7419	. . . . . . . . 9 ⊢ (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188		1m0e1 12443	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
189	187, 188	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
190	189	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191	186, 190	oveq12d 7430	. . . . . . . 8 ⊢ (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192	191	fveq2d 6881	. . . . . . 7 ⊢ (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193		oveq1 7419	. . . . . . . 8 ⊢ (𝑇 = 0 → (𝑇 · (𝐹‘𝑋)) = (0 · (𝐹‘𝑋)))
194	189	oveq1d 7427	. . . . . . . 8 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
195	193, 194	oveq12d 7430	. . . . . . 7 ⊢ (𝑇 = 0 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
196	192, 195	eqeq12d 2777	. . . . . 6 ⊢ (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))))
197	185, 196	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
198	176	addridd 11491	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘𝑋) + 0) = (𝐹‘𝑋))
199	176	mullidd 11308	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑋)) = (𝐹‘𝑋))
200	75	mul02d 11489	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑌)) = 0)
201	199, 200	oveq12d 7430	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))) = ((𝐹‘𝑋) + 0))
202	179	mullidd 11308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
203	66	mul02d 11489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204	202, 203	oveq12d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205	179	addridd 11491	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206	204, 205	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207	206	fveq2d 6881	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹‘𝑋))
208	198, 201, 207	3eqtr4rd 2807	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
209		oveq1 7419	. . . . . . . . 9 ⊢ (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211		1m1e0 12396	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
212	210, 211	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑇 = 1 → (1 − 𝑇) = 0)
213	212	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214	209, 213	oveq12d 7430	. . . . . . . 8 ⊢ (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215	214	fveq2d 6881	. . . . . . 7 ⊢ (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216		oveq1 7419	. . . . . . . 8 ⊢ (𝑇 = 1 → (𝑇 · (𝐹‘𝑋)) = (1 · (𝐹‘𝑋)))
217	212	oveq1d 7427	. . . . . . . 8 ⊢ (𝑇 = 1 → ((1 − 𝑇) · (𝐹‘𝑌)) = (0 · (𝐹‘𝑌)))
218	216, 217	oveq12d 7430	. . . . . . 7 ⊢ (𝑇 = 1 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
219	215, 218	eqeq12d 2777	. . . . . 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 11820	. . . . . 6 ⊢ 0 ≤ 1
224		prunioo 13593	. . . . . 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 2872	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227		elun 4100	. . . 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 27294	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
232	73, 231	ffvelcdmd 7077	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233	162, 159	readdcld 11319	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∈ ℝ)
234	232, 233	leloed 11434	. 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 1570 ∈ wcel 2145 ∀wral 3077 ∪ cun 3897 ⊆ wss 3899 {cpr 4586 class class class wbr 5103 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11522 (,)cioo 13457 [,]cicc 13460

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-ioo 13461 df-ico 13463 df-icc 13464

This theorem is used by: amgmlem 27299 amgmwlem 50931

W3C validator