Metamath Proof Explorer

Theorem expadds

Description: Sum of exponents law for surreals. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion expadds 
|- ( ( A e. No /\ M e. NN0_s /\ N e. NN0_s ) -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0s -> ( M +s j ) = ( M +s 0s ) )
2 1 oveq2d 
 |-  ( j = 0s -> ( A ^su ( M +s j ) ) = ( A ^su ( M +s 0s ) ) )
3 oveq2 
 |-  ( j = 0s -> ( A ^su j ) = ( A ^su 0s ) )
4 3 oveq2d 
 |-  ( j = 0s -> ( ( A ^su M ) x.s ( A ^su j ) ) = ( ( A ^su M ) x.s ( A ^su 0s ) ) )
5 2 4 eqeq12d 
 |-  ( j = 0s -> ( ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) <-> ( A ^su ( M +s 0s ) ) = ( ( A ^su M ) x.s ( A ^su 0s ) ) ) )
6 5 imbi2d 
 |-  ( j = 0s -> ( ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) ) <-> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s 0s ) ) = ( ( A ^su M ) x.s ( A ^su 0s ) ) ) ) )
7 oveq2 
 |-  ( j = k -> ( M +s j ) = ( M +s k ) )
8 7 oveq2d 
 |-  ( j = k -> ( A ^su ( M +s j ) ) = ( A ^su ( M +s k ) ) )
9 oveq2 
 |-  ( j = k -> ( A ^su j ) = ( A ^su k ) )
10 9 oveq2d 
 |-  ( j = k -> ( ( A ^su M ) x.s ( A ^su j ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) )
11 8 10 eqeq12d 
 |-  ( j = k -> ( ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) <-> ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) )
12 11 imbi2d 
 |-  ( j = k -> ( ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) ) <-> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) )
13 oveq2 
 |-  ( j = ( k +s 1s ) -> ( M +s j ) = ( M +s ( k +s 1s ) ) )
14 13 oveq2d 
 |-  ( j = ( k +s 1s ) -> ( A ^su ( M +s j ) ) = ( A ^su ( M +s ( k +s 1s ) ) ) )
15 oveq2 
 |-  ( j = ( k +s 1s ) -> ( A ^su j ) = ( A ^su ( k +s 1s ) ) )
16 15 oveq2d 
 |-  ( j = ( k +s 1s ) -> ( ( A ^su M ) x.s ( A ^su j ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) )
17 14 16 eqeq12d 
 |-  ( j = ( k +s 1s ) -> ( ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) <-> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) ) )
18 17 imbi2d 
 |-  ( j = ( k +s 1s ) -> ( ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) ) <-> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) ) ) )
19 oveq2 
 |-  ( j = N -> ( M +s j ) = ( M +s N ) )
20 19 oveq2d 
 |-  ( j = N -> ( A ^su ( M +s j ) ) = ( A ^su ( M +s N ) ) )
21 oveq2 
 |-  ( j = N -> ( A ^su j ) = ( A ^su N ) )
22 21 oveq2d 
 |-  ( j = N -> ( ( A ^su M ) x.s ( A ^su j ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) )
23 20 22 eqeq12d 
 |-  ( j = N -> ( ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) <-> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) ) )
24 23 imbi2d 
 |-  ( j = N -> ( ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s j ) ) = ( ( A ^su M ) x.s ( A ^su j ) ) ) <-> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) ) ) )
25 expscl 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( A ^su M ) e. No )
26 25 mulsridd 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( ( A ^su M ) x.s 1s ) = ( A ^su M ) )
27 exps0 
 |-  ( A e. No -> ( A ^su 0s ) = 1s )
28 27 oveq2d 
 |-  ( A e. No -> ( ( A ^su M ) x.s ( A ^su 0s ) ) = ( ( A ^su M ) x.s 1s ) )
29 28 adantr 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( ( A ^su M ) x.s ( A ^su 0s ) ) = ( ( A ^su M ) x.s 1s ) )
30 n0sno 
 |-  ( M e. NN0_s -> M e. No )
31 30 adantl 
 |-  ( ( A e. No /\ M e. NN0_s ) -> M e. No )
32 31 addsridd 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( M +s 0s ) = M )
33 32 oveq2d 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s 0s ) ) = ( A ^su M ) )
34 26 29 33 3eqtr4rd 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s 0s ) ) = ( ( A ^su M ) x.s ( A ^su 0s ) ) )
35 simprr 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) )
36 35 oveq1d 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( ( A ^su ( M +s k ) ) x.s A ) = ( ( ( A ^su M ) x.s ( A ^su k ) ) x.s A ) )
37 25 adantr 
 |-  ( ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) -> ( A ^su M ) e. No )
38 37 adantl 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su M ) e. No )
39 simprll 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> A e. No )
40 simpl 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> k e. NN0_s )
41 expscl 
 |-  ( ( A e. No /\ k e. NN0_s ) -> ( A ^su k ) e. No )
42 39 40 41 syl2anc 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su k ) e. No )
43 38 42 39 mulsassd 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( ( ( A ^su M ) x.s ( A ^su k ) ) x.s A ) = ( ( A ^su M ) x.s ( ( A ^su k ) x.s A ) ) )
44 36 43 eqtrd 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( ( A ^su ( M +s k ) ) x.s A ) = ( ( A ^su M ) x.s ( ( A ^su k ) x.s A ) ) )
45 simprlr 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> M e. NN0_s )
46 45 n0snod 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> M e. No )
47 40 n0snod 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> k e. No )
48 1sno 
 |-  1s e. No
49 48 a1i 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> 1s e. No )
50 46 47 49 addsassd 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( ( M +s k ) +s 1s ) = ( M +s ( k +s 1s ) ) )
51 50 oveq2d 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( ( M +s k ) +s 1s ) ) = ( A ^su ( M +s ( k +s 1s ) ) ) )
52 n0addscl 
 |-  ( ( M e. NN0_s /\ k e. NN0_s ) -> ( M +s k ) e. NN0_s )
53 45 40 52 syl2anc 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( M +s k ) e. NN0_s )
54 expsp1 
 |-  ( ( A e. No /\ ( M +s k ) e. NN0_s ) -> ( A ^su ( ( M +s k ) +s 1s ) ) = ( ( A ^su ( M +s k ) ) x.s A ) )
55 39 53 54 syl2anc 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( ( M +s k ) +s 1s ) ) = ( ( A ^su ( M +s k ) ) x.s A ) )
56 51 55 eqtr3d 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su ( M +s k ) ) x.s A ) )
57 expsp1 
 |-  ( ( A e. No /\ k e. NN0_s ) -> ( A ^su ( k +s 1s ) ) = ( ( A ^su k ) x.s A ) )
58 39 40 57 syl2anc 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( k +s 1s ) ) = ( ( A ^su k ) x.s A ) )
59 58 oveq2d 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( ( A ^su k ) x.s A ) ) )
60 44 56 59 3eqtr4d 
 |-  ( ( k e. NN0_s /\ ( ( A e. No /\ M e. NN0_s ) /\ ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) ) -> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) )
61 60 exp32 
 |-  ( k e. NN0_s -> ( ( A e. No /\ M e. NN0_s ) -> ( ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) -> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) ) ) )
62 61 a2d 
 |-  ( k e. NN0_s -> ( ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s k ) ) = ( ( A ^su M ) x.s ( A ^su k ) ) ) -> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s ( k +s 1s ) ) ) = ( ( A ^su M ) x.s ( A ^su ( k +s 1s ) ) ) ) ) )
63 6 12 18 24 34 62 n0sind 
 |-  ( N e. NN0_s -> ( ( A e. No /\ M e. NN0_s ) -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) ) )
64 63 com12 
 |-  ( ( A e. No /\ M e. NN0_s ) -> ( N e. NN0_s -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) ) )
65 64 3impia 
 |-  ( ( A e. No /\ M e. NN0_s /\ N e. NN0_s ) -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) )