Metamath Proof Explorer

Theorem climcnds

Description: The Cauchy condensation test. If a ( k ) is a decreasing sequence of nonnegative terms, then sum_ k e. NN a ( k ) converges iff sum_ n e. NN0 2 ^ n x. a ( 2 ^ n ) converges. (Contributed by Mario Carneiro, 18-Jul-2014) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Hypotheses climcnds.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climcnds.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
climcnds.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
climcnds.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
Assertion climcnds ( 𝜑 → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) )

Proof

Step Hyp Ref Expression
1 climcnds.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
2 climcnds.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
3 climcnds.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
4 climcnds.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 1zzd ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → 1 ∈ ℤ )
7 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
8 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
9 2nn ⊢ 2 ∈ ℕ
10 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
11 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
12 9 10 11 sylancr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
13 12 nnred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
14 fveq2 ⊢ ( 𝑘 = ( 2 ↑ 𝑛 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) )
15 14 eleq1d ⊢ ( 𝑘 = ( 2 ↑ 𝑛 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ∈ ℝ ) )
16 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
18 15 17 12 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ∈ ℝ )
19 13 18 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
20 4 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
21 8 20 sylan2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
22 5 7 21 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
25 24 5 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
26 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
28 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
29 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
30 27 28 29 3syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
31 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝜑 )
32 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( 𝑗 + 1 ) ) → 𝑛 ∈ ℕ )
33 31 32 21 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... ( 𝑗 + 1 ) ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
34 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝜑 )
35 elfz1eq ⊢ ( 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) → 𝑛 = ( 𝑗 + 1 ) )
36 35 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝑛 = ( 𝑗 + 1 ) )
37 nnnn0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
38 peano2nn0 ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
39 37 38 syl ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ0 )
40 39 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
41 36 40 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝑛 ∈ ℕ0 )
42 12 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ0 )
43 42 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 2 ↑ 𝑛 ) )
44 14 breq2d ⊢ ( 𝑘 = ( 2 ↑ 𝑛 ) → ( 0 ≤ ( 𝐹 ‘ 𝑘 ) ↔ 0 ≤ ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
45 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ 0 ≤ ( 𝐹 ‘ 𝑘 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ 0 ≤ ( 𝐹 ‘ 𝑘 ) )
47 44 46 12 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) )
48 13 18 43 47 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( ( 2 ↑ 𝑛 ) · ( 𝐹 ‘ ( 2 ↑ 𝑛 ) ) ) )
49 48 4 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 𝐺 ‘ 𝑛 ) )
50 34 41 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 0 ≤ ( 𝐺 ‘ 𝑛 ) )
51 25 30 33 50 sermono ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) )
52 51 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐺 ) ‘ ( 𝑗 + 1 ) ) )
53 2re ⊢ 2 ∈ ℝ
54 eqidd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
55 1 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
56 simpr ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
57 5 6 54 55 56 isumrecl ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
58 remulcl ⊢ ( ( 2 ∈ ℝ ∧ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
59 53 57 58 sylancr ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
60 23 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ )
61 5 7 1 serfre ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
62 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
63 37 adantl ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
64 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
65 9 63 64 sylancr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ℕ )
66 62 65 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℝ )
67 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ∈ ℝ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∈ ℝ )
68 53 66 67 sylancr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ∈ ℝ )
69 59 adantr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
70 1 2 3 4 climcndslem2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) )
71 70 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) )
72 eqidd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
73 65 5 eleqtrdi ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ 𝑗 ) ∈ ( ℤ≥ ‘ 1 ) )
74 simpll ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝜑 )
75 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) → 𝑘 ∈ ℕ )
76 1 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
77 74 75 76 syl2an ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
78 72 73 77 fsumser ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) )
79 1zzd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℤ )
80 fzfid ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 1 ... ( 2 ↑ 𝑗 ) ) ∈ Fin )
81 75 ssriv ⊢ ( 1 ... ( 2 ↑ 𝑗 ) ) ⊆ ℕ
82 81 a1i ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 1 ... ( 2 ↑ 𝑗 ) ) ⊆ ℕ )
83 eqidd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
84 1 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
85 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
86 simplr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
87 5 79 80 82 83 84 85 86 isumless ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... ( 2 ↑ 𝑗 ) ) ( 𝐹 ‘ 𝑘 ) ≤ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
88 78 87 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ≤ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) )
89 57 adantr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
90 2rp ⊢ 2 ∈ ℝ+
91 90 a1i ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ+ )
92 66 89 91 lemul2d ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ≤ Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ↔ ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ≤ ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ) )
93 88 92 mpbid ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 · ( seq 1 ( + , 𝐹 ) ‘ ( 2 ↑ 𝑗 ) ) ) ≤ ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) )
94 60 68 69 71 93 letrd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) )
95 94 ralrimiva ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) )
96 brralrspcev ⊢ ( ( ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ ( 2 · Σ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ 𝑥 )
97 59 95 96 syl2anc ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐺 ) ‘ 𝑗 ) ≤ 𝑥 )
98 5 6 23 52 97 climsup ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐺 ) ⇝ sup ( ran seq 1 ( + , 𝐺 ) , ℝ , < ) )
99 climrel ⊢ Rel ⇝
100 99 releldmi ⊢ ( seq 1 ( + , 𝐺 ) ⇝ sup ( ran seq 1 ( + , 𝐺 ) , ℝ , < ) → seq 1 ( + , 𝐺 ) ∈ dom ⇝ )
101 98 100 syl ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐺 ) ∈ dom ⇝ )
102 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
103 1nn0 ⊢ 1 ∈ ℕ0
104 103 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
105 20 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
106 102 104 105 iserex ⊢ ( 𝜑 → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐺 ) ∈ dom ⇝ ) )
107 106 biimpar ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
108 101 107 syldan ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
109 1zzd ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → 1 ∈ ℤ )
110 61 adantr ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
111 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( 𝑗 + 1 ) ) → 𝑘 ∈ ℕ )
112 31 111 1 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
113 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝜑 )
114 peano2nn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 + 1 ) ∈ ℕ )
115 114 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ )
116 elfz1eq ⊢ ( 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) → 𝑘 = ( 𝑗 + 1 ) )
117 eleq1 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑘 ∈ ℕ ↔ ( 𝑗 + 1 ) ∈ ℕ ) )
118 117 biimparc ⊢ ( ( ( 𝑗 + 1 ) ∈ ℕ ∧ 𝑘 = ( 𝑗 + 1 ) ) → 𝑘 ∈ ℕ )
119 115 116 118 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ℕ )
120 113 119 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
121 25 30 112 120 sermono ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) )
122 121 adantlr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) )
123 0zd ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → 0 ∈ ℤ )
124 eqidd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
125 20 adantlr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
126 simpr ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
127 102 123 124 125 126 isumrecl ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
128 110 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
129 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
130 102 129 20 serfre ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℝ )
131 130 adantr ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℝ )
132 ffvelcdm ⊢ ( ( seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℝ ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ )
133 131 37 132 syl2an ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ )
134 127 adantr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
135 110 adantr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
136 simpr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
137 26 adantl ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
138 39 adantl ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ0 )
139 138 nn0red ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℝ )
140 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
141 9 138 140 sylancr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
142 141 nnred ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℝ )
143 2z ⊢ 2 ∈ ℤ
144 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
145 143 144 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
146 bernneq3 ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 𝑗 + 1 ) < ( 2 ↑ ( 𝑗 + 1 ) ) )
147 145 138 146 sylancr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) < ( 2 ↑ ( 𝑗 + 1 ) ) )
148 139 142 147 ltled ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) )
149 137 peano2zd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℤ )
150 141 nnzd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℤ )
151 eluz ⊢ ( ( ( 𝑗 + 1 ) ∈ ℤ ∧ ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℤ ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ↔ ( 𝑗 + 1 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
152 149 150 151 syl2anc ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ↔ ( 𝑗 + 1 ) ≤ ( 2 ↑ ( 𝑗 + 1 ) ) ) )
153 148 152 mpbird ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
154 eluzp1m1 ⊢ ( ( 𝑗 ∈ ℤ ∧ ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
155 137 153 154 syl2anc ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
156 eluznn ⊢ ( ( 𝑗 ∈ ℕ ∧ ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ∈ ℕ )
157 136 155 156 syl2anc ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ∈ ℕ )
158 135 157 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ∈ ℝ )
159 25 adantlr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
160 simpll ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝜑 )
161 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) → 𝑘 ∈ ℕ )
162 160 161 1 syl2an ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
163 114 adantl ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑗 + 1 ) ∈ ℕ )
164 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
165 eluznn ⊢ ( ( ( 𝑗 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ℕ )
166 163 164 165 syl2an ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → 𝑘 ∈ ℕ )
167 160 166 2 syl2an2r ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
168 159 155 162 167 sermono ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 1 ( + , 𝐹 ) ‘ ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) )
169 37 adantl ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
170 1 2 3 4 climcndslem1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( seq 1 ( + , 𝐹 ) ‘ ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ≤ ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) )
171 160 169 170 syl2anc ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ ( ( 2 ↑ ( 𝑗 + 1 ) ) − 1 ) ) ≤ ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) )
172 128 158 133 168 171 letrd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) )
173 eqidd ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 0 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
174 169 102 eleqtrdi ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
175 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... 𝑗 ) → 𝑛 ∈ ℕ0 )
176 160 175 105 syl2an ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ( 0 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
177 173 174 176 fsumser ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑛 ∈ ( 0 ... 𝑗 ) ( 𝐺 ‘ 𝑛 ) = ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) )
178 0zd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 0 ∈ ℤ )
179 fzfid ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 0 ... 𝑗 ) ∈ Fin )
180 175 ssriv ⊢ ( 0 ... 𝑗 ) ⊆ ℕ0
181 180 a1i ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( 0 ... 𝑗 ) ⊆ ℕ0 )
182 eqidd ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
183 20 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
184 49 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( 𝐺 ‘ 𝑛 ) )
185 simplr ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
186 102 178 179 181 182 183 184 185 isumless ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → Σ 𝑛 ∈ ( 0 ... 𝑗 ) ( 𝐺 ‘ 𝑛 ) ≤ Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) )
187 177 186 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑗 ) ≤ Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) )
188 128 133 134 172 187 letrd ⊢ ( ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) )
189 188 ralrimiva ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) )
190 brralrspcev ⊢ ( ( Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) ∈ ℝ ∧ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ Σ 𝑛 ∈ ℕ0 ( 𝐺 ‘ 𝑛 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ 𝑥 )
191 127 189 190 syl2anc ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ≤ 𝑥 )
192 5 109 110 122 191 climsup ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) ⇝ sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) )
193 99 releldmi ⊢ ( seq 1 ( + , 𝐹 ) ⇝ sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
194 192 193 syl ⊢ ( ( 𝜑 ∧ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
195 108 194 impbida ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 0 ( + , 𝐺 ) ∈ dom ⇝ ) )