Step | Hyp | Ref
| Expression |
1 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → < Or
ℝ*) |
3 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1zzd 11285 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
5 | | esumpcvgval.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) |
6 | | esumpcvgval.2 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 → 𝐴 = 𝐵) |
7 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑙 ↔ 𝑙 = 𝑘) |
8 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
9 | 6, 7, 8 | 3imtr3i 279 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → 𝐵 = 𝐴) |
10 | 9 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑙 ∈ ℕ ↦ 𝐵) = (𝑘 ∈ ℕ ↦ 𝐴) |
11 | 5, 10 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞)) |
12 | 11 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞)) |
13 | | elrege0 12149 |
. . . . . . . . 9
⊢ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥))) |
14 | 13 | simplbi 475 |
. . . . . . . 8
⊢ (((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑥) ∈ ℝ) |
16 | 3, 4, 15 | serfre 12692 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)):ℕ⟶ℝ) |
17 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ ℕ ↦ 𝐵):ℕ⟶(0[,)+∞)) |
18 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
19 | 18 | peano2nnd 10914 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
20 | 17, 19 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈
(0[,)+∞)) |
21 | | elrege0 12149 |
. . . . . . . . . 10
⊢ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) ↔ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ ∧ 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))) |
22 | 21 | simprbi 479 |
. . . . . . . . 9
⊢ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → 0 ≤
((𝑙 ∈ ℕ ↦
𝐵)‘(𝑛 + 1))) |
23 | 20, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))) |
24 | 16 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ∈ ℝ) |
25 | 21 | simplbi 475 |
. . . . . . . . . 10
⊢ (((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ (0[,)+∞) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ) |
26 | 20, 25 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ∈ ℝ) |
27 | 24, 26 | addge01d 10494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)) ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1))))) |
28 | 23, 27 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))) |
29 | 18, 3 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
30 | | seqp1 12678 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘1) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1)) = ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) + ((𝑙 ∈ ℕ ↦ 𝐵)‘(𝑛 + 1)))) |
32 | 28, 31 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘(𝑛 + 1))) |
33 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
34 | 10 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ ∧ 𝐴 ∈ (0[,)+∞)) →
((𝑙 ∈ ℕ ↦
𝐵)‘𝑘) = 𝐴) |
35 | 33, 5, 34 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
36 | | rge0ssre 12151 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
37 | 36, 5 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) |
38 | 16 | feqmptd 6159 |
. . . . . . . . . 10
⊢ (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))) |
39 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
40 | | elfznn 12241 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
42 | 39, 41, 35 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
43 | 37 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ) |
44 | 39, 41, 43 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
45 | 42, 29, 44 | fsumser 14308 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
46 | 45 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
47 | 46 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
48 | 38, 47 | eqtr2d 2645 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) = seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) |
49 | | esumpcvgval.3 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ ) |
50 | 48, 49 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝
) |
51 | 3, 4, 35, 37, 50 | isumrecl 14338 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ) |
52 | | 1zzd 11285 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℤ) |
53 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
54 | | fzssuz 12253 |
. . . . . . . . . . . 12
⊢
(1...𝑛) ⊆
(ℤ≥‘1) |
55 | 54, 3 | sseqtr4i 3601 |
. . . . . . . . . . 11
⊢
(1...𝑛) ⊆
ℕ |
56 | 55 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
57 | 35 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
58 | 37 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ) |
59 | 5 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,)+∞)) |
60 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
61 | 60 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0[,)+∞) → 0
≤ 𝐴) |
62 | 59, 61 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐴) |
63 | 50 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ∈ dom ⇝
) |
64 | 3, 52, 53, 56, 57, 58, 62, 63 | isumless 14416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)𝐴 ≤ Σ𝑘 ∈ ℕ 𝐴) |
65 | 45, 64 | eqbrtrrd 4607 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) |
66 | 65 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) |
67 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)) |
68 | 67 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑠 = Σ𝑘 ∈ ℕ 𝐴 → (∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ↔ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴)) |
69 | 68 | rspcev 3282 |
. . . . . . 7
⊢
((Σ𝑘 ∈
ℕ 𝐴 ∈ ℝ
∧ ∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ Σ𝑘 ∈ ℕ 𝐴) → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠) |
70 | 51, 66, 69 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ∃𝑠 ∈ ℝ ∀𝑛 ∈ ℕ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠) |
71 | 3, 4, 16, 32, 70 | climsup 14248 |
. . . . 5
⊢ (𝜑 → seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⇝ sup(ran seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)), ℝ, <
)) |
72 | 3, 4, 71, 24 | climrecl 14162 |
. . . 4
⊢ (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈
ℝ) |
73 | 72 | rexrd 9968 |
. . 3
⊢ (𝜑 → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈
ℝ*) |
74 | | eqid 2610 |
. . . . . . 7
⊢ (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴) = (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴) |
75 | | sumex 14266 |
. . . . . . 7
⊢
Σ𝑘 ∈
𝑏 𝐴 ∈ V |
76 | 74, 75 | elrnmpti 5297 |
. . . . . 6
⊢ (𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘 ∈ 𝑏 𝐴) |
77 | | ssnnssfz 28937 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (𝒫 ℕ ∩
Fin) → ∃𝑚 ∈
ℕ 𝑏 ⊆
(1...𝑚)) |
78 | | fzfid 12634 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ⊆ (1...𝑚)) → (1...𝑚) ∈ Fin) |
79 | | elfznn 12241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...𝑚) → 𝑘 ∈ ℕ) |
80 | 79, 5 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞)) |
81 | 60 | simplbi 475 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (0[,)+∞) →
𝐴 ∈
ℝ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ) |
83 | 82 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ) |
84 | 80, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴) |
85 | 84 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ⊆ (1...𝑚)) ∧ 𝑘 ∈ (1...𝑚)) → 0 ≤ 𝐴) |
86 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ⊆ (1...𝑚)) → 𝑏 ⊆ (1...𝑚)) |
87 | 78, 83, 85, 86 | fsumless 14369 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ⊆ (1...𝑚)) → Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
88 | 87 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ⊆ (1...𝑚) → Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
89 | 88 | reximdv 2999 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚) → ∃𝑚 ∈ ℕ Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
90 | 89 | imp 444 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ 𝑏 ⊆ (1...𝑚)) → ∃𝑚 ∈ ℕ Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
91 | 77, 90 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
∃𝑚 ∈ ℕ
Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
92 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑥 = Σ𝑘 ∈ 𝑏 𝐴 → (𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
93 | 92 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑥 = Σ𝑘 ∈ 𝑏 𝐴 → (∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴 ↔ ∃𝑚 ∈ ℕ Σ𝑘 ∈ 𝑏 𝐴 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
94 | 91, 93 | syl5ibrcom 236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
(𝑥 = Σ𝑘 ∈ 𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
95 | 94 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝜑 → (∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘 ∈ 𝑏 𝐴 → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) |
96 | 95 | imp 444 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘 ∈ 𝑏 𝐴) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
97 | 76, 96 | sylan2b 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → ∃𝑚 ∈ ℕ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
98 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑥 = Σ𝑘 ∈ 𝑏 𝐴) → 𝑥 = Σ𝑘 ∈ 𝑏 𝐴) |
99 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢
(𝒫 ℕ ∩ Fin) ⊆ Fin |
100 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
𝑏 ∈ (𝒫 ℕ
∩ Fin)) |
101 | 99, 100 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
𝑏 ∈
Fin) |
102 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝜑) |
103 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
104 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝑏 ∈ (𝒫 ℕ ∩
Fin)) |
105 | 103, 104 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝑏 ∈ 𝒫 ℕ) |
106 | 105 | elpwid 4118 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝑏 ⊆ ℕ) |
107 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝑘 ∈ 𝑏) |
108 | 106, 107 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝑘 ∈ ℕ) |
109 | 102, 108,
5 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝐴 ∈ (0[,)+∞)) |
110 | 109, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝐴 ∈ ℝ) |
111 | 101, 110 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
Σ𝑘 ∈ 𝑏 𝐴 ∈ ℝ) |
112 | 111 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑥 = Σ𝑘 ∈ 𝑏 𝐴) → Σ𝑘 ∈ 𝑏 𝐴 ∈ ℝ) |
113 | 98, 112 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑥 = Σ𝑘 ∈ 𝑏 𝐴) → 𝑥 ∈ ℝ) |
114 | 113 | r19.29an 3059 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑥 = Σ𝑘 ∈ 𝑏 𝐴) → 𝑥 ∈ ℝ) |
115 | 76, 114 | sylan2b 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → 𝑥 ∈ ℝ) |
116 | 115 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ∈ ℝ) |
117 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑚) ∈ Fin) |
118 | 117, 82 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ) |
119 | 118 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ℝ) |
120 | 72 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈
ℝ) |
121 | | simprr 792 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴) |
122 | | frn 5966 |
. . . . . . . . 9
⊢ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵)):ℕ⟶ℝ
→ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
⊆ ℝ) |
123 | 16, 122 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆
ℝ) |
124 | 123 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ℝ) |
125 | | 1nn 10908 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
126 | 125 | ne0ii 3882 |
. . . . . . . . 9
⊢ ℕ
≠ ∅ |
127 | | dm0rn0 5263 |
. . . . . . . . . . 11
⊢ (dom
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) = ∅
↔ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
= ∅) |
128 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵)):ℕ⟶ℝ
→ dom seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
= ℕ) |
129 | 16, 128 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ℕ) |
130 | 129 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝜑 → (dom seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ =
∅)) |
131 | 127, 130 | syl5bbr 273 |
. . . . . . . . . 10
⊢ (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) = ∅ ↔ ℕ =
∅)) |
132 | 131 | necon3bid 2826 |
. . . . . . . . 9
⊢ (𝜑 → (ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ↔ ℕ
≠ ∅)) |
133 | 126, 132 | mpbiri 247 |
. . . . . . . 8
⊢ (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠
∅) |
134 | 133 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅) |
135 | | 1z 11284 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
136 | | seqfn 12675 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ → seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
Fn (ℤ≥‘1)) |
137 | 135, 136 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)) Fn
(ℤ≥‘1) |
138 | 3 | fneq2i 5900 |
. . . . . . . . . . . . . . 15
⊢ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵)) Fn ℕ ↔ seq1(
+ , (𝑙 ∈ ℕ
↦ 𝐵)) Fn
(ℤ≥‘1)) |
139 | 137, 138 | mpbir 220 |
. . . . . . . . . . . . . 14
⊢ seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)) Fn
ℕ |
140 | | dffn5 6151 |
. . . . . . . . . . . . . 14
⊢ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵)) Fn ℕ ↔ seq1(
+ , (𝑙 ∈ ℕ
↦ 𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵))‘𝑛))) |
141 | 139, 140 | mpbi 219 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
142 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑙 ∈ ℕ ↦
𝐵))‘𝑛) ∈ V |
143 | 141, 142 | elrnmpti 5297 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
144 | | r19.29 3054 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑛 ∈ ℕ ((seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛))) |
145 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → (𝑧 ≤ 𝑠 ↔ (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠)) |
146 | 145 | biimparc 503 |
. . . . . . . . . . . . . 14
⊢ (((seq1(
+ , (𝑙 ∈ ℕ
↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧 ≤ 𝑠) |
147 | 146 | rexlimivw 3011 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕ ((seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧 ≤ 𝑠) |
148 | 144, 147 | syl 17 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ ∃𝑛 ∈ ℕ 𝑧 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑧 ≤ 𝑠) |
149 | 143, 148 | sylan2b 491 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 ∧ 𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → 𝑧 ≤ 𝑠) |
150 | 149 | ralrimiva 2949 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) |
151 | 150 | reximi 2994 |
. . . . . . . . 9
⊢
(∃𝑠 ∈
ℝ ∀𝑛 ∈
ℕ (seq1( + , (𝑙
∈ ℕ ↦ 𝐵))‘𝑛) ≤ 𝑠 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) |
152 | 70, 151 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) |
153 | 152 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) |
154 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
155 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝜑) |
156 | 79 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝑘 ∈ ℕ) |
157 | 155, 156,
35 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → ((𝑙 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
158 | 154, 3 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
(ℤ≥‘1)) |
159 | 155, 156,
5 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ (0[,)+∞)) |
160 | 159, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℝ) |
161 | 160 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑚)) → 𝐴 ∈ ℂ) |
162 | 157, 158,
161 | fsumser 14308 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) |
163 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) |
164 | 163 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) ↔ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚))) |
165 | 164 | rspcev 3282 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧
Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑚)) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
166 | 154, 162,
165 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
167 | 141, 142 | elrnmpti 5297 |
. . . . . . . . 9
⊢
(Σ𝑘 ∈
(1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ Σ𝑘 ∈ (1...𝑚)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
168 | 166, 167 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) |
169 | 168 | ad2ant2r 779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) |
170 | | suprub 10863 |
. . . . . . 7
⊢ (((ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ⊆ ℝ
∧ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
≠ ∅ ∧ ∃𝑠
∈ ℝ ∀𝑧
∈ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) ∧ Σ𝑘 ∈ (1...𝑚)𝐴 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
171 | 124, 134,
153, 169, 170 | syl31anc 1321 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → Σ𝑘 ∈ (1...𝑚)𝐴 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
172 | 116, 119,
120, 121, 171 | letrd 10073 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) ∧ (𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ𝑘 ∈ (1...𝑚)𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
173 | 97, 172 | rexlimddv 3017 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → 𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
174 | 72 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ∈
ℝ) |
175 | 115, 174 | lenltd 10062 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → (𝑥 ≤ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬ sup(ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)), ℝ, <
) < 𝑥)) |
176 | 173, 175 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)) → ¬ sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) < 𝑥) |
177 | | simpr1r 1112 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0
≤ 𝑥 ∧ 𝑥 = +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, <
)) |
178 | 177 | 3anassrs 1282 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, <
)) |
179 | 73 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → sup(ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)), ℝ, <
) ∈ ℝ*) |
180 | | pnfnlt 11838 |
. . . . . . . 8
⊢ (sup(ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)), ℝ, <
) ∈ ℝ* → ¬ +∞ < sup(ran seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)), ℝ, <
)) |
181 | 179, 180 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → ¬
+∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
182 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑥 = +∞ → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔
+∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) |
183 | 182 | notbid 307 |
. . . . . . . 8
⊢ (𝑥 = +∞ → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬
+∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) |
184 | 183 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → (¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ¬
+∞ < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) |
185 | 181, 184 | mpbird 246 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → ¬ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, <
)) |
186 | 178, 185 | pm2.21dd 185 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 = +∞) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦) |
187 | | simplll 794 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 𝜑) |
188 | | simpr1l 1111 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0
≤ 𝑥 ∧ 𝑥 < +∞)) → 𝑥 ∈
ℝ*) |
189 | 188 | 3anassrs 1282 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈
ℝ*) |
190 | | simplr 788 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 0 ≤
𝑥) |
191 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < +∞) |
192 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
193 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
194 | | elico1 12089 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑥 ∈ (0[,)+∞)
↔ (𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞))) |
195 | 192, 193,
194 | mp2an 704 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞)) |
196 | 189, 190,
191, 195 | syl3anbrc 1239 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 ∈
(0[,)+∞)) |
197 | | simpr1r 1112 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) ∧ 0
≤ 𝑥 ∧ 𝑥 < +∞)) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, <
)) |
198 | 197 | 3anassrs 1282 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) → 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, <
)) |
199 | 123 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ⊆
ℝ) |
200 | 133 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ≠
∅) |
201 | 152 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
∃𝑠 ∈ ℝ
∀𝑧 ∈ ran seq1(
+ , (𝑙 ∈ ℕ
↦ 𝐵))𝑧 ≤ 𝑠) |
202 | 199, 200,
201 | 3jca 1235 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
(ran seq1( + , (𝑙 ∈
ℕ ↦ 𝐵)) ⊆
ℝ ∧ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ≠ ∅ ∧ ∃𝑠 ∈ ℝ ∀𝑧 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠)) |
203 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
𝑥 ∈
(0[,)+∞)) |
204 | 36, 203 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
𝑥 ∈
ℝ) |
205 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
𝑥 < sup(ran seq1( + ,
(𝑙 ∈ ℕ ↦
𝐵)), ℝ, <
)) |
206 | | suprlub 10864 |
. . . . . . . . 9
⊢ (((ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ⊆ ℝ
∧ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
≠ ∅ ∧ ∃𝑠
∈ ℝ ∀𝑧
∈ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦)) |
207 | 206 | biimpa 500 |
. . . . . . . 8
⊢ ((((ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ⊆ ℝ
∧ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))
≠ ∅ ∧ ∃𝑠
∈ ℝ ∀𝑧
∈ ran seq1( + , (𝑙
∈ ℕ ↦ 𝐵))𝑧 ≤ 𝑠) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) → ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦) |
208 | 202, 204,
205, 207 | syl21anc 1317 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
∃𝑦 ∈ ran seq1( +
, (𝑙 ∈ ℕ ↦
𝐵))𝑥 < 𝑦) |
209 | 40 | ssriv 3572 |
. . . . . . . . . . . . . . . . 17
⊢
(1...𝑛) ⊆
ℕ |
210 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑛) ∈
V |
211 | 210 | elpw 4114 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑛) ∈
𝒫 ℕ ↔ (1...𝑛) ⊆ ℕ) |
212 | 209, 211 | mpbir 220 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑛) ∈
𝒫 ℕ |
213 | | fzfi 12633 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑛) ∈
Fin |
214 | | elin 3758 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑛) ∈
(𝒫 ℕ ∩ Fin) ↔ ((1...𝑛) ∈ 𝒫 ℕ ∧ (1...𝑛) ∈ Fin)) |
215 | 212, 213,
214 | mpbir2an 957 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ∈
(𝒫 ℕ ∩ Fin) |
216 | 215 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → (1...𝑛) ∈ (𝒫 ℕ ∩
Fin)) |
217 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
218 | 45 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
219 | 217, 218 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴) |
220 | | sumeq1 14267 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (1...𝑛) → Σ𝑘 ∈ 𝑏 𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴) |
221 | 220 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (1...𝑛) → (𝑦 = Σ𝑘 ∈ 𝑏 𝐴 ↔ 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴)) |
222 | 221 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑛) ∈
(𝒫 ℕ ∩ Fin) ∧ 𝑦 = Σ𝑘 ∈ (1...𝑛)𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑏 𝐴) |
223 | 216, 219,
222 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑏 𝐴) |
224 | 223 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑏 𝐴)) |
225 | 224 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑏 𝐴)) |
226 | 141, 142 | elrnmpti 5297 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ↔ ∃𝑛 ∈ ℕ 𝑦 = (seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))‘𝑛)) |
227 | 74, 75 | elrnmpti 5297 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)𝑦 = Σ𝑘 ∈ 𝑏 𝐴) |
228 | 225, 226,
227 | 3imtr4g 284 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) → 𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴))) |
229 | 228 | ssrdv 3574 |
. . . . . . . . 9
⊢ (𝜑 → ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)) ⊆ ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴)) |
230 | | ssrexv 3630 |
. . . . . . . . 9
⊢ (ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)) ⊆ ran
(𝑏 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑏 𝐴) → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦)) |
231 | 229, 230 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦)) |
232 | 231 | imp 444 |
. . . . . . 7
⊢ ((𝜑 ∧ ∃𝑦 ∈ ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵))𝑥 < 𝑦) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦) |
233 | 208, 232 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴)𝑥 < 𝑦) |
234 | 187, 196,
198, 233 | syl12anc 1316 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) ∧ 𝑥 < +∞) →
∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴)𝑥 < 𝑦) |
235 | | simplrl 796 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) → 𝑥 ∈
ℝ*) |
236 | | xrlelttric 28906 |
. . . . . . . 8
⊢
((+∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (+∞
≤ 𝑥 ∨ 𝑥 <
+∞)) |
237 | 193, 236 | mpan 702 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ*
→ (+∞ ≤ 𝑥
∨ 𝑥 <
+∞)) |
238 | | xgepnf 28904 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
→ (+∞ ≤ 𝑥
↔ 𝑥 =
+∞)) |
239 | 238 | orbi1d 735 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ*
→ ((+∞ ≤ 𝑥
∨ 𝑥 < +∞)
↔ (𝑥 = +∞ ∨
𝑥 <
+∞))) |
240 | 237, 239 | mpbid 221 |
. . . . . 6
⊢ (𝑥 ∈ ℝ*
→ (𝑥 = +∞ ∨
𝑥 <
+∞)) |
241 | 235, 240 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) → (𝑥 = +∞ ∨ 𝑥 <
+∞)) |
242 | 186, 234,
241 | mpjaodan 823 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧ 0
≤ 𝑥) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦) |
243 | | 0elpw 4760 |
. . . . . . . . 9
⊢ ∅
∈ 𝒫 ℕ |
244 | | 0fin 8073 |
. . . . . . . . 9
⊢ ∅
∈ Fin |
245 | | elin 3758 |
. . . . . . . . 9
⊢ (∅
∈ (𝒫 ℕ ∩ Fin) ↔ (∅ ∈ 𝒫 ℕ
∧ ∅ ∈ Fin)) |
246 | 243, 244,
245 | mpbir2an 957 |
. . . . . . . 8
⊢ ∅
∈ (𝒫 ℕ ∩ Fin) |
247 | | sum0 14299 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
∅ 𝐴 =
0 |
248 | 247 | eqcomi 2619 |
. . . . . . . 8
⊢ 0 =
Σ𝑘 ∈ ∅
𝐴 |
249 | | sumeq1 14267 |
. . . . . . . . . 10
⊢ (𝑏 = ∅ → Σ𝑘 ∈ 𝑏 𝐴 = Σ𝑘 ∈ ∅ 𝐴) |
250 | 249 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑏 = ∅ → (0 =
Σ𝑘 ∈ 𝑏 𝐴 ↔ 0 = Σ𝑘 ∈ ∅ 𝐴)) |
251 | 250 | rspcev 3282 |
. . . . . . . 8
⊢ ((∅
∈ (𝒫 ℕ ∩ Fin) ∧ 0 = Σ𝑘 ∈ ∅ 𝐴) → ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 =
Σ𝑘 ∈ 𝑏 𝐴) |
252 | 246, 248,
251 | mp2an 704 |
. . . . . . 7
⊢
∃𝑏 ∈
(𝒫 ℕ ∩ Fin)0 = Σ𝑘 ∈ 𝑏 𝐴 |
253 | 74, 75 | elrnmpti 5297 |
. . . . . . 7
⊢ (0 ∈
ran (𝑏 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑏 𝐴) ↔ ∃𝑏 ∈ (𝒫 ℕ ∩ Fin)0 =
Σ𝑘 ∈ 𝑏 𝐴) |
254 | 252, 253 | mpbir 220 |
. . . . . 6
⊢ 0 ∈
ran (𝑏 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑏 𝐴) |
255 | | breq2 4587 |
. . . . . . 7
⊢ (𝑦 = 0 → (𝑥 < 𝑦 ↔ 𝑥 < 0)) |
256 | 255 | rspcev 3282 |
. . . . . 6
⊢ ((0
∈ ran (𝑏 ∈
(𝒫 ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑏 𝐴) ∧ 𝑥 < 0) → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦) |
257 | 254, 256 | mpan 702 |
. . . . 5
⊢ (𝑥 < 0 → ∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴)𝑥 < 𝑦) |
258 | 257 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) ∧
𝑥 < 0) →
∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴)𝑥 < 𝑦) |
259 | | xrlelttric 28906 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝑥 ∈ ℝ*) → (0 ≤
𝑥 ∨ 𝑥 < 0)) |
260 | 192, 259 | mpan 702 |
. . . . 5
⊢ (𝑥 ∈ ℝ*
→ (0 ≤ 𝑥 ∨ 𝑥 < 0)) |
261 | 260 | ad2antrl 760 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) → (0
≤ 𝑥 ∨ 𝑥 < 0)) |
262 | 242, 258,
261 | mpjaodan 823 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < ))) →
∃𝑦 ∈ ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴)𝑥 < 𝑦) |
263 | 2, 73, 176, 262 | eqsupd 8246 |
. 2
⊢ (𝜑 → sup(ran (𝑏 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑏 𝐴), ℝ*, < ) = sup(ran
seq1( + , (𝑙 ∈ ℕ
↦ 𝐵)), ℝ, <
)) |
264 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑘𝜑 |
265 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑘ℕ |
266 | | nnex 10903 |
. . . 4
⊢ ℕ
∈ V |
267 | 266 | a1i 11 |
. . 3
⊢ (𝜑 → ℕ ∈
V) |
268 | | icossicc 12131 |
. . . 4
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
269 | 268, 5 | sseldi 3566 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
270 | | elex 3185 |
. . . . . 6
⊢ (𝑏 ∈ (𝒫 ℕ ∩
Fin) → 𝑏 ∈
V) |
271 | 270 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
𝑏 ∈
V) |
272 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ 𝑏 ↦ 𝐴) = (𝑘 ∈ 𝑏 ↦ 𝐴) |
273 | 109, 272 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
(𝑘 ∈ 𝑏 ↦ 𝐴):𝑏⟶(0[,)+∞)) |
274 | | esumpfinvallem 29463 |
. . . . 5
⊢ ((𝑏 ∈ V ∧ (𝑘 ∈ 𝑏 ↦ 𝐴):𝑏⟶(0[,)+∞)) →
(ℂfld Σg (𝑘 ∈ 𝑏 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑏 ↦ 𝐴))) |
275 | 271, 273,
274 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
(ℂfld Σg (𝑘 ∈ 𝑏 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑏 ↦ 𝐴))) |
276 | 110 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) ∧
𝑘 ∈ 𝑏) → 𝐴 ∈ ℂ) |
277 | 101, 276 | gsumfsum 19632 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
(ℂfld Σg (𝑘 ∈ 𝑏 ↦ 𝐴)) = Σ𝑘 ∈ 𝑏 𝐴) |
278 | 275, 277 | eqtr3d 2646 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (𝒫 ℕ ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑏 ↦ 𝐴)) = Σ𝑘 ∈ 𝑏 𝐴) |
279 | 264, 265,
267, 269, 278 | esumval 29435 |
. 2
⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = sup(ran (𝑏 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑏 𝐴), ℝ*, <
)) |
280 | 3, 4, 35, 43, 71 | isumclim 14330 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ ℕ 𝐴 = sup(ran seq1( + , (𝑙 ∈ ℕ ↦ 𝐵)), ℝ, < )) |
281 | 263, 279,
280 | 3eqtr4d 2654 |
1
⊢ (𝜑 → Σ*𝑘 ∈ ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) |