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 
|- ( 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 ) ) )

Proof

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