Metamath Proof Explorer

Theorem zscut

Description: A cut expression for surreal integers. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Assertion zscut 
|- ( A e. ZZ_s -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )

Proof

Step Hyp Ref Expression
1 elzn0s 
 |-  ( A e. ZZ_s <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )
2 n0scut 
 |-  ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) )
3 n0sno 
 |-  ( A e. NN0_s -> A e. No )
4 1sno 
 |-  1s e. No
5 4 a1i 
 |-  ( A e. NN0_s -> 1s e. No )
6 3 5 subscld 
 |-  ( A e. NN0_s -> ( A -s 1s ) e. No )
7 snelpwi 
 |-  ( ( A -s 1s ) e. No -> { ( A -s 1s ) } e. ~P No )
8 nulssgt 
 |-  ( { ( A -s 1s ) } e. ~P No -> { ( A -s 1s ) } <
9 6 7 8 3syl 
 |-  ( A e. NN0_s -> { ( A -s 1s ) } <
10 slerflex 
 |-  ( ( A -s 1s ) e. No -> ( A -s 1s ) <_s ( A -s 1s ) )
11 6 10 syl 
 |-  ( A e. NN0_s -> ( A -s 1s ) <_s ( A -s 1s ) )
12 ovex 
 |-  ( A -s 1s ) e. _V
13 breq1 
 |-  ( x = ( A -s 1s ) -> ( x <_s y <-> ( A -s 1s ) <_s y ) )
14 13 rexbidv 
 |-  ( x = ( A -s 1s ) -> ( E. y e. { ( A -s 1s ) } x <_s y <-> E. y e. { ( A -s 1s ) } ( A -s 1s ) <_s y ) )
15 12 14 ralsn 
 |-  ( A. x e. { ( A -s 1s ) } E. y e. { ( A -s 1s ) } x <_s y <-> E. y e. { ( A -s 1s ) } ( A -s 1s ) <_s y )
16 breq2 
 |-  ( y = ( A -s 1s ) -> ( ( A -s 1s ) <_s y <-> ( A -s 1s ) <_s ( A -s 1s ) ) )
17 12 16 rexsn 
 |-  ( E. y e. { ( A -s 1s ) } ( A -s 1s ) <_s y <-> ( A -s 1s ) <_s ( A -s 1s ) )
18 15 17 bitri 
 |-  ( A. x e. { ( A -s 1s ) } E. y e. { ( A -s 1s ) } x <_s y <-> ( A -s 1s ) <_s ( A -s 1s ) )
19 11 18 sylibr 
 |-  ( A e. NN0_s -> A. x e. { ( A -s 1s ) } E. y e. { ( A -s 1s ) } x <_s y )
20 ral0 
 |-  A. x e. (/) E. y e. { ( A +s 1s ) } y <_s x
21 20 a1i 
 |-  ( A e. NN0_s -> A. x e. (/) E. y e. { ( A +s 1s ) } y <_s x )
22 3 sltm1d 
 |-  ( A e. NN0_s -> ( A -s 1s )
23 6 3 22 ssltsn 
 |-  ( A e. NN0_s -> { ( A -s 1s ) } <
24 2 sneqd 
 |-  ( A e. NN0_s -> { A } = { ( { ( A -s 1s ) } |s (/) ) } )
25 23 24 breqtrd 
 |-  ( A e. NN0_s -> { ( A -s 1s ) } <
26 3 5 addscld 
 |-  ( A e. NN0_s -> ( A +s 1s ) e. No )
27 3 sltp1d 
 |-  ( A e. NN0_s -> A
28 3 26 27 ssltsn 
 |-  ( A e. NN0_s -> { A } <
29 24 28 eqbrtrrd 
 |-  ( A e. NN0_s -> { ( { ( A -s 1s ) } |s (/) ) } <
30 9 19 21 25 29 cofcut1d 
 |-  ( A e. NN0_s -> ( { ( A -s 1s ) } |s (/) ) = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
31 2 30 eqtrd 
 |-  ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
32 31 adantl 
 |-  ( ( A e. No /\ A e. NN0_s ) -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
33 negsfn 
 |-  -us Fn No
34 simpl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> A e. No )
35 4 a1i 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> 1s e. No )
36 34 35 addscld 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( A +s 1s ) e. No )
37 fnsnfv 
 |-  ( ( -us Fn No /\ ( A +s 1s ) e. No ) -> { ( -us ` ( A +s 1s ) ) } = ( -us " { ( A +s 1s ) } ) )
38 33 36 37 sylancr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> { ( -us ` ( A +s 1s ) ) } = ( -us " { ( A +s 1s ) } ) )
39 negsdi 
 |-  ( ( A e. No /\ 1s e. No ) -> ( -us ` ( A +s 1s ) ) = ( ( -us ` A ) +s ( -us ` 1s ) ) )
40 34 4 39 sylancl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` ( A +s 1s ) ) = ( ( -us ` A ) +s ( -us ` 1s ) ) )
41 n0sno 
 |-  ( ( -us ` A ) e. NN0_s -> ( -us ` A ) e. No )
42 41 adantl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` A ) e. No )
43 42 35 subsvald 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( ( -us ` A ) -s 1s ) = ( ( -us ` A ) +s ( -us ` 1s ) ) )
44 40 43 eqtr4d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` ( A +s 1s ) ) = ( ( -us ` A ) -s 1s ) )
45 44 sneqd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> { ( -us ` ( A +s 1s ) ) } = { ( ( -us ` A ) -s 1s ) } )
46 38 45 eqtr3d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us " { ( A +s 1s ) } ) = { ( ( -us ` A ) -s 1s ) } )
47 34 35 subscld 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( A -s 1s ) e. No )
48 fnsnfv 
 |-  ( ( -us Fn No /\ ( A -s 1s ) e. No ) -> { ( -us ` ( A -s 1s ) ) } = ( -us " { ( A -s 1s ) } ) )
49 33 47 48 sylancr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> { ( -us ` ( A -s 1s ) ) } = ( -us " { ( A -s 1s ) } ) )
50 35 34 subsvald 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( 1s -s A ) = ( 1s +s ( -us ` A ) ) )
51 34 35 negsubsdi2d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` ( A -s 1s ) ) = ( 1s -s A ) )
52 42 35 addscomd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( ( -us ` A ) +s 1s ) = ( 1s +s ( -us ` A ) ) )
53 50 51 52 3eqtr4d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` ( A -s 1s ) ) = ( ( -us ` A ) +s 1s ) )
54 53 sneqd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> { ( -us ` ( A -s 1s ) ) } = { ( ( -us ` A ) +s 1s ) } )
55 49 54 eqtr3d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us " { ( A -s 1s ) } ) = { ( ( -us ` A ) +s 1s ) } )
56 46 55 oveq12d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( ( -us " { ( A +s 1s ) } ) |s ( -us " { ( A -s 1s ) } ) ) = ( { ( ( -us ` A ) -s 1s ) } |s { ( ( -us ` A ) +s 1s ) } ) )
57 34 sltm1d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( A -s 1s )
58 34 sltp1d 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> A
59 47 34 36 57 58 slttrd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( A -s 1s )
60 47 36 59 ssltsn 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> { ( A -s 1s ) } <
61 eqidd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
62 60 61 negsunif 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) = ( ( -us " { ( A +s 1s ) } ) |s ( -us " { ( A -s 1s ) } ) ) )
63 n0scut 
 |-  ( ( -us ` A ) e. NN0_s -> ( -us ` A ) = ( { ( ( -us ` A ) -s 1s ) } |s (/) ) )
64 4 a1i 
 |-  ( ( -us ` A ) e. NN0_s -> 1s e. No )
65 41 64 subscld 
 |-  ( ( -us ` A ) e. NN0_s -> ( ( -us ` A ) -s 1s ) e. No )
66 snelpwi 
 |-  ( ( ( -us ` A ) -s 1s ) e. No -> { ( ( -us ` A ) -s 1s ) } e. ~P No )
67 nulssgt 
 |-  ( { ( ( -us ` A ) -s 1s ) } e. ~P No -> { ( ( -us ` A ) -s 1s ) } <
68 65 66 67 3syl 
 |-  ( ( -us ` A ) e. NN0_s -> { ( ( -us ` A ) -s 1s ) } <
69 slerflex 
 |-  ( ( ( -us ` A ) -s 1s ) e. No -> ( ( -us ` A ) -s 1s ) <_s ( ( -us ` A ) -s 1s ) )
70 65 69 syl 
 |-  ( ( -us ` A ) e. NN0_s -> ( ( -us ` A ) -s 1s ) <_s ( ( -us ` A ) -s 1s ) )
71 ovex 
 |-  ( ( -us ` A ) -s 1s ) e. _V
72 breq1 
 |-  ( x = ( ( -us ` A ) -s 1s ) -> ( x <_s y <-> ( ( -us ` A ) -s 1s ) <_s y ) )
73 72 rexbidv 
 |-  ( x = ( ( -us ` A ) -s 1s ) -> ( E. y e. { ( ( -us ` A ) -s 1s ) } x <_s y <-> E. y e. { ( ( -us ` A ) -s 1s ) } ( ( -us ` A ) -s 1s ) <_s y ) )
74 71 73 ralsn 
 |-  ( A. x e. { ( ( -us ` A ) -s 1s ) } E. y e. { ( ( -us ` A ) -s 1s ) } x <_s y <-> E. y e. { ( ( -us ` A ) -s 1s ) } ( ( -us ` A ) -s 1s ) <_s y )
75 breq2 
 |-  ( y = ( ( -us ` A ) -s 1s ) -> ( ( ( -us ` A ) -s 1s ) <_s y <-> ( ( -us ` A ) -s 1s ) <_s ( ( -us ` A ) -s 1s ) ) )
76 71 75 rexsn 
 |-  ( E. y e. { ( ( -us ` A ) -s 1s ) } ( ( -us ` A ) -s 1s ) <_s y <-> ( ( -us ` A ) -s 1s ) <_s ( ( -us ` A ) -s 1s ) )
77 74 76 bitri 
 |-  ( A. x e. { ( ( -us ` A ) -s 1s ) } E. y e. { ( ( -us ` A ) -s 1s ) } x <_s y <-> ( ( -us ` A ) -s 1s ) <_s ( ( -us ` A ) -s 1s ) )
78 70 77 sylibr 
 |-  ( ( -us ` A ) e. NN0_s -> A. x e. { ( ( -us ` A ) -s 1s ) } E. y e. { ( ( -us ` A ) -s 1s ) } x <_s y )
79 ral0 
 |-  A. x e. (/) E. y e. { ( ( -us ` A ) +s 1s ) } y <_s x
80 79 a1i 
 |-  ( ( -us ` A ) e. NN0_s -> A. x e. (/) E. y e. { ( ( -us ` A ) +s 1s ) } y <_s x )
81 41 sltm1d 
 |-  ( ( -us ` A ) e. NN0_s -> ( ( -us ` A ) -s 1s )
82 65 41 81 ssltsn 
 |-  ( ( -us ` A ) e. NN0_s -> { ( ( -us ` A ) -s 1s ) } <
83 63 sneqd 
 |-  ( ( -us ` A ) e. NN0_s -> { ( -us ` A ) } = { ( { ( ( -us ` A ) -s 1s ) } |s (/) ) } )
84 82 83 breqtrd 
 |-  ( ( -us ` A ) e. NN0_s -> { ( ( -us ` A ) -s 1s ) } <
85 41 64 addscld 
 |-  ( ( -us ` A ) e. NN0_s -> ( ( -us ` A ) +s 1s ) e. No )
86 41 sltp1d 
 |-  ( ( -us ` A ) e. NN0_s -> ( -us ` A )
87 41 85 86 ssltsn 
 |-  ( ( -us ` A ) e. NN0_s -> { ( -us ` A ) } <
88 83 87 eqbrtrrd 
 |-  ( ( -us ` A ) e. NN0_s -> { ( { ( ( -us ` A ) -s 1s ) } |s (/) ) } <
89 68 78 80 84 88 cofcut1d 
 |-  ( ( -us ` A ) e. NN0_s -> ( { ( ( -us ` A ) -s 1s ) } |s (/) ) = ( { ( ( -us ` A ) -s 1s ) } |s { ( ( -us ` A ) +s 1s ) } ) )
90 63 89 eqtrd 
 |-  ( ( -us ` A ) e. NN0_s -> ( -us ` A ) = ( { ( ( -us ` A ) -s 1s ) } |s { ( ( -us ` A ) +s 1s ) } ) )
91 90 adantl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` A ) = ( { ( ( -us ` A ) -s 1s ) } |s { ( ( -us ` A ) +s 1s ) } ) )
92 56 62 91 3eqtr4rd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( -us ` A ) = ( -us ` ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) )
93 60 scutcld 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) e. No )
94 negs11 
 |-  ( ( A e. No /\ ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) e. No ) -> ( ( -us ` A ) = ( -us ` ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) <-> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) )
95 93 94 syldan 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( ( -us ` A ) = ( -us ` ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) <-> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) ) )
96 92 95 mpbid 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
97 32 96 jaodan 
 |-  ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )
98 1 97 sylbi 
 |-  ( A e. ZZ_s -> A = ( { ( A -s 1s ) } |s { ( A +s 1s ) } ) )