elnnzs

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

		Ref	Expression
	Assertion	elnnzs	$⊢ N \in ℕ_{s} \leftrightarrow (N \in ℤ_{s} \land 0_{s} <_{s} N)$

Proof

Step	Hyp	Ref	Expression
1		nnsno	$⊢ N \in ℕ_{s} \to N \in No$
2		orc	$⊢ N \in ℕ_{s} \to (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))$
3		nnsgt0	$⊢ N \in ℕ_{s} \to 0_{s} <_{s} N$
4	1 2 3	jca31	$⊢ N \in ℕ_{s} \to ((N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))) \land 0_{s} <_{s} N)$
5		idd	$⊢ (N \in No \land 0_{s} <_{s} N) \to (N \in ℕ_{s} \to N \in ℕ_{s})$
6		negscl	$⊢ N \in No \to +_{s} (N) \in No$
7	6	adantr	$⊢ (N \in No \land 0_{s} <_{s} N) \to +_{s} (N) \in No$
8		0sno	$⊢ 0_{s} \in No$
9		sltneg	$⊢ (0_{s} \in No \land N \in No) \to (0_{s} <_{s} N \leftrightarrow +_{s} (N) <_{s} +_{s} (0_{s}))$
10	8 9	mpan	$⊢ N \in No \to (0_{s} <_{s} N \leftrightarrow +_{s} (N) <_{s} +_{s} (0_{s}))$
11		negs0s	$⊢ +_{s} (0_{s}) = 0_{s}$
12	11	breq2i	$⊢ +_{s} (N) <_{s} +_{s} (0_{s}) \leftrightarrow +_{s} (N) <_{s} 0_{s}$
13	10 12	bitrdi	$⊢ N \in No \to (0_{s} <_{s} N \leftrightarrow +_{s} (N) <_{s} 0_{s})$
14	13	biimpa	$⊢ (N \in No \land 0_{s} <_{s} N) \to +_{s} (N) <_{s} 0_{s}$
15		sltasym	$⊢ (+_{s} (N) \in No \land 0_{s} \in No) \to (+_{s} (N) <_{s} 0_{s} \to \neg 0_{s} <_{s} +_{s} (N))$
16	8 15	mpan2	$⊢ +_{s} (N) \in No \to (+_{s} (N) <_{s} 0_{s} \to \neg 0_{s} <_{s} +_{s} (N))$
17	7 14 16	sylc	$⊢ (N \in No \land 0_{s} <_{s} N) \to \neg 0_{s} <_{s} +_{s} (N)$
18		nnsgt0	$⊢ +_{s} (N) \in ℕ_{s} \to 0_{s} <_{s} +_{s} (N)$
19	17 18	nsyl	$⊢ (N \in No \land 0_{s} <_{s} N) \to \neg +_{s} (N) \in ℕ_{s}$
20		sgt0ne0	$⊢ 0_{s} <_{s} N \to N \neq 0_{s}$
21	20	adantl	$⊢ (N \in No \land 0_{s} <_{s} N) \to N \neq 0_{s}$
22	21	neneqd	$⊢ (N \in No \land 0_{s} <_{s} N) \to \neg N = 0_{s}$
23		ioran	$⊢ \neg (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}) \leftrightarrow (\neg +_{s} (N) \in ℕ_{s} \land \neg N = 0_{s})$
24	19 22 23	sylanbrc	$⊢ (N \in No \land 0_{s} <_{s} N) \to \neg (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})$
25	24	pm2.21d	$⊢ (N \in No \land 0_{s} <_{s} N) \to ((+_{s} (N) \in ℕ_{s} \lor N = 0_{s}) \to N \in ℕ_{s})$
26	5 25	jaod	$⊢ (N \in No \land 0_{s} <_{s} N) \to ((N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})) \to N \in ℕ_{s})$
27	26	ex	$⊢ N \in No \to (0_{s} <_{s} N \to ((N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})) \to N \in ℕ_{s}))$
28	27	com23	$⊢ N \in No \to ((N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})) \to (0_{s} <_{s} N \to N \in ℕ_{s}))$
29	28	imp31	$⊢ ((N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))) \land 0_{s} <_{s} N) \to N \in ℕ_{s}$
30	4 29	impbii	$⊢ N \in ℕ_{s} \leftrightarrow ((N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))) \land 0_{s} <_{s} N)$
31		elzs2	$⊢ N \in ℤ_{s} \leftrightarrow (N \in No \land (N \in ℕ_{s} \lor N = 0_{s} \lor +_{s} (N) \in ℕ_{s}))$
32		3orcomb	$⊢ (N \in ℕ_{s} \lor N = 0_{s} \lor +_{s} (N) \in ℕ_{s}) \leftrightarrow (N \in ℕ_{s} \lor +_{s} (N) \in ℕ_{s} \lor N = 0_{s})$
33		3orass	$⊢ (N \in ℕ_{s} \lor +_{s} (N) \in ℕ_{s} \lor N = 0_{s}) \leftrightarrow (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))$
34	32 33	bitri	$⊢ (N \in ℕ_{s} \lor N = 0_{s} \lor +_{s} (N) \in ℕ_{s}) \leftrightarrow (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))$
35	34	anbi2i	$⊢ (N \in No \land (N \in ℕ_{s} \lor N = 0_{s} \lor +_{s} (N) \in ℕ_{s})) \leftrightarrow (N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})))$
36	31 35	bitri	$⊢ N \in ℤ_{s} \leftrightarrow (N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s})))$
37	36	anbi1i	$⊢ (N \in ℤ_{s} \land 0_{s} <_{s} N) \leftrightarrow ((N \in No \land (N \in ℕ_{s} \lor (+_{s} (N) \in ℕ_{s} \lor N = 0_{s}))) \land 0_{s} <_{s} N)$
38	30 37	bitr4i	$⊢ N \in ℕ_{s} \leftrightarrow (N \in ℤ_{s} \land 0_{s} <_{s} N)$

Metamath Proof Explorer

Theorem elnnzs

Proof