Metamath Proof Explorer

Theorem zmulscld

Description: The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Hypotheses zmulscld.1 
|- ( ph -> A e. ZZ_s )
zmulscld.2 
|- ( ph -> B e. ZZ_s )
Assertion zmulscld 
|- ( ph -> ( A x.s B ) e. ZZ_s )

Proof

Step Hyp Ref Expression
1 zmulscld.1 
 |-  ( ph -> A e. ZZ_s )
2 zmulscld.2 
 |-  ( ph -> B e. ZZ_s )
3 elzs 
 |-  ( A e. ZZ_s <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
4 1 3 sylib 
 |-  ( ph -> 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 2 5 sylib 
 |-  ( ph -> E. z e. NN_s E. w e. NN_s B = ( z -s w ) )
7 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 ) ) )
8 7 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 ) ) )
9 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 ) ) )
10 8 9 bitri 
 |-  ( 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. y e. NN_s A = ( x -s y ) /\ E. z e. NN_s E. w e. NN_s B = ( z -s w ) ) )
11 nnsno 
 |-  ( x e. NN_s -> x e. No )
12 11 ad2antrr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> x e. No )
13 nnsno 
 |-  ( y e. NN_s -> y e. No )
14 13 ad2antrl 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> y e. No )
15 12 14 subscld 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( x -s y ) e. No )
16 nnsno 
 |-  ( z e. NN_s -> z e. No )
17 16 ad2antlr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> z e. No )
18 nnsno 
 |-  ( w e. NN_s -> w e. No )
19 18 ad2antll 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> w e. No )
20 15 17 19 subsdid 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) x.s ( z -s w ) ) = ( ( ( x -s y ) x.s z ) -s ( ( x -s y ) x.s w ) ) )
21 nnmulscl 
 |-  ( ( x e. NN_s /\ z e. NN_s ) -> ( x x.s z ) e. NN_s )
22 21 adantr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( x x.s z ) e. NN_s )
23 22 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( x x.s z ) e. No )
24 simprl 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> y e. NN_s )
25 simplr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> z e. NN_s )
26 nnmulscl 
 |-  ( ( y e. NN_s /\ z e. NN_s ) -> ( y x.s z ) e. NN_s )
27 24 25 26 syl2anc 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( y x.s z ) e. NN_s )
28 27 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( y x.s z ) e. No )
29 23 28 subscld 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x x.s z ) -s ( y x.s z ) ) e. No )
30 nnmulscl 
 |-  ( ( x e. NN_s /\ w e. NN_s ) -> ( x x.s w ) e. NN_s )
31 30 ad2ant2rl 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( x x.s w ) e. NN_s )
32 31 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( x x.s w ) e. No )
33 nnmulscl 
 |-  ( ( y e. NN_s /\ w e. NN_s ) -> ( y x.s w ) e. NN_s )
34 33 adantl 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( y x.s w ) e. NN_s )
35 34 nnsnod 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( y x.s w ) e. No )
36 29 32 35 subsubs2d 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( ( x x.s z ) -s ( y x.s z ) ) -s ( ( x x.s w ) -s ( y x.s w ) ) ) = ( ( ( x x.s z ) -s ( y x.s z ) ) +s ( ( y x.s w ) -s ( x x.s w ) ) ) )
37 12 14 17 subsdird 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) x.s z ) = ( ( x x.s z ) -s ( y x.s z ) ) )
38 12 14 19 subsdird 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) x.s w ) = ( ( x x.s w ) -s ( y x.s w ) ) )
39 37 38 oveq12d 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( ( x -s y ) x.s z ) -s ( ( x -s y ) x.s w ) ) = ( ( ( x x.s z ) -s ( y x.s z ) ) -s ( ( x x.s w ) -s ( y x.s w ) ) ) )
40 23 35 28 32 addsubs4d 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( ( ( x x.s z ) -s ( y x.s z ) ) +s ( ( y x.s w ) -s ( x x.s w ) ) ) )
41 36 39 40 3eqtr4d 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( ( x -s y ) x.s z ) -s ( ( x -s y ) x.s w ) ) = ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) )
42 20 41 eqtrd 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) x.s ( z -s w ) ) = ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) )
43 nnaddscl 
 |-  ( ( ( x x.s z ) e. NN_s /\ ( y x.s w ) e. NN_s ) -> ( ( x x.s z ) +s ( y x.s w ) ) e. NN_s )
44 22 34 43 syl2anc 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x x.s z ) +s ( y x.s w ) ) e. NN_s )
45 nnaddscl 
 |-  ( ( ( y x.s z ) e. NN_s /\ ( x x.s w ) e. NN_s ) -> ( ( y x.s z ) +s ( x x.s w ) ) e. NN_s )
46 27 31 45 syl2anc 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( y x.s z ) +s ( x x.s w ) ) e. NN_s )
47 eqid 
 |-  ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) )
48 rspceov 
 |-  ( ( ( ( x x.s z ) +s ( y x.s w ) ) e. NN_s /\ ( ( y x.s z ) +s ( x x.s w ) ) e. NN_s /\ ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) ) -> E. t e. NN_s E. u e. NN_s ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( t -s u ) )
49 47 48 mp3an3 
 |-  ( ( ( ( x x.s z ) +s ( y x.s w ) ) e. NN_s /\ ( ( y x.s z ) +s ( x x.s w ) ) e. NN_s ) -> E. t e. NN_s E. u e. NN_s ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( t -s u ) )
50 44 46 49 syl2anc 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> E. t e. NN_s E. u e. NN_s ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( t -s u ) )
51 elzs 
 |-  ( ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) e. ZZ_s <-> E. t e. NN_s E. u e. NN_s ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) = ( t -s u ) )
52 50 51 sylibr 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( ( x x.s z ) +s ( y x.s w ) ) -s ( ( y x.s z ) +s ( x x.s w ) ) ) e. ZZ_s )
53 42 52 eqeltrd 
 |-  ( ( ( x e. NN_s /\ z e. NN_s ) /\ ( y e. NN_s /\ w e. NN_s ) ) -> ( ( x -s y ) x.s ( z -s w ) ) e. ZZ_s )
54 oveq12 
 |-  ( ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( A x.s B ) = ( ( x -s y ) x.s ( z -s w ) ) )
55 54 eleq1d 
 |-  ( ( A = ( x -s y ) /\ B = ( z -s w ) ) -> ( ( A x.s B ) e. ZZ_s <-> ( ( x -s y ) x.s ( z -s w ) ) e. ZZ_s ) )
56 53 55 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 x.s B ) e. ZZ_s ) )
57 56 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 x.s B ) e. ZZ_s ) )
58 57 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 x.s B ) e. ZZ_s )
59 10 58 sylbir 
 |-  ( ( 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 ) ) -> ( A x.s B ) e. ZZ_s )
60 4 6 59 syl2anc 
 |-  ( ph -> ( A x.s B ) e. ZZ_s )