| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → 1 ∈
ℤ) |
| 3 | | 1zzd 12648 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
| 4 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 5 | | climcnds.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) = ((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 6 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 7 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
| 8 | | nnexpcl 14115 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 9 | 6, 7, 8 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ) |
| 10 | 9 | nnred 12281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℝ) |
| 11 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = (2↑𝑛) → (𝐹‘𝑘) = (𝐹‘(2↑𝑛))) |
| 12 | 11 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑘 = (2↑𝑛) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(2↑𝑛)) ∈ ℝ)) |
| 13 | | climcnds.1 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 14 | 13 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
| 16 | 12, 15, 9 | rspcdva 3623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(2↑𝑛)) ∈
ℝ) |
| 17 | 10, 16 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((2↑𝑛) · (𝐹‘(2↑𝑛))) ∈
ℝ) |
| 18 | 5, 17 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℝ) |
| 19 | 4, 18 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
| 20 | 1, 3, 19 | serfre 14072 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺):ℕ⟶ℝ) |
| 22 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 23 | 22, 1 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
| 24 | | nnz 12634 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
| 25 | 24 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) |
| 26 | | uzid 12893 |
. . . . . . . 8
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 27 | | peano2uz 12943 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 28 | 25, 26, 27 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
| 29 | | simpl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑) |
| 30 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...(𝑗 + 1)) → 𝑛 ∈ ℕ) |
| 31 | 29, 30, 19 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...(𝑗 + 1))) → (𝐺‘𝑛) ∈ ℝ) |
| 32 | | simpll 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑) |
| 33 | | elfz1eq 13575 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑛 = (𝑗 + 1)) |
| 34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 = (𝑗 + 1)) |
| 35 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
| 36 | | peano2nn0 12566 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ0) |
| 38 | 37 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → (𝑗 + 1) ∈
ℕ0) |
| 39 | 34, 38 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑛 ∈ ℕ0) |
| 40 | 9 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(2↑𝑛) ∈
ℕ0) |
| 41 | 40 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(2↑𝑛)) |
| 42 | 11 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑘 = (2↑𝑛) → (0 ≤ (𝐹‘𝑘) ↔ 0 ≤ (𝐹‘(2↑𝑛)))) |
| 43 | | climcnds.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐹‘𝑘)) |
| 44 | 43 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ ℕ 0 ≤ (𝐹‘𝑘)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ ℕ 0
≤ (𝐹‘𝑘)) |
| 46 | 42, 45, 9 | rspcdva 3623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(𝐹‘(2↑𝑛))) |
| 47 | 10, 16, 41, 46 | mulge0d 11840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
((2↑𝑛) · (𝐹‘(2↑𝑛)))) |
| 48 | 47, 5 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(𝐺‘𝑛)) |
| 49 | 32, 39, 48 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐺‘𝑛)) |
| 50 | 23, 28, 31, 49 | sermono 14075 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1))) |
| 51 | 50 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (seq1( + , 𝐺)‘(𝑗 + 1))) |
| 52 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 53 | | eqidd 2738 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 54 | 13 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 55 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐹) ∈ dom ⇝
) |
| 56 | 1, 2, 53, 54, 55 | isumrecl 15801 |
. . . . . . 7
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → Σ𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) |
| 57 | | remulcl 11240 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ Σ𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℝ) → (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)) ∈ ℝ) |
| 58 | 52, 56, 57 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)) ∈ ℝ) |
| 59 | 21 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ∈
ℝ) |
| 60 | 1, 3, 13 | serfre 14072 |
. . . . . . . . . . 11
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℝ) |
| 61 | 60 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹):ℕ⟶ℝ) |
| 62 | 35 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
| 63 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
| 64 | 6, 62, 63 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℕ) |
| 65 | 61, 64 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘(2↑𝑗)) ∈
ℝ) |
| 66 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ (seq1( + , 𝐹)‘(2↑𝑗)) ∈ ℝ) → (2 · (seq1(
+ , 𝐹)‘(2↑𝑗))) ∈
ℝ) |
| 67 | 52, 65, 66 | sylancr 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· (seq1( + , 𝐹)‘(2↑𝑗))) ∈ ℝ) |
| 68 | 58 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· Σ𝑘 ∈
ℕ (𝐹‘𝑘)) ∈
ℝ) |
| 69 | | climcnds.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
| 70 | 13, 43, 69, 5 | climcndslem2 15886 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐺)‘𝑗) ≤ (2 · (seq1( + , 𝐹)‘(2↑𝑗)))) |
| 71 | 70 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (2 · (seq1( + ,
𝐹)‘(2↑𝑗)))) |
| 72 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 73 | 64, 1 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
(ℤ≥‘1)) |
| 74 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑) |
| 75 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2↑𝑗)) → 𝑘 ∈ ℕ) |
| 76 | 13 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 77 | 74, 75, 76 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(2↑𝑗))) → (𝐹‘𝑘) ∈ ℂ) |
| 78 | 72, 73, 77 | fsumser 15766 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈
(1...(2↑𝑗))(𝐹‘𝑘) = (seq1( + , 𝐹)‘(2↑𝑗))) |
| 79 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 1 ∈
ℤ) |
| 80 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(1...(2↑𝑗)) ∈
Fin) |
| 81 | 75 | ssriv 3987 |
. . . . . . . . . . . 12
⊢
(1...(2↑𝑗))
⊆ ℕ |
| 82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(1...(2↑𝑗)) ⊆
ℕ) |
| 83 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
| 84 | 13 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 85 | 43 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → 0 ≤
(𝐹‘𝑘)) |
| 86 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹) ∈ dom ⇝
) |
| 87 | 1, 79, 80, 82, 83, 84, 85, 86 | isumless 15881 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈
(1...(2↑𝑗))(𝐹‘𝑘) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘)) |
| 88 | 78, 87 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘)) |
| 89 | 56 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈ ℕ
(𝐹‘𝑘) ∈ ℝ) |
| 90 | | 2rp 13039 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
| 91 | 90 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ+) |
| 92 | 65, 89, 91 | lemul2d 13121 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → ((seq1(
+ , 𝐹)‘(2↑𝑗)) ≤ Σ𝑘 ∈ ℕ (𝐹‘𝑘) ↔ (2 · (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 ·
Σ𝑘 ∈ ℕ
(𝐹‘𝑘)))) |
| 93 | 88, 92 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (2
· (seq1( + , 𝐹)‘(2↑𝑗))) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
| 94 | 59, 67, 68, 71, 93 | letrd 11418 |
. . . . . . 7
⊢ (((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
| 95 | 94 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) |
| 96 | | brralrspcev 5203 |
. . . . . 6
⊢ (((2
· Σ𝑘 ∈
ℕ (𝐹‘𝑘)) ∈ ℝ ∧
∀𝑗 ∈ ℕ
(seq1( + , 𝐺)‘𝑗) ≤ (2 · Σ𝑘 ∈ ℕ (𝐹‘𝑘))) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥) |
| 97 | 58, 95, 96 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐺)‘𝑗) ≤ 𝑥) |
| 98 | 1, 2, 21, 51, 97 | climsup 15706 |
. . . 4
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺) ⇝ sup(ran seq1( +
, 𝐺), ℝ, <
)) |
| 99 | | climrel 15528 |
. . . . 5
⊢ Rel
⇝ |
| 100 | 99 | releldmi 5959 |
. . . 4
⊢ (seq1( +
, 𝐺) ⇝ sup(ran seq1(
+ , 𝐺), ℝ, < )
→ seq1( + , 𝐺) ∈
dom ⇝ ) |
| 101 | 98, 100 | syl 17 |
. . 3
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq1( + ,
𝐺) ∈ dom ⇝
) |
| 102 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 103 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 104 | 103 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
| 105 | 18 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ ℂ) |
| 106 | 102, 104,
105 | iserex 15693 |
. . . 4
⊢ (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq1( + , 𝐺) ∈ dom
⇝ )) |
| 107 | 106 | biimpar 477 |
. . 3
⊢ ((𝜑 ∧ seq1( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
| 108 | 101, 107 | syldan 591 |
. 2
⊢ ((𝜑 ∧ seq1( + , 𝐹) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
| 109 | | 1zzd 12648 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 1 ∈
ℤ) |
| 110 | 60 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹):ℕ⟶ℝ) |
| 111 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(𝑗 + 1)) → 𝑘 ∈ ℕ) |
| 112 | 29, 111, 13 | syl2an 596 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℝ) |
| 113 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝜑) |
| 114 | | peano2nn 12278 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
| 115 | 114 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈ ℕ) |
| 116 | | elfz1eq 13575 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1)) → 𝑘 = (𝑗 + 1)) |
| 117 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ)) |
| 118 | 117 | biimparc 479 |
. . . . . . . 8
⊢ (((𝑗 + 1) ∈ ℕ ∧ 𝑘 = (𝑗 + 1)) → 𝑘 ∈ ℕ) |
| 119 | 115, 116,
118 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 𝑘 ∈ ℕ) |
| 120 | 113, 119,
43 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...(𝑗 + 1))) → 0 ≤ (𝐹‘𝑘)) |
| 121 | 23, 28, 112, 120 | sermono 14075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1))) |
| 122 | 121 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘(𝑗 + 1))) |
| 123 | | 0zd 12625 |
. . . . . 6
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → 0 ∈
ℤ) |
| 124 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) = (𝐺‘𝑛)) |
| 125 | 18 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) ∈
ℝ) |
| 126 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺) ∈ dom ⇝
) |
| 127 | 102, 123,
124, 125, 126 | isumrecl 15801 |
. . . . 5
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → Σ𝑛 ∈ ℕ0
(𝐺‘𝑛) ∈ ℝ) |
| 128 | 110 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ∈
ℝ) |
| 129 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
| 130 | 102, 129,
18 | serfre 14072 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℝ) |
| 131 | 130 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq0( + ,
𝐺):ℕ0⟶ℝ) |
| 132 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((seq0( +
, 𝐺):ℕ0⟶ℝ ∧
𝑗 ∈
ℕ0) → (seq0( + , 𝐺)‘𝑗) ∈ ℝ) |
| 133 | 131, 35, 132 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( +
, 𝐺)‘𝑗) ∈
ℝ) |
| 134 | 127 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈
ℕ0 (𝐺‘𝑛) ∈ ℝ) |
| 135 | 110 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq1( +
, 𝐹):ℕ⟶ℝ) |
| 136 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
| 137 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
| 138 | 37 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ0) |
| 139 | 138 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℝ) |
| 140 | | nnexpcl 14115 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
| 141 | 6, 138, 140 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℕ) |
| 142 | 141 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℝ) |
| 143 | | 2z 12649 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
| 144 | | uzid 12893 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 145 | 143, 144 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(ℤ≥‘2) |
| 146 | | bernneq3 14270 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝑗 + 1) ∈ ℕ0) →
(𝑗 + 1) < (2↑(𝑗 + 1))) |
| 147 | 145, 138,
146 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) < (2↑(𝑗 + 1))) |
| 148 | 139, 142,
147 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ≤ (2↑(𝑗 + 1))) |
| 149 | 137 | peano2zd 12725 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℤ) |
| 150 | 141 | nnzd 12640 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
ℤ) |
| 151 | | eluz 12892 |
. . . . . . . . . . . . 13
⊢ (((𝑗 + 1) ∈ ℤ ∧
(2↑(𝑗 + 1)) ∈
ℤ) → ((2↑(𝑗
+ 1)) ∈ (ℤ≥‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1)))) |
| 152 | 149, 150,
151 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1)) ↔ (𝑗 + 1) ≤ (2↑(𝑗 + 1)))) |
| 153 | 148, 152 | mpbird 257 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1))) |
| 154 | | eluzp1m1 12904 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧
(2↑(𝑗 + 1)) ∈
(ℤ≥‘(𝑗 + 1))) → ((2↑(𝑗 + 1)) − 1) ∈
(ℤ≥‘𝑗)) |
| 155 | 137, 153,
154 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘𝑗)) |
| 156 | | eluznn 12960 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧
((2↑(𝑗 + 1)) −
1) ∈ (ℤ≥‘𝑗)) → ((2↑(𝑗 + 1)) − 1) ∈
ℕ) |
| 157 | 136, 155,
156 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
((2↑(𝑗 + 1)) −
1) ∈ ℕ) |
| 158 | 135, 157 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ∈
ℝ) |
| 159 | 23 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
| 160 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝜑) |
| 161 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈
ℕ) |
| 162 | 160, 161,
13 | syl2an 596 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...((2↑(𝑗 + 1)) − 1))) →
(𝐹‘𝑘) ∈ ℝ) |
| 163 | 114 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (𝑗 + 1) ∈
ℕ) |
| 164 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1)) → 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) |
| 165 | | eluznn 12960 |
. . . . . . . . . . 11
⊢ (((𝑗 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ ℕ) |
| 166 | 163, 164,
165 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 𝑘 ∈ ℕ) |
| 167 | 160, 166,
43 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ((𝑗 + 1)...((2↑(𝑗 + 1)) − 1))) → 0 ≤ (𝐹‘𝑘)) |
| 168 | 159, 155,
162, 167 | sermono 14075 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq1( + , 𝐹)‘((2↑(𝑗 + 1)) −
1))) |
| 169 | 35 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
| 170 | 13, 43, 69, 5 | climcndslem1 15885 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗)) |
| 171 | 160, 169,
170 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘((2↑(𝑗 + 1)) − 1)) ≤ (seq0( +
, 𝐺)‘𝑗)) |
| 172 | 128, 158,
133, 168, 171 | letrd 11418 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ (seq0( + , 𝐺)‘𝑗)) |
| 173 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺‘𝑛) = (𝐺‘𝑛)) |
| 174 | 169, 102 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘0)) |
| 175 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (0...𝑗) → 𝑛 ∈ ℕ0) |
| 176 | 160, 175,
105 | syl2an 596 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (0...𝑗)) → (𝐺‘𝑛) ∈ ℂ) |
| 177 | 173, 174,
176 | fsumser 15766 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (0...𝑗)(𝐺‘𝑛) = (seq0( + , 𝐺)‘𝑗)) |
| 178 | | 0zd 12625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → 0 ∈
ℤ) |
| 179 | | fzfid 14014 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(0...𝑗) ∈
Fin) |
| 180 | 175 | ssriv 3987 |
. . . . . . . . . 10
⊢
(0...𝑗) ⊆
ℕ0 |
| 181 | 180 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
(0...𝑗) ⊆
ℕ0) |
| 182 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) = (𝐺‘𝑛)) |
| 183 | 18 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ (𝐺‘𝑛) ∈
ℝ) |
| 184 | 48 | ad4ant14 752 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ0)
→ 0 ≤ (𝐺‘𝑛)) |
| 185 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → seq0( +
, 𝐺) ∈ dom ⇝
) |
| 186 | 102, 178,
179, 181, 182, 183, 184, 185 | isumless 15881 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (0...𝑗)(𝐺‘𝑛) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
| 187 | 177, 186 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq0( +
, 𝐺)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
| 188 | 128, 133,
134, 172, 187 | letrd 11418 |
. . . . . 6
⊢ (((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
| 189 | 188 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) |
| 190 | | brralrspcev 5203 |
. . . . 5
⊢
((Σ𝑛 ∈
ℕ0 (𝐺‘𝑛) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ Σ𝑛 ∈ ℕ0 (𝐺‘𝑛)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥) |
| 191 | 127, 189,
190 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (seq1( + , 𝐹)‘𝑗) ≤ 𝑥) |
| 192 | 1, 109, 110, 122, 191 | climsup 15706 |
. . 3
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹) ⇝ sup(ran seq1( +
, 𝐹), ℝ, <
)) |
| 193 | 99 | releldmi 5959 |
. . 3
⊢ (seq1( +
, 𝐹) ⇝ sup(ran seq1(
+ , 𝐹), ℝ, < )
→ seq1( + , 𝐹) ∈
dom ⇝ ) |
| 194 | 192, 193 | syl 17 |
. 2
⊢ ((𝜑 ∧ seq0( + , 𝐺) ∈ dom ⇝ ) → seq1( + ,
𝐹) ∈ dom ⇝
) |
| 195 | 108, 194 | impbida 801 |
1
⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔
seq0( + , 𝐺) ∈ dom
⇝ )) |