Theorem zs12bdaylem

Description: Lemma for zs12bday . Handle the non-negative case. (Contributed by Scott Fenton, 22-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	Could not format ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> A e. ZZ_s[1/2] ) : No typesetting found for |- ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> A e. ZZ_s[1/2] ) with typecode |-
2		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 |-
3		zs12ge0	Could not format ( ( A e. No /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
4	2 3	sylan	Could not format ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( A e. ZZ_s[1/2] <-> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
5	1 4	mpbid	Could not format ( ( A e. ZZ_s[1/2] /\ 0s <_s A ) -> E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y
6		simpl1	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y x e. NN0_s ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y x e. NN0_s ) with typecode |-
7	6	n0snod	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y x e. No ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y x e. No ) with typecode |-
8		simpl2	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y y e. NN0_s ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y y e. NN0_s ) with typecode |-
9	8	n0snod	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y y e. No ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y y e. No ) with typecode |-
10		simpl3	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y p e. NN0_s ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y p e. NN0_s ) with typecode |-
11	9 10	pw2divscld	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( y /su ( 2s ^su p ) ) e. No ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( y /su ( 2s ^su p ) ) e. No ) with typecode |-
12		addsbday	Could not format ( ( x e. No /\ ( y /su ( 2s ^su p ) ) e. No ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( ( x e. No /\ ( y /su ( 2s ^su p ) ) e. No ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
13	7 11 12	syl2anc	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
14		n0sbday	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(x\right)\in \mathrm{\omega }$$
15	6 14	syl	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` x ) e. _om ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` x ) e. _om ) with typecode |-
16		simpr	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y y y
17		bdaypw2n0sbnd	Could not format ( ( y e. NN0_s /\ p e. NN0_s /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) ) : No typesetting found for |- ( ( y e. NN0_s /\ p e. NN0_s /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) ) with typecode |-
18	8 10 16 17	syl3anc	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) ) with typecode |-
19		n0sbday	$$⊢p\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(p\right)\in \mathrm{\omega }$$
20		peano2	$$⊢\mathrm{bday}\left(p\right)\in \mathrm{\omega }\to \mathrm{suc}\mathrm{bday}\left(p\right)\in \mathrm{\omega }$$
21	19 20	syl	$$⊢p\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{suc}\mathrm{bday}\left(p\right)\in \mathrm{\omega }$$
22	21	3ad2ant3	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\wedge p\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \mathrm{suc}\mathrm{bday}\left(p\right)\in \mathrm{\omega }$$
23	22	adantr	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y suc ( bday ` p ) e. _om ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y suc ( bday ` p ) e. _om ) with typecode |-
24		bdayelon	Could not format ( bday ` ( y /su ( 2s ^su p ) ) ) e. On : No typesetting found for |- ( bday ` ( y /su ( 2s ^su p ) ) ) e. On with typecode |-
25	24	onordi	Could not format Ord ( bday ` ( y /su ( 2s ^su p ) ) ) : No typesetting found for |- Ord ( bday ` ( y /su ( 2s ^su p ) ) ) with typecode |-
26		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
27		ordtr2	Could not format ( ( Ord ( bday ` ( y /su ( 2s ^su p ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) ) : No typesetting found for |- ( ( Ord ( bday ` ( y /su ( 2s ^su p ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) ) with typecode |-
28	25 26 27	mp2an	Could not format ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) : No typesetting found for |- ( ( ( bday ` ( y /su ( 2s ^su p ) ) ) C_ suc ( bday ` p ) /\ suc ( bday ` p ) e. _om ) -> ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) with typecode |-
29	18 23 28	syl2anc	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) with typecode |-
30		omnaddcl	Could not format ( ( ( bday ` x ) e. _om /\ ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) -> ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( bday ` x ) e. _om /\ ( bday ` ( y /su ( 2s ^su p ) ) ) e. _om ) -> ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) with typecode |-
31	15 29 30	syl2anc	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) with typecode |-
32		bdayelon	Could not format ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. On : No typesetting found for |- ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. On with typecode |-
33	32	onordi	Could not format Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) : No typesetting found for |- Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) with typecode |-
34		ordtr2	Could not format ( ( Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( Ord ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) /\ Ord _om ) -> ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) ) with typecode |-
35	33 26 34	mp2an	Could not format ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) C_ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) /\ ( ( bday ` x ) +no ( bday ` ( y /su ( 2s ^su p ) ) ) ) e. _om ) -> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) with typecode |-
36	13 31 35	syl2anc	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) with typecode |-
37		fveq2	Could not format ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) = ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) ) : No typesetting found for |- ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) = ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) ) with typecode |-
38	37	eleq1d	Could not format ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) ) : No typesetting found for |- ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x +s ( y /su ( 2s ^su p ) ) ) ) e. _om ) ) with typecode |-
39	36 38	syl5ibrcom	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) /\ y ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) ) with typecode |-
40	39	ex	Could not format ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( y ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( y ( A = ( x +s ( y /su ( 2s ^su p ) ) ) -> ( bday ` A ) e. _om ) ) ) with typecode |-
41	40	impcomd	Could not format ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) : No typesetting found for |- ( ( x e. NN0_s /\ y e. NN0_s /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) with typecode |-
42	41	3expa	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ p e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) with typecode |-
43	42	rexlimdva	Could not format ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) : No typesetting found for |- ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) ) with typecode |-
44	43	rexlimivv	Could not format ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) : No typesetting found for |- ( E. x e. NN0_s E. y e. NN0_s E. p e. NN0_s ( A = ( x +s ( y /su ( 2s ^su p ) ) ) /\ y ( bday ` A ) e. _om ) with typecode |-
45	5 44	syl	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 |-