Theorem elfzo0z

Description: Membership in a half-open range of nonnegative integers, generalization of elfzo0 requiring the upper bound to be an integer only. (Contributed by Alexander van der Vekens, 23-Sep-2018)

	Ref	Expression
Assertion	elfzo0z	|- ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. ZZ /\ A < B ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo0	|- ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. NN /\ A < B ) )
2		nnz	|- ( B e. NN -> B e. ZZ )
3	2	3anim2i	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) -> ( A e. NN0 /\ B e. ZZ /\ A < B ) )
4		simp1	|- ( ( A e. NN0 /\ B e. ZZ /\ A < B ) -> A e. NN0 )
5		elnn0z	|- ( A e. NN0 <-> ( A e. ZZ /\ 0 <_ A ) )
6		0red	|- ( ( A e. ZZ /\ B e. ZZ ) -> 0 e. RR )
7		zre	|- ( A e. ZZ -> A e. RR )
8	7	adantr	|- ( ( A e. ZZ /\ B e. ZZ ) -> A e. RR )
9		zre	|- ( B e. ZZ -> B e. RR )
10	9	adantl	|- ( ( A e. ZZ /\ B e. ZZ ) -> B e. RR )
11		lelttr	|- ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) )
12	6 8 10 11	syl3anc	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) )
13		elnnz	|- ( B e. NN <-> ( B e. ZZ /\ 0 < B ) )
14	13	simplbi2	|- ( B e. ZZ -> ( 0 < B -> B e. NN ) )
15	14	adantl	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 0 < B -> B e. NN ) )
16	12 15	syld	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 0 <_ A /\ A < B ) -> B e. NN ) )
17	16	expd	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 0 <_ A -> ( A < B -> B e. NN ) ) )
18	17	impancom	|- ( ( A e. ZZ /\ 0 <_ A ) -> ( B e. ZZ -> ( A < B -> B e. NN ) ) )
19	5 18	sylbi	|- ( A e. NN0 -> ( B e. ZZ -> ( A < B -> B e. NN ) ) )
20	19	3imp	|- ( ( A e. NN0 /\ B e. ZZ /\ A < B ) -> B e. NN )
21		simp3	|- ( ( A e. NN0 /\ B e. ZZ /\ A < B ) -> A < B )
22	4 20 21	3jca	|- ( ( A e. NN0 /\ B e. ZZ /\ A < B ) -> ( A e. NN0 /\ B e. NN /\ A < B ) )
23	3 22	impbii	|- ( ( A e. NN0 /\ B e. NN /\ A < B ) <-> ( A e. NN0 /\ B e. ZZ /\ A < B ) )
24	1 23	bitri	|- ( A e. ( 0 ..^ B ) <-> ( A e. NN0 /\ B e. ZZ /\ A < B ) )