Theorem z12bdaylem2 28887

Description: Lemma for z12bday 28901. 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 28741	. . 3 ⊢ (𝜑 → 𝑁 ∈ No)
3		2no 28835	. . . . . . 7 ⊢ 2s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (𝜑 → 2s ∈ No)
5		z12bdaylem.2	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0s)
6	5	n0nod 28741	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ No)
7	4, 6	mulscld 28551	. . . . 5 ⊢ (𝜑 → (2s ·s 𝑀) ∈ No)
8		1no 28226	. . . . . 6 ⊢ 1s ∈ No
9	8	a1i 11	. . . . 5 ⊢ (𝜑 → 1s ∈ No)
10	7, 9	addscld 28396	. . . 4 ⊢ (𝜑 → ((2s ·s 𝑀) +s 1s ) ∈ No)
11		z12bdaylem.3	. . . 4 ⊢ (𝜑 → 𝑃 ∈ ℕ0s)
12	10, 11	pw2divscld 28855	. . 3 ⊢ (𝜑 → (((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)) ∈ No)
13		addbday 28434	. . 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 28834	. . . . . . . 8 ⊢ 2s ∈ ℕs
16		nnn0s 28743	. . . . . . . 8 ⊢ (2s ∈ ℕs → 2s ∈ ℕ0s)
17	15, 16	ax-mp 5	. . . . . . 7 ⊢ 2s ∈ ℕ0s
18		n0mulscl 28761	. . . . . . 7 ⊢ ((2s ∈ ℕ0s ∧ 𝑀 ∈ ℕ0s) → (2s ·s 𝑀) ∈ ℕ0s)
19	17, 5, 18	sylancr 599	. . . . . 6 ⊢ (𝜑 → (2s ·s 𝑀) ∈ ℕ0s)
20		1n0s 28764	. . . . . 6 ⊢ 1s ∈ ℕ0s
21		n0addscl 28760	. . . . . 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 28880	. . . . 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 1399	. . . 4 ⊢ (𝜑 → (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ⊆ suc (bday‘𝑃))
26		bdayon 28168	. . . . 5 ⊢ (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃))) ∈ On
27		bdayon 28168	. . . . . 6 ⊢ (bday‘𝑃) ∈ On
28	27	onsuci 7874	. . . . 5 ⊢ suc (bday‘𝑃) ∈ On
29		bdayon 28168	. . . . 5 ⊢ (bday‘𝑁) ∈ On
30		naddss2 8728	. . . . 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 1491	. . . 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 28760	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s) → (𝑁 +s 𝑃) ∈ ℕ0s)
34	1, 11, 33	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑁 +s 𝑃) ∈ ℕ0s)
35		bdayn0p1 28785	. . . . 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 28752	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0s → 𝑁 ∈ Ons)
38	1, 37	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ Ons)
39		n0on 28752	. . . . . . . 8 ⊢ (𝑃 ∈ ℕ0s → 𝑃 ∈ Ons)
40	11, 39	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ Ons)
41		addonbday 28695	. . . . . . 7 ⊢ ((𝑁 ∈ Ons ∧ 𝑃 ∈ Ons) → (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no (bday‘𝑃)))
42	38, 40, 41	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no (bday‘𝑃)))
43	42	suceqd 6448	. . . . 5 ⊢ (𝜑 → suc (bday‘(𝑁 +s 𝑃)) = suc ((bday‘𝑁) +no (bday‘𝑃)))
44		naddsuc2 8739	. . . . . 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 2816	. . . 4 ⊢ (𝜑 → suc (bday‘(𝑁 +s 𝑃)) = ((bday‘𝑁) +no suc (bday‘𝑃)))
47	36, 46	eqtrd 2798	. . 3 ⊢ (𝜑 → (bday‘((𝑁 +s 𝑃) +s 1s )) = ((bday‘𝑁) +no suc (bday‘𝑃)))
48	32, 47	sseqtrrd 3950	. 2 ⊢ (𝜑 → ((bday‘𝑁) +no (bday‘(((2s ·s 𝑀) +s 1s ) /su (2s↑s𝑃)))) ⊆ (bday‘((𝑁 +s 𝑃) +s 1s )))
49	14, 48	sstrd 3923	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 1570   ∈ wcel 2147   ⊆ wss 3900   class class class wbr 5106  Oncon0 6380  suc csuc 6382  ‘cfv 6558  (class class class)co 7443   +no cnadd 8702  Nocsur 28027   <s clts 28028  bdaycbday 28029   1_s c1s 28222   +_s cadds 28375   ·_s cmuls 28522   /_su cdivs 28603  On_scons 28667  ℕ_0scn0s 28728  ℕ_scnns 28729  2_sc2s 28826  ↑_scexps 28828

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-dc 10551

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-ot 4862  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-1st 8025  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-oadd 8508  df-nadd 8703  df-no 28030  df-lts 28031  df-bday 28032  df-les 28132  df-slts 28174  df-cuts 28176  df-0s 28223  df-1s 28224  df-made 28243  df-old 28244  df-left 28246  df-right 28247  df-norec 28354  df-norec2 28365  df-adds 28376  df-negs 28437  df-subs 28438  df-muls 28523  df-divs 28604  df-ons 28668  df-seqs 28700  df-n0s 28730  df-nns 28731  df-zs 28795  df-2s 28827  df-exps 28829

This theorem is used by: (None)