Theorem negcut

Description: The cut properties of surreal negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negcut	$$⊢A\in \mathrm{No}\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\wedge \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		negsprop	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)$$
2	1	a1d	$$⊢\left(x\in \mathrm{No}\wedge y\in \mathrm{No}\right)\to \left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(0_s\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
3	2	rgen2	$$⊢\forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(0_s\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
4	3	a1i	$$⊢A\in \mathrm{No}\to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(0_s\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
5		id	$$⊢A\in \mathrm{No}\to A\in \mathrm{No}$$
6	4 5	negsproplem3	$$⊢A\in \mathrm{No}\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\wedge \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$