Proof of Theorem jensenlem2
Step | Hyp | Ref
| Expression |
1 | | cnfld0 20170 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
2 | | cnring 20168 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
3 | | ringabl 18971 |
. . . . . . . 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 4013 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
8 | | ssfi 8470 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ Fin) |
9 | 5, 7, 8 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
10 | | resubdrg 20355 |
. . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
11 | 10 | simpli 478 |
. . . . . . . 8
⊢ ℝ
∈ (SubRing‘ℂfld) |
12 | | subrgsubg 19182 |
. . . . . . . 8
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
(SubGrp‘ℂfld)) |
14 | | remulcl 10359 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
15 | 14 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
16 | | jensen.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) |
17 | | rge0ssre 12598 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
18 | | fss 6306 |
. . . . . . . . . 10
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → 𝑇:𝐴⟶ℝ) |
19 | 16, 17, 18 | sylancl 580 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:𝐴⟶ℝ) |
20 | | jensen.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:𝐴⟶𝐷) |
21 | | jensen.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
22 | 20, 21 | fssd 6307 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐴⟶ℝ) |
23 | | inidm 4043 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
24 | 15, 19, 22, 5, 5, 23 | off 7191 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋):𝐴⟶ℝ) |
25 | 24, 7 | fssresd 6323 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵):𝐵⟶ℝ) |
26 | | c0ex 10372 |
. . . . . . . . 9
⊢ 0 ∈
V |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
V) |
28 | 25, 9, 27 | fdmfifsupp 8575 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) finSupp 0) |
29 | 1, 4, 9, 13, 25, 28 | gsumsubgcl 18710 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) ∈ ℝ) |
30 | 29 | recnd 10407 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) ∈ ℂ) |
31 | | ax-resscn 10331 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
32 | 17, 31 | sstri 3830 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
33 | 6 | unssbd 4014 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧} ⊆ 𝐴) |
34 | | vex 3401 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
35 | 34 | snss 4549 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
36 | 33, 35 | sylibr 226 |
. . . . . . . 8
⊢ (𝜑 → 𝑧 ∈ 𝐴) |
37 | 16, 36 | ffvelrnd 6626 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑧) ∈ (0[,)+∞)) |
38 | 32, 37 | sseldi 3819 |
. . . . . 6
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℂ) |
39 | 20, 36 | ffvelrnd 6626 |
. . . . . . . 8
⊢ (𝜑 → (𝑋‘𝑧) ∈ 𝐷) |
40 | 21, 39 | sseldd 3822 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℝ) |
41 | 40 | recnd 10407 |
. . . . . 6
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℂ) |
42 | 38, 41 | mulcld 10399 |
. . . . 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 25169 |
. . . . . . 7
⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧))) |
51 | | jensenlem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈
ℝ+) |
52 | 51 | rpred 12185 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
53 | | elrege0 12596 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) ↔ ((𝑇‘𝑧) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑧))) |
54 | 53 | simplbi 493 |
. . . . . . . . 9
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → (𝑇‘𝑧) ∈ ℝ) |
55 | 37, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℝ) |
56 | 52, 55 | readdcld 10408 |
. . . . . . 7
⊢ (𝜑 → (𝑆 + (𝑇‘𝑧)) ∈ ℝ) |
57 | 50, 56 | eqeltrd 2859 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ℝ) |
58 | 57 | recnd 10407 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ℂ) |
59 | | 0red 10382 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
60 | 51 | rpgt0d 12188 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑆) |
61 | 53 | simprbi 492 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → 0 ≤ (𝑇‘𝑧)) |
62 | 37, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑇‘𝑧)) |
63 | 52, 55 | addge01d 10965 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (𝑇‘𝑧) ↔ 𝑆 ≤ (𝑆 + (𝑇‘𝑧)))) |
64 | 62, 63 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≤ (𝑆 + (𝑇‘𝑧))) |
65 | 64, 50 | breqtrrd 4916 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ 𝐿) |
66 | 59, 52, 57, 60, 65 | ltletrd 10538 |
. . . . . 6
⊢ (𝜑 → 0 < 𝐿) |
67 | 66 | gt0ne0d 10941 |
. . . . 5
⊢ (𝜑 → 𝐿 ≠ 0) |
68 | 30, 42, 58, 67 | divdird 11191 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
69 | | cnfldbas 20150 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
70 | | cnfldadd 20151 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
71 | | ringcmn 18972 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
72 | 2, 71 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ CMnd) |
73 | 7 | sselda 3821 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
74 | 16 | ffvelrnda 6625 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
75 | 73, 74 | syldan 585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
76 | 32, 75 | sseldi 3819 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ ℂ) |
77 | 21 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ⊆ ℝ) |
78 | 20 | ffvelrnda 6625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋‘𝑥) ∈ 𝐷) |
79 | 73, 78 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ 𝐷) |
80 | 77, 79 | sseldd 3822 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℝ) |
81 | 80 | recnd 10407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℂ) |
82 | 76, 81 | mulcld 10399 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝑋‘𝑥)) ∈ ℂ) |
83 | | fveq2 6448 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑇‘𝑥) = (𝑇‘𝑧)) |
84 | | fveq2 6448 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑋‘𝑥) = (𝑋‘𝑧)) |
85 | 83, 84 | oveq12d 6942 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝑋‘𝑥)) = ((𝑇‘𝑧) · (𝑋‘𝑧))) |
86 | 69, 70, 72, 9, 82, 36, 47, 42, 85 | gsumunsn 18749 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
87 | 16 | feqmptd 6511 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝑥 ∈ 𝐴 ↦ (𝑇‘𝑥))) |
88 | 20 | feqmptd 6511 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (𝑥 ∈ 𝐴 ↦ (𝑋‘𝑥))) |
89 | 5, 74, 78, 87, 88 | offval2 7193 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
90 | 89 | reseq1d 5643 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧}))) |
91 | 6 | resmptd 5704 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
92 | 90, 91 | eqtrd 2814 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
93 | 92 | oveq2d 6940 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
94 | 89 | reseq1d 5643 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵)) |
95 | 7 | resmptd 5704 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
96 | 94, 95 | eqtrd 2814 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
97 | 96 | oveq2d 6940 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
98 | 97 | oveq1d 6939 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
99 | 86, 93, 98 | 3eqtr4d 2824 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
100 | 99 | oveq1d 6939 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿)) |
101 | 52 | recnd 10407 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
102 | 51 | rpne0d 12190 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ 0) |
103 | 30, 101, 58, 102, 67 | dmdcand 11182 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿)) |
104 | 58, 101, 58, 67 | divsubdird 11192 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝐿 / 𝐿) − (𝑆 / 𝐿))) |
105 | 101, 38, 50 | mvrladdd 10790 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 − 𝑆) = (𝑇‘𝑧)) |
106 | 105 | oveq1d 6939 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝑇‘𝑧) / 𝐿)) |
107 | 58, 67 | dividd 11151 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 / 𝐿) = 1) |
108 | 107 | oveq1d 6939 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 / 𝐿) − (𝑆 / 𝐿)) = (1 − (𝑆 / 𝐿))) |
109 | 104, 106,
108 | 3eqtr3rd 2823 |
. . . . . . 7
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) = ((𝑇‘𝑧) / 𝐿)) |
110 | 109 | oveq1d 6939 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
111 | 38, 41, 58, 67 | div23d 11190 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
112 | 110, 111 | eqtr4d 2817 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿)) |
113 | 103, 112 | oveq12d 6942 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) = (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
114 | 68, 100, 113 | 3eqtr4d 2824 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
115 | | jensenlem.4 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷) |
116 | 52, 57, 67 | redivcld 11205 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ∈ ℝ) |
117 | 51 | rpge0d 12189 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑆) |
118 | | divge0 11248 |
. . . . . . 7
⊢ (((𝑆 ∈ ℝ ∧ 0 ≤
𝑆) ∧ (𝐿 ∈ ℝ ∧ 0 < 𝐿)) → 0 ≤ (𝑆 / 𝐿)) |
119 | 52, 117, 57, 66, 118 | syl22anc 829 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑆 / 𝐿)) |
120 | 58 | mulid1d 10396 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 1) = 𝐿) |
121 | 65, 120 | breqtrrd 4916 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ (𝐿 · 1)) |
122 | | 1red 10379 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
123 | | ledivmul 11255 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝐿 ∈
ℝ ∧ 0 < 𝐿))
→ ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
124 | 52, 122, 57, 66, 123 | syl112anc 1442 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
125 | 121, 124 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ≤ 1) |
126 | | elicc01 12608 |
. . . . . 6
⊢ ((𝑆 / 𝐿) ∈ (0[,]1) ↔ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 ≤ (𝑆 / 𝐿) ∧ (𝑆 / 𝐿) ≤ 1)) |
127 | 116, 119,
125, 126 | syl3anbrc 1400 |
. . . . 5
⊢ (𝜑 → (𝑆 / 𝐿) ∈ (0[,]1)) |
128 | 115, 39, 127 | 3jca 1119 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) |
129 | 21, 44 | cvxcl 25167 |
. . . 4
⊢ ((𝜑 ∧ (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
130 | 128, 129 | mpdan 677 |
. . 3
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
131 | 114, 130 | eqeltrd 2859 |
. 2
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷) |
132 | 43, 130 | ffvelrnd 6626 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ∈ ℝ) |
133 | 43, 115 | ffvelrnd 6626 |
. . . . . 6
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
134 | 116, 133 | remulcld 10409 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ∈ ℝ) |
135 | 43, 39 | ffvelrnd 6626 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℝ) |
136 | 55, 135 | remulcld 10409 |
. . . . . 6
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
137 | 136, 57, 67 | redivcld 11205 |
. . . . 5
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) ∈ ℝ) |
138 | 134, 137 | readdcld 10408 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ∈ ℝ) |
139 | | fco 6310 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
140 | 43, 20, 139 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
141 | 15, 19, 140, 5, 5, 23 | off 7191 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℝ) |
142 | 141, 7 | fssresd 6323 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵):𝐵⟶ℝ) |
143 | 142, 9, 27 | fdmfifsupp 8575 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) finSupp 0) |
144 | 1, 4, 9, 13, 142, 143 | gsumsubgcl 18710 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℝ) |
145 | 144, 52, 102 | redivcld 11205 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ) |
146 | 116, 145 | remulcld 10409 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
147 | | 1re 10378 |
. . . . . . 7
⊢ 1 ∈
ℝ |
148 | | resubcl 10689 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (𝑆 /
𝐿) ∈ ℝ) →
(1 − (𝑆 / 𝐿)) ∈
ℝ) |
149 | 147, 116,
148 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) ∈ ℝ) |
150 | 149, 135 | remulcld 10409 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
151 | 146, 150 | readdcld 10408 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ∈ ℝ) |
152 | | oveq2 6932 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · 𝑥) = (𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
153 | 152 | fvoveq1d 6946 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)))) |
154 | | fveq2 6448 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘𝑥) = (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
155 | 154 | oveq2d 6940 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)))) |
156 | 155 | oveq1d 6939 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
157 | 153, 156 | breq12d 4901 |
. . . . . . . . 9
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
158 | 157 | imbi2d 332 |
. . . . . . . 8
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
159 | | oveq2 6932 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · (𝑋‘𝑧))) |
160 | 159 | oveq2d 6940 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) |
161 | 160 | fveq2d 6452 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))))) |
162 | | fveq2 6448 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑧))) |
163 | 162 | oveq2d 6940 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) |
164 | 163 | oveq2d 6940 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) |
165 | 161, 164 | breq12d 4901 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋‘𝑧) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))))) |
166 | 165 | imbi2d 332 |
. . . . . . . 8
⊢ (𝑦 = (𝑋‘𝑧) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))))) |
167 | | oveq1 6931 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) = ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) |
168 | | oveq2 6932 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑆 / 𝐿) → (1 − 𝑡) = (1 − (𝑆 / 𝐿))) |
169 | 168 | oveq1d 6939 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝑋‘𝑧)) = ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) |
170 | 167, 169 | oveq12d 6942 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
171 | 170 | fveq2d 6452 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
172 | | oveq1 6931 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) = ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)))) |
173 | 168 | oveq1d 6939 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
174 | 172, 173 | oveq12d 6942 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
175 | 171, 174 | breq12d 4901 |
. . . . . . . . 9
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) ↔ (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
176 | 175 | imbi2d 332 |
. . . . . . . 8
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) ↔ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))))) |
177 | 46 | expcom 404 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1)) → (𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
178 | 158, 166,
176, 177 | vtocl3ga 3478 |
. . . . . . 7
⊢
((((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1)) → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
179 | 115, 39, 127, 178 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
180 | 179 | pm2.43i 52 |
. . . . 5
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
181 | 109 | oveq1d 6939 |
. . . . . . 7
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
182 | 135 | recnd 10407 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℂ) |
183 | 38, 182, 58, 67 | div23d 11190 |
. . . . . . 7
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
184 | 181, 183 | eqtr4d 2817 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) |
185 | 184 | oveq2d 6940 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
186 | 180, 185 | breqtrd 4914 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
187 | 183, 181 | eqtr4d 2817 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
188 | 187 | oveq2d 6940 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
189 | | jensenlem.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) |
190 | 52, 57, 60, 66 | divgt0d 11315 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝑆 / 𝐿)) |
191 | | lemul2 11232 |
. . . . . . . 8
⊢ (((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ ∧
((ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ ∧ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 < (𝑆 / 𝐿))) → ((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
192 | 133, 145,
116, 190, 191 | syl112anc 1442 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
193 | 189, 192 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆))) |
194 | 134, 146,
150, 193 | leadd1dd 10991 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
195 | 188, 194 | eqbrtrd 4910 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
196 | 132, 138,
151, 186, 195 | letrd 10535 |
. . 3
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
197 | 114 | fveq2d 6452 |
. . 3
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
198 | 144 | recnd 10407 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℂ) |
199 | 136 | recnd 10407 |
. . . . 5
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℂ) |
200 | 198, 199,
58, 67 | divdird 11191 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
201 | 17, 74 | sseldi 3819 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ ℝ) |
202 | 43 | ffvelrnda 6625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘𝑥) ∈ 𝐷) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
203 | 78, 202 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
204 | 201, 203 | remulcld 10409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℝ) |
205 | 204 | recnd 10407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
206 | 73, 205 | syldan 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
207 | 84 | fveq2d 6452 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐹‘(𝑋‘𝑥)) = (𝐹‘(𝑋‘𝑧))) |
208 | 83, 207 | oveq12d 6942 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) = ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) |
209 | 69, 70, 72, 9, 206, 36, 47, 199, 208 | gsumunsn 18749 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
210 | 43 | feqmptd 6511 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦))) |
211 | | fveq2 6448 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑥))) |
212 | 78, 88, 210, 211 | fmptco 6663 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋‘𝑥)))) |
213 | 5, 74, 203, 87, 212 | offval2 7193 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
214 | 213 | reseq1d 5643 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧}))) |
215 | 6 | resmptd 5704 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
216 | 214, 215 | eqtrd 2814 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
217 | 216 | oveq2d 6940 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
218 | 213 | reseq1d 5643 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵)) |
219 | 7 | resmptd 5704 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
220 | 218, 219 | eqtrd 2814 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
221 | 220 | oveq2d 6940 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
222 | 221 | oveq1d 6939 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
223 | 209, 217,
222 | 3eqtr4d 2824 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
224 | 223 | oveq1d 6939 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿)) |
225 | 198, 101,
58, 102, 67 | dmdcand 11182 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿)) |
226 | 225, 184 | oveq12d 6942 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
227 | 200, 224,
226 | 3eqtr4d 2824 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
228 | 196, 197,
227 | 3brtr4d 4920 |
. 2
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) |
229 | 131, 228 | jca 507 |
1
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿))) |