| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
| 2 | | sge0xaddlem1.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | | sge0xaddlem1.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) |
| 4 | 1, 2, 3 | sge0revalmpt 46393 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) = sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, <
)) |
| 5 | | sge0xaddlem1.c |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,)+∞)) |
| 6 | 1, 2, 5 | sge0revalmpt 46393 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) = sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, <
)) |
| 7 | 4, 6 | oveq12d 7449 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) = (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran
(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, <
))) |
| 8 | 4 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) =
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵))) |
| 9 | | sge0xaddlem1.sb |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ) |
| 10 | 8, 9 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) ∈
ℝ) |
| 11 | | sge0xaddlem1.sc |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) ∈ ℝ) |
| 12 | 6, 11 | eqeltrrd 2842 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < ) ∈
ℝ) |
| 13 | 10, 12 | readdcld 11290 |
. . . 4
⊢ (𝜑 → (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran
(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < )) ∈
ℝ) |
| 14 | 13 | rexrd 11311 |
. . 3
⊢ (𝜑 → (sup(ran (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑦 𝐵), ℝ*, < ) + sup(ran
(𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑧 𝐶), ℝ*, < )) ∈
ℝ*) |
| 15 | 7, 14 | eqeltrd 2841 |
. 2
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ∈
ℝ*) |
| 16 | | elinel2 4202 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
| 17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
| 18 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝜑) |
| 19 | | elpwinss 45054 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
| 21 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
| 22 | 20, 21 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴) |
| 23 | 22 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴) |
| 24 | | rge0ssre 13496 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ |
| 25 | 24, 3 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
| 26 | 18, 23, 25 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ ℝ) |
| 27 | 24, 5 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ) |
| 28 | 18, 23, 27 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐶 ∈ ℝ) |
| 29 | 26, 28 | readdcld 11290 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → (𝐵 + 𝐶) ∈ ℝ) |
| 30 | 17, 29 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ) |
| 31 | 30 | rexrd 11311 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈
ℝ*) |
| 32 | 31 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈
ℝ*) |
| 33 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) |
| 34 | 33 | rnmptss 7143 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝐴 ∩
Fin)Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆
ℝ*) |
| 35 | 32, 34 | syl 17 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆
ℝ*) |
| 36 | | supxrcl 13357 |
. . . 4
⊢ (ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ* →
sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ*) |
| 37 | 35, 36 | syl 17 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ*) |
| 38 | | sge0xaddlem1.rp |
. . . 4
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 39 | 38 | rpxrd 13078 |
. . 3
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
| 40 | 37, 39 | xaddcld 13343 |
. 2
⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)
∈ ℝ*) |
| 41 | | sge0xaddlem1.ufi |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ Fin) |
| 42 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝜑) |
| 43 | | sge0xaddlem1.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ 𝐴) |
| 44 | 43 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝑘 ∈ 𝐴) |
| 45 | 42, 44, 3 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐵 ∈ (0[,)+∞)) |
| 46 | 24, 45 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑈) → 𝐵 ∈ ℝ) |
| 47 | 41, 46 | fsumrecl 15770 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ∈ ℝ) |
| 48 | 38 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 49 | 48 | rehalfcld 12513 |
. . . . . 6
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) |
| 50 | 47, 49 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) ∈ ℝ) |
| 51 | | sge0xaddlem1.wfi |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) |
| 52 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (0[,)+∞) ⊆
ℝ) |
| 53 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝜑) |
| 54 | | sge0xaddlem1.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ⊆ 𝐴) |
| 55 | 54 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑊 ⊆ 𝐴) |
| 56 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊) |
| 57 | 55, 56 | sseldd 3984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝐴) |
| 58 | 53, 57, 5 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐶 ∈ (0[,)+∞)) |
| 59 | 52, 58 | sseldd 3984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐶 ∈ ℝ) |
| 60 | 51, 59 | fsumrecl 15770 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ∈ ℝ) |
| 61 | 60, 49 | readdcld 11290 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2)) ∈ ℝ) |
| 62 | 50, 61 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ∈ ℝ) |
| 63 | 62 | rexrd 11311 |
. . 3
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ∈
ℝ*) |
| 64 | | sge0xaddlem1.ltb |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) < (Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2))) |
| 65 | | sge0xaddlem1.ltc |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶)) < (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) |
| 66 | 9, 11, 50, 61, 64, 65 | ltadd12dd 45354 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) < ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2)))) |
| 67 | 47 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ∈ ℂ) |
| 68 | 49 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (𝐸 / 2) ∈ ℂ) |
| 69 | 60 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ∈ ℂ) |
| 70 | 67, 68, 69, 68 | add4d 11490 |
. . . . 5
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + ((𝐸 / 2) + (𝐸 / 2)))) |
| 71 | 48 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 72 | 71 | 2halvesd 12512 |
. . . . . 6
⊢ (𝜑 → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
| 73 | 72 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + ((𝐸 / 2) + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸)) |
| 74 | 70, 73 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) = ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸)) |
| 75 | 74, 63 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈
ℝ*) |
| 76 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 77 | 76 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 78 | 74, 62 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈ ℝ) |
| 79 | | ltpnf 13162 |
. . . . . . . . 9
⊢
(((Σ𝑘 ∈
𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ∈ ℝ → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) < +∞) |
| 80 | 78, 79 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) < +∞) |
| 81 | 75, 77, 80 | xrltled 13192 |
. . . . . . 7
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ +∞) |
| 82 | 81 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ ((Σ𝑘 ∈
𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ +∞) |
| 83 | | oveq1 7438 |
. . . . . . . 8
⊢ (sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞
→ (sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸) =
(+∞ +𝑒 𝐸)) |
| 84 | 83 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ (sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸) =
(+∞ +𝑒 𝐸)) |
| 85 | 48 | renemnfd 11313 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ≠ -∞) |
| 86 | | xaddpnf2 13269 |
. . . . . . . . 9
⊢ ((𝐸 ∈ ℝ*
∧ 𝐸 ≠ -∞)
→ (+∞ +𝑒 𝐸) = +∞) |
| 87 | 39, 85, 86 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (+∞
+𝑒 𝐸) =
+∞) |
| 88 | 87 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ (+∞ +𝑒 𝐸) = +∞) |
| 89 | 84, 88 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ +∞ = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 90 | 82, 89 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ ((Σ𝑘 ∈
𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 91 | | simpl 482 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ 𝜑) |
| 92 | | sge0xaddlem1.xr |
. . . . . . . 8
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
(0[,]+∞)) |
| 93 | 91, 92 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
(0[,]+∞)) |
| 94 | | neqne 2948 |
. . . . . . . 8
⊢ (¬
sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞
→ sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠
+∞) |
| 95 | 94 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠
+∞) |
| 96 | | ge0xrre 45544 |
. . . . . . 7
⊢ ((sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
(0[,]+∞) ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ≠
+∞) → sup(ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) |
| 97 | 93, 95, 96 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) |
| 98 | 47, 60 | readdcld 11290 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ∈ ℝ) |
| 99 | 98 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → (Σ𝑘
∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ∈ ℝ) |
| 100 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → sup(ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) |
| 101 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → 𝐸 ∈
ℝ) |
| 102 | 41, 51 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∈ Fin ∧ 𝑊 ∈ Fin)) |
| 103 | | unfi 9211 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ Fin ∧ 𝑊 ∈ Fin) → (𝑈 ∪ 𝑊) ∈ Fin) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ Fin) |
| 105 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝜑) |
| 106 | 43, 54 | unssd 4192 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 ∪ 𝑊) ⊆ 𝐴) |
| 107 | 106 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → (𝑈 ∪ 𝑊) ⊆ 𝐴) |
| 108 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝑘 ∈ (𝑈 ∪ 𝑊)) |
| 109 | 107, 108 | sseldd 3984 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝑘 ∈ 𝐴) |
| 110 | 105, 109,
25 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐵 ∈ ℝ) |
| 111 | 109, 27 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐶 ∈ ℝ) |
| 112 | 110, 111 | readdcld 11290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → (𝐵 + 𝐶) ∈ ℝ) |
| 113 | 104, 112 | fsumrecl 15770 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ℝ) |
| 114 | 113 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → Σ𝑘
∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ℝ) |
| 115 | 104, 110 | fsumrecl 15770 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 ∈ ℝ) |
| 116 | 104, 111 | fsumrecl 15770 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶 ∈ ℝ) |
| 117 | | icossicc 13476 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 118 | 117, 3 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
| 119 | | xrge0ge0 45358 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (0[,]+∞) → 0
≤ 𝐵) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐵) |
| 121 | 109, 120 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 0 ≤ 𝐵) |
| 122 | | ssun1 4178 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ⊆ (𝑈 ∪ 𝑊) |
| 123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ⊆ (𝑈 ∪ 𝑊)) |
| 124 | 104, 110,
121, 123 | fsumless 15832 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ 𝑈 𝐵 ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵) |
| 125 | 117, 5 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (0[,]+∞)) |
| 126 | | xrge0ge0 45358 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ (0[,]+∞) → 0
≤ 𝐶) |
| 127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ≤ 𝐶) |
| 128 | 109, 127 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 0 ≤ 𝐶) |
| 129 | | ssun2 4179 |
. . . . . . . . . . . . . 14
⊢ 𝑊 ⊆ (𝑈 ∪ 𝑊) |
| 130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ⊆ (𝑈 ∪ 𝑊)) |
| 131 | 104, 111,
128, 130 | fsumless 15832 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ 𝑊 𝐶 ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶) |
| 132 | 47, 60, 115, 116, 124, 131 | leadd12dd 45328 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶)) |
| 133 | 110 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐵 ∈ ℂ) |
| 134 | 111 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑈 ∪ 𝑊)) → 𝐶 ∈ ℂ) |
| 135 | 104, 133,
134 | fsumadd 15776 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) = (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶)) |
| 136 | 135 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐵 + Σ𝑘 ∈ (𝑈 ∪ 𝑊)𝐶) = Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶)) |
| 137 | 132, 136 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶)) |
| 138 | 137 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → (Σ𝑘
∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶)) |
| 139 | 35 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)) ⊆
ℝ*) |
| 140 | 104, 106 | elpwd 4606 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ 𝒫 𝐴) |
| 141 | 140, 104 | elind 4200 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ∪ 𝑊) ∈ (𝒫 𝐴 ∩ Fin)) |
| 142 | 113 | elexd 3504 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ V) |
| 143 | | sumeq1 15725 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑈 ∪ 𝑊) → Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶) = Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶)) |
| 144 | 33, 143 | elrnmpt1s 5970 |
. . . . . . . . . . . 12
⊢ (((𝑈 ∪ 𝑊) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ V) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))) |
| 145 | 141, 142,
144 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))) |
| 146 | 145 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → Σ𝑘
∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))) |
| 147 | | supxrub 13366 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)) ⊆ ℝ* ∧
Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶))) → Σ𝑘 ∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, <
)) |
| 148 | 139, 146,
147 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → Σ𝑘
∈ (𝑈 ∪ 𝑊)(𝐵 + 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, <
)) |
| 149 | 99, 114, 100, 138, 148 | letrd 11418 |
. . . . . . . 8
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → (Σ𝑘
∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) ≤ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, <
)) |
| 150 | 99, 100, 101, 149 | leadd1dd 11877 |
. . . . . . 7
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → ((Σ𝑘
∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸)) |
| 151 | | rexadd 13274 |
. . . . . . . . 9
⊢ ((sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ ∧ 𝐸 ∈
ℝ) → (sup(ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸) =
(sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸)) |
| 152 | 100, 101,
151 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → (sup(ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸) =
(sup(ran (𝑥 ∈
(𝒫 𝐴 ∩ Fin)
↦ Σ𝑘 ∈
𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸)) |
| 153 | 152 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → (sup(ran (𝑥
∈ (𝒫 𝐴 ∩
Fin) ↦ Σ𝑘
∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) + 𝐸) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 154 | 150, 153 | breqtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) ∈
ℝ) → ((Σ𝑘
∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 155 | 91, 97, 154 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ ¬ sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < ) = +∞)
→ ((Σ𝑘 ∈
𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 156 | 90, 155 | pm2.61dan 813 |
. . . 4
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + Σ𝑘 ∈ 𝑊 𝐶) + 𝐸) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 157 | 74, 156 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → ((Σ𝑘 ∈ 𝑈 𝐵 + (𝐸 / 2)) + (Σ𝑘 ∈ 𝑊 𝐶 + (𝐸 / 2))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 158 | 15, 63, 40, 66, 157 | xrltletrd 13203 |
. 2
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) < (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |
| 159 | 15, 40, 158 | xrltled 13192 |
1
⊢ (𝜑 →
((Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐵)) +
(Σ^‘(𝑘 ∈ 𝐴 ↦ 𝐶))) ≤ (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 (𝐵 + 𝐶)), ℝ*, < )
+𝑒 𝐸)) |