Theorem pw2bday

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

	Ref	Expression
Assertion	pw2bday	Could not format assertion : No typesetting found for |- ( N e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	Could not format ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = ( 2s ^su 0s ) ) with typecode |-
2		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
3		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
4	2 3	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
5	1 4	eqtrdi	Could not format ( m = 0s -> ( 2s ^su m ) = 1s ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = 1s ) with typecode |-
6	5	oveq2d	Could not format ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su 1s ) ) : No typesetting found for |- ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su 1s ) ) with typecode |-
7		1sno	$$⊢1_s\in \mathrm{No}$$
8		divs1	$$⊢1_s\in \mathrm{No}\to 1_s{/}_{\mathrm{su}}{1}_s=1_s$$
9	7 8	ax-mp	$$⊢1_s{/}_{\mathrm{su}}{1}_s=1_s$$
10	6 9	eqtrdi	Could not format ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = 1s ) : No typesetting found for |- ( m = 0s -> ( 1s /su ( 2s ^su m ) ) = 1s ) with typecode |-
11	10	fveq2d	Could not format ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` 1s ) ) : No typesetting found for |- ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` 1s ) ) with typecode |-
12		bday1s	$$⊢\mathrm{bday}\left(1_s\right)=1_{𝑜}$$
13	11 12	eqtrdi	Could not format ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = 1o ) : No typesetting found for |- ( m = 0s -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = 1o ) with typecode |-
14	13	eleq1d	Could not format ( m = 0s -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> 1o e. _om ) ) : No typesetting found for |- ( m = 0s -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> 1o e. _om ) ) with typecode |-
15		oveq2	Could not format ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) : No typesetting found for |- ( m = n -> ( 2s ^su m ) = ( 2s ^su n ) ) with typecode |-
16	15	oveq2d	Could not format ( m = n -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- ( m = n -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su n ) ) ) with typecode |-
17	16	fveq2d	Could not format ( m = n -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( m = n -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
18	17	eleq1d	Could not format ( m = n -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) ) : No typesetting found for |- ( m = n -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) ) with typecode |-
19		oveq2	Could not format ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 2s ^su m ) = ( 2s ^su ( n +s 1s ) ) ) with typecode |-
20	19	oveq2d	Could not format ( m = ( n +s 1s ) -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
21	20	fveq2d	Could not format ( m = ( n +s 1s ) -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
22	21	eleq1d	Could not format ( m = ( n +s 1s ) -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
23		oveq2	Could not format ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) : No typesetting found for |- ( m = N -> ( 2s ^su m ) = ( 2s ^su N ) ) with typecode |-
24	23	oveq2d	Could not format ( m = N -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su N ) ) ) : No typesetting found for |- ( m = N -> ( 1s /su ( 2s ^su m ) ) = ( 1s /su ( 2s ^su N ) ) ) with typecode |-
25	24	fveq2d	Could not format ( m = N -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su N ) ) ) ) : No typesetting found for |- ( m = N -> ( bday ` ( 1s /su ( 2s ^su m ) ) ) = ( bday ` ( 1s /su ( 2s ^su N ) ) ) ) with typecode |-
26	25	eleq1d	Could not format ( m = N -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) ) : No typesetting found for |- ( m = N -> ( ( bday ` ( 1s /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) ) with typecode |-
27		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
28		cutpw2	Could not format ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( n e. NN0_s -> ( 1s /su ( 2s ^su ( n +s 1s ) ) ) = ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) with typecode |-
29	28	fveq2d	Could not format ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) ) with typecode |-
30		0sno	$$⊢0_s\in \mathrm{No}$$
31	30	a1i	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s\in \mathrm{No}$$
32	7	a1i	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s\in \mathrm{No}$$
33		expscl	Could not format ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su n ) e. No ) with typecode |-
34	2 33	mpan	Could not format ( n e. NN0_s -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( n e. NN0_s -> ( 2s ^su n ) e. No ) with typecode |-
35		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
36		expsne0	Could not format ( ( 2s e. No /\ 2s =/= 0s /\ n e. NN0_s ) -> ( 2s ^su n ) =/= 0s ) : No typesetting found for |- ( ( 2s e. No /\ 2s =/= 0s /\ n e. NN0_s ) -> ( 2s ^su n ) =/= 0s ) with typecode |-
37	2 35 36	mp3an12	Could not format ( n e. NN0_s -> ( 2s ^su n ) =/= 0s ) : No typesetting found for |- ( n e. NN0_s -> ( 2s ^su n ) =/= 0s ) with typecode |-
38	32 34 37	divscld	Could not format ( n e. NN0_s -> ( 1s /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( n e. NN0_s -> ( 1s /su ( 2s ^su n ) ) e. No ) with typecode |-
39		muls02	Could not format ( ( 2s ^su n ) e. No -> ( 0s x.s ( 2s ^su n ) ) = 0s ) : No typesetting found for |- ( ( 2s ^su n ) e. No -> ( 0s x.s ( 2s ^su n ) ) = 0s ) with typecode |-
40	34 39	syl	Could not format ( n e. NN0_s -> ( 0s x.s ( 2s ^su n ) ) = 0s ) : No typesetting found for |- ( n e. NN0_s -> ( 0s x.s ( 2s ^su n ) ) = 0s ) with typecode |-
41		0slt1s	$$⊢0_s{<}_s{1}_s$$
42	40 41	eqbrtrdi	Could not format ( n e. NN0_s -> ( 0s x.s ( 2s ^su n ) ) ( 0s x.s ( 2s ^su n ) )
43		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
44		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
45	43 44	ax-mp	Could not format 0s
46		expsgt0	Could not format ( ( 2s e. No /\ n e. NN0_s /\ 0s 0s 0s
47	2 45 46	mp3an13	Could not format ( n e. NN0_s -> 0s 0s
48	31 32 34 47	sltmuldivd	Could not format ( n e. NN0_s -> ( ( 0s x.s ( 2s ^su n ) ) 0s ( ( 0s x.s ( 2s ^su n ) ) 0s
49	42 48	mpbid	Could not format ( n e. NN0_s -> 0s 0s
50	31 38 49	ssltsn	Could not format ( n e. NN0_s -> { 0s } < { 0s } <
51		suc0	$$⊢\mathrm{suc}\varnothing =\left\{\varnothing \right\}$$
52		bday0s	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
53	52	sneqi	$$⊢\left\{\mathrm{bday}\left(0_s\right)\right\}=\left\{\varnothing \right\}$$
54		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
55		fnsnfv	$$⊢\left(\mathrm{bday}Fn\mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left\{\mathrm{bday}\left(0_s\right)\right\}=\mathrm{bday}\left[\left\{0_s\right\}\right]$$
56	54 30 55	mp2an	$$⊢\left\{\mathrm{bday}\left(0_s\right)\right\}=\mathrm{bday}\left[\left\{0_s\right\}\right]$$
57	51 53 56	3eqtr2i	$$⊢\mathrm{suc}\varnothing =\mathrm{bday}\left[\left\{0_s\right\}\right]$$
58	57	a1i	$$⊢n\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{suc}\varnothing =\mathrm{bday}\left[\left\{0_s\right\}\right]$$
59		fnsnfv	Could not format ( ( bday Fn No /\ ( 1s /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( bday Fn No /\ ( 1s /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) with typecode |-
60	54 59	mpan	Could not format ( ( 1s /su ( 2s ^su n ) ) e. No -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( 1s /su ( 2s ^su n ) ) e. No -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) with typecode |-
61	38 60	syl	Could not format ( n e. NN0_s -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( n e. NN0_s -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } = ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) with typecode |-
62	58 61	uneq12d	Could not format ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) ) with typecode |-
63		imaundi	Could not format ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) = ( ( bday " { 0s } ) u. ( bday " { ( 1s /su ( 2s ^su n ) ) } ) ) with typecode |-
64	62 63	eqtr4di	Could not format ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) = ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) ) with typecode |-
65		0ss	Could not format (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
66		ord0	$$⊢\mathrm{Ord}\varnothing$$
67		bdayelon	Could not format ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On : No typesetting found for |- ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On with typecode |-
68	67	onordi	Could not format Ord ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- Ord ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
69		ordsucsssuc	Could not format ( ( Ord (/) /\ Ord ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) -> ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) ) : No typesetting found for |- ( ( Ord (/) /\ Ord ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) -> ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) ) with typecode |-
70	66 68 69	mp2an	Could not format ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( (/) C_ ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
71	65 70	mpbi	Could not format suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- suc (/) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
72		fvex	Could not format ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _V : No typesetting found for |- ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _V with typecode |-
73	72	sucid	Could not format ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
74		snssi	Could not format ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) -> { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
75	73 74	ax-mp	Could not format { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
76	71 75	unssi	Could not format ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) : No typesetting found for |- ( suc (/) u. { ( bday ` ( 1s /su ( 2s ^su n ) ) ) } ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) with typecode |-
77	64 76	eqsstrrdi	Could not format ( n e. NN0_s -> ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( bday " ( { 0s } u. { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
78	67	onsuci	Could not format suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On : No typesetting found for |- suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On with typecode |-
79		scutbdaybnd	Could not format ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
80	78 79	mp3an2	Could not format ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( { 0s } < ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
81	50 77 80	syl2anc	Could not format ( n e. NN0_s -> ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( bday ` ( { 0s } |s { ( 1s /su ( 2s ^su n ) ) } ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
82	29 81	eqsstrd	Could not format ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
83		bdayelon	Could not format ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On : No typesetting found for |- ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On with typecode |-
84		onsssuc	Could not format ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On ) -> ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. On /\ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. On ) -> ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) ) with typecode |-
85	83 78 84	mp2an	Could not format ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) C_ suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) <-> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
86	82 85	sylib	Could not format ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( n e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) ) with typecode |-
87		peano2	Could not format ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
88		peano2	Could not format ( suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
89	87 88	syl	Could not format ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
90		elnn	Could not format ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) /\ suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) /\ suc suc ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
91	86 89 90	syl2an	Could not format ( ( n e. NN0_s /\ ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( n e. NN0_s /\ ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om ) -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
92	91	ex	Could not format ( n e. NN0_s -> ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( n e. NN0_s -> ( ( bday ` ( 1s /su ( 2s ^su n ) ) ) e. _om -> ( bday ` ( 1s /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
93	14 18 22 26 27 92	n0sind	Could not format ( N e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) : No typesetting found for |- ( N e. NN0_s -> ( bday ` ( 1s /su ( 2s ^su N ) ) ) e. _om ) with typecode |-