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	$⊢ Z = ℤ_{\geq M}$
	iseralt.2	$⊢ φ \to M \in ℤ$
	iseralt.3	$⊢ φ \to G : Z ⟶ ℝ$
	iseralt.4	$⊢ (φ \land k \in Z) \to G (k + 1) \leq G (k)$
	iseralt.5	$⊢ φ \to G ⇝ 0$
Assertion	iseraltlem1	$⊢ (φ \land N \in Z) \to 0 \leq G (N)$

Proof

Step	Hyp	Ref	Expression
1		iseralt.1	$⊢ Z = ℤ_{\geq M}$
2		iseralt.2	$⊢ φ \to M \in ℤ$
3		iseralt.3	$⊢ φ \to G : Z ⟶ ℝ$
4		iseralt.4	$⊢ (φ \land k \in Z) \to G (k + 1) \leq G (k)$
5		iseralt.5	$⊢ φ \to G ⇝ 0$
6		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
7		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
8	7 1	eleq2s	$⊢ N \in Z \to N \in ℤ$
9	8	adantl	$⊢ (φ \land N \in Z) \to N \in ℤ$
10	5	adantr	$⊢ (φ \land N \in Z) \to G ⇝ 0$
11	3	ffvelcdmda	$⊢ (φ \land N \in Z) \to G (N) \in ℝ$
12	11	recnd	$⊢ (φ \land N \in Z) \to G (N) \in ℂ$
13		1z	$⊢ 1 \in ℤ$
14		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
15		zex	$⊢ ℤ \in V$
16	14 15	climconst2	$⊢ (G (N) \in ℂ \land 1 \in ℤ) \to (ℤ \times \{G (N)\}) ⇝ G (N)$
17	12 13 16	sylancl	$⊢ (φ \land N \in Z) \to (ℤ \times \{G (N)\}) ⇝ G (N)$
18	3	ad2antrr	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to G : Z ⟶ ℝ$
19	1	uztrn2	$⊢ (N \in Z \land n \in ℤ_{\geq N}) \to n \in Z$
20	19	adantll	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to n \in Z$
21	18 20	ffvelcdmd	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to G (n) \in ℝ$
22		eluzelz	$⊢ n \in ℤ_{\geq N} \to n \in ℤ$
23	22	adantl	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to n \in ℤ$
24		fvex	$⊢ G (N) \in V$
25	24	fvconst2	$⊢ n \in ℤ \to (ℤ \times \{G (N)\}) (n) = G (N)$
26	23 25	syl	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to (ℤ \times \{G (N)\}) (n) = G (N)$
27	11	adantr	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to G (N) \in ℝ$
28	26 27	eqeltrd	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to (ℤ \times \{G (N)\}) (n) \in ℝ$
29		simpr	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to n \in ℤ_{\geq N}$
30	18	adantr	$⊢ (((φ \land N \in Z) \land n \in ℤ_{\geq N}) \land k \in (N \dots n)) \to G : Z ⟶ ℝ$
31		simplr	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to N \in Z$
32		elfzuz	$⊢ k \in (N \dots n) \to k \in ℤ_{\geq N}$
33	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
34	31 32 33	syl2an	$⊢ (((φ \land N \in Z) \land n \in ℤ_{\geq N}) \land k \in (N \dots n)) \to k \in Z$
35	30 34	ffvelcdmd	$⊢ (((φ \land N \in Z) \land n \in ℤ_{\geq N}) \land k \in (N \dots n)) \to G (k) \in ℝ$
36		simpl	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to (φ \land N \in Z)$
37		elfzuz	$⊢ k \in (N \dots n - 1) \to k \in ℤ_{\geq N}$
38	33	adantll	$⊢ ((φ \land N \in Z) \land k \in ℤ_{\geq N}) \to k \in Z$
39	4	adantlr	$⊢ ((φ \land N \in Z) \land k \in Z) \to G (k + 1) \leq G (k)$
40	38 39	syldan	$⊢ ((φ \land N \in Z) \land k \in ℤ_{\geq N}) \to G (k + 1) \leq G (k)$
41	36 37 40	syl2an	$⊢ (((φ \land N \in Z) \land n \in ℤ_{\geq N}) \land k \in (N \dots n - 1)) \to G (k + 1) \leq G (k)$
42	29 35 41	monoord2	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to G (n) \leq G (N)$
43	42 26	breqtrrd	$⊢ ((φ \land N \in Z) \land n \in ℤ_{\geq N}) \to G (n) \leq (ℤ \times \{G (N)\}) (n)$
44	6 9 10 17 21 28 43	climle	$⊢ (φ \land N \in Z) \to 0 \leq G (N)$

Metamath Proof Explorer

Theorem iseraltlem1

Proof