Theorem bdaypw2n0bnd

Description: Upper bound for the birthday of a proper fraction of a power of two. This is actually a strict equality when A is odd, but we do not need this for the rest of our development. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Assertion	bdaypw2n0bnd	Could not format assertion : No typesetting found for |- ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		n0s0suc	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to \left(N=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)$$
2		n0lts1e0	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{<}_s{1}_s\leftrightarrow A=0_s\right)$$
3		oveq1	$$⊢A=0_s\to A{/}_{\mathrm{su}}{1}_s=0_s{/}_{\mathrm{su}}{1}_s$$
4		0no	$$⊢0_s\in \mathrm{No}$$
5		divs1	$$⊢0_s\in \mathrm{No}\to 0_s{/}_{\mathrm{su}}{1}_s=0_s$$
6	4 5	ax-mp	$$⊢0_s{/}_{\mathrm{su}}{1}_s=0_s$$
7	3 6	eqtrdi	$$⊢A=0_s\to A{/}_{\mathrm{su}}{1}_s=0_s$$
8	7	fveq2d	$$⊢A=0_s\to \mathrm{bday}\left(A{/}_{\mathrm{su}}{1}_s\right)=\mathrm{bday}\left(0_s\right)$$
9		bday0	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
10	8 9	eqtrdi	$$⊢A=0_s\to \mathrm{bday}\left(A{/}_{\mathrm{su}}{1}_s\right)=\varnothing$$
11		0ss	$$⊢\varnothing \subseteq \mathrm{suc}\varnothing$$
12	10 11	eqsstrdi	$$⊢A=0_s\to \mathrm{bday}\left(A{/}_{\mathrm{su}}{1}_s\right)\subseteq \mathrm{suc}\varnothing$$
13	2 12	biimtrdi	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{<}_s{1}_s\to \mathrm{bday}\left(A{/}_{\mathrm{su}}{1}_s\right)\subseteq \mathrm{suc}\varnothing \right)$$
14		oveq2	Could not format ( N = 0s -> ( 2s ^su N ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( N = 0s -> ( 2s ^su N ) = ( 2s ^su 0s ) ) with typecode |-
15		2no	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
16		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
17	15 16	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
18	14 17	eqtrdi	Could not format ( N = 0s -> ( 2s ^su N ) = 1s ) : No typesetting found for |- ( N = 0s -> ( 2s ^su N ) = 1s ) with typecode |-
19	18	breq2d	Could not format ( N = 0s -> ( A A ( A A
20	18	oveq2d	Could not format ( N = 0s -> ( A /su ( 2s ^su N ) ) = ( A /su 1s ) ) : No typesetting found for |- ( N = 0s -> ( A /su ( 2s ^su N ) ) = ( A /su 1s ) ) with typecode |-
21	20	fveq2d	Could not format ( N = 0s -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su 1s ) ) ) : No typesetting found for |- ( N = 0s -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su 1s ) ) ) with typecode |-
22		fveq2	$$⊢N=0_s\to \mathrm{bday}\left(N\right)=\mathrm{bday}\left(0_s\right)$$
23	22 9	eqtrdi	$$⊢N=0_s\to \mathrm{bday}\left(N\right)=\varnothing$$
24	23	suceqd	$$⊢N=0_s\to \mathrm{suc}\mathrm{bday}\left(N\right)=\mathrm{suc}\varnothing$$
25	21 24	sseq12d	Could not format ( N = 0s -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) : No typesetting found for |- ( N = 0s -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) with typecode |-
26	19 25	imbi12d	Could not format ( N = 0s -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) ) : No typesetting found for |- ( N = 0s -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su 1s ) ) C_ suc (/) ) ) ) with typecode |-
27	13 26	imbitrrid	Could not format ( N = 0s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) : No typesetting found for |- ( N = 0s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) with typecode |-
28		bdaypw2n0bndlem	Could not format ( ( A e. NN0_s /\ x e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) : No typesetting found for |- ( ( A e. NN0_s /\ x e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) with typecode |-
29	28	3exp	Could not format ( A e. NN0_s -> ( x e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) : No typesetting found for |- ( A e. NN0_s -> ( x e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) with typecode |-
30	29	com12	Could not format ( x e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) : No typesetting found for |- ( x e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) with typecode |-
31		oveq2	Could not format ( N = ( x +s 1s ) -> ( 2s ^su N ) = ( 2s ^su ( x +s 1s ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( 2s ^su N ) = ( 2s ^su ( x +s 1s ) ) ) with typecode |-
32	31	breq2d	Could not format ( N = ( x +s 1s ) -> ( A A ( A A
33	31	oveq2d	Could not format ( N = ( x +s 1s ) -> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su ( x +s 1s ) ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( A /su ( 2s ^su N ) ) = ( A /su ( 2s ^su ( x +s 1s ) ) ) ) with typecode |-
34	33	fveq2d	Could not format ( N = ( x +s 1s ) -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( bday ` ( A /su ( 2s ^su N ) ) ) = ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) ) with typecode |-
35		fveq2	$$⊢N=x{+}_s{1}_s\to \mathrm{bday}\left(N\right)=\mathrm{bday}\left(x{+}_s{1}_s\right)$$
36	35	suceqd	$$⊢N=x{+}_s{1}_s\to \mathrm{suc}\mathrm{bday}\left(N\right)=\mathrm{suc}\mathrm{bday}\left(x{+}_s{1}_s\right)$$
37	34 36	sseq12d	Could not format ( N = ( x +s 1s ) -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) <-> ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) with typecode |-
38	32 37	imbi12d	Could not format ( N = ( x +s 1s ) -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) <-> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) with typecode |-
39	38	imbi2d	Could not format ( N = ( x +s 1s ) -> ( ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) <-> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) ) : No typesetting found for |- ( N = ( x +s 1s ) -> ( ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) <-> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su ( x +s 1s ) ) ) ) C_ suc ( bday ` ( x +s 1s ) ) ) ) ) ) with typecode |-
40	30 39	syl5ibrcom	Could not format ( x e. NN0_s -> ( N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) ) : No typesetting found for |- ( x e. NN0_s -> ( N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) ) with typecode |-
41	40	rexlimiv	Could not format ( E. x e. NN0_s N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) : No typesetting found for |- ( E. x e. NN0_s N = ( x +s 1s ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) with typecode |-
42	27 41	jaoi	Could not format ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) : No typesetting found for |- ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) with typecode |-
43	1 42	syl	Could not format ( N e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) : No typesetting found for |- ( N e. NN0_s -> ( A e. NN0_s -> ( A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) ) ) with typecode |-
44	43	3imp21	Could not format ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) : No typesetting found for |- ( ( A e. NN0_s /\ N e. NN0_s /\ A ( bday ` ( A /su ( 2s ^su N ) ) ) C_ suc ( bday ` N ) ) with typecode |-