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

Theorem scvxcvx 25490
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
StepHypRef Expression
1 scvxcvx.1 . . . . . . . . 9 (𝜑𝐷 ⊆ ℝ)
21adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3 simpr1 1186 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋𝐷)
42, 3sseldd 3965 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
54adantr 481 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6 simpr2 1187 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌𝐷)
72, 6sseldd 3965 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
87adantr 481 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
95, 8lttri4d 10769 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋))
10 oveq1 7152 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11 oveq2 7153 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
1211oveq1d 7160 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
1310, 12oveq12d 7163 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
1413fveq2d 6667 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15 oveq1 7152 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑡 · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
1611oveq1d 7160 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
1715, 16oveq12d 7163 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
1814, 17breq12d 5070 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
193adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋𝐷)
206adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌𝐷)
2119, 20jca 512 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋𝐷𝑌𝐷))
22 simprr 769 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23 simpll 763 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24 breq1 5060 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥 < 𝑦𝑋 < 𝑦))
25 oveq2 7153 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
2625fvoveq1d 7167 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
2827oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑋)))
2928oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))
3026, 29breq12d 5070 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3130ralbidv 3194 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3231imbi2d 342 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))))
3324, 32imbi12d 346 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))))
34 breq2 5061 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋 < 𝑦𝑋 < 𝑌))
35 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
3635oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
3736fveq2d 6667 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → (𝐹𝑦) = (𝐹𝑌))
3938oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑌)))
4039oveq2d 7161 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
4137, 40breq12d 5070 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4241ralbidv 3194 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4342imbi2d 342 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
4434, 43imbi12d 346 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))))
45 scvxcvx.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
46453expia 1113 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
4746ralrimiv 3178 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
4847expcom 414 . . . . . . . . . . . 12 ((𝑥𝐷𝑦𝐷𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
49483expia 1113 . . . . . . . . . . 11 ((𝑥𝐷𝑦𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))))
5033, 44, 49vtocl2ga 3572 . . . . . . . . . 10 ((𝑋𝐷𝑌𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
5121, 22, 23, 50syl3c 66 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
52 simprl 767 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
5318, 51, 52rspcdva 3622 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
5453orcd 869 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
5554expr 457 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
56 unitssre 12873 . . . . . . . . . . . . . . . 16 (0[,]1) ⊆ ℝ
57 simpr3 1188 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
5856, 57sseldi 3962 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5958recnd 10657 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60 ax-1cn 10583 . . . . . . . . . . . . . 14 1 ∈ ℂ
61 pncan3 10882 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
6259, 60, 61sylancl 586 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
6362oveq1d 7160 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64 subcl 10873 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
6560, 59, 64sylancr 587 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
667recnd 10657 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
6759, 65, 66adddird 10654 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
6866mulid2d 10647 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
6963, 67, 683eqtr3d 2861 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
7069fveq2d 6667 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹𝑌))
7162oveq1d 7160 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
72 scvxcvx.2 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐷⟶ℝ)
7372adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
7473, 6ffvelrnd 6844 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℝ)
7574recnd 10657 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℂ)
7659, 65, 75adddird 10654 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
7775mulid2d 10647 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑌)) = (𝐹𝑌))
7871, 76, 773eqtr3d 2861 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))) = (𝐹𝑌))
7970, 78eqtr4d 2856 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8079adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
81 oveq2 7153 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
8281fvoveq1d 7167 . . . . . . . . 9 (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83 fveq2 6663 . . . . . . . . . . 11 (𝑋 = 𝑌 → (𝐹𝑋) = (𝐹𝑌))
8483oveq2d 7161 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · (𝐹𝑋)) = (𝑇 · (𝐹𝑌)))
8584oveq1d 7160 . . . . . . . . 9 (𝑋 = 𝑌 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8682, 85eqeq12d 2834 . . . . . . . 8 (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌)))))
8780, 86syl5ibrcom 248 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
88 olc 862 . . . . . . 7 ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
8987, 88syl6 35 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
90 oveq1 7152 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91 oveq2 7153 . . . . . . . . . . . . . 14 (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
9291oveq1d 7160 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
9390, 92oveq12d 7163 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
9493fveq2d 6667 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95 oveq1 7152 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
9691oveq1d 7160 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹𝑋)) = ((1 − (1 − 𝑇)) · (𝐹𝑋)))
9795, 96oveq12d 7163 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
9894, 97breq12d 5070 . . . . . . . . . 10 (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋)))))
996adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌𝐷)
1003adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋𝐷)
10199, 100jca 512 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌𝐷𝑋𝐷))
102 simprr 769 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103 simpll 763 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104 breq1 5060 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝑥 < 𝑦𝑌 < 𝑦))
105 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106105fvoveq1d 7167 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐹𝑥) = (𝐹𝑌))
108107oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑌)))
109108oveq1d 7160 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))
110106, 109breq12d 5070 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
111110ralbidv 3194 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
112111imbi2d 342 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))))
113104, 112imbi12d 346 . . . . . . . . . . . 12 (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))))
114 breq2 5061 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑌 < 𝑦𝑌 < 𝑋))
115 oveq2 7153 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116115oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117116fveq2d 6667 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
119118oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑋)))
120119oveq2d 7161 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
121117, 120breq12d 5070 . . . . . . . . . . . . . . 15 (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
122121ralbidv 3194 . . . . . . . . . . . . . 14 (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
123122imbi2d 342 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
124114, 123imbi12d 346 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))))
125113, 124, 49vtocl2ga 3572 . . . . . . . . . . 11 ((𝑌𝐷𝑋𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
126101, 102, 103, 125syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
127 1re 10629 . . . . . . . . . . . . 13 1 ∈ ℝ
128 elioore 12756 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129 resubcl 10938 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130127, 128, 129sylancr 587 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131 eliooord 12784 . . . . . . . . . . . . . 14 (𝑇 ∈ (0(,)1) → (0 < 𝑇𝑇 < 1))
132131simprd 496 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133 posdif 11121 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134128, 127, 133sylancl 586 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135132, 134mpbid 233 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136131simpld 495 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137 ltsubpos 11120 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138128, 127, 137sylancl 586 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139136, 138mpbid 233 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140 0xr 10676 . . . . . . . . . . . . 13 0 ∈ ℝ*
141 1xr 10688 . . . . . . . . . . . . 13 1 ∈ ℝ*
142 elioo2 12767 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143140, 141, 142mp2an 688 . . . . . . . . . . . 12 ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144130, 135, 139, 143syl3anbrc 1335 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145144ad2antrl 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
14698, 126, 145rspcdva 3622 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
147127, 58, 129sylancr 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148147, 7remulcld 10659 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149148recnd 10657 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
15058, 4remulcld 10659 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151150recnd 10657 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152 nncan 10903 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
15360, 59, 152sylancr 587 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154153oveq1d 7160 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155154oveq2d 7161 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156149, 151, 155comraddd 10842 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157156adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158157fveq2d 6667 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159147, 74remulcld 10659 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℝ)
160159recnd 10657 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℂ)
16173, 3ffvelrnd 6844 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℝ)
16258, 161remulcld 10659 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℝ)
163162recnd 10657 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℂ)
164153oveq1d 7160 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
165164oveq2d 7161 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + (𝑇 · (𝐹𝑋))))
166160, 163, 165comraddd 10842 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
167166adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
168146, 158, 1673brtr3d 5088 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
169168orcd 869 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
170169expr 457 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
17155, 89, 1703jaod 1420 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
1729, 171mpd 15 . . . 4 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
173172ex 413 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
174 elpri 4579 . . . 4 (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
17575addid2d 10829 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + (𝐹𝑌)) = (𝐹𝑌))
176161recnd 10657 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℂ)
177176mul02d 10826 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑋)) = 0)
178177, 77oveq12d 7163 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))) = (0 + (𝐹𝑌)))
1794recnd 10657 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180179mul02d 10826 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181180, 68oveq12d 7163 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
18266addid2d 10829 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183181, 182eqtrd 2853 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184183fveq2d 6667 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹𝑌))
185175, 178, 1843eqtr4rd 2864 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
186 oveq1 7152 . . . . . . . . 9 (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187 oveq2 7153 . . . . . . . . . . 11 (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188 1m0e1 11746 . . . . . . . . . . 11 (1 − 0) = 1
189187, 188syl6eq 2869 . . . . . . . . . 10 (𝑇 = 0 → (1 − 𝑇) = 1)
190189oveq1d 7160 . . . . . . . . 9 (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191186, 190oveq12d 7163 . . . . . . . 8 (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192191fveq2d 6667 . . . . . . 7 (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193 oveq1 7152 . . . . . . . 8 (𝑇 = 0 → (𝑇 · (𝐹𝑋)) = (0 · (𝐹𝑋)))
194189oveq1d 7160 . . . . . . . 8 (𝑇 = 0 → ((1 − 𝑇) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
195193, 194oveq12d 7163 . . . . . . 7 (𝑇 = 0 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
196192, 195eqeq12d 2834 . . . . . 6 (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌)))))
197185, 196syl5ibrcom 248 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
198176addid1d 10828 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹𝑋) + 0) = (𝐹𝑋))
199176mulid2d 10647 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑋)) = (𝐹𝑋))
20075mul02d 10826 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑌)) = 0)
201199, 200oveq12d 7163 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))) = ((𝐹𝑋) + 0))
202179mulid2d 10647 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
20366mul02d 10826 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204202, 203oveq12d 7163 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205179addid1d 10828 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206204, 205eqtrd 2853 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207206fveq2d 6667 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹𝑋))
208198, 201, 2073eqtr4rd 2864 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
209 oveq1 7152 . . . . . . . . 9 (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210 oveq2 7153 . . . . . . . . . . 11 (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211 1m1e0 11697 . . . . . . . . . . 11 (1 − 1) = 0
212210, 211syl6eq 2869 . . . . . . . . . 10 (𝑇 = 1 → (1 − 𝑇) = 0)
213212oveq1d 7160 . . . . . . . . 9 (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214209, 213oveq12d 7163 . . . . . . . 8 (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215214fveq2d 6667 . . . . . . 7 (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216 oveq1 7152 . . . . . . . 8 (𝑇 = 1 → (𝑇 · (𝐹𝑋)) = (1 · (𝐹𝑋)))
217212oveq1d 7160 . . . . . . . 8 (𝑇 = 1 → ((1 − 𝑇) · (𝐹𝑌)) = (0 · (𝐹𝑌)))
218216, 217oveq12d 7163 . . . . . . 7 (𝑇 = 1 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
219215, 218eqeq12d 2834 . . . . . 6 (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌)))))
220208, 219syl5ibrcom 248 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
221197, 220jaod 853 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
222174, 221, 88syl56 36 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
223 0le1 11151 . . . . . 6 0 ≤ 1
224 prunioo 12855 . . . . . 6 ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225140, 141, 223, 224mp3an 1452 . . . . 5 ((0(,)1) ∪ {0, 1}) = (0[,]1)
22657, 225eleqtrrdi 2921 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227 elun 4122 . . . 4 (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
228226, 227sylib 219 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
229173, 222, 228mpjaod 854 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
230 scvxcvx.3 . . . . 5 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
2311, 230cvxcl 25489 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
23273, 231ffvelrnd 6844 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233162, 159readdcld 10658 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∈ ℝ)
234232, 233leloed 10771 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
235229, 234mpbird 258 1 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841  w3o 1078  w3a 1079   = wceq 1528  wcel 2105  wral 3135  cun 3931  wss 3933  {cpr 4559   class class class wbr 5057  wf 6344  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  *cxr 10662   < clt 10663  cle 10664  cmin 10858  (,)cioo 12726  [,]cicc 12729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  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  25494  amgmwlem  44831
  Copyright terms: Public domain W3C validator