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

Metamath Proof Explorer

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