Metamath Proof Explorer

Theorem elfzo0

Description: Membership in a half-open integer range based at 0. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	elfzo0	$⊢ A \in (0 ..^B) \leftrightarrow (A \in ℕ_{0} \land B \in ℕ \land A < B)$

Proof

Step	Hyp	Ref	Expression
1		elfzouz	$⊢ A \in (0 ..^B) \to A \in ℤ_{\geq 0}$
2		elnn0uz	$⊢ A \in ℕ_{0} \leftrightarrow A \in ℤ_{\geq 0}$
3	1 2	sylibr	$⊢ A \in (0 ..^B) \to A \in ℕ_{0}$
4		elfzolt3b	$⊢ A \in (0 ..^B) \to 0 \in (0 ..^B)$
5		lbfzo0	$⊢ 0 \in (0 ..^B) \leftrightarrow B \in ℕ$
6	4 5	sylib	$⊢ A \in (0 ..^B) \to B \in ℕ$
7		elfzolt2	$⊢ A \in (0 ..^B) \to A < B$
8	3 6 7	3jca	$⊢ A \in (0 ..^B) \to (A \in ℕ_{0} \land B \in ℕ \land A < B)$
9		simp1	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to A \in ℕ_{0}$
10	9 2	sylib	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to A \in ℤ_{\geq 0}$
11		nnz	$⊢ B \in ℕ \to B \in ℤ$
12	11	3ad2ant2	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to B \in ℤ$
13		simp3	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to A < B$
14		elfzo2	$⊢ A \in (0 ..^B) \leftrightarrow (A \in ℤ_{\geq 0} \land B \in ℤ \land A < B)$
15	10 12 13 14	syl3anbrc	$⊢ (A \in ℕ_{0} \land B \in ℕ \land A < B) \to A \in (0 ..^B)$
16	8 15	impbii	$⊢ A \in (0 ..^B) \leftrightarrow (A \in ℕ_{0} \land B \in ℕ \land A < B)$