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	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s ( 2s ↑s 𝑁 ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		n0s0suc	⊢ ( 𝑁 ∈ ℕ0s → ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) )
2		n0lts1e0	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 <s 1s ↔ 𝐴 = 0s ) )
3		oveq1	⊢ ( 𝐴 = 0s → ( 𝐴 /su 1s ) = ( 0s /su 1s ) )
4		0no	⊢ 0s ∈ No
5		divs1	⊢ ( 0s ∈ No → ( 0s /su 1s ) = 0s )
6	4 5	ax-mp	⊢ ( 0s /su 1s ) = 0s
7	3 6	eqtrdi	⊢ ( 𝐴 = 0s → ( 𝐴 /su 1s ) = 0s )
8	7	fveq2d	⊢ ( 𝐴 = 0s → ( bday ‘ ( 𝐴 /su 1s ) ) = ( bday ‘ 0s ) )
9		bday0	⊢ ( bday ‘ 0s ) = ∅
10	8 9	eqtrdi	⊢ ( 𝐴 = 0s → ( bday ‘ ( 𝐴 /su 1s ) ) = ∅ )
11		0ss	⊢ ∅ ⊆ suc ∅
12	10 11	eqsstrdi	⊢ ( 𝐴 = 0s → ( bday ‘ ( 𝐴 /su 1s ) ) ⊆ suc ∅ )
13	2 12	biimtrdi	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 <s 1s → ( bday ‘ ( 𝐴 /su 1s ) ) ⊆ suc ∅ ) )
14		oveq2	⊢ ( 𝑁 = 0s → ( 2s ↑s 𝑁 ) = ( 2s ↑s 0s ) )
15		2no	⊢ 2s ∈ No
16		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
17	15 16	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
18	14 17	eqtrdi	⊢ ( 𝑁 = 0s → ( 2s ↑s 𝑁 ) = 1s )
19	18	breq2d	⊢ ( 𝑁 = 0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) ↔ 𝐴 <s 1s ) )
20	18	oveq2d	⊢ ( 𝑁 = 0s → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su 1s ) )
21	20	fveq2d	⊢ ( 𝑁 = 0s → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( bday ‘ ( 𝐴 /su 1s ) ) )
22		fveq2	⊢ ( 𝑁 = 0s → ( bday ‘ 𝑁 ) = ( bday ‘ 0s ) )
23	22 9	eqtrdi	⊢ ( 𝑁 = 0s → ( bday ‘ 𝑁 ) = ∅ )
24	23	suceqd	⊢ ( 𝑁 = 0s → suc ( bday ‘ 𝑁 ) = suc ∅ )
25	21 24	sseq12d	⊢ ( 𝑁 = 0s → ( ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ↔ ( bday ‘ ( 𝐴 /su 1s ) ) ⊆ suc ∅ ) )
26	19 25	imbi12d	⊢ ( 𝑁 = 0s → ( ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ↔ ( 𝐴 <s 1s → ( bday ‘ ( 𝐴 /su 1s ) ) ⊆ suc ∅ ) ) )
27	13 26	imbitrrid	⊢ ( 𝑁 = 0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) )
28		bdaypw2n0bndlem	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s ∧ 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) )
29	28	3exp	⊢ ( 𝐴 ∈ ℕ0s → ( 𝑥 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) ) ) )
30	29	com12	⊢ ( 𝑥 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) ) ) )
31		oveq2	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( 2s ↑s 𝑁 ) = ( 2s ↑s ( 𝑥 +s 1s ) ) )
32	31	breq2d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( 𝐴 <s ( 2s ↑s 𝑁 ) ↔ 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) ) )
33	31	oveq2d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) = ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) )
34	33	fveq2d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) = ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) )
35		fveq2	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( bday ‘ 𝑁 ) = ( bday ‘ ( 𝑥 +s 1s ) ) )
36	35	suceqd	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → suc ( bday ‘ 𝑁 ) = suc ( bday ‘ ( 𝑥 +s 1s ) ) )
37	34 36	sseq12d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ↔ ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) ) )
38	32 37	imbi12d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ↔ ( 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) ) ) )
39	38	imbi2d	⊢ ( 𝑁 = ( 𝑥 +s 1s ) → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s ( 𝑥 +s 1s ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s ( 𝑥 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 𝑥 +s 1s ) ) ) ) ) )
40	30 39	syl5ibrcom	⊢ ( 𝑥 ∈ ℕ0s → ( 𝑁 = ( 𝑥 +s 1s ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) ) )
41	40	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) )
42	27 41	jaoi	⊢ ( ( 𝑁 = 0s ∨ ∃ 𝑥 ∈ ℕ0s 𝑁 = ( 𝑥 +s 1s ) ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) )
43	1 42	syl	⊢ ( 𝑁 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 <s ( 2s ↑s 𝑁 ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) ) ) )
44	43	3imp21	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ∧ 𝐴 <s ( 2s ↑s 𝑁 ) ) → ( bday ‘ ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ) ⊆ suc ( bday ‘ 𝑁 ) )