Metamath Proof Explorer

Theorem zs12no

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

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

Proof

Step Hyp Ref Expression
1 elzs12 
 |-  ( A e. ZZ_s[1/2] <-> E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) )
2 zno 
 |-  ( a e. ZZ_s -> a e. No )
3 2 adantr 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> a e. No )
4 simpr 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> n e. NN0_s )
5 3 4 pw2divscld 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( a /su ( 2s ^su n ) ) e. No )
6 eleq1 
 |-  ( A = ( a /su ( 2s ^su n ) ) -> ( A e. No <-> ( a /su ( 2s ^su n ) ) e. No ) )
7 5 6 syl5ibrcom 
 |-  ( ( a e. ZZ_s /\ n e. NN0_s ) -> ( A = ( a /su ( 2s ^su n ) ) -> A e. No ) )
8 7 rexlimivv 
 |-  ( E. a e. ZZ_s E. n e. NN0_s A = ( a /su ( 2s ^su n ) ) -> A e. No )
9 1 8 sylbi 
 |-  ( A e. ZZ_s[1/2] -> A e. No )