Theorem eln0zs

Description: Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	eln0zs	⊢ ( 𝑁 ∈ ℕ0s ↔ ( 𝑁 ∈ ℤs ∧ 0s ≤s 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		n0zs	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ ℤs )
2		n0sge0	⊢ ( 𝑁 ∈ ℕ0s → 0s ≤s 𝑁 )
3	1 2	jca	⊢ ( 𝑁 ∈ ℕ0s → ( 𝑁 ∈ ℤs ∧ 0s ≤s 𝑁 ) )
4		elzs	⊢ ( 𝑁 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝑁 = ( 𝑥 -s 𝑦 ) )
5		nnsno	⊢ ( 𝑥 ∈ ℕs → 𝑥 ∈ No )
6	5	adantr	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → 𝑥 ∈ No )
7		nnsno	⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ No )
8	7	adantl	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → 𝑦 ∈ No )
9	6 8	subsge0d	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 0s ≤s ( 𝑥 -s 𝑦 ) ↔ 𝑦 ≤s 𝑥 ) )
10		nnn0s	⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ ℕ0s )
11		nnn0s	⊢ ( 𝑥 ∈ ℕs → 𝑥 ∈ ℕ0s )
12		n0subs	⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s ) → ( 𝑦 ≤s 𝑥 ↔ ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) )
13	10 11 12	syl2anr	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 𝑦 ≤s 𝑥 ↔ ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) )
14	9 13	bitrd	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 0s ≤s ( 𝑥 -s 𝑦 ) ↔ ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) )
15	14	biimpd	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 0s ≤s ( 𝑥 -s 𝑦 ) → ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) )
16		breq2	⊢ ( 𝑁 = ( 𝑥 -s 𝑦 ) → ( 0s ≤s 𝑁 ↔ 0s ≤s ( 𝑥 -s 𝑦 ) ) )
17		eleq1	⊢ ( 𝑁 = ( 𝑥 -s 𝑦 ) → ( 𝑁 ∈ ℕ0s ↔ ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) )
18	16 17	imbi12d	⊢ ( 𝑁 = ( 𝑥 -s 𝑦 ) → ( ( 0s ≤s 𝑁 → 𝑁 ∈ ℕ0s ) ↔ ( 0s ≤s ( 𝑥 -s 𝑦 ) → ( 𝑥 -s 𝑦 ) ∈ ℕ0s ) ) )
19	15 18	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 𝑁 = ( 𝑥 -s 𝑦 ) → ( 0s ≤s 𝑁 → 𝑁 ∈ ℕ0s ) ) )
20	19	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝑁 = ( 𝑥 -s 𝑦 ) → ( 0s ≤s 𝑁 → 𝑁 ∈ ℕ0s ) )
21	4 20	sylbi	⊢ ( 𝑁 ∈ ℤs → ( 0s ≤s 𝑁 → 𝑁 ∈ ℕ0s ) )
22	21	imp	⊢ ( ( 𝑁 ∈ ℤs ∧ 0s ≤s 𝑁 ) → 𝑁 ∈ ℕ0s )
23	3 22	impbii	⊢ ( 𝑁 ∈ ℕ0s ↔ ( 𝑁 ∈ ℤs ∧ 0s ≤s 𝑁 ) )