Proof of Theorem jensenlem2
| Step | Hyp | Ref
| Expression |
| 1 | | cnfld0 21405 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
| 2 | | cnring 21403 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
| 3 | | ringabl 20278 |
. . . . . . . 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 4193 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| 8 | 5, 7 | ssfid 9301 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 9 | | resubdrg 21626 |
. . . . . . . . 9
⊢ (ℝ
∈ (SubRing‘ℂfld) ∧ ℝfld ∈
DivRing) |
| 10 | 9 | simpli 483 |
. . . . . . . 8
⊢ ℝ
∈ (SubRing‘ℂfld) |
| 11 | | subrgsubg 20577 |
. . . . . . . 8
⊢ (ℝ
∈ (SubRing‘ℂfld) → ℝ ∈
(SubGrp‘ℂfld)) |
| 12 | 10, 11 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈
(SubGrp‘ℂfld)) |
| 13 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
| 15 | | jensen.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) |
| 16 | | rge0ssre 13496 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
| 17 | | fss 6752 |
. . . . . . . . . 10
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → 𝑇:𝐴⟶ℝ) |
| 18 | 15, 16, 17 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:𝐴⟶ℝ) |
| 19 | | jensen.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:𝐴⟶𝐷) |
| 20 | | jensen.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
| 21 | 19, 20 | fssd 6753 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:𝐴⟶ℝ) |
| 22 | | inidm 4227 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 23 | 14, 18, 21, 5, 5, 22 | off 7715 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∘f · 𝑋):𝐴⟶ℝ) |
| 24 | 23, 7 | fssresd 6775 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐵):𝐵⟶ℝ) |
| 25 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
V) |
| 27 | 24, 8, 26 | fdmfifsupp 9415 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐵) finSupp 0) |
| 28 | 1, 4, 8, 12, 24, 27 | gsumsubgcl 19938 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) ∈ ℝ) |
| 29 | 28 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) ∈ ℂ) |
| 30 | | ax-resscn 11212 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
| 31 | 16, 30 | sstri 3993 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℂ |
| 32 | 6 | unssbd 4194 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧} ⊆ 𝐴) |
| 33 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
| 34 | 33 | snss 4785 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
| 35 | 32, 34 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → 𝑧 ∈ 𝐴) |
| 36 | 15, 35 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝑧) ∈ (0[,)+∞)) |
| 37 | 31, 36 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℂ) |
| 38 | 19, 35 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (𝜑 → (𝑋‘𝑧) ∈ 𝐷) |
| 39 | 20, 38 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℝ) |
| 40 | 39 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (𝑋‘𝑧) ∈ ℂ) |
| 41 | 37, 40 | mulcld 11281 |
. . . . 5
⊢ (𝜑 → ((𝑇‘𝑧) · (𝑋‘𝑧)) ∈ ℂ) |
| 42 | | jensen.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) |
| 43 | | jensen.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) |
| 44 | | jensen.7 |
. . . . . . . 8
⊢ (𝜑 → 0 <
(ℂfld Σg 𝑇)) |
| 45 | | jensen.8 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
| 46 | | jensenlem.1 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵) |
| 47 | | jensenlem.s |
. . . . . . . 8
⊢ 𝑆 = (ℂfld
Σg (𝑇 ↾ 𝐵)) |
| 48 | | jensenlem.l |
. . . . . . . 8
⊢ 𝐿 = (ℂfld
Σg (𝑇 ↾ (𝐵 ∪ {𝑧}))) |
| 49 | 20, 42, 43, 5, 15, 19, 44, 45, 46, 6, 47, 48 | jensenlem1 27030 |
. . . . . . 7
⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧))) |
| 50 | | jensenlem.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈
ℝ+) |
| 51 | 50 | rpred 13077 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 52 | | elrege0 13494 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) ↔ ((𝑇‘𝑧) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑧))) |
| 53 | 52 | simplbi 497 |
. . . . . . . . 9
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → (𝑇‘𝑧) ∈ ℝ) |
| 54 | 36, 53 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘𝑧) ∈ ℝ) |
| 55 | 51, 54 | readdcld 11290 |
. . . . . . 7
⊢ (𝜑 → (𝑆 + (𝑇‘𝑧)) ∈ ℝ) |
| 56 | 49, 55 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ ℝ) |
| 57 | 56 | recnd 11289 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ℂ) |
| 58 | | 0red 11264 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
| 59 | 50 | rpgt0d 13080 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑆) |
| 60 | 52 | simprbi 496 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑧) ∈ (0[,)+∞) → 0 ≤ (𝑇‘𝑧)) |
| 61 | 36, 60 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑇‘𝑧)) |
| 62 | 51, 54 | addge01d 11851 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (𝑇‘𝑧) ↔ 𝑆 ≤ (𝑆 + (𝑇‘𝑧)))) |
| 63 | 61, 62 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ≤ (𝑆 + (𝑇‘𝑧))) |
| 64 | 63, 49 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ 𝐿) |
| 65 | 58, 51, 56, 59, 64 | ltletrd 11421 |
. . . . . 6
⊢ (𝜑 → 0 < 𝐿) |
| 66 | 65 | gt0ne0d 11827 |
. . . . 5
⊢ (𝜑 → 𝐿 ≠ 0) |
| 67 | 29, 41, 57, 66 | divdird 12081 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
| 68 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 69 | | cnfldadd 21370 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
| 70 | | ringcmn 20279 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
| 71 | 2, 70 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ CMnd) |
| 72 | 7 | sselda 3983 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
| 73 | 15 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
| 74 | 72, 73 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
| 75 | 31, 74 | sselid 3981 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) ∈ ℂ) |
| 76 | 20 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ⊆ ℝ) |
| 77 | 19 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑋‘𝑥) ∈ 𝐷) |
| 78 | 72, 77 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ 𝐷) |
| 79 | 76, 78 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℝ) |
| 80 | 79 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℂ) |
| 81 | 75, 80 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝑋‘𝑥)) ∈ ℂ) |
| 82 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑇‘𝑥) = (𝑇‘𝑧)) |
| 83 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑋‘𝑥) = (𝑋‘𝑧)) |
| 84 | 82, 83 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝑋‘𝑥)) = ((𝑇‘𝑧) · (𝑋‘𝑧))) |
| 85 | 68, 69, 71, 8, 81, 35, 46, 41, 84 | gsumunsn 19978 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
| 86 | 15 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝑥 ∈ 𝐴 ↦ (𝑇‘𝑥))) |
| 87 | 19 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = (𝑥 ∈ 𝐴 ↦ (𝑋‘𝑥))) |
| 88 | 5, 73, 77, 86, 87 | offval2 7717 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘f · 𝑋) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
| 89 | 88 | reseq1d 5996 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧}))) |
| 90 | 6 | resmptd 6058 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
| 91 | 89, 90 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
| 92 | 91 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
| 93 | 88 | reseq1d 5996 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵)) |
| 94 | 7 | resmptd 6058 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
| 95 | 93, 94 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) |
| 96 | 95 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥))))) |
| 97 | 96 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝑋‘𝑥)))) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
| 98 | 85, 92, 97 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧)))) |
| 99 | 98 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝑋‘𝑧))) / 𝐿)) |
| 100 | 51 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 101 | 50 | rpne0d 13082 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ 0) |
| 102 | 29, 100, 57, 101, 66 | dmdcand 12072 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝐿)) |
| 103 | 57, 100, 57, 66 | divsubdird 12082 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝐿 / 𝐿) − (𝑆 / 𝐿))) |
| 104 | 100, 37, 49 | mvrladdd 11676 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 − 𝑆) = (𝑇‘𝑧)) |
| 105 | 104 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − 𝑆) / 𝐿) = ((𝑇‘𝑧) / 𝐿)) |
| 106 | 57, 66 | dividd 12041 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 / 𝐿) = 1) |
| 107 | 106 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 / 𝐿) − (𝑆 / 𝐿)) = (1 − (𝑆 / 𝐿))) |
| 108 | 103, 105,
107 | 3eqtr3rd 2786 |
. . . . . . 7
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) = ((𝑇‘𝑧) / 𝐿)) |
| 109 | 108 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
| 110 | 37, 40, 57, 66 | div23d 12080 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝑋‘𝑧))) |
| 111 | 109, 110 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)) = (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿)) |
| 112 | 102, 111 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) = (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝑋‘𝑧)) / 𝐿))) |
| 113 | 67, 99, 112 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
| 114 | | jensenlem.4 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷) |
| 115 | 51, 56, 66 | redivcld 12095 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ∈ ℝ) |
| 116 | 50 | rpge0d 13081 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑆) |
| 117 | | divge0 12137 |
. . . . . . 7
⊢ (((𝑆 ∈ ℝ ∧ 0 ≤
𝑆) ∧ (𝐿 ∈ ℝ ∧ 0 < 𝐿)) → 0 ≤ (𝑆 / 𝐿)) |
| 118 | 51, 116, 56, 65, 117 | syl22anc 839 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝑆 / 𝐿)) |
| 119 | 57 | mulridd 11278 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 · 1) = 𝐿) |
| 120 | 64, 119 | breqtrrd 5171 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ (𝐿 · 1)) |
| 121 | | 1red 11262 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
| 122 | | ledivmul 12144 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝐿 ∈
ℝ ∧ 0 < 𝐿))
→ ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
| 123 | 51, 121, 56, 65, 122 | syl112anc 1376 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 / 𝐿) ≤ 1 ↔ 𝑆 ≤ (𝐿 · 1))) |
| 124 | 120, 123 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑆 / 𝐿) ≤ 1) |
| 125 | | elicc01 13506 |
. . . . . 6
⊢ ((𝑆 / 𝐿) ∈ (0[,]1) ↔ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 ≤ (𝑆 / 𝐿) ∧ (𝑆 / 𝐿) ≤ 1)) |
| 126 | 115, 118,
124, 125 | syl3anbrc 1344 |
. . . . 5
⊢ (𝜑 → (𝑆 / 𝐿) ∈ (0[,]1)) |
| 127 | 114, 38, 126 | 3jca 1129 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) |
| 128 | 20, 43 | cvxcl 27028 |
. . . 4
⊢ ((𝜑 ∧ (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1))) → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
| 129 | 127, 128 | mpdan 687 |
. . 3
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) ∈ 𝐷) |
| 130 | 113, 129 | eqeltrd 2841 |
. 2
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷) |
| 131 | 42, 129 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ∈ ℝ) |
| 132 | 42, 114 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
| 133 | 115, 132 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) ∈ ℝ) |
| 134 | 42, 38 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℝ) |
| 135 | 54, 134 | remulcld 11291 |
. . . . . 6
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
| 136 | 135, 56, 66 | redivcld 12095 |
. . . . 5
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) ∈ ℝ) |
| 137 | 133, 136 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ∈ ℝ) |
| 138 | | fco 6760 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
| 139 | 42, 19, 138 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
| 140 | 14, 18, 139, 5, 5, 22 | off 7715 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℝ) |
| 141 | 140, 7 | fssresd 6775 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵):𝐵⟶ℝ) |
| 142 | 141, 8, 26 | fdmfifsupp 9415 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵) finSupp 0) |
| 143 | 1, 4, 8, 12, 141, 142 | gsumsubgcl 19938 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℝ) |
| 144 | 143, 51, 101 | redivcld 12095 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ) |
| 145 | 115, 144 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) ∈ ℝ) |
| 146 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 147 | | resubcl 11573 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ (𝑆 /
𝐿) ∈ ℝ) →
(1 − (𝑆 / 𝐿)) ∈
ℝ) |
| 148 | 146, 115,
147 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (1 − (𝑆 / 𝐿)) ∈ ℝ) |
| 149 | 148, 134 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) ∈ ℝ) |
| 150 | 145, 149 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ∈ ℝ) |
| 151 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · 𝑥) = (𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) |
| 152 | 151 | fvoveq1d 7453 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)))) |
| 153 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → (𝐹‘𝑥) = (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) |
| 154 | 153 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → (𝑡 · (𝐹‘𝑥)) = (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)))) |
| 155 | 154 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
| 156 | 152, 155 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
| 157 | 156 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑥 = ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) → ((𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))))) |
| 158 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · (𝑋‘𝑧))) |
| 159 | 158 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) |
| 160 | 159 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) = (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))))) |
| 161 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋‘𝑧) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑧))) |
| 162 | 161 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑧) → ((1 − 𝑡) · (𝐹‘𝑦)) = ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) |
| 163 | 162 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋‘𝑧) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) = ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) |
| 164 | 160, 163 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋‘𝑧) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦))) ↔ (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))))) |
| 165 | 164 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑦 = (𝑋‘𝑧) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘𝑦)))) ↔ (𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))))) |
| 166 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) = ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) |
| 167 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (𝑆 / 𝐿) → (1 − 𝑡) = (1 − (𝑆 / 𝐿))) |
| 168 | 167 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝑋‘𝑧)) = ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))) |
| 169 | 166, 168 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧))) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) |
| 170 | 169 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
| 171 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → (𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) = ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)))) |
| 172 | 167 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑆 / 𝐿) → ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
| 173 | 171, 172 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 174 | 170, 173 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧)))) ↔ (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
| 175 | 174 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑡 = (𝑆 / 𝐿) → ((𝜑 → (𝐹‘((𝑡 · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − 𝑡) · (𝑋‘𝑧)))) ≤ ((𝑡 · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − 𝑡) · (𝐹‘(𝑋‘𝑧))))) ↔ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))))) |
| 176 | 45 | expcom 413 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1)) → (𝜑 → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))) |
| 177 | 157, 165,
175, 176 | vtocl3ga 3583 |
. . . . . . 7
⊢
((((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷 ∧ (𝑋‘𝑧) ∈ 𝐷 ∧ (𝑆 / 𝐿) ∈ (0[,]1)) → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
| 178 | 114, 38, 126, 177 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))))) |
| 179 | 178 | pm2.43i 52 |
. . . . 5
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 180 | 108 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
| 181 | 134 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑋‘𝑧)) ∈ ℂ) |
| 182 | 37, 181, 57, 66 | div23d 12080 |
. . . . . . 7
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = (((𝑇‘𝑧) / 𝐿) · (𝐹‘(𝑋‘𝑧)))) |
| 183 | 180, 182 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))) = (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) |
| 184 | 183 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
| 185 | 179, 184 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
| 186 | 182, 180 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿) = ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) |
| 187 | 186 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) = (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 188 | | jensenlem.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) |
| 189 | 51, 56, 59, 65 | divgt0d 12203 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝑆 / 𝐿)) |
| 190 | | lemul2 12120 |
. . . . . . . 8
⊢ (((𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ∈ ℝ ∧
((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ∈ ℝ ∧ ((𝑆 / 𝐿) ∈ ℝ ∧ 0 < (𝑆 / 𝐿))) → ((𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
| 191 | 132, 144,
115, 189, 190 | syl112anc 1376 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆) ↔ ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)))) |
| 192 | 188, 191 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) ≤ ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆))) |
| 193 | 133, 145,
149, 192 | leadd1dd 11877 |
. . . . 5
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 194 | 187, 193 | eqbrtrd 5165 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆))) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿)) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 195 | 131, 137,
150, 185, 194 | letrd 11418 |
. . 3
⊢ (𝜑 → (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧)))) ≤ (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 196 | 113 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) = (𝐹‘(((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝑋‘𝑧))))) |
| 197 | 143 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) ∈ ℂ) |
| 198 | 135 | recnd 11289 |
. . . . 5
⊢ (𝜑 → ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) ∈ ℂ) |
| 199 | 197, 198,
57, 66 | divdird 12081 |
. . . 4
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
| 200 | 16, 73 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ ℝ) |
| 201 | 42 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑋‘𝑥) ∈ 𝐷) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
| 202 | 77, 201 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑋‘𝑥)) ∈ ℝ) |
| 203 | 200, 202 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℝ) |
| 204 | 203 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
| 205 | 72, 204 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) ∈ ℂ) |
| 206 | 83 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝐹‘(𝑋‘𝑥)) = (𝐹‘(𝑋‘𝑧))) |
| 207 | 82, 206 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))) = ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) |
| 208 | 68, 69, 71, 8, 205, 35, 46, 198, 207 | gsumunsn 19978 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
| 209 | 42 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦))) |
| 210 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋‘𝑥) → (𝐹‘𝑦) = (𝐹‘(𝑋‘𝑥))) |
| 211 | 77, 87, 209, 210 | fmptco 7149 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 ∘ 𝑋) = (𝑥 ∈ 𝐴 ↦ (𝐹‘(𝑋‘𝑥)))) |
| 212 | 5, 73, 202, 86, 211 | offval2 7717 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)) = (𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
| 213 | 212 | reseq1d 5996 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧}))) |
| 214 | 6 | resmptd 6058 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
| 215 | 213, 214 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧})) = (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
| 216 | 215 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = (ℂfld
Σg (𝑥 ∈ (𝐵 ∪ {𝑧}) ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
| 217 | 212 | reseq1d 5996 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵) = ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵)) |
| 218 | 7 | resmptd 6058 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
| 219 | 217, 218 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) |
| 220 | 219 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) = (ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥)))))) |
| 221 | 220 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) = ((ℂfld
Σg (𝑥 ∈ 𝐵 ↦ ((𝑇‘𝑥) · (𝐹‘(𝑋‘𝑥))))) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
| 222 | 208, 216,
221 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) = ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))))) |
| 223 | 222 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) + ((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧)))) / 𝐿)) |
| 224 | 197, 100,
57, 101, 66 | dmdcand 12072 |
. . . . 5
⊢ (𝜑 → ((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) = ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿)) |
| 225 | 224, 183 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧)))) = (((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝐿) + (((𝑇‘𝑧) · (𝐹‘(𝑋‘𝑧))) / 𝐿))) |
| 226 | 199, 223,
225 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) = (((𝑆 / 𝐿) · ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆)) + ((1 − (𝑆 / 𝐿)) · (𝐹‘(𝑋‘𝑧))))) |
| 227 | 195, 196,
226 | 3brtr4d 5175 |
. 2
⊢ (𝜑 → (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) |
| 228 | 130, 227 | jca 511 |
1
⊢ (𝜑 → (((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld
Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿))) |