Metamath Proof Explorer

Theorem zz12s

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

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

Proof

Step Hyp Ref Expression
1 2no 
 |-  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 5 divs1d 
 |-  ( A e. ZZ_s -> ( A /su 1s ) = A )
7 4 6 eqtr2id 
 |-  ( A e. ZZ_s -> A = ( A /su ( 2s ^su 0s ) ) )
8 0n0s 
 |-  0s e. NN0_s
9 oveq1 
 |-  ( x = A -> ( x /su ( 2s ^su y ) ) = ( A /su ( 2s ^su y ) ) )
10 9 eqeq2d 
 |-  ( x = A -> ( A = ( x /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su y ) ) ) )
11 oveq2 
 |-  ( y = 0s -> ( 2s ^su y ) = ( 2s ^su 0s ) )
12 11 oveq2d 
 |-  ( y = 0s -> ( A /su ( 2s ^su y ) ) = ( A /su ( 2s ^su 0s ) ) )
13 12 eqeq2d 
 |-  ( y = 0s -> ( A = ( A /su ( 2s ^su y ) ) <-> A = ( A /su ( 2s ^su 0s ) ) ) )
14 10 13 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 ) ) )
15 8 14 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 ) ) )
16 7 15 mpdan 
 |-  ( A e. ZZ_s -> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
17 elz12s 
 |-  ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) )
18 16 17 sylibr 
 |-  ( A e. ZZ_s -> A e. ZZ_s[1/2] )