Theorem jm2.27dlem4

Description: Lemma for rmydioph . Infer NN -hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Hypotheses	jm2.27dlem3.1	|- A e. NN
	jm2.27dlem4.2	|- B = ( A + 1 )
Assertion	jm2.27dlem4	|- B e. NN

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem3.1	|- A e. NN
2		jm2.27dlem4.2	|- B = ( A + 1 )
3		peano2nn	|- ( A e. NN -> ( A + 1 ) e. NN )
4	1 3	ax-mp	|- ( A + 1 ) e. NN
5	2 4	eqeltri	|- B e. NN