Metamath Proof Explorer

Theorem pw2cutp1

Description: Simplify pw2cut in the case of successors of surreal integers. (Contributed by Scott Fenton, 11-Nov-2025)

Ref Expression
Hypotheses pw2cutp1.1 
|- ( ph -> A e. ZZ_s )
pw2cutp1.3 
|- ( ph -> N e. NN0_s )
Assertion pw2cutp1 
|- ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) = ( ( ( 2s x.s A ) +s 1s ) /su ( 2s ^su ( N +s 1s ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2cutp1.1 
 |-  ( ph -> A e. ZZ_s )
2 pw2cutp1.3 
 |-  ( ph -> N e. NN0_s )
3 1 znod 
 |-  ( ph -> A e. No )
4 1zs 
 |-  1s e. ZZ_s
5 zaddscl 
 |-  ( ( A e. ZZ_s /\ 1s e. ZZ_s ) -> ( A +s 1s ) e. ZZ_s )
6 1 4 5 sylancl 
 |-  ( ph -> ( A +s 1s ) e. ZZ_s )
7 6 znod 
 |-  ( ph -> ( A +s 1s ) e. No )
8 3 sltp1d 
 |-  ( ph -> A
9 2nns 
 |-  2s e. NN_s
10 nnzs 
 |-  ( 2s e. NN_s -> 2s e. ZZ_s )
11 9 10 ax-mp 
 |-  2s e. ZZ_s
12 11 a1i 
 |-  ( ph -> 2s e. ZZ_s )
13 12 1 zmulscld 
 |-  ( ph -> ( 2s x.s A ) e. ZZ_s )
14 zaddscl 
 |-  ( ( ( 2s x.s A ) e. ZZ_s /\ 1s e. ZZ_s ) -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s )
15 13 4 14 sylancl 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s )
16 zscut 
 |-  ( ( ( 2s x.s A ) +s 1s ) e. ZZ_s -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } ) )
17 15 16 syl 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } ) )
18 no2times 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )
19 3 18 syl 
 |-  ( ph -> ( 2s x.s A ) = ( A +s A ) )
20 19 oveq1d 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) )
21 1sno 
 |-  1s e. No
22 21 a1i 
 |-  ( ph -> 1s e. No )
23 3 3 22 addsassd 
 |-  ( ph -> ( ( A +s A ) +s 1s ) = ( A +s ( A +s 1s ) ) )
24 20 23 eqtrd 
 |-  ( ph -> ( ( 2s x.s A ) +s 1s ) = ( A +s ( A +s 1s ) ) )
25 13 znod 
 |-  ( ph -> ( 2s x.s A ) e. No )
26 pncans 
 |-  ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) )
27 25 21 26 sylancl 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) )
28 27 sneqd 
 |-  ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } )
29 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
30 2sno 
 |-  2s e. No
31 mulsrid 
 |-  ( 2s e. No -> ( 2s x.s 1s ) = 2s )
32 30 31 ax-mp 
 |-  ( 2s x.s 1s ) = 2s
33 29 32 eqtr4i 
 |-  ( 1s +s 1s ) = ( 2s x.s 1s )
34 33 oveq2i 
 |-  ( ( 2s x.s A ) +s ( 1s +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) )
35 25 22 22 addsassd 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( ( 2s x.s A ) +s ( 1s +s 1s ) ) )
36 30 a1i 
 |-  ( ph -> 2s e. No )
37 36 3 22 addsdid 
 |-  ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) )
38 34 35 37 3eqtr4a 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( 2s x.s ( A +s 1s ) ) )
39 38 sneqd 
 |-  ( ph -> { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } = { ( 2s x.s ( A +s 1s ) ) } )
40 28 39 oveq12d 
 |-  ( ph -> ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } ) = ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) )
41 17 24 40 3eqtr3rd 
 |-  ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) )
42 3 7 2 8 41 pw2cut 
 |-  ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) = ( ( A +s ( A +s 1s ) ) /su ( 2s ^su ( N +s 1s ) ) ) )
43 24 oveq1d 
 |-  ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su ( 2s ^su ( N +s 1s ) ) ) = ( ( A +s ( A +s 1s ) ) /su ( 2s ^su ( N +s 1s ) ) ) )
44 42 43 eqtr4d 
 |-  ( ph -> ( { ( A /su ( 2s ^su N ) ) } |s { ( ( A +s 1s ) /su ( 2s ^su N ) ) } ) = ( ( ( 2s x.s A ) +s 1s ) /su ( 2s ^su ( N +s 1s ) ) ) )