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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑁 ) ∈ ℝ )
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	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
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	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
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 ≤ ( 𝐺 ‘ 𝑁 ) )