Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
3 | | xrltso 11850 |
. . . . . 6
⊢ < Or
ℝ* |
4 | 3 | supex 8252 |
. . . . 5
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V) |
6 | | elsng 4139 |
. . . 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 246 |
. 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 476 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → +∞ ∈ ran
𝐹) |
14 | 10, 12, 13 | sge0pnfval 39266 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
15 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝐹 Fn 𝑋) |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑋) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹 Fn 𝑋) |
18 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
20 | 13, 19 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
21 | | iccssxr 12127 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ ℝ* |
22 | | sge0tsms.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
23 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
24 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
25 | | elinel1 3761 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
26 | | elpwi 4117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
29 | | fssres 5983 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
30 | 24, 28, 29 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
31 | | elinel2 3762 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
33 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
ℝ) |
34 | 30, 32, 33 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) finSupp 0) |
35 | 22, 23, 30, 34 | gsumge0cl 39264 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈ (0[,]+∞)) |
36 | 21, 35 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
37 | 36 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) |
40 | 39 | rnmptss 6299 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ⊆
ℝ*) |
42 | | snelpwi 4839 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
43 | | snfi 7923 |
. . . . . . . . . . . . . . 15
⊢ {𝑦} ∈ Fin |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
45 | 42, 44 | elind 3760 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
46 | 45 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
47 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
48 | | snssi 4280 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → {𝑦} ⊆ 𝑋) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → {𝑦} ⊆ 𝑋) |
50 | 47, 49 | fssresd 5984 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
51 | 50 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥))) |
52 | | fvres 6117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑥) = (𝐹‘𝑥)) |
53 | 52 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
55 | 51, 54 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
56 | 55 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
57 | 56 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
58 | | xrge0cmn 19607 |
. . . . . . . . . . . . . . . . 17
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
59 | 22, 58 | eqeltri 2684 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ∈ CMnd |
60 | | cmnmnd 18031 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ Mnd |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐺 ∈ Mnd) |
63 | | simp2 1055 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
64 | 11 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
65 | 64 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
66 | | df-ss 3554 |
. . . . . . . . . . . . . . . . . 18
⊢
((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩
ℝ*) = (0[,]+∞)) |
67 | 21, 66 | mpbi 219 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∩ ℝ*) =
(0[,]+∞) |
68 | 67 | eqcomi 2619 |
. . . . . . . . . . . . . . . 16
⊢
(0[,]+∞) = ((0[,]+∞) ∩
ℝ*) |
69 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ∈ V |
70 | | xrsbas 19581 |
. . . . . . . . . . . . . . . . . 18
⊢
ℝ* =
(Base‘ℝ*𝑠) |
71 | 22, 70 | ressbas 15757 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∈ V → ((0[,]+∞) ∩
ℝ*) = (Base‘𝐺)) |
72 | 69, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((0[,]+∞) ∩ ℝ*) = (Base‘𝐺) |
73 | 68, 72 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢
(0[,]+∞) = (Base‘𝐺) |
74 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
75 | 73, 74 | gsumsn 18177 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) ∈ (0[,]+∞)) → (𝐺 Σg
(𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
76 | 62, 63, 65, 75 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
77 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
78 | 57, 76, 77 | 3eqtrrd 2649 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐺 Σg
(𝐹 ↾ {𝑦}))) |
79 | | reseq2 5312 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑦} → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝐹 ↾ {𝑦}))) |
81 | 80 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑦} → (+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)) ↔ +∞ = (𝐺 Σg (𝐹 ↾ {𝑦})))) |
82 | 81 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(𝐺
Σg (𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥))) |
83 | 46, 78, 82 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥))) |
84 | | pnfxr 9971 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
ℝ*) |
86 | 39 | elrnmpt 5293 |
. . . . . . . . . . . 12
⊢ (+∞
∈ ℝ* → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)))) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (+∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
88 | 83, 87 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
89 | | supxrpnf 12020 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆ ℝ*
∧ +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
90 | 41, 88, 89 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
91 | 90 | 3exp 1256 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
92 | 91 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
93 | 92 | rexlimdv 3012 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞)) |
94 | 20, 93 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
95 | 14, 94 | eqtr4d 2647 |
. . . 4
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
96 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝑋 ∈ 𝑉) |
97 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,]+∞)) |
98 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ¬ +∞
∈ ran 𝐹) |
99 | 97, 98 | fge0iccico 39263 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
100 | 96, 99 | sge0reval 39265 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
101 | 24, 28 | feqresmpt 6160 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
102 | 101 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
103 | 102 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
104 | 22 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
105 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
106 | | xrsadd 19582 |
. . . . . . . . . . . . . 14
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
107 | 105, 106 | ressplusg 15818 |
. . . . . . . . . . . . 13
⊢
((0[,]+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞)))) |
108 | 69, 107 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
109 | 108 | eqcomi 2619 |
. . . . . . . . . . 11
⊢
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) = +𝑒 |
110 | 104, 109 | eqtr2i 2633 |
. . . . . . . . . 10
⊢
+𝑒 = (+g‘𝐺) |
111 | 22 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
112 | | icossicc 12131 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
113 | 69, 112 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆
(0[,]+∞)) |
114 | | ressabs 15766 |
. . . . . . . . . . . 12
⊢
(((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆ (0[,]+∞))
→ ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s
(0[,)+∞))) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) =
(ℝ*𝑠 ↾s
(0[,)+∞)) |
116 | 111, 115 | eqtr2i 2633 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (𝐺
↾s (0[,)+∞)) |
117 | 59 | elexi 3186 |
. . . . . . . . . . 11
⊢ 𝐺 ∈ V |
118 | 117 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐺 ∈ V) |
119 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
120 | 112 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ⊆
(0[,]+∞)) |
121 | | 0xr 9965 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
122 | 121 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ∈
ℝ*) |
123 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → +∞ ∈
ℝ*) |
124 | 97 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,]+∞)) |
125 | 27 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
126 | 125 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
127 | 124, 126 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
128 | 21, 127 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈
ℝ*) |
129 | | iccgelb 12101 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑦) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑦)) |
130 | 122, 123,
127, 129 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ≤ (𝐹‘𝑦)) |
131 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) = +∞ → (𝐹‘𝑦) = +∞) |
132 | 131 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) = +∞ → +∞ = (𝐹‘𝑦)) |
133 | 132 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐹‘𝑦)) |
134 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝑋⟶(0[,]+∞) → Fun 𝐹) |
135 | 11, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
136 | 135 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) |
137 | 23, 125 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
138 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
139 | 11, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom 𝐹 = 𝑋) |
140 | 139 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 = dom 𝐹) |
141 | 140 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) |
142 | 137, 141 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) |
143 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) |
144 | 136, 142,
143 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ ran 𝐹) |
146 | 133, 145 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
147 | 146 | adantlllr 38222 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
148 | 98 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → ¬ +∞ ∈
ran 𝐹) |
149 | 147, 148 | pm2.65da 598 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑦) = +∞) |
150 | 149 | neqned 2789 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ≠ +∞) |
151 | | ge0xrre 38605 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) |
152 | 127, 150,
151 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
153 | 152 | ltpnfd 11831 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) < +∞) |
154 | 122, 123,
128, 130, 153 | elicod 12095 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
155 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
156 | 154, 155 | fmptd 6292 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)):𝑥⟶(0[,)+∞)) |
157 | | 0e0icopnf 12153 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
158 | 157 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
(0[,)+∞)) |
159 | 21 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
160 | | xaddid2 11947 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (0 +𝑒 𝑦) = 𝑦) |
161 | | xaddid1 11946 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (𝑦
+𝑒 0) = 𝑦) |
162 | 160, 161 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ ((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
163 | 159, 162 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (0[,]+∞) →
((0 +𝑒 𝑦) = 𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
164 | 163 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ (0[,]+∞)) → ((0
+𝑒 𝑦) =
𝑦 ∧ (𝑦 +𝑒 0) = 𝑦)) |
165 | 73, 110, 116, 118, 119, 120, 156, 158, 164 | gsumress 17099 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
166 | | rege0subm 19621 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
167 | 166 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
168 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
169 | 119, 167,
156, 168 | gsumsubm 17196 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
170 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
171 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
172 | 171 | mptex 6390 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V |
173 | 172 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V) |
174 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(ℂfld ↾s (0[,)+∞)) ∈
V |
175 | 174 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
↾s (0[,)+∞)) ∈ V) |
176 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) ∈ V |
177 | 176 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
178 | | rge0ssre 12151 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℝ |
179 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
180 | 178, 179 | sstri 3577 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℂ |
181 | | cnfldbas 19571 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
(Base‘ℂfld) |
182 | 168, 181 | ressbas2 15758 |
. . . . . . . . . . . . . . . 16
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
183 | 180, 182 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
184 | 183 | eqcomi 2619 |
. . . . . . . . . . . . . 14
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (0[,)+∞) |
185 | 112, 21 | sstri 3577 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ ℝ* |
186 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
187 | 186, 70 | ressbas2 15758 |
. . . . . . . . . . . . . . 15
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
188 | 185, 187 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
189 | 184, 188 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℝ*𝑠 ↾s
(0[,)+∞))) |
190 | 189 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Base‘(ℂfld ↾s (0[,)+∞))) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
191 | | rge0srg 19636 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(ℂfld ↾s (0[,)+∞)) ∈
SRing) |
193 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
194 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
195 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℂfld ↾s
(0[,)+∞))) |
196 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘(ℂfld
↾s (0[,)+∞))) |
197 | 195, 196 | srgacl 18347 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s (0[,)+∞)) ∈
SRing ∧ 𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
198 | 192, 193,
194, 197 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
199 | 198 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
200 | 178 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
201 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
202 | 201, 184 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(0[,)+∞)) |
203 | 200, 202 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
ℝ) |
204 | 203 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
ℝ) |
205 | 178 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
206 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
207 | 206, 184 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(0[,)+∞)) |
208 | 205, 207 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
ℝ) |
209 | 208 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
ℝ) |
210 | | rexadd 11937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 +𝑒 𝑡) = (𝑠 + 𝑡)) |
211 | 210 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 + 𝑡) = (𝑠 +𝑒 𝑡)) |
212 | 166 | elexi 3186 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ∈ V |
213 | | cnfldadd 19572 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℂfld) |
214 | 168, 213 | ressplusg 15818 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
215 | 212, 214 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
216 | 215, 213 | eqtr3i 2634 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘ℂfld) |
217 | 216, 213 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = + |
218 | 217 | oveqi 6562 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡) |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡)) |
220 | 186, 106 | ressplusg 15818 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
221 | 212, 220 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
222 | 221 | eqcomi 2619 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) = +𝑒 |
223 | 222 | oveqi 6562 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡) |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡)) |
225 | 211, 219,
224 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
226 | 204, 209,
225 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
227 | 226 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
228 | | funmpt 5840 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
229 | 228 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Fun (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
230 | 154, 183 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
231 | 230 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
232 | 155 | rnmptss 6299 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞))) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
234 | 173, 175,
177, 190, 199, 227, 229, 233 | gsumpropd2 17097 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
235 | 169, 170,
234 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
236 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
237 | 152 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ) |
238 | 236, 237 | gsumfsum 19632 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
239 | 235, 238 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
240 | 103, 165,
239 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (𝐺 Σg (𝐹 ↾ 𝑥))) |
241 | 240 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
242 | 241 | rneqd 5274 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
243 | 242 | supeq1d 8235 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, <
)) |
244 | 100, 243 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
245 | 95, 244 | pm2.61dan 828 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
246 | 22, 9, 11, 1 | xrge0tsms 22445 |
. . 3
⊢ (𝜑 → (𝐺 tsums 𝐹) = {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
247 | 245, 246 | eleq12d 2682 |
. 2
⊢ (𝜑 →
((Σ^‘𝐹) ∈ (𝐺 tsums 𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) ∈
{sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)})) |
248 | 8, 247 | mpbird 246 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (𝐺 tsums 𝐹)) |