Theorem bdaypw2bnd

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

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

Proof

Step	Hyp	Ref	Expression
1		bdaypw2bnd.1	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
2		bdaypw2bnd.2	$$⊢\phi \to X\in {\mathbb{N}}_{\mathrm{0s}}$$
3		bdaypw2bnd.3	$$⊢\phi \to Y\in {\mathbb{N}}_{\mathrm{0s}}$$
4		bdaypw2bnd.4	$$⊢\phi \to P\in {\mathbb{N}}_{\mathrm{0s}}$$
5		bdaypw2bnd.5	Could not format ( ph -> Y Y
6		bdaypw2bnd.6	$$⊢\phi \to \left(X{+}_{s}P\right){<}_{s}N$$
7	2	n0nod	$$⊢\phi \to X\in \mathrm{No}$$
8	3	n0nod	$$⊢\phi \to Y\in \mathrm{No}$$
9	8 4	pw2divscld	Could not format ( ph -> ( Y /su ( 2s ^su P ) ) e. No ) : No typesetting found for |- ( ph -> ( Y /su ( 2s ^su P ) ) e. No ) with typecode |-
10		addbday	Could not format ( ( X e. No /\ ( Y /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) ) : No typesetting found for |- ( ( X e. No /\ ( Y /su ( 2s ^su P ) ) e. No ) -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) ) with typecode |-
11	7 9 10	syl2anc	Could not format ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) ) : No typesetting found for |- ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) ) with typecode |-
12		bdaypw2n0bnd	Could not format ( ( Y e. NN0_s /\ P e. NN0_s /\ Y ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) : No typesetting found for |- ( ( Y e. NN0_s /\ P e. NN0_s /\ Y ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) with typecode |-
13	3 4 5 12	syl3anc	Could not format ( ph -> ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) : No typesetting found for |- ( ph -> ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) ) with typecode |-
14		bdayon	Could not format ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On : No typesetting found for |- ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On with typecode |-
15		bdayon	$$⊢\mathrm{bday}\left(P\right)\in \mathrm{On}$$
16	15	onsuci	$$⊢\mathrm{suc}\mathrm{bday}\left(P\right)\in \mathrm{On}$$
17		bdayon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
18		naddss2	Could not format ( ( ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( Y /su ( 2s ^su P ) ) ) e. On /\ suc ( bday ` P ) e. On /\ ( bday ` X ) e. On ) -> ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) ) with typecode |-
19	14 16 17 18	mp3an	Could not format ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) : No typesetting found for |- ( ( bday ` ( Y /su ( 2s ^su P ) ) ) C_ suc ( bday ` P ) <-> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) with typecode |-
20	13 19	sylib	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( ( bday ` X ) +no suc ( bday ` P ) ) ) with typecode |-
21		bdayn0p1	$$⊢P\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(P{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(P\right)$$
22	4 21	syl	$$⊢\phi \to \mathrm{bday}\left(P{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(P\right)$$
23	22	oveq2d	$$⊢\phi \to \mathrm{bday}\left(X\right)+\mathrm{bday}\left(P{+}_s{1}_s\right)=\mathrm{bday}\left(X\right)+\mathrm{suc}\mathrm{bday}\left(P\right)$$
24		n0on	$$⊢X\in {\mathbb{N}}_{\mathrm{0s}}\to X\in {On}_s$$
25	2 24	syl	$$⊢\phi \to X\in {On}_s$$
26		peano2n0s	$$⊢P\in {\mathbb{N}}_{\mathrm{0s}}\to P{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
27	4 26	syl	$$⊢\phi \to P{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
28		n0on	$$⊢P{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\to P{+}_s{1}_s\in {On}_s$$
29	27 28	syl	$$⊢\phi \to P{+}_s{1}_s\in {On}_s$$
30		addonbday	$$⊢\left(X\in {On}_s\wedge P{+}_s{1}_s\in {On}_s\right)\to \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)=\mathrm{bday}\left(X\right)+\mathrm{bday}\left(P{+}_s{1}_s\right)$$
31	25 29 30	syl2anc	$$⊢\phi \to \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)=\mathrm{bday}\left(X\right)+\mathrm{bday}\left(P{+}_s{1}_s\right)$$
32		n0on	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to N\in {On}_s$$
33	1 32	syl	$$⊢\phi \to N\in {On}_s$$
34		n0addscl	$$⊢\left(X\in {\mathbb{N}}_{\mathrm{0s}}\wedge P{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\to X{+}_s\left(P{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
35	2 27 34	syl2anc	$$⊢\phi \to X{+}_s\left(P{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
36		n0on	$$⊢X{+}_s\left(P{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\to X{+}_s\left(P{+}_s{1}_s\right)\in {On}_s$$
37	35 36	syl	$$⊢\phi \to X{+}_s\left(P{+}_s{1}_s\right)\in {On}_s$$
38		onlts	$$⊢\left(N\in {On}_s\wedge X{+}_s\left(P{+}_s{1}_s\right)\in {On}_s\right)\to \left(N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\leftrightarrow \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
39	33 37 38	syl2anc	$$⊢\phi \to \left(N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\leftrightarrow \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
40	39	notbid	$$⊢\phi \to \left(\neg N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\leftrightarrow \neg \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
41		n0addscl	$$⊢\left(X\in {\mathbb{N}}_{\mathrm{0s}}\wedge P\in {\mathbb{N}}_{\mathrm{0s}}\right)\to X{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}$$
42	2 4 41	syl2anc	$$⊢\phi \to X{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}$$
43		n0ltsp1le	$$⊢\left(X{+}_{s}P\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left(X{+}_{s}P\right){<}_{s}N\leftrightarrow \left(\left(X{+}_{s}P\right){+}_s{1}_s\right){\le }_{s}N\right)$$
44	42 1 43	syl2anc	$$⊢\phi \to \left(\left(X{+}_{s}P\right){<}_{s}N\leftrightarrow \left(\left(X{+}_{s}P\right){+}_s{1}_s\right){\le }_{s}N\right)$$
45	4	n0nod	$$⊢\phi \to P\in \mathrm{No}$$
46		1no	$$⊢1_s\in \mathrm{No}$$
47	46	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
48	7 45 47	addsassd	$$⊢\phi \to \left(X{+}_{s}P\right){+}_s{1}_s=X{+}_s\left(P{+}_s{1}_s\right)$$
49	48	breq1d	$$⊢\phi \to \left(\left(\left(X{+}_{s}P\right){+}_s{1}_s\right){\le }_{s}N\leftrightarrow \left(X{+}_s\left(P{+}_s{1}_s\right)\right){\le }_{s}N\right)$$
50	35	n0nod	$$⊢\phi \to X{+}_s\left(P{+}_s{1}_s\right)\in \mathrm{No}$$
51	1	n0nod	$$⊢\phi \to N\in \mathrm{No}$$
52		lenlts	$$⊢\left(X{+}_s\left(P{+}_s{1}_s\right)\in \mathrm{No}\wedge N\in \mathrm{No}\right)\to \left(\left(X{+}_s\left(P{+}_s{1}_s\right)\right){\le }_{s}N\leftrightarrow \neg N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
53	50 51 52	syl2anc	$$⊢\phi \to \left(\left(X{+}_s\left(P{+}_s{1}_s\right)\right){\le }_{s}N\leftrightarrow \neg N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
54	44 49 53	3bitrd	$$⊢\phi \to \left(\left(X{+}_{s}P\right){<}_{s}N\leftrightarrow \neg N{<}_s\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
55		bdayon	$$⊢\mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\in \mathrm{On}$$
56		bdayon	$$⊢\mathrm{bday}\left(N\right)\in \mathrm{On}$$
57		ontri1	$$⊢\left(\mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\in \mathrm{On}\wedge \mathrm{bday}\left(N\right)\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\subseteq \mathrm{bday}\left(N\right)\leftrightarrow \neg \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
58	55 56 57	mp2an	$$⊢\mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\subseteq \mathrm{bday}\left(N\right)\leftrightarrow \neg \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)$$
59	58	a1i	$$⊢\phi \to \left(\mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\subseteq \mathrm{bday}\left(N\right)\leftrightarrow \neg \mathrm{bday}\left(N\right)\in \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\right)$$
60	40 54 59	3bitr4d	$$⊢\phi \to \left(\left(X{+}_{s}P\right){<}_{s}N\leftrightarrow \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\subseteq \mathrm{bday}\left(N\right)\right)$$
61	6 60	mpbid	$$⊢\phi \to \mathrm{bday}\left(X{+}_s\left(P{+}_s{1}_s\right)\right)\subseteq \mathrm{bday}\left(N\right)$$
62	31 61	eqsstrrd	$$⊢\phi \to \mathrm{bday}\left(X\right)+\mathrm{bday}\left(P{+}_s{1}_s\right)\subseteq \mathrm{bday}\left(N\right)$$
63	23 62	eqsstrrd	$$⊢\phi \to \mathrm{bday}\left(X\right)+\mathrm{suc}\mathrm{bday}\left(P\right)\subseteq \mathrm{bday}\left(N\right)$$
64	20 63	sstrd	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) ) : No typesetting found for |- ( ph -> ( ( bday ` X ) +no ( bday ` ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) ) with typecode |-
65	11 64	sstrd	Could not format ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) ) : No typesetting found for |- ( ph -> ( bday ` ( X +s ( Y /su ( 2s ^su P ) ) ) ) C_ ( bday ` N ) ) with typecode |-