Step |
Hyp |
Ref |
Expression |
1 |
|
esumpcvgval.1 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) ) |
2 |
|
esumpcvgval.2 |
⊢ ( 𝑘 = 𝑙 → 𝐴 = 𝐵 ) |
3 |
|
esumpcvgval.3 |
⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ ) |
4 |
|
xrltso |
⊢ < Or ℝ* |
5 |
4
|
a1i |
⊢ ( 𝜑 → < Or ℝ* ) |
6 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
7 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
8 |
|
eqcom |
⊢ ( 𝑘 = 𝑙 ↔ 𝑙 = 𝑘 ) |
9 |
|
eqcom |
⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 ) |
10 |
2 8 9
|
3imtr3i |
⊢ ( 𝑙 = 𝑘 → 𝐵 = 𝐴 ) |
11 |
10
|
cbvmptv |
⊢ ( 𝑙 ∈ ℕ ↦ 𝐵 ) = ( 𝑘 ∈ ℕ ↦ 𝐴 ) |
12 |
1 11
|
fmptd |
⊢ ( 𝜑 → ( 𝑙 ∈ ℕ ↦ 𝐵 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
13 |
12
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ) |
14 |
|
elrege0 |
⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ) ) |
15 |
14
|
simplbi |
⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ) |
16 |
13 15
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ) |
17 |
6 7 16
|
serfre |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) : ℕ ⟶ ℝ ) |
18 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ ℕ ↦ 𝐵 ) : ℕ ⟶ ( 0 [,) +∞ ) ) |
19 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
20 |
19
|
peano2nnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ ) |
21 |
18 20
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) ) |
22 |
|
elrege0 |
⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) |
23 |
22
|
simprbi |
⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) |
24 |
21 23
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) |
25 |
17
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ∈ ℝ ) |
26 |
22
|
simplbi |
⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) |
27 |
21 26
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) |
28 |
25 27
|
addge01d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ↔ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) ) |
29 |
24 28
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) |
30 |
19 6
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) ) |
31 |
|
seqp1 |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) |
32 |
30 31
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) |
33 |
29 32
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) ) |
34 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ ) |
35 |
11
|
fvmpt2 |
⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 ) |
36 |
34 1 35
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 ) |
37 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
38 |
37 1
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ ) |
39 |
17
|
feqmptd |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) ) |
40 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 ) |
41 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ ) |
42 |
41
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ ) |
43 |
40 42 36
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 ) |
44 |
38
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ ) |
45 |
40 42 44
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ℂ ) |
46 |
43 30 45
|
fsumser |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
47 |
46
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) |
48 |
47
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) |
49 |
39 48
|
eqtr2d |
⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) |
50 |
49 3
|
eqeltrrd |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ∈ dom ⇝ ) |
51 |
6 7 36 38 50
|
isumrecl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ ) |
52 |
|
1zzd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℤ ) |
53 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin ) |
54 |
|
fzssuz |
⊢ ( 1 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 1 ) |
55 |
54 6
|
sseqtrri |
⊢ ( 1 ... 𝑛 ) ⊆ ℕ |
56 |
55
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ ) |
57 |
36
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 ) |
58 |
38
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ ) |
59 |
1
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) ) |
60 |
|
elrege0 |
⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) |
61 |
60
|
simprbi |
⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝐴 ) |
62 |
59 61
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ 𝐴 ) |
63 |
50
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ∈ dom ⇝ ) |
64 |
6 52 53 56 57 58 62 63
|
isumless |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ Σ 𝑘 ∈ ℕ 𝐴 ) |
65 |
46 64
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 ) |
66 |
65
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 ) |
67 |
|
brralrspcev |
⊢ ( ( Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 ) → ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ) |
68 |
51 66 67
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ) |
69 |
6 7 17 33 68
|
climsup |
⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⇝ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
70 |
6 7 69 25
|
climrecl |
⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ ) |
71 |
70
|
rexrd |
⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* ) |
72 |
|
eqid |
⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) |
73 |
|
sumex |
⊢ Σ 𝑘 ∈ 𝑏 𝐴 ∈ V |
74 |
72 73
|
elrnmpti |
⊢ ( 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
75 |
|
ssnnssfz |
⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) → ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) ) |
76 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → ( 1 ... 𝑚 ) ∈ Fin ) |
77 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... 𝑚 ) → 𝑘 ∈ ℕ ) |
78 |
77 1
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) ) |
79 |
60
|
simplbi |
⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) → 𝐴 ∈ ℝ ) |
80 |
78 79
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ ) |
81 |
80
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ ) |
82 |
78 61
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 0 ≤ 𝐴 ) |
83 |
82
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 0 ≤ 𝐴 ) |
84 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → 𝑏 ⊆ ( 1 ... 𝑚 ) ) |
85 |
76 81 83 84
|
fsumless |
⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
86 |
85
|
ex |
⊢ ( 𝜑 → ( 𝑏 ⊆ ( 1 ... 𝑚 ) → Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
87 |
86
|
reximdv |
⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
88 |
87
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
89 |
75 88
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
90 |
|
breq1 |
⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ( 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ↔ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
91 |
90
|
rexbidv |
⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ( ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ↔ ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
92 |
89 91
|
syl5ibrcom |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
93 |
92
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) |
94 |
93
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
95 |
74 94
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
96 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
97 |
|
inss2 |
⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ Fin |
98 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) |
99 |
97 98
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ Fin ) |
100 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝜑 ) |
101 |
|
inss1 |
⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ 𝒫 ℕ |
102 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) |
103 |
101 102
|
sseldi |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ∈ 𝒫 ℕ ) |
104 |
103
|
elpwid |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ⊆ ℕ ) |
105 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ 𝑏 ) |
106 |
104 105
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ ℕ ) |
107 |
100 106 1
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ( 0 [,) +∞ ) ) |
108 |
107 79
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ℝ ) |
109 |
99 108
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → Σ 𝑘 ∈ 𝑏 𝐴 ∈ ℝ ) |
110 |
109
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → Σ 𝑘 ∈ 𝑏 𝐴 ∈ ℝ ) |
111 |
96 110
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 ∈ ℝ ) |
112 |
111
|
r19.29an |
⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 ∈ ℝ ) |
113 |
74 112
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → 𝑥 ∈ ℝ ) |
114 |
113
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ∈ ℝ ) |
115 |
|
fzfid |
⊢ ( 𝜑 → ( 1 ... 𝑚 ) ∈ Fin ) |
116 |
115 80
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ℝ ) |
117 |
116
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ℝ ) |
118 |
70
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ ) |
119 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) |
120 |
17
|
frnd |
⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ) |
121 |
120
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ) |
122 |
|
1nn |
⊢ 1 ∈ ℕ |
123 |
122
|
ne0ii |
⊢ ℕ ≠ ∅ |
124 |
|
dm0rn0 |
⊢ ( dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ) |
125 |
17
|
fdmd |
⊢ ( 𝜑 → dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ℕ ) |
126 |
125
|
eqeq1d |
⊢ ( 𝜑 → ( dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ℕ = ∅ ) ) |
127 |
124 126
|
bitr3id |
⊢ ( 𝜑 → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ℕ = ∅ ) ) |
128 |
127
|
necon3bid |
⊢ ( 𝜑 → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ↔ ℕ ≠ ∅ ) ) |
129 |
123 128
|
mpbiri |
⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ) |
130 |
129
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ) |
131 |
|
1z |
⊢ 1 ∈ ℤ |
132 |
|
seqfn |
⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) ) |
133 |
131 132
|
ax-mp |
⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) |
134 |
6
|
fneq2i |
⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) ) |
135 |
133 134
|
mpbir |
⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ |
136 |
|
dffn5 |
⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) ) |
137 |
135 136
|
mpbi |
⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
138 |
|
fvex |
⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ∈ V |
139 |
137 138
|
elrnmpti |
⊢ ( 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
140 |
|
r19.29 |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) ) |
141 |
|
breq1 |
⊢ ( 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ( 𝑧 ≤ 𝑠 ↔ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ) ) |
142 |
141
|
biimparc |
⊢ ( ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 ) |
143 |
142
|
rexlimivw |
⊢ ( ∃ 𝑛 ∈ ℕ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 ) |
144 |
140 143
|
syl |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 ) |
145 |
139 144
|
sylan2b |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) → 𝑧 ≤ 𝑠 ) |
146 |
145
|
ralrimiva |
⊢ ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 → ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) |
147 |
146
|
reximi |
⊢ ( ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) |
148 |
68 147
|
syl |
⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) |
149 |
148
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) |
150 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ ) |
151 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝜑 ) |
152 |
77
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝑘 ∈ ℕ ) |
153 |
151 152 36
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 ) |
154 |
150 6
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) ) |
155 |
151 152 1
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) ) |
156 |
155 79
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ ) |
157 |
156
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℂ ) |
158 |
153 154 157
|
fsumser |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) ) |
159 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) ) |
160 |
159
|
rspceeqv |
⊢ ( ( 𝑚 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
161 |
150 158 160
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
162 |
137 138
|
elrnmpti |
⊢ ( Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
163 |
161 162
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) |
164 |
163
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) |
165 |
|
suprub |
⊢ ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
166 |
121 130 149 164 165
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
167 |
114 117 118 119 166
|
letrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
168 |
95 167
|
rexlimddv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
169 |
70
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ ) |
170 |
113 169
|
lenltd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ( 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) < 𝑥 ) ) |
171 |
168 170
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ¬ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) < 𝑥 ) |
172 |
|
simpr1r |
⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 = +∞ ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
173 |
172
|
3anassrs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
174 |
71
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* ) |
175 |
|
pnfnlt |
⊢ ( sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* → ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
176 |
174 175
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
177 |
|
breq1 |
⊢ ( 𝑥 = +∞ → ( 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) |
178 |
177
|
notbid |
⊢ ( 𝑥 = +∞ → ( ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) |
179 |
178
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ( ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) |
180 |
176 179
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
181 |
173 180
|
pm2.21dd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
182 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝜑 ) |
183 |
|
simpr1l |
⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) → 𝑥 ∈ ℝ* ) |
184 |
183
|
3anassrs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 ∈ ℝ* ) |
185 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 0 ≤ 𝑥 ) |
186 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 < +∞ ) |
187 |
|
0xr |
⊢ 0 ∈ ℝ* |
188 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
189 |
|
elico1 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) |
190 |
187 188 189
|
mp2an |
⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) |
191 |
184 185 186 190
|
syl3anbrc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 ∈ ( 0 [,) +∞ ) ) |
192 |
|
simpr1r |
⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
193 |
192
|
3anassrs |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
194 |
120
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ) |
195 |
129
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ) |
196 |
148
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) |
197 |
194 195 196
|
3jca |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ) |
198 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 ∈ ( 0 [,) +∞ ) ) |
199 |
37 198
|
sseldi |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 ∈ ℝ ) |
200 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
201 |
|
suprlub |
⊢ ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) ) |
202 |
201
|
biimpa |
⊢ ( ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) → ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) |
203 |
197 199 200 202
|
syl21anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) |
204 |
41
|
ssriv |
⊢ ( 1 ... 𝑛 ) ⊆ ℕ |
205 |
|
ovex |
⊢ ( 1 ... 𝑛 ) ∈ V |
206 |
205
|
elpw |
⊢ ( ( 1 ... 𝑛 ) ∈ 𝒫 ℕ ↔ ( 1 ... 𝑛 ) ⊆ ℕ ) |
207 |
204 206
|
mpbir |
⊢ ( 1 ... 𝑛 ) ∈ 𝒫 ℕ |
208 |
|
fzfi |
⊢ ( 1 ... 𝑛 ) ∈ Fin |
209 |
|
elin |
⊢ ( ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( ( 1 ... 𝑛 ) ∈ 𝒫 ℕ ∧ ( 1 ... 𝑛 ) ∈ Fin ) ) |
210 |
207 208 209
|
mpbir2an |
⊢ ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) |
211 |
210
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) ) |
212 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
213 |
46
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
214 |
212 213
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑦 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) |
215 |
|
sumeq1 |
⊢ ( 𝑏 = ( 1 ... 𝑛 ) → Σ 𝑘 ∈ 𝑏 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) |
216 |
215
|
rspceeqv |
⊢ ( ( ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
217 |
211 214 216
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
218 |
217
|
ex |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) ) |
219 |
218
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) ) |
220 |
137 138
|
elrnmpti |
⊢ ( 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) |
221 |
72 73
|
elrnmpti |
⊢ ( 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
222 |
219 220 221
|
3imtr4g |
⊢ ( 𝜑 → ( 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) → 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ) |
223 |
222
|
ssrdv |
⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) |
224 |
|
ssrexv |
⊢ ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) → ( ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) ) |
225 |
223 224
|
syl |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) ) |
226 |
225
|
imp |
⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
227 |
203 226
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
228 |
182 191 193 227
|
syl12anc |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
229 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ* ) |
230 |
|
xrlelttric |
⊢ ( ( +∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) ) |
231 |
188 230
|
mpan |
⊢ ( 𝑥 ∈ ℝ* → ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) ) |
232 |
|
xgepnf |
⊢ ( 𝑥 ∈ ℝ* → ( +∞ ≤ 𝑥 ↔ 𝑥 = +∞ ) ) |
233 |
232
|
orbi1d |
⊢ ( 𝑥 ∈ ℝ* → ( ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) ↔ ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) ) ) |
234 |
231 233
|
mpbid |
⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) ) |
235 |
229 234
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) ) |
236 |
181 228 235
|
mpjaodan |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
237 |
|
0elpw |
⊢ ∅ ∈ 𝒫 ℕ |
238 |
|
0fin |
⊢ ∅ ∈ Fin |
239 |
|
elin |
⊢ ( ∅ ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( ∅ ∈ 𝒫 ℕ ∧ ∅ ∈ Fin ) ) |
240 |
237 238 239
|
mpbir2an |
⊢ ∅ ∈ ( 𝒫 ℕ ∩ Fin ) |
241 |
|
sum0 |
⊢ Σ 𝑘 ∈ ∅ 𝐴 = 0 |
242 |
241
|
eqcomi |
⊢ 0 = Σ 𝑘 ∈ ∅ 𝐴 |
243 |
|
sumeq1 |
⊢ ( 𝑏 = ∅ → Σ 𝑘 ∈ 𝑏 𝐴 = Σ 𝑘 ∈ ∅ 𝐴 ) |
244 |
243
|
rspceeqv |
⊢ ( ( ∅ ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 0 = Σ 𝑘 ∈ ∅ 𝐴 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
245 |
240 242 244
|
mp2an |
⊢ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴 |
246 |
72 73
|
elrnmpti |
⊢ ( 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴 ) |
247 |
245 246
|
mpbir |
⊢ 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) |
248 |
|
breq2 |
⊢ ( 𝑦 = 0 → ( 𝑥 < 𝑦 ↔ 𝑥 < 0 ) ) |
249 |
248
|
rspcev |
⊢ ( ( 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ∧ 𝑥 < 0 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
250 |
247 249
|
mpan |
⊢ ( 𝑥 < 0 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
251 |
250
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 𝑥 < 0 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
252 |
|
xrlelttric |
⊢ ( ( 0 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) ) |
253 |
187 252
|
mpan |
⊢ ( 𝑥 ∈ ℝ* → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) ) |
254 |
253
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) ) |
255 |
236 251 254
|
mpjaodan |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) |
256 |
5 71 171 255
|
eqsupd |
⊢ ( 𝜑 → sup ( ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
257 |
|
nfv |
⊢ Ⅎ 𝑘 𝜑 |
258 |
|
nfcv |
⊢ Ⅎ 𝑘 ℕ |
259 |
|
nnex |
⊢ ℕ ∈ V |
260 |
259
|
a1i |
⊢ ( 𝜑 → ℕ ∈ V ) |
261 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
262 |
261 1
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) ) |
263 |
|
elex |
⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝑏 ∈ V ) |
264 |
263
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ V ) |
265 |
107
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) : 𝑏 ⟶ ( 0 [,) +∞ ) ) |
266 |
|
esumpfinvallem |
⊢ ( ( 𝑏 ∈ V ∧ ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) : 𝑏 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) ) |
267 |
264 265 266
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) ) |
268 |
108
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ℂ ) |
269 |
99 268
|
gsumfsum |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑏 𝐴 ) |
270 |
267 269
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑏 𝐴 ) |
271 |
257 258 260 262 270
|
esumval |
⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) , ℝ* , < ) ) |
272 |
6 7 36 44 69
|
isumclim |
⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐴 = sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) |
273 |
256 271 272
|
3eqtr4d |
⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 ) |