Theorem cutpos

Description: Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	cutpos.1	$$⊢\phi \to A\in \mathrm{No}$$
	cutpos.2	$$⊢\phi \to 0_s{<}_{s}A$$
Assertion	cutpos	$$⊢\phi \to A=\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){|}_{s}R\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cutpos.1	$$⊢\phi \to A\in \mathrm{No}$$
2		cutpos.2	$$⊢\phi \to 0_s{<}_{s}A$$
3		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
4	3	a1i	$$⊢\phi \to L\left(A\right){\ll }_{s}R\left(A\right)$$
5		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
6	1 5	syl	$$⊢\phi \to L\left(A\right){|}_{s}R\left(A\right)=A$$
7	6	eqcomd	$$⊢\phi \to A=L\left(A\right){|}_{s}R\left(A\right)$$
8	1 2	0elleft	$$⊢\phi \to 0_s\in L\left(A\right)$$
9	4 7 8	cutlt	$$⊢\phi \to A=\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){|}_{s}R\left(A\right)$$