Metamath Proof Explorer


Theorem negsproplem6

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is the same age as B . (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
negsproplem6.4 φ bday A = bday B
Assertion negsproplem6 φ + 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 negsproplem6.4 φ bday A = bday B
6 nodense A No B No bday A = bday B A < s B d No bday d bday A A < s d d < s B
7 2 3 5 4 6 syl22anc φ d No bday d bday A A < s d d < s B
8 uncom bday A bday B = bday B bday A
9 8 eleq2i bday x bday y bday A bday B bday x bday y bday B bday A
10 9 imbi1i bday x bday y bday A bday B + s x No x < s y + s y < s + s x bday x bday y bday B bday A + s x No x < s y + s y < s + s x
11 10 2ralbii x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x x No y No bday x bday y bday B bday A + s x No x < s y + s y < s + s x
12 1 11 sylib φ x No y No bday x bday y bday B bday A + s x No x < s y + s y < s + s x
13 12 3 negsproplem3 φ + s B No + s R B s + s B + s B s + s L B
14 13 simp1d φ + s B No
15 14 adantr φ d No bday d bday A A < s d d < s B + s B No
16 1 adantr φ d No bday d bday A A < s d d < s B x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
17 simprl φ d No bday d bday A A < s d d < s B d No
18 0sno 0 s No
19 18 a1i φ d No bday d bday A A < s d d < s B 0 s No
20 bday0s bday 0 s =
21 20 uneq2i bday d bday 0 s = bday d
22 un0 bday d = bday d
23 21 22 eqtri bday d bday 0 s = bday d
24 simprr1 φ d No bday d bday A A < s d d < s B bday d bday A
25 elun1 bday d bday A bday d bday A bday B
26 24 25 syl φ d No bday d bday A A < s d d < s B bday d bday A bday B
27 23 26 eqeltrid φ d No bday d bday A A < s d d < s B bday d bday 0 s bday A bday B
28 16 17 19 27 negsproplem1 φ d No bday d bday A A < s d d < s B + s d No d < s 0 s + s 0 s < s + s d
29 28 simpld φ d No bday d bday A A < s d d < s B + s d No
30 1 2 negsproplem3 φ + s A No + s R A s + s A + s A s + s L A
31 30 simp1d φ + s A No
32 31 adantr φ d No bday d bday A A < s d d < s B + s A No
33 13 simp3d φ + s B s + s L B
34 33 adantr φ d No bday d bday A A < s d d < s B + s B s + s L B
35 fvex + s B V
36 35 snid + s B + s B
37 36 a1i φ d No bday d bday A A < s d d < s B + s B + s B
38 negsfn + s Fn No
39 leftssno L B No
40 bdayelon bday A On
41 oldbday bday A On d No d Old bday A bday d bday A
42 40 17 41 sylancr φ d No bday d bday A A < s d d < s B d Old bday A bday d bday A
43 24 42 mpbird φ d No bday d bday A A < s d d < s B d Old bday A
44 5 fveq2d φ Old bday A = Old bday B
45 44 adantr φ d No bday d bday A A < s d d < s B Old bday A = Old bday B
46 43 45 eleqtrd φ d No bday d bday A A < s d d < s B d Old bday B
47 simprr3 φ d No bday d bday A A < s d d < s B d < s B
48 leftval L B = d Old bday B | d < s B
49 48 reqabi d L B d Old bday B d < s B
50 46 47 49 sylanbrc φ d No bday d bday A A < s d d < s B d L B
51 fnfvima + s Fn No L B No d L B + s d + s L B
52 38 39 50 51 mp3an12i φ d No bday d bday A A < s d d < s B + s d + s L B
53 34 37 52 ssltsepcd φ d No bday d bday A A < s d d < s B + s B < s + s d
54 30 simp2d φ + s R A s + s A
55 54 adantr φ d No bday d bday A A < s d d < s B + s R A s + s A
56 rightssno R A No
57 simprr2 φ d No bday d bday A A < s d d < s B A < s d
58 rightval R A = d Old bday A | A < s d
59 58 reqabi d R A d Old bday A A < s d
60 43 57 59 sylanbrc φ d No bday d bday A A < s d d < s B d R A
61 fnfvima + s Fn No R A No d R A + s d + s R A
62 38 56 60 61 mp3an12i φ d No bday d bday A A < s d d < s B + s d + s R A
63 fvex + s A V
64 63 snid + s A + s A
65 64 a1i φ d No bday d bday A A < s d d < s B + s A + s A
66 55 62 65 ssltsepcd φ d No bday d bday A A < s d d < s B + s d < s + s A
67 15 29 32 53 66 slttrd φ d No bday d bday A A < s d d < s B + s B < s + s A
68 7 67 rexlimddv φ + s B < s + s A