This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iseraltlem1

Description: Lemma for iseralt . A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
Assertion iseraltlem1 ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 0 ≤ ( 𝐺 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
4 iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
5 iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
6 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
7 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8 7 1 eleq2s ⊢ ( 𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝑁 ∈ ℤ )
10 5 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝐺 ⇝ 0 )
11 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑁 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑁 ) ∈ ℂ )
13 1z ⊢ 1 ∈ ℤ
14 uzssz ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℤ
15 zex ⊢ ℤ ∈ V
16 14 15 climconst2 ⊢ ( ( ( 𝐺 ‘ 𝑁 ) ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ⇝ ( 𝐺 ‘ 𝑁 ) )
17 12 13 16 sylancl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ⇝ ( 𝐺 ‘ 𝑁 ) )
18 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐺 : 𝑍 ⟶ ℝ )
19 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
20 19 adantll ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ 𝑍 )
21 18 20 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
22 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑛 ∈ ℤ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℤ )
24 fvex ⊢ ( 𝐺 ‘ 𝑁 ) ∈ V
25 24 fvconst2 ⊢ ( 𝑛 ∈ ℤ → ( ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ‘ 𝑛 ) = ( 𝐺 ‘ 𝑁 ) )
26 23 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ‘ 𝑛 ) = ( 𝐺 ‘ 𝑁 ) )
27 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ 𝑁 ) ∈ ℝ )
28 26 27 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ‘ 𝑛 ) ∈ ℝ )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
30 18 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → 𝐺 : 𝑍 ⟶ ℝ )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ 𝑍 )
32 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
33 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
34 31 32 33 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
35 30 34 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
36 simpl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) )
37 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... ( 𝑛 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
38 33 adantll ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
39 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
40 38 39 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
41 36 37 40 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... ( 𝑛 − 1 ) ) ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
42 29 35 41 monoord2 ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑁 ) )
43 42 26 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ ( ( ℤ × { ( 𝐺 ‘ 𝑁 ) } ) ‘ 𝑛 ) )
44 6 9 10 17 21 28 43 climle ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 0 ≤ ( 𝐺 ‘ 𝑁 ) )