Theorem z12bdaylem2 28862

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

Hypotheses

Ref	Expression
z12bdaylem.1	⊢ (𝜑 → 𝑁 ∈ ℕ0s)
z12bdaylem.2	⊢ (𝜑 → 𝑀 ∈ ℕ0s)
z12bdaylem.3	⊢ (𝜑 → 𝑃 ∈ ℕ0s)
z12bdaylem.4	⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) <s (2s↑s𝑃))

Assertion

Ref	Expression
z12bdaylem2	⊢ (𝜑 → (bday‘(𝑁 +s (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ (bday‘((𝑁 +s 𝑃) +s 1s )))

Proof of Theorem z12bdaylem2

Step	Hyp	Ref	Expression
1		z12bdaylem.1	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ0s)
2	1	n0nod 28716	. . 3 ⊢ (𝜑 → 𝑁 ∈ No)
3		2no 28810	. . . . . . 7 ⊢ 2s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 2s ∈ No)
5		z12bdaylem.2	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0s)
6	5	n0nod 28716	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ No)
7	4, 6	mulscld 28526	. . . . 5 ⊢ (𝜑 → (2s ·s 𝑀) ∈ No)
8		1no 28201	. . . . . 6 ⊢ 1s ∈ No
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → 1s ∈ No)
10	7, 9	addscld 28371	. . . 4 ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) ∈ No)
11		z12bdaylem.3	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ0s)
12	10, 11	pw2divscld 28830	. . 3 ⊢ (𝜑 → (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)) ∈ No)
13		addbday 28409	. . 3 ⊢ ((𝑁 ∈ 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𝑃)))))
14	2, 12, 13	syl2anc 596	. 2 ⊢ (𝜑 → (bday‘(𝑁 +s (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ ((bday‘𝑁) +no (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))))
15		2nns 28809	. . . . . . . 8 ⊢ 2s ∈ ℕs
16		nnn0s 28718	. . . . . . . 8 ⊢ (2s ∈ ℕs → 2s ∈ ℕ0s)
17	15, 16	ax-mp 5	. . . . . . 7 ⊢ 2s ∈ ℕ0s
18		n0mulscl 28736	. . . . . . 7 ⊢ ((2s ∈ ℕ0s ∧ 𝑀 ∈ ℕ0s) → (2s ·s 𝑀) ∈ ℕ0s)
19	17, 5, 18	sylancr 599	. . . . . 6 ⊢ (𝜑 → (2s ·s 𝑀) ∈ ℕ0s)
20		1n0s 28739	. . . . . 6 ⊢ 1s ∈ ℕ0s
21		n0addscl 28735	. . . . . 6 ⊢ (((2s ·s 𝑀) ∈ ℕ0s ∧ 1s ∈ ℕ0s) → ((2s ·s 𝑀) +s 1s ) ∈ ℕ0s)
22	19, 20, 21	sylancl 598	. . . . 5 ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) ∈ ℕ0s)
23		z12bdaylem.4	. . . . 5 ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) <s (2s↑s𝑃))
24		bdaypw2n0bnd 28855	. . . . 5 ⊢ ((((2s ·s 𝑀) +s 1s ) ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s ∧ ((2s ·s 𝑀) +s 1s ) <s (2s↑s𝑃)) → (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ⊆ suc (bday‘𝑃))
25	22, 11, 23, 24	syl3anc 1398	. . . 4 ⊢ (𝜑 → (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ⊆ suc (bday‘𝑃))
26		bdayon 28143	. . . . 5 ⊢ (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ∈ On
27		bdayon 28143	. . . . . 6 ⊢ (bday‘𝑃) ∈ On
28	27	onsuci 7850	. . . . 5 ⊢ suc (bday‘𝑃) ∈ On
29		bdayon 28143	. . . . 5 ⊢ (bday‘𝑁) ∈ On
30		naddss2 8703	. . . . 5 ⊢ (((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 1490	. . . 4 ⊢ ((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 221	. . 3 ⊢ (𝜑 → ((bday‘𝑁) +no (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ ((bday‘𝑁) +no suc (bday‘𝑃)))
33		n0addscl 28735	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s) → (𝑁 +s 𝑃) ∈ ℕ0s)
34	1, 11, 33	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑁 +s 𝑃) ∈ ℕ0s)
35		bdayn0p1 28760	. . . . 5 ⊢ ((𝑁 +s 𝑃) ∈ ℕ0s → (bday‘((𝑁 +s 𝑃) +s 1s )) = suc (bday‘(𝑁 +s 𝑃)))
36	34, 35	syl 18	. . . 4 ⊢ (𝜑 → (bday‘((𝑁 +s 𝑃) +s 1s )) = suc (bday‘(𝑁 +s 𝑃)))
37		n0on 28727	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0s → 𝑁 ∈ Ons)
38	1, 37	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ Ons)
39		n0on 28727	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ0s → 𝑃 ∈ Ons)
40	11, 39	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ Ons)
41		addonbday 28670	. . . . . . 7 ⊢ ((𝑁 ∈ Ons ∧ 𝑃 ∈ Ons) → (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no (bday‘𝑃)))
42	38, 40, 41	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no (bday‘𝑃)))
43	42	suceqd 6430	. . . . 5 ⊢ (𝜑 → suc (bday‘(𝑁 +s 𝑃)) = suc ((bday‘𝑁) +no (bday‘𝑃)))
44		naddsuc2 8714	. . . . . 6 ⊢ (((bday‘𝑁) ∈ On ∧ (bday‘𝑃) ∈ On) → ((bday‘𝑁) +no suc (bday‘𝑃)) = suc ((bday‘𝑁) +no (bday‘𝑃)))
45	29, 27, 44	mp2an 705	. . . . 5 ⊢ ((bday‘𝑁) +no suc (bday‘𝑃)) = suc ((bday‘𝑁) +no (bday‘𝑃))
46	43, 45	eqtr4di 2813	. . . 4 ⊢ (𝜑 → suc (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no suc (bday‘𝑃)))
47	36, 46	eqtrd 2795	. . 3 ⊢ (𝜑 → (bday‘((𝑁 +s 𝑃) +s 1s )) = ((bday‘𝑁) +no suc (bday‘𝑃)))
48	32, 47	sseqtrrd 3945	. 2 ⊢ (𝜑 → ((bday‘𝑁) +no (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ (bday‘((𝑁 +s 𝑃) +s 1s )))
49	14, 48	sstrd 3918	1 ⊢ (𝜑 → (bday‘(𝑁 +s (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ (bday‘((𝑁 +s 𝑃) +s 1s )))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895   class class class wbr 5102  Oncon0 6362  suc csuc 6364  ‘cfv 6538  (class class class)co 7420   +no cnadd 8677  Nocsur 28002   <s clts 28003  bdaycbday 28004   1_s c1s 28197   +_s cadds 28350   ·_s cmuls 28497   /_su cdivs 28578  On_scons 28642  ℕ_0scn0s 28703  ℕ_scnns 28704  2_sc2s 28801  ↑_scexps 28803

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-dc 10527

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-ot 4858  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-2o 8480  df-oadd 8483  df-nadd 8678  df-no 28005  df-lts 28006  df-bday 28007  df-les 28107  df-slts 28149  df-cuts 28151  df-0s 28198  df-1s 28199  df-made 28218  df-old 28219  df-left 28221  df-right 28222  df-norec 28329  df-norec2 28340  df-adds 28351  df-negs 28412  df-subs 28413  df-muls 28498  df-divs 28579  df-ons 28643  df-seqs 28675  df-n0s 28705  df-nns 28706  df-zs 28770  df-2s 28802  df-exps 28804

This theorem is used by: (None)