zaddscl

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

		Ref	Expression
	Assertion	zaddscl	$⊢ (A \in ℤ_{s} \land B \in ℤ_{s}) \to A +_{s} B \in ℤ_{s}$

Proof

Step	Hyp	Ref	Expression
1		reeanv	$⊢ \exists x \in ℕ_{s} \exists z \in ℕ_{s} (\exists y \in ℕ_{s} A = x -_{s} y \land \exists w \in ℕ_{s} B = z -_{s} w) \leftrightarrow (\exists x \in ℕ_{s} \exists y \in ℕ_{s} A = x -_{s} y \land \exists z \in ℕ_{s} \exists w \in ℕ_{s} B = z -_{s} w)$
2		reeanv	$⊢ \exists y \in ℕ_{s} \exists w \in ℕ_{s} (A = x -_{s} y \land B = z -_{s} w) \leftrightarrow (\exists y \in ℕ_{s} A = x -_{s} y \land \exists w \in ℕ_{s} B = z -_{s} w)$
3	2	2rexbii	$⊢ \exists x \in ℕ_{s} \exists z \in ℕ_{s} \exists y \in ℕ_{s} \exists w \in ℕ_{s} (A = x -_{s} y \land B = z -_{s} w) \leftrightarrow \exists x \in ℕ_{s} \exists z \in ℕ_{s} (\exists y \in ℕ_{s} A = x -_{s} y \land \exists w \in ℕ_{s} B = z -_{s} w)$
4		elzs	$⊢ A \in ℤ_{s} \leftrightarrow \exists x \in ℕ_{s} \exists y \in ℕ_{s} A = x -_{s} y$
5		elzs	$⊢ B \in ℤ_{s} \leftrightarrow \exists z \in ℕ_{s} \exists w \in ℕ_{s} B = z -_{s} w$
6	4 5	anbi12i	$⊢ (A \in ℤ_{s} \land B \in ℤ_{s}) \leftrightarrow (\exists x \in ℕ_{s} \exists y \in ℕ_{s} A = x -_{s} y \land \exists z \in ℕ_{s} \exists w \in ℕ_{s} B = z -_{s} w)$
7	1 3 6	3bitr4ri	$⊢ (A \in ℤ_{s} \land B \in ℤ_{s}) \leftrightarrow \exists x \in ℕ_{s} \exists z \in ℕ_{s} \exists y \in ℕ_{s} \exists w \in ℕ_{s} (A = x -_{s} y \land B = z -_{s} w)$
8		simpll	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to x \in ℕ_{s}$
9	8	nnsnod	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to x \in No$
10		simplr	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to z \in ℕ_{s}$
11	10	nnsnod	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to z \in No$
12		simprl	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to y \in ℕ_{s}$
13	12	nnsnod	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to y \in No$
14		simprr	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to w \in ℕ_{s}$
15	14	nnsnod	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to w \in No$
16	9 11 13 15	addsubs4d	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to (x +_{s} z) -_{s} (y +_{s} w) = (x -_{s} y) +_{s} (z -_{s} w)$
17		nnaddscl	$⊢ (x \in ℕ_{s} \land z \in ℕ_{s}) \to x +_{s} z \in ℕ_{s}$
18		nnaddscl	$⊢ (y \in ℕ_{s} \land w \in ℕ_{s}) \to y +_{s} w \in ℕ_{s}$
19		nnzsubs	$⊢ (x +_{s} z \in ℕ_{s} \land y +_{s} w \in ℕ_{s}) \to (x +_{s} z) -_{s} (y +_{s} w) \in ℤ_{s}$
20	17 18 19	syl2an	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to (x +_{s} z) -_{s} (y +_{s} w) \in ℤ_{s}$
21	16 20	eqeltrrd	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to (x -_{s} y) +_{s} (z -_{s} w) \in ℤ_{s}$
22		oveq12	$⊢ (A = x -_{s} y \land B = z -_{s} w) \to A +_{s} B = (x -_{s} y) +_{s} (z -_{s} w)$
23	22	eleq1d	$⊢ (A = x -_{s} y \land B = z -_{s} w) \to (A +_{s} B \in ℤ_{s} \leftrightarrow (x -_{s} y) +_{s} (z -_{s} w) \in ℤ_{s})$
24	21 23	syl5ibrcom	$⊢ ((x \in ℕ_{s} \land z \in ℕ_{s}) \land (y \in ℕ_{s} \land w \in ℕ_{s})) \to ((A = x -_{s} y \land B = z -_{s} w) \to A +_{s} B \in ℤ_{s})$
25	24	rexlimdvva	$⊢ (x \in ℕ_{s} \land z \in ℕ_{s}) \to (\exists y \in ℕ_{s} \exists w \in ℕ_{s} (A = x -_{s} y \land B = z -_{s} w) \to A +_{s} B \in ℤ_{s})$
26	25	rexlimivv	$⊢ \exists x \in ℕ_{s} \exists z \in ℕ_{s} \exists y \in ℕ_{s} \exists w \in ℕ_{s} (A = x -_{s} y \land B = z -_{s} w) \to A +_{s} B \in ℤ_{s}$
27	7 26	sylbi	$⊢ (A \in ℤ_{s} \land B \in ℤ_{s}) \to A +_{s} B \in ℤ_{s}$

Metamath Proof Explorer

Theorem zaddscl

Proof