| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gsumesum.0 | . . 3
⊢
Ⅎ𝑘𝜑 | 
| 2 |  | nfcv 2904 | . . 3
⊢
Ⅎ𝑘𝐴 | 
| 3 |  | gsumesum.1 | . . 3
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 4 |  | gsumesum.2 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) | 
| 5 |  | eqidd 2737 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) | 
| 6 | 1, 2, 3, 4, 5 | esumval 34048 | . 2
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, <
)) | 
| 7 |  | xrltso 13184 | . . . 4
⊢  < Or
ℝ* | 
| 8 | 7 | a1i 11 | . . 3
⊢ (𝜑 → < Or
ℝ*) | 
| 9 |  | iccssxr 13471 | . . . 4
⊢
(0[,]+∞) ⊆ ℝ* | 
| 10 |  | xrge0base 33017 | . . . . 5
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) | 
| 11 |  | xrge0cmn 21427 | . . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd | 
| 12 | 11 | a1i 11 | . . . . 5
⊢ (𝜑 →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) | 
| 13 | 4 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐵 ∈ (0[,]+∞))) | 
| 14 | 1, 13 | ralrimi 3256 | . . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) | 
| 15 | 10, 12, 3, 14 | gsummptcl 19986 | . . . 4
⊢ (𝜑 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ (0[,]+∞)) | 
| 16 | 9, 15 | sselid 3980 | . . 3
⊢ (𝜑 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈
ℝ*) | 
| 17 |  | pwidg 4619 | . . . . . . 7
⊢ (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴) | 
| 18 | 3, 17 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐴) | 
| 19 | 18, 3 | elind 4199 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝒫 𝐴 ∩ Fin)) | 
| 20 |  | eqidd 2737 | . . . . 5
⊢ (𝜑 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 21 |  | mpteq1 5234 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑘 ∈ 𝑥 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)) | 
| 22 | 21 | oveq2d 7448 | . . . . . 6
⊢ (𝑥 = 𝐴 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 23 | 22 | rspceeqv 3644 | . . . . 5
⊢ ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) → ∃𝑥 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) | 
| 24 | 19, 20, 23 | syl2anc 584 | . . . 4
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) | 
| 25 |  | eqid 2736 | . . . . 5
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) | 
| 26 |  | ovex 7465 | . . . . 5
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈ V | 
| 27 | 25, 26 | elrnmpti 5972 | . . . 4
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) | 
| 28 | 24, 27 | sylibr 234 | . . 3
⊢ (𝜑 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) | 
| 29 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) | 
| 30 |  | mpteq1 5234 | . . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑘 ∈ 𝑥 ↦ 𝐵) = (𝑘 ∈ 𝑎 ↦ 𝐵)) | 
| 31 | 30 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑥 = 𝑎 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 32 | 31 | cbvmptv 5254 | . . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 33 |  | ovex 7465 | . . . . . . 7
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ V | 
| 34 | 32, 33 | elrnmpti 5972 | . . . . . 6
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 35 | 29, 34 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 36 | 11 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) | 
| 37 |  | inss2 4237 | . . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin | 
| 38 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) | 
| 39 | 37, 38 | sselid 3980 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ Fin) | 
| 40 |  | nfv 1913 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑎 ∈ (𝒫 𝐴 ∩ Fin) | 
| 41 | 1, 40 | nfan 1898 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) | 
| 42 |  | simpll 766 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝜑) | 
| 43 |  | inss1 4236 | . . . . . . . . . . . . . . . . . 18
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 | 
| 44 | 43 | sseli 3978 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴) | 
| 45 | 44 | elpwid 4608 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ⊆ 𝐴) | 
| 46 | 45 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑎 ⊆ 𝐴) | 
| 47 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ 𝑎) | 
| 48 | 46, 47 | sseldd 3983 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ 𝐴) | 
| 49 | 42, 48, 4 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝐵 ∈ (0[,]+∞)) | 
| 50 | 49 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘 ∈ 𝑎 → 𝐵 ∈ (0[,]+∞))) | 
| 51 | 41, 50 | ralrimi 3256 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘 ∈ 𝑎 𝐵 ∈ (0[,]+∞)) | 
| 52 | 10, 36, 39, 51 | gsummptcl 19986 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ (0[,]+∞)) | 
| 53 | 9, 52 | sselid 3980 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈
ℝ*) | 
| 54 |  | diffi 9216 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝑎) ∈ Fin) | 
| 55 | 3, 54 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∖ 𝑎) ∈ Fin) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐴 ∖ 𝑎) ∈ Fin) | 
| 57 |  | simpll 766 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴 ∖ 𝑎)) → 𝜑) | 
| 58 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴 ∖ 𝑎)) → 𝑘 ∈ (𝐴 ∖ 𝑎)) | 
| 59 | 58 | eldifad 3962 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴 ∖ 𝑎)) → 𝑘 ∈ 𝐴) | 
| 60 | 57, 59, 4 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴 ∖ 𝑎)) → 𝐵 ∈ (0[,]+∞)) | 
| 61 | 60 | ex 412 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘 ∈ (𝐴 ∖ 𝑎) → 𝐵 ∈ (0[,]+∞))) | 
| 62 | 41, 61 | ralrimi 3256 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘 ∈ (𝐴 ∖ 𝑎)𝐵 ∈ (0[,]+∞)) | 
| 63 | 10, 36, 56, 62 | gsummptcl 19986 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ (0[,]+∞)) | 
| 64 | 9, 63 | sselid 3980 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈
ℝ*) | 
| 65 |  | elxrge0 13498 | . . . . . . . . . . 11
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ (0[,]+∞) ↔
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ ℝ* ∧ 0 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 66 | 65 | simprbi 496 | . . . . . . . . . 10
⊢
(((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ (0[,]+∞) → 0 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵))) | 
| 67 | 63, 66 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵))) | 
| 68 |  | xraddge02 32761 | . . . . . . . . . 10
⊢
((((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ ℝ* ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ ℝ*) → (0
≤ ((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵))))) | 
| 69 | 68 | imp 406 | . . . . . . . . 9
⊢
(((((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ ℝ* ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) ∈ ℝ*) ∧ 0 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵))) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 70 | 53, 64, 67, 69 | syl21anc 837 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 71 | 70 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 72 |  | simpll 766 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝜑) | 
| 73 | 45 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ 𝐴) | 
| 74 |  | xrge00 33018 | . . . . . . . . . 10
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (0[,]+∞))) | 
| 75 |  | xrge0plusg 33019 | . . . . . . . . . 10
⊢ 
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) | 
| 76 | 11 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) | 
| 77 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → 𝐴 ∈ Fin) | 
| 78 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) | 
| 79 | 1, 4, 78 | fmptdf 7136 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) | 
| 80 | 79 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶(0[,]+∞)) | 
| 81 | 78 | fnmpt 6707 | . . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ (0[,]+∞) → (𝑘 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | 
| 82 | 14, 81 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) | 
| 83 |  | c0ex 11256 | . . . . . . . . . . . . 13
⊢ 0 ∈
V | 
| 84 | 83 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
V) | 
| 85 | 82, 3, 84 | fndmfifsupp 9419 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵) finSupp 0) | 
| 86 | 85 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑘 ∈ 𝐴 ↦ 𝐵) finSupp 0) | 
| 87 |  | disjdif 4471 | . . . . . . . . . . 11
⊢ (𝑎 ∩ (𝐴 ∖ 𝑎)) = ∅ | 
| 88 | 87 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → (𝑎 ∩ (𝐴 ∖ 𝑎)) = ∅) | 
| 89 |  | undif 4481 | . . . . . . . . . . . . 13
⊢ (𝑎 ⊆ 𝐴 ↔ (𝑎 ∪ (𝐴 ∖ 𝑎)) = 𝐴) | 
| 90 | 89 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑎 ⊆ 𝐴 → (𝑎 ∪ (𝐴 ∖ 𝑎)) = 𝐴) | 
| 91 | 90 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝑎 ⊆ 𝐴 → 𝐴 = (𝑎 ∪ (𝐴 ∖ 𝑎))) | 
| 92 | 91 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) → 𝐴 = (𝑎 ∪ (𝐴 ∖ 𝑎))) | 
| 93 | 10, 74, 75, 76, 77, 80, 86, 88, 92 | gsumsplit 19947 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑎)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎))))) | 
| 94 |  | resmpt 6054 | . . . . . . . . . . . 12
⊢ (𝑎 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑎) = (𝑘 ∈ 𝑎 ↦ 𝐵)) | 
| 95 | 94 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑎 ⊆ 𝐴 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑎)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 96 | 95 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑎)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) | 
| 97 |  | difss 4135 | . . . . . . . . . . . . 13
⊢ (𝐴 ∖ 𝑎) ⊆ 𝐴 | 
| 98 |  | resmpt 6054 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∖ 𝑎) ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎)) = (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) | 
| 99 | 97, 98 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎)) = (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵) | 
| 100 | 99 | oveq2i 7443 | . . . . . . . . . . 11
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎))) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)) | 
| 101 | 100 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎))) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵))) | 
| 102 | 96, 101 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ 𝑎)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg ((𝑘 ∈ 𝐴 ↦ 𝐵) ↾ (𝐴 ∖ 𝑎)))) =
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 103 | 93, 102 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ⊆ 𝐴) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 104 | 72, 73, 103 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) =
(((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) +𝑒
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ (𝐴 ∖ 𝑎) ↦ 𝐵)))) | 
| 105 | 71, 104 | breqtrrd 5170 | . . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 106 | 105 | ralrimiva 3145 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → ∀𝑎 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 107 |  | r19.29r 3115 | . . . . . 6
⊢
((∃𝑎 ∈
(𝒫 𝐴 ∩
Fin)𝑦 =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∧ ∀𝑎 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)))) | 
| 108 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑦 =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) → (𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ↔
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)))) | 
| 109 | 108 | biimpar 477 | . . . . . . 7
⊢ ((𝑦 =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) → 𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 110 | 109 | rexlimivw 3150 | . . . . . 6
⊢
(∃𝑎 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∧
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) → 𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 111 | 107, 110 | syl 17 | . . . . 5
⊢
((∃𝑎 ∈
(𝒫 𝐴 ∩
Fin)𝑦 =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∧ ∀𝑎 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) → 𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 112 | 35, 106, 111 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → 𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 113 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈
ℝ*) | 
| 114 | 11 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) | 
| 115 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) | 
| 116 | 37, 115 | sselid 3980 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) | 
| 117 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝐴 ∩ Fin) | 
| 118 | 1, 117 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) | 
| 119 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝜑) | 
| 120 | 43 | sseli 3978 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) | 
| 121 | 120 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) | 
| 122 | 121 | elpwid 4608 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ 𝐴) | 
| 123 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) | 
| 124 | 122, 123 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴) | 
| 125 | 119, 124,
4 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ (0[,]+∞)) | 
| 126 | 125 | ex 412 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘 ∈ 𝑥 → 𝐵 ∈ (0[,]+∞))) | 
| 127 | 118, 126 | ralrimi 3256 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘 ∈ 𝑥 𝐵 ∈ (0[,]+∞)) | 
| 128 | 10, 114, 116, 127 | gsummptcl 19986 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈ (0[,]+∞)) | 
| 129 | 9, 128 | sselid 3980 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈
ℝ*) | 
| 130 | 129 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈
ℝ*) | 
| 131 | 25 | rnmptss 7142 | . . . . . . 7
⊢
(∀𝑥 ∈
(𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ⊆
ℝ*) | 
| 132 | 130, 131 | syl 17 | . . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ⊆
ℝ*) | 
| 133 | 132 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → 𝑦 ∈ ℝ*) | 
| 134 |  | xrltnle 11329 | . . . . . 6
⊢
((((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) < 𝑦 ↔ ¬ 𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)))) | 
| 135 | 134 | con2bid 354 | . . . . 5
⊢
((((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ∈ ℝ* ∧ 𝑦 ∈ ℝ*)
→ (𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ↔ ¬
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) < 𝑦)) | 
| 136 | 113, 133,
135 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → (𝑦 ≤
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) ↔ ¬
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) < 𝑦)) | 
| 137 | 112, 136 | mpbid 232 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))) → ¬
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) < 𝑦) | 
| 138 | 8, 16, 28, 137 | supmax 9508 | . 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, < ) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵))) | 
| 139 | 6, 138 | eqtr2d 2777 | 1
⊢ (𝜑 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ*𝑘 ∈ 𝐴𝐵) |