Step | Hyp | Ref
| Expression |
1 | | nnuz 12477 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12208 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 1
∈ ℤ) |
3 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ∈ dom ⇝
) |
4 | | rge0ssre 13044 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
5 | | ax-resscn 10786 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
6 | 4, 5 | sstri 3910 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℂ |
7 | | esumcvg.m |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵) |
8 | 7 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,)+∞) ↔ 𝐵 ∈
(0[,)+∞))) |
9 | 8 | cbvralvw 3358 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
10 | | rsp 3127 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
11 | 9, 10 | sylbir 238 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
12 | 11 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑘 ∈ ℕ → 𝐴 ∈
(0[,)+∞))) |
13 | 12 | imp 410 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,)+∞)) |
14 | 6, 13 | sseldi 3899 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℂ) |
15 | 14 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℂ) |
16 | | esumcvg.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
17 | | fzfid 13546 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
(1...𝑛) ∈
Fin) |
18 | | elfznn 13141 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
19 | 18, 13 | sylan2 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
20 | 19 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
21 | 17, 20 | esumpfinval 31755 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴) |
22 | 21 | mpteq2dva 5150 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
23 | 16, 22 | syl5eq 2790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
24 | 6, 20 | sseldi 3899 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
25 | 17, 24 | fsumcl 15297 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ ℂ) |
26 | 23, 25 | fvmpt2d 6831 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
27 | 26 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
28 | 1, 2, 3, 15, 27 | isumclim3 15323 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴) |
29 | | esumcvg.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
30 | 17, 20 | fsumrp0cl 31023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,)+∞)) |
31 | 21, 30 | eqeltrd 2838 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,)+∞)) |
32 | 31, 16 | fmptd 6931 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹:ℕ⟶(0[,)+∞)) |
33 | 32 | adantr 484 |
. . . . . 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 294 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝐵 = 𝐴) |
39 | 38 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 = 𝑘) → 𝐵 = 𝐴) |
40 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
41 | | esumcvg.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
42 | 35, 39, 40, 41 | fvmptd 6825 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
43 | 34, 42 | sylancom 591 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
((𝑚 ∈ ℕ ↦
𝐵)‘𝑘) = 𝐴) |
44 | 13 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
(0[,)+∞)) |
45 | | elrege0 13042 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
46 | 44, 45 | sylib 221 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
47 | 46 | simpld 498 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℝ) |
48 | | ovex 7246 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ∈
V |
49 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
50 | 18 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
51 | 49, 50, 41 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
52 | 51 | ralrimiva 3105 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,]+∞)) |
53 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(1...𝑛) |
54 | 53 | esumcl 31710 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑛) ∈ V
∧ ∀𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
55 | 48, 52, 54 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
56 | 55, 16 | fmptd 6931 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(0[,]+∞)) |
57 | 56 | ffnd 6546 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn ℕ) |
58 | 57 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 Fn ℕ) |
59 | | 1z 12207 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
60 | | seqfn 13586 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → seq1( + , (𝑚
∈ ℕ ↦ 𝐵))
Fn (ℤ≥‘1)) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
(ℤ≥‘1) |
62 | 1 | fneq2i 6477 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
𝐵)) Fn ℕ ↔ seq1(
+ , (𝑚 ∈ ℕ
↦ 𝐵)) Fn
(ℤ≥‘1)) |
63 | 61, 62 | mpbir 234 |
. . . . . . . . . . . 12
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ |
64 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ) |
65 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
66 | 18, 42 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
67 | 65, 66 | sylancom 591 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
68 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) |
69 | 68, 1 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
70 | 67, 69, 24 | fsumser 15294 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
71 | 26, 70 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
72 | 58, 64, 71 | eqfnfvd 6855 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
73 | 72 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
74 | 73, 3 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
seq1( + , (𝑚 ∈ ℕ
↦ 𝐵)) ∈ dom
⇝ ) |
75 | 1, 2, 43, 47, 74 | isumrecl 15329 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
ℝ) |
76 | 46 | simprd 499 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) → 0
≤ 𝐴) |
77 | 1, 2, 43, 47, 74, 76 | isumge0 15330 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 0
≤ Σ𝑘 ∈
ℕ 𝐴) |
78 | | elrege0 13042 |
. . . . . . 7
⊢
(Σ𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ (Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ℕ 𝐴)) |
79 | 75, 77, 78 | sylanbrc 586 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
(0[,)+∞)) |
80 | | ssid 3923 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,)+∞) |
81 | 29, 33, 79, 80 | lmlimxrge0 31612 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴 ↔ 𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴)) |
82 | 28, 81 | mpbird 260 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴) |
83 | 16, 3 | eqeltrrid 2843 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ) |
84 | 22 | eleq1d 2822 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
85 | 84 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
86 | 83, 85 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ ) |
87 | 44, 7, 86 | esumpcvgval 31758 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) |
88 | 82, 87 | breqtrrd 5081 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
89 | 32 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹:ℕ⟶(0[,)+∞)) |
90 | | simpr 488 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℕ) |
91 | 90 | nnzd 12281 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℤ) |
92 | | uzid 12453 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
93 | | peano2uz 12497 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
95 | | simplll 775 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → (𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈
(0[,)+∞))) |
96 | 95, 13 | sylancom 591 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → 𝐴 ∈
(0[,)+∞)) |
97 | 90, 94, 96 | esumpmono 31759 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ≤ Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
98 | 26, 21 | eqtr4d 2780 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
99 | 98 | adantlr 715 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
100 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑛 → (1...𝑙) = (1...𝑛)) |
101 | | esumeq1 31714 |
. . . . . . . . . . 11
⊢
((1...𝑙) =
(1...𝑛) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
102 | 100, 101 | syl 17 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑛 → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
103 | 102 | cbvmptv 5158 |
. . . . . . . . 9
⊢ (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
104 | 16, 103 | eqtr4i 2768 |
. . . . . . . 8
⊢ 𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) |
105 | 104 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴)) |
106 | | simpr3 1198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → 𝑙 = (𝑛 + 1)) |
107 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑙 = (𝑛 + 1) → (1...𝑙) = (1...(𝑛 + 1))) |
108 | | esumeq1 31714 |
. . . . . . . . 9
⊢
((1...𝑙) =
(1...(𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
109 | 106, 107,
108 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
110 | 109 | 3anassrs 1362 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑙 = (𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
111 | 90 | peano2nnd 11847 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
ℕ) |
112 | | ovex 7246 |
. . . . . . . 8
⊢
(1...(𝑛 + 1)) ∈
V |
113 | | simp-4l 783 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝜑) |
114 | | elfznn 13141 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑛 + 1)) → 𝑘 ∈ ℕ) |
115 | 114 | adantl 485 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝑘 ∈
ℕ) |
116 | 113, 115,
41 | syl2anc 587 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝐴 ∈
(0[,]+∞)) |
117 | 116 | ralrimiva 3105 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
118 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1...(𝑛 + 1)) |
119 | 118 | esumcl 31710 |
. . . . . . . 8
⊢
(((1...(𝑛 + 1))
∈ V ∧ ∀𝑘
∈ (1...(𝑛 + 1))𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
120 | 112, 117,
119 | sylancr 590 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
121 | 105, 110,
111, 120 | fvmptd 6825 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘(𝑛 + 1)) =
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴) |
122 | 97, 99, 121 | 3brtr4d 5085 |
. . . . 5
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
123 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
¬ 𝐹 ∈ dom ⇝
) |
124 | 29, 89, 122, 123 | lmdvglim 31618 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)+∞) |
125 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
126 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘ℕ |
127 | | nnex 11836 |
. . . . . . . 8
⊢ ℕ
∈ V |
128 | 127 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ℕ
∈ V) |
129 | 41 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,]+∞)) |
130 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
131 | | simpll 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
132 | | inss1 4143 |
. . . . . . . . . . . . . 14
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
133 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ (𝒫 ℕ ∩
Fin)) |
134 | 132, 133 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ 𝒫 ℕ) |
135 | 134 | elpwid 4524 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ ℕ) |
136 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
137 | 135, 136 | sseldd 3902 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ ℕ) |
138 | 131, 137,
13 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
139 | 138 | fmpttd 6932 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (𝑘 ∈
𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) |
140 | | esumpfinvallem 31754 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ∧ (𝑘 ∈ 𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) →
(ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
141 | 130, 139,
140 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
142 | | inss2 4144 |
. . . . . . . . . 10
⊢
(𝒫 ℕ ∩ Fin) ⊆ Fin |
143 | 142, 130 | sseldi 3899 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
Fin) |
144 | 131, 137,
14 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℂ) |
145 | 143, 144 | gsumfsum 20430 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
146 | 141, 145 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → ((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
147 | 125, 126,
128, 129, 146 | esumval 31726 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
148 | 147 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
149 | 89, 122, 123 | lmdvg 31617 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
150 | 149 | r19.21bi 3130 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
151 | | nnz 12199 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℤ) |
152 | | uzid 12453 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℤ → 𝑙 ∈
(ℤ≥‘𝑙)) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
(ℤ≥‘𝑙)) |
154 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → 𝑛 = 𝑙) |
155 | 154 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝐹‘𝑛) = (𝐹‘𝑙)) |
156 | 155 | breq2d 5065 |
. . . . . . . . . . . 12
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝑦 < (𝐹‘𝑛) ↔ 𝑦 < (𝐹‘𝑙))) |
157 | 153, 156 | rspcdv 3529 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ℕ →
(∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛) → 𝑦 < (𝐹‘𝑙))) |
158 | 157 | reximia 3165 |
. . . . . . . . . 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 488 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝑙 ∈
ℕ) |
163 | 161, 162 | ffvelrnd 6905 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ (0[,)+∞)) |
164 | 4, 163 | sseldi 3899 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ ℝ) |
165 | | ltle 10921 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑙) ∈ ℝ) → (𝑦 < (𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
166 | 160, 164,
165 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
167 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑙 → (1...𝑛) = (1...𝑙)) |
168 | | esumeq1 31714 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) =
(1...𝑙) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑙 → Σ*𝑘 ∈ (1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
170 | | esumex 31709 |
. . . . . . . . . . . . . . 15
⊢
Σ*𝑘
∈ (1...𝑙)𝐴 ∈ V |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 ∈ V) |
172 | 16, 169, 162, 171 | fvmptd3 6841 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ*𝑘 ∈ (1...𝑙)𝐴) |
173 | | fzfid 13546 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (1...𝑙)
∈ Fin) |
174 | | simp-4l 783 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
175 | | elfznn 13141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...𝑙) → 𝑘 ∈ ℕ) |
176 | 175 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝑘 ∈
ℕ) |
177 | 174, 176,
13 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝐴 ∈
(0[,)+∞)) |
178 | 173, 177 | esumpfinval 31755 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
179 | 172, 178 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ𝑘 ∈ (1...𝑙)𝐴) |
180 | 179 | breq2d 5065 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 ≤
(𝐹‘𝑙) ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
181 | 166, 180 | sylibd 242 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
182 | 181 | reximdva 3193 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
(∃𝑙 ∈ ℕ
𝑦 < (𝐹‘𝑙) → ∃𝑙 ∈ ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
183 | 159, 182 | mpd 15 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) |
184 | | fzssuz 13153 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ⊆
(ℤ≥‘1) |
185 | 184, 1 | sseqtrri 3938 |
. . . . . . . . . . . . 13
⊢
(1...𝑙) ⊆
ℕ |
186 | | ovex 7246 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ∈
V |
187 | 186 | elpw 4517 |
. . . . . . . . . . . . 13
⊢
((1...𝑙) ∈
𝒫 ℕ ↔ (1...𝑙) ⊆ ℕ) |
188 | 185, 187 | mpbir 234 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
𝒫 ℕ |
189 | | fzfi 13545 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
Fin |
190 | | elin 3882 |
. . . . . . . . . . . 12
⊢
((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ↔ ((1...𝑙) ∈ 𝒫 ℕ ∧ (1...𝑙) ∈ Fin)) |
191 | 188, 189,
190 | mpbir2an 711 |
. . . . . . . . . . 11
⊢
(1...𝑙) ∈
(𝒫 ℕ ∩ Fin) |
192 | | sumex 15251 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ V |
193 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴) = (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
194 | | sumeq1 15252 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1...𝑙) → Σ𝑘 ∈ 𝑥 𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
195 | 193, 194 | elrnmpt1s 5826 |
. . . . . . . . . . 11
⊢
(((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ∧ Σ𝑘 ∈ (1...𝑙)𝐴 ∈ V) → Σ𝑘 ∈ (1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)) |
196 | 191, 192,
195 | mp2an 692 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
197 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 |
198 | | breq2 5057 |
. . . . . . . . . . 11
⊢ (𝑧 = Σ𝑘 ∈ (1...𝑙)𝐴 → (𝑦 ≤ 𝑧 ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
199 | 197, 198 | rspce 3526 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ∧ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
200 | 196, 199 | mpan 690 |
. . . . . . . . 9
⊢ (𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
201 | 200 | rexlimivw 3201 |
. . . . . . . 8
⊢
(∃𝑙 ∈
ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
202 | 183, 201 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
203 | 202 | ralrimiva 3105 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
204 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
205 | 142, 204 | sseldi 3899 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
Fin) |
206 | 138 | adantllr 719 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
207 | 4, 206 | sseldi 3899 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℝ) |
208 | 205, 207 | fsumrecl 15298 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈ ℝ) |
209 | 208 | rexrd 10883 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈
ℝ*) |
210 | 209 | fmpttd 6932 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
(𝑥 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ*) |
211 | | frn 6552 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ* → ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ⊆
ℝ*) |
212 | | supxrunb1 12909 |
. . . . . . 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 235 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
sup(ran (𝑥 ∈
(𝒫 ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞) |
215 | 148, 214 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 =
+∞) |
216 | 124, 215 | breqtrrd 5081 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
217 | 88, 216 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
218 | 16 | reseq1i 5847 |
. . . . . . . 8
⊢ (𝐹 ↾
(ℤ≥‘𝑘)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) |
219 | | eleq1w 2820 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (𝑙 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
220 | 219 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝜑 ∧ 𝑙 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
221 | | sbequ12r 2250 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ([𝑙 / 𝑘]𝐴 = +∞ ↔ 𝐴 = +∞)) |
222 | 220, 221 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞))) |
223 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
224 | 223 | reseq2d 5851 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘))) |
225 | 223 | xpeq1d 5580 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((ℤ≥‘𝑙) × {+∞}) =
((ℤ≥‘𝑘) × {+∞})) |
226 | 224, 225 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞}) ↔
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞}))) |
227 | 222, 226 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞})) ↔
(((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})))) |
228 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ 𝑙 ∈ ℕ) |
229 | | nfs1v 2157 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘[𝑙 / 𝑘]𝐴 = +∞ |
230 | 228, 229 | nfan 1907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) |
231 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑛 ∈
(ℤ≥‘𝑙) |
232 | 230, 231 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) |
233 | | ovexd 7248 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → (1...𝑛) ∈ V) |
234 | | simp-4l 783 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
235 | 18 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
236 | 234, 235,
41 | syl2anc 587 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
237 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ ℕ) |
238 | | elnnuz 12478 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ ℕ ↔ 𝑙 ∈
(ℤ≥‘1)) |
239 | | eluzfz 13107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑙 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
240 | 238, 239 | sylanb 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
241 | 237, 240 | sylancom 591 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
242 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → [𝑙 / 𝑘]𝐴 = +∞) |
243 | | sbequ12 2249 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐴 = +∞ ↔ [𝑙 / 𝑘]𝐴 = +∞)) |
244 | 229, 243 | rspce 3526 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ (1...𝑛) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
245 | 241, 242,
244 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
246 | 232, 233,
236, 245 | esumpinfval 31753 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = +∞) |
247 | 246 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) |
248 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) →
(ℤ≥‘𝑙) = (ℤ≥‘𝑙)) |
249 | | mpteq12 5142 |
. . . . . . . . . . . 12
⊢
(((ℤ≥‘𝑙) = (ℤ≥‘𝑙) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
250 | 248, 249 | sylan 583 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
251 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → 𝑙 ∈ ℕ) |
252 | | uznnssnn 12491 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ →
(ℤ≥‘𝑙) ⊆ ℕ) |
253 | | resmpt 5905 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑙) ⊆ ℕ → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
254 | 251, 252,
253 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
255 | 254 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
256 | | fconstmpt 5611 |
. . . . . . . . . . . 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 2007 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
261 | 218, 260 | syl5eq 2790 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) |
262 | 261 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 = +∞ → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
263 | 262 | reximdva 3193 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ℕ 𝐴 = +∞ → ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
264 | 263 | imp 410 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ (𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
265 | | xrge0topn 31607 |
. . . . . . . . . . 11
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
266 | 29, 265 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
267 | | letopon 22102 |
. . . . . . . . . . 11
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
268 | | iccssxr 13018 |
. . . . . . . . . . 11
⊢
(0[,]+∞) ⊆ ℝ* |
269 | | resttopon 22058 |
. . . . . . . . . . 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 2834 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘(0[,]+∞)) |
272 | 271 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐽 ∈
(TopOn‘(0[,]+∞))) |
273 | | 0xr 10880 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
274 | | pnfxr 10887 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
275 | | 0lepnf 12724 |
. . . . . . . . . 10
⊢ 0 ≤
+∞ |
276 | | ubicc2 13053 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → +∞ ∈ (0[,]+∞)) |
277 | 273, 274,
275, 276 | mp3an 1463 |
. . . . . . . . 9
⊢ +∞
∈ (0[,]+∞) |
278 | 277 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → +∞ ∈
(0[,]+∞)) |
279 | 40 | nnzd 12281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
280 | | eqid 2737 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
281 | 280 | lmconst 22158 |
. . . . . . . 8
⊢ ((𝐽 ∈
(TopOn‘(0[,]+∞)) ∧ +∞ ∈ (0[,]+∞) ∧ 𝑘 ∈ ℤ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
282 | 272, 278,
279, 281 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
283 | | breq1 5056 |
. . . . . . . 8
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
((𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞ ↔
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞)) |
284 | 283 | biimprd 251 |
. . . . . . 7
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
(((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞ → (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
285 | 282, 284 | mpan9 510 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) |
286 | | ovexd 7248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0[,]+∞) ∈
V) |
287 | | cnex 10810 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
288 | 287 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℂ ∈
V) |
289 | 56 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞)) |
290 | | nnsscn 11835 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℂ |
291 | 290 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℕ ⊆
ℂ) |
292 | | elpm2r 8526 |
. . . . . . . . 9
⊢
((((0[,]+∞) ∈ V ∧ ℂ ∈ V) ∧ (𝐹:ℕ⟶(0[,]+∞)
∧ ℕ ⊆ ℂ)) → 𝐹 ∈ ((0[,]+∞) ↑pm
ℂ)) |
293 | 286, 288,
289, 291, 292 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ ((0[,]+∞) ↑pm
ℂ)) |
294 | 272, 293,
279 | lmres 22197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹(⇝𝑡‘𝐽)+∞ ↔ (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
295 | 294 | biimpar 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
296 | 285, 295 | syldan 594 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
297 | 296 | r19.29an 3207 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
298 | 264, 297 | syldan 594 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
299 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
300 | | nfre1 3225 |
. . . . 5
⊢
Ⅎ𝑘∃𝑘 ∈ ℕ 𝐴 = +∞ |
301 | 299, 300 | nfan 1907 |
. . . 4
⊢
Ⅎ𝑘(𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) |
302 | 127 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ℕ ∈
V) |
303 | 41 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
304 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ 𝐴 = +∞) |
305 | 301, 302,
303, 304 | esumpinfval 31753 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → Σ*𝑘 ∈ ℕ𝐴 = +∞) |
306 | 298, 305 | breqtrrd 5081 |
. 2
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
307 | | eleq1w 2820 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑘 ∈ ℕ ↔ 𝑚 ∈ ℕ)) |
308 | 307 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑚 ∈ ℕ))) |
309 | 7 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,]+∞) ↔ 𝐵 ∈
(0[,]+∞))) |
310 | 308, 309 | imbi12d 348 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)))) |
311 | 310, 41 | chvarvv 2007 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)) |
312 | | eliccelico 30818 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → (𝐵
∈ (0[,]+∞) ↔ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞))) |
313 | 273, 274,
275, 312 | mp3an 1463 |
. . . . . 6
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 ∈ (0[,)+∞)
∨ 𝐵 =
+∞)) |
314 | 311, 313 | sylib 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
315 | 314 | ralrimiva 3105 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
316 | | r19.30 3253 |
. . . 4
⊢
(∀𝑚 ∈
ℕ (𝐵 ∈
(0[,)+∞) ∨ 𝐵 =
+∞) → (∀𝑚
∈ ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑚 ∈ ℕ 𝐵 = +∞)) |
317 | 315, 316 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
318 | 7 | eqeq1d 2739 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐴 = +∞ ↔ 𝐵 = +∞)) |
319 | 318 | cbvrexvw 3359 |
. . . 4
⊢
(∃𝑘 ∈
ℕ 𝐴 = +∞ ↔
∃𝑚 ∈ ℕ
𝐵 =
+∞) |
320 | 319 | orbi2i 913 |
. . 3
⊢
((∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑘 ∈ ℕ 𝐴 = +∞) ↔ (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
321 | 317, 320 | sylibr 237 |
. 2
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑘 ∈ ℕ
𝐴 =
+∞)) |
322 | 217, 306,
321 | mpjaodan 959 |
1
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |