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	⊢ ( 𝜑 → 𝐴 ∈ ℤs )
	pw2cutp1.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2cutp1	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) = ( ( ( 2s ·s 𝐴 ) +s 1s ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pw2cutp1.1	⊢ ( 𝜑 → 𝐴 ∈ ℤs )
2		pw2cutp1.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3	1	znod	⊢ ( 𝜑 → 𝐴 ∈ No )
4		1zs	⊢ 1s ∈ ℤs
5		zaddscl	⊢ ( ( 𝐴 ∈ ℤs ∧ 1s ∈ ℤs ) → ( 𝐴 +s 1s ) ∈ ℤs )
6	1 4 5	sylancl	⊢ ( 𝜑 → ( 𝐴 +s 1s ) ∈ ℤs )
7	6	znod	⊢ ( 𝜑 → ( 𝐴 +s 1s ) ∈ No )
8	3	ltsp1d	⊢ ( 𝜑 → 𝐴 <s ( 𝐴 +s 1s ) )
9		2nns	⊢ 2s ∈ ℕs
10		nnzs	⊢ ( 2s ∈ ℕs → 2s ∈ ℤs )
11	9 10	ax-mp	⊢ 2s ∈ ℤs
12	11	a1i	⊢ ( 𝜑 → 2s ∈ ℤs )
13	12 1	zmulscld	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ∈ ℤs )
14		zaddscl	⊢ ( ( ( 2s ·s 𝐴 ) ∈ ℤs ∧ 1s ∈ ℤs ) → ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℤs )
15	13 4 14	sylancl	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℤs )
16		zcuts	⊢ ( ( ( 2s ·s 𝐴 ) +s 1s ) ∈ ℤs → ( ( 2s ·s 𝐴 ) +s 1s ) = ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s { ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) } ) )
17	15 16	syl	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s { ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) } ) )
18		no2times	⊢ ( 𝐴 ∈ No → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
19	3 18	syl	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) = ( 𝐴 +s 𝐴 ) )
20	19	oveq1d	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( ( 𝐴 +s 𝐴 ) +s 1s ) )
21		1no	⊢ 1s ∈ No
22	21	a1i	⊢ ( 𝜑 → 1s ∈ No )
23	3 3 22	addsassd	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐴 ) +s 1s ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
24	20 23	eqtrd	⊢ ( 𝜑 → ( ( 2s ·s 𝐴 ) +s 1s ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
25	13	znod	⊢ ( 𝜑 → ( 2s ·s 𝐴 ) ∈ No )
26		pncans	⊢ ( ( ( 2s ·s 𝐴 ) ∈ No ∧ 1s ∈ No ) → ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) = ( 2s ·s 𝐴 ) )
27	25 21 26	sylancl	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) = ( 2s ·s 𝐴 ) )
28	27	sneqd	⊢ ( 𝜑 → { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } = { ( 2s ·s 𝐴 ) } )
29		1p1e2s	⊢ ( 1s +s 1s ) = 2s
30		2no	⊢ 2s ∈ No
31		mulsrid	⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
32	30 31	ax-mp	⊢ ( 2s ·s 1s ) = 2s
33	29 32	eqtr4i	⊢ ( 1s +s 1s ) = ( 2s ·s 1s )
34	33	oveq2i	⊢ ( ( 2s ·s 𝐴 ) +s ( 1s +s 1s ) ) = ( ( 2s ·s 𝐴 ) +s ( 2s ·s 1s ) )
35	25 22 22	addsassd	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) = ( ( 2s ·s 𝐴 ) +s ( 1s +s 1s ) ) )
36	30	a1i	⊢ ( 𝜑 → 2s ∈ No )
37	36 3 22	addsdid	⊢ ( 𝜑 → ( 2s ·s ( 𝐴 +s 1s ) ) = ( ( 2s ·s 𝐴 ) +s ( 2s ·s 1s ) ) )
38	34 35 37	3eqtr4a	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) = ( 2s ·s ( 𝐴 +s 1s ) ) )
39	38	sneqd	⊢ ( 𝜑 → { ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) } = { ( 2s ·s ( 𝐴 +s 1s ) ) } )
40	28 39	oveq12d	⊢ ( 𝜑 → ( { ( ( ( 2s ·s 𝐴 ) +s 1s ) −s 1s ) } |s { ( ( ( 2s ·s 𝐴 ) +s 1s ) +s 1s ) } ) = ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s ( 𝐴 +s 1s ) ) } ) )
41	17 24 40	3eqtr3rd	⊢ ( 𝜑 → ( { ( 2s ·s 𝐴 ) } |s { ( 2s ·s ( 𝐴 +s 1s ) ) } ) = ( 𝐴 +s ( 𝐴 +s 1s ) ) )
42	3 7 2 8 41	pw2cut	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) = ( ( 𝐴 +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
43	24	oveq1d	⊢ ( 𝜑 → ( ( ( 2s ·s 𝐴 ) +s 1s ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) = ( ( 𝐴 +s ( 𝐴 +s 1s ) ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )
44	42 43	eqtr4d	⊢ ( 𝜑 → ( { ( 𝐴 /su ( 2s ↑s 𝑁 ) ) } |s { ( ( 𝐴 +s 1s ) /su ( 2s ↑s 𝑁 ) ) } ) = ( ( ( 2s ·s 𝐴 ) +s 1s ) /su ( 2s ↑s ( 𝑁 +s 1s ) ) ) )