Metamath Proof Explorer


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 ) )