Metamath Proof Explorer

Theorem bdayfin

Description: A surreal has a finite birthday iff it is a dyadic fraction. (Contributed by Scott Fenton, 26-Feb-2026)

Ref Expression
Assertion bdayfin 
|- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( bday ` A ) e. _om ) )

Proof

Step Hyp Ref Expression
1 zs12bday 
 |-  ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om )
2 bdayfinlem 
 |-  ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] )
3 2 3exp 
 |-  ( A e. No -> ( 0s <_s A -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) )
4 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
5 bdayfinlem 
 |-  ( ( ( -us ` A ) e. No /\ 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] )
6 5 3expib 
 |-  ( ( -us ` A ) e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) )
7 4 6 syl 
 |-  ( A e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) )
8 0sno 
 |-  0s e. No
9 sleneg 
 |-  ( ( A e. No /\ 0s e. No ) -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
10 8 9 mpan2 
 |-  ( A e. No -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) )
11 negs0s 
 |-  ( -us ` 0s ) = 0s
12 11 breq1i 
 |-  ( ( -us ` 0s ) <_s ( -us ` A ) <-> 0s <_s ( -us ` A ) )
13 10 12 bitrdi 
 |-  ( A e. No -> ( A <_s 0s <-> 0s <_s ( -us ` A ) ) )
14 negsbday 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
15 14 eqcomd 
 |-  ( A e. No -> ( bday ` A ) = ( bday ` ( -us ` A ) ) )
16 15 eleq1d 
 |-  ( A e. No -> ( ( bday ` A ) e. _om <-> ( bday ` ( -us ` A ) ) e. _om ) )
17 13 16 anbi12d 
 |-  ( A e. No -> ( ( A <_s 0s /\ ( bday ` A ) e. _om ) <-> ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) ) )
18 zs12negsclb 
 |-  ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) )
19 7 17 18 3imtr4d 
 |-  ( A e. No -> ( ( A <_s 0s /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] ) )
20 19 expd 
 |-  ( A e. No -> ( A <_s 0s -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) )
21 sletric 
 |-  ( ( 0s e. No /\ A e. No ) -> ( 0s <_s A \/ A <_s 0s ) )
22 8 21 mpan 
 |-  ( A e. No -> ( 0s <_s A \/ A <_s 0s ) )
23 3 20 22 mpjaod 
 |-  ( A e. No -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) )
24 1 23 impbid2 
 |-  ( A e. No -> ( A e. ZZ_s[1/2] <-> ( bday ` A ) e. _om ) )