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	Could not format assertion : No typesetting found for |- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( bday ` A ) e. _om ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		z12bday	Could not format ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) with typecode |-
2		bdayfinlem	Could not format ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] ) : No typesetting found for |- ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] ) with typecode |-
3	2	3exp	Could not format ( A e. No -> ( 0s <_s A -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) ) : No typesetting found for |- ( A e. No -> ( 0s <_s A -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) ) with typecode |-
4		negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$
5		bdayfinlem	Could not format ( ( ( -us ` A ) e. No /\ 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( ( -us ` A ) e. No /\ 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) with typecode |-
6	5	3expib	Could not format ( ( -us ` A ) e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( -us ` A ) e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) ) with typecode |-
7	4 6	syl	Could not format ( A e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( ( 0s <_s ( -us ` A ) /\ ( bday ` ( -us ` A ) ) e. _om ) -> ( -us ` A ) e. ZZ_s[1/2] ) ) with typecode |-
8		0no	$$⊢0_s\in \mathrm{No}$$
9		lenegs	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left(A{\le }_s{0}_s\leftrightarrow {+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\right)$$
10	8 9	mpan2	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\leftrightarrow {+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\right)$$
11		neg0s	$$⊢{+}_s\left(0_s\right)=0_s$$
12	11	breq1i	$$⊢{+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\leftrightarrow 0_s{\le }_s{+}_s\left(A\right)$$
13	10 12	bitrdi	$$⊢A\in \mathrm{No}\to \left(A{\le }_s{0}_s\leftrightarrow 0_s{\le }_s{+}_s\left(A\right)\right)$$
14		negbday	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$
15	14	eqcomd	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{bday}\left({+}_s\left(A\right)\right)$$
16	15	eleq1d	$$⊢A\in \mathrm{No}\to \left(\mathrm{bday}\left(A\right)\in \mathrm{\omega }\leftrightarrow \mathrm{bday}\left({+}_s\left(A\right)\right)\in \mathrm{\omega }\right)$$
17	13 16	anbi12d	$$⊢A\in \mathrm{No}\to \left(\left(A{\le }_s{0}_s\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\leftrightarrow \left(0_s{\le }_s{+}_s\left(A\right)\wedge \mathrm{bday}\left({+}_s\left(A\right)\right)\in \mathrm{\omega }\right)\right)$$
18		z12negsclb	Could not format ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( -us ` A ) e. ZZ_s[1/2] ) ) with typecode |-
19	7 17 18	3imtr4d	Could not format ( A e. No -> ( ( A <_s 0s /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( ( A <_s 0s /\ ( bday ` A ) e. _om ) -> A e. ZZ_s[1/2] ) ) with typecode |-
20	19	expd	Could not format ( A e. No -> ( A <_s 0s -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) ) : No typesetting found for |- ( A e. No -> ( A <_s 0s -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) ) with typecode |-
21		lestric	$$⊢\left(0_s\in \mathrm{No}\wedge A\in \mathrm{No}\right)\to \left(0_s{\le }_{s}A\vee A{\le }_s{0}_s\right)$$
22	8 21	mpan	$$⊢A\in \mathrm{No}\to \left(0_s{\le }_{s}A\vee A{\le }_s{0}_s\right)$$
23	3 20 22	mpjaod	Could not format ( A e. No -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A e. No -> ( ( bday ` A ) e. _om -> A e. ZZ_s[1/2] ) ) with typecode |-
24	1 23	impbid2	Could not format ( A e. No -> ( A e. ZZ_s[1/2] <-> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( A e. No -> ( A e. ZZ_s[1/2] <-> ( bday ` A ) e. _om ) ) with typecode |-