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	⊢ 𝐴 ∈ ℕ
	jm2.27dlem4.2	⊢ 𝐵 = ( 𝐴 + 1 )
Assertion	jm2.27dlem4	⊢ 𝐵 ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem3.1	⊢ 𝐴 ∈ ℕ
2		jm2.27dlem4.2	⊢ 𝐵 = ( 𝐴 + 1 )
3		peano2nn	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )
4	1 3	ax-mp	⊢ ( 𝐴 + 1 ) ∈ ℕ
5	2 4	eqeltri	⊢ 𝐵 ∈ ℕ