Theorem zzs12

Description: A surreal integer is a dyadic fraction. (Contributed by Scott Fenton, 7-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
2		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
3	1 2	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
4	3	oveq2i	Could not format ( A /su ( 2s ^su 0s ) ) = ( A /su 1s ) : No typesetting found for |- ( A /su ( 2s ^su 0s ) ) = ( A /su 1s ) with typecode |-
5		zno	$$⊢A\in {\mathbb{Z}}_s\to A\in \mathrm{No}$$
6		divs1	$$⊢A\in \mathrm{No}\to A{/}_{\mathrm{su}}{1}_s=A$$
7	5 6	syl	$$⊢A\in {\mathbb{Z}}_s\to A{/}_{\mathrm{su}}{1}_s=A$$
8	4 7	eqtr2id	Could not format ( A e. ZZ_s -> A = ( A /su ( 2s ^su 0s ) ) ) : No typesetting found for |- ( A e. ZZ_s -> A = ( A /su ( 2s ^su 0s ) ) ) with typecode |-
9		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
10		oveq1	Could not format ( x = A -> ( x /su ( 2s ^su y ) ) = ( A /su ( 2s ^su y ) ) ) : No typesetting found for |- ( x = A -> ( x /su ( 2s ^su y ) ) = ( A /su ( 2s ^su y ) ) ) with typecode |-
11	10	eqeq2d	Could not format ( x = A -> ( A = ( x /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( x = A -> ( A = ( x /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su y ) ) ) ) with typecode |-
12		oveq2	Could not format ( y = 0s -> ( 2s ^su y ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( y = 0s -> ( 2s ^su y ) = ( 2s ^su 0s ) ) with typecode |-
13	12	oveq2d	Could not format ( y = 0s -> ( A /su ( 2s ^su y ) ) = ( A /su ( 2s ^su 0s ) ) ) : No typesetting found for |- ( y = 0s -> ( A /su ( 2s ^su y ) ) = ( A /su ( 2s ^su 0s ) ) ) with typecode |-
14	13	eqeq2d	Could not format ( y = 0s -> ( A = ( A /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su 0s ) ) ) ) : No typesetting found for |- ( y = 0s -> ( A = ( A /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su 0s ) ) ) ) with typecode |-
15	11 14	rspc2ev	Could not format ( ( A e. ZZ_s /\ 0s e. NN0_s /\ A = ( A /su ( 2s ^su 0s ) ) ) -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( A e. ZZ_s /\ 0s e. NN0_s /\ A = ( A /su ( 2s ^su 0s ) ) ) -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
16	9 15	mp3an2	Could not format ( ( A e. ZZ_s /\ A = ( A /su ( 2s ^su 0s ) ) ) -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( ( A e. ZZ_s /\ A = ( A /su ( 2s ^su 0s ) ) ) -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
17	8 16	mpdan	Could not format ( A e. ZZ_s -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A e. ZZ_s -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
18		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
19	17 18	sylibr	Could not format ( A e. ZZ_s -> A e. ZZ_s[1/2] ) : No typesetting found for |- ( A e. ZZ_s -> A e. ZZ_s[1/2] ) with typecode |-