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

Proof

Step Hyp Ref Expression
1 elzs2 ⊢ N ∈ ℤ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s
2 3orass ⊢ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s
3 eln0s ⊢ + s ⁡ N ∈ ℕ 0s ↔ + s ⁡ N ∈ ℕ s ∨ + s ⁡ N = 0 s
4 neg0s ⊢ + s ⁡ 0 s = 0 s
5 4 eqeq2i ⊢ + s ⁡ N = + s ⁡ 0 s ↔ + s ⁡ N = 0 s
6 0no ⊢ 0 s ∈ No
7 negs11 ⊢ N ∈ No ∧ 0 s ∈ No → + s ⁡ N = + s ⁡ 0 s ↔ N = 0 s
8 6 7 mpan2 ⊢ N ∈ No → + s ⁡ N = + s ⁡ 0 s ↔ N = 0 s
9 5 8 bitr3id ⊢ N ∈ No → + s ⁡ N = 0 s ↔ N = 0 s
10 9 orbi2d ⊢ N ∈ No → + s ⁡ N ∈ ℕ s ∨ + s ⁡ N = 0 s ↔ + s ⁡ N ∈ ℕ s ∨ N = 0 s
11 3 10 bitrid ⊢ N ∈ No → + s ⁡ N ∈ ℕ 0s ↔ + s ⁡ N ∈ ℕ s ∨ N = 0 s
12 orcom ⊢ + s ⁡ N ∈ ℕ s ∨ N = 0 s ↔ N = 0 s ∨ + s ⁡ N ∈ ℕ s
13 11 12 bitrdi ⊢ N ∈ No → + s ⁡ N ∈ ℕ 0s ↔ N = 0 s ∨ + s ⁡ N ∈ ℕ s
14 13 orbi2d ⊢ N ∈ No → N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ 0s ↔ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s
15 2 14 bitr4id ⊢ N ∈ No → N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ 0s
16 15 pm5.32i ⊢ N ∈ No ∧ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ 0s
17 1 16 bitri ⊢ N ∈ ℤ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ 0s