Step | Hyp | Ref
| Expression |
1 | | eqid 2651 |
. . . 4
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
3 | | xrltso 12012 |
. . . . . 6
⊢ < Or
ℝ* |
4 | 3 | supex 8410 |
. . . . 5
⊢ sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
∈ V) |
6 | | elsng 4224 |
. . . 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 247 |
. 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 40908 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) →
(Σ^‘𝐹) = +∞) |
15 | | ffn 6083 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶(0[,]+∞) → 𝐹 Fn 𝑋) |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝑋) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → 𝐹 Fn 𝑋) |
18 | | fvelrnb 6282 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑋 → (+∞ ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (+∞ ∈ ran
𝐹 ↔ ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞)) |
20 | 13, 19 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → ∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞) |
21 | | iccssxr 12294 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ ℝ* |
22 | | sge0tsms.g |
. . . . . . . . . . . . . . 15
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
23 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) |
24 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,]+∞)) |
25 | | elinel1 3832 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ 𝒫 𝑋) |
26 | | elpwi 4201 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋) |
29 | | fssres 6108 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝑋⟶(0[,]+∞) ∧ 𝑥 ⊆ 𝑋) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
30 | 24, 28, 29 | syl2anc 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,]+∞)) |
31 | | elinel2 3833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
33 | | 0red 10079 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
ℝ) |
34 | 30, 32, 33 | fdmfifsupp 8326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) finSupp 0) |
35 | 22, 23, 30, 34 | gsumge0cl 40906 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈ (0[,]+∞)) |
36 | 21, 35 | sseldi 3634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
37 | 36 | ralrimiva 2995 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
38 | 37 | 3ad2ant1 1102 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∀𝑥 ∈ (𝒫 𝑋 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑥)) ∈
ℝ*) |
39 | | eqid 2651 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) |
40 | 39 | rnmptss 6432 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝒫 𝑋 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑥)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆
ℝ*) |
41 | 38, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ⊆
ℝ*) |
42 | | snelpwi 4942 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ 𝒫 𝑋) |
43 | | snfi 8079 |
. . . . . . . . . . . . . . 15
⊢ {𝑦} ∈ Fin |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ Fin) |
45 | 42, 44 | elind 3831 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑋 → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
46 | 45 | 3ad2ant2 1103 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → {𝑦} ∈ (𝒫 𝑋 ∩ Fin)) |
47 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) |
48 | | snssi 4371 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → {𝑦} ⊆ 𝑋) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → {𝑦} ⊆ 𝑋) |
50 | 47, 49 | fssresd 6109 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}):{𝑦}⟶(0[,]+∞)) |
51 | 50 | feqmptd 6288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥))) |
52 | | fvres 6245 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑦} → ((𝐹 ↾ {𝑦})‘𝑥) = (𝐹‘𝑥)) |
53 | 52 | mpteq2ia 4773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑦} ↦ ((𝐹 ↾ {𝑦})‘𝑥)) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
55 | 51, 54 | eqtrd 2685 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) |
56 | 55 | oveq2d 6706 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
57 | 56 | 3adant3 1101 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝐹 ↾ {𝑦})) = (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥)))) |
58 | | xrge0cmn 19836 |
. . . . . . . . . . . . . . . . 17
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
59 | 22, 58 | eqeltri 2726 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 ∈ CMnd |
60 | | cmnmnd 18254 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐺 ∈ Mnd |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝐺 ∈ Mnd) |
63 | | simp2 1082 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → 𝑦 ∈ 𝑋) |
64 | 11 | ffvelrnda 6399 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
65 | 64 | 3adant3 1101 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
66 | | df-ss 3621 |
. . . . . . . . . . . . . . . . . 18
⊢
((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩
ℝ*) = (0[,]+∞)) |
67 | 21, 66 | mpbi 220 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∩ ℝ*) =
(0[,]+∞) |
68 | 67 | eqcomi 2660 |
. . . . . . . . . . . . . . . 16
⊢
(0[,]+∞) = ((0[,]+∞) ∩
ℝ*) |
69 | | ovex 6718 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,]+∞) ∈ V |
70 | | xrsbas 19810 |
. . . . . . . . . . . . . . . . . 18
⊢
ℝ* =
(Base‘ℝ*𝑠) |
71 | 22, 70 | ressbas 15977 |
. . . . . . . . . . . . . . . . 17
⊢
((0[,]+∞) ∈ V → ((0[,]+∞) ∩
ℝ*) = (Base‘𝐺)) |
72 | 69, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((0[,]+∞) ∩ ℝ*) = (Base‘𝐺) |
73 | 68, 72 | eqtri 2673 |
. . . . . . . . . . . . . . 15
⊢
(0[,]+∞) = (Base‘𝐺) |
74 | | fveq2 6229 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
75 | 73, 74 | gsumsn 18400 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) ∈ (0[,]+∞)) → (𝐺 Σg
(𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
76 | 62, 63, 65, 75 | syl3anc 1366 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐺 Σg (𝑥 ∈ {𝑦} ↦ (𝐹‘𝑥))) = (𝐹‘𝑦)) |
77 | | simp3 1083 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) = +∞) |
78 | 57, 76, 77 | 3eqtrrd 2690 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐺 Σg
(𝐹 ↾ {𝑦}))) |
79 | | reseq2 5423 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = {𝑦} → (𝐹 ↾ 𝑥) = (𝐹 ↾ {𝑦})) |
80 | 79 | oveq2d 6706 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = {𝑦} → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝐹 ↾ {𝑦}))) |
81 | 80 | eqeq2d 2661 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {𝑦} → (+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)) ↔ +∞ = (𝐺 Σg (𝐹 ↾ {𝑦})))) |
82 | 81 | rspcev 3340 |
. . . . . . . . . . . 12
⊢ (({𝑦} ∈ (𝒫 𝑋 ∩ Fin) ∧ +∞ =
(𝐺
Σg (𝐹 ↾ {𝑦}))) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥))) |
83 | 46, 78, 82 | syl2anc 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥))) |
84 | | pnfxr 10130 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈
ℝ*) |
86 | 39 | elrnmpt 5404 |
. . . . . . . . . . . 12
⊢ (+∞
∈ ℝ* → (+∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg (𝐹 ↾ 𝑥)))) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → (+∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)+∞ = (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
88 | 83, 87 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥)))) |
89 | | supxrpnf 12186 |
. . . . . . . . . 10
⊢ ((ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))) ⊆ ℝ*
∧ +∞ ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) =
+∞) |
90 | 41, 88, 89 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑦) = +∞) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
91 | 90 | 3exp 1283 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
92 | 91 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (𝑦 ∈ 𝑋 → ((𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞))) |
93 | 92 | rexlimdv 3059 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → (∃𝑦 ∈ 𝑋 (𝐹‘𝑦) = +∞ → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞)) |
94 | 20, 93 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ +∞ ∈ ran 𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, < )
= +∞) |
95 | 14, 94 | eqtr4d 2688 |
. . . 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 40905 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → 𝐹:𝑋⟶(0[,)+∞)) |
100 | 96, 99 | sge0reval 40907 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
101 | 24, 28 | feqresmpt 6289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
102 | 101 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
103 | 102 | oveq2d 6706 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑥)) = (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
104 | 22 | fveq2i 6232 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
105 | | eqid 2651 |
. . . . . . . . . . . . . 14
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) = (ℝ*𝑠 ↾s
(0[,]+∞)) |
106 | | xrsadd 19811 |
. . . . . . . . . . . . . 14
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
107 | 105, 106 | ressplusg 16040 |
. . . . . . . . . . . . 13
⊢
((0[,]+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞)))) |
108 | 69, 107 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) |
109 | 108 | eqcomi 2660 |
. . . . . . . . . . 11
⊢
(+g‘(ℝ*𝑠
↾s (0[,]+∞))) = +𝑒 |
110 | 104, 109 | eqtr2i 2674 |
. . . . . . . . . 10
⊢
+𝑒 = (+g‘𝐺) |
111 | 22 | oveq1i 6700 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s
(0[,)+∞)) = ((ℝ*𝑠 ↾s
(0[,]+∞)) ↾s (0[,)+∞)) |
112 | | icossicc 12298 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
113 | 69, 112 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢
((0[,]+∞) ∈ V ∧ (0[,)+∞) ⊆
(0[,]+∞)) |
114 | | ressabs 15986 |
. . . . . . . . . . . 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 2674 |
. . . . . . . . . 10
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (𝐺
↾s (0[,)+∞)) |
117 | 59 | elexi 3244 |
. . . . . . . . . . 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 10124 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
122 | 121 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ∈
ℝ*) |
123 | 84 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → +∞ ∈
ℝ*) |
124 | 97 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,]+∞)) |
125 | 27 | sselda 3636 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝒫 𝑋 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
126 | 125 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
127 | 124, 126 | ffvelrnd 6400 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,]+∞)) |
128 | 21, 127 | sseldi 3634 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈
ℝ*) |
129 | | iccgelb 12268 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝐹‘𝑦) ∈ (0[,]+∞)) → 0 ≤ (𝐹‘𝑦)) |
130 | 122, 123,
127, 129 | syl3anc 1366 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 0 ≤ (𝐹‘𝑦)) |
131 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑦) = +∞ → (𝐹‘𝑦) = +∞) |
132 | 131 | eqcomd 2657 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) = +∞ → +∞ = (𝐹‘𝑦)) |
133 | 132 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ = (𝐹‘𝑦)) |
134 | | ffun 6086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝑋⟶(0[,]+∞) → Fun 𝐹) |
135 | 11, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
136 | 135 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → Fun 𝐹) |
137 | 23, 125 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋) |
138 | | fdm 6089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝑋⟶(0[,]+∞) → dom 𝐹 = 𝑋) |
139 | 11, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom 𝐹 = 𝑋) |
140 | 139 | eqcomd 2657 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 = dom 𝐹) |
141 | 140 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑋 = dom 𝐹) |
142 | 137, 141 | eleqtrd 2732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ dom 𝐹) |
143 | | fvelrn 6392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ ran 𝐹) |
144 | 136, 142,
143 | syl2anc 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ran 𝐹) |
145 | 144 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → (𝐹‘𝑦) ∈ ran 𝐹) |
146 | 133, 145 | eqeltrd 2730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
147 | 146 | adantlllr 39513 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → +∞ ∈ ran
𝐹) |
148 | 98 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran 𝐹)
∧ 𝑥 ∈ (𝒫
𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) ∧ (𝐹‘𝑦) = +∞) → ¬ +∞ ∈
ran 𝐹) |
149 | 147, 148 | pm2.65da 599 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑦) = +∞) |
150 | 149 | neqned 2830 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ≠ +∞) |
151 | | ge0xrre 40076 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) ∈ (0[,]+∞) ∧ (𝐹‘𝑦) ≠ +∞) → (𝐹‘𝑦) ∈ ℝ) |
152 | 127, 150,
151 | syl2anc 694 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
153 | 152 | ltpnfd 11993 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) < +∞) |
154 | 122, 123,
128, 130, 153 | elicod 12262 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
155 | | eqid 2651 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) = (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
156 | 154, 155 | fmptd 6425 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)):𝑥⟶(0[,)+∞)) |
157 | | 0e0icopnf 12320 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
158 | 157 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 0 ∈
(0[,)+∞)) |
159 | 21 | sseli 3632 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0[,]+∞) →
𝑦 ∈
ℝ*) |
160 | | xaddid2 12111 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ (0 +𝑒 𝑦) = 𝑦) |
161 | | xaddid1 12110 |
. . . . . . . . . . . . 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 17323 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐺 Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
166 | | rege0subm 19850 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
167 | 166 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
168 | | eqid 2651 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s (0[,)+∞)) =
(ℂfld ↾s (0[,)+∞)) |
169 | 119, 167,
156, 168 | gsumsubm 17420 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
170 | | eqidd 2652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
171 | | vex 3234 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
172 | 171 | mptex 6527 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V |
173 | 172 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ∈ V) |
174 | | ovexd 6720 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
↾s (0[,)+∞)) ∈ V) |
175 | | ovexd 6720 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,)+∞))
∈ V) |
176 | | rge0ssre 12318 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℝ |
177 | | ax-resscn 10031 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
⊆ ℂ |
178 | 176, 177 | sstri 3645 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℂ |
179 | | cnfldbas 19798 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
(Base‘ℂfld) |
180 | 168, 179 | ressbas2 15978 |
. . . . . . . . . . . . . . . 16
⊢
((0[,)+∞) ⊆ ℂ → (0[,)+∞) =
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
181 | 178, 180 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) = (Base‘(ℂfld ↾s
(0[,)+∞))) |
182 | 181 | eqcomi 2660 |
. . . . . . . . . . . . . 14
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (0[,)+∞) |
183 | 112, 21 | sstri 3645 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ ℝ* |
184 | | eqid 2651 |
. . . . . . . . . . . . . . . 16
⊢
(ℝ*𝑠 ↾s
(0[,)+∞)) = (ℝ*𝑠 ↾s
(0[,)+∞)) |
185 | 184, 70 | ressbas2 15978 |
. . . . . . . . . . . . . . 15
⊢
((0[,)+∞) ⊆ ℝ* → (0[,)+∞) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
186 | 183, 185 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) = (Base‘(ℝ*𝑠
↾s (0[,)+∞))) |
187 | 182, 186 | eqtri 2673 |
. . . . . . . . . . . . 13
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℝ*𝑠 ↾s
(0[,)+∞))) |
188 | 187 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
(Base‘(ℂfld ↾s (0[,)+∞))) =
(Base‘(ℝ*𝑠 ↾s
(0[,)+∞)))) |
189 | | rge0srg 19865 |
. . . . . . . . . . . . . . 15
⊢
(ℂfld ↾s (0[,)+∞)) ∈
SRing |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(ℂfld ↾s (0[,)+∞)) ∈
SRing) |
191 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
192 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
193 | | eqid 2651 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(ℂfld ↾s (0[,)+∞)))
= (Base‘(ℂfld ↾s
(0[,)+∞))) |
194 | | eqid 2651 |
. . . . . . . . . . . . . . 15
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘(ℂfld
↾s (0[,)+∞))) |
195 | 193, 194 | srgacl 18570 |
. . . . . . . . . . . . . 14
⊢
(((ℂfld ↾s (0[,)+∞)) ∈
SRing ∧ 𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
196 | 190, 191,
192, 195 | syl3anc 1366 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
197 | 196 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
198 | 176 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
199 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
200 | 199, 182 | syl6eleq 2740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
(0[,)+∞)) |
201 | 198, 200 | sseldd 3637 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑠 ∈
ℝ) |
202 | 201 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑠 ∈
ℝ) |
203 | 176 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
(0[,)+∞) ⊆ ℝ) |
204 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(Base‘(ℂfld ↾s
(0[,)+∞)))) |
205 | 204, 182 | syl6eleq 2740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
(0[,)+∞)) |
206 | 203, 205 | sseldd 3637 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) →
𝑡 ∈
ℝ) |
207 | 206 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
𝑡 ∈
ℝ) |
208 | | rexadd 12101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 +𝑒 𝑡) = (𝑠 + 𝑡)) |
209 | 208 | eqcomd 2657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠 + 𝑡) = (𝑠 +𝑒 𝑡)) |
210 | 166 | elexi 3244 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0[,)+∞) ∈ V |
211 | | cnfldadd 19799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℂfld) |
212 | 168, 211 | ressplusg 16040 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((0[,)+∞) ∈ V → + =
(+g‘(ℂfld ↾s
(0[,)+∞)))) |
213 | 210, 212 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ + =
(+g‘(ℂfld ↾s
(0[,)+∞))) |
214 | 213, 211 | eqtr3i 2675 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = (+g‘ℂfld) |
215 | 214, 211 | eqtr4i 2676 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℂfld ↾s
(0[,)+∞))) = + |
216 | 215 | oveqi 6703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡) |
217 | 216 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠 + 𝑡)) |
218 | 184, 106 | ressplusg 16040 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,)+∞) ∈ V → +𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞)))) |
219 | 210, 218 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
+𝑒 =
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) |
220 | 219 | eqcomi 2660 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘(ℝ*𝑠
↾s (0[,)+∞))) = +𝑒 |
221 | 220 | oveqi 6703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡) |
222 | 221 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡) =
(𝑠 +𝑒 𝑡)) |
223 | 209, 217,
222 | 3eqtr4d 2695 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
224 | 202, 207,
223 | syl2anc 694 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∈
(Base‘(ℂfld ↾s (0[,)+∞))) ∧
𝑡 ∈
(Base‘(ℂfld ↾s (0[,)+∞)))) →
(𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
225 | 224 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (𝑠 ∈ (Base‘(ℂfld
↾s (0[,)+∞))) ∧ 𝑡 ∈ (Base‘(ℂfld
↾s (0[,)+∞))))) → (𝑠(+g‘(ℂfld
↾s (0[,)+∞)))𝑡) = (𝑠(+g‘(ℝ*𝑠
↾s (0[,)+∞)))𝑡)) |
226 | | funmpt 5964 |
. . . . . . . . . . . . 13
⊢ Fun
(𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) |
227 | 226 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Fun (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) |
228 | 154, 181 | syl6eleq 2740 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
229 | 228 | ralrimiva 2995 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞)))) |
230 | 155 | rnmptss 6432 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑥 (𝐹‘𝑦) ∈ (Base‘(ℂfld
↾s (0[,)+∞))) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ran (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)) ⊆ (Base‘(ℂfld
↾s (0[,)+∞)))) |
232 | 173, 174,
175, 188, 197, 225, 227, 231 | gsumpropd2 17321 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((ℂfld
↾s (0[,)+∞)) Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
233 | 169, 170,
232 | 3eqtrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) =
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦)))) |
234 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin) |
235 | 152 | recnd 10106 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ) |
236 | 234, 235 | gsumfsum 19861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (ℂfld
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
237 | 233, 236 | eqtr3d 2687 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,)+∞))
Σg (𝑦 ∈ 𝑥 ↦ (𝐹‘𝑦))) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
238 | 103, 165,
237 | 3eqtrrd 2690 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (𝐺 Σg (𝐹 ↾ 𝑥))) |
239 | 238 | mpteq2dva 4777 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
240 | 239 | rneqd 5385 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥)))) |
241 | 240 | supeq1d 8393 |
. . . . 5
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) → sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) = sup(ran
(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑥))), ℝ*, <
)) |
242 | 100, 241 | eqtrd 2685 |
. . . 4
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
𝐹) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
243 | 95, 242 | pm2.61dan 849 |
. . 3
⊢ (𝜑 →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)) |
244 | 22, 9, 11, 1 | xrge0tsms 22684 |
. . 3
⊢ (𝜑 → (𝐺 tsums 𝐹) = {sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, <
)}) |
245 | 243, 244 | eleq12d 2724 |
. 2
⊢ (𝜑 →
((Σ^‘𝐹) ∈ (𝐺 tsums 𝐹) ↔ sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑥))), ℝ*, < ) ∈
{sup(ran (𝑥 ∈
(𝒫 𝑋 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑥))), ℝ*, <
)})) |
246 | 8, 245 | mpbird 247 |
1
⊢ (𝜑 →
(Σ^‘𝐹) ∈ (𝐺 tsums 𝐹)) |