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