Metamath Proof Explorer

Theorem elznns

Description: Surreal integer property expressed in terms of positive integers and non-negative integers. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Assertion elznns ( 𝑁 ∈ ℤs ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )

Proof

Step Hyp Ref Expression
1 elzs2 ⊢ ( 𝑁 ∈ ℤs ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) )
2 3orass ⊢ ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ↔ ( 𝑁 ∈ ℕs ∨ ( 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) )
3 eln0s ⊢ ( ( -us ‘ 𝑁 ) ∈ ℕ0s ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ ( -us ‘ 𝑁 ) = 0s ) )
4 negs0s ⊢ ( -us ‘ 0s ) = 0s
5 4 eqeq2i ⊢ ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ ( -us ‘ 𝑁 ) = 0s )
6 0sno ⊢ 0s ∈ No
7 negs11 ⊢ ( ( 𝑁 ∈ No ∧ 0s ∈ No ) → ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ 𝑁 = 0s ) )
8 6 7 mpan2 ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ 𝑁 = 0s ) )
9 5 8 bitr3id ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) = 0s ↔ 𝑁 = 0s ) )
10 9 orbi2d ⊢ ( 𝑁 ∈ No → ( ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ ( -us ‘ 𝑁 ) = 0s ) ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
11 3 10 bitrid ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) ∈ ℕ0s ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
12 orcom ⊢ ( ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ↔ ( 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) )
13 11 12 bitrdi ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) ∈ ℕ0s ↔ ( 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) )
14 13 orbi2d ⊢ ( 𝑁 ∈ No → ( ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ↔ ( 𝑁 ∈ ℕs ∨ ( 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) ) )
15 2 14 bitr4id ⊢ ( 𝑁 ∈ No → ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ↔ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )
16 15 pm5.32i ⊢ ( ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )
17 1 16 bitri ⊢ ( 𝑁 ∈ ℤs ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )