Theorem zs12addscl

Description: The dyadics are closed under addition. (Contributed by Scott Fenton, 11-Dec-2025)

	Ref	Expression
Assertion	zs12addscl	Could not format assertion : No typesetting found for |- ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s B ) e. ZZ_s[1/2] ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) ) with typecode |-
2		elzs12	Could not format ( B e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) : No typesetting found for |- ( B e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) with typecode |-
3		reeanv	Could not format ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) with typecode |-
4	3	2rexbii	Could not format ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) with typecode |-
5		reeanv	Could not format ( E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( E. a e. ZZ_s E. b e. ZZ_s ( E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) with typecode |-
6	4 5	bitri	Could not format ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) <-> ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) ) with typecode |-
7		simpll	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to a\in {\mathbb{Z}}_s$$
8	7	znod	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to a\in \mathrm{No}$$
9		simprl	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to n\in {\mathbb{N}}_{\mathrm{0s}}$$
10		simprr	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to m\in {\mathbb{N}}_{\mathrm{0s}}$$
11	8 9 10	pw2divscan4d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
12		simplr	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to b\in {\mathbb{Z}}_s$$
13	12	znod	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to b\in \mathrm{No}$$
14	13 10 9	pw2divscan4d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) ) with typecode |-
15	10	n0snod	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to m\in \mathrm{No}$$
16	9	n0snod	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to n\in \mathrm{No}$$
17	15 16	addscomd	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to m{+}_{s}n=n{+}_{s}m$$
18	17	oveq2d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su ( m +s n ) ) = ( 2s ^su ( n +s m ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su ( m +s n ) ) = ( 2s ^su ( n +s m ) ) ) with typecode |-
19	18	oveq2d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( m +s n ) ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
20	14 19	eqtrd	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( b /su ( 2s ^su m ) ) = ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
21	11 20	oveq12d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) ) with typecode |-
22		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
23		expscl	Could not format ( ( 2s e. No /\ m e. NN0_s ) -> ( 2s ^su m ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ m e. NN0_s ) -> ( 2s ^su m ) e. No ) with typecode |-
24	22 10 23	sylancr	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. No ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. No ) with typecode |-
25	24 8	mulscld	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. No ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. No ) with typecode |-
26		expscl	Could not format ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) with typecode |-
27	22 9 26	sylancr	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. No ) with typecode |-
28	27 13	mulscld	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. No ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. No ) with typecode |-
29		n0addscl	$$⊢\left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to n{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}$$
30	29	adantl	$$⊢\left(\left(a\in {\mathbb{Z}}_s\wedge b\in {\mathbb{Z}}_s\right)\wedge \left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to n{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}$$
31	25 28 30	pw2divsdird	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) /su ( 2s ^su ( n +s m ) ) ) +s ( ( ( 2s ^su n ) x.s b ) /su ( 2s ^su ( n +s m ) ) ) ) ) with typecode |-
32	21 31	eqtr4d	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
33		oveq1	Could not format ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( c /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) ) : No typesetting found for |- ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( c /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) ) with typecode |-
34	33	eqeq2d	Could not format ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) ) ) : No typesetting found for |- ( c = ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) ) ) with typecode |-
35		oveq2	Could not format ( p = ( n +s m ) -> ( 2s ^su p ) = ( 2s ^su ( n +s m ) ) ) : No typesetting found for |- ( p = ( n +s m ) -> ( 2s ^su p ) = ( 2s ^su ( n +s m ) ) ) with typecode |-
36	35	oveq2d	Could not format ( p = ( n +s m ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( p = ( n +s m ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
37	36	eqeq2d	Could not format ( p = ( n +s m ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) ) : No typesetting found for |- ( p = ( n +s m ) -> ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su p ) ) <-> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) ) with typecode |-
38		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
39		nnzs	Could not format ( 2s e. NN_s -> 2s e. ZZ_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. ZZ_s ) with typecode |-
40	38 39	ax-mp	Could not format 2s e. ZZ_s : No typesetting found for |- 2s e. ZZ_s with typecode |-
41		zexpscl	Could not format ( ( 2s e. ZZ_s /\ m e. NN0_s ) -> ( 2s ^su m ) e. ZZ_s ) : No typesetting found for |- ( ( 2s e. ZZ_s /\ m e. NN0_s ) -> ( 2s ^su m ) e. ZZ_s ) with typecode |-
42	40 10 41	sylancr	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. ZZ_s ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su m ) e. ZZ_s ) with typecode |-
43	42 7	zmulscld	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. ZZ_s ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su m ) x.s a ) e. ZZ_s ) with typecode |-
44		zexpscl	Could not format ( ( 2s e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su n ) e. ZZ_s ) : No typesetting found for |- ( ( 2s e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su n ) e. ZZ_s ) with typecode |-
45	40 9 44	sylancr	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. ZZ_s ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( 2s ^su n ) e. ZZ_s ) with typecode |-
46	45 12	zmulscld	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. ZZ_s ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( 2s ^su n ) x.s b ) e. ZZ_s ) with typecode |-
47	43 46	zaddscld	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) e. ZZ_s ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) e. ZZ_s ) with typecode |-
48		eqidd	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) ) with typecode |-
49	34 37 47 30 48	2rspcedvdw	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) ) with typecode |-
50		elzs12	Could not format ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] <-> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) ) : No typesetting found for |- ( ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] <-> E. c e. ZZ_s E. p e. NN0_s ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) = ( c /su ( 2s ^su p ) ) ) with typecode |-
51	49 50	sylibr	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( ( ( 2s ^su m ) x.s a ) +s ( ( 2s ^su n ) x.s b ) ) /su ( 2s ^su ( n +s m ) ) ) e. ZZ_s[1/2] ) with typecode |-
52	32 51	eqeltrd	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] ) with typecode |-
53		oveq12	Could not format ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) = ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) = ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) ) with typecode |-
54	53	eleq1d	Could not format ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( ( A +s B ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( ( A +s B ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) +s ( b /su ( 2s ^su m ) ) ) e. ZZ_s[1/2] ) ) with typecode |-
55	52 54	syl5ibrcom	Could not format ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( ( a e. ZZ_s /\ b e. ZZ_s ) /\ ( n e. NN0_s /\ m e. NN0_s ) ) -> ( ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) ) with typecode |-
56	55	rexlimdvva	Could not format ( ( a e. ZZ_s /\ b e. ZZ_s ) -> ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ b e. ZZ_s ) -> ( E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) ) with typecode |-
57	56	rexlimivv	Could not format ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) : No typesetting found for |- ( E. a e. ZZ_s E. b e. ZZ_s E. n e. NN0_s E. m e. NN0_s ( A = ( a /su ( 2s ^su n ) ) /\ B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) with typecode |-
58	6 57	sylbir	Could not format ( ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) /\ E. b e. ZZ_s E. m e. NN0_s B = ( b /su ( 2s ^su m ) ) ) -> ( A +s B ) e. ZZ_s[1/2] ) with typecode |-
59	1 2 58	syl2anb	Could not format ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s B ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( A e. ZZ_s[1/2] /\ B e. ZZ_s[1/2] ) -> ( A +s B ) e. ZZ_s[1/2] ) with typecode |-