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 ffvelcdmda ⊢ ( ( 𝐹 : ℕ ⟶ ( 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 bilani ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
22 7 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
23 22 ffvelcdmda ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
24 1 19 21 23 climrecl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ )
25 simpr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
26 21 adantr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
27 simplll ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
28 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) )
29 3 28 sselid ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
30 27 29 sylancom ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
31 elrege0 ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑗 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑗 ) ) )
32 31 simprbi ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
33 28 32 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
34 33 adantlr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
35 34 adantlr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
36 1 25 26 30 35 climserle ⊢ ( ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
37 36 ralrimiva ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
38 brralrspcev ⊢ ( ( ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
39 24 37 38 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
40 ffn ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → seq 1 ( + , 𝐹 ) Fn ℕ )
41 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
42 41 ralrn ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
43 7 40 42 3syl ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
44 43 rexbidv ⊢ ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
45 44 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
46 39 45 mpbird ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 )
47 suprcl ⊢ ( ( ran seq 1 ( + , 𝐹 ) ⊆ ℝ ∧ ran seq 1 ( + , 𝐹 ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )
48 9 18 46 47 syl3anc ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ seq 1 ( + , 𝐹 ) ∈ dom ⇝ ) → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )