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 ⊢ N ∈ ℤ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s

Proof

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