Metamath Proof Explorer


Theorem lbfzo0

Description: An integer is strictly greater than zero iff it is a member of NN . (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion lbfzo0 00..^AA

Proof

Step Hyp Ref Expression
1 0z 0
2 3anass 0A0<A0A0<A
3 1 2 mpbiran 0A0<AA0<A
4 fzolb 00..^A0A0<A
5 elnnz AA0<A
6 3 4 5 3bitr4i 00..^AA