Metamath Proof Explorer

Theorem esumcvg

Description: The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 . (Contributed by Thierry Arnoux, 5-Sep-2017)

Ref Expression
Hypotheses esumcvg.j ⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
esumcvg.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
esumcvg.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
esumcvg.m ⊢ ( 𝑘 = 𝑚 → 𝐴 = 𝐵 )
Assertion esumcvg ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )

Proof

Step Hyp Ref Expression
1 esumcvg.j ⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
2 esumcvg.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
3 esumcvg.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
4 esumcvg.m ⊢ ( 𝑘 = 𝑚 → 𝐴 = 𝐵 )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 1 ∈ ℤ )
7 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
8 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
9 ax-resscn ⊢ ℝ ⊆ ℂ
10 8 9 sstri ⊢ ( 0 [,) +∞ ) ⊆ ℂ
11 4 eleq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ 𝐵 ∈ ( 0 [,) +∞ ) ) )
12 11 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ ( 0 [,) +∞ ) ↔ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) )
13 rsp ⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ ( 0 [,) +∞ ) → ( 𝑘 ∈ ℕ → 𝐴 ∈ ( 0 [,) +∞ ) ) )
14 12 13 sylbir ⊢ ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) → ( 𝑘 ∈ ℕ → 𝐴 ∈ ( 0 [,) +∞ ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑘 ∈ ℕ → 𝐴 ∈ ( 0 [,) +∞ ) ) )
16 15 imp ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
17 10 16 sselid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ )
18 17 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ )
19 fzfid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
20 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
21 20 16 sylan2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
22 21 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
23 19 22 esumpfinval ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
24 23 mpteq2dva ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
25 2 24 syl5eq ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
26 10 22 sselid ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ℂ )
27 19 26 fsumcl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ℂ )
28 25 27 fvmpt2d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
29 28 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
30 5 6 7 18 29 isumclim3 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ Σ 𝑘 ∈ ℕ 𝐴 )
31 19 22 fsumrp0cl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,) +∞ ) )
32 23 31 eqeltrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,) +∞ ) )
33 32 2 fmptd ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
35 simplll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝜑 )
36 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑚 ∈ ℕ ↦ 𝐵 ) = ( 𝑚 ∈ ℕ ↦ 𝐵 ) )
37 eqcom ⊢ ( 𝑘 = 𝑚 ↔ 𝑚 = 𝑘 )
38 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
39 4 37 38 3imtr3i ⊢ ( 𝑚 = 𝑘 → 𝐵 = 𝐴 )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑚 = 𝑘 ) → 𝐵 = 𝐴 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
42 36 40 41 3 fvmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
43 35 42 sylancom ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
44 16 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
45 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
46 44 45 sylib ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
47 46 simpld ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
48 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
49 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
50 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
51 49 50 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
52 51 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
53 nfcv ⊢ Ⅎ 𝑘 ( 1 ... 𝑛 )
54 53 esumcl ⊢ ( ( ( 1 ... 𝑛 ) ∈ V ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
55 48 52 54 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
56 55 2 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
57 56 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℕ )
58 57 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐹 Fn ℕ )
59 1z ⊢ 1 ∈ ℤ
60 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) )
61 59 60 ax-mp ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 )
62 5 fneq2i ⊢ ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) )
63 61 62 mpbir ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ
64 63 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ )
65 simplll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
66 20 42 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑚 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
67 65 66 sylancom ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑚 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
68 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
69 68 5 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
70 67 69 26 fsumser ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
71 28 70 eqtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
72 58 64 71 eqfnfvd ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐹 = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) )
74 73 7 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ 𝐵 ) ) ∈ dom ⇝ )
75 5 6 43 47 74 isumrecl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ )
76 46 simprd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ 𝐴 )
77 5 6 43 47 74 76 isumge0 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 0 ≤ Σ 𝑘 ∈ ℕ 𝐴 )
78 elrege0 ⊢ ( Σ 𝑘 ∈ ℕ 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ℕ 𝐴 ) )
79 75 77 78 sylanbrc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → Σ 𝑘 ∈ ℕ 𝐴 ∈ ( 0 [,) +∞ ) )
80 ssid ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,) +∞ )
81 1 34 79 80 lmlimxrge0 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ 𝑘 ∈ ℕ 𝐴 ↔ 𝐹 ⇝ Σ 𝑘 ∈ ℕ 𝐴 ) )
82 30 81 mpbird ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ 𝑘 ∈ ℕ 𝐴 )
83 2 7 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ )
84 24 eleq1d ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ ↔ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ ) )
85 84 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ ↔ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ ) )
86 83 85 mpbid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ )
87 44 4 86 esumpcvgval ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )
88 82 87 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )
89 33 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
90 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
91 90 nnzd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
92 uzid ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) )
93 peano2uz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
94 91 92 93 3syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
95 simplll ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) )
96 95 16 sylancom ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
97 90 94 96 esumpmono ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 )
98 28 23 eqtr4d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
99 98 adantlr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
100 oveq2 ⊢ ( 𝑙 = 𝑛 → ( 1 ... 𝑙 ) = ( 1 ... 𝑛 ) )
101 esumeq1 ⊢ ( ( 1 ... 𝑙 ) = ( 1 ... 𝑛 ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
102 100 101 syl ⊢ ( 𝑙 = 𝑛 → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
103 102 cbvmptv ⊢ ( 𝑙 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
104 2 103 eqtr4i ⊢ 𝐹 = ( 𝑙 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
105 104 a1i ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → 𝐹 = ( 𝑙 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) )
106 simpr3 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ( ¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = ( 𝑛 + 1 ) ) ) → 𝑙 = ( 𝑛 + 1 ) )
107 oveq2 ⊢ ( 𝑙 = ( 𝑛 + 1 ) → ( 1 ... 𝑙 ) = ( 1 ... ( 𝑛 + 1 ) ) )
108 esumeq1 ⊢ ( ( 1 ... 𝑙 ) = ( 1 ... ( 𝑛 + 1 ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 )
109 106 107 108 3syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ( ¬ 𝐹 ∈ dom ⇝ ∧ 𝑛 ∈ ℕ ∧ 𝑙 = ( 𝑛 + 1 ) ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 )
110 109 3anassrs ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 = ( 𝑛 + 1 ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 )
111 90 peano2nnd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
112 ovex ⊢ ( 1 ... ( 𝑛 + 1 ) ) ∈ V
113 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝜑 )
114 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) → 𝑘 ∈ ℕ )
115 114 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ )
116 113 115 3 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
117 116 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 ∈ ( 0 [,] +∞ ) )
118 nfcv ⊢ Ⅎ 𝑘 ( 1 ... ( 𝑛 + 1 ) )
119 118 esumcl ⊢ ( ( ( 1 ... ( 𝑛 + 1 ) ) ∈ V ∧ ∀ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 ∈ ( 0 [,] +∞ ) )
120 112 117 119 sylancr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 ∈ ( 0 [,] +∞ ) )
121 105 110 111 120 fvmptd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = Σ* 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) 𝐴 )
122 97 99 121 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
123 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → ¬ 𝐹 ∈ dom ⇝ )
124 1 89 122 123 lmdvglim ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )
125 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) )
126 nfcv ⊢ Ⅎ 𝑘 ℕ
127 nnex ⊢ ℕ ∈ V
128 127 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → ℕ ∈ V )
129 3 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
130 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) )
131 simpll ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) )
132 inss1 ⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ 𝒫 ℕ
133 simplr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) )
134 132 133 sselid ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ∈ 𝒫 ℕ )
135 134 elpwid ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ⊆ ℕ )
136 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑥 )
137 135 136 sseldd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ ℕ )
138 131 137 16 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
139 138 fmpttd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) : 𝑥 ⟶ ( 0 [,) +∞ ) )
140 esumpfinvallem ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ∧ ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) : 𝑥 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) )
141 130 139 140 syl2anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) )
142 inss2 ⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ Fin
143 142 130 sselid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ∈ Fin )
144 131 137 17 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐴 ∈ ℂ )
145 143 144 gsumfsum ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑥 𝐴 )
146 141 145 eqtr3d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑥 𝐴 )
147 125 126 128 129 146 esumval ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) , ℝ* , < ) )
148 147 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) , ℝ* , < ) )
149 89 122 123 lmdvg ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑙 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) 𝑦 < ( 𝐹 ‘ 𝑛 ) )
150 149 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑙 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) 𝑦 < ( 𝐹 ‘ 𝑛 ) )
151 nnz ⊢ ( 𝑙 ∈ ℕ → 𝑙 ∈ ℤ )
152 uzid ⊢ ( 𝑙 ∈ ℤ → 𝑙 ∈ ( ℤ≥ ‘ 𝑙 ) )
153 151 152 syl ⊢ ( 𝑙 ∈ ℕ → 𝑙 ∈ ( ℤ≥ ‘ 𝑙 ) )
154 simpr ⊢ ( ( 𝑙 ∈ ℕ ∧ 𝑛 = 𝑙 ) → 𝑛 = 𝑙 )
155 154 fveq2d ⊢ ( ( 𝑙 ∈ ℕ ∧ 𝑛 = 𝑙 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑙 ) )
156 155 breq2d ⊢ ( ( 𝑙 ∈ ℕ ∧ 𝑛 = 𝑙 ) → ( 𝑦 < ( 𝐹 ‘ 𝑛 ) ↔ 𝑦 < ( 𝐹 ‘ 𝑙 ) ) )
157 153 156 rspcdv ⊢ ( 𝑙 ∈ ℕ → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) 𝑦 < ( 𝐹 ‘ 𝑛 ) → 𝑦 < ( 𝐹 ‘ 𝑙 ) ) )
158 157 reximia ⊢ ( ∃ 𝑙 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) 𝑦 < ( 𝐹 ‘ 𝑛 ) → ∃ 𝑙 ∈ ℕ 𝑦 < ( 𝐹 ‘ 𝑙 ) )
159 150 158 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑙 ∈ ℕ 𝑦 < ( 𝐹 ‘ 𝑙 ) )
160 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → 𝑦 ∈ ℝ )
161 89 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
162 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → 𝑙 ∈ ℕ )
163 161 162 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) ∈ ( 0 [,) +∞ ) )
164 8 163 sselid ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ )
165 ltle ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑙 ) ∈ ℝ ) → ( 𝑦 < ( 𝐹 ‘ 𝑙 ) → 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
166 160 164 165 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝑦 < ( 𝐹 ‘ 𝑙 ) → 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
167 oveq2 ⊢ ( 𝑛 = 𝑙 → ( 1 ... 𝑛 ) = ( 1 ... 𝑙 ) )
168 esumeq1 ⊢ ( ( 1 ... 𝑛 ) = ( 1 ... 𝑙 ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
169 167 168 syl ⊢ ( 𝑛 = 𝑙 → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
170 esumex ⊢ Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ V
171 170 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ V )
172 2 169 162 171 fvmptd3 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) = Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
173 fzfid ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 1 ... 𝑙 ) ∈ Fin )
174 simp-4l ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑙 ) ) → ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) )
175 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑙 ) → 𝑘 ∈ ℕ )
176 175 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑙 ) ) → 𝑘 ∈ ℕ )
177 174 176 16 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑙 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
178 173 177 esumpfinval ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
179 172 178 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) = Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
180 179 breq2d ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) )
181 166 180 sylibd ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ ℕ ) → ( 𝑦 < ( 𝐹 ‘ 𝑙 ) → 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) )
182 181 reximdva ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑙 ∈ ℕ 𝑦 < ( 𝐹 ‘ 𝑙 ) → ∃ 𝑙 ∈ ℕ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) )
183 159 182 mpd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑙 ∈ ℕ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
184 fzssuz ⊢ ( 1 ... 𝑙 ) ⊆ ( ℤ≥ ‘ 1 )
185 184 5 sseqtrri ⊢ ( 1 ... 𝑙 ) ⊆ ℕ
186 ovex ⊢ ( 1 ... 𝑙 ) ∈ V
187 186 elpw ⊢ ( ( 1 ... 𝑙 ) ∈ 𝒫 ℕ ↔ ( 1 ... 𝑙 ) ⊆ ℕ )
188 185 187 mpbir ⊢ ( 1 ... 𝑙 ) ∈ 𝒫 ℕ
189 fzfi ⊢ ( 1 ... 𝑙 ) ∈ Fin
190 elin ⊢ ( ( 1 ... 𝑙 ) ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( ( 1 ... 𝑙 ) ∈ 𝒫 ℕ ∧ ( 1 ... 𝑙 ) ∈ Fin ) )
191 188 189 190 mpbir2an ⊢ ( 1 ... 𝑙 ) ∈ ( 𝒫 ℕ ∩ Fin )
192 sumex ⊢ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ V
193 eqid ⊢ ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) = ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 )
194 sumeq1 ⊢ ( 𝑥 = ( 1 ... 𝑙 ) → Σ 𝑘 ∈ 𝑥 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 )
195 193 194 elrnmpt1s ⊢ ( ( ( 1 ... 𝑙 ) ∈ ( 𝒫 ℕ ∩ Fin ) ∧ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ V ) → Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) )
196 191 192 195 mp2an ⊢ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 )
197 nfv ⊢ Ⅎ 𝑧 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴
198 breq2 ⊢ ( 𝑧 = Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) )
199 197 198 rspce ⊢ ( ( Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) ∧ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 )
200 196 199 mpan ⊢ ( 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 )
201 200 rexlimivw ⊢ ( ∃ 𝑙 ∈ ℕ 𝑦 ≤ Σ 𝑘 ∈ ( 1 ... 𝑙 ) 𝐴 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 )
202 183 201 syl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 )
203 202 ralrimiva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 )
204 simpr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) )
205 142 204 sselid ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑥 ∈ Fin )
206 138 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
207 8 206 sselid ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐴 ∈ ℝ )
208 205 207 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐴 ∈ ℝ )
209 208 rexrd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ) → Σ 𝑘 ∈ 𝑥 𝐴 ∈ ℝ* )
210 209 fmpttd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) : ( 𝒫 ℕ ∩ Fin ) ⟶ ℝ* )
211 frn ⊢ ( ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) : ( 𝒫 ℕ ∩ Fin ) ⟶ ℝ* → ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) ⊆ ℝ* )
212 supxrunb1 ⊢ ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) ⊆ ℝ* → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) , ℝ* , < ) = +∞ ) )
213 210 211 212 3syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) 𝑦 ≤ 𝑧 ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) , ℝ* , < ) = +∞ ) )
214 203 213 mpbid ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → sup ( ran ( 𝑥 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑥 𝐴 ) , ℝ* , < ) = +∞ )
215 148 214 eqtrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → Σ* 𝑘 ∈ ℕ 𝐴 = +∞ )
216 124 215 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) ∧ ¬ 𝐹 ∈ dom ⇝ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )
217 88 216 pm2.61dan ⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )
218 2 reseq1i ⊢ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑘 ) )
219 eleq1w ⊢ ( 𝑙 = 𝑘 → ( 𝑙 ∈ ℕ ↔ 𝑘 ∈ ℕ ) )
220 219 anbi2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑘 ∈ ℕ ) ) )
221 sbequ12r ⊢ ( 𝑙 = 𝑘 → ( [ 𝑙 / 𝑘 ] 𝐴 = +∞ ↔ 𝐴 = +∞ ) )
222 220 221 anbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝐴 = +∞ ) ) )
223 fveq2 ⊢ ( 𝑙 = 𝑘 → ( ℤ≥ ‘ 𝑙 ) = ( ℤ≥ ‘ 𝑘 ) )
224 223 reseq2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) )
225 223 xpeq1d ⊢ ( 𝑙 = 𝑘 → ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) )
226 224 225 eqeq12d ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) ↔ ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) )
227 222 226 imbi12d ⊢ ( 𝑙 = 𝑘 → ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) ) ↔ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) ) )
228 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑙 ∈ ℕ )
229 nfs1v ⊢ Ⅎ 𝑘 [ 𝑙 / 𝑘 ] 𝐴 = +∞
230 228 229 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ )
231 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ( ℤ≥ ‘ 𝑙 )
232 230 231 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) )
233 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → ( 1 ... 𝑛 ) ∈ V )
234 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
235 20 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
236 234 235 3 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
237 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → 𝑙 ∈ ℕ )
238 elnnuz ⊢ ( 𝑙 ∈ ℕ ↔ 𝑙 ∈ ( ℤ≥ ‘ 1 ) )
239 eluzfz ⊢ ( ( 𝑙 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → 𝑙 ∈ ( 1 ... 𝑛 ) )
240 238 239 sylanb ⊢ ( ( 𝑙 ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → 𝑙 ∈ ( 1 ... 𝑛 ) )
241 237 240 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → 𝑙 ∈ ( 1 ... 𝑛 ) )
242 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → [ 𝑙 / 𝑘 ] 𝐴 = +∞ )
243 sbequ12 ⊢ ( 𝑘 = 𝑙 → ( 𝐴 = +∞ ↔ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) )
244 229 243 rspce ⊢ ( ( 𝑙 ∈ ( 1 ... 𝑛 ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ∃ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ )
245 241 242 244 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → ∃ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ )
246 232 233 236 245 esumpinfval ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ )
247 246 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ )
248 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ( ℤ≥ ‘ 𝑙 ) = ( ℤ≥ ‘ 𝑙 ) )
249 mpteq12 ⊢ ( ( ( ℤ≥ ‘ 𝑙 ) = ( ℤ≥ ‘ 𝑙 ) ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ +∞ ) )
250 248 249 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ +∞ ) )
251 simplr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → 𝑙 ∈ ℕ )
252 uznnssnn ⊢ ( 𝑙 ∈ ℕ → ( ℤ≥ ‘ 𝑙 ) ⊆ ℕ )
253 resmpt ⊢ ( ( ℤ≥ ‘ 𝑙 ) ⊆ ℕ → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
254 251 252 253 3syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
255 254 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
256 fconstmpt ⊢ ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ +∞ )
257 256 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ ) → ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) ↦ +∞ ) )
258 250 255 257 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑙 ) Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) )
259 247 258 mpdan ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ [ 𝑙 / 𝑘 ] 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑙 ) ) = ( ( ℤ≥ ‘ 𝑙 ) × { +∞ } ) )
260 227 259 chvarvv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝐴 = +∞ ) → ( ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) )
261 218 260 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝐴 = +∞ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) )
262 261 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐴 = +∞ → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) )
263 262 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℕ 𝐴 = +∞ → ∃ 𝑘 ∈ ℕ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) )
264 263 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → ∃ 𝑘 ∈ ℕ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) )
265 xrge0topn ⊢ ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
266 1 265 eqtri ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
267 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
268 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
269 resttopon ⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) )
270 267 268 269 mp2an ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
271 266 270 eqeltri ⊢ 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) )
272 271 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) )
273 0xr ⊢ 0 ∈ ℝ*
274 pnfxr ⊢ +∞ ∈ ℝ*
275 0lepnf ⊢ 0 ≤ +∞
276 ubicc2 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
277 273 274 275 276 mp3an ⊢ +∞ ∈ ( 0 [,] +∞ )
278 277 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → +∞ ∈ ( 0 [,] +∞ ) )
279 41 nnzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
280 eqid ⊢ ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑘 )
281 280 lmconst ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( 0 [,] +∞ ) ) ∧ +∞ ∈ ( 0 [,] +∞ ) ∧ 𝑘 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ( ⇝𝑡 ‘ 𝐽 ) +∞ )
282 272 278 279 281 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ( ⇝𝑡 ‘ 𝐽 ) +∞ )
283 breq1 ⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) ( ⇝𝑡 ‘ 𝐽 ) +∞ ↔ ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ( ⇝𝑡 ‘ 𝐽 ) +∞ ) )
284 283 biimprd ⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) → ( ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ( ⇝𝑡 ‘ 𝐽 ) +∞ → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) ( ⇝𝑡 ‘ 𝐽 ) +∞ ) )
285 282 284 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) ( ⇝𝑡 ‘ 𝐽 ) +∞ )
286 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 0 [,] +∞ ) ∈ V )
287 cnex ⊢ ℂ ∈ V
288 287 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ℂ ∈ V )
289 56 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
290 nnsscn ⊢ ℕ ⊆ ℂ
291 290 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ℕ ⊆ ℂ )
292 elpm2r ⊢ ( ( ( ( 0 [,] +∞ ) ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) ∧ ℕ ⊆ ℂ ) ) → 𝐹 ∈ ( ( 0 [,] +∞ ) ↑pm ℂ ) )
293 286 288 289 291 292 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 ∈ ( ( 0 [,] +∞ ) ↑pm ℂ ) )
294 272 293 279 lmres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) ( ⇝𝑡 ‘ 𝐽 ) +∞ ) )
295 294 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) ( ⇝𝑡 ‘ 𝐽 ) +∞ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )
296 285 295 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )
297 296 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( ( ℤ≥ ‘ 𝑘 ) × { +∞ } ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )
298 264 297 syldan ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )
299 nfv ⊢ Ⅎ 𝑘 𝜑
300 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ℕ 𝐴 = +∞
301 299 300 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ )
302 127 a1i ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → ℕ ∈ V )
303 3 adantlr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
304 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → ∃ 𝑘 ∈ ℕ 𝐴 = +∞ )
305 301 302 303 304 esumpinfval ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → Σ* 𝑘 ∈ ℕ 𝐴 = +∞ )
306 298 305 breqtrrd ⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )
307 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ ℕ ↔ 𝑚 ∈ ℕ ) )
308 307 anbi2d ⊢ ( 𝑘 = 𝑚 → ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ↔ ( 𝜑 ∧ 𝑚 ∈ ℕ ) ) )
309 4 eleq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ 𝐵 ∈ ( 0 [,] +∞ ) ) )
310 308 309 imbi12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ) )
311 310 3 chvarvv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐵 ∈ ( 0 [,] +∞ ) )
312 eliccelico ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 ∈ ( 0 [,) +∞ ) ∨ 𝐵 = +∞ ) ) )
313 273 274 275 312 mp3an ⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 ∈ ( 0 [,) +∞ ) ∨ 𝐵 = +∞ ) )
314 311 313 sylib ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐵 ∈ ( 0 [,) +∞ ) ∨ 𝐵 = +∞ ) )
315 314 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝐵 ∈ ( 0 [,) +∞ ) ∨ 𝐵 = +∞ ) )
316 r19.30 ⊢ ( ∀ 𝑚 ∈ ℕ ( 𝐵 ∈ ( 0 [,) +∞ ) ∨ 𝐵 = +∞ ) → ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ∨ ∃ 𝑚 ∈ ℕ 𝐵 = +∞ ) )
317 315 316 syl ⊢ ( 𝜑 → ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ∨ ∃ 𝑚 ∈ ℕ 𝐵 = +∞ ) )
318 4 eqeq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐴 = +∞ ↔ 𝐵 = +∞ ) )
319 318 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ↔ ∃ 𝑚 ∈ ℕ 𝐵 = +∞ )
320 319 orbi2i ⊢ ( ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ∨ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) ↔ ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ∨ ∃ 𝑚 ∈ ℕ 𝐵 = +∞ ) )
321 317 320 sylibr ⊢ ( 𝜑 → ( ∀ 𝑚 ∈ ℕ 𝐵 ∈ ( 0 [,) +∞ ) ∨ ∃ 𝑘 ∈ ℕ 𝐴 = +∞ ) )
322 217 306 321 mpjaodan ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )