Theorem nnzs

Description: A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	nnzs	⊢ ( 𝐴 ∈ ℕs → 𝐴 ∈ ℤs )

Proof

Step	Hyp	Ref	Expression
1		peano2nns	⊢ ( 𝐴 ∈ ℕs → ( 𝐴 +s 1s ) ∈ ℕs )
2		nnsno	⊢ ( 𝐴 ∈ ℕs → 𝐴 ∈ No )
3		1sno	⊢ 1s ∈ No
4		pncans	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ No ) → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
5	2 3 4	sylancl	⊢ ( 𝐴 ∈ ℕs → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
6	5	eqcomd	⊢ ( 𝐴 ∈ ℕs → 𝐴 = ( ( 𝐴 +s 1s ) -s 1s ) )
7		1nns	⊢ 1s ∈ ℕs
8		rspceov	⊢ ( ( ( 𝐴 +s 1s ) ∈ ℕs ∧ 1s ∈ ℕs ∧ 𝐴 = ( ( 𝐴 +s 1s ) -s 1s ) ) → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
9	7 8	mp3an2	⊢ ( ( ( 𝐴 +s 1s ) ∈ ℕs ∧ 𝐴 = ( ( 𝐴 +s 1s ) -s 1s ) ) → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
10	1 6 9	syl2anc	⊢ ( 𝐴 ∈ ℕs → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
11		elzs	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
12	10 11	sylibr	⊢ ( 𝐴 ∈ ℕs → 𝐴 ∈ ℤs )