Metamath Proof Explorer

Theorem nnmulscl

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

Ref Expression
Assertion nnmulscl 
|- ( ( A e. NN_s /\ B e. NN_s ) -> ( A x.s B ) e. NN_s )

Proof

Step Hyp Ref Expression
1 n0mulscl 
 |-  ( ( A e. NN0_s /\ B e. NN0_s ) -> ( A x.s B ) e. NN0_s )
2 1 ad2ant2r 
 |-  ( ( ( A e. NN0_s /\ 0s  ( A x.s B ) e. NN0_s )
3 simpll 
 |-  ( ( ( A e. NN0_s /\ 0s  A e. NN0_s )
4 3 n0snod 
 |-  ( ( ( A e. NN0_s /\ 0s  A e. No )
5 simprl 
 |-  ( ( ( A e. NN0_s /\ 0s  B e. NN0_s )
6 5 n0snod 
 |-  ( ( ( A e. NN0_s /\ 0s  B e. No )
7 simplr 
 |-  ( ( ( A e. NN0_s /\ 0s  0s
8 simprr 
 |-  ( ( ( A e. NN0_s /\ 0s  0s
9 4 6 7 8 mulsgt0d 
 |-  ( ( ( A e. NN0_s /\ 0s  0s
10 2 9 jca 
 |-  ( ( ( A e. NN0_s /\ 0s  ( ( A x.s B ) e. NN0_s /\ 0s
11 elnns2 
 |-  ( A e. NN_s <-> ( A e. NN0_s /\ 0s
12 elnns2 
 |-  ( B e. NN_s <-> ( B e. NN0_s /\ 0s
13 11 12 anbi12i 
 |-  ( ( A e. NN_s /\ B e. NN_s ) <-> ( ( A e. NN0_s /\ 0s
14 elnns2 
 |-  ( ( A x.s B ) e. NN_s <-> ( ( A x.s B ) e. NN0_s /\ 0s
15 10 13 14 3imtr4i 
 |-  ( ( A e. NN_s /\ B e. NN_s ) -> ( A x.s B ) e. NN_s )