Metamath Proof Explorer

Theorem rge0scvg

Description: Implication of convergence for a nonnegative series. This could be used to shorten prmreclem6 . (Contributed by Thierry Arnoux, 28-Jul-2017)

Ref Expression
Assertion rge0scvg ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
2 1zzd ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → 1 ∈ ℤ )
3 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
4 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℕ ⟶ ℝ )
5 3 4 mpan2 ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → 𝐹 : ℕ ⟶ ℝ )
6 5 ffvelrnda ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
7 1 2 6 serfre ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
8 7 frnd ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ran seq 1 ( + , 𝐹 ) ⊆ ℝ )
9 8 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ran seq 1 ( + , 𝐹 ) ⊆ ℝ )
10 1nn ⊢ 1 ∈ ℕ
11 fdm ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → dom seq 1 ( + , 𝐹 ) = ℕ )
12 10 11 eleqtrrid ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → 1 ∈ dom seq 1 ( + , 𝐹 ) )
13 ne0i ⊢ ( 1 ∈ dom seq 1 ( + , 𝐹 ) → dom seq 1 ( + , 𝐹 ) ≠ ∅ )
14 dm0rn0 ⊢ ( dom seq 1 ( + , 𝐹 ) = ∅ ↔ ran seq 1 ( + , 𝐹 ) = ∅ )
15 14 necon3bii ⊢ ( dom seq 1 ( + , 𝐹 ) ≠ ∅ ↔ ran seq 1 ( + , 𝐹 ) ≠ ∅ )
16 13 15 sylib ⊢ ( 1 ∈ dom seq 1 ( + , 𝐹 ) → ran seq 1 ( + , 𝐹 ) ≠ ∅ )
17 7 12 16 3syl ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ran seq 1 ( + , 𝐹 ) ≠ ∅ )
18 17 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ran seq 1 ( + , 𝐹 ) ≠ ∅ )
19 1zzd ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → 1 ∈ ℤ )
20 climdm ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
21 20 biimpi ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
22 21 adantl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
23 7 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
24 23 ffvelrnda ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
25 1 19 22 24 climrecl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ )
26 simpr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
27 22 adantr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
28 simplll ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
29 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
30 3 29 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
31 28 30 sylancom ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
32 elrege0 ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑗 ) ) )
33 32 simprbi ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
34 29 33 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
35 34 adantlr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
36 35 adantlr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
37 1 26 27 31 36 climserle ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
38 37 ralrimiva ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
39 brralrspcev ⊢ ( ( ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
40 25 38 39 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
41 ffn ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → seq 1 ( + , 𝐹 ) Fn ℕ )
42 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
43 42 ralrn ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
44 7 41 43 3syl ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
45 44 rexbidv ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
46 45 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
47 40 46 mpbird ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 )
48 suprcl ⊢ ( ( ran seq 1 ( + , 𝐹 ) ⊆ ℝ ∧ ran seq 1 ( + , 𝐹 ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )
49 9 18 47 48 syl3anc ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )