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

Theorem scvxcvx 25003
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 472 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ)
3 simpr1 1248 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋𝐷)
42, 3sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ)
54adantr 472 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ)
6 simpr2 1250 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌𝐷)
72, 6sseldd 3762 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ)
87adantr 472 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ)
95, 8lttri4d 10432 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋))
10 oveq1 6849 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋))
11 oveq2 6850 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇))
1211oveq1d 6857 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌))
1310, 12oveq12d 6860 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
1413fveq2d 6379 . . . . . . . . . 10 (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
15 oveq1 6849 . . . . . . . . . . 11 (𝑡 = 𝑇 → (𝑡 · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
1611oveq1d 6857 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
1715, 16oveq12d 6860 . . . . . . . . . 10 (𝑡 = 𝑇 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
1814, 17breq12d 4822 . . . . . . . . 9 (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
193adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋𝐷)
206adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌𝐷)
2119, 20jca 507 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋𝐷𝑌𝐷))
22 simprr 789 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌)
23 simpll 783 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑)
24 breq1 4812 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥 < 𝑦𝑋 < 𝑦))
25 oveq2 6850 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋))
2625fvoveq1d 6864 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))))
27 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑋 → (𝐹𝑥) = (𝐹𝑋))
2827oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑋 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑋)))
2928oveq1d 6857 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))
3026, 29breq12d 4822 . . . . . . . . . . . . . 14 (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3130ralbidv 3133 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))
3231imbi2d 331 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))))
3324, 32imbi12d 335 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))))))
34 breq2 4813 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋 < 𝑦𝑋 < 𝑌))
35 oveq2 6850 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌))
3635oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))
3736fveq2d 6379 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))))
38 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑌 → (𝐹𝑦) = (𝐹𝑌))
3938oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑌)))
4039oveq2d 6858 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌 → ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
4137, 40breq12d 4822 . . . . . . . . . . . . . 14 (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4241ralbidv 3133 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))
4342imbi2d 331 . . . . . . . . . . . 12 (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
4434, 43imbi12d 335 . . . . . . . . . . 11 (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌)))))))
45 scvxcvx.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
46453expia 1150 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
4746ralrimiv 3112 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
4847expcom 402 . . . . . . . . . . . 12 ((𝑥𝐷𝑦𝐷𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))))
49483expia 1150 . . . . . . . . . . 11 ((𝑥𝐷𝑦𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))))
5033, 44, 49vtocl2ga 3426 . . . . . . . . . 10 ((𝑋𝐷𝑌𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))))
5121, 22, 23, 50syl3c 66 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹𝑋)) + ((1 − 𝑡) · (𝐹𝑌))))
52 simprl 787 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1))
5318, 51, 52rspcdva 3467 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
5453orcd 899 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
5554expr 448 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
56 unitssre 12526 . . . . . . . . . . . . . . . 16 (0[,]1) ⊆ ℝ
57 simpr3 1252 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1))
5856, 57sseldi 3759 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ)
5958recnd 10322 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ)
60 ax-1cn 10247 . . . . . . . . . . . . . 14 1 ∈ ℂ
61 pncan3 10543 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑇 + (1 − 𝑇)) = 1)
6259, 60, 61sylancl 580 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1)
6362oveq1d 6857 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌))
64 subcl 10534 . . . . . . . . . . . . . 14 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈ ℂ)
6560, 59, 64sylancr 581 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℂ)
667recnd 10322 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ)
6759, 65, 66adddird 10319 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))
6866mulid2d 10312 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌)
6963, 67, 683eqtr3d 2807 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌)
7069fveq2d 6379 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹𝑌))
7162oveq1d 6857 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
72 scvxcvx.2 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐷⟶ℝ)
7372adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ)
7473, 6ffvelrnd 6550 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℝ)
7574recnd 10322 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑌) ∈ ℂ)
7659, 65, 75adddird 10319 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹𝑌)) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
7775mulid2d 10312 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑌)) = (𝐹𝑌))
7871, 76, 773eqtr3d 2807 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))) = (𝐹𝑌))
7970, 78eqtr4d 2802 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8079adantr 472 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
81 oveq2 6850 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌))
8281fvoveq1d 6864 . . . . . . . . 9 (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))))
83 fveq2 6375 . . . . . . . . . . 11 (𝑋 = 𝑌 → (𝐹𝑋) = (𝐹𝑌))
8483oveq2d 6858 . . . . . . . . . 10 (𝑋 = 𝑌 → (𝑇 · (𝐹𝑋)) = (𝑇 · (𝐹𝑌)))
8584oveq1d 6857 . . . . . . . . 9 (𝑋 = 𝑌 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌))))
8682, 85eqeq12d 2780 . . . . . . . 8 (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑌)) + ((1 − 𝑇) · (𝐹𝑌)))))
8780, 86syl5ibrcom 238 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
88 olc 894 . . . . . . 7 ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
8987, 88syl6 35 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
90 oveq1 6849 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌))
91 oveq2 6850 . . . . . . . . . . . . . 14 (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇)))
9291oveq1d 6857 . . . . . . . . . . . . 13 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋))
9390, 92oveq12d 6860 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))
9493fveq2d 6379 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))))
95 oveq1 6849 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹𝑌)) = ((1 − 𝑇) · (𝐹𝑌)))
9691oveq1d 6857 . . . . . . . . . . . 12 (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹𝑋)) = ((1 − (1 − 𝑇)) · (𝐹𝑋)))
9795, 96oveq12d 6860 . . . . . . . . . . 11 (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
9894, 97breq12d 4822 . . . . . . . . . 10 (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋)))))
996adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌𝐷)
1003adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋𝐷)
10199, 100jca 507 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌𝐷𝑋𝐷))
102 simprr 789 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋)
103 simpll 783 . . . . . . . . . . 11 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑)
104 breq1 4812 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → (𝑥 < 𝑦𝑌 < 𝑦))
105 oveq2 6850 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌))
106105fvoveq1d 6864 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))))
107 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐹𝑥) = (𝐹𝑌))
108107oveq2d 6858 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → (𝑡 · (𝐹𝑥)) = (𝑡 · (𝐹𝑌)))
109108oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))
110106, 109breq12d 4822 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
111110ralbidv 3133 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))
112111imbi2d 331 . . . . . . . . . . . . 13 (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))))
113104, 112imbi12d 335 . . . . . . . . . . . 12 (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))))))
114 breq2 4813 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑌 < 𝑦𝑌 < 𝑋))
115 oveq2 6850 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋))
116115oveq2d 6858 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))
117116fveq2d 6379 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))))
118 fveq2 6375 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑋 → (𝐹𝑦) = (𝐹𝑋))
119118oveq2d 6858 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹𝑦)) = ((1 − 𝑡) · (𝐹𝑋)))
120119oveq2d 6858 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑋 → ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) = ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
121117, 120breq12d 4822 . . . . . . . . . . . . . . 15 (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
122121ralbidv 3133 . . . . . . . . . . . . . 14 (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))
123122imbi2d 331 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
124114, 123imbi12d 335 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋)))))))
125113, 124, 49vtocl2ga 3426 . . . . . . . . . . 11 ((𝑌𝐷𝑋𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))))
126101, 102, 103, 125syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹𝑌)) + ((1 − 𝑡) · (𝐹𝑋))))
127 1re 10293 . . . . . . . . . . . . 13 1 ∈ ℝ
128 elioore 12407 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 ∈ ℝ)
129 resubcl 10599 . . . . . . . . . . . . 13 ((1 ∈ ℝ ∧ 𝑇 ∈ ℝ) → (1 − 𝑇) ∈ ℝ)
130127, 128, 129sylancr 581 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ ℝ)
131 eliooord 12435 . . . . . . . . . . . . . 14 (𝑇 ∈ (0(,)1) → (0 < 𝑇𝑇 < 1))
132131simprd 489 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 𝑇 < 1)
133 posdif 10775 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
134128, 127, 133sylancl 580 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 − 𝑇)))
135132, 134mpbid 223 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → 0 < (1 − 𝑇))
136131simpld 488 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → 0 < 𝑇)
137 ltsubpos 10774 . . . . . . . . . . . . . 14 ((𝑇 ∈ ℝ ∧ 1 ∈ ℝ) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
138128, 127, 137sylancl 580 . . . . . . . . . . . . 13 (𝑇 ∈ (0(,)1) → (0 < 𝑇 ↔ (1 − 𝑇) < 1))
139136, 138mpbid 223 . . . . . . . . . . . 12 (𝑇 ∈ (0(,)1) → (1 − 𝑇) < 1)
140 0xr 10340 . . . . . . . . . . . . 13 0 ∈ ℝ*
141127rexri 10351 . . . . . . . . . . . . 13 1 ∈ ℝ*
142 elioo2 12418 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ 1 ∈ ℝ*) → ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)))
143140, 141, 142mp2an 683 . . . . . . . . . . . 12 ((1 − 𝑇) ∈ (0(,)1) ↔ ((1 − 𝑇) ∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))
144130, 135, 139, 143syl3anbrc 1443 . . . . . . . . . . 11 (𝑇 ∈ (0(,)1) → (1 − 𝑇) ∈ (0(,)1))
145144ad2antrl 719 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1))
14698, 126, 145rspcdva 3467 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))))
147 nncan 10564 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇)
14860, 59, 147sylancr 581 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − (1 − 𝑇)) = 𝑇)
149148oveq1d 6857 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · 𝑋) = (𝑇 · 𝑋))
150149oveq2d 6858 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)))
151127, 58, 129sylancr 581 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈ ℝ)
152151, 7remulcld 10324 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ)
153152recnd 10322 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ)
15458, 4remulcld 10324 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ)
155154recnd 10322 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ)
156153, 155addcomd 10492 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
157150, 156eqtrd 2799 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
158157adantr 472 . . . . . . . . . 10 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))
159158fveq2d 6379 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))))
160148oveq1d 6857 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − (1 − 𝑇)) · (𝐹𝑋)) = (𝑇 · (𝐹𝑋)))
161160oveq2d 6858 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = (((1 − 𝑇) · (𝐹𝑌)) + (𝑇 · (𝐹𝑋))))
162151, 74remulcld 10324 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℝ)
163162recnd 10322 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹𝑌)) ∈ ℂ)
16473, 3ffvelrnd 6550 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℝ)
16558, 164remulcld 10324 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℝ)
166165recnd 10322 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹𝑋)) ∈ ℂ)
167163, 166addcomd 10492 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + (𝑇 · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
168161, 167eqtrd 2799 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
169168adantr 472 . . . . . . . . 9 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹𝑌)) + ((1 − (1 − 𝑇)) · (𝐹𝑋))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
170146, 159, 1693brtr3d 4840 . . . . . . . 8 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
171170orcd 899 . . . . . . 7 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
172171expr 448 . . . . . 6 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
17355, 89, 1723jaod 1553 . . . . 5 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌𝑋 = 𝑌𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
1749, 173mpd 15 . . . 4 (((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
175174ex 401 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
176 elpri 4356 . . . 4 (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1))
17775addid2d 10491 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + (𝐹𝑌)) = (𝐹𝑌))
178164recnd 10322 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹𝑋) ∈ ℂ)
179178mul02d 10488 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑋)) = 0)
180179, 77oveq12d 6860 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))) = (0 + (𝐹𝑌)))
1814recnd 10322 . . . . . . . . . . 11 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ)
182181mul02d 10488 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0)
183182, 68oveq12d 6860 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌))
18466addid2d 10491 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌)
185183, 184eqtrd 2799 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌)
186185fveq2d 6379 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹𝑌))
187177, 180, 1863eqtr4rd 2810 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
188 oveq1 6849 . . . . . . . . 9 (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋))
189 oveq2 6850 . . . . . . . . . . 11 (𝑇 = 0 → (1 − 𝑇) = (1 − 0))
190 1m0e1 11400 . . . . . . . . . . 11 (1 − 0) = 1
191189, 190syl6eq 2815 . . . . . . . . . 10 (𝑇 = 0 → (1 − 𝑇) = 1)
192191oveq1d 6857 . . . . . . . . 9 (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌))
193188, 192oveq12d 6860 . . . . . . . 8 (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌)))
194193fveq2d 6379 . . . . . . 7 (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌))))
195 oveq1 6849 . . . . . . . 8 (𝑇 = 0 → (𝑇 · (𝐹𝑋)) = (0 · (𝐹𝑋)))
196191oveq1d 6857 . . . . . . . 8 (𝑇 = 0 → ((1 − 𝑇) · (𝐹𝑌)) = (1 · (𝐹𝑌)))
197195, 196oveq12d 6860 . . . . . . 7 (𝑇 = 0 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌))))
198194, 197eqeq12d 2780 . . . . . 6 (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹𝑋)) + (1 · (𝐹𝑌)))))
199187, 198syl5ibrcom 238 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
200178addid1d 10490 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹𝑋) + 0) = (𝐹𝑋))
201178mulid2d 10312 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · (𝐹𝑋)) = (𝐹𝑋))
20275mul02d 10488 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · (𝐹𝑌)) = 0)
203201, 202oveq12d 6860 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))) = ((𝐹𝑋) + 0))
204181mulid2d 10312 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋)
20566mul02d 10488 . . . . . . . . . 10 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0)
206204, 205oveq12d 6860 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0))
207181addid1d 10490 . . . . . . . . 9 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋)
208206, 207eqtrd 2799 . . . . . . . 8 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋)
209208fveq2d 6379 . . . . . . 7 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹𝑋))
210200, 203, 2093eqtr4rd 2810 . . . . . 6 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
211 oveq1 6849 . . . . . . . . 9 (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋))
212 oveq2 6850 . . . . . . . . . . 11 (𝑇 = 1 → (1 − 𝑇) = (1 − 1))
213 1m1e0 11344 . . . . . . . . . . 11 (1 − 1) = 0
214212, 213syl6eq 2815 . . . . . . . . . 10 (𝑇 = 1 → (1 − 𝑇) = 0)
215214oveq1d 6857 . . . . . . . . 9 (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌))
216211, 215oveq12d 6860 . . . . . . . 8 (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌)))
217216fveq2d 6379 . . . . . . 7 (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌))))
218 oveq1 6849 . . . . . . . 8 (𝑇 = 1 → (𝑇 · (𝐹𝑋)) = (1 · (𝐹𝑋)))
219214oveq1d 6857 . . . . . . . 8 (𝑇 = 1 → ((1 − 𝑇) · (𝐹𝑌)) = (0 · (𝐹𝑌)))
220218, 219oveq12d 6860 . . . . . . 7 (𝑇 = 1 → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌))))
221217, 220eqeq12d 2780 . . . . . 6 (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹𝑋)) + (0 · (𝐹𝑌)))))
222210, 221syl5ibrcom 238 . . . . 5 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
223199, 222jaod 885 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
224176, 223, 88syl56 36 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
225 0le1 10805 . . . . . 6 0 ≤ 1
226 prunioo 12508 . . . . . 6 ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1) → ((0(,)1) ∪ {0, 1}) = (0[,]1))
227140, 141, 225, 226mp3an 1585 . . . . 5 ((0(,)1) ∪ {0, 1}) = (0[,]1)
22857, 227syl6eleqr 2855 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0, 1}))
229 elun 3915 . . . 4 (𝑇 ∈ ((0(,)1) ∪ {0, 1}) ↔ (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
230228, 229sylib 209 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1}))
231175, 224, 230mpjaod 886 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌)))))
232 scvxcvx.3 . . . . 5 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
2331, 232cvxcl 25002 . . . 4 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
23473, 233ffvelrnd 6550 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ)
235165, 162readdcld 10323 . . 3 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∈ ℝ)
236234, 235leloed 10434 . 2 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))))
237231, 236mpbird 248 1 ((𝜑 ∧ (𝑋𝐷𝑌𝐷𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹𝑋)) + ((1 − 𝑇) · (𝐹𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873  w3o 1106  w3a 1107   = wceq 1652  wcel 2155  wral 3055  cun 3730  wss 3732  {cpr 4336   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  *cxr 10327   < clt 10328  cle 10329  cmin 10520  (,)cioo 12377  [,]cicc 12380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-ioo 12381  df-ico 12383  df-icc 12384
This theorem is referenced by:  amgmlem  25007  amgmwlem  43220
  Copyright terms: Public domain W3C validator