Metamath Proof Explorer


Theorem negsproplem5

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when B is simpler than A . (Contributed by Scott Fenton, 3-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
negsproplem4.1 φ A No
negsproplem4.2 φ B No
negsproplem4.3 φ A < s B
negsproplem5.4 φ bday B bday A
Assertion negsproplem5 φ + s B < s + s 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 negsproplem4.1 φ A No
3 negsproplem4.2 φ B No
4 negsproplem4.3 φ A < s B
5 negsproplem5.4 φ bday B bday A
6 1 2 negsproplem3 φ + s A No + s R A s + s A + s A s + s L A
7 6 simp2d φ + s R A s + s A
8 negsfn + s Fn No
9 rightssno R A No
10 bdayelon bday A On
11 oldbday bday A On B No B Old bday A bday B bday A
12 10 3 11 sylancr φ B Old bday A bday B bday A
13 5 12 mpbird φ B Old bday A
14 breq2 b = B A < s b A < s B
15 rightval R A = b Old bday A | A < s b
16 14 15 elrab2 B R A B Old bday A A < s B
17 13 4 16 sylanbrc φ B R A
18 fnfvima + s Fn No R A No B R A + s B + s R A
19 8 9 17 18 mp3an12i φ + s B + s R A
20 fvex + s A V
21 20 snid + s A + s A
22 21 a1i φ + s A + s A
23 7 19 22 ssltsepcd φ + s B < s + s A