Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 1
∈ ℤ) |
3 | | simpr 477 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ∈ dom ⇝
) |
4 | | rge0ssre 12280 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
5 | | ax-resscn 9993 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
6 | 4, 5 | sstri 3612 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℂ |
7 | | esumcvg.m |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → 𝐴 = 𝐵) |
8 | 7 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,)+∞) ↔ 𝐵 ∈
(0[,)+∞))) |
9 | 8 | cbvralv 3171 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
10 | | rsp 2929 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
11 | 9, 10 | sylbir 225 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) → (𝑘
∈ ℕ → 𝐴
∈ (0[,)+∞))) |
12 | 11 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑘 ∈ ℕ → 𝐴 ∈
(0[,)+∞))) |
13 | 12 | imp 445 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,)+∞)) |
14 | 6, 13 | sseldi 3601 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
ℂ) |
15 | 14 | adantlr 751 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℂ) |
16 | | esumcvg.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
17 | | fzfid 12772 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
(1...𝑛) ∈
Fin) |
18 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
19 | 18, 13 | sylan2 491 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
20 | 19 | adantlr 751 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,)+∞)) |
21 | 17, 20 | esumpfinval 30137 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ𝑘 ∈ (1...𝑛)𝐴) |
22 | 21 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
23 | 16, 22 | syl5eq 2668 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (1...𝑛)𝐴)) |
24 | 6, 20 | sseldi 3601 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
25 | 17, 24 | fsumcl 14464 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ ℂ) |
26 | 23, 25 | fvmpt2d 6293 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
27 | 26 | adantlr 751 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ𝑘 ∈ (1...𝑛)𝐴) |
28 | 1, 2, 3, 15, 27 | isumclim3 14490 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴) |
29 | | esumcvg.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
30 | 17, 20 | fsumrp0cl 29695 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,)+∞)) |
31 | 21, 30 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,)+∞)) |
32 | 31, 16 | fmptd 6385 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹:ℕ⟶(0[,)+∞)) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹:ℕ⟶(0[,)+∞)) |
34 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝜑) |
35 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑚 ∈ ℕ ↦ 𝐵) = (𝑚 ∈ ℕ ↦ 𝐵)) |
36 | | eqcom 2629 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 ↔ 𝑚 = 𝑘) |
37 | | eqcom 2629 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
38 | 7, 36, 37 | 3imtr3i 280 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝐵 = 𝐴) |
39 | 38 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 = 𝑘) → 𝐵 = 𝐴) |
40 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
41 | | esumcvg.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
42 | 35, 39, 40, 41 | fvmptd 6288 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
43 | 34, 42 | sylancom 701 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
((𝑚 ∈ ℕ ↦
𝐵)‘𝑘) = 𝐴) |
44 | 13 | adantlr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
(0[,)+∞)) |
45 | | elrege0 12278 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0[,)+∞) ↔
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
46 | 44, 45 | sylib 208 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) |
47 | 46 | simpld 475 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) →
𝐴 ∈
ℝ) |
48 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑛) ∈
V |
49 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
50 | 18 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
51 | 49, 50, 41 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
52 | 51 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)𝐴 ∈ (0[,]+∞)) |
53 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(1...𝑛) |
54 | 53 | esumcl 30092 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑛) ∈ V
∧ ∀𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
55 | 48, 52, 54 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ∈ (0[,]+∞)) |
56 | 55, 16 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(0[,]+∞)) |
57 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℕ⟶(0[,]+∞)
→ 𝐹 Fn
ℕ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn ℕ) |
59 | 58 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 Fn ℕ) |
60 | | 1z 11407 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
61 | | seqfn 12813 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℤ → seq1( + , (𝑚
∈ ℕ ↦ 𝐵))
Fn (ℤ≥‘1)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
(ℤ≥‘1) |
63 | 1 | fneq2i 5986 |
. . . . . . . . . . . . 13
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
𝐵)) Fn ℕ ↔ seq1(
+ , (𝑚 ∈ ℕ
↦ 𝐵)) Fn
(ℤ≥‘1)) |
64 | 62, 63 | mpbir 221 |
. . . . . . . . . . . 12
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ |
65 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → seq1( + ,
(𝑚 ∈ ℕ ↦
𝐵)) Fn
ℕ) |
66 | | simplll 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
67 | 18, 42 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
68 | 66, 67 | sylancom 701 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ 𝐵)‘𝑘) = 𝐴) |
69 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) |
70 | 69, 1 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
71 | 68, 70, 24 | fsumser 14461 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑛)𝐴 = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
72 | 26, 71 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))‘𝑛)) |
73 | 59, 65, 72 | eqfnfvd 6314 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
74 | 73 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ 𝐵))) |
75 | 74, 3 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
seq1( + , (𝑚 ∈ ℕ
↦ 𝐵)) ∈ dom
⇝ ) |
76 | 1, 2, 43, 47, 75 | isumrecl 14496 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
ℝ) |
77 | 46 | simprd 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ ℕ) → 0
≤ 𝐴) |
78 | 1, 2, 43, 47, 75, 77 | isumge0 14497 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) → 0
≤ Σ𝑘 ∈
ℕ 𝐴) |
79 | | elrege0 12278 |
. . . . . . 7
⊢
(Σ𝑘 ∈
ℕ 𝐴 ∈
(0[,)+∞) ↔ (Σ𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ℕ 𝐴)) |
80 | 76, 78, 79 | sylanbrc 698 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ𝑘 ∈ ℕ
𝐴 ∈
(0[,)+∞)) |
81 | | ssid 3624 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,)+∞) |
82 | 29, 33, 80, 81 | lmlimxrge0 29994 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴 ↔ 𝐹 ⇝ Σ𝑘 ∈ ℕ 𝐴)) |
83 | 28, 82 | mpbird 247 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ𝑘 ∈ ℕ 𝐴) |
84 | 16, 3 | syl5eqelr 2706 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ) |
85 | 22 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
86 | 85 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ∈ dom ⇝ ↔ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ )) |
87 | 84, 86 | mpbid 222 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
(𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (1...𝑛)𝐴) ∈ dom ⇝ ) |
88 | 44, 7, 87 | esumpcvgval 30140 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = Σ𝑘 ∈ ℕ 𝐴) |
89 | 83, 88 | breqtrrd 4681 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
90 | 32 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹:ℕ⟶(0[,)+∞)) |
91 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℕ) |
92 | 91 | nnzd 11481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝑛 ∈
ℤ) |
93 | | uzid 11702 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
94 | | peano2uz 11741 |
. . . . . . . 8
⊢ (𝑛 ∈
(ℤ≥‘𝑛) → (𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
(ℤ≥‘𝑛)) |
96 | | simplll 798 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → (𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈
(0[,)+∞))) |
97 | 96, 13 | sylancom 701 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
ℕ) → 𝐴 ∈
(0[,)+∞)) |
98 | 91, 95, 97 | esumpmono 30141 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)𝐴 ≤ Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
99 | 26, 21 | eqtr4d 2659 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
100 | 99 | adantlr 751 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) = Σ*𝑘 ∈ (1...𝑛)𝐴) |
101 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑛 → (1...𝑙) = (1...𝑛)) |
102 | | esumeq1 30096 |
. . . . . . . . . . 11
⊢
((1...𝑙) =
(1...𝑛) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑛 → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...𝑛)𝐴) |
104 | 103 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) |
105 | 16, 104 | eqtr4i 2647 |
. . . . . . . 8
⊢ 𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴) |
106 | 105 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
𝐹 = (𝑙 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑙)𝐴)) |
107 | | simpr3 1069 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → 𝑙 = (𝑛 + 1)) |
108 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑙 = (𝑛 + 1) → (1...𝑙) = (1...(𝑛 + 1))) |
109 | | esumeq1 30096 |
. . . . . . . . 9
⊢
((1...𝑙) =
(1...(𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
110 | 107, 108,
109 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ (¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = (𝑛 + 1))) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
111 | 110 | 3anassrs 1290 |
. . . . . . 7
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑙 = (𝑛 + 1)) →
Σ*𝑘 ∈
(1...𝑙)𝐴 = Σ*𝑘 ∈ (1...(𝑛 + 1))𝐴) |
112 | 91 | peano2nnd 11037 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝑛 + 1) ∈
ℕ) |
113 | | ovex 6678 |
. . . . . . . 8
⊢
(1...(𝑛 + 1)) ∈
V |
114 | | simp-4l 806 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝜑) |
115 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑛 + 1)) → 𝑘 ∈ ℕ) |
116 | 115 | adantl 482 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝑘 ∈
ℕ) |
117 | 114, 116,
41 | syl2anc 693 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑛 ∈
ℕ) ∧ 𝑘 ∈
(1...(𝑛 + 1))) → 𝐴 ∈
(0[,]+∞)) |
118 | 117 | ralrimiva 2966 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
∀𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
119 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑘(1...(𝑛 + 1)) |
120 | 119 | esumcl 30092 |
. . . . . . . 8
⊢
(((1...(𝑛 + 1))
∈ V ∧ ∀𝑘
∈ (1...(𝑛 + 1))𝐴 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
121 | 113, 118,
120 | sylancr 695 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴 ∈
(0[,]+∞)) |
122 | 106, 111,
112, 121 | fvmptd 6288 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘(𝑛 + 1)) =
Σ*𝑘 ∈
(1...(𝑛 + 1))𝐴) |
123 | 98, 100, 122 | 3brtr4d 4685 |
. . . . 5
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
124 | | simpr 477 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
¬ 𝐹 ∈ dom ⇝
) |
125 | 29, 90, 123, 124 | lmdvglim 30000 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)+∞) |
126 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) |
127 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑘ℕ |
128 | | nnex 11026 |
. . . . . . . 8
⊢ ℕ
∈ V |
129 | 128 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → ℕ
∈ V) |
130 | 41 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈
(0[,]+∞)) |
131 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
132 | | simpll 790 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
133 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
(𝒫 ℕ ∩ Fin) ⊆ 𝒫 ℕ |
134 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ (𝒫 ℕ ∩
Fin)) |
135 | 133, 134 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ 𝒫 ℕ) |
136 | 135 | elpwid 4170 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ ℕ) |
137 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
138 | 136, 137 | sseldd 3604 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ ℕ) |
139 | 132, 138,
13 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
140 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑥 ↦ 𝐴) = (𝑘 ∈ 𝑥 ↦ 𝐴) |
141 | 139, 140 | fmptd 6385 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (𝑘 ∈
𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) |
142 | | esumpfinvallem 30136 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ∧ (𝑘 ∈ 𝑥 ↦ 𝐴):𝑥⟶(0[,)+∞)) →
(ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
143 | 131, 141,
142 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐴))) |
144 | | inss2 3834 |
. . . . . . . . . 10
⊢
(𝒫 ℕ ∩ Fin) ⊆ Fin |
145 | 144, 131 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → 𝑥 ∈
Fin) |
146 | 132, 138,
14 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℂ) |
147 | 145, 146 | gsumfsum 19813 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → (ℂfld Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
148 | 143, 147 | eqtr3d 2658 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (𝒫 ℕ ∩
Fin)) → ((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐴)) = Σ𝑘 ∈ 𝑥 𝐴) |
149 | 126, 127,
129, 130, 148 | esumval 30108 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
150 | 149 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 = sup(ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴), ℝ*, <
)) |
151 | 90, 123, 124 | lmdvg 29999 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
152 | 151 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛)) |
153 | | nnz 11399 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
ℤ) |
154 | | uzid 11702 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℤ → 𝑙 ∈
(ℤ≥‘𝑙)) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ℕ → 𝑙 ∈
(ℤ≥‘𝑙)) |
156 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → 𝑛 = 𝑙) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝐹‘𝑛) = (𝐹‘𝑙)) |
158 | 157 | breq2d 4665 |
. . . . . . . . . . . 12
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 = 𝑙) → (𝑦 < (𝐹‘𝑛) ↔ 𝑦 < (𝐹‘𝑙))) |
159 | 155, 158 | rspcdv 3312 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ℕ →
(∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛) → 𝑦 < (𝐹‘𝑙))) |
160 | 159 | reximia 3009 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘𝑙)𝑦 < (𝐹‘𝑛) → ∃𝑙 ∈ ℕ 𝑦 < (𝐹‘𝑙)) |
161 | 152, 160 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
𝑦 < (𝐹‘𝑙)) |
162 | | simplr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝑦 ∈
ℝ) |
163 | 90 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝐹:ℕ⟶(0[,)+∞)) |
164 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝑙 ∈
ℕ) |
165 | 163, 164 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ (0[,)+∞)) |
166 | 4, 165 | sseldi 3601 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) ∈ ℝ) |
167 | | ltle 10126 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ (𝐹‘𝑙) ∈ ℝ) → (𝑦 < (𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
168 | 162, 166,
167 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ (𝐹‘𝑙))) |
169 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → 𝐹 = (𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
170 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑙 → (1...𝑛) = (1...𝑙)) |
171 | | esumeq1 30096 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑛) =
(1...𝑙) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑙 → Σ*𝑘 ∈ (1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑛 = 𝑙) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = Σ*𝑘 ∈ (1...𝑙)𝐴) |
174 | | esumex 30091 |
. . . . . . . . . . . . . . 15
⊢
Σ*𝑘
∈ (1...𝑙)𝐴 ∈ V |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 ∈ V) |
176 | 169, 173,
164, 175 | fvmptd 6288 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ*𝑘 ∈ (1...𝑙)𝐴) |
177 | | fzfid 12772 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (1...𝑙)
∈ Fin) |
178 | | simp-4l 806 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → (𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞))) |
179 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...𝑙) → 𝑘 ∈ ℕ) |
180 | 179 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝑘 ∈
ℕ) |
181 | 178, 180,
13 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) ∧ 𝑘 ∈
(1...𝑙)) → 𝐴 ∈
(0[,)+∞)) |
182 | 177, 181 | esumpfinval 30137 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → Σ*𝑘 ∈ (1...𝑙)𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
183 | 176, 182 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝐹‘𝑙) = Σ𝑘 ∈ (1...𝑙)𝐴) |
184 | 183 | breq2d 4665 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 ≤
(𝐹‘𝑙) ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
185 | 168, 184 | sylibd 229 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑦 ∈
ℝ) ∧ 𝑙 ∈
ℕ) → (𝑦 <
(𝐹‘𝑙) → 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
186 | 185 | reximdva 3017 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
(∃𝑙 ∈ ℕ
𝑦 < (𝐹‘𝑙) → ∃𝑙 ∈ ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
187 | 161, 186 | mpd 15 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑙 ∈ ℕ
𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) |
188 | | fzssuz 12382 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ⊆
(ℤ≥‘1) |
189 | 188, 1 | sseqtr4i 3638 |
. . . . . . . . . . . . 13
⊢
(1...𝑙) ⊆
ℕ |
190 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢
(1...𝑙) ∈
V |
191 | 190 | elpw 4164 |
. . . . . . . . . . . . 13
⊢
((1...𝑙) ∈
𝒫 ℕ ↔ (1...𝑙) ⊆ ℕ) |
192 | 189, 191 | mpbir 221 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
𝒫 ℕ |
193 | | fzfi 12771 |
. . . . . . . . . . . 12
⊢
(1...𝑙) ∈
Fin |
194 | | elin 3796 |
. . . . . . . . . . . 12
⊢
((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ↔ ((1...𝑙) ∈ 𝒫 ℕ ∧ (1...𝑙) ∈ Fin)) |
195 | 192, 193,
194 | mpbir2an 955 |
. . . . . . . . . . 11
⊢
(1...𝑙) ∈
(𝒫 ℕ ∩ Fin) |
196 | | sumex 14418 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ V |
197 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴) = (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
198 | | sumeq1 14419 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1...𝑙) → Σ𝑘 ∈ 𝑥 𝐴 = Σ𝑘 ∈ (1...𝑙)𝐴) |
199 | 197, 198 | elrnmpt1s 5373 |
. . . . . . . . . . 11
⊢
(((1...𝑙) ∈
(𝒫 ℕ ∩ Fin) ∧ Σ𝑘 ∈ (1...𝑙)𝐴 ∈ V) → Σ𝑘 ∈ (1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)) |
200 | 195, 196,
199 | mp2an 708 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) |
201 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 |
202 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑧 = Σ𝑘 ∈ (1...𝑙)𝐴 → (𝑦 ≤ 𝑧 ↔ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴)) |
203 | 201, 202 | rspce 3304 |
. . . . . . . . . 10
⊢
((Σ𝑘 ∈
(1...𝑙)𝐴 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ∧ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴) → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
204 | 200, 203 | mpan 706 |
. . . . . . . . 9
⊢ (𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
205 | 204 | rexlimivw 3029 |
. . . . . . . 8
⊢
(∃𝑙 ∈
ℕ 𝑦 ≤ Σ𝑘 ∈ (1...𝑙)𝐴 → ∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
206 | 187, 205 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑦 ∈ ℝ) →
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
207 | 206 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧) |
208 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
(𝒫 ℕ ∩ Fin)) |
209 | 144, 208 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → 𝑥 ∈
Fin) |
210 | 139 | adantllr 755 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ (0[,)+∞)) |
211 | 4, 210 | sseldi 3601 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑚 ∈ ℕ
𝐵 ∈ (0[,)+∞))
∧ ¬ 𝐹 ∈ dom
⇝ ) ∧ 𝑥 ∈
(𝒫 ℕ ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐴 ∈ ℝ) |
212 | 209, 211 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈ ℝ) |
213 | 212 | rexrd 10089 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧
𝑥 ∈ (𝒫 ℕ
∩ Fin)) → Σ𝑘
∈ 𝑥 𝐴 ∈
ℝ*) |
214 | 213, 197 | fmptd 6385 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
(𝑥 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ*) |
215 | | frn 6053 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴):(𝒫 ℕ ∩
Fin)⟶ℝ* → ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴) ⊆
ℝ*) |
216 | | supxrunb1 12149 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ (𝒫
ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴) ⊆ ℝ* →
(∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞)) |
217 | 214, 215,
216 | 3syl 18 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
(∀𝑦 ∈ ℝ
∃𝑧 ∈ ran (𝑥 ∈ (𝒫 ℕ ∩
Fin) ↦ Σ𝑘
∈ 𝑥 𝐴)𝑦 ≤ 𝑧 ↔ sup(ran (𝑥 ∈ (𝒫 ℕ ∩ Fin) ↦
Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞)) |
218 | 207, 217 | mpbid 222 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
sup(ran (𝑥 ∈
(𝒫 ℕ ∩ Fin) ↦ Σ𝑘 ∈ 𝑥 𝐴), ℝ*, < ) =
+∞) |
219 | 150, 218 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
Σ*𝑘 ∈
ℕ𝐴 =
+∞) |
220 | 125, 219 | breqtrrd 4681 |
. . 3
⊢ (((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) ∧ ¬ 𝐹 ∈ dom ⇝ ) →
𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
221 | 89, 220 | pm2.61dan 832 |
. 2
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞)) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
222 | 16 | reseq1i 5392 |
. . . . . . . 8
⊢ (𝐹 ↾
(ℤ≥‘𝑘)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) |
223 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (𝑙 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
224 | 223 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝜑 ∧ 𝑙 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
225 | | sbequ12r 2112 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ([𝑙 / 𝑘]𝐴 = +∞ ↔ 𝐴 = +∞)) |
226 | 224, 225 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞))) |
227 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (ℤ≥‘𝑙) =
(ℤ≥‘𝑘)) |
228 | 227 | reseq2d 5396 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘))) |
229 | 227 | xpeq1d 5138 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((ℤ≥‘𝑙) × {+∞}) =
((ℤ≥‘𝑘) × {+∞})) |
230 | 228, 229 | eqeq12d 2637 |
. . . . . . . . . 10
⊢ (𝑙 = 𝑘 → (((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞}) ↔
((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞}))) |
231 | 226, 230 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑙 = 𝑘 → ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) × {+∞})) ↔
(((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})))) |
232 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ 𝑙 ∈ ℕ) |
233 | | nfs1v 2437 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘[𝑙 / 𝑘]𝐴 = +∞ |
234 | 232, 233 | nfan 1828 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) |
235 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘 𝑛 ∈
(ℤ≥‘𝑙) |
236 | 234, 235 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) |
237 | | ovexd 6680 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → (1...𝑛) ∈ V) |
238 | | simp-4l 806 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
239 | 18 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
240 | 238, 239,
41 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (0[,]+∞)) |
241 | | simpllr 799 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ ℕ) |
242 | | elnnuz 11724 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 ∈ ℕ ↔ 𝑙 ∈
(ℤ≥‘1)) |
243 | | eluzfz 12337 |
. . . . . . . . . . . . . . 15
⊢ ((𝑙 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
244 | 242, 243 | sylanb 489 |
. . . . . . . . . . . . . 14
⊢ ((𝑙 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
245 | 241, 244 | sylancom 701 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → 𝑙 ∈ (1...𝑛)) |
246 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → [𝑙 / 𝑘]𝐴 = +∞) |
247 | | sbequ12 2111 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑙 → (𝐴 = +∞ ↔ [𝑙 / 𝑘]𝐴 = +∞)) |
248 | 233, 247 | rspce 3304 |
. . . . . . . . . . . . 13
⊢ ((𝑙 ∈ (1...𝑛) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
249 | 245, 246,
248 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) → ∃𝑘 ∈ (1...𝑛)𝐴 = +∞) |
250 | 236, 237,
240, 249 | esumpinfval 30135 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ 𝑛 ∈ (ℤ≥‘𝑙)) →
Σ*𝑘 ∈
(1...𝑛)𝐴 = +∞) |
251 | 250 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) |
252 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) →
(ℤ≥‘𝑙) = (ℤ≥‘𝑙)) |
253 | | mpteq12 4736 |
. . . . . . . . . . . 12
⊢
(((ℤ≥‘𝑙) = (ℤ≥‘𝑙) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
254 | 252, 253 | sylan 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
255 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → 𝑙 ∈ ℕ) |
256 | | uznnssnn 11735 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ℕ →
(ℤ≥‘𝑙) ⊆ ℕ) |
257 | | resmpt 5449 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑙) ⊆ ℕ → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
258 | 255, 256,
257 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
259 | 258 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
Σ*𝑘 ∈
(1...𝑛)𝐴)) |
260 | | fconstmpt 5163 |
. . . . . . . . . . . 12
⊢
((ℤ≥‘𝑙) × {+∞}) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞) |
261 | 260 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) →
((ℤ≥‘𝑙) × {+∞}) = (𝑛 ∈ (ℤ≥‘𝑙) ↦
+∞)) |
262 | 254, 259,
261 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) ∧ ∀𝑛 ∈
(ℤ≥‘𝑙)Σ*𝑘 ∈ (1...𝑛)𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) ×
{+∞})) |
263 | 251, 262 | mpdan 702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ [𝑙 / 𝑘]𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑙)) = ((ℤ≥‘𝑙) ×
{+∞})) |
264 | 231, 263 | chvarv 2263 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → ((𝑛 ∈ ℕ ↦
Σ*𝑘 ∈
(1...𝑛)𝐴) ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
265 | 222, 264 | syl5eq 2668 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝐴 = +∞) → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) |
266 | 265 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐴 = +∞ → (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
267 | 266 | reximdva 3017 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ℕ 𝐴 = +∞ → ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞}))) |
268 | 267 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ (𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) ×
{+∞})) |
269 | | xrge0topn 29989 |
. . . . . . . . . . 11
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
270 | 29, 269 | eqtri 2644 |
. . . . . . . . . 10
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
271 | | letopon 21009 |
. . . . . . . . . . 11
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
272 | | iccssxr 12256 |
. . . . . . . . . . 11
⊢
(0[,]+∞) ⊆ ℝ* |
273 | | resttopon 20965 |
. . . . . . . . . . 11
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
(0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞))) |
274 | 271, 272,
273 | mp2an 708 |
. . . . . . . . . 10
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞)) |
275 | 270, 274 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝐽 ∈
(TopOn‘(0[,]+∞)) |
276 | 275 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐽 ∈
(TopOn‘(0[,]+∞))) |
277 | | 0xr 10086 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
278 | | pnfxr 10092 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
279 | | 0lepnf 11966 |
. . . . . . . . . 10
⊢ 0 ≤
+∞ |
280 | | ubicc2 12289 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → +∞ ∈ (0[,]+∞)) |
281 | 277, 278,
279, 280 | mp3an 1424 |
. . . . . . . . 9
⊢ +∞
∈ (0[,]+∞) |
282 | 281 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → +∞ ∈
(0[,]+∞)) |
283 | 40 | nnzd 11481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
284 | | eqid 2622 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
285 | 284 | lmconst 21065 |
. . . . . . . 8
⊢ ((𝐽 ∈
(TopOn‘(0[,]+∞)) ∧ +∞ ∈ (0[,]+∞) ∧ 𝑘 ∈ ℤ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
286 | 276, 282,
283, 285 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞) |
287 | | breq1 4656 |
. . . . . . . 8
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
((𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞ ↔
((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞)) |
288 | 287 | biimprd 238 |
. . . . . . 7
⊢ ((𝐹 ↾
(ℤ≥‘𝑘)) = ((ℤ≥‘𝑘) × {+∞}) →
(((ℤ≥‘𝑘) ×
{+∞})(⇝𝑡‘𝐽)+∞ → (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
289 | 286, 288 | mpan9 486 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) |
290 | | ovexd 6680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (0[,]+∞) ∈
V) |
291 | | cnex 10017 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
292 | 291 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℂ ∈
V) |
293 | 56 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(0[,]+∞)) |
294 | | nnsscn 11025 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℂ |
295 | 294 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ℕ ⊆
ℂ) |
296 | | elpm2r 7875 |
. . . . . . . . 9
⊢
((((0[,]+∞) ∈ V ∧ ℂ ∈ V) ∧ (𝐹:ℕ⟶(0[,]+∞)
∧ ℕ ⊆ ℂ)) → 𝐹 ∈ ((0[,]+∞)
↑pm ℂ)) |
297 | 290, 292,
293, 295, 296 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 ∈ ((0[,]+∞)
↑pm ℂ)) |
298 | 276, 297,
283 | lmres 21104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹(⇝𝑡‘𝐽)+∞ ↔ (𝐹 ↾
(ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞)) |
299 | 298 | biimpar 502 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘))(⇝𝑡‘𝐽)+∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
300 | 289, 299 | syldan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
301 | 300 | r19.29an 3077 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ (𝐹 ↾ (ℤ≥‘𝑘)) =
((ℤ≥‘𝑘) × {+∞})) → 𝐹(⇝𝑡‘𝐽)+∞) |
302 | 268, 301 | syldan 487 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)+∞) |
303 | | nfv 1843 |
. . . . 5
⊢
Ⅎ𝑘𝜑 |
304 | | nfre1 3005 |
. . . . 5
⊢
Ⅎ𝑘∃𝑘 ∈ ℕ 𝐴 = +∞ |
305 | 303, 304 | nfan 1828 |
. . . 4
⊢
Ⅎ𝑘(𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) |
306 | 128 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ℕ ∈
V) |
307 | 41 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) |
308 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → ∃𝑘 ∈ ℕ 𝐴 = +∞) |
309 | 305, 306,
307, 308 | esumpinfval 30135 |
. . 3
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → Σ*𝑘 ∈ ℕ𝐴 = +∞) |
310 | 302, 309 | breqtrrd 4681 |
. 2
⊢ ((𝜑 ∧ ∃𝑘 ∈ ℕ 𝐴 = +∞) → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |
311 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑘 ∈ ℕ ↔ 𝑚 ∈ ℕ)) |
312 | 311 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑚 ∈ ℕ))) |
313 | 7 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → (𝐴 ∈ (0[,]+∞) ↔ 𝐵 ∈
(0[,]+∞))) |
314 | 312, 313 | imbi12d 334 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)))) |
315 | 314, 41 | chvarv 2263 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ (0[,]+∞)) |
316 | | eliccelico 29539 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
≤ +∞) → (𝐵
∈ (0[,]+∞) ↔ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞))) |
317 | 277, 278,
279, 316 | mp3an 1424 |
. . . . . 6
⊢ (𝐵 ∈ (0[,]+∞) ↔
(𝐵 ∈ (0[,)+∞)
∨ 𝐵 =
+∞)) |
318 | 315, 317 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
319 | 318 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝐵 ∈ (0[,)+∞) ∨ 𝐵 = +∞)) |
320 | | r19.30 3082 |
. . . 4
⊢
(∀𝑚 ∈
ℕ (𝐵 ∈
(0[,)+∞) ∨ 𝐵 =
+∞) → (∀𝑚
∈ ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑚 ∈ ℕ 𝐵 = +∞)) |
321 | 319, 320 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
322 | 7 | eqeq1d 2624 |
. . . . 5
⊢ (𝑘 = 𝑚 → (𝐴 = +∞ ↔ 𝐵 = +∞)) |
323 | 322 | cbvrexv 3172 |
. . . 4
⊢
(∃𝑘 ∈
ℕ 𝐴 = +∞ ↔
∃𝑚 ∈ ℕ
𝐵 =
+∞) |
324 | 323 | orbi2i 541 |
. . 3
⊢
((∀𝑚 ∈
ℕ 𝐵 ∈
(0[,)+∞) ∨ ∃𝑘 ∈ ℕ 𝐴 = +∞) ↔ (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑚 ∈ ℕ
𝐵 =
+∞)) |
325 | 321, 324 | sylibr 224 |
. 2
⊢ (𝜑 → (∀𝑚 ∈ ℕ 𝐵 ∈ (0[,)+∞) ∨
∃𝑘 ∈ ℕ
𝐴 =
+∞)) |
326 | 221, 310,
325 | mpjaodan 827 |
1
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)Σ*𝑘 ∈ ℕ𝐴) |