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

Metamath Proof Explorer

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