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 e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) )

Proof

Step	Hyp	Ref	Expression
1		elfzouz	|- ( A e. ( 0 ..^ B ) -> A e. ( ZZ>= ` 0 ) )
2		elnn0uz	|- ( A e. NN0 <-> A e. ( ZZ>= ` 0 ) )
3	1 2	sylibr	|- ( A e. ( 0 ..^ B ) -> A e. NN0 )
4		elfzolt3b	|- ( A e. ( 0 ..^ B ) -> 0 e. ( 0 ..^ B ) )
5		lbfzo0	|- ( 0 e. ( 0 ..^ B ) <-> B e. NN )
6	4 5	sylib	|- ( A e. ( 0 ..^ B ) -> B e. NN )
7		elfzolt2	|- ( A e. ( 0 ..^ B ) -> A < B )
8	3 6 7	3jca	|- ( A e. ( 0 ..^ B ) -> ( A e. NN0 /\ B e. NN /\ A < B ) )
9		simp1	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> A e. NN0 )
10	9 2	sylib	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> A e. ( ZZ>= ` 0 ) )
11		nnz	|- ( B e. NN -> B e. ZZ )
12	11	3ad2ant2	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> B e. ZZ )
13		simp3	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> A < B )
14		elfzo2	|- ( A e. ( 0 ..^ B ) <-> ( A e. ( ZZ>= ` 0 ) /\ B e. ZZ /\ A < B ) )
15	10 12 13 14	syl3anbrc	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> A e. ( 0 ..^ B ) )
16	8 15	impbii	|- ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) )