Theorem zscut

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

	Ref	Expression
Assertion	zscut	⊢ ( 𝐴 ∈ ℤs → 𝐴 = ( { ( 𝐴 -s 1s ) } |s { ( 𝐴 +s 1s ) } ) )

Proof

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