eluz2

Description: Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show M e. ZZ . (Contributed by NM, 5-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
2		simp1	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to M \in ℤ$
3		eluz1	$⊢ M \in ℤ \to (N \in ℤ_{\geq M} \leftrightarrow (N \in ℤ \land M \leq N))$
4		ibar	$⊢ M \in ℤ \to ((N \in ℤ \land M \leq N) \leftrightarrow (M \in ℤ \land (N \in ℤ \land M \leq N)))$
5	3 4	bitrd	$⊢ M \in ℤ \to (N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land (N \in ℤ \land M \leq N)))$
6		3anass	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \leftrightarrow (M \in ℤ \land (N \in ℤ \land M \leq N))$
7	5 6	bitr4di	$⊢ M \in ℤ \to (N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N))$
8	1 2 7	pm5.21nii	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$

Metamath Proof Explorer

Theorem eluz2

Proof