climuzcnv

Description: Utility lemma to convert between m <_ k and k e. ( ZZ>=m ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012)

		Ref	Expression
	Assertion	climuzcnv	$⊢ m \in ℕ \to ((k \in ℤ_{\geq m} \to φ) \leftrightarrow (k \in ℕ \to (m \leq k \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$⊢ m \in ℕ \leftrightarrow m \in ℤ_{\geq 1}$
2		uztrn	$⊢ (k \in ℤ_{\geq m} \land m \in ℤ_{\geq 1}) \to k \in ℤ_{\geq 1}$
3	1 2	sylan2b	$⊢ (k \in ℤ_{\geq m} \land m \in ℕ) \to k \in ℤ_{\geq 1}$
4		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
5	3 4	sylibr	$⊢ (k \in ℤ_{\geq m} \land m \in ℕ) \to k \in ℕ$
6	5	expcom	$⊢ m \in ℕ \to (k \in ℤ_{\geq m} \to k \in ℕ)$
7		eluzle	$⊢ k \in ℤ_{\geq m} \to m \leq k$
8	7	a1i	$⊢ m \in ℕ \to (k \in ℤ_{\geq m} \to m \leq k)$
9	6 8	jcad	$⊢ m \in ℕ \to (k \in ℤ_{\geq m} \to (k \in ℕ \land m \leq k))$
10		nnz	$⊢ k \in ℕ \to k \in ℤ$
11		nnz	$⊢ m \in ℕ \to m \in ℤ$
12		eluz2	$⊢ k \in ℤ_{\geq m} \leftrightarrow (m \in ℤ \land k \in ℤ \land m \leq k)$
13	12	biimpri	$⊢ (m \in ℤ \land k \in ℤ \land m \leq k) \to k \in ℤ_{\geq m}$
14	11 13	syl3an1	$⊢ (m \in ℕ \land k \in ℤ \land m \leq k) \to k \in ℤ_{\geq m}$
15	10 14	syl3an2	$⊢ (m \in ℕ \land k \in ℕ \land m \leq k) \to k \in ℤ_{\geq m}$
16	15	3expib	$⊢ m \in ℕ \to ((k \in ℕ \land m \leq k) \to k \in ℤ_{\geq m})$
17	9 16	impbid	$⊢ m \in ℕ \to (k \in ℤ_{\geq m} \leftrightarrow (k \in ℕ \land m \leq k))$
18	17	imbi1d	$⊢ m \in ℕ \to ((k \in ℤ_{\geq m} \to φ) \leftrightarrow ((k \in ℕ \land m \leq k) \to φ))$
19		impexp	$⊢ ((k \in ℕ \land m \leq k) \to φ) \leftrightarrow (k \in ℕ \to (m \leq k \to φ))$
20	18 19	bitrdi	$⊢ m \in ℕ \to ((k \in ℤ_{\geq m} \to φ) \leftrightarrow (k \in ℕ \to (m \leq k \to φ)))$

Metamath Proof Explorer

Theorem climuzcnv

Proof