Metamath Proof Explorer

Theorem zzs12

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

Ref Expression
Assertion zzs12 
|- ( A e. ZZ_s -> A e. ZZ_s[1/2] )

Proof

Step Hyp Ref Expression
1 2sno 
 |-  2s e. No
2 exps0 
 |-  ( 2s e. No -> ( 2s ^su 0s ) = 1s )
3 1 2 ax-mp 
 |-  ( 2s ^su 0s ) = 1s
4 3 oveq2i 
 |-  ( A /su ( 2s ^su 0s ) ) = ( A /su 1s )
5 zno 
 |-  ( A e. ZZ_s -> A e. No )
6 divs1 
 |-  ( A e. No -> ( A /su 1s ) = A )
7 5 6 syl 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = A )
8 4 7 eqtr2id 
 |-  ( A e. ZZ_s -> A = ( A /su ( 2s ^su 0s ) ) )
9 0n0s 
 |-  0s e. NN0_s
10 oveq1 
 |-  ( x = A -> ( x /su ( 2s ^su y ) ) = ( A /su ( 2s ^su y ) ) )
11 10 eqeq2d 
 |-  ( x = A -> ( A = ( x /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su y ) ) ) )
12 oveq2 
 |-  ( y = 0s -> ( 2s ^su y ) = ( 2s ^su 0s ) )
13 12 oveq2d 
 |-  ( y = 0s -> ( A /su ( 2s ^su y ) ) = ( A /su ( 2s ^su 0s ) ) )
14 13 eqeq2d 
 |-  ( y = 0s -> ( A = ( A /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su 0s ) ) ) )
15 11 14 rspc2ev 
 |-  ( ( 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 ) ) )
16 9 15 mp3an2 
 |-  ( ( 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 ) ) )
17 8 16 mpdan 
 |-  ( A e. ZZ_s -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
18 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
19 17 18 sylibr 
 |-  ( A e. ZZ_s -> A e. ZZ_s[1/2] )