Theorem zs12bday

Description: A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025) (Proof shortened by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Assertion	zs12bday	Could not format assertion : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zs12bdaylem	Could not format ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( bday ` A ) e. _om ) : No typesetting found for |- ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( bday ` A ) e. _om ) with typecode |-
2		0sno	$$⊢0_s\in \mathrm{No}$$
3		zs12no	Could not format ( A e. ZZ_s[1/2] -> A e. No ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> A e. No ) with typecode |-
4		sletric	$$⊢\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)$$
5	2 3 4	sylancr	Could not format ( A e. ZZ_s[1/2] -> ( 0s <_s A \/ A <_s 0s ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( 0s <_s A \/ A <_s 0s ) ) with typecode |-
6	5	ord	Could not format ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> A <_s 0s ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> A <_s 0s ) ) with typecode |-
7		sleneg	$$⊢\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)$$
8	3 2 7	sylancl	Could not format ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> ( -us ` 0s ) <_s ( -us ` A ) ) ) with typecode |-
9		negs0s	$$⊢{+}_s\left(0_s\right)=0_s$$
10	9	breq1i	$$⊢{+}_s\left(0_s\right){\le }_s{+}_s\left(A\right)\leftrightarrow 0_s{\le }_s{+}_s\left(A\right)$$
11	8 10	bitrdi	Could not format ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> 0s <_s ( -us ` A ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A <_s 0s <-> 0s <_s ( -us ` A ) ) ) with typecode |-
12		zs12negscl	Could not format ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( -us ` A ) e. ZZ_s[1/2] ) with typecode |-
13		zs12bdaylem	Could not format ( ( ( -us ` A ) e. ZZ_s[1/2] /\ 0s <_s ( -us ` A ) ) -> ( bday ` ( -us ` A ) ) e. _om ) : No typesetting found for |- ( ( ( -us ` A ) e. ZZ_s[1/2] /\ 0s <_s ( -us ` A ) ) -> ( bday ` ( -us ` A ) ) e. _om ) with typecode |-
14	13	ex	Could not format ( ( -us ` A ) e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) ) : No typesetting found for |- ( ( -us ` A ) e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) ) with typecode |-
15	12 14	syl	Could not format ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` ( -us ` A ) ) e. _om ) ) with typecode |-
16		negsbday	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$
17	3 16	syl	Could not format ( A e. ZZ_s[1/2] -> ( bday ` ( -us ` A ) ) = ( bday ` A ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( bday ` ( -us ` A ) ) = ( bday ` A ) ) with typecode |-
18	17	eleq1d	Could not format ( A e. ZZ_s[1/2] -> ( ( bday ` ( -us ` A ) ) e. _om <-> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( ( bday ` ( -us ` A ) ) e. _om <-> ( bday ` A ) e. _om ) ) with typecode |-
19	15 18	sylibd	Could not format ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( 0s <_s ( -us ` A ) -> ( bday ` A ) e. _om ) ) with typecode |-
20	11 19	sylbid	Could not format ( A e. ZZ_s[1/2] -> ( A <_s 0s -> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( A <_s 0s -> ( bday ` A ) e. _om ) ) with typecode |-
21	6 20	syld	Could not format ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( -. 0s <_s A -> ( bday ` A ) e. _om ) ) with typecode |-
22	21	imp	Could not format ( ( A e. ZZ_s[1/2] /\ -. 0s <_s A ) -> ( bday ` A ) e. _om ) : No typesetting found for |- ( ( A e. ZZ_s[1/2] /\ -. 0s <_s A ) -> ( bday ` A ) e. _om ) with typecode |-
23	1 22	pm2.61dan	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 |-