Metamath Proof Explorer


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 φ A No
cutpos.2 φ 0 s < s A
Assertion cutpos φ A = 0 s x L A | 0 s < s x | s R A

Proof

Step Hyp Ref Expression
1 cutpos.1 φ A No
2 cutpos.2 φ 0 s < s A
3 lltropt L A s R A
4 3 a1i φ L A s R A
5 lrcut A No L A | s R A = A
6 1 5 syl φ L A | s R A = A
7 6 eqcomd φ A = L A | s R A
8 1 2 0elleft φ 0 s L A
9 4 7 8 cutlt φ A = 0 s x L A | 0 s < s x | s R A