Theorem zaddscl

Description: The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	zaddscl	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs ) → ( 𝐴 +s 𝐵 ) ∈ ℤs )

Proof

Step	Hyp	Ref	Expression
1		reeanv	⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
2		reeanv	⊢ ( ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
3	2	2rexbii	⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ( ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
4		elzs	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
5		elzs	⊢ ( 𝐵 ∈ ℤs ↔ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) )
6	4 5	anbi12i	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs ) ↔ ( ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ∧ ∃ 𝑧 ∈ ℕs ∃ 𝑤 ∈ ℕs 𝐵 = ( 𝑧 -s 𝑤 ) ) )
7	1 3 6	3bitr4ri	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs ) ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) )
8		simpll	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑥 ∈ ℕs )
9	8	nnnod	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑥 ∈ No )
10		simplr	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑧 ∈ ℕs )
11	10	nnnod	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑧 ∈ No )
12		simprl	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑦 ∈ ℕs )
13	12	nnnod	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑦 ∈ No )
14		simprr	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑤 ∈ ℕs )
15	14	nnnod	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → 𝑤 ∈ No )
16	9 11 13 15	addsubs4d	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 +s 𝑧 ) -s ( 𝑦 +s 𝑤 ) ) = ( ( 𝑥 -s 𝑦 ) +s ( 𝑧 -s 𝑤 ) ) )
17		nnaddscl	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( 𝑥 +s 𝑧 ) ∈ ℕs )
18		nnaddscl	⊢ ( ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) → ( 𝑦 +s 𝑤 ) ∈ ℕs )
19		nnzsubs	⊢ ( ( ( 𝑥 +s 𝑧 ) ∈ ℕs ∧ ( 𝑦 +s 𝑤 ) ∈ ℕs ) → ( ( 𝑥 +s 𝑧 ) -s ( 𝑦 +s 𝑤 ) ) ∈ ℤs )
20	17 18 19	syl2an	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 +s 𝑧 ) -s ( 𝑦 +s 𝑤 ) ) ∈ ℤs )
21	16 20	eqeltrrd	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝑥 -s 𝑦 ) +s ( 𝑧 -s 𝑤 ) ) ∈ ℤs )
22		oveq12	⊢ ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 +s 𝐵 ) = ( ( 𝑥 -s 𝑦 ) +s ( 𝑧 -s 𝑤 ) ) )
23	22	eleq1d	⊢ ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( ( 𝐴 +s 𝐵 ) ∈ ℤs ↔ ( ( 𝑥 -s 𝑦 ) +s ( 𝑧 -s 𝑤 ) ) ∈ ℤs ) )
24	21 23	syl5ibrcom	⊢ ( ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) ∧ ( 𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs ) ) → ( ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs ) )
25	24	rexlimdvva	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑧 ∈ ℕs ) → ( ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs ) )
26	25	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℕs ∃ 𝑧 ∈ ℕs ∃ 𝑦 ∈ ℕs ∃ 𝑤 ∈ ℕs ( 𝐴 = ( 𝑥 -s 𝑦 ) ∧ 𝐵 = ( 𝑧 -s 𝑤 ) ) → ( 𝐴 +s 𝐵 ) ∈ ℤs )
27	7 26	sylbi	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs ) → ( 𝐴 +s 𝐵 ) ∈ ℤs )