| Step | Hyp | Ref
| Expression |
| 1 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
| 2 | | xrge0gsumle.g |
. . . . . . . . . 10
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 3 | | xrsbas 21396 |
. . . . . . . . . 10
⊢
ℝ* =
(Base‘ℝ*𝑠) |
| 4 | 2, 3 | ressbas2 17283 |
. . . . . . . . 9
⊢
((0[,]+∞) ⊆ ℝ* → (0[,]+∞) =
(Base‘𝐺)) |
| 5 | 1, 4 | ax-mp 5 |
. . . . . . . 8
⊢
(0[,]+∞) = (Base‘𝐺) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) |
| 7 | 6 | xrge0subm 21425 |
. . . . . . . . 9
⊢
(0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) |
| 8 | | xrex 13029 |
. . . . . . . . . . . . 13
⊢
ℝ* ∈ V |
| 9 | 8 | difexi 5330 |
. . . . . . . . . . . 12
⊢
(ℝ* ∖ {-∞}) ∈ V |
| 10 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
ℝ*) |
| 11 | | ge0nemnf 13215 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ≠
-∞) |
| 12 | 10, 11 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
(𝑥 ∈
ℝ* ∧ 𝑥
≠ -∞)) |
| 13 | | elxrge0 13497 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
| 14 | | eldifsn 4786 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (ℝ*
∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠
-∞)) |
| 15 | 12, 13, 14 | 3imtr4i 292 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) |
| 16 | 15 | ssriv 3987 |
. . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
| 17 | | ressabs 17294 |
. . . . . . . . . . . 12
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) |
| 18 | 9, 16, 17 | mp2an 692 |
. . . . . . . . . . 11
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 19 | 2, 18 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) |
| 20 | 6 | xrs10 21423 |
. . . . . . . . . 10
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) |
| 21 | 19, 20 | subm0 18828 |
. . . . . . . . 9
⊢
((0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) → 0 =
(0g‘𝐺)) |
| 22 | 7, 21 | ax-mp 5 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
| 23 | | xrge0cmn 21426 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
| 24 | 2, 23 | eqeltri 2837 |
. . . . . . . . 9
⊢ 𝐺 ∈ CMnd |
| 25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
| 26 | | elfpw 9394 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin)) |
| 27 | 26 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin) |
| 28 | 27 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin) |
| 29 | | xrge0gsumle.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) |
| 30 | 26 | simplbi 497 |
. . . . . . . . 9
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴) |
| 31 | | fssres 6774 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
| 32 | 29, 30, 31 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
| 33 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
V) |
| 35 | 32, 28, 34 | fdmfifsupp 9415 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0) |
| 36 | 5, 22, 25, 28, 32, 35 | gsumcl 19933 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞)) |
| 37 | 1, 36 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈
ℝ*) |
| 38 | 37 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
| 39 | 38 | frnd 6744 |
. . . 4
⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
| 40 | | 0ss 4400 |
. . . . . . 7
⊢ ∅
⊆ 𝐴 |
| 41 | | 0fi 9082 |
. . . . . . 7
⊢ ∅
∈ Fin |
| 42 | | elfpw 9394 |
. . . . . . 7
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
| 43 | 40, 41, 42 | mpbir2an 711 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
| 44 | | 0cn 11253 |
. . . . . 6
⊢ 0 ∈
ℂ |
| 45 | | eqid 2737 |
. . . . . . 7
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) |
| 46 | | reseq2 5992 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅)) |
| 47 | | res0 6001 |
. . . . . . . . . 10
⊢ (𝐹 ↾ ∅) =
∅ |
| 48 | 46, 47 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = (𝐺 Σg
∅)) |
| 50 | 22 | gsum0 18697 |
. . . . . . . 8
⊢ (𝐺 Σg
∅) = 0 |
| 51 | 49, 50 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = 0) |
| 52 | 45, 51 | elrnmpt1s 5970 |
. . . . . 6
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
| 53 | 43, 44, 52 | mp2an 692 |
. . . . 5
⊢ 0 ∈
ran (𝑠 ∈ (𝒫
𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) |
| 54 | 53 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))) |
| 55 | 39, 54 | sseldd 3984 |
. . 3
⊢ (𝜑 → 0 ∈
ℝ*) |
| 56 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 57 | | xrge0gsumle.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝒫 𝐴 ∩ Fin)) |
| 58 | 57 | elin2d 4205 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 59 | | diffi 9215 |
. . . . . 6
⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐶) ∈ Fin) |
| 60 | 58, 59 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝐶) ∈ Fin) |
| 61 | | elfpw 9394 |
. . . . . . . . 9
⊢ (𝐵 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin)) |
| 62 | 61 | simplbi 497 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝒫 𝐴 ∩ Fin) → 𝐵 ⊆ 𝐴) |
| 63 | 57, 62 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| 64 | 63 | ssdifssd 4147 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝐶) ⊆ 𝐴) |
| 65 | 29, 64 | fssresd 6775 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐵 ∖ 𝐶)):(𝐵 ∖ 𝐶)⟶(0[,]+∞)) |
| 66 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
V) |
| 67 | 65, 60, 66 | fdmfifsupp 9415 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐵 ∖ 𝐶)) finSupp 0) |
| 68 | 5, 22, 56, 60, 65, 67 | gsumcl 19933 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞)) |
| 69 | 1, 68 | sselid 3981 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈
ℝ*) |
| 70 | | xrge0gsumle.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ⊆ 𝐵) |
| 71 | 58, 70 | ssfid 9301 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Fin) |
| 72 | 70, 63 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
| 73 | 29, 72 | fssresd 6775 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶(0[,]+∞)) |
| 74 | 73, 71, 66 | fdmfifsupp 9415 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐶) finSupp 0) |
| 75 | 5, 22, 56, 71, 73, 74 | gsumcl 19933 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ∈ (0[,]+∞)) |
| 76 | 1, 75 | sselid 3981 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ∈
ℝ*) |
| 77 | | elxrge0 13497 |
. . . . 5
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞) ↔ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ ℝ* ∧ 0 ≤
(𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶))))) |
| 78 | 77 | simprbi 496 |
. . . 4
⊢ ((𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ (0[,]+∞) → 0 ≤
(𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
| 79 | 68, 78 | syl 17 |
. . 3
⊢ (𝜑 → 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
| 80 | | xleadd2a 13296 |
. . 3
⊢ (((0
∈ ℝ* ∧ (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))) ∈ ℝ* ∧ (𝐺 Σg
(𝐹 ↾ 𝐶)) ∈ ℝ*)
∧ 0 ≤ (𝐺
Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) ≤ ((𝐺 Σg
(𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))))) |
| 81 | 55, 69, 76, 79, 80 | syl31anc 1375 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) ≤ ((𝐺 Σg
(𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg
(𝐹 ↾ (𝐵 ∖ 𝐶))))) |
| 82 | 76 | xaddridd 13285 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 0) = (𝐺 Σg
(𝐹 ↾ 𝐶))) |
| 83 | | ovex 7464 |
. . . . 5
⊢
(0[,]+∞) ∈ V |
| 84 | | xrsadd 21397 |
. . . . . 6
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
| 85 | 2, 84 | ressplusg 17334 |
. . . . 5
⊢
((0[,]+∞) ∈ V → +𝑒 =
(+g‘𝐺)) |
| 86 | 83, 85 | ax-mp 5 |
. . . 4
⊢
+𝑒 = (+g‘𝐺) |
| 87 | 29, 63 | fssresd 6775 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
| 88 | 87, 58, 66 | fdmfifsupp 9415 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐵) finSupp 0) |
| 89 | | disjdif 4472 |
. . . . 5
⊢ (𝐶 ∩ (𝐵 ∖ 𝐶)) = ∅ |
| 90 | 89 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐶 ∩ (𝐵 ∖ 𝐶)) = ∅) |
| 91 | | undif2 4477 |
. . . . 5
⊢ (𝐶 ∪ (𝐵 ∖ 𝐶)) = (𝐶 ∪ 𝐵) |
| 92 | | ssequn1 4186 |
. . . . . 6
⊢ (𝐶 ⊆ 𝐵 ↔ (𝐶 ∪ 𝐵) = 𝐵) |
| 93 | 70, 92 | sylib 218 |
. . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐵) = 𝐵) |
| 94 | 91, 93 | eqtr2id 2790 |
. . . 4
⊢ (𝜑 → 𝐵 = (𝐶 ∪ (𝐵 ∖ 𝐶))) |
| 95 | 5, 22, 86, 56, 57, 87, 88, 90, 94 | gsumsplit 19946 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐵)) = ((𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶))))) |
| 96 | 70 | resabs1d 6026 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ↾ 𝐶) = (𝐹 ↾ 𝐶)) |
| 97 | 96 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) = (𝐺 Σg (𝐹 ↾ 𝐶))) |
| 98 | | difss 4136 |
. . . . . 6
⊢ (𝐵 ∖ 𝐶) ⊆ 𝐵 |
| 99 | | resabs1 6024 |
. . . . . 6
⊢ ((𝐵 ∖ 𝐶) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)) = (𝐹 ↾ (𝐵 ∖ 𝐶))) |
| 100 | 98, 99 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)) = (𝐹 ↾ (𝐵 ∖ 𝐶))) |
| 101 | 100 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶))) = (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) |
| 102 | 97, 101 | oveq12d 7449 |
. . 3
⊢ (𝜑 → ((𝐺 Σg ((𝐹 ↾ 𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹 ↾ 𝐵) ↾ (𝐵 ∖ 𝐶)))) = ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶))))) |
| 103 | 95, 102 | eqtr2d 2778 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵 ∖ 𝐶)))) = (𝐺 Σg (𝐹 ↾ 𝐵))) |
| 104 | 81, 82, 103 | 3brtr3d 5174 |
1
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ≤ (𝐺 Σg (𝐹 ↾ 𝐵))) |