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 26953

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 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3		simpr1 1195	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ 𝐷)
4	2, 3	sseldd 3964	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
5	4	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6		simpr2 1196	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ 𝐷)
7	2, 6	sseldd 3964	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
8	7	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
9	5, 8	lttri4d 11381	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋))
10		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
12	11	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
13	10, 12	oveq12d 7428	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
14	13	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → (𝑡 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
16	11	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
17	15, 16	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
18	14, 17	breq12d 5137	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
19	3	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 ∈ 𝐷)
20	6	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌 ∈ 𝐷)
21	19, 20	jca 511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷))
22		simprr 772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24		breq1 5127	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 < 𝑦 ↔ 𝑋 < 𝑦))
25		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
26	25	fvoveq1d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
28	27	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑋 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑋)))
29	28	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))
30	26, 29	breq12d 5137	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
31	30	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
32	31	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
33	24, 32	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
34		breq2 5128	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝑋 < 𝑦 ↔ 𝑋 < 𝑌))
35		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
36	35	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
37	36	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
39	38	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑌)))
40	39	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))
41	37, 40	breq12d 5137	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
42	41	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))
43	42	imbi2d 340	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))
44	34, 43	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))))
45		scvxcvx.4	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
46	45	3expia 1121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
47	46	ralrimiv 3132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
48	47	expcom 413	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
49	48	3expia 1121	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
50	33, 44, 49	vtocl2ga 3562	. . . . . . . . . 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 3607	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
54	53	orcd 873	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
55	54	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
56		unitssre 13521	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
57		simpr3 1197	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
58	56, 57	sselid 3961	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
59	58	recnd 11268	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60		ax-1cn 11192	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
61		pncan3 11495	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
62	59, 60, 61	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
63	62	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64		subcl 11486	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
65	60, 59, 64	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
66	7	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
67	59, 65, 66	adddird 11265	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
68	66	mullidd 11258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
69	63, 67, 68	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
70	69	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹‘𝑌))
71	62	oveq1d 7425	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
72		scvxcvx.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
74	73, 6	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℝ)
75	74	recnd 11268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℂ)
76	59, 65, 75	adddird 11265	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
77	75	mullidd 11258	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑌)) = (𝐹‘𝑌))
78	71, 76, 77	3eqtr3d 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))) = (𝐹‘𝑌))
79	70, 78	eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
80	79	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
81		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
82	81	fvoveq1d 7432	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑋 = 𝑌 → (𝐹‘𝑋) = (𝐹‘𝑌))
84	83	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑋 = 𝑌 → (𝑇 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑌)))
85	84	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑋 = 𝑌 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))
86	82, 85	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
87	80, 86	syl5ibrcom 247	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
88		olc 868	. . . . . . 7 ⊢ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
89	87, 88	syl6 35	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
90		oveq1 7417	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
92	91	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
93	90, 92	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
94	93	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌)))
96	91	oveq1d 7425	. . . . . . . . . . . 12 ⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹‘𝑋)) = ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))
97	95, 96	oveq12d 7428	. . . . . . . . . . 11 ⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
98	94, 97	breq12d 5137	. . . . . . . . . 10 ⊢ (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))))
99	6	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 ∈ 𝐷)
100	3	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋 ∈ 𝐷)
101	99, 100	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷))
102		simprr 772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103		simpll 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104		breq1 5127	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝑥 < 𝑦 ↔ 𝑌 < 𝑦))
105		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106	105	fvoveq1d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107		fveq2 6881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
108	107	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑌 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑌)))
109	108	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑌 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))
110	106, 109	breq12d 5137	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
111	110	ralbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))
112	111	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))))
113	104, 112	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))))
114		breq2 5128	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑋))
115		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116	115	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117	116	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118		fveq2 6881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
119	118	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑋)))
120	119	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑋 → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
121	117, 120	breq12d 5137	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
122	121	ralbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))
123	122	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
124	114, 123	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))))
125	113, 124, 49	vtocl2ga 3562	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))
126	101, 102, 103, 125	syl3c 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))
127		1re 11240	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
128		elioore 13397	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129		resubcl 11552	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130	127, 128, 129	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131		eliooord 13427	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ∧ 𝑇 < 1))
132	131	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133		posdif 11735	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134	128, 127, 133	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135	132, 134	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136	131	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137		ltsubpos 11734	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138	128, 127, 137	sylancl 586	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139	136, 138	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140		0xr 11287	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ^*
141		1xr 11299	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ^*
142		elioo2 13408	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143	140, 141, 142	mp2an 692	. . . . . . . . . . . 12 ⊢ ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144	130, 135, 139, 143	syl3anbrc 1344	. . . . . . . . . . 11 ⊢ (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145	144	ad2antrl 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
146	98, 126, 145	rspcdva 3607	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))
147	127, 58, 129	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148	147, 7	remulcld 11270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149	148	recnd 11268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
150	58, 4	remulcld 11270	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151	150	recnd 11268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152		nncan 11517	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
153	60, 59, 152	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154	153	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155	154	oveq2d 7426	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156	149, 151, 155	comraddd 11454	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157	156	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158	157	fveq2d 6885	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159	147, 74	remulcld 11270	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℝ)
160	159	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℂ)
161	73, 3	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℝ)
162	58, 161	remulcld 11270	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℝ)
163	162	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℂ)
164	153	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋)))
165	164	oveq2d 7426	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋))))
166	160, 163, 165	comraddd 11454	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
167	166	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
168	146, 158, 167	3brtr3d 5155	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
169	168	orcd 873	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
170	169	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
171	55, 89, 170	3jaod 1431	. . . . 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 412	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
174		elpri 4630	. . . 4 ⊢ (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
175	75	addlidd 11441	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + (𝐹‘𝑌)) = (𝐹‘𝑌))
176	161	recnd 11268	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℂ)
177	176	mul02d 11438	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑋)) = 0)
178	177, 77	oveq12d 7428	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))) = (0 + (𝐹‘𝑌)))
179	4	recnd 11268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180	179	mul02d 11438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181	180, 68	oveq12d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
182	66	addlidd 11441	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183	181, 182	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184	183	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹‘𝑌))
185	175, 178, 184	3eqtr4rd 2782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
186		oveq1 7417	. . . . . . . . 9 ⊢ (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188		1m0e1 12366	. . . . . . . . . . 11 ⊢ (1 − 0) = 1
189	187, 188	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑇 = 0 → (1 − 𝑇) = 1)
190	189	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191	186, 190	oveq12d 7428	. . . . . . . 8 ⊢ (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192	191	fveq2d 6885	. . . . . . 7 ⊢ (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193		oveq1 7417	. . . . . . . 8 ⊢ (𝑇 = 0 → (𝑇 · (𝐹‘𝑋)) = (0 · (𝐹‘𝑋)))
194	189	oveq1d 7425	. . . . . . . 8 ⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌)))
195	193, 194	oveq12d 7428	. . . . . . 7 ⊢ (𝑇 = 0 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))
196	192, 195	eqeq12d 2752	. . . . . 6 ⊢ (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))))
197	185, 196	syl5ibrcom 247	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
198	176	addridd 11440	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘𝑋) + 0) = (𝐹‘𝑋))
199	176	mullidd 11258	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑋)) = (𝐹‘𝑋))
200	75	mul02d 11438	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑌)) = 0)
201	199, 200	oveq12d 7428	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))) = ((𝐹‘𝑋) + 0))
202	179	mullidd 11258	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
203	66	mul02d 11438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204	202, 203	oveq12d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205	179	addridd 11440	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206	204, 205	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207	206	fveq2d 6885	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹‘𝑋))
208	198, 201, 207	3eqtr4rd 2782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
209		oveq1 7417	. . . . . . . . 9 ⊢ (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211		1m1e0 12317	. . . . . . . . . . 11 ⊢ (1 − 1) = 0
212	210, 211	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑇 = 1 → (1 − 𝑇) = 0)
213	212	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214	209, 213	oveq12d 7428	. . . . . . . 8 ⊢ (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215	214	fveq2d 6885	. . . . . . 7 ⊢ (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216		oveq1 7417	. . . . . . . 8 ⊢ (𝑇 = 1 → (𝑇 · (𝐹‘𝑋)) = (1 · (𝐹‘𝑋)))
217	212	oveq1d 7425	. . . . . . . 8 ⊢ (𝑇 = 1 → ((1 − 𝑇) · (𝐹‘𝑌)) = (0 · (𝐹‘𝑌)))
218	216, 217	oveq12d 7428	. . . . . . 7 ⊢ (𝑇 = 1 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))
219	215, 218	eqeq12d 2752	. . . . . 6 ⊢ (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌)))))
220	208, 219	syl5ibrcom 247	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
221	197, 220	jaod 859	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
222	174, 221, 88	syl56 36	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
223		0le1 11765	. . . . . 6 ⊢ 0 ≤ 1
224		prunioo 13503	. . . . . 6 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225	140, 141, 223, 224	mp3an 1463	. . . . 5 ⊢ ((0(,)1) ∪ {0, 1}) = (0[,]1)
226	57, 225	eleqtrrdi 2846	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227		elun 4133	. . . 4 ⊢ (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
228	226, 227	sylib 218	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
229	173, 222, 228	mpjaod 860	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))
230		scvxcvx.3	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
231	1, 230	cvxcl 26952	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
232	73, 231	ffvelcdmd 7080	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233	162, 159	readdcld 11269	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∈ ℝ)
234	232, 233	leloed 11383	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))))
235	229, 234	mpbird 257	1 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3052 ∪ cun 3929 ⊆ wss 3931 {cpr 4608 class class class wbr 5124 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 (,)cioo 13367 [,]cicc 13370

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-sup 9459 df-inf 9460 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-n0 12507 df-z 12594 df-uz 12858 df-q 12970 df-rp 13014 df-ioo 13371 df-ico 13373 df-icc 13374

This theorem is referenced by: amgmlem 26957 amgmwlem 49633

W3C validator