Metamath Proof Explorer

Theorem n0mulscl

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = 0s -> ( A x.s n ) = ( A x.s 0s ) )
2 1 eleq1d 
 |-  ( n = 0s -> ( ( A x.s n ) e. NN0_s <-> ( A x.s 0s ) e. NN0_s ) )
3 2 imbi2d 
 |-  ( n = 0s -> ( ( A e. NN0_s -> ( A x.s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A x.s 0s ) e. NN0_s ) ) )
4 oveq2 
 |-  ( n = m -> ( A x.s n ) = ( A x.s m ) )
5 4 eleq1d 
 |-  ( n = m -> ( ( A x.s n ) e. NN0_s <-> ( A x.s m ) e. NN0_s ) )
6 5 imbi2d 
 |-  ( n = m -> ( ( A e. NN0_s -> ( A x.s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A x.s m ) e. NN0_s ) ) )
7 oveq2 
 |-  ( n = ( m +s 1s ) -> ( A x.s n ) = ( A x.s ( m +s 1s ) ) )
8 7 eleq1d 
 |-  ( n = ( m +s 1s ) -> ( ( A x.s n ) e. NN0_s <-> ( A x.s ( m +s 1s ) ) e. NN0_s ) )
9 8 imbi2d 
 |-  ( n = ( m +s 1s ) -> ( ( A e. NN0_s -> ( A x.s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A x.s ( m +s 1s ) ) e. NN0_s ) ) )
10 oveq2 
 |-  ( n = B -> ( A x.s n ) = ( A x.s B ) )
11 10 eleq1d 
 |-  ( n = B -> ( ( A x.s n ) e. NN0_s <-> ( A x.s B ) e. NN0_s ) )
12 11 imbi2d 
 |-  ( n = B -> ( ( A e. NN0_s -> ( A x.s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A x.s B ) e. NN0_s ) ) )
13 n0sno 
 |-  ( A e. NN0_s -> A e. No )
14 muls01 
 |-  ( A e. No -> ( A x.s 0s ) = 0s )
15 13 14 syl 
 |-  ( A e. NN0_s -> ( A x.s 0s ) = 0s )
16 0n0s 
 |-  0s e. NN0_s
17 15 16 eqeltrdi 
 |-  ( A e. NN0_s -> ( A x.s 0s ) e. NN0_s )
18 13 ad2antrr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> A e. No )
19 n0sno 
 |-  ( m e. NN0_s -> m e. No )
20 19 ad2antlr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> m e. No )
21 1sno 
 |-  1s e. No
22 21 a1i 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> 1s e. No )
23 18 20 22 addsdid 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> ( A x.s ( m +s 1s ) ) = ( ( A x.s m ) +s ( A x.s 1s ) ) )
24 13 mulsridd 
 |-  ( A e. NN0_s -> ( A x.s 1s ) = A )
25 24 oveq2d 
 |-  ( A e. NN0_s -> ( ( A x.s m ) +s ( A x.s 1s ) ) = ( ( A x.s m ) +s A ) )
26 25 ad2antrr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> ( ( A x.s m ) +s ( A x.s 1s ) ) = ( ( A x.s m ) +s A ) )
27 23 26 eqtrd 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> ( A x.s ( m +s 1s ) ) = ( ( A x.s m ) +s A ) )
28 n0addscl 
 |-  ( ( ( A x.s m ) e. NN0_s /\ A e. NN0_s ) -> ( ( A x.s m ) +s A ) e. NN0_s )
29 28 ancoms 
 |-  ( ( A e. NN0_s /\ ( A x.s m ) e. NN0_s ) -> ( ( A x.s m ) +s A ) e. NN0_s )
30 29 adantlr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> ( ( A x.s m ) +s A ) e. NN0_s )
31 27 30 eqeltrd 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A x.s m ) e. NN0_s ) -> ( A x.s ( m +s 1s ) ) e. NN0_s )
32 31 ex 
 |-  ( ( A e. NN0_s /\ m e. NN0_s ) -> ( ( A x.s m ) e. NN0_s -> ( A x.s ( m +s 1s ) ) e. NN0_s ) )
33 32 expcom 
 |-  ( m e. NN0_s -> ( A e. NN0_s -> ( ( A x.s m ) e. NN0_s -> ( A x.s ( m +s 1s ) ) e. NN0_s ) ) )
34 33 a2d 
 |-  ( m e. NN0_s -> ( ( A e. NN0_s -> ( A x.s m ) e. NN0_s ) -> ( A e. NN0_s -> ( A x.s ( m +s 1s ) ) e. NN0_s ) ) )
35 3 6 9 12 17 34 n0sind 
 |-  ( B e. NN0_s -> ( A e. NN0_s -> ( A x.s B ) e. NN0_s ) )
36 35 impcom 
 |-  ( ( A e. NN0_s /\ B e. NN0_s ) -> ( A x.s B ) e. NN0_s )