Theorem zseo

Description: A surreal integer is either even or odd. (Contributed by Scott Fenton, 19-Aug-2025)

	Ref	Expression
Assertion	zseo	Could not format assertion : No typesetting found for |- ( N e. ZZ_s -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elzs	$$⊢N\in {\mathbb{Z}}_s\leftrightarrow \exists y\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_{s}N=y{-}_{s}z$$
2		nnn0s	$$⊢y\in {\mathbb{N}}_s\to y\in {\mathbb{N}}_{\mathrm{0s}}$$
3		n0seo	Could not format ( y e. NN0_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) : No typesetting found for |- ( y e. NN0_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) with typecode |-
4	2 3	syl	Could not format ( y e. NN_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) : No typesetting found for |- ( y e. NN_s -> ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) ) with typecode |-
5		nnn0s	$$⊢z\in {\mathbb{N}}_s\to z\in {\mathbb{N}}_{\mathrm{0s}}$$
6		n0seo	Could not format ( z e. NN0_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( z e. NN0_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
7	5 6	syl	Could not format ( z e. NN_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( z e. NN_s -> ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
8		reeanv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) with typecode |-
9		n0zs	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w\in {\mathbb{Z}}_s$$
10	9	adantr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to w\in {\mathbb{Z}}_s$$
11		n0zs	$$⊢t\in {\mathbb{N}}_{\mathrm{0s}}\to t\in {\mathbb{Z}}_s$$
12	11	adantl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to t\in {\mathbb{Z}}_s$$
13	10 12	zsubscld	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to w{-}_{s}t\in {\mathbb{Z}}_s$$
14		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
15	14	a1i	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> 2s e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> 2s e. No ) with typecode |-
16		n0sno	$$⊢w\in {\mathbb{N}}_{\mathrm{0s}}\to w\in \mathrm{No}$$
17	16	adantr	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to w\in \mathrm{No}$$
18		n0sno	$$⊢t\in {\mathbb{N}}_{\mathrm{0s}}\to t\in \mathrm{No}$$
19	18	adantl	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to t\in \mathrm{No}$$
20	15 17 19	subsdid	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |-
21	20	eqcomd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |-
22		oveq2	Could not format ( x = ( w -s t ) -> ( 2s x.s x ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( x = ( w -s t ) -> ( 2s x.s x ) = ( 2s x.s ( w -s t ) ) ) with typecode |-
23	22	rspceeqv	Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) with typecode |-
24	13 21 23	syl2anc	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) with typecode |-
25		oveq12	Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |-
26	25	eqeq1d	Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) with typecode |-
27	26	rexbidv	Could not format ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( 2s x.s t ) ) = ( 2s x.s x ) ) ) with typecode |-
28	24 27	syl5ibrcom	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |-
29	28	rexlimivv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |-
30	8 29	sylbir	Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |-
31	30	orcd	Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
32		reeanv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) ) with typecode |-
33	15 17	mulscld	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s w ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s w ) e. No ) with typecode |-
34		1sno	$$⊢1_s\in \mathrm{No}$$
35	34	a1i	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in \mathrm{No}$$
36	15 19	mulscld	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s t ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s t ) e. No ) with typecode |-
37	33 35 36	addsubsd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) ) with typecode |-
38	21	oveq1d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |-
39	37 38	eqtrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |-
40	22	oveq1d	Could not format ( x = ( w -s t ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) : No typesetting found for |- ( x = ( w -s t ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) with typecode |-
41	40	rspceeqv	Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s ( w -s t ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
42	13 39 41	syl2anc	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
43		oveq12	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) ) with typecode |-
44	43	eqeq1d	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
45	44	rexbidv	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( 2s x.s t ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
46	42 45	syl5ibrcom	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
47	46	rexlimivv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
48	32 47	sylbir	Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
49	48	olcd	Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( 2s x.s t ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
50		reeanv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
51		1zs	$$⊢1_s\in {\mathbb{Z}}_s$$
52	51	a1i	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in {\mathbb{Z}}_s$$
53	13 52	zsubscld	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(w{-}_{s}t\right){-}_s{1}_s\in {\mathbb{Z}}_s$$
54	13	znod	$$⊢\left(w\in {\mathbb{N}}_{\mathrm{0s}}\wedge t\in {\mathbb{N}}_{\mathrm{0s}}\right)\to w{-}_{s}t\in \mathrm{No}$$
55	15 54 35	subsdid	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( ( w -s t ) -s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( ( w -s t ) -s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) ) with typecode |-
56	55	oveq1d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) ) with typecode |-
57		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 |-
58	14 57	ax-mp	Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |-
59	58	oveq2i	Could not format ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s 2s ) : No typesetting found for |- ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) = ( ( 2s x.s ( w -s t ) ) -s 2s ) with typecode |-
60	59	oveq1i	Could not format ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) : No typesetting found for |- ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) with typecode |-
61	15 54	mulscld	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( 2s x.s ( w -s t ) ) e. No ) with typecode |-
62	61 35 15	addsubsd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) ) with typecode |-
63	61 35 15	addsubsassd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) +s 1s ) -s 2s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |-
64	62 63	eqtr3d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s 2s ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |-
65	60 64	eqtrid	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s ( w -s t ) ) -s ( 2s x.s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |-
66	56 65	eqtrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) ) with typecode |-
67		subscl	Could not format ( ( 1s e. No /\ 2s e. No ) -> ( 1s -s 2s ) e. No ) : No typesetting found for |- ( ( 1s e. No /\ 2s e. No ) -> ( 1s -s 2s ) e. No ) with typecode |-
68	34 14 67	mp2an	Could not format ( 1s -s 2s ) e. No : No typesetting found for |- ( 1s -s 2s ) e. No with typecode |-
69		negnegs	Could not format ( ( 1s -s 2s ) e. No -> ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) ) : No typesetting found for |- ( ( 1s -s 2s ) e. No -> ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) ) with typecode |-
70	68 69	ax-mp	Could not format ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) : No typesetting found for |- ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( 1s -s 2s ) with typecode |-
71	34	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
72	14	a1i	Could not format ( T. -> 2s e. No ) : No typesetting found for |- ( T. -> 2s e. No ) with typecode |-
73	71 72	negsubsdi2d	Could not format ( T. -> ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) ) : No typesetting found for |- ( T. -> ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) ) with typecode |-
74	73	mptru	Could not format ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) : No typesetting found for |- ( -us ` ( 1s -s 2s ) ) = ( 2s -s 1s ) with typecode |-
75		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
76		subadds	Could not format ( ( 2s e. No /\ 1s e. No /\ 1s e. No ) -> ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) ) : No typesetting found for |- ( ( 2s e. No /\ 1s e. No /\ 1s e. No ) -> ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) ) with typecode |-
77	14 34 34 76	mp3an	Could not format ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) : No typesetting found for |- ( ( 2s -s 1s ) = 1s <-> ( 1s +s 1s ) = 2s ) with typecode |-
78	75 77	mpbir	Could not format ( 2s -s 1s ) = 1s : No typesetting found for |- ( 2s -s 1s ) = 1s with typecode |-
79	74 78	eqtri	Could not format ( -us ` ( 1s -s 2s ) ) = 1s : No typesetting found for |- ( -us ` ( 1s -s 2s ) ) = 1s with typecode |-
80	79	fveq2i	Could not format ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( -us ` 1s ) : No typesetting found for |- ( -us ` ( -us ` ( 1s -s 2s ) ) ) = ( -us ` 1s ) with typecode |-
81	70 80	eqtr3i	Could not format ( 1s -s 2s ) = ( -us ` 1s ) : No typesetting found for |- ( 1s -s 2s ) = ( -us ` 1s ) with typecode |-
82	81	oveq2i	Could not format ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) : No typesetting found for |- ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) with typecode |-
83	61 35	subsvald	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( 2s x.s ( w -s t ) ) +s ( -us ` 1s ) ) ) with typecode |-
84	82 83	eqtr4id	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( 2s x.s ( w -s t ) ) -s 1s ) ) with typecode |-
85	20	oveq1d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) -s 1s ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) with typecode |-
86	84 85	eqtrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s ( w -s t ) ) +s ( 1s -s 2s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) ) with typecode |-
87	33 36 35	subsubs4d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) -s 1s ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
88	66 86 87	3eqtrrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) with typecode |-
89		oveq2	Could not format ( x = ( ( w -s t ) -s 1s ) -> ( 2s x.s x ) = ( 2s x.s ( ( w -s t ) -s 1s ) ) ) : No typesetting found for |- ( x = ( ( w -s t ) -s 1s ) -> ( 2s x.s x ) = ( 2s x.s ( ( w -s t ) -s 1s ) ) ) with typecode |-
90	89	oveq1d	Could not format ( x = ( ( w -s t ) -s 1s ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) : No typesetting found for |- ( x = ( ( w -s t ) -s 1s ) -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) with typecode |-
91	90	rspceeqv	Could not format ( ( ( ( w -s t ) -s 1s ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( ( ( w -s t ) -s 1s ) e. ZZ_s /\ ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s ( ( w -s t ) -s 1s ) ) +s 1s ) ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
92	53 88 91	syl2anc	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
93		oveq12	Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
94	93	eqeq1d	Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
95	94	rexbidv	Could not format ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( ( 2s x.s w ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
96	92 95	syl5ibrcom	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
97	96	rexlimivv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( 2s x.s w ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
98	50 97	sylbir	Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) with typecode |-
99	98	olcd	Could not format ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( 2s x.s w ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
100		reeanv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) <-> ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
101	33 35 36 35	addsubs4d	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) ) with typecode |-
102		subsid	$$⊢1_s\in \mathrm{No}\to 1_s{-}_s{1}_s=0_s$$
103	34 102	ax-mp	$$⊢1_s{-}_s{1}_s=0_s$$
104	103	oveq2i	Could not format ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) : No typesetting found for |- ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) with typecode |-
105	33 36	subscld	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) e. No ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( 2s x.s w ) -s ( 2s x.s t ) ) e. No ) with typecode |-
106	105	addsridd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( ( 2s x.s w ) -s ( 2s x.s t ) ) ) with typecode |-
107	106 21	eqtrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s 0s ) = ( 2s x.s ( w -s t ) ) ) with typecode |-
108	104 107	eqtrid	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) -s ( 2s x.s t ) ) +s ( 1s -s 1s ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |-
109	101 108	eqtrd	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) with typecode |-
110	22	rspceeqv	Could not format ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( ( w -s t ) e. ZZ_s /\ ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s ( w -s t ) ) ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) with typecode |-
111	13 109 110	syl2anc	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) with typecode |-
112		oveq12	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( y -s z ) = ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) ) with typecode |-
113	112	eqeq1d	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( ( y -s z ) = ( 2s x.s x ) <-> ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) with typecode |-
114	113	rexbidv	Could not format ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) <-> E. x e. ZZ_s ( ( ( 2s x.s w ) +s 1s ) -s ( ( 2s x.s t ) +s 1s ) ) = ( 2s x.s x ) ) ) with typecode |-
115	111 114	syl5ibrcom	Could not format ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( ( w e. NN0_s /\ t e. NN0_s ) -> ( ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |-
116	115	rexlimivv	Could not format ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( E. w e. NN0_s E. t e. NN0_s ( y = ( ( 2s x.s w ) +s 1s ) /\ z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |-
117	100 116	sylbir	Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) with typecode |-
118	117	orcd	Could not format ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) /\ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
119	31 49 99 118	ccase	Could not format ( ( ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) /\ ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( ( E. w e. NN0_s y = ( 2s x.s w ) \/ E. w e. NN0_s y = ( ( 2s x.s w ) +s 1s ) ) /\ ( E. t e. NN0_s z = ( 2s x.s t ) \/ E. t e. NN0_s z = ( ( 2s x.s t ) +s 1s ) ) ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
120	4 7 119	syl2an	Could not format ( ( y e. NN_s /\ z e. NN_s ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( ( y e. NN_s /\ z e. NN_s ) -> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
121		eqeq1	Could not format ( N = ( y -s z ) -> ( N = ( 2s x.s x ) <-> ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( N = ( 2s x.s x ) <-> ( y -s z ) = ( 2s x.s x ) ) ) with typecode |-
122	121	rexbidv	Could not format ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) <-> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) <-> E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) ) ) with typecode |-
123		eqeq1	Could not format ( N = ( y -s z ) -> ( N = ( ( 2s x.s x ) +s 1s ) <-> ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( N = ( ( 2s x.s x ) +s 1s ) <-> ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
124	123	rexbidv	Could not format ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) <-> E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
125	122 124	orbi12d	Could not format ( N = ( y -s z ) -> ( ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) ) : No typesetting found for |- ( N = ( y -s z ) -> ( ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. ZZ_s ( y -s z ) = ( 2s x.s x ) \/ E. x e. ZZ_s ( y -s z ) = ( ( 2s x.s x ) +s 1s ) ) ) ) with typecode |-
126	120 125	syl5ibrcom	Could not format ( ( y e. NN_s /\ z e. NN_s ) -> ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) ) : No typesetting found for |- ( ( y e. NN_s /\ z e. NN_s ) -> ( N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) ) with typecode |-
127	126	rexlimivv	Could not format ( E. y e. NN_s E. z e. NN_s N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( E. y e. NN_s E. z e. NN_s N = ( y -s z ) -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-
128	1 127	sylbi	Could not format ( N e. ZZ_s -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) : No typesetting found for |- ( N e. ZZ_s -> ( E. x e. ZZ_s N = ( 2s x.s x ) \/ E. x e. ZZ_s N = ( ( 2s x.s x ) +s 1s ) ) ) with typecode |-