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	$$⊢\phi \to A\in {\mathbb{Z}}_s$$
	pw2cutp1.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
Assertion	pw2cutp1	Could not format assertion : No typesetting found for |- ( 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 ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		pw2cutp1.1	$$⊢\phi \to A\in {\mathbb{Z}}_s$$
2		pw2cutp1.3	$$⊢\phi \to N\in {\mathbb{N}}_{\mathrm{0s}}$$
3	1	znod	$$⊢\phi \to A\in \mathrm{No}$$
4		1zs	$$⊢1_s\in {\mathbb{Z}}_s$$
5		zaddscl	$$⊢\left(A\in {\mathbb{Z}}_s\wedge 1_s\in {\mathbb{Z}}_s\right)\to A{+}_s{1}_s\in {\mathbb{Z}}_s$$
6	1 4 5	sylancl	$$⊢\phi \to A{+}_s{1}_s\in {\mathbb{Z}}_s$$
7	6	znod	$$⊢\phi \to A{+}_s{1}_s\in \mathrm{No}$$
8	3	sltp1d	$$⊢\phi \to A{<}_s\left(A{+}_s{1}_s\right)$$
9		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
10		nnzs	Could not format ( 2s e. NN_s -> 2s e. ZZ_s ) : No typesetting found for |- ( 2s e. NN_s -> 2s e. ZZ_s ) with typecode |-
11	9 10	ax-mp	Could not format 2s e. ZZ_s : No typesetting found for |- 2s e. ZZ_s with typecode |-
12	11	a1i	Could not format ( ph -> 2s e. ZZ_s ) : No typesetting found for |- ( ph -> 2s e. ZZ_s ) with typecode |-
13	12 1	zmulscld	Could not format ( ph -> ( 2s x.s A ) e. ZZ_s ) : No typesetting found for |- ( ph -> ( 2s x.s A ) e. ZZ_s ) with typecode |-
14		zaddscl	Could not format ( ( ( 2s x.s A ) e. ZZ_s /\ 1s e. ZZ_s ) -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s ) : No typesetting found for |- ( ( ( 2s x.s A ) e. ZZ_s /\ 1s e. ZZ_s ) -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s ) with typecode |-
15	13 4 14	sylancl	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) e. ZZ_s ) with typecode |-
16		zscut	Could not format ( ( ( 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 ) } ) ) : No typesetting found for |- ( ( ( 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 ) } ) ) with typecode |-
17	15 16	syl	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } |s { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } ) ) with typecode |-
18		no2times	Could not format ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( A e. No -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
19	3 18	syl	Could not format ( ph -> ( 2s x.s A ) = ( A +s A ) ) : No typesetting found for |- ( ph -> ( 2s x.s A ) = ( A +s A ) ) with typecode |-
20	19	oveq1d	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( ( A +s A ) +s 1s ) ) with typecode |-
21		1sno	$$⊢1_s\in \mathrm{No}$$
22	21	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
23	3 3 22	addsassd	$$⊢\phi \to \left(A{+}_{s}A\right){+}_s{1}_s=A{+}_s\left(A{+}_s{1}_s\right)$$
24	20 23	eqtrd	Could not format ( ph -> ( ( 2s x.s A ) +s 1s ) = ( A +s ( A +s 1s ) ) ) : No typesetting found for |- ( ph -> ( ( 2s x.s A ) +s 1s ) = ( A +s ( A +s 1s ) ) ) with typecode |-
25	13	znod	Could not format ( ph -> ( 2s x.s A ) e. No ) : No typesetting found for |- ( ph -> ( 2s x.s A ) e. No ) with typecode |-
26		pncans	Could not format ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) : No typesetting found for |- ( ( ( 2s x.s A ) e. No /\ 1s e. No ) -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) with typecode |-
27	25 21 26	sylancl	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) -s 1s ) = ( 2s x.s A ) ) with typecode |-
28	27	sneqd	Could not format ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } ) : No typesetting found for |- ( ph -> { ( ( ( 2s x.s A ) +s 1s ) -s 1s ) } = { ( 2s x.s A ) } ) with typecode |-
29		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
30		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
31		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 |-
32	30 31	ax-mp	Could not format ( 2s x.s 1s ) = 2s : No typesetting found for |- ( 2s x.s 1s ) = 2s with typecode |-
33	29 32	eqtr4i	Could not format ( 1s +s 1s ) = ( 2s x.s 1s ) : No typesetting found for |- ( 1s +s 1s ) = ( 2s x.s 1s ) with typecode |-
34	33	oveq2i	Could not format ( ( 2s x.s A ) +s ( 1s +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) : No typesetting found for |- ( ( 2s x.s A ) +s ( 1s +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) with typecode |-
35	25 22 22	addsassd	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( ( 2s x.s A ) +s ( 1s +s 1s ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( ( 2s x.s A ) +s ( 1s +s 1s ) ) ) with typecode |-
36	30	a1i	Could not format ( ph -> 2s e. No ) : No typesetting found for |- ( ph -> 2s e. No ) with typecode |-
37	36 3 22	addsdid	Could not format ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) ) : No typesetting found for |- ( ph -> ( 2s x.s ( A +s 1s ) ) = ( ( 2s x.s A ) +s ( 2s x.s 1s ) ) ) with typecode |-
38	34 35 37	3eqtr4a	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( 2s x.s ( A +s 1s ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) +s 1s ) = ( 2s x.s ( A +s 1s ) ) ) with typecode |-
39	38	sneqd	Could not format ( ph -> { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } = { ( 2s x.s ( A +s 1s ) ) } ) : No typesetting found for |- ( ph -> { ( ( ( 2s x.s A ) +s 1s ) +s 1s ) } = { ( 2s x.s ( A +s 1s ) ) } ) with typecode |-
40	28 39	oveq12d	Could not format ( 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 ) ) } ) ) : No typesetting found for |- ( 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 ) ) } ) ) with typecode |-
41	17 24 40	3eqtr3rd	Could not format ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) ) : No typesetting found for |- ( ph -> ( { ( 2s x.s A ) } |s { ( 2s x.s ( A +s 1s ) ) } ) = ( A +s ( A +s 1s ) ) ) with typecode |-
42	3 7 2 8 41	pw2cut	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
43	24	oveq1d	Could not format ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su ( 2s ^su ( N +s 1s ) ) ) = ( ( A +s ( A +s 1s ) ) /su ( 2s ^su ( N +s 1s ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( 2s x.s A ) +s 1s ) /su ( 2s ^su ( N +s 1s ) ) ) = ( ( A +s ( A +s 1s ) ) /su ( 2s ^su ( N +s 1s ) ) ) ) with typecode |-
44	42 43	eqtr4d	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-