| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 3 | | xrltso 13183 |
. . . . . 6
⊢ < Or
ℝ* |
| 4 | 3 | supex 9503 |
. . . . 5
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V |
| 5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V) |
| 6 | | elsng 4640 |
. . . 4
⊢ (sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V → (sup(ran (𝑥
∈ (𝒫 𝑋 ∩
Fin) ↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, < ) ∈
{sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, < )} ↔
sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, <
))) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ {sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, < )} ↔
sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, <
))) |
| 8 | 2, 7 | mpbird 257 |
. 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ {sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
| 9 | | sge0tsms.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) |
| 11 | | sge0tsms.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
| 13 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
| 14 | 10, 12, 13 | sge0pnfval 46388 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
| 15 | 11 | ffnd 6737 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑋) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹 Fn 𝑋) |
| 17 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
| 18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
| 19 | 13, 18 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
| 20 | | iccssxr 13470 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ ℝ* |
| 21 | | sge0tsms.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
| 23 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
| 24 | | elinel1 4201 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
| 25 | | elpwi 4607 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
| 28 | | fssres 6774 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
| 29 | 23, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
| 30 | | elinel2 4202 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
| 32 | | 0red 11264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
ℝ) |
| 33 | 29, 31, 32 | fdmfifsupp 9415 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) finSupp 0) |
| 34 | 21, 22, 29, 33 | gsumge0cl 46386 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈ (0[,]+∞)) |
| 35 | 20, 34 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 36 | 35 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
| 38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) |
| 39 | 38 | rnmptss 7143 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
| 40 | 37, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ⊆
ℝ*) |
| 41 | | snelpwi 5448 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
| 42 | | snfi 9083 |
. . . . . . . . . . . . . . 15
⊢ {𝑦} ∈ Fin |
| 43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
| 44 | 41, 43 | elind 4200 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
| 45 | 44 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
| 46 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
| 47 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → {𝑦} ⊆ 𝑋) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → {𝑦} ⊆ 𝑋) |
| 49 | 46, 48 | fssresd 6775 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
| 50 | 49 | feqmptd 6977 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥))) |
| 51 | | fvres 6925 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑥) = (𝐹‘𝑥)) |
| 52 | 51 | mpteq2ia 5245 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)) |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
| 54 | 50, 53 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
| 55 | 54 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
| 56 | 55 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
| 57 | | xrge0cmn 21426 |
. . . . . . . . . . . . . . . . 17
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
| 58 | 21, 57 | eqeltri 2837 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ∈ CMnd |
| 59 | | cmnmnd 19815 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
| 60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ Mnd |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐺 ∈ Mnd) |
| 62 | | simp2 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
| 63 | 11 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
| 64 | 63 | 3adant3 1133 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
| 65 | | dfss2 3969 |
. . . . . . . . . . . . . . . . . 18
⊢
((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩
ℝ*) = (0[,]+∞)) |
| 66 | 20, 65 | mpbi 230 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∩ ℝ*) =
(0[,]+∞) |
| 67 | 66 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢
(0[,]+∞) = ((0[,]+∞) ∩
ℝ*) |
| 68 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ∈ V |
| 69 | | xrsbas 21396 |
. . . . . . . . . . . . . . . . . 18
⊢
ℝ* =
(Base‘ℝ*𝑠) |
| 70 | 21, 69 | ressbas 17280 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∈ V → ((0[,]+∞) ∩
ℝ*) = (Base‘𝐺)) |
| 71 | 68, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((0[,]+∞) ∩ ℝ*) = (Base‘𝐺) |
| 72 | 67, 71 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢
(0[,]+∞) = (Base‘𝐺) |
| 73 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 74 | 72, 73 | gsumsn 19972 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) ∈ (0[,]+∞)) → (𝐺 Σg
(𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
| 75 | 61, 62, 64, 74 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
| 76 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
| 77 | 56, 75, 76 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐺 Σg
(𝐹 ↾ {𝑦}))) |
| 78 | | reseq2 5992 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑦} → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝐹 ↾ {𝑦}))) |
| 80 | 79 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(𝐺
Σg (𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥))) |
| 81 | 45, 77, 80 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥))) |
| 82 | | pnfxr 11315 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
| 83 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
ℝ*) |
| 84 | 38 | elrnmpt 5969 |
. . . . . . . . . . . 12
⊢ (+∞
∈ ℝ* → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)))) |
| 85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (+∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
| 86 | 81, 85 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
| 87 | | supxrpnf 13360 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆ ℝ*
∧ +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
| 88 | 40, 86, 87 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
| 89 | 88 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
| 90 | 89 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
| 91 | 90 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞)) |
| 92 | 19, 91 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
| 93 | 14, 92 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 94 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
| 95 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
| 96 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
| 97 | 95, 96 | fge0iccico 46385 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
| 98 | 94, 97 | sge0reval 46387 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
| 99 | 23, 27 | feqresmpt 6978 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
| 100 | 99 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
| 101 | 100 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 102 | 21 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 103 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
| 104 | | xrsadd 21397 |
. . . . . . . . . . . . . 14
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
| 105 | 103, 104 | ressplusg 17334 |
. . . . . . . . . . . . 13
⊢
((0[,]+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞)))) |
| 106 | 68, 105 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
| 107 | 106 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) = +𝑒 |
| 108 | 102, 107 | eqtr2i 2766 |
. . . . . . . . . 10
⊢
+𝑒 = (+g‘𝐺) |
| 109 | 21 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
| 110 | | icossicc 13476 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 111 | 68, 110 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆
(0[,]+∞)) |
| 112 | | ressabs 17294 |
. . . . . . . . . . . 12
⊢
(((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆ (0[,]+∞))
→ ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s
(0[,)+∞))) |
| 113 | 111, 112 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s
(0[,)+∞)) |
| 114 | 109, 113 | eqtr2i 2766 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (𝐺
↾s (0[,)+∞)) |
| 115 | 58 | elexi 3503 |
. . . . . . . . . . 11
⊢ 𝐺 ∈ V |
| 116 | 115 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺 ∈ V) |
| 117 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
| 118 | 110 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ⊆
(0[,]+∞)) |
| 119 | | 0xr 11308 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
| 120 | 119 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ∈
ℝ*) |
| 121 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → +∞ ∈
ℝ*) |
| 122 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,]+∞)) |
| 123 | 26 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
| 124 | 123 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
| 125 | 122, 124 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
| 126 | 20, 125 | sselid 3981 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈
ℝ*) |
| 127 | | iccgelb 13443 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑦) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑦)) |
| 128 | 120, 121,
125, 127 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ≤ (𝐹‘𝑦)) |
| 129 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) = +∞ → (𝐹‘𝑦) = +∞) |
| 130 | 129 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) = +∞ → +∞ = (𝐹‘𝑦)) |
| 131 | 130 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐹‘𝑦)) |
| 132 | 11 | ffund 6740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
| 133 | 132 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) |
| 134 | 22, 123 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
| 135 | 11 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom 𝐹 = 𝑋) |
| 136 | 135 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 = dom 𝐹) |
| 137 | 136 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) |
| 138 | 134, 137 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) |
| 139 | | fvelrn 7096 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) |
| 140 | 133, 138,
139 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) |
| 141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ ran 𝐹) |
| 142 | 131, 141 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
| 143 | 142 | adantl3r 750 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
| 144 | 96 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → ¬ +∞ ∈
ran 𝐹) |
| 145 | 143, 144 | pm2.65da 817 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑦) = +∞) |
| 146 | 145 | neqned 2947 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ≠ +∞) |
| 147 | | ge0xrre 45544 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) |
| 148 | 125, 146,
147 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
| 149 | 148 | ltpnfd 13163 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) < +∞) |
| 150 | 120, 121,
126, 128, 149 | elicod 13437 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
| 151 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
| 152 | 150, 151 | fmptd 7134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)):𝑥⟶(0[,)+∞)) |
| 153 | | 0e0icopnf 13498 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
| 154 | 153 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
(0[,)+∞)) |
| 155 | | eliccxr 13475 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
| 156 | | xaddlid 13284 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (0 +𝑒 𝑦) = 𝑦) |
| 157 | | xaddrid 13283 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (𝑦
+𝑒 0) = 𝑦) |
| 158 | 156, 157 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
| 159 | 155, 158 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]+∞) →
((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
| 160 | 159 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ (0[,]+∞)) → ((0
+𝑒 𝑦) =
𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
| 161 | 72, 108, 114, 116, 117, 118, 152, 154, 160 | gsumress 18695 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 162 | | rege0subm 21441 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
| 163 | 162 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
| 164 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
| 165 | 117, 163,
152, 164 | gsumsubm 18848 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 166 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 167 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 168 | 167 | mptex 7243 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V |
| 169 | 168 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V) |
| 170 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
↾s (0[,)+∞)) ∈ V) |
| 171 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
| 172 | | rge0ssre 13496 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℝ |
| 173 | | ax-resscn 11212 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
| 174 | 172, 173 | sstri 3993 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℂ |
| 175 | | cnfldbas 21368 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
(Base‘ℂfld) |
| 176 | 164, 175 | ressbas2 17283 |
. . . . . . . . . . . . . . . 16
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 177 | 174, 176 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
| 178 | 177 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (0[,)+∞) |
| 179 | 110, 20 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ ℝ* |
| 180 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
| 181 | 180, 69 | ressbas2 17283 |
. . . . . . . . . . . . . . 15
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
| 182 | 179, 181 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
| 183 | 178, 182 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℝ*𝑠 ↾s
(0[,)+∞))) |
| 184 | 183 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Base‘(ℂfld ↾s (0[,)+∞))) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
| 185 | | rge0srg 21456 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
| 186 | 185 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(ℂfld ↾s (0[,)+∞)) ∈
SRing) |
| 187 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 188 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 189 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℂfld ↾s
(0[,)+∞))) |
| 190 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘(ℂfld
↾s (0[,)+∞))) |
| 191 | 189, 190 | srgacl 20202 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s (0[,)+∞)) ∈
SRing ∧ 𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 192 | 186, 187,
188, 191 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 193 | 192 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 194 | 172 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
| 195 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 196 | 195, 178 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(0[,)+∞)) |
| 197 | 194, 196 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
ℝ) |
| 198 | 197 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
ℝ) |
| 199 | 172 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
| 200 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
| 201 | 200, 178 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(0[,)+∞)) |
| 202 | 199, 201 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
ℝ) |
| 203 | 202 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
ℝ) |
| 204 | | rexadd 13274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 +𝑒 𝑡) = (𝑠 + 𝑡)) |
| 205 | 204 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 + 𝑡) = (𝑠 +𝑒 𝑡)) |
| 206 | 162 | elexi 3503 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ∈ V |
| 207 | | cnfldadd 21370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℂfld) |
| 208 | 164, 207 | ressplusg 17334 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
| 209 | 206, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
| 210 | 209, 207 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘ℂfld) |
| 211 | 210, 207 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = + |
| 212 | 211 | oveqi 7444 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡) |
| 213 | 212 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡)) |
| 214 | 180, 104 | ressplusg 17334 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
| 215 | 206, 214 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
| 216 | 215 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) = +𝑒 |
| 217 | 216 | oveqi 7444 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡) |
| 218 | 217 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡)) |
| 219 | 205, 213,
218 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
| 220 | 198, 203,
219 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
| 221 | 220 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
| 222 | | funmpt 6604 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
| 223 | 222 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Fun (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
| 224 | 150, 177 | eleqtrdi 2851 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 225 | 224 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 226 | 151 | rnmptss 7143 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞))) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 227 | 225, 226 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
| 228 | 169, 170,
171, 184, 193, 221, 223, 227 | gsumpropd2 18693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 229 | 165, 166,
228 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
| 230 | 30 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
| 231 | 148 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ) |
| 232 | 230, 231 | gsumfsum 21452 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 233 | 229, 232 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
| 234 | 101, 161,
233 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (𝐺 Σg (𝐹 ↾ 𝑥))) |
| 235 | 234 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
| 236 | 235 | rneqd 5949 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
| 237 | 236 | supeq1d 9486 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 238 | 98, 237 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 239 | 93, 238 | pm2.61dan 813 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
| 240 | 21, 9, 11, 1 | xrge0tsms 24856 |
. . 3
⊢ (𝜑 → (𝐺 tsums 𝐹) = {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
| 241 | 239, 240 | eleq12d 2835 |
. 2
⊢ (𝜑 →
((Σ^‘𝐹) ∈ (𝐺 tsums 𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) ∈
{sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)})) |
| 242 | 8, 241 | mpbird 257 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (𝐺 tsums 𝐹)) |