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

Theorem scvxcvx 25562
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 483 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3 simpr1 1190 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋𝐷)
42, 3sseldd 3967 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
54adantr 483 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6 simpr2 1191 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌𝐷)
72, 6sseldd 3967 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
87adantr 483 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
95, 8lttri4d 10780 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋))
10 oveq1 7162 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11 oveq2 7163 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
1211oveq1d 7170 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
1310, 12oveq12d 7173 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
1413fveq2d 6673 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15 oveq1 7162 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑡 · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
1611oveq1d 7170 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
1715, 16oveq12d 7173 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
1814, 17breq12d 5078 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
193adantr 483 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋𝐷)
206adantr 483 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌𝐷)
2119, 20jca 514 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋𝐷𝑌𝐷))
22 simprr 771 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23 simpll 765 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24 breq1 5068 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥 < 𝑦𝑋 < 𝑦))
25 oveq2 7163 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
2625fvoveq1d 7177 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27 fveq2 6669 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
2827oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑋)))
2928oveq1d 7170 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))
3026, 29breq12d 5078 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3130ralbidv 3197 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3231imbi2d 343 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))))
3324, 32imbi12d 347 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))))
34 breq2 5069 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋 < 𝑦𝑋 < 𝑌))
35 oveq2 7163 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
3635oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
3736fveq2d 6673 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38 fveq2 6669 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → (𝐹𝑦) = (𝐹𝑌))
3938oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑌)))
4039oveq2d 7171 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
4137, 40breq12d 5078 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4241ralbidv 3197 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4342imbi2d 343 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
4434, 43imbi12d 347 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))))
45 scvxcvx.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
46453expia 1117 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
4746ralrimiv 3181 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
4847expcom 416 . . . . . . . . . . . 12 ((𝑥𝐷𝑦𝐷𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
49483expia 1117 . . . . . . . . . . 11 ((𝑥𝐷𝑦𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))))
5033, 44, 49vtocl2ga 3574 . . . . . . . . . 10 ((𝑋𝐷𝑌𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
5121, 22, 23, 50syl3c 66 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
52 simprl 769 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
5318, 51, 52rspcdva 3624 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
5453orcd 869 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
5554expr 459 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
56 unitssre 12884 . . . . . . . . . . . . . . . 16 (0[,]1) ⊆ ℝ
57 simpr3 1192 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
5856, 57sseldi 3964 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5958recnd 10668 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60 ax-1cn 10594 . . . . . . . . . . . . . 14 1 ∈ ℂ
61 pncan3 10893 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
6259, 60, 61sylancl 588 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
6362oveq1d 7170 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64 subcl 10884 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
6560, 59, 64sylancr 589 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
667recnd 10668 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
6759, 65, 66adddird 10665 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
6866mulid2d 10658 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
6963, 67, 683eqtr3d 2864 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
7069fveq2d 6673 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹𝑌))
7162oveq1d 7170 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
72 scvxcvx.2 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐷⟶ℝ)
7372adantr 483 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
7473, 6ffvelrnd 6851 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℝ)
7574recnd 10668 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℂ)
7659, 65, 75adddird 10665 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
7775mulid2d 10658 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑌)) = (𝐹𝑌))
7871, 76, 773eqtr3d 2864 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))) = (𝐹𝑌))
7970, 78eqtr4d 2859 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8079adantr 483 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
81 oveq2 7163 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
8281fvoveq1d 7177 . . . . . . . . 9 (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83 fveq2 6669 . . . . . . . . . . 11 (𝑋 = 𝑌 → (𝐹𝑋) = (𝐹𝑌))
8483oveq2d 7171 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · (𝐹𝑋)) = (𝑇 · (𝐹𝑌)))
8584oveq1d 7170 . . . . . . . . 9 (𝑋 = 𝑌 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8682, 85eqeq12d 2837 . . . . . . . 8 (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌)))))
8780, 86syl5ibrcom 249 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
88 olc 864 . . . . . . 7 ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
8987, 88syl6 35 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
90 oveq1 7162 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91 oveq2 7163 . . . . . . . . . . . . . 14 (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
9291oveq1d 7170 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
9390, 92oveq12d 7173 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
9493fveq2d 6673 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95 oveq1 7162 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
9691oveq1d 7170 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹𝑋)) = ((1 − (1 − 𝑇)) · (𝐹𝑋)))
9795, 96oveq12d 7173 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
9894, 97breq12d 5078 . . . . . . . . . 10 (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋)))))
996adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌𝐷)
1003adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋𝐷)
10199, 100jca 514 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌𝐷𝑋𝐷))
102 simprr 771 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103 simpll 765 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104 breq1 5068 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝑥 < 𝑦𝑌 < 𝑦))
105 oveq2 7163 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106105fvoveq1d 7177 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107 fveq2 6669 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐹𝑥) = (𝐹𝑌))
108107oveq2d 7171 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑌)))
109108oveq1d 7170 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))
110106, 109breq12d 5078 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
111110ralbidv 3197 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
112111imbi2d 343 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))))
113104, 112imbi12d 347 . . . . . . . . . . . 12 (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))))
114 breq2 5069 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑌 < 𝑦𝑌 < 𝑋))
115 oveq2 7163 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116115oveq2d 7171 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117116fveq2d 6673 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118 fveq2 6669 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
119118oveq2d 7171 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑋)))
120119oveq2d 7171 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
121117, 120breq12d 5078 . . . . . . . . . . . . . . 15 (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
122121ralbidv 3197 . . . . . . . . . . . . . 14 (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
123122imbi2d 343 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
124114, 123imbi12d 347 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))))
125113, 124, 49vtocl2ga 3574 . . . . . . . . . . 11 ((𝑌𝐷𝑋𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
126101, 102, 103, 125syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
127 1re 10640 . . . . . . . . . . . . 13 1 ∈ ℝ
128 elioore 12767 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129 resubcl 10949 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130127, 128, 129sylancr 589 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131 eliooord 12795 . . . . . . . . . . . . . 14 (𝑇 ∈ (0(,)1) → (0 < 𝑇𝑇 < 1))
132131simprd 498 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133 posdif 11132 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134128, 127, 133sylancl 588 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135132, 134mpbid 234 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136131simpld 497 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137 ltsubpos 11131 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138128, 127, 137sylancl 588 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139136, 138mpbid 234 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140 0xr 10687 . . . . . . . . . . . . 13 0 ∈ ℝ*
141 1xr 10699 . . . . . . . . . . . . 13 1 ∈ ℝ*
142 elioo2 12778 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143140, 141, 142mp2an 690 . . . . . . . . . . . 12 ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144130, 135, 139, 143syl3anbrc 1339 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145144ad2antrl 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
14698, 126, 145rspcdva 3624 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
147127, 58, 129sylancr 589 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
148147, 7remulcld 10670 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
149148recnd 10668 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
15058, 4remulcld 10670 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
151150recnd 10668 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
152 nncan 10914 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
15360, 59, 152sylancr 589 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
154153oveq1d 7170 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
155154oveq2d 7171 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
156149, 151, 155comraddd 10853 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157156adantr 483 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158157fveq2d 6673 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
159147, 74remulcld 10670 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℝ)
160159recnd 10668 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℂ)
16173, 3ffvelrnd 6851 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℝ)
16258, 161remulcld 10670 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℝ)
163162recnd 10668 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℂ)
164153oveq1d 7170 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
165164oveq2d 7171 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + (𝑇 · (𝐹𝑋))))
166160, 163, 165comraddd 10853 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
167166adantr 483 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
168146, 158, 1673brtr3d 5096 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
169168orcd 869 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
170169expr 459 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
17155, 89, 1703jaod 1424 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
1729, 171mpd 15 . . . 4 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
173172ex 415 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
174 elpri 4588 . . . 4 (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
17575addid2d 10840 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + (𝐹𝑌)) = (𝐹𝑌))
176161recnd 10668 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℂ)
177176mul02d 10837 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑋)) = 0)
178177, 77oveq12d 7173 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))) = (0 + (𝐹𝑌)))
1794recnd 10668 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
180179mul02d 10837 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
181180, 68oveq12d 7173 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
18266addid2d 10840 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
183181, 182eqtrd 2856 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
184183fveq2d 6673 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹𝑌))
185175, 178, 1843eqtr4rd 2867 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
186 oveq1 7162 . . . . . . . . 9 (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
187 oveq2 7163 . . . . . . . . . . 11 (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
188 1m0e1 11757 . . . . . . . . . . 11 (1 − 0) = 1
189187, 188syl6eq 2872 . . . . . . . . . 10 (𝑇 = 0 → (1 − 𝑇) = 1)
190189oveq1d 7170 . . . . . . . . 9 (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
191186, 190oveq12d 7173 . . . . . . . 8 (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
192191fveq2d 6673 . . . . . . 7 (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
193 oveq1 7162 . . . . . . . 8 (𝑇 = 0 → (𝑇 · (𝐹𝑋)) = (0 · (𝐹𝑋)))
194189oveq1d 7170 . . . . . . . 8 (𝑇 = 0 → ((1 − 𝑇) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
195193, 194oveq12d 7173 . . . . . . 7 (𝑇 = 0 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
196192, 195eqeq12d 2837 . . . . . 6 (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌)))))
197185, 196syl5ibrcom 249 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
198176addid1d 10839 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹𝑋) + 0) = (𝐹𝑋))
199176mulid2d 10658 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑋)) = (𝐹𝑋))
20075mul02d 10837 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑌)) = 0)
201199, 200oveq12d 7173 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))) = ((𝐹𝑋) + 0))
202179mulid2d 10658 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
20366mul02d 10837 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
204202, 203oveq12d 7173 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
205179addid1d 10839 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
206204, 205eqtrd 2856 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
207206fveq2d 6673 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹𝑋))
208198, 201, 2073eqtr4rd 2867 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
209 oveq1 7162 . . . . . . . . 9 (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
210 oveq2 7163 . . . . . . . . . . 11 (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
211 1m1e0 11708 . . . . . . . . . . 11 (1 − 1) = 0
212210, 211syl6eq 2872 . . . . . . . . . 10 (𝑇 = 1 → (1 − 𝑇) = 0)
213212oveq1d 7170 . . . . . . . . 9 (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
214209, 213oveq12d 7173 . . . . . . . 8 (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
215214fveq2d 6673 . . . . . . 7 (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
216 oveq1 7162 . . . . . . . 8 (𝑇 = 1 → (𝑇 · (𝐹𝑋)) = (1 · (𝐹𝑋)))
217212oveq1d 7170 . . . . . . . 8 (𝑇 = 1 → ((1 − 𝑇) · (𝐹𝑌)) = (0 · (𝐹𝑌)))
218216, 217oveq12d 7173 . . . . . . 7 (𝑇 = 1 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
219215, 218eqeq12d 2837 . . . . . 6 (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌)))))
220208, 219syl5ibrcom 249 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
221197, 220jaod 855 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
222174, 221, 88syl56 36 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
223 0le1 11162 . . . . . 6 0 ≤ 1
224 prunioo 12866 . . . . . 6 ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
225140, 141, 223, 224mp3an 1457 . . . . 5 ((0(,)1) ∪ {0, 1}) = (0[,]1)
22657, 225eleqtrrdi 2924 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
227 elun 4124 . . . 4 (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
228226, 227sylib 220 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
229173, 222, 228mpjaod 856 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
230 scvxcvx.3 . . . . 5 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
2311, 230cvxcl 25561 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
23273, 231ffvelrnd 6851 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
233162, 159readdcld 10669 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∈ ℝ)
234232, 233leloed 10782 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
235229, 234mpbird 259 1 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wo 843  w3o 1082  w3a 1083   = wceq 1533  wcel 2110  wral 3138  cun 3933  wss 3935  {cpr 4568   class class class wbr 5065  wf 6350  cfv 6354  (class class class)co 7155  cc 10534  cr 10535  0cc0 10536  1c1 10537   + caddc 10539   · cmul 10541  *cxr 10673   < clt 10674  cle 10675  cmin 10869  (,)cioo 12737  [,]cicc 12740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-sup 8905  df-inf 8906  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-n0 11897  df-z 11981  df-uz 12243  df-q 12348  df-rp 12389  df-ioo 12741  df-ico 12743  df-icc 12744
This theorem is referenced by:  amgmlem  25566  amgmwlem  44902
  Copyright terms: Public domain W3C validator