Metamath Proof Explorer


Theorem negsproplem3

Description: Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 φ x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
negsproplem2.1 φ A No
Assertion negsproplem3 φ + s A No + s R A s + s A + s A s + s L A

Proof

Step Hyp Ref Expression
1 negsproplem.1 φ x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
2 negsproplem2.1 φ A No
3 1 2 negsproplem2 φ + s R A s + s L A
4 scutcut + s R A s + s L A + s R A | s + s L A No + s R A s + s R A | s + s L A + s R A | s + s L A s + s L A
5 3 4 syl φ + s R A | s + s L A No + s R A s + s R A | s + s L A + s R A | s + s L A s + s L A
6 negsval A No + s A = + s R A | s + s L A
7 2 6 syl φ + s A = + s R A | s + s L A
8 7 eleq1d φ + s A No + s R A | s + s L A No
9 7 sneqd φ + s A = + s R A | s + s L A
10 9 breq2d φ + s R A s + s A + s R A s + s R A | s + s L A
11 9 breq1d φ + s A s + s L A + s R A | s + s L A s + s L A
12 8 10 11 3anbi123d φ + s A No + s R A s + s A + s A s + s L A + s R A | s + s L A No + s R A s + s R A | s + s L A + s R A | s + s L A s + s L A
13 5 12 mpbird φ + s A No + s R A s + s A + s A s + s L A