Theorem elfzfzo

Description: Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elfzfzo	|- ( A e. ( M ..^ N ) <-> ( A e. ( M ... N ) /\ A < N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzofz	|- ( A e. ( M ..^ N ) -> A e. ( M ... N ) )
2		elfzolt2	|- ( A e. ( M ..^ N ) -> A < N )
3	1 2	jca	|- ( A e. ( M ..^ N ) -> ( A e. ( M ... N ) /\ A < N ) )
4		elfzuz	|- ( A e. ( M ... N ) -> A e. ( ZZ>= ` M ) )
5	4	adantr	|- ( ( A e. ( M ... N ) /\ A < N ) -> A e. ( ZZ>= ` M ) )
6		elfzel2	|- ( A e. ( M ... N ) -> N e. ZZ )
7	6	adantr	|- ( ( A e. ( M ... N ) /\ A < N ) -> N e. ZZ )
8		simpr	|- ( ( A e. ( M ... N ) /\ A < N ) -> A < N )
9		elfzo2	|- ( A e. ( M ..^ N ) <-> ( A e. ( ZZ>= ` M ) /\ N e. ZZ /\ A < N ) )
10	5 7 8 9	syl3anbrc	|- ( ( A e. ( M ... N ) /\ A < N ) -> A e. ( M ..^ N ) )
11	3 10	impbii	|- ( A e. ( M ..^ N ) <-> ( A e. ( M ... N ) /\ A < N ) )