Theorem pw2bday

Description: The inverses of powers of two have finite birthdays. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	pw2bday	⊢ ( 𝑁 ∈ ℕ0s → ( bday ‘ ( 1s /su ( 2s ↑s 𝑁 ) ) ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = ( 2s ↑s 0s ) )
2		2sno	⊢ 2s ∈ No
3		exps0	⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
4	2 3	ax-mp	⊢ ( 2s ↑s 0s ) = 1s
5	1 4	eqtrdi	⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = 1s )
6	5	oveq2d	⊢ ( 𝑚 = 0s → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su 1s ) )
7		1sno	⊢ 1s ∈ No
8		divs1	⊢ ( 1s ∈ No → ( 1s /su 1s ) = 1s )
9	7 8	ax-mp	⊢ ( 1s /su 1s ) = 1s
10	6 9	eqtrdi	⊢ ( 𝑚 = 0s → ( 1s /su ( 2s ↑s 𝑚 ) ) = 1s )
11	10	fveq2d	⊢ ( 𝑚 = 0s → ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ 1s ) )
12		bday1s	⊢ ( bday ‘ 1s ) = 1o
13	11 12	eqtrdi	⊢ ( 𝑚 = 0s → ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) = 1o )
14	13	eleq1d	⊢ ( 𝑚 = 0s → ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ 1o ∈ ω ) )
15		oveq2	⊢ ( 𝑚 = 𝑛 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑛 ) )
16	15	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s 𝑛 ) ) )
17	16	fveq2d	⊢ ( 𝑚 = 𝑛 → ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
18	17	eleq1d	⊢ ( 𝑚 = 𝑛 → ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) )
19		oveq2	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
20	19	oveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
21	20	fveq2d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
22	21	eleq1d	⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
23		oveq2	⊢ ( 𝑚 = 𝑁 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑁 ) )
24	23	oveq2d	⊢ ( 𝑚 = 𝑁 → ( 1s /su ( 2s ↑s 𝑚 ) ) = ( 1s /su ( 2s ↑s 𝑁 ) ) )
25	24	fveq2d	⊢ ( 𝑚 = 𝑁 → ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 1s /su ( 2s ↑s 𝑁 ) ) ) )
26	25	eleq1d	⊢ ( 𝑚 = 𝑁 → ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 1s /su ( 2s ↑s 𝑁 ) ) ) ∈ ω ) )
27		1onn	⊢ 1o ∈ ω
28		cutpw2	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
29	28	fveq2d	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) )
30		0sno	⊢ 0s ∈ No
31	30	a1i	⊢ ( 𝑛 ∈ ℕ0s → 0s ∈ No )
32	7	a1i	⊢ ( 𝑛 ∈ ℕ0s → 1s ∈ No )
33		expscl	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ No )
34	2 33	mpan	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ∈ No )
35		2ne0s	⊢ 2s ≠ 0s
36		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ≠ 0s )
37	2 35 36	mp3an12	⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ≠ 0s )
38	32 34 37	divscld	⊢ ( 𝑛 ∈ ℕ0s → ( 1s /su ( 2s ↑s 𝑛 ) ) ∈ No )
39		muls02	⊢ ( ( 2s ↑s 𝑛 ) ∈ No → ( 0s ·s ( 2s ↑s 𝑛 ) ) = 0s )
40	34 39	syl	⊢ ( 𝑛 ∈ ℕ0s → ( 0s ·s ( 2s ↑s 𝑛 ) ) = 0s )
41		0slt1s	⊢ 0s <s 1s
42	40 41	eqbrtrdi	⊢ ( 𝑛 ∈ ℕ0s → ( 0s ·s ( 2s ↑s 𝑛 ) ) <s 1s )
43		2nns	⊢ 2s ∈ ℕs
44		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
45	43 44	ax-mp	⊢ 0s <s 2s
46		expsgt0	⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s 𝑛 ) )
47	2 45 46	mp3an13	⊢ ( 𝑛 ∈ ℕ0s → 0s <s ( 2s ↑s 𝑛 ) )
48	31 32 34 47	sltmuldivd	⊢ ( 𝑛 ∈ ℕ0s → ( ( 0s ·s ( 2s ↑s 𝑛 ) ) <s 1s ↔ 0s <s ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
49	42 48	mpbid	⊢ ( 𝑛 ∈ ℕ0s → 0s <s ( 1s /su ( 2s ↑s 𝑛 ) ) )
50	31 38 49	ssltsn	⊢ ( 𝑛 ∈ ℕ0s → { 0s } <<s { ( 1s /su ( 2s ↑s 𝑛 ) ) } )
51		suc0	⊢ suc ∅ = { ∅ }
52		bday0s	⊢ ( bday ‘ 0s ) = ∅
53	52	sneqi	⊢ { ( bday ‘ 0s ) } = { ∅ }
54		bdayfn	⊢ bday Fn No
55		fnsnfv	⊢ ( ( bday Fn No ∧ 0s ∈ No ) → { ( bday ‘ 0s ) } = ( bday “ { 0s } ) )
56	54 30 55	mp2an	⊢ { ( bday ‘ 0s ) } = ( bday “ { 0s } )
57	51 53 56	3eqtr2i	⊢ suc ∅ = ( bday “ { 0s } )
58	57	a1i	⊢ ( 𝑛 ∈ ℕ0s → suc ∅ = ( bday “ { 0s } ) )
59		fnsnfv	⊢ ( ( bday Fn No ∧ ( 1s /su ( 2s ↑s 𝑛 ) ) ∈ No ) → { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
60	54 59	mpan	⊢ ( ( 1s /su ( 2s ↑s 𝑛 ) ) ∈ No → { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
61	38 60	syl	⊢ ( 𝑛 ∈ ℕ0s → { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
62	58 61	uneq12d	⊢ ( 𝑛 ∈ ℕ0s → ( suc ∅ ∪ { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } ) = ( ( bday “ { 0s } ) ∪ ( bday “ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) )
63		imaundi	⊢ ( bday “ ( { 0s } ∪ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) = ( ( bday “ { 0s } ) ∪ ( bday “ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) )
64	62 63	eqtr4di	⊢ ( 𝑛 ∈ ℕ0s → ( suc ∅ ∪ { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } ) = ( bday “ ( { 0s } ∪ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) )
65		0ss	⊢ ∅ ⊆ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
66		ord0	⊢ Ord ∅
67		bdayelon	⊢ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ On
68	67	onordi	⊢ Ord ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
69		ordsucsssuc	⊢ ( ( Ord ∅ ∧ Ord ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ) → ( ∅ ⊆ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ↔ suc ∅ ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ) )
70	66 68 69	mp2an	⊢ ( ∅ ⊆ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ↔ suc ∅ ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
71	65 70	mpbi	⊢ suc ∅ ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
72		fvex	⊢ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ V
73	72	sucid	⊢ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
74		snssi	⊢ ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) → { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
75	73 74	ax-mp	⊢ { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
76	71 75	unssi	⊢ ( suc ∅ ∪ { ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) } ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) )
77	64 76	eqsstrrdi	⊢ ( 𝑛 ∈ ℕ0s → ( bday “ ( { 0s } ∪ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
78	67	onsuci	⊢ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ On
79		scutbdaybnd	⊢ ( ( { 0s } <<s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ∧ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ On ∧ ( bday “ ( { 0s } ∪ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ) → ( bday ‘ ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
80	78 79	mp3an2	⊢ ( ( { 0s } <<s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ∧ ( bday “ ( { 0s } ∪ { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ) → ( bday ‘ ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
81	50 77 80	syl2anc	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( { 0s } |s { ( 1s /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
82	29 81	eqsstrd	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
83		bdayelon	⊢ ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On
84		onsssuc	⊢ ( ( ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ On ∧ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ On ) → ( ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ↔ ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ) )
85	83 78 84	mp2an	⊢ ( ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ⊆ suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ↔ ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
86	82 85	sylib	⊢ ( 𝑛 ∈ ℕ0s → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) )
87		peano2	⊢ ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω → suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
88		peano2	⊢ ( suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω → suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
89	87 88	syl	⊢ ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω → suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
90		elnn	⊢ ( ( ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∧ suc suc ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
91	86 89 90	syl2an	⊢ ( ( 𝑛 ∈ ℕ0s ∧ ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
92	91	ex	⊢ ( 𝑛 ∈ ℕ0s → ( ( bday ‘ ( 1s /su ( 2s ↑s 𝑛 ) ) ) ∈ ω → ( bday ‘ ( 1s /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
93	14 18 22 26 27 92	n0sind	⊢ ( 𝑁 ∈ ℕ0s → ( bday ‘ ( 1s /su ( 2s ↑s 𝑁 ) ) ) ∈ ω )