Proof of Theorem scvxcvx
Step | Hyp | Ref
| Expression |
1 | | scvxcvx.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
2 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐷 ⊆ ℝ) |
3 | | simpr1 1060 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ 𝐷) |
4 | 2, 3 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℝ) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑋 ∈ ℝ) |
6 | | simpr2 1061 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ 𝐷) |
7 | 2, 6 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℝ) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → 𝑌 ∈ ℝ) |
9 | 5, 8 | lttri4d 10057 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋)) |
10 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑇 ∈ (0(,)1)) |
11 | 3 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 ∈ 𝐷) |
12 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑌 ∈ 𝐷) |
13 | 11, 12 | jca 553 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) |
14 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝑋 < 𝑌) |
15 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → 𝜑) |
16 | | breq1 4586 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑥 < 𝑦 ↔ 𝑋 < 𝑦)) |
17 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑋 → (𝑡 · 𝑥) = (𝑡 · 𝑋)) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑋 → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)))) |
20 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
21 | 20 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑋 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑋))) |
22 | 21 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
23 | 19, 22 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑋 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
24 | 23 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
25 | 24 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
26 | 16, 25 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))))) |
27 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → (𝑋 < 𝑦 ↔ 𝑋 < 𝑌)) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑌)) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑌 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑌 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)))) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) |
32 | 31 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑌 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑌))) |
33 | 32 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑌 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))) |
34 | 30, 33 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑌 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))) |
35 | 34 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))) |
36 | 35 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))) |
37 | 27, 36 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑌 → ((𝑋 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))))))) |
38 | | scvxcvx.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
39 | 38 | 3expia 1259 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → (𝑡 ∈ (0(,)1) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
40 | 39 | ralrimiv 2948 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
41 | 40 | expcom 450 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
42 | 41 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
43 | 26, 37, 42 | vtocl2ga 3247 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷) → (𝑋 < 𝑌 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))))) |
44 | 13, 14, 15, 43 | syl3c 64 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌)))) |
45 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (𝑡 · 𝑋) = (𝑇 · 𝑋)) |
46 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (1 − 𝑡) = (1 − 𝑇)) |
47 | 46 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · 𝑌) = ((1 − 𝑇) · 𝑌)) |
48 | 45, 47 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) |
49 | 48 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))) |
50 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (𝑡 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋))) |
51 | 46 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ((1 − 𝑡) · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌))) |
52 | 50, 51 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
53 | 49, 52 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
54 | 53 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑇 ∈ (0(,)1) →
(∀𝑡 ∈
(0(,)1)(𝐹‘((𝑡 · 𝑋) + ((1 − 𝑡) · 𝑌))) < ((𝑡 · (𝐹‘𝑋)) + ((1 − 𝑡) · (𝐹‘𝑌))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
55 | 10, 44, 54 | sylc 63 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
56 | 55 | orcd 406 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑋 < 𝑌)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
57 | 56 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 < 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
58 | | unitssre 12190 |
. . . . . . . . . . . . . . . 16
⊢ (0[,]1)
⊆ ℝ |
59 | | simpr3 1062 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ (0[,]1)) |
60 | 58, 59 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ℂ) |
62 | | ax-1cn 9873 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
63 | | pncan3 10168 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑇 + (1
− 𝑇)) =
1) |
64 | 61, 62, 63 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 + (1 − 𝑇)) = 1) |
65 | 64 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = (1 · 𝑌)) |
66 | | subcl 10159 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − 𝑇) ∈ ℂ) |
67 | 62, 61, 66 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈
ℂ) |
68 | 7 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑌 ∈ ℂ) |
69 | 61, 67, 68 | adddird 9944 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · 𝑌) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) |
70 | 68 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑌) = 𝑌) |
71 | 65, 69, 70 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)) = 𝑌) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = (𝐹‘𝑌)) |
73 | 64 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌))) |
74 | | scvxcvx.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝐹:𝐷⟶ℝ) |
76 | 75, 6 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℝ) |
77 | 76 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑌) ∈ ℂ) |
78 | 61, 67, 77 | adddird 9944 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 + (1 − 𝑇)) · (𝐹‘𝑌)) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
79 | 77 | mulid2d 9937 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑌)) = (𝐹‘𝑌)) |
80 | 73, 78, 79 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))) = (𝐹‘𝑌)) |
81 | 72, 80 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
82 | 81 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
83 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑋 = 𝑌 → (𝑇 · 𝑋) = (𝑇 · 𝑌)) |
84 | 83 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑋 = 𝑌 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) |
85 | 84 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌)))) |
86 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑋 = 𝑌 → (𝐹‘𝑋) = (𝐹‘𝑌)) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑋 = 𝑌 → (𝑇 · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑌))) |
88 | 87 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑋 = 𝑌 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
89 | 85, 88 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((𝑇 · 𝑌) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑌)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
90 | 82, 89 | syl5ibrcom 236 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
91 | | olc 398 |
. . . . . . 7
⊢ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
92 | 90, 91 | syl6 34 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑋 = 𝑌 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
93 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
94 | | elioore 12076 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (0(,)1) → 𝑇 ∈
ℝ) |
95 | | resubcl 10224 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝑇
∈ ℝ) → (1 − 𝑇) ∈ ℝ) |
96 | 93, 94, 95 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (0(,)1) → (1
− 𝑇) ∈
ℝ) |
97 | | eliooord 12104 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ (0(,)1) → (0 <
𝑇 ∧ 𝑇 < 1)) |
98 | 97 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (0(,)1) → 𝑇 < 1) |
99 | | posdif 10400 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑇 < 1
↔ 0 < (1 − 𝑇))) |
100 | 94, 93, 99 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (0(,)1) → (𝑇 < 1 ↔ 0 < (1 −
𝑇))) |
101 | 98, 100 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (0(,)1) → 0 < (1
− 𝑇)) |
102 | 97 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (0(,)1) → 0 <
𝑇) |
103 | | ltsubpos 10399 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ ℝ ∧ 1 ∈
ℝ) → (0 < 𝑇
↔ (1 − 𝑇) <
1)) |
104 | 94, 93, 103 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ (0(,)1) → (0 <
𝑇 ↔ (1 − 𝑇) < 1)) |
105 | 102, 104 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ (0(,)1) → (1
− 𝑇) <
1) |
106 | | 0xr 9965 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
107 | 93 | rexri 9976 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ* |
108 | | elioo2 12087 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((1
− 𝑇) ∈ (0(,)1)
↔ ((1 − 𝑇)
∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1))) |
109 | 106, 107,
108 | mp2an 704 |
. . . . . . . . . . . 12
⊢ ((1
− 𝑇) ∈ (0(,)1)
↔ ((1 − 𝑇)
∈ ℝ ∧ 0 < (1 − 𝑇) ∧ (1 − 𝑇) < 1)) |
110 | 96, 101, 105, 109 | syl3anbrc 1239 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (0(,)1) → (1
− 𝑇) ∈
(0(,)1)) |
111 | 110 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (1 − 𝑇) ∈ (0(,)1)) |
112 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 ∈ 𝐷) |
113 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑋 ∈ 𝐷) |
114 | 112, 113 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷)) |
115 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝑌 < 𝑋) |
116 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → 𝜑) |
117 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑌 → (𝑥 < 𝑦 ↔ 𝑌 < 𝑦)) |
118 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑌 → (𝑡 · 𝑥) = (𝑡 · 𝑌)) |
119 | 118 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑌 → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) |
120 | 119 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)))) |
121 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌)) |
122 | 121 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑌 → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘𝑌))) |
123 | 122 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
124 | 120, 123 | breq12d 4596 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
125 | 124 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
126 | 125 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑌 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
127 | 117, 126 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → ((𝑥 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))))) |
128 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑋)) |
129 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · 𝑋)) |
130 | 129 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑋 → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) |
131 | 130 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑋 → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)))) |
132 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋)) |
133 | 132 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑋 → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘𝑋))) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑋 → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))) |
135 | 131, 134 | breq12d 4596 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑋 → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))) |
136 | 135 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑋 → (∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))) |
137 | 136 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → ((𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))) |
138 | 128, 137 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑋 → ((𝑌 < 𝑦 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑦))))) ↔ (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))))))) |
139 | 127, 138,
42 | vtocl2ga 3247 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷) → (𝑌 < 𝑋 → (𝜑 → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))))) |
140 | 114, 115,
116, 139 | syl3c 64 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ∀𝑡 ∈ (0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋)))) |
141 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (1 − 𝑇) → (𝑡 · 𝑌) = ((1 − 𝑇) · 𝑌)) |
142 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (1 − 𝑇) → (1 − 𝑡) = (1 − (1 − 𝑇))) |
143 | 142 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · 𝑋) = ((1 − (1 − 𝑇)) · 𝑋)) |
144 | 141, 143 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋)) = (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) |
145 | 144 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑡 = (1 − 𝑇) → (𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) = (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)))) |
146 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (1 − 𝑇) → (𝑡 · (𝐹‘𝑌)) = ((1 − 𝑇) · (𝐹‘𝑌))) |
147 | 142 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (1 − 𝑇) → ((1 − 𝑡) · (𝐹‘𝑋)) = ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) |
148 | 146, 147 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑡 = (1 − 𝑇) → ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))) |
149 | 145, 148 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑡 = (1 − 𝑇) → ((𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) ↔ (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))) |
150 | 149 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((1
− 𝑇) ∈ (0(,)1)
→ (∀𝑡 ∈
(0(,)1)(𝐹‘((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑋))) < ((𝑡 · (𝐹‘𝑌)) + ((1 − 𝑡) · (𝐹‘𝑋))) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))))) |
151 | 111, 140,
150 | sylc 63 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) < (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋)))) |
152 | | nncan 10189 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − (1 − 𝑇)) = 𝑇) |
153 | 62, 61, 152 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − (1
− 𝑇)) = 𝑇) |
154 | 153 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1
− 𝑇)) · 𝑋) = (𝑇 · 𝑋)) |
155 | 154 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋))) |
156 | 93, 60, 95 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 − 𝑇) ∈
ℝ) |
157 | 156, 7 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℝ) |
158 | 157 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · 𝑌) ∈ ℂ) |
159 | 60, 4 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℝ) |
160 | 159 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · 𝑋) ∈ ℂ) |
161 | 158, 160 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + (𝑇 · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) |
162 | 155, 161 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) |
163 | 162 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋)) = ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) |
164 | 163 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘(((1 − 𝑇) · 𝑌) + ((1 − (1 − 𝑇)) · 𝑋))) = (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)))) |
165 | 153 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − (1
− 𝑇)) · (𝐹‘𝑋)) = (𝑇 · (𝐹‘𝑋))) |
166 | 165 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋)))) |
167 | 156, 76 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℝ) |
168 | 167 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 − 𝑇) · (𝐹‘𝑌)) ∈ ℂ) |
169 | 75, 3 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℝ) |
170 | 60, 169 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℝ) |
171 | 170 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 · (𝐹‘𝑋)) ∈ ℂ) |
172 | 168, 171 | addcomd 10117 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + (𝑇 · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
173 | 166, 172 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
174 | 173 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (((1 − 𝑇) · (𝐹‘𝑌)) + ((1 − (1 − 𝑇)) · (𝐹‘𝑋))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
175 | 151, 164,
174 | 3brtr3d 4614 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |
176 | 175 | orcd 406 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ (𝑇 ∈ (0(,)1) ∧ 𝑌 < 𝑋)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
177 | 176 | expr 641 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → (𝑌 < 𝑋 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
178 | 57, 92, 177 | 3jaod 1384 |
. . . . 5
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ∨ 𝑌 < 𝑋) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
179 | 9, 178 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) ∧ 𝑇 ∈ (0(,)1)) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
180 | 179 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
181 | | elpri 4145 |
. . . 4
⊢ (𝑇 ∈ {0, 1} → (𝑇 = 0 ∨ 𝑇 = 1)) |
182 | 77 | addid2d 10116 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + (𝐹‘𝑌)) = (𝐹‘𝑌)) |
183 | 169 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘𝑋) ∈ ℂ) |
184 | 183 | mul02d 10113 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑋)) = 0) |
185 | 184, 79 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))) = (0 + (𝐹‘𝑌))) |
186 | 4 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑋 ∈ ℂ) |
187 | 186 | mul02d 10113 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑋) = 0) |
188 | 187, 70 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = (0 + 𝑌)) |
189 | 68 | addid2d 10116 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 + 𝑌) = 𝑌) |
190 | 188, 189 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((0 · 𝑋) + (1 · 𝑌)) = 𝑌) |
191 | 190 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = (𝐹‘𝑌)) |
192 | 182, 185,
191 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))) |
193 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑇 = 0 → (𝑇 · 𝑋) = (0 · 𝑋)) |
194 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑇 = 0 → (1 − 𝑇) = (1 −
0)) |
195 | | 1m0e1 11008 |
. . . . . . . . . . 11
⊢ (1
− 0) = 1 |
196 | 194, 195 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑇 = 0 → (1 − 𝑇) = 1) |
197 | 196 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑇 = 0 → ((1 − 𝑇) · 𝑌) = (1 · 𝑌)) |
198 | 193, 197 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑇 = 0 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((0 · 𝑋) + (1 · 𝑌))) |
199 | 198 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((0 · 𝑋) + (1 · 𝑌)))) |
200 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑇 = 0 → (𝑇 · (𝐹‘𝑋)) = (0 · (𝐹‘𝑋))) |
201 | 196 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑇 = 0 → ((1 − 𝑇) · (𝐹‘𝑌)) = (1 · (𝐹‘𝑌))) |
202 | 200, 201 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑇 = 0 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌)))) |
203 | 199, 202 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑇 = 0 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((0 · 𝑋) + (1 · 𝑌))) = ((0 · (𝐹‘𝑋)) + (1 · (𝐹‘𝑌))))) |
204 | 192, 203 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 0 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
205 | 183 | addid1d 10115 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘𝑋) + 0) = (𝐹‘𝑋)) |
206 | 183 | mulid2d 9937 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · (𝐹‘𝑋)) = (𝐹‘𝑋)) |
207 | 77 | mul02d 10113 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · (𝐹‘𝑌)) = 0) |
208 | 206, 207 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))) = ((𝐹‘𝑋) + 0)) |
209 | 186 | mulid2d 9937 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (1 · 𝑋) = 𝑋) |
210 | 68 | mul02d 10113 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (0 · 𝑌) = 0) |
211 | 209, 210 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = (𝑋 + 0)) |
212 | 186 | addid1d 10115 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑋 + 0) = 𝑋) |
213 | 211, 212 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((1 · 𝑋) + (0 · 𝑌)) = 𝑋) |
214 | 213 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = (𝐹‘𝑋)) |
215 | 205, 208,
214 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌)))) |
216 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑇 = 1 → (𝑇 · 𝑋) = (1 · 𝑋)) |
217 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑇 = 1 → (1 − 𝑇) = (1 −
1)) |
218 | | 1m1e0 10966 |
. . . . . . . . . . 11
⊢ (1
− 1) = 0 |
219 | 217, 218 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑇 = 1 → (1 − 𝑇) = 0) |
220 | 219 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑇 = 1 → ((1 − 𝑇) · 𝑌) = (0 · 𝑌)) |
221 | 216, 220 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑇 = 1 → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) = ((1 · 𝑋) + (0 · 𝑌))) |
222 | 221 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = (𝐹‘((1 · 𝑋) + (0 · 𝑌)))) |
223 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑇 = 1 → (𝑇 · (𝐹‘𝑋)) = (1 · (𝐹‘𝑋))) |
224 | 219 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝑇 = 1 → ((1 − 𝑇) · (𝐹‘𝑌)) = (0 · (𝐹‘𝑌))) |
225 | 223, 224 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑇 = 1 → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌)))) |
226 | 222, 225 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑇 = 1 → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ (𝐹‘((1 · 𝑋) + (0 · 𝑌))) = ((1 · (𝐹‘𝑋)) + (0 · (𝐹‘𝑌))))) |
227 | 215, 226 | syl5ibrcom 236 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 = 1 → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
228 | 204, 227 | jaod 394 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 = 0 ∨ 𝑇 = 1) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
229 | 181, 228,
91 | syl56 35 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ {0, 1} → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
230 | | 0le1 10430 |
. . . . . 6
⊢ 0 ≤
1 |
231 | | prunioo 12172 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1)
→ ((0(,)1) ∪ {0, 1}) = (0[,]1)) |
232 | 106, 107,
230, 231 | mp3an 1416 |
. . . . 5
⊢ ((0(,)1)
∪ {0, 1}) = (0[,]1) |
233 | 59, 232 | syl6eleqr 2699 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → 𝑇 ∈ ((0(,)1) ∪ {0,
1})) |
234 | | elun 3715 |
. . . 4
⊢ (𝑇 ∈ ((0(,)1) ∪ {0, 1})
↔ (𝑇 ∈ (0(,)1)
∨ 𝑇 ∈ {0,
1})) |
235 | 233, 234 | sylib 207 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝑇 ∈ (0(,)1) ∨ 𝑇 ∈ {0, 1})) |
236 | 180, 229,
235 | mpjaod 395 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))) |
237 | | scvxcvx.3 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) |
238 | 1, 237 | cvxcl 24511 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷) |
239 | 75, 238 | ffvelrnd 6268 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ∈ ℝ) |
240 | 170, 167 | readdcld 9948 |
. . 3
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∈ ℝ) |
241 | 239, 240 | leloed 10059 |
. 2
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ↔ ((𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) < ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))) ∨ (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) = ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))))) |
242 | 236, 241 | mpbird 246 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌)))) |