This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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