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 Could not format assertion : No typesetting found for |- ( 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 ) ) ) with typecode |-

Proof

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