Theorem expadds

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

	Ref	Expression
Assertion	expadds	Could not format assertion : No typesetting found for |- ( ( A e. No /\ M e. NN0_s /\ N e. NN0_s ) -> ( A ^su ( M +s N ) ) = ( ( A ^su M ) x.s ( A ^su N ) ) ) with typecode |-

Proof

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