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 12731 |
. . . . . 6
⊢ < Or
ℝ* |
4 | 3 | supex 9079 |
. . . . 5
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V) |
6 | | elsng 4555 |
. . . 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 260 |
. 2
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ {sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
9 | | sge0tsms.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝑋 ∈ 𝑉) |
11 | | sge0tsms.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
12 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
13 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
14 | 10, 12, 13 | sge0pnfval 43586 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
15 | 11 | ffnd 6546 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑋) |
16 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹 Fn 𝑋) |
17 | | fvelrnb 6773 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
19 | 13, 18 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
20 | | iccssxr 13018 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ ℝ* |
21 | | sge0tsms.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
22 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
23 | 11 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
24 | | elinel1 4109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
25 | | elpwi 4522 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
27 | 26 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
28 | | fssres 6585 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
29 | 23, 27, 28 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
30 | | elinel2 4110 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
31 | 30 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
32 | | 0red 10836 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
ℝ) |
33 | 29, 31, 32 | fdmfifsupp 8995 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) finSupp 0) |
34 | 21, 22, 29, 33 | gsumge0cl 43584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈ (0[,]+∞)) |
35 | 20, 34 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
36 | 35 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
37 | 36 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) |
39 | 38 | rnmptss 6939 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
40 | 37, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ⊆
ℝ*) |
41 | | snelpwi 5329 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
42 | | snfi 8721 |
. . . . . . . . . . . . . . 15
⊢ {𝑦} ∈ Fin |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
44 | 41, 43 | elind 4108 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
45 | 44 | 3ad2ant2 1136 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
46 | 11 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
47 | | snssi 4721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → {𝑦} ⊆ 𝑋) |
48 | 47 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → {𝑦} ⊆ 𝑋) |
49 | 46, 48 | fssresd 6586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
50 | 49 | feqmptd 6780 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥))) |
51 | | fvres 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑥) = (𝐹‘𝑥)) |
52 | 51 | mpteq2ia 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
54 | 50, 53 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
55 | 54 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
56 | 55 | 3adant3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
57 | | xrge0cmn 20405 |
. . . . . . . . . . . . . . . . 17
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
58 | 21, 57 | eqeltri 2834 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ∈ CMnd |
59 | | cmnmnd 19186 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ Mnd |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐺 ∈ Mnd) |
62 | | simp2 1139 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
63 | 11 | ffvelrnda 6904 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
64 | 63 | 3adant3 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
65 | | df-ss 3883 |
. . . . . . . . . . . . . . . . . 18
⊢
((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩
ℝ*) = (0[,]+∞)) |
66 | 20, 65 | mpbi 233 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∩ ℝ*) =
(0[,]+∞) |
67 | 66 | eqcomi 2746 |
. . . . . . . . . . . . . . . 16
⊢
(0[,]+∞) = ((0[,]+∞) ∩
ℝ*) |
68 | | ovex 7246 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ∈ V |
69 | | xrsbas 20379 |
. . . . . . . . . . . . . . . . . 18
⊢
ℝ* =
(Base‘ℝ*𝑠) |
70 | 21, 69 | ressbas 16790 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∈ V → ((0[,]+∞) ∩
ℝ*) = (Base‘𝐺)) |
71 | 68, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((0[,]+∞) ∩ ℝ*) = (Base‘𝐺) |
72 | 67, 71 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢
(0[,]+∞) = (Base‘𝐺) |
73 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
74 | 72, 73 | gsumsn 19339 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) ∈ (0[,]+∞)) → (𝐺 Σg
(𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
75 | 61, 62, 64, 74 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
76 | | simp3 1140 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
77 | 56, 75, 76 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐺 Σg
(𝐹 ↾ {𝑦}))) |
78 | | reseq2 5846 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
79 | 78 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑦} → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝐹 ↾ {𝑦}))) |
80 | 79 | rspceeqv 3552 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(𝐺
Σg (𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥))) |
81 | 45, 77, 80 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥))) |
82 | | pnfxr 10887 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
ℝ*) |
84 | 38 | elrnmpt 5825 |
. . . . . . . . . . . 12
⊢ (+∞
∈ ℝ* → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (+∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
86 | 81, 85 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
87 | | supxrpnf 12908 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆ ℝ*
∧ +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
88 | 40, 86, 87 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
89 | 88 | 3exp 1121 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
90 | 89 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
91 | 90 | rexlimdv 3202 |
. . . . . 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 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
95 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
96 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
97 | 95, 96 | fge0iccico 43583 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
98 | 94, 97 | sge0reval 43585 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
99 | 23, 27 | feqresmpt 6781 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
100 | 99 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
101 | 100 | oveq2d 7229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
102 | 21 | fveq2i 6720 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
103 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
104 | | xrsadd 20380 |
. . . . . . . . . . . . . 14
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
105 | 103, 104 | ressplusg 16834 |
. . . . . . . . . . . . 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 7223 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
110 | | icossicc 13024 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
111 | 68, 110 | pm3.2i 474 |
. . . . . . . . . . . 12
⊢
((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆
(0[,]+∞)) |
112 | | ressabs 16800 |
. . . . . . . . . . . 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 3427 |
. . . . . . . . . . 11
⊢ 𝐺 ∈ V |
116 | 115 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺 ∈ V) |
117 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
118 | 110 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ⊆
(0[,]+∞)) |
119 | | 0xr 10880 |
. . . . . . . . . . . . 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 3901 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
124 | 123 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
125 | 122, 124 | ffvelrnd 6905 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
126 | 20, 125 | sseldi 3899 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈
ℝ*) |
127 | | iccgelb 12991 |
. . . . . . . . . . . . 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 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐹‘𝑦)) |
132 | 11 | ffund 6549 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
133 | 132 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) |
134 | 22, 123 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
135 | 11 | fdmd 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom 𝐹 = 𝑋) |
136 | 135 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 = dom 𝐹) |
137 | 136 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) |
138 | 134, 137 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) |
139 | | fvelrn 6897 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) |
140 | 133, 138,
139 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) |
141 | 140 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ ran 𝐹) |
142 | 131, 141 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 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 42744 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) |
148 | 125, 146,
147 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
149 | 148 | ltpnfd 12713 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) < +∞) |
150 | 120, 121,
126, 128, 149 | elicod 12985 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
151 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
152 | 150, 151 | fmptd 6931 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)):𝑥⟶(0[,)+∞)) |
153 | | 0e0icopnf 13046 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
154 | 153 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
(0[,)+∞)) |
155 | | eliccxr 13023 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
156 | | xaddid2 12832 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (0 +𝑒 𝑦) = 𝑦) |
157 | | xaddid1 12831 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (𝑦
+𝑒 0) = 𝑦) |
158 | 156, 157 | jca 515 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
159 | 155, 158 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]+∞) →
((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
160 | 159 | adantl 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ (0[,]+∞)) → ((0
+𝑒 𝑦) =
𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
161 | 72, 108, 114, 116, 117, 118, 152, 154, 160 | gsumress 18154 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
162 | | rege0subm 20419 |
. . . . . . . . . . . . 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 18261 |
. . . . . . . . . . 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 3412 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
168 | 167 | mptex 7039 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V |
169 | 168 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V) |
170 | | ovexd 7248 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
↾s (0[,)+∞)) ∈ V) |
171 | | ovexd 7248 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
172 | | rge0ssre 13044 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℝ |
173 | | ax-resscn 10786 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
174 | 172, 173 | sstri 3910 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℂ |
175 | | cnfldbas 20367 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
(Base‘ℂfld) |
176 | 164, 175 | ressbas2 16791 |
. . . . . . . . . . . . . . . 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 3910 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ ℝ* |
180 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
181 | 180, 69 | ressbas2 16791 |
. . . . . . . . . . . . . . 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 20434 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(ℂfld ↾s (0[,)+∞)) ∈
SRing) |
187 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
188 | | simpr 488 |
. . . . . . . . . . . . . 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 19539 |
. . . . . . . . . . . . . 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 485 |
. . . . . . . . . . . 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 2848 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(0[,)+∞)) |
197 | 194, 196 | sseldd 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
ℝ) |
198 | 197 | adantr 484 |
. . . . . . . . . . . . . 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 2848 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(0[,)+∞)) |
202 | 199, 201 | sseldd 3902 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
ℝ) |
203 | 202 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
ℝ) |
204 | | rexadd 12822 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 +𝑒 𝑡) = (𝑠 + 𝑡)) |
205 | 204 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 + 𝑡) = (𝑠 +𝑒 𝑡)) |
206 | 162 | elexi 3427 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ∈ V |
207 | | cnfldadd 20368 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℂfld) |
208 | 164, 207 | ressplusg 16834 |
. . . . . . . . . . . . . . . . . . . 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 7226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡) |
213 | 212 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡)) |
214 | 180, 104 | ressplusg 16834 |
. . . . . . . . . . . . . . . . . . 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 7226 |
. . . . . . . . . . . . . . . 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 587 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
221 | 220 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
222 | | funmpt 6418 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
223 | 222 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Fun (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
224 | 150, 177 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
225 | 224 | ralrimiva 3105 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
226 | 151 | rnmptss 6939 |
. . . . . . . . . . . . 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 18152 |
. . . . . . . . . . 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 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
231 | 148 | recnd 10861 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ) |
232 | 230, 231 | gsumfsum 20430 |
. . . . . . . . . 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 5150 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
236 | 235 | rneqd 5807 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
237 | 236 | supeq1d 9062 |
. . . . 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 23731 |
. . 3
⊢ (𝜑 → (𝐺 tsums 𝐹) = {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
241 | 239, 240 | eleq12d 2832 |
. 2
⊢ (𝜑 →
((Σ^‘𝐹) ∈ (𝐺 tsums 𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) ∈
{sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)})) |
242 | 8, 241 | mpbird 260 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (𝐺 tsums 𝐹)) |