Theorem bdaypw2bnd

Description: Birthday bounding rule for non-negative dyadic rationals. (Contributed by Scott Fenton, 25-Feb-2026)

	Ref	Expression
Hypotheses	bdaypw2bnd.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
	bdaypw2bnd.2	⊢ ( 𝜑 → 𝑋 ∈ ℕ0s )
	bdaypw2bnd.3	⊢ ( 𝜑 → 𝑌 ∈ ℕ0s )
	bdaypw2bnd.4	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
	bdaypw2bnd.5	⊢ ( 𝜑 → 𝑌 <s ( 2s ↑s 𝑃 ) )
	bdaypw2bnd.6	⊢ ( 𝜑 → ( 𝑋 +s 𝑃 ) <s 𝑁 )
Assertion	bdaypw2bnd	⊢ ( 𝜑 → ( bday ‘ ( 𝑋 +s ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		bdaypw2bnd.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		bdaypw2bnd.2	⊢ ( 𝜑 → 𝑋 ∈ ℕ0s )
3		bdaypw2bnd.3	⊢ ( 𝜑 → 𝑌 ∈ ℕ0s )
4		bdaypw2bnd.4	⊢ ( 𝜑 → 𝑃 ∈ ℕ0s )
5		bdaypw2bnd.5	⊢ ( 𝜑 → 𝑌 <s ( 2s ↑s 𝑃 ) )
6		bdaypw2bnd.6	⊢ ( 𝜑 → ( 𝑋 +s 𝑃 ) <s 𝑁 )
7	2	n0snod	⊢ ( 𝜑 → 𝑋 ∈ No )
8	3	n0snod	⊢ ( 𝜑 → 𝑌 ∈ No )
9	8 4	pw2divscld	⊢ ( 𝜑 → ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ∈ No )
10		addsbday	⊢ ( ( 𝑋 ∈ No ∧ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ∈ No ) → ( bday ‘ ( 𝑋 +s ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) )
11	7 9 10	syl2anc	⊢ ( 𝜑 → ( bday ‘ ( 𝑋 +s ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) )
12		bdaypw2n0sbnd	⊢ ( ( 𝑌 ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s ∧ 𝑌 <s ( 2s ↑s 𝑃 ) ) → ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) )
13	3 4 5 12	syl3anc	⊢ ( 𝜑 → ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) )
14		bdayelon	⊢ ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ∈ On
15		bdayelon	⊢ ( bday ‘ 𝑃 ) ∈ On
16	15	onsuci	⊢ suc ( bday ‘ 𝑃 ) ∈ On
17		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
18		naddss2	⊢ ( ( ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ∈ On ∧ suc ( bday ‘ 𝑃 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑋 ) +no suc ( bday ‘ 𝑃 ) ) ) )
19	14 16 17 18	mp3an	⊢ ( ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ⊆ suc ( bday ‘ 𝑃 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑋 ) +no suc ( bday ‘ 𝑃 ) ) )
20	13 19	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( ( bday ‘ 𝑋 ) +no suc ( bday ‘ 𝑃 ) ) )
21		bdayn0p1	⊢ ( 𝑃 ∈ ℕ0s → ( bday ‘ ( 𝑃 +s 1s ) ) = suc ( bday ‘ 𝑃 ) )
22	4 21	syl	⊢ ( 𝜑 → ( bday ‘ ( 𝑃 +s 1s ) ) = suc ( bday ‘ 𝑃 ) )
23	22	oveq2d	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑃 +s 1s ) ) ) = ( ( bday ‘ 𝑋 ) +no suc ( bday ‘ 𝑃 ) ) )
24		n0ons	⊢ ( 𝑋 ∈ ℕ0s → 𝑋 ∈ Ons )
25	2 24	syl	⊢ ( 𝜑 → 𝑋 ∈ Ons )
26		peano2n0s	⊢ ( 𝑃 ∈ ℕ0s → ( 𝑃 +s 1s ) ∈ ℕ0s )
27	4 26	syl	⊢ ( 𝜑 → ( 𝑃 +s 1s ) ∈ ℕ0s )
28		n0ons	⊢ ( ( 𝑃 +s 1s ) ∈ ℕ0s → ( 𝑃 +s 1s ) ∈ Ons )
29	27 28	syl	⊢ ( 𝜑 → ( 𝑃 +s 1s ) ∈ Ons )
30		addsonbday	⊢ ( ( 𝑋 ∈ Ons ∧ ( 𝑃 +s 1s ) ∈ Ons ) → ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑃 +s 1s ) ) ) )
31	25 29 30	syl2anc	⊢ ( 𝜑 → ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑃 +s 1s ) ) ) )
32		n0ons	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ Ons )
33	1 32	syl	⊢ ( 𝜑 → 𝑁 ∈ Ons )
34		n0addscl	⊢ ( ( 𝑋 ∈ ℕ0s ∧ ( 𝑃 +s 1s ) ∈ ℕ0s ) → ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ ℕ0s )
35	2 27 34	syl2anc	⊢ ( 𝜑 → ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ ℕ0s )
36		n0ons	⊢ ( ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ ℕ0s → ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ Ons )
37	35 36	syl	⊢ ( 𝜑 → ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ Ons )
38		onslt	⊢ ( ( 𝑁 ∈ Ons ∧ ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ Ons ) → ( 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ↔ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ) )
39	33 37 38	syl2anc	⊢ ( 𝜑 → ( 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ↔ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ) )
40	39	notbid	⊢ ( 𝜑 → ( ¬ 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ↔ ¬ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ) )
41		n0addscl	⊢ ( ( 𝑋 ∈ ℕ0s ∧ 𝑃 ∈ ℕ0s ) → ( 𝑋 +s 𝑃 ) ∈ ℕ0s )
42	2 4 41	syl2anc	⊢ ( 𝜑 → ( 𝑋 +s 𝑃 ) ∈ ℕ0s )
43		n0sltp1le	⊢ ( ( ( 𝑋 +s 𝑃 ) ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑋 +s 𝑃 ) <s 𝑁 ↔ ( ( 𝑋 +s 𝑃 ) +s 1s ) ≤s 𝑁 ) )
44	42 1 43	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑃 ) <s 𝑁 ↔ ( ( 𝑋 +s 𝑃 ) +s 1s ) ≤s 𝑁 ) )
45	4	n0snod	⊢ ( 𝜑 → 𝑃 ∈ No )
46		1sno	⊢ 1s ∈ No
47	46	a1i	⊢ ( 𝜑 → 1s ∈ No )
48	7 45 47	addsassd	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑃 ) +s 1s ) = ( 𝑋 +s ( 𝑃 +s 1s ) ) )
49	48	breq1d	⊢ ( 𝜑 → ( ( ( 𝑋 +s 𝑃 ) +s 1s ) ≤s 𝑁 ↔ ( 𝑋 +s ( 𝑃 +s 1s ) ) ≤s 𝑁 ) )
50	35	n0snod	⊢ ( 𝜑 → ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ No )
51	1	n0snod	⊢ ( 𝜑 → 𝑁 ∈ No )
52		slenlt	⊢ ( ( ( 𝑋 +s ( 𝑃 +s 1s ) ) ∈ No ∧ 𝑁 ∈ No ) → ( ( 𝑋 +s ( 𝑃 +s 1s ) ) ≤s 𝑁 ↔ ¬ 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ) )
53	50 51 52	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 +s ( 𝑃 +s 1s ) ) ≤s 𝑁 ↔ ¬ 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ) )
54	44 49 53	3bitrd	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑃 ) <s 𝑁 ↔ ¬ 𝑁 <s ( 𝑋 +s ( 𝑃 +s 1s ) ) ) )
55		bdayelon	⊢ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ∈ On
56		bdayelon	⊢ ( bday ‘ 𝑁 ) ∈ On
57		ontri1	⊢ ( ( ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ∈ On ∧ ( bday ‘ 𝑁 ) ∈ On ) → ( ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) ↔ ¬ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ) )
58	55 56 57	mp2an	⊢ ( ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) ↔ ¬ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) )
59	58	a1i	⊢ ( 𝜑 → ( ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) ↔ ¬ ( bday ‘ 𝑁 ) ∈ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ) )
60	40 54 59	3bitr4d	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑃 ) <s 𝑁 ↔ ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) ) )
61	6 60	mpbid	⊢ ( 𝜑 → ( bday ‘ ( 𝑋 +s ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) )
62	31 61	eqsstrrd	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑃 +s 1s ) ) ) ⊆ ( bday ‘ 𝑁 ) )
63	23 62	eqsstrrd	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no suc ( bday ‘ 𝑃 ) ) ⊆ ( bday ‘ 𝑁 ) )
64	20 63	sstrd	⊢ ( 𝜑 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ 𝑁 ) )
65	11 64	sstrd	⊢ ( 𝜑 → ( bday ‘ ( 𝑋 +s ( 𝑌 /su ( 2s ↑s 𝑃 ) ) ) ) ⊆ ( bday ‘ 𝑁 ) )