Theorem n0addscl

Description: The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	n0addscl	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s ) → ( 𝐴 +s 𝐵 ) ∈ ℕ0s )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 0s → ( 𝐴 +s 𝑛 ) = ( 𝐴 +s 0s ) )
2	1	eleq1d	⊢ ( 𝑛 = 0s → ( ( 𝐴 +s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 +s 0s ) ∈ ℕ0s ) )
3	2	imbi2d	⊢ ( 𝑛 = 0s → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 0s ) ∈ ℕ0s ) ) )
4		oveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐴 +s 𝑛 ) = ( 𝐴 +s 𝑚 ) )
5	4	eleq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 +s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) )
6	5	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) ) )
7		oveq2	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( 𝐴 +s 𝑛 ) = ( 𝐴 +s ( 𝑚 +s 1s ) ) )
8	7	eleq1d	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( ( 𝐴 +s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) )
9	8	imbi2d	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
10		oveq2	⊢ ( 𝑛 = 𝐵 → ( 𝐴 +s 𝑛 ) = ( 𝐴 +s 𝐵 ) )
11	10	eleq1d	⊢ ( 𝑛 = 𝐵 → ( ( 𝐴 +s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 +s 𝐵 ) ∈ ℕ0s ) )
12	11	imbi2d	⊢ ( 𝑛 = 𝐵 → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝐵 ) ∈ ℕ0s ) ) )
13		n0sno	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
14	13	addsridd	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 0s ) = 𝐴 )
15		id	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ ℕ0s )
16	14 15	eqeltrd	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 0s ) ∈ ℕ0s )
17	13	adantr	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → 𝐴 ∈ No )
18	17	adantr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → 𝐴 ∈ No )
19		n0sno	⊢ ( 𝑚 ∈ ℕ0s → 𝑚 ∈ No )
20	19	adantl	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → 𝑚 ∈ No )
21	20	adantr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → 𝑚 ∈ No )
22		1sno	⊢ 1s ∈ No
23	22	a1i	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → 1s ∈ No )
24	18 21 23	addsassd	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → ( ( 𝐴 +s 𝑚 ) +s 1s ) = ( 𝐴 +s ( 𝑚 +s 1s ) ) )
25		peano2n0s	⊢ ( ( 𝐴 +s 𝑚 ) ∈ ℕ0s → ( ( 𝐴 +s 𝑚 ) +s 1s ) ∈ ℕ0s )
26	25	adantl	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → ( ( 𝐴 +s 𝑚 ) +s 1s ) ∈ ℕ0s )
27	24 26	eqeltrrd	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s )
28	27	ex	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → ( ( 𝐴 +s 𝑚 ) ∈ ℕ0s → ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) )
29	28	expcom	⊢ ( 𝑚 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( ( 𝐴 +s 𝑚 ) ∈ ℕ0s → ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
30	29	a2d	⊢ ( 𝑚 ∈ ℕ0s → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 +s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
31	3 6 9 12 16 30	n0sind	⊢ ( 𝐵 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 𝐵 ) ∈ ℕ0s ) )
32	31	impcom	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s ) → ( 𝐴 +s 𝐵 ) ∈ ℕ0s )