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

Theorem scvxcvx 25723
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 484 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3 simpr1 1195 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋𝐷)
42, 3sseldd 3878 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
54adantr 484 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6 simpr2 1196 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌𝐷)
72, 6sseldd 3878 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
87adantr 484 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
95, 8lttri4d 10859 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋))
10 oveq1 7177 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11 oveq2 7178 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
1211oveq1d 7185 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
1310, 12oveq12d 7188 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
1413fveq2d 6678 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15 oveq1 7177 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑡 · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
1611oveq1d 7185 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
1715, 16oveq12d 7188 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
1814, 17breq12d 5043 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
193adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋𝐷)
206adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌𝐷)
2119, 20jca 515 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋𝐷𝑌𝐷))
22 simprr 773 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23 simpll 767 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24 breq1 5033 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥 < 𝑦𝑋 < 𝑦))
25 oveq2 7178 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
2625fvoveq1d 7192 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27 fveq2 6674 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
2827oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑋)))
2928oveq1d 7185 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))
3026, 29breq12d 5043 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3130ralbidv 3109 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3231imbi2d 344 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))))
3324, 32imbi12d 348 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))))
34 breq2 5034 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋 < 𝑦𝑋 < 𝑌))
35 oveq2 7178 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
3635oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
3736fveq2d 6678 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38 fveq2 6674 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → (𝐹𝑦) = (𝐹𝑌))
3938oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑌)))
4039oveq2d 7186 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
4137, 40breq12d 5043 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4241ralbidv 3109 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4342imbi2d 344 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
4434, 43imbi12d 348 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))))
45 scvxcvx.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
46453expia 1122 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
4746ralrimiv 3095 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
4847expcom 417 . . . . . . . . . . . 12 ((𝑥𝐷𝑦𝐷𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
49483expia 1122 . . . . . . . . . . 11 ((𝑥𝐷𝑦𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))))
5033, 44, 49vtocl2ga 3479 . . . . . . . . . 10 ((𝑋𝐷𝑌𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
5121, 22, 23, 50syl3c 66 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
52 simprl 771 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
5318, 51, 52rspcdva 3528 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
5453orcd 872 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
5554expr 460 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
56 unitssre 12973 . . . . . . . . . . . . . . . 16 (0[,]1) ⊆ ℝ
57 simpr3 1197 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
5856, 57sseldi 3875 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5958recnd 10747 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60 ax-1cn 10673 . . . . . . . . . . . . . 14 1 ∈ ℂ
61 pncan3 10972 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
6259, 60, 61sylancl 589 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
6362oveq1d 7185 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64 subcl 10963 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
6560, 59, 64sylancr 590 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
667recnd 10747 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
6759, 65, 66adddird 10744 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
6866mulid2d 10737 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
6963, 67, 683eqtr3d 2781 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
7069fveq2d 6678 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹𝑌))
7162oveq1d 7185 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
72 scvxcvx.2 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐷⟶ℝ)
7372adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
7473, 6ffvelrnd 6862 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℝ)
7574recnd 10747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℂ)
7659, 65, 75adddird 10744 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
7775mulid2d 10737 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑌)) = (𝐹𝑌))
7871, 76, 773eqtr3d 2781 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))) = (𝐹𝑌))
7970, 78eqtr4d 2776 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8079adantr 484 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
81 oveq2 7178 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
8281fvoveq1d 7192 . . . . . . . . 9 (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83 fveq2 6674 . . . . . . . . . . 11 (𝑋 = 𝑌 → (𝐹𝑋) = (𝐹𝑌))
8483oveq2d 7186 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · (𝐹𝑋)) = (𝑇 · (𝐹𝑌)))
8584oveq1d 7185 . . . . . . . . 9 (𝑋 = 𝑌 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8682, 85eqeq12d 2754 . . . . . . . 8 (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌)))))
8780, 86syl5ibrcom 250 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
88 olc 867 . . . . . . 7 ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
8987, 88syl6 35 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
90 oveq1 7177 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91 oveq2 7178 . . . . . . . . . . . . . 14 (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
9291oveq1d 7185 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
9390, 92oveq12d 7188 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
9493fveq2d 6678 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95 oveq1 7177 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
9691oveq1d 7185 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹𝑋)) = ((1 − (1 − 𝑇)) · (𝐹𝑋)))
9795, 96oveq12d 7188 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
9894, 97breq12d 5043 . . . . . . . . . 10 (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋)))))
996adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌𝐷)
1003adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋𝐷)
10199, 100jca 515 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌𝐷𝑋𝐷))
102 simprr 773 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103 simpll 767 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104 breq1 5033 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝑥 < 𝑦𝑌 < 𝑦))
105 oveq2 7178 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106105fvoveq1d 7192 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107 fveq2 6674 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐹𝑥) = (𝐹𝑌))
108107oveq2d 7186 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑌)))
109108oveq1d 7185 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))
110106, 109breq12d 5043 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
111110ralbidv 3109 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
112111imbi2d 344 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))))
113104, 112imbi12d 348 . . . . . . . . . . . 12 (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))))
114 breq2 5034 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑌 < 𝑦𝑌 < 𝑋))
115 oveq2 7178 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116115oveq2d 7186 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117116fveq2d 6678 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118 fveq2 6674 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
119118oveq2d 7186 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑋)))
120119oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
121117, 120breq12d 5043 . . . . . . . . . . . . . . 15 (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
122121ralbidv 3109 . . . . . . . . . . . . . 14 (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
123122imbi2d 344 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
124114, 123imbi12d 348 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))))
125113, 124, 49vtocl2ga 3479 . . . . . . . . . . 11 ((𝑌𝐷𝑋𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
126101, 102, 103, 125syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
127 1re 10719 . . . . . . . . . . . . 13 1 ∈ ℝ
128 elioore 12851 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129 resubcl 11028 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130127, 128, 129sylancr 590 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131 eliooord 12880 . . . . . . . . . . . . . 14 (𝑇 ∈ (0(,)1) → (0 < 𝑇𝑇 < 1))
132131simprd 499 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133 posdif 11211 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134128, 127, 133sylancl 589 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135132, 134mpbid 235 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136131simpld 498 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137 ltsubpos 11210 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138128, 127, 137sylancl 589 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139136, 138mpbid 235 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140 0xr 10766 . . . . . . . . . . . . 13 0 ∈ ℝ*
141 1xr 10778 . . . . . . . . . . . . 13 1 ∈ ℝ*
142 elioo2 12862 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143140, 141, 142mp2an 692 . . . . . . . . . . . 12 ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144130, 135, 139, 143syl3anbrc 1344 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145144ad2antrl 728 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
14698, 126, 145rspcdva 3528 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
147127, 58, 129sylancr 590 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148147, 7remulcld 10749 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149148recnd 10747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
15058, 4remulcld 10749 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151150recnd 10747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152 nncan 10993 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
15360, 59, 152sylancr 590 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154153oveq1d 7185 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155154oveq2d 7186 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156149, 151, 155comraddd 10932 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157156adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158157fveq2d 6678 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159147, 74remulcld 10749 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℝ)
160159recnd 10747 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℂ)
16173, 3ffvelrnd 6862 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℝ)
16258, 161remulcld 10749 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℝ)
163162recnd 10747 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℂ)
164153oveq1d 7185 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
165164oveq2d 7186 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + (𝑇 · (𝐹𝑋))))
166160, 163, 165comraddd 10932 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
167166adantr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
168146, 158, 1673brtr3d 5061 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
169168orcd 872 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
170169expr 460 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
17155, 89, 1703jaod 1429 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
1729, 171mpd 15 . . . 4 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
173172ex 416 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
174 elpri 4538 . . . 4 (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
17575addid2d 10919 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + (𝐹𝑌)) = (𝐹𝑌))
176161recnd 10747 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℂ)
177176mul02d 10916 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑋)) = 0)
178177, 77oveq12d 7188 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))) = (0 + (𝐹𝑌)))
1794recnd 10747 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180179mul02d 10916 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181180, 68oveq12d 7188 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
18266addid2d 10919 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183181, 182eqtrd 2773 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184183fveq2d 6678 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹𝑌))
185175, 178, 1843eqtr4rd 2784 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
186 oveq1 7177 . . . . . . . . 9 (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187 oveq2 7178 . . . . . . . . . . 11 (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188 1m0e1 11837 . . . . . . . . . . 11 (1 − 0) = 1
189187, 188eqtrdi 2789 . . . . . . . . . 10 (𝑇 = 0 → (1 − 𝑇) = 1)
190189oveq1d 7185 . . . . . . . . 9 (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191186, 190oveq12d 7188 . . . . . . . 8 (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192191fveq2d 6678 . . . . . . 7 (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193 oveq1 7177 . . . . . . . 8 (𝑇 = 0 → (𝑇 · (𝐹𝑋)) = (0 · (𝐹𝑋)))
194189oveq1d 7185 . . . . . . . 8 (𝑇 = 0 → ((1 − 𝑇) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
195193, 194oveq12d 7188 . . . . . . 7 (𝑇 = 0 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
196192, 195eqeq12d 2754 . . . . . 6 (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌)))))
197185, 196syl5ibrcom 250 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
198176addid1d 10918 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹𝑋) + 0) = (𝐹𝑋))
199176mulid2d 10737 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑋)) = (𝐹𝑋))
20075mul02d 10916 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑌)) = 0)
201199, 200oveq12d 7188 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))) = ((𝐹𝑋) + 0))
202179mulid2d 10737 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
20366mul02d 10916 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204202, 203oveq12d 7188 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205179addid1d 10918 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206204, 205eqtrd 2773 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207206fveq2d 6678 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹𝑋))
208198, 201, 2073eqtr4rd 2784 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
209 oveq1 7177 . . . . . . . . 9 (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210 oveq2 7178 . . . . . . . . . . 11 (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211 1m1e0 11788 . . . . . . . . . . 11 (1 − 1) = 0
212210, 211eqtrdi 2789 . . . . . . . . . 10 (𝑇 = 1 → (1 − 𝑇) = 0)
213212oveq1d 7185 . . . . . . . . 9 (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214209, 213oveq12d 7188 . . . . . . . 8 (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215214fveq2d 6678 . . . . . . 7 (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216 oveq1 7177 . . . . . . . 8 (𝑇 = 1 → (𝑇 · (𝐹𝑋)) = (1 · (𝐹𝑋)))
217212oveq1d 7185 . . . . . . . 8 (𝑇 = 1 → ((1 − 𝑇) · (𝐹𝑌)) = (0 · (𝐹𝑌)))
218216, 217oveq12d 7188 . . . . . . 7 (𝑇 = 1 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
219215, 218eqeq12d 2754 . . . . . 6 (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌)))))
220208, 219syl5ibrcom 250 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
221197, 220jaod 858 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
222174, 221, 88syl56 36 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
223 0le1 11241 . . . . . 6 0 ≤ 1
224 prunioo 12955 . . . . . 6 ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225140, 141, 223, 224mp3an 1462 . . . . 5 ((0(,)1) ∪ {0, 1}) = (0[,]1)
22657, 225eleqtrrdi 2844 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227 elun 4039 . . . 4 (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
228226, 227sylib 221 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
229173, 222, 228mpjaod 859 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
230 scvxcvx.3 . . . . 5 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
2311, 230cvxcl 25722 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
23273, 231ffvelrnd 6862 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233162, 159readdcld 10748 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∈ ℝ)
234232, 233leloed 10861 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
235229, 234mpbird 260 1 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2114  wral 3053  cun 3841  wss 3843  {cpr 4518   class class class wbr 5030  wf 6335  cfv 6339  (class class class)co 7170  cc 10613  cr 10614  0cc0 10615  1c1 10616   + caddc 10618   · cmul 10620  *cxr 10752   < clt 10753  cle 10754  cmin 10948  (,)cioo 12821  [,]cicc 12824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-sup 8979  df-inf 8980  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-n0 11977  df-z 12063  df-uz 12325  df-q 12431  df-rp 12473  df-ioo 12825  df-ico 12827  df-icc 12828
This theorem is referenced by:  amgmlem  25727  amgmwlem  45959
  Copyright terms: Public domain W3C validator