Metamath Proof Explorer


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 s y s z s N = y - s z
2 nnn0s y s y 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 s z 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 0s w s
10 9 adantr w 0s t 0s w s
11 n0zs t 0s t s
12 11 adantl w 0s t 0s t s
13 10 12 zsubscld w 0s t 0s w - s t 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 0s w No
17 16 adantr w 0s t 0s w No
18 n0sno t 0s t No
19 18 adantl w 0s t 0s t 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 No
35 34 a1i w 0s t 0s 1 s 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 s
52 51 a1i w 0s t 0s 1 s s
53 13 52 zsubscld w 0s t 0s w - s t - s 1 s s
54 13 znod w 0s t 0s w - s t 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 1 s 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 No 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 |-