Proof of Theorem jensenlem2
Step | Hyp | Ref
| Expression |
1 | | cnfld0 19770 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
2 | | cnring 19768 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
3 | | ringabl 18580 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Abel) |
4 | 2, 3 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ Abel) |
5 | | jensen.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
6 | | jensenlem.2 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴) |
7 | 6 | unssad 3790 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
8 | | ssfi 8180 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) |
9 | 5, 7, 8 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
10 | | resubdrg 19954 |
. . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
11 | 10 | simpli 474 |
. . . . . . . 8
⊢ ℝ
∈ (SubRing‘ℂfld) |
12 | | subrgsubg 18786 |
. . . . . . . 8
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
(SubGrp‘ℂfld)) |
14 | | remulcl 10021 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
15 | 14 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
16 | | jensen.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) |
17 | | rge0ssre 12280 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
18 | | fss 6056 |
. . . . . . . . . 10
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → 𝑇:𝐴⟶ℝ) |
19 | 16, 17, 18 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:𝐴⟶ℝ) |
20 | | jensen.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:𝐴⟶𝐷) |
21 | | jensen.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
22 | 20, 21 | fssd 6057 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐴⟶ℝ) |
23 | | inidm 3822 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
24 | 15, 19, 22, 5, 5, 23 | off 6912 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋):𝐴⟶ℝ) |
25 | 24, 7 | fssresd 6071 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵):𝐵⟶ℝ) |
26 | | c0ex 10034 |
. . . . . . . . 9
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
V) |
28 | 25, 9, 27 | fdmfifsupp 8285 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) finSupp 0) |
29 | 1, 4, 9, 13, 25, 28 | gsumsubgcl 18320 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) ∈ ℝ) |
30 | 29 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) ∈ ℂ) |
31 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
32 | 17, 31 | sstri 3612 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
33 | 6 | unssbd 3791 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧} ⊆ 𝐴) |
34 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
35 | 34 | snss 4316 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
36 | 33, 35 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → 𝑧 ∈ 𝐴) |
37 | 16, 36 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑧) ∈ (0[,)+∞)) |
38 | 32, 37 | sseldi 3601 |
. . . . . 6
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℂ) |
39 | 20, 36 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑋‘𝑧) ∈ 𝐷) |
40 | 21, 39 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℝ) |
41 | 40 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℂ) |
42 | 38, 41 | mulcld 10060 |
. . . . 5
⊢ (𝜑 → ((𝑇‘𝑧) · (𝑋‘𝑧)) ∈ ℂ) |
43 | | jensen.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) |
44 | | jensen.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) |
45 | | jensen.7 |
. . . . . . . 8
⊢ (𝜑 → 0 <
(ℂfld Σg 𝑇)) |
46 | | jensen.8 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
47 | | jensenlem.1 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) |
48 | | jensenlem.s |
. . . . . . . 8
⊢ 𝑆 = (ℂfld
Σg (𝑇 ↾ 𝐵)) |
49 | | jensenlem.l |
. . . . . . . 8
⊢ 𝐿 = (ℂfld
Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) |
50 | 21, 43, 44, 5, 16, 20, 45, 46, 47, 6, 48, 49 | jensenlem1 24713 |
. . . . . . 7
⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧))) |
51 | | jensenlem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈
ℝ+) |
52 | 51 | rpred 11872 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
53 | | elrege0 12278 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) ↔ ((𝑇‘𝑧) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑧))) |
54 | 53 | simplbi 476 |
. . . . . . . . 9
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → (𝑇‘𝑧) ∈ ℝ) |
55 | 37, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℝ) |
56 | 52, 55 | readdcld 10069 |
. . . . . . 7
⊢ (𝜑 → (𝑆 + (𝑇‘𝑧)) ∈ ℝ) |
57 | 50, 56 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ℝ) |
58 | 57 | recnd 10068 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ℂ) |
59 | | 0red 10041 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
60 | 51 | rpgt0d 11875 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑆) |
61 | 53 | simprbi 480 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → 0 ≤ (𝑇‘𝑧)) |
62 | 37, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑇‘𝑧)) |
63 | 52, 55 | addge01d 10615 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (𝑇‘𝑧) ↔ 𝑆 ≤ (𝑆 + (𝑇‘𝑧)))) |
64 | 62, 63 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≤ (𝑆 + (𝑇‘𝑧))) |
65 | 64, 50 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ 𝐿) |
66 | 59, 52, 57, 60, 65 | ltletrd 10197 |
. . . . . 6
⊢ (𝜑 → 0 < 𝐿) |
67 | 66 | gt0ne0d 10592 |
. . . . 5
⊢ (𝜑 → 𝐿 ≠ 0) |
68 | 30, 42, 58, 67 | divdird 10839 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
69 | | cnfldbas 19750 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
70 | | cnfldadd 19751 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
71 | | ringcmn 18581 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
72 | 2, 71 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ CMnd) |
73 | 7 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
74 | 16 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
75 | 73, 74 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
76 | 32, 75 | sseldi 3601 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ ℂ) |
77 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ⊆ ℝ) |
78 | 20 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋‘𝑥) ∈ 𝐷) |
79 | 73, 78 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ 𝐷) |
80 | 77, 79 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℝ) |
81 | 80 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℂ) |
82 | 76, 81 | mulcld 10060 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝑋‘𝑥)) ∈ ℂ) |
83 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑇‘𝑥) = (𝑇‘𝑧)) |
84 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑋‘𝑥) = (𝑋‘𝑧)) |
85 | 83, 84 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝑋‘𝑥)) = ((𝑇‘𝑧) · (𝑋‘𝑧))) |
86 | 69, 70, 72, 9, 82, 36, 47, 42, 85 | gsumunsn 18359 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
87 | 16 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝑥 ∈ 𝐴 ↦ (𝑇‘𝑥))) |
88 | 20 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (𝑥 ∈ 𝐴 ↦ (𝑋‘𝑥))) |
89 | 5, 74, 78, 87, 88 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
90 | 89 | reseq1d 5395 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧}))) |
91 | 6 | resmptd 5452 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
92 | 90, 91 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
93 | 92 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
94 | 89 | reseq1d 5395 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵)) |
95 | 7 | resmptd 5452 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
96 | 94, 95 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
97 | 96 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
98 | 97 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
99 | 86, 93, 98 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
100 | 99 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿)) |
101 | 52 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
102 | 51 | rpne0d 11877 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ 0) |
103 | 30, 101, 58, 102, 67 | dmdcand 10830 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿)) |
104 | 58, 101, 58, 67 | divsubdird 10840 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝐿 / 𝐿) − (𝑆 / 𝐿))) |
105 | 50 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 − 𝑆) = ((𝑆 + (𝑇‘𝑧)) − 𝑆)) |
106 | 101, 38 | pncan2d 10394 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 + (𝑇‘𝑧)) − 𝑆) = (𝑇‘𝑧)) |
107 | 105, 106 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 − 𝑆) = (𝑇‘𝑧)) |
108 | 107 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝑇‘𝑧) / 𝐿)) |
109 | 58, 67 | dividd 10799 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 / 𝐿) = 1) |
110 | 109 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 / 𝐿) − (𝑆 / 𝐿)) = (1 − (𝑆 / 𝐿))) |
111 | 104, 108,
110 | 3eqtr3rd 2665 |
. . . . . . 7
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) = ((𝑇‘𝑧) / 𝐿)) |
112 | 111 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
113 | 38, 41, 58, 67 | div23d 10838 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
114 | 112, 113 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿)) |
115 | 103, 114 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
116 | 68, 100, 115 | 3eqtr4d 2666 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
117 | | jensenlem.4 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷) |
118 | 52, 57, 67 | redivcld 10853 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ∈ ℝ) |
119 | 51 | rpge0d 11876 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑆) |
120 | | divge0 10892 |
. . . . . . 7
⊢ (((𝑆 ∈ ℝ ∧ 0 ≤
𝑆) ∧ (𝐿 ∈ ℝ ∧ 0 < 𝐿)) → 0 ≤ (𝑆 / 𝐿)) |
121 | 52, 119, 57, 66, 120 | syl22anc 1327 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑆 / 𝐿)) |
122 | 58 | mulid1d 10057 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 1) = 𝐿) |
123 | 65, 122 | breqtrrd 4681 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ (𝐿 · 1)) |
124 | | 1red 10055 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
125 | | ledivmul 10899 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝐿 ∈
ℝ ∧ 0 < 𝐿))
→ ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
126 | 52, 124, 57, 66, 125 | syl112anc 1330 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
127 | 123, 126 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ≤ 1) |
128 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
129 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
130 | 128, 129 | elicc2i 12239 |
. . . . . 6
⊢ ((𝑆 / 𝐿) ∈ (0[,]1) ↔ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 ≤ (𝑆 / 𝐿) ∧ (𝑆 / 𝐿) ≤ 1)) |
131 | 118, 121,
127, 130 | syl3anbrc 1246 |
. . . . 5
⊢ (𝜑 → (𝑆 / 𝐿) ∈ (0[,]1)) |
132 | 117, 39, 131 | 3jca 1242 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) |
133 | 21, 44 | cvxcl 24711 |
. . . 4
⊢ ((𝜑 ∧ (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
134 | 132, 133 | mpdan 702 |
. . 3
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
135 | 116, 134 | eqeltrd 2701 |
. 2
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷) |
136 | 43, 134 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ∈ ℝ) |
137 | 43, 117 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
138 | 118, 137 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ∈ ℝ) |
139 | 43, 39 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℝ) |
140 | 55, 139 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
141 | 140, 57, 67 | redivcld 10853 |
. . . . 5
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) ∈ ℝ) |
142 | 138, 141 | readdcld 10069 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ∈ ℝ) |
143 | | fco 6058 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
144 | 43, 20, 143 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
145 | 15, 19, 144, 5, 5, 23 | off 6912 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℝ) |
146 | 145, 7 | fssresd 6071 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵):𝐵⟶ℝ) |
147 | 146, 9, 27 | fdmfifsupp 8285 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) finSupp 0) |
148 | 1, 4, 9, 13, 146, 147 | gsumsubgcl 18320 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℝ) |
149 | 148, 52, 102 | redivcld 10853 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ) |
150 | 118, 149 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
151 | | resubcl 10345 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (𝑆 /
𝐿) ∈ ℝ) →
(1 − (𝑆 / 𝐿)) ∈
ℝ) |
152 | 129, 118,
151 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) ∈ ℝ) |
153 | 152, 139 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
154 | 150, 153 | readdcld 10069 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ∈ ℝ) |
155 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · 𝑥) = (𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
156 | 155 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)))) |
158 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘𝑥) = (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
159 | 158 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)))) |
160 | 159 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
161 | 157, 160 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
162 | 161 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
163 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · (𝑋‘𝑧))) |
164 | 163 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) |
165 | 164 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))))) |
166 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑧))) |
167 | 166 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) |
168 | 167 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) |
169 | 165, 168 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋‘𝑧) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))))) |
170 | 169 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑦 = (𝑋‘𝑧) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))))) |
171 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) = ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
172 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑆 / 𝐿) → (1 − 𝑡) = (1 − (𝑆 / 𝐿))) |
173 | 172 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝑋‘𝑧)) = ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) |
174 | 171, 173 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
175 | 174 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
176 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) = ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)))) |
177 | 172 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
178 | 176, 177 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
179 | 175, 178 | breq12d 4666 |
. . . . . . . . 9
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) ↔ (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
180 | 179 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) ↔ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))))) |
181 | 46 | expcom 451 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1)) → (𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
182 | 162, 170,
180, 181 | vtocl3ga 3276 |
. . . . . . 7
⊢
((((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1)) → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
183 | 117, 39, 131, 182 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
184 | 183 | pm2.43i 52 |
. . . . 5
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
185 | 111 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
186 | 139 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℂ) |
187 | 38, 186, 58, 67 | div23d 10838 |
. . . . . . 7
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
188 | 185, 187 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) |
189 | 188 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
190 | 184, 189 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
191 | 187, 185 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
192 | 191 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
193 | | jensenlem.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) |
194 | 52, 57, 60, 66 | divgt0d 10959 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝑆 / 𝐿)) |
195 | | lemul2 10876 |
. . . . . . . 8
⊢ (((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ ∧
((ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ ∧ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 < (𝑆 / 𝐿))) → ((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
196 | 137, 149,
118, 194, 195 | syl112anc 1330 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
197 | 193, 196 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆))) |
198 | 138, 150,
153, 197 | leadd1dd 10641 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
199 | 192, 198 | eqbrtrd 4675 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
200 | 136, 142,
154, 190, 199 | letrd 10194 |
. . 3
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
201 | 116 | fveq2d 6195 |
. . 3
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
202 | 148 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℂ) |
203 | 140 | recnd 10068 |
. . . . 5
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℂ) |
204 | 202, 203,
58, 67 | divdird 10839 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
205 | 17, 74 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ ℝ) |
206 | 43 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘𝑥) ∈ 𝐷) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
207 | 78, 206 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
208 | 205, 207 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℝ) |
209 | 208 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
210 | 73, 209 | syldan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
211 | 84 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐹‘(𝑋‘𝑥)) = (𝐹‘(𝑋‘𝑧))) |
212 | 83, 211 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) = ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) |
213 | 69, 70, 72, 9, 210, 36, 47, 203, 212 | gsumunsn 18359 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
214 | 43 | feqmptd 6249 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦))) |
215 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑥))) |
216 | 78, 88, 214, 215 | fmptco 6396 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋‘𝑥)))) |
217 | 5, 74, 207, 87, 216 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
218 | 217 | reseq1d 5395 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧}))) |
219 | 6 | resmptd 5452 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
220 | 218, 219 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
221 | 220 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
222 | 217 | reseq1d 5395 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵)) |
223 | 7 | resmptd 5452 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
224 | 222, 223 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
225 | 224 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
226 | 225 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
227 | 213, 221,
226 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
228 | 227 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿)) |
229 | 202, 101,
58, 102, 67 | dmdcand 10830 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿)) |
230 | 229, 188 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
231 | 204, 228,
230 | 3eqtr4d 2666 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
232 | 200, 201,
231 | 3brtr4d 4685 |
. 2
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) |
233 | 135, 232 | jca 554 |
1
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿))) |