Metamath Proof Explorer

Theorem elnnzs

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

Ref Expression
Assertion elnnzs ⊢ N ∈ ℕ s ↔ N ∈ ℤ s ∧ 0 s < s N

Proof

Step Hyp Ref Expression
1 nnno ⊢ N ∈ ℕ s → N ∈ No
2 orc ⊢ N ∈ ℕ s → N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
3 nnsgt0 ⊢ N ∈ ℕ s → 0 s < s N
4 1 2 3 jca31 ⊢ N ∈ ℕ s → N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s ∧ 0 s < s N
5 idd ⊢ N ∈ No ∧ 0 s < s N → N ∈ ℕ s → N ∈ ℕ s
6 negscl ⊢ N ∈ No → + s ⁡ N ∈ No
7 6 adantr ⊢ N ∈ No ∧ 0 s < s N → + s ⁡ N ∈ No
8 0no ⊢ 0 s ∈ No
9 ltnegs ⊢ 0 s ∈ No ∧ N ∈ No → 0 s < s N ↔ + s ⁡ N < s + s ⁡ 0 s
10 8 9 mpan ⊢ N ∈ No → 0 s < s N ↔ + s ⁡ N < s + s ⁡ 0 s
11 neg0s ⊢ + s ⁡ 0 s = 0 s
12 11 breq2i ⊢ + s ⁡ N < s + s ⁡ 0 s ↔ + s ⁡ N < s 0 s
13 10 12 bitrdi ⊢ N ∈ No → 0 s < s N ↔ + s ⁡ N < s 0 s
14 13 biimpa ⊢ N ∈ No ∧ 0 s < s N → + s ⁡ N < s 0 s
15 ltsasym ⊢ + s ⁡ N ∈ No ∧ 0 s ∈ No → + s ⁡ N < s 0 s → ¬ 0 s < s + s ⁡ N
16 8 15 mpan2 ⊢ + s ⁡ N ∈ No → + s ⁡ N < s 0 s → ¬ 0 s < s + s ⁡ N
17 7 14 16 sylc ⊢ N ∈ No ∧ 0 s < s N → ¬ 0 s < s + s ⁡ N
18 nnsgt0 ⊢ + s ⁡ N ∈ ℕ s → 0 s < s + s ⁡ N
19 17 18 nsyl ⊢ N ∈ No ∧ 0 s < s N → ¬ + s ⁡ N ∈ ℕ s
20 gt0ne0s ⊢ 0 s < s N → N ≠ 0 s
21 20 adantl ⊢ N ∈ No ∧ 0 s < s N → N ≠ 0 s
22 21 neneqd ⊢ N ∈ No ∧ 0 s < s N → ¬ N = 0 s
23 ioran ⊢ ¬ + s ⁡ N ∈ ℕ s ∨ N = 0 s ↔ ¬ + s ⁡ N ∈ ℕ s ∧ ¬ N = 0 s
24 19 22 23 sylanbrc ⊢ N ∈ No ∧ 0 s < s N → ¬ + s ⁡ N ∈ ℕ s ∨ N = 0 s
25 24 pm2.21d ⊢ N ∈ No ∧ 0 s < s N → + s ⁡ N ∈ ℕ s ∨ N = 0 s → N ∈ ℕ s
26 5 25 jaod ⊢ N ∈ No ∧ 0 s < s N → N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s → N ∈ ℕ s
27 26 ex ⊢ N ∈ No → 0 s < s N → N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s → N ∈ ℕ s
28 27 com23 ⊢ N ∈ No → N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s → 0 s < s N → N ∈ ℕ s
29 28 imp31 ⊢ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s ∧ 0 s < s N → N ∈ ℕ s
30 4 29 impbii ⊢ N ∈ ℕ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s ∧ 0 s < s N
31 elzs2 ⊢ N ∈ ℤ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s
32 3orcomb ⊢ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
33 3orass ⊢ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s ↔ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
34 32 33 bitri ⊢ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
35 34 anbi2i ⊢ N ∈ No ∧ N ∈ ℕ s ∨ N = 0 s ∨ + s ⁡ N ∈ ℕ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
36 31 35 bitri ⊢ N ∈ ℤ s ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s
37 36 anbi1i ⊢ N ∈ ℤ s ∧ 0 s < s N ↔ N ∈ No ∧ N ∈ ℕ s ∨ + s ⁡ N ∈ ℕ s ∨ N = 0 s ∧ 0 s < s N
38 30 37 bitr4i ⊢ N ∈ ℕ s ↔ N ∈ ℤ s ∧ 0 s < s N