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 ( 𝑁 ∈ ℕs ↔ ( 𝑁 ∈ ℤs ∧ 0s <s 𝑁 ) )

Proof

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