Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → 1 ∈
ℤ) |
3 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
4 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
5 | | climcnds.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
6 | | 2nn 11062 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
7 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
8 | | nnexpcl 12735 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
9 | 6, 7, 8 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ) |
10 | 9 | nnred 10912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℝ) |
11 | | climcnds.1 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
12 | 11 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
14 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛))) |
15 | 14 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ)) |
16 | 15 | rspcv 3278 |
. . . . . . . . . . 11
⊢
((2↑𝑛) ∈
ℕ → (∀𝑘
∈ ℕ (𝐹‘𝑘) ∈ ℝ → (𝐹‘(2↑𝑛)) ∈ ℝ)) |
17 | 9, 13, 16 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈
ℝ) |
18 | 10, 17 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈
ℝ) |
19 | 5, 18 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℝ) |
20 | 4, 19 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
21 | 1, 3, 20 | serfre 12692 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺):ℕ⟶ℝ) |
23 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
24 | 23, 1 | syl6eleq 2698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
25 | | nnz 11276 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
27 | | uzid 11578 |
. . . . . . . 8
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
28 | | peano2uz 11617 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
30 | | simpl 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑) |
31 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...(𝑗 + 1)) → 𝑛 ∈ ℕ) |
32 | 30, 31, 20 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...(𝑗 + 1))) → (𝐺‘𝑛) ∈ ℝ) |
33 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑) |
34 | | elfz1eq 12223 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑛 = (𝑗 + 1)) |
35 | 34 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 = (𝑗 + 1)) |
36 | | nnnn0 11176 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
37 | | peano2nn0 11210 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ0) |
39 | 38 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → (𝑗 + 1) ∈
ℕ0) |
40 | 35, 39 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 ∈ ℕ0) |
41 | 9 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ0) |
42 | 41 | nn0ge0d 11231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(2↑𝑛)) |
43 | | climcnds.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) |
44 | 43 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹‘𝑘)) |
45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ 0
≤ (𝐹‘𝑘)) |
46 | 14 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2↑𝑛) → (0 ≤ (𝐹‘𝑘) ↔ 0 ≤ (𝐹‘(2↑𝑛)))) |
47 | 46 | rspcv 3278 |
. . . . . . . . . . 11
⊢
((2↑𝑛) ∈
ℕ → (∀𝑘
∈ ℕ 0 ≤ (𝐹‘𝑘) → 0 ≤ (𝐹‘(2↑𝑛)))) |
48 | 9, 45, 47 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(𝐹‘(2↑𝑛))) |
49 | 10, 17, 42, 48 | mulge0d 10483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
50 | 49, 5 | breqtrrd 4611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(𝐺‘𝑛)) |
51 | 33, 40, 50 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐺‘𝑛)) |
52 | 24, 29, 32, 51 | sermono 12695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1))) |
53 | 52 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1))) |
54 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
55 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
56 | 11 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
57 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐹) ∈ dom ⇝
) |
58 | 1, 2, 55, 56, 57 | isumrecl 14338 |
. . . . . . 7
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → Σ𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
59 | | remulcl 9900 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) → (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)) ∈ ℝ) |
60 | 54, 58, 59 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)) ∈ ℝ) |
61 | 22 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ∈
ℝ) |
62 | 1, 3, 11 | serfre 12692 |
. . . . . . . . . . 11
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ) |
63 | 62 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹):ℕ⟶ℝ) |
64 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
65 | | nnexpcl 12735 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
66 | 6, 64, 65 | sylancr 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℕ) |
67 | 63, 66 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘(2↑𝑗)) ∈
ℝ) |
68 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1(
+ , 𝐹)‘(2↑𝑗))) ∈
ℝ) |
69 | 54, 67, 68 | sylancr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ) |
70 | 60 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· Σ𝑘 ∈
ℕ (𝐹‘𝑘)) ∈
ℝ) |
71 | | climcnds.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
72 | 11, 43, 71, 5 | climcndslem2 14421 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) |
73 | 72 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (2 · (seq1( + ,
𝐹)‘(2↑𝑗)))) |
74 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
75 | 66, 1 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
(ℤ≥‘1)) |
76 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑) |
77 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ) |
78 | 11 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
79 | 76, 77, 78 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) ∈ ℂ) |
80 | 74, 75, 79 | fsumser 14308 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈
(1...(2↑𝑗))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑𝑗))) |
81 | | 1zzd 11285 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 1 ∈
ℤ) |
82 | | fzfid 12634 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(1...(2↑𝑗)) ∈
Fin) |
83 | 77 | ssriv 3572 |
. . . . . . . . . . . 12
⊢
(1...(2↑𝑗))
⊆ ℕ |
84 | 83 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(1...(2↑𝑗)) ⊆
ℕ) |
85 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
86 | 56 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
87 | 76, 43 | sylan 487 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤
(𝐹‘𝑘)) |
88 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹) ∈ dom ⇝
) |
89 | 1, 81, 82, 84, 85, 86, 87, 88 | isumless 14416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈
(1...(2↑𝑗))(𝐹‘𝑘) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘)) |
90 | 80, 89 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘)) |
91 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
92 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ) |
93 | | 2pos 10989 |
. . . . . . . . . . 11
⊢ 0 <
2 |
94 | 93 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 0 <
2) |
95 | | lemul2 10755 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹)‘(2↑𝑗)) ∈ ℝ ∧
Σ𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → ((seq1( + , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘) ↔ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)))) |
96 | 67, 91, 92, 94, 95 | syl112anc 1322 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((seq1(
+ , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘) ↔ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)))) |
97 | 90, 96 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
98 | 61, 69, 70, 73, 97 | letrd 10073 |
. . . . . . 7
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
99 | 98 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
100 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘)) → ((seq1( + , 𝐺)‘𝑗) ≤ 𝑥 ↔ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘)))) |
101 | 100 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘)) → (∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘)))) |
102 | 101 | rspcev 3282 |
. . . . . 6
⊢ (((2
· Σ𝑘 ∈
ℕ (𝐹‘𝑘)) ∈ ℝ ∧
∀𝑗 ∈ ℕ
(seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥) |
103 | 60, 99, 102 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥) |
104 | 1, 2, 22, 53, 103 | climsup 14248 |
. . . 4
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺) ⇝ sup(ran seq1( +
, 𝐺), ℝ, <
)) |
105 | | climrel 14071 |
. . . . 5
⊢ Rel
⇝ |
106 | 105 | releldmi 5283 |
. . . 4
⊢ (seq1( +
, 𝐺) ⇝ sup(ran seq1(
+ , 𝐺), ℝ, < )
→ seq1( + , 𝐺) ∈
dom ⇝ ) |
107 | 104, 106 | syl 17 |
. . 3
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺) ∈ dom ⇝
) |
108 | | nn0uz 11598 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
109 | | 1nn0 11185 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
110 | 109 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
111 | 19 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℂ) |
112 | 108, 110,
111 | iserex 14235 |
. . . 4
⊢ (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq1( + , 𝐺) ∈ dom
⇝ )) |
113 | 112 | biimpar 501 |
. . 3
⊢ ((𝜑 ∧ seq1( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
114 | 107, 113 | syldan 486 |
. 2
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
115 | | 1zzd 11285 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 1 ∈
ℤ) |
116 | 62 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹):ℕ⟶ℝ) |
117 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(𝑗 + 1)) → 𝑘 ∈ ℕ) |
118 | 30, 117, 11 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℝ) |
119 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑) |
120 | | peano2nn 10909 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
121 | 120 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
122 | | elfz1eq 12223 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑘 = (𝑗 + 1)) |
123 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ)) |
124 | 123 | biimparc 503 |
. . . . . . . 8
⊢ (((𝑗 + 1) ∈ ℕ ∧ 𝑘 = (𝑗 + 1)) → 𝑘 ∈ ℕ) |
125 | 121, 122,
124 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑘 ∈ ℕ) |
126 | 119, 125,
43 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐹‘𝑘)) |
127 | 24, 29, 118, 126 | sermono 12695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1))) |
128 | 127 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1))) |
129 | | 0zd 11266 |
. . . . . 6
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 0 ∈
ℤ) |
130 | | eqidd 2611 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) = (𝐺‘𝑛)) |
131 | 19 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) ∈
ℝ) |
132 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
133 | 108, 129,
130, 131, 132 | isumrecl 14338 |
. . . . 5
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → Σ𝑛 ∈ ℕ0
(𝐺‘𝑛) ∈ ℝ) |
134 | 116 | ffvelrnda 6267 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ∈
ℝ) |
135 | | 0zd 11266 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
136 | 108, 135,
19 | serfre 12692 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ) |
137 | 136 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺):ℕ0⟶ℝ) |
138 | | ffvelrn 6265 |
. . . . . . . 8
⊢ ((seq0( +
, 𝐺):ℕ0⟶ℝ ∧
𝑗 ∈
ℕ0) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ) |
139 | 137, 36, 138 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( +
, 𝐺)‘𝑗) ∈
ℝ) |
140 | 133 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈
ℕ0 (𝐺‘𝑛) ∈ ℝ) |
141 | 116 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹):ℕ⟶ℝ) |
142 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
143 | 25 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
144 | 38 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ0) |
145 | 144 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℝ) |
146 | | nnexpcl 12735 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
147 | 6, 144, 146 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℕ) |
148 | 147 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℝ) |
149 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
150 | | uzid 11578 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(ℤ≥‘2) |
152 | | bernneq3 12854 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝑗 + 1) ∈ ℕ0) →
(𝑗 + 1) < (2↑(𝑗 + 1))) |
153 | 151, 144,
152 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) < (2↑(𝑗 + 1))) |
154 | 145, 148,
153 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≤ (2↑(𝑗 + 1))) |
155 | 143 | peano2zd 11361 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℤ) |
156 | 147 | nnzd 11357 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℤ) |
157 | | eluz 11577 |
. . . . . . . . . . . . 13
⊢ (((𝑗 + 1) ∈ ℤ ∧
(2↑(𝑗 + 1)) ∈
ℤ) → ((2↑(𝑗
+ 1)) ∈ (ℤ≥‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1)))) |
158 | 155, 156,
157 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1)))) |
159 | 154, 158 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1))) |
160 | | eluzp1m1 11587 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧
(2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1))) → ((2↑(𝑗 + 1)) − 1) ∈
(ℤ≥‘𝑗)) |
161 | 143, 159,
160 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘𝑗)) |
162 | | eluznn 11634 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘𝑗)) → ((2↑(𝑗 + 1)) − 1) ∈
ℕ) |
163 | 142, 161,
162 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) −
1) ∈ ℕ) |
164 | 141, 163 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ∈
ℝ) |
165 | 24 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
166 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑) |
167 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈
ℕ) |
168 | 166, 167,
11 | syl2an 493 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℝ) |
169 | 166 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 𝜑) |
170 | 120 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ) |
171 | | elfzuz 12209 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) |
172 | | eluznn 11634 |
. . . . . . . . . . 11
⊢ (((𝑗 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ ℕ) |
173 | 170, 171,
172 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ) |
174 | 169, 173,
43 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 0 ≤ (𝐹‘𝑘)) |
175 | 165, 161,
168, 174 | sermono 12695 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) −
1))) |
176 | 36 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
177 | 11, 43, 71, 5 | climcndslem1 14420 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗)) |
178 | 166, 176,
177 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗)) |
179 | 134, 164,
139, 175, 178 | letrd 10073 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq0( + , 𝐺)‘𝑗)) |
180 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺‘𝑛) = (𝐺‘𝑛)) |
181 | 176, 108 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘0)) |
182 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (0...𝑗) → 𝑛 ∈ ℕ0) |
183 | 166, 182,
111 | syl2an 493 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺‘𝑛) ∈ ℂ) |
184 | 180, 181,
183 | fsumser 14308 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (0...𝑗)(𝐺‘𝑛) = (seq0( + , 𝐺)‘𝑗)) |
185 | | 0zd 11266 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 0 ∈
ℤ) |
186 | | fzfid 12634 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(0...𝑗) ∈
Fin) |
187 | 182 | ssriv 3572 |
. . . . . . . . . 10
⊢
(0...𝑗) ⊆
ℕ0 |
188 | 187 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(0...𝑗) ⊆
ℕ0) |
189 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) = (𝐺‘𝑛)) |
190 | 166, 19 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) ∈
ℝ) |
191 | 166, 50 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ 0 ≤ (𝐺‘𝑛)) |
192 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq0( +
, 𝐺) ∈ dom ⇝
) |
193 | 108, 185,
186, 188, 189, 190, 191, 192 | isumless 14416 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (0...𝑗)(𝐺‘𝑛) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
194 | 184, 193 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( +
, 𝐺)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
195 | 134, 139,
140, 179, 194 | letrd 10073 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
196 | 195 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
197 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = Σ𝑛 ∈ ℕ0 (𝐺‘𝑛) → ((seq1( + , 𝐹)‘𝑗) ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛))) |
198 | 197 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = Σ𝑛 ∈ ℕ0 (𝐺‘𝑛) → (∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛))) |
199 | 198 | rspcev 3282 |
. . . . 5
⊢
((Σ𝑛 ∈
ℕ0 (𝐺‘𝑛) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥) |
200 | 133, 196,
199 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥) |
201 | 1, 115, 116, 128, 200 | climsup 14248 |
. . 3
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹) ⇝ sup(ran seq1( +
, 𝐹), ℝ, <
)) |
202 | 105 | releldmi 5283 |
. . 3
⊢ (seq1( +
, 𝐹) ⇝ sup(ran seq1(
+ , 𝐹), ℝ, < )
→ seq1( + , 𝐹) ∈
dom ⇝ ) |
203 | 201, 202 | syl 17 |
. 2
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹) ∈ dom ⇝
) |
204 | 114, 203 | impbida 873 |
1
⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔
seq0( + , 𝐺) ∈ dom
⇝ )) |