Theorem bdayfinlem

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

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

Proof

Step	Hyp	Ref	Expression
1		bdayn0sf1o	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
2		f1ocnvdm	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to {\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
3	1 2	mpan	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{\omega }\to {\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
4	3	3ad2ant3	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to {\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
5	4	n0zsd	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to {\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\in {\mathbb{Z}}_s$$
6		zzs12	Could not format ( ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) with typecode |-
7	5 6	syl	Could not format ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) with typecode |-
8		eleq1	Could not format ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> ( A e. ZZ_s[1/2] <-> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> ( A e. ZZ_s[1/2] <-> ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) e. ZZ_s[1/2] ) ) with typecode |-
9	7 8	syl5ibrcom	Could not format ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) -> A e. ZZ_s[1/2] ) ) with typecode |-
10		n0zs	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in {\mathbb{Z}}_s$$
11		zzs12	Could not format ( x e. ZZ_s -> x e. ZZ_s[1/2] ) : No typesetting found for |- ( x e. ZZ_s -> x e. ZZ_s[1/2] ) with typecode |-
12	10 11	syl	Could not format ( x e. NN0_s -> x e. ZZ_s[1/2] ) : No typesetting found for |- ( x e. NN0_s -> x e. ZZ_s[1/2] ) with typecode |-
13	12	adantr	Could not format ( ( x e. NN0_s /\ y e. NN0_s ) -> x e. ZZ_s[1/2] ) : No typesetting found for |- ( ( x e. NN0_s /\ y e. NN0_s ) -> x e. ZZ_s[1/2] ) with typecode |-
14		n0zs	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y\in {\mathbb{Z}}_s$$
15		elzs12i	Could not format ( ( y e. ZZ_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( y e. ZZ_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) with typecode |-
16	14 15	sylan	Could not format ( ( y e. NN0_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( y e. NN0_s /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) with typecode |-
17	16	adantll	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) with typecode |-
18		zs12addscl	Could not format ( ( x e. ZZ_s[1/2] /\ ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( x e. ZZ_s[1/2] /\ ( y /su ( 2s ^su z ) ) e. ZZ_s[1/2] ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) with typecode |-
19	13 17 18	syl2an2r	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) with typecode |-
20		eleq1	Could not format ( A = ( x +s ( y /su ( 2s ^su z ) ) ) -> ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( A = ( x +s ( y /su ( 2s ^su z ) ) ) -> ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) ) with typecode |-
21	20	3ad2ant1	Could not format ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y ( A e. ZZ_s[1/2] <-> ( x +s ( y /su ( 2s ^su z ) ) ) e. ZZ_s[1/2] ) ) with typecode |-
22	19 21	syl5ibrcom	Could not format ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( ( x e. NN0_s /\ y e. NN0_s ) /\ z e. NN0_s ) -> ( ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) with typecode |-
23	22	rexlimdva	Could not format ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( x e. NN0_s /\ y e. NN0_s ) -> ( E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) with typecode |-
24	23	rexlimivv	Could not format ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) : No typesetting found for |- ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) with typecode |-
25	24	a1i	Could not format ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) : No typesetting found for |- ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y A e. ZZ_s[1/2] ) ) with typecode |-
26		simp1	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to A\in \mathrm{No}$$
27	4	fvresd	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)=\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)$$
28		f1ocnvfv2	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)=\mathrm{bday}\left(A\right)$$
29	1 28	mpan	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{\omega }\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)=\mathrm{bday}\left(A\right)$$
30	29	3ad2ant3	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)=\mathrm{bday}\left(A\right)$$
31	27 30	eqtr3d	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)=\mathrm{bday}\left(A\right)$$
32	31	eqimsscd	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to \mathrm{bday}\left(A\right)\subseteq \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)}^{-1}\left(\mathrm{bday}\left(A\right)\right)\right)$$
33		simp2	$$⊢\left(A\in \mathrm{No}\wedge 0_s{\le }_{s}A\wedge \mathrm{bday}\left(A\right)\in \mathrm{\omega }\right)\to 0_s{\le }_{s}A$$
34	4 26 32 33	bdayfinbnd	Could not format ( ( A e. No /\ 0s <_s A /\ ( bday ` A ) e. _om ) -> ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) \/ E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y ( A = ( `' ( bday |` NN0_s ) ` ( bday ` A ) ) \/ E. x e. NN0_s E. y e. NN0_s E. z e. NN0_s ( A = ( x +s ( y /su ( 2s ^su z ) ) ) /\ y
35	9 25 34	mpjaod	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 |-