Theorem zs12bday

Description: A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Assertion	zs12bday	Could not format assertion : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elzs12	Could not format ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) : No typesetting found for |- ( A e. ZZ_s[1/2] <-> E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) ) with typecode |-
2		fvoveq1	Could not format ( z = x -> ( bday ` ( z /su ( 2s ^su y ) ) ) = ( bday ` ( x /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( z = x -> ( bday ` ( z /su ( 2s ^su y ) ) ) = ( bday ` ( x /su ( 2s ^su y ) ) ) ) with typecode |-
3	2	eleq1d	Could not format ( z = x -> ( ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) ) : No typesetting found for |- ( z = x -> ( ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) ) with typecode |-
4		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 |-
5		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
6		exps0	Could not format ( 2s e. No -> ( 2s ^su 0s ) = 1s ) : No typesetting found for |- ( 2s e. No -> ( 2s ^su 0s ) = 1s ) with typecode |-
7	5 6	ax-mp	Could not format ( 2s ^su 0s ) = 1s : No typesetting found for |- ( 2s ^su 0s ) = 1s with typecode |-
8	4 7	eqtrdi	Could not format ( m = 0s -> ( 2s ^su m ) = 1s ) : No typesetting found for |- ( m = 0s -> ( 2s ^su m ) = 1s ) with typecode |-
9	8	oveq2d	Could not format ( m = 0s -> ( z /su ( 2s ^su m ) ) = ( z /su 1s ) ) : No typesetting found for |- ( m = 0s -> ( z /su ( 2s ^su m ) ) = ( z /su 1s ) ) with typecode |-
10	9	fveq2d	Could not format ( m = 0s -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su 1s ) ) ) : No typesetting found for |- ( m = 0s -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su 1s ) ) ) with typecode |-
11	10	eleq1d	Could not format ( m = 0s -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su 1s ) ) e. _om ) ) : No typesetting found for |- ( m = 0s -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su 1s ) ) e. _om ) ) with typecode |-
12	11	ralbidv	Could not format ( m = 0s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su 1s ) ) e. _om ) ) : No typesetting found for |- ( m = 0s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su 1s ) ) e. _om ) ) with typecode |-
13		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 |-
14	13	oveq2d	Could not format ( m = n -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su n ) ) ) : No typesetting found for |- ( m = n -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su n ) ) ) with typecode |-
15	14	fveq2d	Could not format ( m = n -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( m = n -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su n ) ) ) ) with typecode |-
16	15	eleq1d	Could not format ( m = n -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) ) : No typesetting found for |- ( m = n -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) ) with typecode |-
17	16	ralbidv	Could not format ( m = n -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) ) : No typesetting found for |- ( m = n -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) ) with typecode |-
18		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 |-
19	18	oveq2d	Could not format ( m = ( n +s 1s ) -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
20	19	fveq2d	Could not format ( m = ( n +s 1s ) -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
21	20	eleq1d	Could not format ( m = ( n +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
22	21	ralbidv	Could not format ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
23		fvoveq1	Could not format ( z = w -> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( z = w -> ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
24	23	eleq1d	Could not format ( z = w -> ( ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( z = w -> ( ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
25	24	cbvralvw	Could not format ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
26	22 25	bitrdi	Could not format ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( m = ( n +s 1s ) -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
27		oveq2	Could not format ( m = y -> ( 2s ^su m ) = ( 2s ^su y ) ) : No typesetting found for |- ( m = y -> ( 2s ^su m ) = ( 2s ^su y ) ) with typecode |-
28	27	oveq2d	Could not format ( m = y -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su y ) ) ) : No typesetting found for |- ( m = y -> ( z /su ( 2s ^su m ) ) = ( z /su ( 2s ^su y ) ) ) with typecode |-
29	28	fveq2d	Could not format ( m = y -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( m = y -> ( bday ` ( z /su ( 2s ^su m ) ) ) = ( bday ` ( z /su ( 2s ^su y ) ) ) ) with typecode |-
30	29	eleq1d	Could not format ( m = y -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) ) : No typesetting found for |- ( m = y -> ( ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) ) with typecode |-
31	30	ralbidv	Could not format ( m = y -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) ) : No typesetting found for |- ( m = y -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su m ) ) ) e. _om <-> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) ) with typecode |-
32		zno	$$⊢z\in {\mathbb{Z}}_s\to z\in \mathrm{No}$$
33		divs1	$$⊢z\in \mathrm{No}\to z{/}_{\mathrm{su}}{1}_s=z$$
34	32 33	syl	$$⊢z\in {\mathbb{Z}}_s\to z{/}_{\mathrm{su}}{1}_s=z$$
35	34	fveq2d	$$⊢z\in {\mathbb{Z}}_s\to \mathrm{bday}\left(z{/}_{\mathrm{su}}{1}_s\right)=\mathrm{bday}\left(z\right)$$
36		zsbday	$$⊢z\in {\mathbb{Z}}_s\to \mathrm{bday}\left(z\right)\in \mathrm{\omega }$$
37	35 36	eqeltrd	$$⊢z\in {\mathbb{Z}}_s\to \mathrm{bday}\left(z{/}_{\mathrm{su}}{1}_s\right)\in \mathrm{\omega }$$
38	37	rgen	$$⊢\forall z\in {\mathbb{Z}}_s\mathrm{bday}\left(z{/}_{\mathrm{su}}{1}_s\right)\in \mathrm{\omega }$$
39		zseo	Could not format ( w e. ZZ_s -> ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( w e. ZZ_s -> ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
40		expsp1	Could not format ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ n e. NN0_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
41	5 40	mpan	Could not format ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( n e. NN0_s -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
42	41	adantr	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su ( n +s 1s ) ) = ( ( 2s ^su n ) x.s 2s ) ) with typecode |-
43	42	oveq2d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) ) with typecode |-
44	5	a1i	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s e. No ) with typecode |-
45		zno	$$⊢t\in {\mathbb{Z}}_s\to t\in \mathrm{No}$$
46	45	adantl	$$⊢\left(n\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{Z}}_s\right)\to t\in \mathrm{No}$$
47	44 46	mulscld	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No ) with typecode |-
48		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 |-
49	5 48	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 |-
50	49	adantr	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No ) with typecode |-
51		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
52		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 |-
53	5 51 52	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 |-
54	53	adantr	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s ) with typecode |-
55	51	a1i	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s =/= 0s ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> 2s =/= 0s ) with typecode |-
56	47 50 44 54 55	divdivs1d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s t ) /su ( ( 2s ^su n ) x.s 2s ) ) ) with typecode |-
57	44 46 50 54	divsassd	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su n ) ) = ( 2s x.s ( t /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su n ) ) = ( 2s x.s ( t /su ( 2s ^su n ) ) ) ) with typecode |-
58	57	oveq1d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) /su ( 2s ^su n ) ) /su 2s ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) ) with typecode |-
59	43 56 58	3eqtr2d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) ) with typecode |-
60	46 50 54	divscld	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No ) with typecode |-
61	60 44 55	divscan3d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) = ( t /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s ( t /su ( 2s ^su n ) ) ) /su 2s ) = ( t /su ( 2s ^su n ) ) ) with typecode |-
62	59 61	eqtrd	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( t /su ( 2s ^su n ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) = ( t /su ( 2s ^su n ) ) ) with typecode |-
63	62	fveq2d	Could not format ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( n e. NN0_s /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) with typecode |-
64	63	adantlr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) with typecode |-
65		fvoveq1	Could not format ( z = t -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( z = t -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) with typecode |-
66	65	eleq1d	Could not format ( z = t -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) ) : No typesetting found for |- ( z = t -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) ) with typecode |-
67	66	rspccva	Could not format ( ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
68	67	adantll	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( t /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
69	64 68	eqeltrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
70		fvoveq1	Could not format ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
71	70	eleq1d	Could not format ( w = ( 2s x.s t ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( w = ( 2s x.s t ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( 2s x.s t ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
72	69 71	syl5ibrcom	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
73	72	rexlimdva	Could not format ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( 2s x.s t ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
74	45	adantl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. No ) with typecode |-
75		no2times	Could not format ( t e. No -> ( 2s x.s t ) = ( t +s t ) ) : No typesetting found for |- ( t e. No -> ( 2s x.s t ) = ( t +s t ) ) with typecode |-
76	74 75	syl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( t +s t ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( t +s t ) ) with typecode |-
77	76	oveq1d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( ( t +s t ) +s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( ( t +s t ) +s 1s ) ) with typecode |-
78		1sno	$$⊢1_s\in \mathrm{No}$$
79	78	a1i	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. No ) with typecode |-
80	74 74 79	addsassd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s t ) +s 1s ) = ( t +s ( t +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s t ) +s 1s ) = ( t +s ( t +s 1s ) ) ) with typecode |-
81	77 80	eqtrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( t +s ( t +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( t +s ( t +s 1s ) ) ) with typecode |-
82	81	oveq1d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
83	74 79	addscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. No ) with typecode |-
84		simpll	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> n e. NN0_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> n e. NN0_s ) with typecode |-
85	74	sltp1d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t t
86		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
87		nnzs	Could not format ( 2s e. NN_s -> 2s e. ZZ_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. ZZ_s ) with typecode |-
88	86 87	mp1i	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. ZZ_s ) with typecode |-
89		simpr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> t e. ZZ_s ) with typecode |-
90	88 89	zmulscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. ZZ_s ) with typecode |-
91	90	znod	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) e. No ) with typecode |-
92		pncans	Could not format ( ( ( 2s x.s t ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) ) : No typesetting found for |- ( ( ( 2s x.s t ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) ) with typecode |-
93	91 78 92	sylancl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) -s 1s ) = ( 2s x.s t ) ) with typecode |-
94	93	eqcomd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( ( ( 2s x.s t ) +s 1s ) -s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s t ) = ( ( ( 2s x.s t ) +s 1s ) -s 1s ) ) with typecode |-
95	94	sneqd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s t ) } = { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s t ) } = { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } ) with typecode |-
96		mulsrid	Could not format ( 2s e. No -> ( 2s x.s 1s ) = 2s ) : No typesetting found for |- ( 2s e. No -> ( 2s x.s 1s ) = 2s ) with typecode |-
97	5 96	ax-mp	Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |-
98		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
99	97 98	eqtr4i	Could not format ( 2s x.s 1s ) = ( 1s +s 1s ) : No typesetting found for |- ( 2s x.s 1s ) = ( 1s +s 1s ) with typecode |-
100	99	oveq2i	Could not format ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) ) : No typesetting found for |- ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) ) with typecode |-
101	5	a1i	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 2s e. No ) with typecode |-
102	101 74 79	addsdid	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( 2s x.s t ) +s ( 2s x.s 1s ) ) ) with typecode |-
103	91 79 79	addsassd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) +s 1s ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) +s 1s ) = ( ( 2s x.s t ) +s ( 1s +s 1s ) ) ) with typecode |-
104	100 102 103	3eqtr4a	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( ( 2s x.s t ) +s 1s ) +s 1s ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s x.s ( t +s 1s ) ) = ( ( ( 2s x.s t ) +s 1s ) +s 1s ) ) with typecode |-
105	104	sneqd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s ( t +s 1s ) ) } = { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( 2s x.s ( t +s 1s ) ) } = { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) with typecode |-
106	95 105	oveq12d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) with typecode |-
107		1zs	$$⊢1_s\in {\mathbb{Z}}_s$$
108	107	a1i	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 1s e. ZZ_s ) with typecode |-
109	90 108	zaddscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) e. ZZ_s ) with typecode |-
110		zscut	Could not format ( ( ( 2s x.s t ) +s 1s ) e. ZZ_s -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) : No typesetting found for |- ( ( ( 2s x.s t ) +s 1s ) e. ZZ_s -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) with typecode |-
111	109 110	syl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s x.s t ) +s 1s ) = ( { ( ( ( 2s x.s t ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s t ) +s 1s ) +s 1s ) } ) ) with typecode |-
112	106 111 81	3eqtr2d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( t +s ( t +s 1s ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( 2s x.s t ) } |s { ( 2s x.s ( t +s 1s ) ) } ) = ( t +s ( t +s 1s ) ) ) with typecode |-
113	74 83 84 85 112	pw2cut	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( ( t +s ( t +s 1s ) ) /su ( 2s ^su ( n +s 1s ) ) ) ) with typecode |-
114	82 113	eqtr4d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) = ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
115	114	fveq2d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
116	49	ad2antrr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) e. No ) with typecode |-
117	53	ad2antrr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( 2s ^su n ) =/= 0s ) with typecode |-
118	74 116 117	divscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) e. No ) with typecode |-
119	83 116 117	divscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No ) with typecode |-
120	74 116 117	divscan2d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) = t ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) = t ) with typecode |-
121	120 85	eqbrtrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) )
122		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
123	86 122	ax-mp	Could not format 0s
124		expsgt0	Could not format ( ( 2s e. No /\ n e. NN0_s /\ 0s 0s 0s
125	5 123 124	mp3an13	Could not format ( n e. NN0_s -> 0s 0s
126	125	ad2antrr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> 0s 0s
127	118 83 116 126	sltmuldiv2d	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) ( t /su ( 2s ^su n ) ) ( ( ( 2s ^su n ) x.s ( t /su ( 2s ^su n ) ) ) ( t /su ( 2s ^su n ) )
128	121 127	mpbid	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t /su ( 2s ^su n ) ) ( t /su ( 2s ^su n ) )
129	118 119 128	ssltsn	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( t /su ( 2s ^su n ) ) } < { ( t /su ( 2s ^su n ) ) } <
130		imaundi	Could not format ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
131	130	unieqi	Could not format U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
132		uniun	Could not format U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- U. ( ( bday " { ( t /su ( 2s ^su n ) ) } ) u. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
133	131 132	eqtri	Could not format U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) = ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
134		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
135		fnsnfv	Could not format ( ( bday Fn No /\ ( t /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( bday Fn No /\ ( t /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) ) with typecode |-
136	134 118 135	sylancr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday " { ( t /su ( 2s ^su n ) ) } ) ) with typecode |-
137	136	unieqd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = U. ( bday " { ( t /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = U. ( bday " { ( t /su ( 2s ^su n ) ) } ) ) with typecode |-
138		fvex	Could not format ( bday ` ( t /su ( 2s ^su n ) ) ) e. _V : No typesetting found for |- ( bday ` ( t /su ( 2s ^su n ) ) ) e. _V with typecode |-
139	138	unisn	Could not format U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday ` ( t /su ( 2s ^su n ) ) ) : No typesetting found for |- U. { ( bday ` ( t /su ( 2s ^su n ) ) ) } = ( bday ` ( t /su ( 2s ^su n ) ) ) with typecode |-
140	137 139	eqtr3di	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) = ( bday ` ( t /su ( 2s ^su n ) ) ) ) with typecode |-
141	140 68	eqeltrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om ) with typecode |-
142		fnsnfv	Could not format ( ( bday Fn No /\ ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( bday Fn No /\ ( ( t +s 1s ) /su ( 2s ^su n ) ) e. No ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
143	134 119 142	sylancr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
144	143	unieqd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) with typecode |-
145		fvex	Could not format ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _V : No typesetting found for |- ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _V with typecode |-
146	145	unisn	Could not format U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) : No typesetting found for |- U. { ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) } = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) with typecode |-
147	144 146	eqtr3di	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) ) with typecode |-
148		fvoveq1	Could not format ( z = ( t +s 1s ) -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) ) : No typesetting found for |- ( z = ( t +s 1s ) -> ( bday ` ( z /su ( 2s ^su n ) ) ) = ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) ) with typecode |-
149	148	eleq1d	Could not format ( z = ( t +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om ) ) : No typesetting found for |- ( z = ( t +s 1s ) -> ( ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om <-> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om ) ) with typecode |-
150		simplr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
151	89 108	zaddscld	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. ZZ_s ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( t +s 1s ) e. ZZ_s ) with typecode |-
152	149 150 151	rspcdva	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( t +s 1s ) /su ( 2s ^su n ) ) ) e. _om ) with typecode |-
153	147 152	eqeltrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om ) with typecode |-
154		omun	Could not format ( ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om /\ U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) e. _om /\ U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) e. _om ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
155	141 153 154	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( U. ( bday " { ( t /su ( 2s ^su n ) ) } ) u. U. ( bday " { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
156	133 155	eqeltrid	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
157		peano2	Could not format ( U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
158	156 157	syl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
159		nnon	Could not format ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) : No typesetting found for |- ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) with typecode |-
160	158 159	syl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) with typecode |-
161		imassrn	Could not format ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ ran bday : No typesetting found for |- ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ ran bday with typecode |-
162		bdayrn	$$⊢\mathrm{ran}\mathrm{bday}=\mathrm{On}$$
163	161 162	sseqtri	Could not format ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On : No typesetting found for |- ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On with typecode |-
164		onsucuni	Could not format ( ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ On -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
165	163 164	mp1i	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
166		scutbdaybnd	Could not format ( ( { ( t /su ( 2s ^su n ) ) } < ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( { ( t /su ( 2s ^su n ) ) } < ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
167	129 160 165 166	syl3anc	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
168		bdayelon	Could not format ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On : No typesetting found for |- ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On with typecode |-
169		onsssuc	Could not format ( ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On /\ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On /\ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. On ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) with typecode |-
170	168 160 169	sylancr	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) C_ suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) <-> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) ) with typecode |-
171	167 170	mpbid	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( { ( t /su ( 2s ^su n ) ) } |s { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
172	115 171	eqeltrd	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) ) with typecode |-
173		peano2	Could not format ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
174	158 173	syl	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) with typecode |-
175		elnn	Could not format ( ( ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) /\ suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) /\ suc suc U. ( bday " ( { ( t /su ( 2s ^su n ) ) } u. { ( ( t +s 1s ) /su ( 2s ^su n ) ) } ) ) e. _om ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
176	172 174 175	syl2anc	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
177		fvoveq1	Could not format ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) : No typesetting found for |- ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) = ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) ) with typecode |-
178	177	eleq1d	Could not format ( w = ( ( 2s x.s t ) +s 1s ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( w = ( ( 2s x.s t ) +s 1s ) -> ( ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om <-> ( bday ` ( ( ( 2s x.s t ) +s 1s ) /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
179	176 178	syl5ibrcom	Could not format ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) /\ t e. ZZ_s ) -> ( w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
180	179	rexlimdva	Could not format ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
181	73 180	jaod	Could not format ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( ( E. t e. ZZ_s w = ( 2s x.s t ) \/ E. t e. ZZ_s w = ( ( 2s x.s t ) +s 1s ) ) -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
182	39 181	syl5	Could not format ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( w e. ZZ_s -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> ( w e. ZZ_s -> ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
183	182	ralrimiv	Could not format ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) : No typesetting found for |- ( ( n e. NN0_s /\ A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om ) -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) with typecode |-
184	183	ex	Could not format ( n e. NN0_s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) : No typesetting found for |- ( n e. NN0_s -> ( A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su n ) ) ) e. _om -> A. w e. ZZ_s ( bday ` ( w /su ( 2s ^su ( n +s 1s ) ) ) ) e. _om ) ) with typecode |-
185	12 17 26 31 38 184	n0sind	Could not format ( y e. NN0_s -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) : No typesetting found for |- ( y e. NN0_s -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) with typecode |-
186	185	adantl	Could not format ( ( x e. ZZ_s /\ y e. NN0_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) : No typesetting found for |- ( ( x e. ZZ_s /\ y e. NN0_s ) -> A. z e. ZZ_s ( bday ` ( z /su ( 2s ^su y ) ) ) e. _om ) with typecode |-
187		simpl	$$⊢\left(x\in {\mathbb{Z}}_s\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to x\in {\mathbb{Z}}_s$$
188	3 186 187	rspcdva	Could not format ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) : No typesetting found for |- ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) with typecode |-
189		fveq2	Could not format ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) = ( bday ` ( x /su ( 2s ^su y ) ) ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) = ( bday ` ( x /su ( 2s ^su y ) ) ) ) with typecode |-
190	189	eleq1d	Could not format ( A = ( x /su ( 2s ^su y ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) ) : No typesetting found for |- ( A = ( x /su ( 2s ^su y ) ) -> ( ( bday ` A ) e. _om <-> ( bday ` ( x /su ( 2s ^su y ) ) ) e. _om ) ) with typecode |-
191	188 190	syl5ibrcom	Could not format ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om ) ) : No typesetting found for |- ( ( x e. ZZ_s /\ y e. NN0_s ) -> ( A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om ) ) with typecode |-
192	191	rexlimivv	Could not format ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om ) : No typesetting found for |- ( E. x e. ZZ_s E. y e. NN0_s A = ( x /su ( 2s ^su y ) ) -> ( bday ` A ) e. _om ) with typecode |-
193	1 192	sylbi	Could not format ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) : No typesetting found for |- ( A e. ZZ_s[1/2] -> ( bday ` A ) e. _om ) with typecode |-