Theorem zs12bdaylem2

Description: Lemma for zs12bday . Show the first half of the equality. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Hypotheses	zs12bdaylem.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.2	$$⊢\phi \to M\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.3	$$⊢\phi \to P\in {\mathbb{N}}_{\mathrm{0s}}$$
	zs12bdaylem.4	No typesetting found for |- ( ph -> ( ( 2s x.s M ) +s 1s )
Assertion	zs12bdaylem2	Could not format assertion : No typesetting found for |- ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zs12bdaylem.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
2		zs12bdaylem.2	$$⊢\phi \to M\in {\mathbb{N}}_{\mathrm{0s}}$$
3		zs12bdaylem.3	$$⊢\phi \to P\in {\mathbb{N}}_{\mathrm{0s}}$$
4		zs12bdaylem.4	Could not format ( ph -> ( ( 2s x.s M ) +s 1s ) ( ( 2s x.s M ) +s 1s )
5	1	n0snod	$$⊢\phi \to N\in \mathrm{No}$$
6		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
7	6	a1i	Could not format ( ph -> 2s e. No ) : No typesetting found for |- ( ph -> 2s e. No ) with typecode |-
8	2	n0snod	$$⊢\phi \to M\in \mathrm{No}$$
9	7 8	mulscld	Could not format ( ph -> ( 2s x.s M ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s M ) e. No ) with typecode |-
10		1sno	$$⊢1_s\in \mathrm{No}$$
11	10	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
12	9 11	addscld	Could not format ( ph -> ( ( 2s x.s M ) +s 1s ) e. No ) : No typesetting found for |- ( ph -> ( ( 2s x.s M ) +s 1s ) e. No ) with typecode |-
13	12 3	pw2divscld	Could not format ( ph -> ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No ) with typecode |-
14		addsbday	Could not format ( ( N e. No /\ ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) ) : No typesetting found for |- ( ( N e. No /\ ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) ) with typecode |-
15	5 13 14	syl2anc	Could not format ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) ) : No typesetting found for |- ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) ) with typecode |-
16		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
17		nnn0s	Could not format ( 2s e. NN_s -> 2s e. NN0_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. NN0_s ) with typecode |-
18	16 17	ax-mp	Could not format 2s e. NN0_s : No typesetting found for |- 2s e. NN0_s with typecode |-
19		n0mulscl	Could not format ( ( 2s e. NN0_s /\ M e. NN0_s ) -> ( 2s x.s M ) e. NN0_s ) : No typesetting found for |- ( ( 2s e. NN0_s /\ M e. NN0_s ) -> ( 2s x.s M ) e. NN0_s ) with typecode |-
20	18 2 19	sylancr	Could not format ( ph -> ( 2s x.s M ) e. NN0_s ) : No typesetting found for |- ( ph -> ( 2s x.s M ) e. NN0_s ) with typecode |-
21		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
22		n0addscl	Could not format ( ( ( 2s x.s M ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s M ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ( ( 2s x.s M ) e. NN0_s /\ 1s e. NN0_s ) -> ( ( 2s x.s M ) +s 1s ) e. NN0_s ) with typecode |-
23	20 21 22	sylancl	Could not format ( ph -> ( ( 2s x.s M ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( ph -> ( ( 2s x.s M ) +s 1s ) e. NN0_s ) with typecode |-
24		bdaypw2n0sbnd	Could not format ( ( ( ( 2s x.s M ) +s 1s ) e. NN0_s /\ P e. NN0_s /\ ( ( 2s x.s M ) +s 1s ) ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) : No typesetting found for |- ( ( ( ( 2s x.s M ) +s 1s ) e. NN0_s /\ P e. NN0_s /\ ( ( 2s x.s M ) +s 1s ) ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) with typecode |-
25	23 3 4 24	syl3anc	Could not format ( ph -> ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) : No typesetting found for |- ( ph -> ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) with typecode |-
26		bdayelon	Could not format ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On : No typesetting found for |- ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On with typecode |-
27		bdayelon	$$⊢\mathrm{bday}\left(P\right)\in \mathrm{On}$$
28	27	onsuci	$$⊢\mathrm{suc}\mathrm{bday}\left(P\right)\in \mathrm{On}$$
29		bdayelon	$$⊢\mathrm{bday}\left(N\right)\in \mathrm{On}$$
30		naddss2	Could not format ( ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` N ) e. On ) -> ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` N ) e. On ) -> ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) ) with typecode |-
31	26 28 29 30	mp3an	Could not format ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) : No typesetting found for |- ( ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) with typecode |-
32	25 31	sylib	Could not format ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` N ) +no suc ( bday ` P ) ) ) with typecode |-
33		n0addscl	$$⊢\left(N\in {\mathbb{N}}_{\mathrm{0s}}\wedge P\in {\mathbb{N}}_{\mathrm{0s}}\right)\to N{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}$$
34	1 3 33	syl2anc	$$⊢\phi \to N{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}$$
35		bdayn0p1	$$⊢N{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(\left(N{+}_{s}P\right){+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(N{+}_{s}P\right)$$
36	34 35	syl	$$⊢\phi \to \mathrm{bday}\left(\left(N{+}_{s}P\right){+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(N{+}_{s}P\right)$$
37		n0ons	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to N\in {On}_s$$
38	1 37	syl	$$⊢\phi \to N\in {On}_s$$
39		n0ons	$$⊢P\in {\mathbb{N}}_{\mathrm{0s}}\to P\in {On}_s$$
40	3 39	syl	$$⊢\phi \to P\in {On}_s$$
41		addsonbday	$$⊢\left(N\in {On}_s\wedge P\in {On}_s\right)\to \mathrm{bday}\left(N{+}_{s}P\right)=\mathrm{bday}\left(N\right)+\mathrm{bday}\left(P\right)$$
42	38 40 41	syl2anc	$$⊢\phi \to \mathrm{bday}\left(N{+}_{s}P\right)=\mathrm{bday}\left(N\right)+\mathrm{bday}\left(P\right)$$
43	42	suceqd	$$⊢\phi \to \mathrm{suc}\mathrm{bday}\left(N{+}_{s}P\right)=\mathrm{suc}\left(\mathrm{bday}\left(N\right)+\mathrm{bday}\left(P\right)\right)$$
44		naddsuc2	$$⊢\left(\mathrm{bday}\left(N\right)\in \mathrm{On}\wedge \mathrm{bday}\left(P\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(N\right)+\mathrm{suc}\mathrm{bday}\left(P\right)=\mathrm{suc}\left(\mathrm{bday}\left(N\right)+\mathrm{bday}\left(P\right)\right)$$
45	29 27 44	mp2an	$$⊢\mathrm{bday}\left(N\right)+\mathrm{suc}\mathrm{bday}\left(P\right)=\mathrm{suc}\left(\mathrm{bday}\left(N\right)+\mathrm{bday}\left(P\right)\right)$$
46	43 45	eqtr4di	$$⊢\phi \to \mathrm{suc}\mathrm{bday}\left(N{+}_{s}P\right)=\mathrm{bday}\left(N\right)+\mathrm{suc}\mathrm{bday}\left(P\right)$$
47	36 46	eqtrd	$$⊢\phi \to \mathrm{bday}\left(\left(N{+}_{s}P\right){+}_s{1}_s\right)=\mathrm{bday}\left(N\right)+\mathrm{suc}\mathrm{bday}\left(P\right)$$
48	32 47	sseqtrrd	Could not format ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` N ) +no ( bday ` ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) ) with typecode |-
49	15 48	sstrd	Could not format ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) ) : No typesetting found for |- ( ph -> ( bday ` ( N +s ( ( ( 2s x.s M ) +s 1s ) /su ( 2s ^su P ) ) ) ) C_ ( bday ` ( ( N +s P ) +s 1s ) ) ) with typecode |-