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 25571

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 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3		simpr1 1191	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ 𝐷)
4	2, 3	sseldd 3916	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
5	4	adantr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6		simpr2 1192	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ 𝐷)
7	2, 6	sseldd 3916	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
8	7	adantr 484	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
9	5, 8	lttri4d 10770	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋))
10		oveq1 7142	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11		oveq2 7143	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
12	11	oveq1d 7150	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
13	10, 12	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
14	13	fveq2d 6649	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15		oveq1 7142	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑡 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
16	11	oveq1d 7150	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
17	15, 16	oveq12d 7153	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
18	14, 17	breq12d 5043	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
19	3	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 ∈ 𝐷)
20	6	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌 ∈ 𝐷)
21	19, 20	jca 515	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷))
22		simprr 772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24		breq1 5033	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 < 𝑦 ↔ 𝑋 < 𝑦))
25		oveq2 7143	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
26	25	fvoveq1d 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
28	27	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑋)))
29	28	oveq1d 7150	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))
30	26, 29	breq12d 5043	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
31	30	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
32	31	imbi2d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
33	24, 32	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
34		breq2 5034	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 < 𝑦 ↔ 𝑋 < 𝑌))
35		oveq2 7143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
36	35	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
37	36	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
39	38	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑌)))
40	39	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
41	37, 40	breq12d 5043	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
42	41	ralbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
43	42	imbi2d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))
44	34, 43	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))))
45		scvxcvx.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
46	45	3expia 1118	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
47	46	ralrimiv 3148	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
48	47	expcom 417	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
49	48	3expia 1118	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
50	33, 44, 49	vtocl2ga 3523	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))
51	21, 22, 23, 50	syl3c 66	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
52		simprl 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
53	18, 51, 52	rspcdva 3573	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
54	53	orcd 870	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
55	54	expr 460	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
56		unitssre 12877	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
57		simpr3 1193	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
58	56, 57	sseldi 3913	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
59	58	recnd 10658	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60		ax-1cn 10584	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
61		pncan3 10883	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
62	59, 60, 61	sylancl 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
63	62	oveq1d 7150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64		subcl 10874	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
65	60, 59, 64	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
66	7	recnd 10658	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
67	59, 65, 66	adddird 10655	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
68	66	mulid2d 10648	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
69	63, 67, 68	3eqtr3d 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
70	69	fveq2d 6649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹‘𝑌))
71	62	oveq1d 7150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
72		scvxcvx.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
73	72	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
74	73, 6	ffvelrnd 6829	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℝ)
75	74	recnd 10658	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℂ)
76	59, 65, 75	adddird 10655	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
77	75	mulid2d 10648	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑌)) = (𝐹‘𝑌))
78	71, 76, 77	3eqtr3d 2841	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))) = (𝐹‘𝑌))
79	70, 78	eqtr4d 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
80	79	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
81		oveq2 7143	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
82	81	fvoveq1d 7157	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83		fveq2 6645	. . . . . . . . . . 11 ⊢ (𝑋 = 𝑌 → (𝐹‘𝑋) = (𝐹‘𝑌))
84	83	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑌)))
85	84	oveq1d 7150	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
86	82, 85	eqeq12d 2814	. . . . . . . 8 ⊢ (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
87	80, 86	syl5ibrcom 250	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
88		olc 865	. . . . . . 7 ⊢ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
89	87, 88	syl6 35	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
90		oveq1 7142	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91		oveq2 7143	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
92	91	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
93	90, 92	oveq12d 7153	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
94	93	fveq2d 6649	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95		oveq1 7142	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
96	91	oveq1d 7150	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹‘𝑋)) = ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))
97	95, 96	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
98	94, 97	breq12d 5043	. . . . . . . . . 10 ⊢ (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))))
99	6	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 ∈ 𝐷)
100	3	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋 ∈ 𝐷)
101	99, 100	jca 515	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷))
102		simprr 772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104		breq1 5033	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝑥 < 𝑦 ↔ 𝑌 < 𝑦))
105		oveq2 7143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106	105	fvoveq1d 7157	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107		fveq2 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
108	107	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑌)))
109	108	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))
110	106, 109	breq12d 5043	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
111	110	ralbidv 3162	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
112	111	imbi2d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
113	104, 112	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
114		breq2 5034	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑋))
115		oveq2 7143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116	115	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117	116	fveq2d 6649	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118		fveq2 6645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
119	118	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑋)))
120	119	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
121	117, 120	breq12d 5043	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
122	121	ralbidv 3162	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
123	122	imbi2d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
124	114, 123	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))))
125	113, 124, 49	vtocl2ga 3523	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
126	101, 102, 103, 125	syl3c 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
127		1re 10630	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
128		elioore 12756	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129		resubcl 10939	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130	127, 128, 129	sylancr 590	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131		eliooord 12784	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ∧ 𝑇 < 1))
132	131	simprd 499	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133		posdif 11122	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134	128, 127, 133	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135	132, 134	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136	131	simpld 498	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137		ltsubpos 11121	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138	128, 127, 137	sylancl 589	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139	136, 138	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140		0xr 10677	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ^*
141		1xr 10689	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
142		elioo2 12767	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143	140, 141, 142	mp2an 691	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144	130, 135, 139, 143	syl3anbrc 1340	. . . . . . . . . . 11 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145	144	ad2antrl 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
146	98, 126, 145	rspcdva 3573	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
147	127, 58, 129	sylancr 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148	147, 7	remulcld 10660	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149	148	recnd 10658	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
150	58, 4	remulcld 10660	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151	150	recnd 10658	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152		nncan 10904	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
153	60, 59, 152	sylancr 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154	153	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155	154	oveq2d 7151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156	149, 151, 155	comraddd 10843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157	156	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158	157	fveq2d 6649	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159	147, 74	remulcld 10660	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℝ)
160	159	recnd 10658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℂ)
161	73, 3	ffvelrnd 6829	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℝ)
162	58, 161	remulcld 10660	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℝ)
163	162	recnd 10658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℂ)
164	153	oveq1d 7150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
165	164	oveq2d 7151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋))))
166	160, 163, 165	comraddd 10843	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
167	166	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
168	146, 158, 167	3brtr3d 5061	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
169	168	orcd 870	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
170	169	expr 460	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
171	55, 89, 170	3jaod 1425	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
172	9, 171	mpd 15	. . . 4 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
173	172	ex 416	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
174		elpri 4547	. . . 4 ⊢ (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
175	75	addid2d 10830	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + (𝐹‘𝑌)) = (𝐹‘𝑌))
176	161	recnd 10658	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℂ)
177	176	mul02d 10827	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑋)) = 0)
178	177, 77	oveq12d 7153	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))) = (0 + (𝐹‘𝑌)))
179	4	recnd 10658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180	179	mul02d 10827	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181	180, 68	oveq12d 7153	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
182	66	addid2d 10830	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183	181, 182	eqtrd 2833	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184	183	fveq2d 6649	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹‘𝑌))
185	175, 178, 184	3eqtr4rd 2844	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
186		oveq1 7142	. . . . . . . . 9 ⊢ (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187		oveq2 7143	. . . . . . . . . . 11 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188		1m0e1 11746	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
189	187, 188	eqtrdi 2849	. . . . . . . . . 10 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
190	189	oveq1d 7150	. . . . . . . . 9 ⊢ (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191	186, 190	oveq12d 7153	. . . . . . . 8 ⊢ (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192	191	fveq2d 6649	. . . . . . 7 ⊢ (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193		oveq1 7142	. . . . . . . 8 ⊢ (𝑇 = 0 → (𝑇 · (𝐹‘𝑋)) = (0 · (𝐹‘𝑋)))
194	189	oveq1d 7150	. . . . . . . 8 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
195	193, 194	oveq12d 7153	. . . . . . 7 ⊢ (𝑇 = 0 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
196	192, 195	eqeq12d 2814	. . . . . 6 ⊢ (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))))
197	185, 196	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
198	176	addid1d 10829	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘𝑋) + 0) = (𝐹‘𝑋))
199	176	mulid2d 10648	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑋)) = (𝐹‘𝑋))
200	75	mul02d 10827	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑌)) = 0)
201	199, 200	oveq12d 7153	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))) = ((𝐹‘𝑋) + 0))
202	179	mulid2d 10648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
203	66	mul02d 10827	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204	202, 203	oveq12d 7153	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205	179	addid1d 10829	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206	204, 205	eqtrd 2833	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207	206	fveq2d 6649	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹‘𝑋))
208	198, 201, 207	3eqtr4rd 2844	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
209		oveq1 7142	. . . . . . . . 9 ⊢ (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210		oveq2 7143	. . . . . . . . . . 11 ⊢ (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211		1m1e0 11697	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
212	210, 211	eqtrdi 2849	. . . . . . . . . 10 ⊢ (𝑇 = 1 → (1 − 𝑇) = 0)
213	212	oveq1d 7150	. . . . . . . . 9 ⊢ (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214	209, 213	oveq12d 7153	. . . . . . . 8 ⊢ (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215	214	fveq2d 6649	. . . . . . 7 ⊢ (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216		oveq1 7142	. . . . . . . 8 ⊢ (𝑇 = 1 → (𝑇 · (𝐹‘𝑋)) = (1 · (𝐹‘𝑋)))
217	212	oveq1d 7150	. . . . . . . 8 ⊢ (𝑇 = 1 → ((1 − 𝑇) · (𝐹‘𝑌)) = (0 · (𝐹‘𝑌)))
218	216, 217	oveq12d 7153	. . . . . . 7 ⊢ (𝑇 = 1 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
219	215, 218	eqeq12d 2814	. . . . . 6 ⊢ (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌)))))
220	208, 219	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
221	197, 220	jaod 856	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
222	174, 221, 88	syl56 36	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
223		0le1 11152	. . . . . 6 ⊢ 0 ≤ 1
224		prunioo 12859	. . . . . 6 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225	140, 141, 223, 224	mp3an 1458	. . . . 5 ⊢ ((0(,)1) ∪ {0, 1}) = (0[,]1)
226	57, 225	eleqtrrdi 2901	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227		elun 4076	. . . 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 857	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
230		scvxcvx.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
231	1, 230	cvxcl 25570	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
232	73, 231	ffvelrnd 6829	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233	162, 159	readdcld 10659	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∈ ℝ)
234	232, 233	leloed 10772	. 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

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∪ cun 3879 ⊆ wss 3881 {cpr 4527 class class class wbr 5030 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 ℝ^*cxr 10663 < clt 10664 ≤ cle 10665 − cmin 10859 (,)cioo 12726 [,]cicc 12729

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-sup 8890 df-inf 8891 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-n0 11886 df-z 11970 df-uz 12232 df-q 12337 df-rp 12378 df-ioo 12730 df-ico 12732 df-icc 12733

This theorem is referenced by: amgmlem 25575 amgmwlem 45330

W3C validator