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	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
	zs12bdaylem.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ0s )
	zs12bdaylem.3	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
	zs12bdaylem.4	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) )
Assertion	zs12bdaylem2	⊢ ( 𝜑 → ( bday ‘ ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		zs12bdaylem.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		zs12bdaylem.2	⊢ ( 𝜑 → 𝑀 ∈ ℕ0s )
3		zs12bdaylem.3	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
4		zs12bdaylem.4	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) )
5	1	n0snod	⊢ ( 𝜑 → 𝑁 ∈ No )
6		2sno	⊢ 2s ∈ No
7	6	a1i	⊢ ( 𝜑 → 2s ∈ No )
8	2	n0snod	⊢ ( 𝜑 → 𝑀 ∈ No )
9	7 8	mulscld	⊢ ( 𝜑 → ( 2s ·s 𝑀 ) ∈ No )
10		1sno	⊢ 1s ∈ No
11	10	a1i	⊢ ( 𝜑 → 1s ∈ No )
12	9 11	addscld	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) ∈ No )
13	12 3	pw2divscld	⊢ ( 𝜑 → ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ∈ No )
14		addsbday	⊢ ( ( 𝑁 ∈ No ∧ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ∈ No ) → ( bday ‘ ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) )
15	5 13 14	syl2anc	⊢ ( 𝜑 → ( bday ‘ ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) )
16		2nns	⊢ 2s ∈ ℕs
17		nnn0s	⊢ ( 2s ∈ ℕs → 2s ∈ ℕ0s )
18	16 17	ax-mp	⊢ 2s ∈ ℕ0s
19		n0mulscl	⊢ ( ( 2s ∈ ℕ0s ∧ 𝑀 ∈ ℕ0s ) → ( 2s ·s 𝑀 ) ∈ ℕ0s )
20	18 2 19	sylancr	⊢ ( 𝜑 → ( 2s ·s 𝑀 ) ∈ ℕ0s )
21		1n0s	⊢ 1s ∈ ℕ0s
22		n0addscl	⊢ ( ( ( 2s ·s 𝑀 ) ∈ ℕ0s ∧ 1s ∈ ℕ0s ) → ( ( 2s ·s 𝑀 ) +s 1s ) ∈ ℕ0s )
23	20 21 22	sylancl	⊢ ( 𝜑 → ( ( 2s ·s 𝑀 ) +s 1s ) ∈ ℕ0s )
24		bdaypw2n0sbnd	⊢ ( ( ( ( 2s ·s 𝑀 ) +s 1s ) ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s ∧ ( ( 2s ·s 𝑀 ) +s 1s ) <s ( 2s ↑s 𝑃 ) ) → ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) )
25	23 3 4 24	syl3anc	⊢ ( 𝜑 → ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) )
26		bdayelon	⊢ ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ∈ On
27		bdayelon	⊢ ( bday ‘ 𝑃 ) ∈ On
28	27	onsuci	⊢ suc ( bday ‘ 𝑃 ) ∈ On
29		bdayelon	⊢ ( bday ‘ 𝑁 ) ∈ On
30		naddss2	⊢ ( ( ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ∈ On ∧ suc ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝑁 ) ∈ On ) → ( ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) ↔ ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) ) )
31	26 28 29 30	mp3an	⊢ ( ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) ↔ ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) )
32	25 31	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) )
33		n0addscl	⊢ ( ( 𝑁 ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s ) → ( 𝑁 +s 𝑃 ) ∈ ℕ0s )
34	1 3 33	syl2anc	⊢ ( 𝜑 → ( 𝑁 +s 𝑃 ) ∈ ℕ0s )
35		bdayn0p1	⊢ ( ( 𝑁 +s 𝑃 ) ∈ ℕ0s → ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) = suc ( bday ‘ ( 𝑁 +s 𝑃 ) ) )
36	34 35	syl	⊢ ( 𝜑 → ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) = suc ( bday ‘ ( 𝑁 +s 𝑃 ) ) )
37		n0ons	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ Ons )
38	1 37	syl	⊢ ( 𝜑 → 𝑁 ∈ Ons )
39		n0ons	⊢ ( 𝑃 ∈ ℕ0s → 𝑃 ∈ Ons )
40	3 39	syl	⊢ ( 𝜑 → 𝑃 ∈ Ons )
41		addsonbday	⊢ ( ( 𝑁 ∈ Ons ∧ 𝑃 ∈ Ons ) → ( bday ‘ ( 𝑁 +s 𝑃 ) ) = ( ( bday ‘ 𝑁 ) +no ( bday ‘ 𝑃 ) ) )
42	38 40 41	syl2anc	⊢ ( 𝜑 → ( bday ‘ ( 𝑁 +s 𝑃 ) ) = ( ( bday ‘ 𝑁 ) +no ( bday ‘ 𝑃 ) ) )
43	42	suceqd	⊢ ( 𝜑 → suc ( bday ‘ ( 𝑁 +s 𝑃 ) ) = suc ( ( bday ‘ 𝑁 ) +no ( bday ‘ 𝑃 ) ) )
44		naddsuc2	⊢ ( ( ( bday ‘ 𝑁 ) ∈ On ∧ ( bday ‘ 𝑃 ) ∈ On ) → ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) = suc ( ( bday ‘ 𝑁 ) +no ( bday ‘ 𝑃 ) ) )
45	29 27 44	mp2an	⊢ ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) = suc ( ( bday ‘ 𝑁 ) +no ( bday ‘ 𝑃 ) )
46	43 45	eqtr4di	⊢ ( 𝜑 → suc ( bday ‘ ( 𝑁 +s 𝑃 ) ) = ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) )
47	36 46	eqtrd	⊢ ( 𝜑 → ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) = ( ( bday ‘ 𝑁 ) +no suc ( bday ‘ 𝑃 ) ) )
48	32 47	sseqtrrd	⊢ ( 𝜑 → ( ( bday ‘ 𝑁 ) +no ( bday ‘ ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) )
49	15 48	sstrd	⊢ ( 𝜑 → ( bday ‘ ( 𝑁 +s ( ( ( 2s ·s 𝑀 ) +s 1s ) /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ ( ( 𝑁 +s 𝑃 ) +s 1s ) ) )