Metamath Proof Explorer

Theorem zaddscl

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

Ref Expression
Assertion zaddscl 
|- ( ( A e. ZZ_s /\ B e. ZZ_s ) -> ( A +s B ) e. ZZ_s )

Proof

Step Hyp Ref Expression
1 reeanv 
 |-  ( E. x e. NN_s E. z e. NN_s ( E. y e. NN_s A = ( x -s y ) /\ E. w e. NN_s B = ( z -s w ) ) <-> ( E. x e. NN_s E. y e. NN_s A = ( x -s y ) /\ E. z e. NN_s E. w e. NN_s B = ( z -s w ) ) )
2 reeanv 
 |-  ( E. y e. NN_s E. w e. NN_s ( A = ( x -s y ) /\ B = ( z -s w ) ) <-> ( E. y e. NN_s A = ( x -s y ) /\ E. w e. NN_s B = ( z -s w ) ) )
3 2 2rexbii 
 |-  ( E. x e. NN_s E. z e. NN_s E. y e. NN_s E. w e. NN_s ( A = ( x -s y ) /\ B = ( z -s w ) ) <-> E. x e. NN_s E. z e. NN_s ( E. y e. NN_s A = ( x -s y ) /\ E. w e. NN_s B = ( z -s w ) ) )
4 elzs 
 |-  ( A e. ZZ_s <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
5 elzs 
 |-  ( B e. ZZ_s <-> E. z e. NN_s E. w e. NN_s B = ( z -s w ) )
6 4 5 anbi12i 
 |-  ( ( A e. ZZ_s /\ B e. ZZ_s ) <-> ( E. x e. NN_s E. y e. NN_s A = ( x -s y ) /\ E. z e. NN_s E. w e. NN_s B = ( z -s w ) ) )
7 1 3 6 3bitr4ri 
 |-  ( ( A e. ZZ_s /\ B e. ZZ_s ) <-> E. x e. NN_s E. z e. NN_s E. y e. NN_s E. w e. NN_s ( A = ( x -s y ) /\ B = ( z -s w ) ) )
8 simpll 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> x e. NN_s )
9 8 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> x e. No )
10 simplr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> z e. NN_s )
11 10 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> z e. No )
12 simprl 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> y e. NN_s )
13 12 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> y e. No )
14 simprr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> w e. NN_s )
15 14 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> w e. No )
16 9 11 13 15 addsubs4d 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x +s z ) -s ( y +s w ) ) = ( ( x -s y ) +s ( z -s w ) ) )
17 nnaddscl 
 |-  ( ( x e. NN_s /\ z e. NN_s ) -> ( x +s z ) e. NN_s )
18 nnaddscl 
 |-  ( ( y e. NN_s /\ w e. NN_s ) -> ( y +s w ) e. NN_s )
19 nnzsubs 
 |-  ( ( ( x +s z ) e. NN_s /\ ( y +s w ) e. NN_s ) -> ( ( x +s z ) -s ( y +s w ) ) e. ZZ_s )
20 17 18 19 syl2an 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x +s z ) -s ( y +s w ) ) e. ZZ_s )
21 16 20 eqeltrrd 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) +s ( z -s w ) ) e. ZZ_s )
22 oveq12 
 |-  ( ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( A +s B ) = ( ( x -s y ) +s ( z -s w ) ) )
23 22 eleq1d 
 |-  ( ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( ( A +s B ) e. ZZ_s <-> ( ( x -s y ) +s ( z -s w ) ) e. ZZ_s ) )
24 21 23 syl5ibrcom 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( A +s B ) e. ZZ_s ) )
25 24 rexlimdvva 
 |-  ( ( x e. NN_s /\ z e. NN_s ) -> ( E. y e. NN_s E. w e. NN_s ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( A +s B ) e. ZZ_s ) )
26 25 rexlimivv 
 |-  ( E. x e. NN_s E. z e. NN_s E. y e. NN_s E. w e. NN_s ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( A +s B ) e. ZZ_s )
27 7 26 sylbi 
 |-  ( ( A e. ZZ_s /\ B e. ZZ_s ) -> ( A +s B ) e. ZZ_s )