| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 1
∈ ℤ) |
| 3 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ∈ dom ⇝
) |
| 4 | | rge0ssre 13496 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
| 5 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 6 | 4, 5 | sstri 3993 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℂ |
| 7 | | esumcvg.m |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵) |
| 8 | 7 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,)+∞) ↔ 𝐵 ∈
(0[,)+∞))) |
| 9 | 8 | cbvralvw 3237 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
| 10 | | rsp 3247 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
| 11 | 9, 10 | sylbir 235 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
| 12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑘 ∈ ℕ → 𝐴 ∈
(0[,)+∞))) |
| 13 | 12 | imp 406 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,)+∞)) |
| 14 | 6, 13 | sselid 3981 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℂ) |
| 15 | 14 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℂ) |
| 16 | | esumcvg.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
| 17 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
(1...𝑛) ∈
Fin) |
| 18 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
| 19 | 18, 13 | sylan2 593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
| 20 | 19 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
| 21 | 17, 20 | esumpfinval 34076 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴) |
| 22 | 21 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
| 23 | 16, 22 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
| 24 | 6, 20 | sselid 3981 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
| 25 | 17, 24 | fsumcl 15769 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ ℂ) |
| 26 | 23, 25 | fvmpt2d 7029 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
| 27 | 26 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
| 28 | 1, 2, 3, 15, 27 | isumclim3 15795 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴) |
| 29 | | esumcvg.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
| 30 | 17, 20 | fsumrp0cl 33026 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,)+∞)) |
| 31 | 21, 30 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,)+∞)) |
| 32 | 31, 16 | fmptd 7134 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹:ℕ⟶(0[,)+∞)) |
| 33 | 32 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹:ℕ⟶(0[,)+∞)) |
| 34 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝜑) |
| 35 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑚 ∈ ℕ ↦ 𝐵) = (𝑚 ∈ ℕ ↦ 𝐵)) |
| 36 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 ↔ 𝑚 = 𝑘) |
| 37 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
| 38 | 7, 36, 37 | 3imtr3i 291 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝐵 = 𝐴) |
| 39 | 38 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 = 𝑘) → 𝐵 = 𝐴) |
| 40 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
| 41 | | esumcvg.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
| 42 | 35, 39, 40, 41 | fvmptd 7023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
| 43 | 34, 42 | sylancom 588 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
((𝑚 ∈ ℕ ↦
𝐵)‘𝑘) = 𝐴) |
| 44 | 13 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
(0[,)+∞)) |
| 45 | | elrege0 13494 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
| 46 | 44, 45 | sylib 218 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
| 47 | 46 | simpld 494 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℝ) |
| 48 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ∈
V |
| 49 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
| 50 | 18 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 51 | 49, 50, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
| 52 | 51 | ralrimiva 3146 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,]+∞)) |
| 53 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(1...𝑛) |
| 54 | 53 | esumcl 34031 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑛) ∈ V
∧ ∀𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
| 55 | 48, 52, 54 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
| 56 | 55, 16 | fmptd 7134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(0[,]+∞)) |
| 57 | 56 | ffnd 6737 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn ℕ) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 Fn ℕ) |
| 59 | | 1z 12647 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
| 60 | | seqfn 14054 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → seq1( + , (𝑚
∈ ℕ ↦ 𝐵))
Fn (ℤ≥‘1)) |
| 61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
(ℤ≥‘1) |
| 62 | 1 | fneq2i 6666 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
𝐵)) Fn ℕ ↔ seq1(
+ , (𝑚 ∈ ℕ
↦ 𝐵)) Fn
(ℤ≥‘1)) |
| 63 | 61, 62 | mpbir 231 |
. . . . . . . . . . . 12
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ |
| 64 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ) |
| 65 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
| 66 | 18, 42 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
| 67 | 65, 66 | sylancom 588 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
| 68 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) |
| 69 | 68, 1 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
| 70 | 67, 69, 24 | fsumser 15766 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
| 71 | 26, 70 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
| 72 | 58, 64, 71 | eqfnfvd 7054 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
| 73 | 72 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
| 74 | 73, 3 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
seq1( + , (𝑚 ∈ ℕ
↦ 𝐵)) ∈ dom
⇝ ) |
| 75 | 1, 2, 43, 47, 74 | isumrecl 15801 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
ℝ) |
| 76 | 46 | simprd 495 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) → 0
≤ 𝐴) |
| 77 | 1, 2, 43, 47, 74, 76 | isumge0 15802 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 0
≤ Σ𝑘 ∈
ℕ 𝐴) |
| 78 | | elrege0 13494 |
. . . . . . 7
⊢
(Σ𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ (Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ℕ 𝐴)) |
| 79 | 75, 77, 78 | sylanbrc 583 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
(0[,)+∞)) |
| 80 | | ssid 4006 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,)+∞) |
| 81 | 29, 33, 79, 80 | lmlimxrge0 33947 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴 ↔ 𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴)) |
| 82 | 28, 81 | mpbird 257 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴) |
| 83 | 16, 3 | eqeltrrid 2846 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ) |
| 84 | 22 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
| 85 | 84 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
| 86 | 83, 85 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ ) |
| 87 | 44, 7, 86 | esumpcvgval 34079 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) |
| 88 | 82, 87 | breqtrrd 5171 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
| 89 | 32 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹:ℕ⟶(0[,)+∞)) |
| 90 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℕ) |
| 91 | 90 | nnzd 12640 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℤ) |
| 92 | | uzid 12893 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
| 93 | | peano2uz 12943 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
| 94 | 91, 92, 93 | 3syl 18 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
| 95 | | simplll 775 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → (𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈
(0[,)+∞))) |
| 96 | 95, 13 | sylancom 588 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → 𝐴 ∈
(0[,)+∞)) |
| 97 | 90, 94, 96 | esumpmono 34080 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ≤ Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
| 98 | 26, 21 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
| 99 | 98 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
| 100 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑛 → (1...𝑙) = (1...𝑛)) |
| 101 | | esumeq1 34035 |
. . . . . . . . . . 11
⊢
((1...𝑙) =
(1...𝑛) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑛 → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
| 103 | 102 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
| 104 | 16, 103 | eqtr4i 2768 |
. . . . . . . 8
⊢ 𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) |
| 105 | 104 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴)) |
| 106 | | simpr3 1197 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → 𝑙 = (𝑛 + 1)) |
| 107 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑙 = (𝑛 + 1) → (1...𝑙) = (1...(𝑛 + 1))) |
| 108 | | esumeq1 34035 |
. . . . . . . . 9
⊢
((1...𝑙) =
(1...(𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
| 109 | 106, 107,
108 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
| 110 | 109 | 3anassrs 1361 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑙 = (𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
| 111 | 90 | peano2nnd 12283 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
ℕ) |
| 112 | | ovex 7464 |
. . . . . . . 8
⊢
(1...(𝑛 + 1)) ∈
V |
| 113 | | simp-4l 783 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝜑) |
| 114 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑛 + 1)) → 𝑘 ∈ ℕ) |
| 115 | 114 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝑘 ∈
ℕ) |
| 116 | 113, 115,
41 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝐴 ∈
(0[,]+∞)) |
| 117 | 116 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
| 118 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1...(𝑛 + 1)) |
| 119 | 118 | esumcl 34031 |
. . . . . . . 8
⊢
(((1...(𝑛 + 1))
∈ V ∧ ∀𝑘
∈ (1...(𝑛 + 1))𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
| 120 | 112, 117,
119 | sylancr 587 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
| 121 | 105, 110,
111, 120 | fvmptd 7023 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘(𝑛 + 1)) =
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴) |
| 122 | 97, 99, 121 | 3brtr4d 5175 |
. . . . 5
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
| 123 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
¬ 𝐹 ∈ dom ⇝
) |
| 124 | 29, 89, 122, 123 | lmdvglim 33953 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)+∞) |
| 125 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
| 126 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘ℕ |
| 127 | | nnex 12272 |
. . . . . . . 8
⊢ ℕ
∈ V |
| 128 | 127 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ℕ
∈ V) |
| 129 | 41 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,]+∞)) |
| 130 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
| 131 | | simpll 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
| 132 | | inss1 4237 |
. . . . . . . . . . . . . 14
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
| 133 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ (𝒫 ℕ ∩
Fin)) |
| 134 | 132, 133 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ 𝒫 ℕ) |
| 135 | 134 | elpwid 4609 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ ℕ) |
| 136 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
| 137 | 135, 136 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ ℕ) |
| 138 | 131, 137,
13 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
| 139 | 138 | fmpttd 7135 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (𝑘 ∈
𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) |
| 140 | | esumpfinvallem 34075 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ∧ (𝑘 ∈ 𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) →
(ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
| 141 | 130, 139,
140 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
| 142 | | inss2 4238 |
. . . . . . . . . 10
⊢
(𝒫 ℕ ∩ Fin) ⊆ Fin |
| 143 | 142, 130 | sselid 3981 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
Fin) |
| 144 | 131, 137,
14 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℂ) |
| 145 | 143, 144 | gsumfsum 21452 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
| 146 | 141, 145 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → ((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
| 147 | 125, 126,
128, 129, 146 | esumval 34047 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
| 148 | 147 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
| 149 | 89, 122, 123 | lmdvg 33952 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
| 150 | 149 | r19.21bi 3251 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
| 151 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℤ) |
| 152 | | uzid 12893 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℤ → 𝑙 ∈
(ℤ≥‘𝑙)) |
| 153 | 151, 152 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
(ℤ≥‘𝑙)) |
| 154 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → 𝑛 = 𝑙) |
| 155 | 154 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝐹‘𝑛) = (𝐹‘𝑙)) |
| 156 | 155 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝑦 < (𝐹‘𝑛) ↔ 𝑦 < (𝐹‘𝑙))) |
| 157 | 153, 156 | rspcdv 3614 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ℕ →
(∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛) → 𝑦 < (𝐹‘𝑙))) |
| 158 | 157 | reximia 3081 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛) → ∃𝑙 ∈ ℕ 𝑦 < (𝐹‘𝑙)) |
| 159 | 150, 158 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
𝑦 < (𝐹‘𝑙)) |
| 160 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝑦 ∈
ℝ) |
| 161 | 89 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝐹:ℕ⟶(0[,)+∞)) |
| 162 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝑙 ∈
ℕ) |
| 163 | 161, 162 | ffvelcdmd 7105 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ (0[,)+∞)) |
| 164 | 4, 163 | sselid 3981 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ ℝ) |
| 165 | | ltle 11349 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑙) ∈ ℝ) → (𝑦 < (𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
| 166 | 160, 164,
165 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
| 167 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑙 → (1...𝑛) = (1...𝑙)) |
| 168 | | esumeq1 34035 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) =
(1...𝑙) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
| 169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑙 → Σ*𝑘 ∈ (1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
| 170 | | esumex 34030 |
. . . . . . . . . . . . . . 15
⊢
Σ*𝑘
∈ (1...𝑙)𝐴 ∈ V |
| 171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 ∈ V) |
| 172 | 16, 169, 162, 171 | fvmptd3 7039 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ*𝑘 ∈ (1...𝑙)𝐴) |
| 173 | | fzfid 14014 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (1...𝑙)
∈ Fin) |
| 174 | | simp-4l 783 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
| 175 | | elfznn 13593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...𝑙) → 𝑘 ∈ ℕ) |
| 176 | 175 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝑘 ∈
ℕ) |
| 177 | 174, 176,
13 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝐴 ∈
(0[,)+∞)) |
| 178 | 173, 177 | esumpfinval 34076 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
| 179 | 172, 178 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ𝑘 ∈ (1...𝑙)𝐴) |
| 180 | 179 | breq2d 5155 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 ≤
(𝐹‘𝑙) ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
| 181 | 166, 180 | sylibd 239 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
| 182 | 181 | reximdva 3168 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
(∃𝑙 ∈ ℕ
𝑦 < (𝐹‘𝑙) → ∃𝑙 ∈ ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
| 183 | 159, 182 | mpd 15 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) |
| 184 | | fzssuz 13605 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ⊆
(ℤ≥‘1) |
| 185 | 184, 1 | sseqtrri 4033 |
. . . . . . . . . . . . 13
⊢
(1...𝑙) ⊆
ℕ |
| 186 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ∈
V |
| 187 | 186 | elpw 4604 |
. . . . . . . . . . . . 13
⊢
((1...𝑙) ∈
𝒫 ℕ ↔ (1...𝑙) ⊆ ℕ) |
| 188 | 185, 187 | mpbir 231 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
𝒫 ℕ |
| 189 | | fzfi 14013 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
Fin |
| 190 | | elin 3967 |
. . . . . . . . . . . 12
⊢
((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ↔ ((1...𝑙) ∈ 𝒫 ℕ ∧ (1...𝑙) ∈ Fin)) |
| 191 | 188, 189,
190 | mpbir2an 711 |
. . . . . . . . . . 11
⊢
(1...𝑙) ∈
(𝒫 ℕ ∩ Fin) |
| 192 | | sumex 15724 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ V |
| 193 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴) = (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
| 194 | | sumeq1 15725 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1...𝑙) → Σ𝑘 ∈ 𝑥 𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
| 195 | 193, 194 | elrnmpt1s 5970 |
. . . . . . . . . . 11
⊢
(((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ∧ Σ𝑘 ∈ (1...𝑙)𝐴 ∈ V) → Σ𝑘 ∈ (1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)) |
| 196 | 191, 192,
195 | mp2an 692 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
| 197 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 |
| 198 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑧 = Σ𝑘 ∈ (1...𝑙)𝐴 → (𝑦 ≤ 𝑧 ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
| 199 | 197, 198 | rspce 3611 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ∧ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
| 200 | 196, 199 | mpan 690 |
. . . . . . . . 9
⊢ (𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
| 201 | 200 | rexlimivw 3151 |
. . . . . . . 8
⊢
(∃𝑙 ∈
ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
| 202 | 183, 201 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
| 203 | 202 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
| 204 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
| 205 | 142, 204 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
Fin) |
| 206 | 138 | adantllr 719 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
| 207 | 4, 206 | sselid 3981 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℝ) |
| 208 | 205, 207 | fsumrecl 15770 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈ ℝ) |
| 209 | 208 | rexrd 11311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈
ℝ*) |
| 210 | 209 | fmpttd 7135 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
(𝑥 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ*) |
| 211 | | frn 6743 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ* → ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ⊆
ℝ*) |
| 212 | | supxrunb1 13361 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴) ⊆ ℝ* →
(∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞)) |
| 213 | 210, 211,
212 | 3syl 18 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
(∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞)) |
| 214 | 203, 213 | mpbid 232 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
sup(ran (𝑥 ∈
(𝒫 ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞) |
| 215 | 148, 214 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 =
+∞) |
| 216 | 124, 215 | breqtrrd 5171 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
| 217 | 88, 216 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
| 218 | 16 | reseq1i 5993 |
. . . . . . . 8
⊢ (𝐹 ↾
(ℤ≥‘𝑘)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) |
| 219 | | eleq1w 2824 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (𝑙 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
| 220 | 219 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝜑 ∧ 𝑙 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
| 221 | | sbequ12r 2252 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ([𝑙 / 𝑘]𝐴 = +∞ ↔ 𝐴 = +∞)) |
| 222 | 220, 221 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞))) |
| 223 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
| 224 | 223 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘))) |
| 225 | 223 | xpeq1d 5714 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((ℤ≥‘𝑙) × {+∞}) =
((ℤ≥‘𝑘) × {+∞})) |
| 226 | 224, 225 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞}) ↔
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞}))) |
| 227 | 222, 226 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞})) ↔
(((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})))) |
| 228 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ 𝑙 ∈ ℕ) |
| 229 | | nfs1v 2156 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘[𝑙 / 𝑘]𝐴 = +∞ |
| 230 | 228, 229 | nfan 1899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) |
| 231 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑛 ∈
(ℤ≥‘𝑙) |
| 232 | 230, 231 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) |
| 233 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → (1...𝑛) ∈ V) |
| 234 | | simp-4l 783 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
| 235 | 18 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 236 | 234, 235,
41 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
| 237 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ ℕ) |
| 238 | | elnnuz 12922 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ ℕ ↔ 𝑙 ∈
(ℤ≥‘1)) |
| 239 | | eluzfz 13559 |
. . . . . . . . . . . . . . 15
⊢ ((𝑙 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
| 240 | 238, 239 | sylanb 581 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
| 241 | 237, 240 | sylancom 588 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
| 242 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → [𝑙 / 𝑘]𝐴 = +∞) |
| 243 | | sbequ12 2251 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐴 = +∞ ↔ [𝑙 / 𝑘]𝐴 = +∞)) |
| 244 | 229, 243 | rspce 3611 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ (1...𝑛) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
| 245 | 241, 242,
244 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
| 246 | 232, 233,
236, 245 | esumpinfval 34074 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = +∞) |
| 247 | 246 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) |
| 248 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) →
(ℤ≥‘𝑙) = (ℤ≥‘𝑙)) |
| 249 | | mpteq12 5234 |
. . . . . . . . . . . 12
⊢
(((ℤ≥‘𝑙) = (ℤ≥‘𝑙) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
| 250 | 248, 249 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
| 251 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → 𝑙 ∈ ℕ) |
| 252 | | uznnssnn 12937 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ →
(ℤ≥‘𝑙) ⊆ ℕ) |
| 253 | | resmpt 6055 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑙) ⊆ ℕ → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
| 254 | 251, 252,
253 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
| 255 | 254 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
| 256 | | fconstmpt 5747 |
. . . . . . . . . . . 12
⊢
((ℤ≥‘𝑙) × {+∞}) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞) |
| 257 | 256 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) →
((ℤ≥‘𝑙) × {+∞}) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
| 258 | 250, 255,
257 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) ×
{+∞})) |
| 259 | 247, 258 | mpdan 687 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) ×
{+∞})) |
| 260 | 227, 259 | chvarvv 1998 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
| 261 | 218, 260 | eqtrid 2789 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) |
| 262 | 261 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 = +∞ → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
| 263 | 262 | reximdva 3168 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ℕ 𝐴 = +∞ → ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
| 264 | 263 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ (𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
| 265 | | xrge0topn 33942 |
. . . . . . . . . . 11
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
| 266 | 29, 265 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
| 267 | | letopon 23213 |
. . . . . . . . . . 11
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
| 268 | | iccssxr 13470 |
. . . . . . . . . . 11
⊢
(0[,]+∞) ⊆ ℝ* |
| 269 | | resttopon 23169 |
. . . . . . . . . . 11
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
(0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞))) |
| 270 | 267, 268,
269 | mp2an 692 |
. . . . . . . . . 10
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞)) |
| 271 | 266, 270 | eqeltri 2837 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘(0[,]+∞)) |
| 272 | 271 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐽 ∈
(TopOn‘(0[,]+∞))) |
| 273 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 274 | | pnfxr 11315 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
| 275 | | 0lepnf 13175 |
. . . . . . . . . 10
⊢ 0 ≤
+∞ |
| 276 | | ubicc2 13505 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → +∞ ∈ (0[,]+∞)) |
| 277 | 273, 274,
275, 276 | mp3an 1463 |
. . . . . . . . 9
⊢ +∞
∈ (0[,]+∞) |
| 278 | 277 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → +∞ ∈
(0[,]+∞)) |
| 279 | 40 | nnzd 12640 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
| 280 | | eqid 2737 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
| 281 | 280 | lmconst 23269 |
. . . . . . . 8
⊢ ((𝐽 ∈
(TopOn‘(0[,]+∞)) ∧ +∞ ∈ (0[,]+∞) ∧ 𝑘 ∈ ℤ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
| 282 | 272, 278,
279, 281 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
| 283 | | breq1 5146 |
. . . . . . . 8
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
((𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞ ↔
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞)) |
| 284 | 283 | biimprd 248 |
. . . . . . 7
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
(((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞ → (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
| 285 | 282, 284 | mpan9 506 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) |
| 286 | | ovexd 7466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0[,]+∞) ∈
V) |
| 287 | | cnex 11236 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
| 288 | 287 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℂ ∈
V) |
| 289 | 56 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞)) |
| 290 | | nnsscn 12271 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℂ |
| 291 | 290 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℕ ⊆
ℂ) |
| 292 | | elpm2r 8885 |
. . . . . . . . 9
⊢
((((0[,]+∞) ∈ V ∧ ℂ ∈ V) ∧ (𝐹:ℕ⟶(0[,]+∞)
∧ ℕ ⊆ ℂ)) → 𝐹 ∈ ((0[,]+∞) ↑pm
ℂ)) |
| 293 | 286, 288,
289, 291, 292 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ ((0[,]+∞) ↑pm
ℂ)) |
| 294 | 272, 293,
279 | lmres 23308 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹(⇝𝑡‘𝐽)+∞ ↔ (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
| 295 | 294 | biimpar 477 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
| 296 | 285, 295 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
| 297 | 296 | r19.29an 3158 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
| 298 | 264, 297 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
| 299 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
| 300 | | nfre1 3285 |
. . . . 5
⊢
Ⅎ𝑘∃𝑘 ∈ ℕ 𝐴 = +∞ |
| 301 | 299, 300 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑘(𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) |
| 302 | 127 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ℕ ∈
V) |
| 303 | 41 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
| 304 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ 𝐴 = +∞) |
| 305 | 301, 302,
303, 304 | esumpinfval 34074 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → Σ*𝑘 ∈ ℕ𝐴 = +∞) |
| 306 | 298, 305 | breqtrrd 5171 |
. 2
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
| 307 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑘 ∈ ℕ ↔ 𝑚 ∈ ℕ)) |
| 308 | 307 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑚 ∈ ℕ))) |
| 309 | 7 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,]+∞) ↔ 𝐵 ∈
(0[,]+∞))) |
| 310 | 308, 309 | imbi12d 344 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)))) |
| 311 | 310, 41 | chvarvv 1998 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)) |
| 312 | | eliccelico 32779 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → (𝐵
∈ (0[,]+∞) ↔ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞))) |
| 313 | 273, 274,
275, 312 | mp3an 1463 |
. . . . . 6
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 ∈ (0[,)+∞)
∨ 𝐵 =
+∞)) |
| 314 | 311, 313 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
| 315 | 314 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
| 316 | | r19.30 3120 |
. . . 4
⊢
(∀𝑚 ∈
ℕ (𝐵 ∈
(0[,)+∞) ∨ 𝐵 =
+∞) → (∀𝑚
∈ ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑚 ∈ ℕ 𝐵 = +∞)) |
| 317 | 315, 316 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
| 318 | 7 | eqeq1d 2739 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐴 = +∞ ↔ 𝐵 = +∞)) |
| 319 | 318 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑘 ∈
ℕ 𝐴 = +∞ ↔
∃𝑚 ∈ ℕ
𝐵 =
+∞) |
| 320 | 319 | orbi2i 913 |
. . 3
⊢
((∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑘 ∈ ℕ 𝐴 = +∞) ↔ (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
| 321 | 317, 320 | sylibr 234 |
. 2
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑘 ∈ ℕ
𝐴 =
+∞)) |
| 322 | 217, 306,
321 | mpjaodan 961 |
1
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |