Metamath Proof Explorer

Theorem elzs2

Description: A surreal integer is either a positive integer, zero, or the negative of a positive integer. (Contributed by Scott Fenton, 25-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 elzn0s ⊢ ( 𝑁 ∈ ℤs ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕ0s ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )
2 eln0s ⊢ ( 𝑁 ∈ ℕ0s ↔ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) )
3 2 a1i ⊢ ( 𝑁 ∈ No → ( 𝑁 ∈ ℕ0s ↔ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ) )
4 eln0s ⊢ ( ( -us ‘ 𝑁 ) ∈ ℕ0s ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ ( -us ‘ 𝑁 ) = 0s ) )
5 neg0s ⊢ ( -us ‘ 0s ) = 0s
6 5 eqeq2i ⊢ ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ ( -us ‘ 𝑁 ) = 0s )
7 0no ⊢ 0s ∈ No
8 negs11 ⊢ ( ( 𝑁 ∈ No ∧ 0s ∈ No ) → ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ 𝑁 = 0s ) )
9 7 8 mpan2 ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) = ( -us ‘ 0s ) ↔ 𝑁 = 0s ) )
10 6 9 bitr3id ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) = 0s ↔ 𝑁 = 0s ) )
11 10 orbi2d ⊢ ( 𝑁 ∈ No → ( ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ ( -us ‘ 𝑁 ) = 0s ) ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
12 4 11 bitrid ⊢ ( 𝑁 ∈ No → ( ( -us ‘ 𝑁 ) ∈ ℕ0s ↔ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
13 3 12 orbi12d ⊢ ( 𝑁 ∈ No → ( ( 𝑁 ∈ ℕ0s ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ↔ ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ∨ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) ) )
14 3orcoma ⊢ ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ↔ ( 𝑁 = 0s ∨ 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) )
15 3orass ⊢ ( ( 𝑁 = 0s ∨ 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ↔ ( 𝑁 = 0s ∨ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) )
16 orcom ⊢ ( ( 𝑁 = 0s ∨ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) ↔ ( ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ∨ 𝑁 = 0s ) )
17 orordir ⊢ ( ( ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ∨ 𝑁 = 0s ) ↔ ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ∨ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
18 16 17 bitri ⊢ ( ( 𝑁 = 0s ∨ ( 𝑁 ∈ ℕs ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) ↔ ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ∨ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) )
19 14 15 18 3bitrri ⊢ ( ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ∨ ( ( -us ‘ 𝑁 ) ∈ ℕs ∨ 𝑁 = 0s ) ) ↔ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) )
20 13 19 bitr2di ⊢ ( 𝑁 ∈ No → ( ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ↔ ( 𝑁 ∈ ℕ0s ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )
21 20 pm5.32i ⊢ ( ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕ0s ∨ ( -us ‘ 𝑁 ) ∈ ℕ0s ) ) )
22 1 21 bitr4i ⊢ ( 𝑁 ∈ ℤs ↔ ( 𝑁 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘ 𝑁 ) ∈ ℕs ) ) )