Metamath Proof Explorer

Theorem n0seo

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

Ref Expression
Assertion n0seo 
|- ( N e. NN0_s -> ( E. x e. NN0_s N = ( 2s x.s x ) \/ E. x e. NN0_s N = ( ( 2s x.s x ) +s 1s ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( m = 0s -> ( m = ( 2s x.s x ) <-> 0s = ( 2s x.s x ) ) )
2 1 rexbidv 
 |-  ( m = 0s -> ( E. x e. NN0_s m = ( 2s x.s x ) <-> E. x e. NN0_s 0s = ( 2s x.s x ) ) )
3 eqeq1 
 |-  ( m = 0s -> ( m = ( ( 2s x.s x ) +s 1s ) <-> 0s = ( ( 2s x.s x ) +s 1s ) ) )
4 3 rexbidv 
 |-  ( m = 0s -> ( E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) <-> E. x e. NN0_s 0s = ( ( 2s x.s x ) +s 1s ) ) )
5 2 4 orbi12d 
 |-  ( m = 0s -> ( ( E. x e. NN0_s m = ( 2s x.s x ) \/ E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. NN0_s 0s = ( 2s x.s x ) \/ E. x e. NN0_s 0s = ( ( 2s x.s x ) +s 1s ) ) ) )
6 eqeq1 
 |-  ( m = n -> ( m = ( 2s x.s x ) <-> n = ( 2s x.s x ) ) )
7 6 rexbidv 
 |-  ( m = n -> ( E. x e. NN0_s m = ( 2s x.s x ) <-> E. x e. NN0_s n = ( 2s x.s x ) ) )
8 eqeq1 
 |-  ( m = n -> ( m = ( ( 2s x.s x ) +s 1s ) <-> n = ( ( 2s x.s x ) +s 1s ) ) )
9 8 rexbidv 
 |-  ( m = n -> ( E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) <-> E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) ) )
10 7 9 orbi12d 
 |-  ( m = n -> ( ( E. x e. NN0_s m = ( 2s x.s x ) \/ E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. NN0_s n = ( 2s x.s x ) \/ E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) ) ) )
11 eqeq1 
 |-  ( m = ( n +s 1s ) -> ( m = ( 2s x.s x ) <-> ( n +s 1s ) = ( 2s x.s x ) ) )
12 11 rexbidv 
 |-  ( m = ( n +s 1s ) -> ( E. x e. NN0_s m = ( 2s x.s x ) <-> E. x e. NN0_s ( n +s 1s ) = ( 2s x.s x ) ) )
13 oveq2 
 |-  ( x = y -> ( 2s x.s x ) = ( 2s x.s y ) )
14 13 eqeq2d 
 |-  ( x = y -> ( ( n +s 1s ) = ( 2s x.s x ) <-> ( n +s 1s ) = ( 2s x.s y ) ) )
15 14 cbvrexvw 
 |-  ( E. x e. NN0_s ( n +s 1s ) = ( 2s x.s x ) <-> E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) )
16 12 15 bitrdi 
 |-  ( m = ( n +s 1s ) -> ( E. x e. NN0_s m = ( 2s x.s x ) <-> E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) ) )
17 eqeq1 
 |-  ( m = ( n +s 1s ) -> ( m = ( ( 2s x.s x ) +s 1s ) <-> ( n +s 1s ) = ( ( 2s x.s x ) +s 1s ) ) )
18 17 rexbidv 
 |-  ( m = ( n +s 1s ) -> ( E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) <-> E. x e. NN0_s ( n +s 1s ) = ( ( 2s x.s x ) +s 1s ) ) )
19 13 oveq1d 
 |-  ( x = y -> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s y ) +s 1s ) )
20 19 eqeq2d 
 |-  ( x = y -> ( ( n +s 1s ) = ( ( 2s x.s x ) +s 1s ) <-> ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
21 20 cbvrexvw 
 |-  ( E. x e. NN0_s ( n +s 1s ) = ( ( 2s x.s x ) +s 1s ) <-> E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) )
22 18 21 bitrdi 
 |-  ( m = ( n +s 1s ) -> ( E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) <-> E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
23 16 22 orbi12d 
 |-  ( m = ( n +s 1s ) -> ( ( E. x e. NN0_s m = ( 2s x.s x ) \/ E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) \/ E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) ) )
24 eqeq1 
 |-  ( m = N -> ( m = ( 2s x.s x ) <-> N = ( 2s x.s x ) ) )
25 24 rexbidv 
 |-  ( m = N -> ( E. x e. NN0_s m = ( 2s x.s x ) <-> E. x e. NN0_s N = ( 2s x.s x ) ) )
26 eqeq1 
 |-  ( m = N -> ( m = ( ( 2s x.s x ) +s 1s ) <-> N = ( ( 2s x.s x ) +s 1s ) ) )
27 26 rexbidv 
 |-  ( m = N -> ( E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) <-> E. x e. NN0_s N = ( ( 2s x.s x ) +s 1s ) ) )
28 25 27 orbi12d 
 |-  ( m = N -> ( ( E. x e. NN0_s m = ( 2s x.s x ) \/ E. x e. NN0_s m = ( ( 2s x.s x ) +s 1s ) ) <-> ( E. x e. NN0_s N = ( 2s x.s x ) \/ E. x e. NN0_s N = ( ( 2s x.s x ) +s 1s ) ) ) )
29 0n0s 
 |-  0s e. NN0_s
30 2sno 
 |-  2s e. No
31 muls01 
 |-  ( 2s e. No -> ( 2s x.s 0s ) = 0s )
32 30 31 ax-mp 
 |-  ( 2s x.s 0s ) = 0s
33 32 eqcomi 
 |-  0s = ( 2s x.s 0s )
34 oveq2 
 |-  ( x = 0s -> ( 2s x.s x ) = ( 2s x.s 0s ) )
35 34 rspceeqv 
 |-  ( ( 0s e. NN0_s /\ 0s = ( 2s x.s 0s ) ) -> E. x e. NN0_s 0s = ( 2s x.s x ) )
36 29 33 35 mp2an 
 |-  E. x e. NN0_s 0s = ( 2s x.s x )
37 36 orci 
 |-  ( E. x e. NN0_s 0s = ( 2s x.s x ) \/ E. x e. NN0_s 0s = ( ( 2s x.s x ) +s 1s ) )
38 eqid 
 |-  ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s x ) +s 1s )
39 oveq2 
 |-  ( y = x -> ( 2s x.s y ) = ( 2s x.s x ) )
40 39 oveq1d 
 |-  ( y = x -> ( ( 2s x.s y ) +s 1s ) = ( ( 2s x.s x ) +s 1s ) )
41 40 rspceeqv 
 |-  ( ( x e. NN0_s /\ ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s x ) +s 1s ) ) -> E. y e. NN0_s ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s y ) +s 1s ) )
42 38 41 mpan2 
 |-  ( x e. NN0_s -> E. y e. NN0_s ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s y ) +s 1s ) )
43 oveq1 
 |-  ( n = ( 2s x.s x ) -> ( n +s 1s ) = ( ( 2s x.s x ) +s 1s ) )
44 43 eqeq1d 
 |-  ( n = ( 2s x.s x ) -> ( ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) <-> ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
45 44 rexbidv 
 |-  ( n = ( 2s x.s x ) -> ( E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) <-> E. y e. NN0_s ( ( 2s x.s x ) +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
46 42 45 syl5ibrcom 
 |-  ( x e. NN0_s -> ( n = ( 2s x.s x ) -> E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
47 46 rexlimiv 
 |-  ( E. x e. NN0_s n = ( 2s x.s x ) -> E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) )
48 peano2n0s 
 |-  ( x e. NN0_s -> ( x +s 1s ) e. NN0_s )
49 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
50 mulsrid 
 |-  ( 2s e. No -> ( 2s x.s 1s ) = 2s )
51 30 50 ax-mp 
 |-  ( 2s x.s 1s ) = 2s
52 49 51 eqtr4i 
 |-  ( 1s +s 1s ) = ( 2s x.s 1s )
53 52 oveq2i 
 |-  ( ( 2s x.s x ) +s ( 1s +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) )
54 30 a1i 
 |-  ( x e. NN0_s -> 2s e. No )
55 n0sno 
 |-  ( x e. NN0_s -> x e. No )
56 54 55 mulscld 
 |-  ( x e. NN0_s -> ( 2s x.s x ) e. No )
57 1sno 
 |-  1s e. No
58 57 a1i 
 |-  ( x e. NN0_s -> 1s e. No )
59 56 58 58 addsassd 
 |-  ( x e. NN0_s -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( ( 2s x.s x ) +s ( 1s +s 1s ) ) )
60 54 55 58 addsdid 
 |-  ( x e. NN0_s -> ( 2s x.s ( x +s 1s ) ) = ( ( 2s x.s x ) +s ( 2s x.s 1s ) ) )
61 53 59 60 3eqtr4a 
 |-  ( x e. NN0_s -> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s ( x +s 1s ) ) )
62 oveq2 
 |-  ( y = ( x +s 1s ) -> ( 2s x.s y ) = ( 2s x.s ( x +s 1s ) ) )
63 62 rspceeqv 
 |-  ( ( ( x +s 1s ) e. NN0_s /\ ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s ( x +s 1s ) ) ) -> E. y e. NN0_s ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s y ) )
64 48 61 63 syl2anc 
 |-  ( x e. NN0_s -> E. y e. NN0_s ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s y ) )
65 oveq1 
 |-  ( n = ( ( 2s x.s x ) +s 1s ) -> ( n +s 1s ) = ( ( ( 2s x.s x ) +s 1s ) +s 1s ) )
66 65 eqeq1d 
 |-  ( n = ( ( 2s x.s x ) +s 1s ) -> ( ( n +s 1s ) = ( 2s x.s y ) <-> ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s y ) ) )
67 66 rexbidv 
 |-  ( n = ( ( 2s x.s x ) +s 1s ) -> ( E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) <-> E. y e. NN0_s ( ( ( 2s x.s x ) +s 1s ) +s 1s ) = ( 2s x.s y ) ) )
68 64 67 syl5ibrcom 
 |-  ( x e. NN0_s -> ( n = ( ( 2s x.s x ) +s 1s ) -> E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) ) )
69 68 rexlimiv 
 |-  ( E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) -> E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) )
70 47 69 orim12i 
 |-  ( ( E. x e. NN0_s n = ( 2s x.s x ) \/ E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) ) -> ( E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) \/ E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) ) )
71 70 orcomd 
 |-  ( ( E. x e. NN0_s n = ( 2s x.s x ) \/ E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) ) -> ( E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) \/ E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) )
72 71 a1i 
 |-  ( n e. NN0_s -> ( ( E. x e. NN0_s n = ( 2s x.s x ) \/ E. x e. NN0_s n = ( ( 2s x.s x ) +s 1s ) ) -> ( E. y e. NN0_s ( n +s 1s ) = ( 2s x.s y ) \/ E. y e. NN0_s ( n +s 1s ) = ( ( 2s x.s y ) +s 1s ) ) ) )
73 5 10 23 28 37 72 n0sind 
 |-  ( N e. NN0_s -> ( E. x e. NN0_s N = ( 2s x.s x ) \/ E. x e. NN0_s N = ( ( 2s x.s x ) +s 1s ) ) )