Theorem zs12half

Description: Half of a dyadic is a dyadic. (Contributed by Scott Fenton, 11-Dec-2025)

	Ref	Expression
Assertion	zs12half	Could not format assertion : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A /su 2s ) 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		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
3		exps1	Could not format ( 2s e. No -> ( 2s ^su 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 1s ) = 2s ) with typecode |-
4	2 3	ax-mp	Could not format ( 2s ^su 1s ) = 2s : No typesetting found for |- ( 2s ^su 1s ) = 2s with typecode |-
5	4	oveq2i	Could not format ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( ( a /su ( 2s ^su n ) ) /su 2s ) : No typesetting found for |- ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( ( a /su ( 2s ^su n ) ) /su 2s ) with typecode |-
6		zno	$$⊢a\in {\mathbb{Z}}_s\to a\in \mathrm{No}$$
7	6	adantr	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to a\in \mathrm{No}$$
8		simpr	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to n\in {\mathbb{N}}_{\mathrm{0s}}$$
9		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
10	9	a1i	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
11	7 8 10	pw2divscan4d	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) = ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
12	4 2	eqeltri	Could not format ( 2s ^su 1s ) e. No : No typesetting found for |- ( 2s ^su 1s ) e. No with typecode |-
13	12	a1i	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su 1s ) e. No ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( 2s ^su 1s ) e. No ) with typecode |-
14		peano2n0s	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
15	14	adantl	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to n{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
16	13 7 15	pw2divsassd	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( 2s ^su 1s ) x.s a ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
17	11 16	eqtr2d	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) ) with typecode |-
18	7 8	pw2divscld	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) e. No ) with typecode |-
19	7 15	pw2divscld	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. No ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. No ) with typecode |-
20	18 19 10	pw2divsmuld	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) <-> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) <-> ( ( 2s ^su 1s ) x.s ( a /su ( 2s ^su ( n +s 1s ) ) ) ) = ( a /su ( 2s ^su n ) ) ) ) with typecode |-
21	17 20	mpbird	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su ( 2s ^su 1s ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
22	5 21	eqtr3id	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
23		oveq1	Could not format ( b = a -> ( b /su ( 2s ^su m ) ) = ( a /su ( 2s ^su m ) ) ) : No typesetting found for |- ( b = a -> ( b /su ( 2s ^su m ) ) = ( a /su ( 2s ^su m ) ) ) with typecode |-
24	23	eqeq2d	Could not format ( b = a -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) ) ) : No typesetting found for |- ( b = a -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) ) ) with typecode |-
25		oveq2	Could not format ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) with typecode |-
26	25	oveq2d	Could not format ( m = ( n +s 1s ) -> ( a /su ( 2s ^su m ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( a /su ( 2s ^su m ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
27	26	eqeq2d	Could not format ( m = ( n +s 1s ) -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su m ) ) <-> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
28		simpl	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to a\in {\mathbb{Z}}_s$$
29		eqidd	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( a /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
30	24 27 28 15 29	2rspcedvdw	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) ) with typecode |-
31		elzs12	Could not format ( ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) ) : No typesetting found for |- ( ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] <-> E. b e. ZZ_s E. m e. NN0_s ( a /su ( 2s ^su ( n +s 1s ) ) ) = ( b /su ( 2s ^su m ) ) ) with typecode |-
32	30 31	sylibr	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su ( n +s 1s ) ) ) e. ZZ_s[1/2] ) with typecode |-
33	22 32	eqeltrd	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] ) with typecode |-
34		oveq1	Could not format ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) = ( ( a /su ( 2s ^su n ) ) /su 2s ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) = ( ( a /su ( 2s ^su n ) ) /su 2s ) ) with typecode |-
35	34	eleq1d	Could not format ( A = ( a /su ( 2s ^su n ) ) -> ( ( A /su 2s ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su n ) ) -> ( ( A /su 2s ) e. ZZ_s[1/2] <-> ( ( a /su ( 2s ^su n ) ) /su 2s ) e. ZZ_s[1/2] ) ) with typecode |-
36	33 35	syl5ibrcom	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) e. ZZ_s[1/2] ) ) with typecode |-
37	36	rexlimivv	Could not format ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) -> ( A /su 2s ) 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 ) ) -> ( A /su 2s ) e. ZZ_s[1/2] ) with typecode |-
38	1 37	sylbi	Could not format ( A e. ZZ_s[1/2] -> ( A /su 2s ) e. ZZ_s[1/2] ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A /su 2s ) e. ZZ_s[1/2] ) with typecode |-