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

Metamath Proof Explorer

Theorem elnn0nn

Description: The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnn0nn 
|- ( N e. NN0 <-> ( N e. CC /\ ( N + 1 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
2 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
3 1 2 jca 
 |-  ( N e. NN0 -> ( N e. CC /\ ( N + 1 ) e. NN ) )
4 simpl 
 |-  ( ( N e. CC /\ ( N + 1 ) e. NN ) -> N e. CC )
5 ax-1cn 
 |-  1 e. CC
6 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
7 4 5 6 sylancl 
 |-  ( ( N e. CC /\ ( N + 1 ) e. NN ) -> ( ( N + 1 ) - 1 ) = N )
8 nnm1nn0 
 |-  ( ( N + 1 ) e. NN -> ( ( N + 1 ) - 1 ) e. NN0 )
9 8 adantl 
 |-  ( ( N e. CC /\ ( N + 1 ) e. NN ) -> ( ( N + 1 ) - 1 ) e. NN0 )
10 7 9 eqeltrrd 
 |-  ( ( N e. CC /\ ( N + 1 ) e. NN ) -> N e. NN0 )
11 3 10 impbii 
 |-  ( N e. NN0 <-> ( N e. CC /\ ( N + 1 ) e. NN ) )