Theorem elzn0s

Description: A surreal integer is a surreal that is a non-negative integer or whose negative is a non-negative integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	elzn0s	⊢ ( 𝐴 ∈ ℤs ↔ ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )

Proof

Step	Hyp	Ref	Expression
1		elzs	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
2		nnsno	⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ No )
3		nnsno	⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ No )
4		subscl	⊢ ( ( 𝑛 ∈ No ∧ 𝑚 ∈ No ) → ( 𝑛 -s 𝑚 ) ∈ No )
5	2 3 4	syl2an	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑛 -s 𝑚 ) ∈ No )
6		sletric	⊢ ( ( 𝑚 ∈ No ∧ 𝑛 ∈ No ) → ( 𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚 ) )
7	3 2 6	syl2anr	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚 ) )
8		nnn0s	⊢ ( 𝑚 ∈ ℕs → 𝑚 ∈ ℕ0s )
9		nnn0s	⊢ ( 𝑛 ∈ ℕs → 𝑛 ∈ ℕ0s )
10		n0subs	⊢ ( ( 𝑚 ∈ ℕ0s ∧ 𝑛 ∈ ℕ0s ) → ( 𝑚 ≤s 𝑛 ↔ ( 𝑛 -s 𝑚 ) ∈ ℕ0s ) )
11	8 9 10	syl2anr	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑚 ≤s 𝑛 ↔ ( 𝑛 -s 𝑚 ) ∈ ℕ0s ) )
12		n0subs	⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → ( 𝑛 ≤s 𝑚 ↔ ( 𝑚 -s 𝑛 ) ∈ ℕ0s ) )
13	9 8 12	syl2an	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑛 ≤s 𝑚 ↔ ( 𝑚 -s 𝑛 ) ∈ ℕ0s ) )
14	2	adantr	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 𝑛 ∈ No )
15	3	adantl	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → 𝑚 ∈ No )
16	14 15	negsubsdi2d	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( -us ‘ ( 𝑛 -s 𝑚 ) ) = ( 𝑚 -s 𝑛 ) )
17	16	eleq1d	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ↔ ( 𝑚 -s 𝑛 ) ∈ ℕ0s ) )
18	13 17	bitr4d	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝑛 ≤s 𝑚 ↔ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) )
19	11 18	orbi12d	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( ( 𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚 ) ↔ ( ( 𝑛 -s 𝑚 ) ∈ ℕ0s ∨ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) ) )
20	7 19	mpbid	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( ( 𝑛 -s 𝑚 ) ∈ ℕ0s ∨ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) )
21	5 20	jca	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( ( 𝑛 -s 𝑚 ) ∈ No ∧ ( ( 𝑛 -s 𝑚 ) ∈ ℕ0s ∨ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) ) )
22		eleq1	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( 𝐴 ∈ No ↔ ( 𝑛 -s 𝑚 ) ∈ No ) )
23		eleq1	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( 𝐴 ∈ ℕ0s ↔ ( 𝑛 -s 𝑚 ) ∈ ℕ0s ) )
24		fveq2	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( -us ‘ 𝐴 ) = ( -us ‘ ( 𝑛 -s 𝑚 ) ) )
25	24	eleq1d	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( ( -us ‘ 𝐴 ) ∈ ℕ0s ↔ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) )
26	23 25	orbi12d	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ↔ ( ( 𝑛 -s 𝑚 ) ∈ ℕ0s ∨ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) ) )
27	22 26	anbi12d	⊢ ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) ↔ ( ( 𝑛 -s 𝑚 ) ∈ No ∧ ( ( 𝑛 -s 𝑚 ) ∈ ℕ0s ∨ ( -us ‘ ( 𝑛 -s 𝑚 ) ) ∈ ℕ0s ) ) ) )
28	21 27	syl5ibrcom	⊢ ( ( 𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs ) → ( 𝐴 = ( 𝑛 -s 𝑚 ) → ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) ) )
29	28	rexlimivv	⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) → ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )
30		n0p1nns	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) ∈ ℕs )
31		1nns	⊢ 1s ∈ ℕs
32	31	a1i	⊢ ( 𝐴 ∈ ℕ0s → 1s ∈ ℕs )
33		n0sno	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
34		1sno	⊢ 1s ∈ No
35		pncans	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ No ) → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
36	33 34 35	sylancl	⊢ ( 𝐴 ∈ ℕ0s → ( ( 𝐴 +s 1s ) -s 1s ) = 𝐴 )
37	36	eqcomd	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( ( 𝐴 +s 1s ) -s 1s ) )
38		rspceov	⊢ ( ( ( 𝐴 +s 1s ) ∈ ℕs ∧ 1s ∈ ℕs ∧ 𝐴 = ( ( 𝐴 +s 1s ) -s 1s ) ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
39	30 32 37 38	syl3anc	⊢ ( 𝐴 ∈ ℕ0s → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
40	39	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ∈ ℕ0s ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
41	31	a1i	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → 1s ∈ ℕs )
42	34	a1i	⊢ ( 𝐴 ∈ No → 1s ∈ No )
43		id	⊢ ( 𝐴 ∈ No → 𝐴 ∈ No )
44	42 43	subsvald	⊢ ( 𝐴 ∈ No → ( 1s -s 𝐴 ) = ( 1s +s ( -us ‘ 𝐴 ) ) )
45		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
46	42 45	addscomd	⊢ ( 𝐴 ∈ No → ( 1s +s ( -us ‘ 𝐴 ) ) = ( ( -us ‘ 𝐴 ) +s 1s ) )
47	44 46	eqtrd	⊢ ( 𝐴 ∈ No → ( 1s -s 𝐴 ) = ( ( -us ‘ 𝐴 ) +s 1s ) )
48	47	adantr	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( 1s -s 𝐴 ) = ( ( -us ‘ 𝐴 ) +s 1s ) )
49		n0p1nns	⊢ ( ( -us ‘ 𝐴 ) ∈ ℕ0s → ( ( -us ‘ 𝐴 ) +s 1s ) ∈ ℕs )
50	49	adantl	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( ( -us ‘ 𝐴 ) +s 1s ) ∈ ℕs )
51	48 50	eqeltrd	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( 1s -s 𝐴 ) ∈ ℕs )
52	42 43	nncansd	⊢ ( 𝐴 ∈ No → ( 1s -s ( 1s -s 𝐴 ) ) = 𝐴 )
53	52	eqcomd	⊢ ( 𝐴 ∈ No → 𝐴 = ( 1s -s ( 1s -s 𝐴 ) ) )
54	53	adantr	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → 𝐴 = ( 1s -s ( 1s -s 𝐴 ) ) )
55		rspceov	⊢ ( ( 1s ∈ ℕs ∧ ( 1s -s 𝐴 ) ∈ ℕs ∧ 𝐴 = ( 1s -s ( 1s -s 𝐴 ) ) ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
56	41 51 54 55	syl3anc	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
57	40 56	jaodan	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) )
58	29 57	impbii	⊢ ( ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 𝐴 = ( 𝑛 -s 𝑚 ) ↔ ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )
59	1 58	bitri	⊢ ( 𝐴 ∈ ℤs ↔ ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )