Theorem zs12no

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

	Ref	Expression
Assertion	zs12no	Could not format assertion : No typesetting found for |- ( A e. ZZ_s[1/2] -> A e. No ) 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		zno	$$⊢a\in {\mathbb{Z}}_s\to a\in \mathrm{No}$$
3	2	adantr	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to a\in \mathrm{No}$$
4		simpr	$$⊢\left(a\in {\mathbb{Z}}_s\wedge n\in {\mathbb{N}}_{\mathrm{0s}}\right)\to n\in {\mathbb{N}}_{\mathrm{0s}}$$
5	3 4	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 |-
6		eleq1	Could not format ( A = ( a /su ( 2s ^su n ) ) -> ( A e. No <-> ( a /su ( 2s ^su n ) ) e. No ) ) : No typesetting found for |- ( A = ( a /su ( 2s ^su n ) ) -> ( A e. No <-> ( a /su ( 2s ^su n ) ) e. No ) ) with typecode |-
7	5 6	syl5ibrcom	Could not format ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> A e. No ) ) : No typesetting found for |- ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> A e. No ) ) with typecode |-
8	7	rexlimivv	Could not format ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) -> A e. No ) : No typesetting found for |- ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) -> A e. No ) with typecode |-
9	1 8	sylbi	Could not format ( A e. ZZ_s[1/2] -> A e. No ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> A e. No ) with typecode |-