Metamath Proof Explorer


Theorem mulsprop

Description: Surreals are closed under multiplication and obey a particular ordering law. Theorem 3.4 of Gonshor p. 17. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Assertion mulsprop A No B No C No D No E No F No A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E

Proof

Step Hyp Ref Expression
1 bdayelon bday A On
2 bdayelon bday B On
3 naddcl bday A On bday B On bday A + bday B On
4 1 2 3 mp2an bday A + bday B On
5 bdayelon bday C On
6 bdayelon bday E On
7 naddcl bday C On bday E On bday C + bday E On
8 5 6 7 mp2an bday C + bday E On
9 bdayelon bday D On
10 bdayelon bday F On
11 naddcl bday D On bday F On bday D + bday F On
12 9 10 11 mp2an bday D + bday F On
13 8 12 onun2i bday C + bday E bday D + bday F On
14 naddcl bday C On bday F On bday C + bday F On
15 5 10 14 mp2an bday C + bday F On
16 naddcl bday D On bday E On bday D + bday E On
17 9 6 16 mp2an bday D + bday E On
18 15 17 onun2i bday C + bday F bday D + bday E On
19 13 18 onun2i bday C + bday E bday D + bday F bday C + bday F bday D + bday E On
20 4 19 onun2i bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E On
21 risset bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E On x On x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
22 20 21 mpbi x On x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
23 fveq2 a = g bday a = bday g
24 23 oveq1d a = g bday a + bday b = bday g + bday b
25 24 uneq1d a = g bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
26 25 eqeq2d a = g x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e x = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
27 oveq1 a = g a s b = g s b
28 27 eleq1d a = g a s b No g s b No
29 28 anbi1d a = g a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
30 26 29 imbi12d a = g x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e x = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
31 fveq2 b = h bday b = bday h
32 31 oveq2d b = h bday g + bday b = bday g + bday h
33 32 uneq1d b = h bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e
34 33 eqeq2d b = h x = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e x = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e
35 oveq2 b = h g s b = g s h
36 35 eleq1d b = h g s b No g s h No
37 36 anbi1d b = h g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e
38 34 37 imbi12d b = h x = bday g + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e g s b No c < s d e < s f c s f - s c s e < s d s f - s d s e x = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e
39 fveq2 c = i bday c = bday i
40 39 oveq1d c = i bday c + bday e = bday i + bday e
41 40 uneq1d c = i bday c + bday e bday d + bday f = bday i + bday e bday d + bday f
42 39 oveq1d c = i bday c + bday f = bday i + bday f
43 42 uneq1d c = i bday c + bday f bday d + bday e = bday i + bday f bday d + bday e
44 41 43 uneq12d c = i bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday i + bday e bday d + bday f bday i + bday f bday d + bday e
45 44 uneq2d c = i bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e
46 45 eqeq2d c = i x = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e x = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e
47 breq1 c = i c < s d i < s d
48 47 anbi1d c = i c < s d e < s f i < s d e < s f
49 oveq1 c = i c s f = i s f
50 oveq1 c = i c s e = i s e
51 49 50 oveq12d c = i c s f - s c s e = i s f - s i s e
52 51 breq1d c = i c s f - s c s e < s d s f - s d s e i s f - s i s e < s d s f - s d s e
53 48 52 imbi12d c = i c < s d e < s f c s f - s c s e < s d s f - s d s e i < s d e < s f i s f - s i s e < s d s f - s d s e
54 53 anbi2d c = i g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e
55 46 54 imbi12d c = i x = bday g + bday h bday c + bday e bday d + bday f bday c + bday f bday d + bday e g s h No c < s d e < s f c s f - s c s e < s d s f - s d s e x = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e
56 fveq2 d = j bday d = bday j
57 56 oveq1d d = j bday d + bday f = bday j + bday f
58 57 uneq2d d = j bday i + bday e bday d + bday f = bday i + bday e bday j + bday f
59 56 oveq1d d = j bday d + bday e = bday j + bday e
60 59 uneq2d d = j bday i + bday f bday d + bday e = bday i + bday f bday j + bday e
61 58 60 uneq12d d = j bday i + bday e bday d + bday f bday i + bday f bday d + bday e = bday i + bday e bday j + bday f bday i + bday f bday j + bday e
62 61 uneq2d d = j bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e
63 62 eqeq2d d = j x = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e x = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e
64 breq2 d = j i < s d i < s j
65 64 anbi1d d = j i < s d e < s f i < s j e < s f
66 oveq1 d = j d s f = j s f
67 oveq1 d = j d s e = j s e
68 66 67 oveq12d d = j d s f - s d s e = j s f - s j s e
69 68 breq2d d = j i s f - s i s e < s d s f - s d s e i s f - s i s e < s j s f - s j s e
70 65 69 imbi12d d = j i < s d e < s f i s f - s i s e < s d s f - s d s e i < s j e < s f i s f - s i s e < s j s f - s j s e
71 70 anbi2d d = j g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e
72 63 71 imbi12d d = j x = bday g + bday h bday i + bday e bday d + bday f bday i + bday f bday d + bday e g s h No i < s d e < s f i s f - s i s e < s d s f - s d s e x = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e
73 fveq2 e = k bday e = bday k
74 73 oveq2d e = k bday i + bday e = bday i + bday k
75 74 uneq1d e = k bday i + bday e bday j + bday f = bday i + bday k bday j + bday f
76 73 oveq2d e = k bday j + bday e = bday j + bday k
77 76 uneq2d e = k bday i + bday f bday j + bday e = bday i + bday f bday j + bday k
78 75 77 uneq12d e = k bday i + bday e bday j + bday f bday i + bday f bday j + bday e = bday i + bday k bday j + bday f bday i + bday f bday j + bday k
79 78 uneq2d e = k bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k
80 79 eqeq2d e = k x = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e x = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k
81 breq1 e = k e < s f k < s f
82 81 anbi2d e = k i < s j e < s f i < s j k < s f
83 oveq2 e = k i s e = i s k
84 83 oveq2d e = k i s f - s i s e = i s f - s i s k
85 oveq2 e = k j s e = j s k
86 85 oveq2d e = k j s f - s j s e = j s f - s j s k
87 84 86 breq12d e = k i s f - s i s e < s j s f - s j s e i s f - s i s k < s j s f - s j s k
88 82 87 imbi12d e = k i < s j e < s f i s f - s i s e < s j s f - s j s e i < s j k < s f i s f - s i s k < s j s f - s j s k
89 88 anbi2d e = k g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k
90 80 89 imbi12d e = k x = bday g + bday h bday i + bday e bday j + bday f bday i + bday f bday j + bday e g s h No i < s j e < s f i s f - s i s e < s j s f - s j s e x = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k
91 fveq2 f = l bday f = bday l
92 91 oveq2d f = l bday j + bday f = bday j + bday l
93 92 uneq2d f = l bday i + bday k bday j + bday f = bday i + bday k bday j + bday l
94 91 oveq2d f = l bday i + bday f = bday i + bday l
95 94 uneq1d f = l bday i + bday f bday j + bday k = bday i + bday l bday j + bday k
96 93 95 uneq12d f = l bday i + bday k bday j + bday f bday i + bday f bday j + bday k = bday i + bday k bday j + bday l bday i + bday l bday j + bday k
97 96 uneq2d f = l bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k
98 97 eqeq2d f = l x = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k
99 breq2 f = l k < s f k < s l
100 99 anbi2d f = l i < s j k < s f i < s j k < s l
101 oveq2 f = l i s f = i s l
102 101 oveq1d f = l i s f - s i s k = i s l - s i s k
103 oveq2 f = l j s f = j s l
104 103 oveq1d f = l j s f - s j s k = j s l - s j s k
105 102 104 breq12d f = l i s f - s i s k < s j s f - s j s k i s l - s i s k < s j s l - s j s k
106 100 105 imbi12d f = l i < s j k < s f i s f - s i s k < s j s f - s j s k i < s j k < s l i s l - s i s k < s j s l - s j s k
107 106 anbi2d f = l g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
108 98 107 imbi12d f = l x = bday g + bday h bday i + bday k bday j + bday f bday i + bday f bday j + bday k g s h No i < s j k < s f i s f - s i s k < s j s f - s j s k x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
109 30 38 55 72 90 108 cbvral6vw a No b No c No d No e No f No x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
110 eqeq1 x = y x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
111 110 imbi1d x = y x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
112 111 6ralbidv x = y a No b No c No d No e No f No x = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
113 109 112 bitr3id x = y g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
114 raleq x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
115 ralrot3 a No b No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
116 ralrot3 c No d No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
117 ralrot3 e No f No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
118 r19.23v y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
119 risset bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
120 119 imbi1i bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
121 118 120 bitr4i y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
122 121 2ralbii e No f No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
123 117 122 bitr3i y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
124 123 2ralbii c No d No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
125 116 124 bitr3i y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
126 125 2ralbii a No b No y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
127 115 126 bitr3i y bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
128 114 127 bitrdi x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
129 simpl a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
130 simprl1 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g No
131 simprl2 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No h No
132 129 130 131 mulsproplem11 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g s h No
133 129 adantr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
134 simprl3 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i No
135 134 adantr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l i No
136 simprr1 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No j No
137 136 adantr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l j No
138 simprr2 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No k No
139 138 adantr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l k No
140 simprr3 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No l No
141 140 adantr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l l No
142 simprl a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l i < s j
143 simprr a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l k < s l
144 133 135 137 139 141 142 143 mulsproplem14 a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l i s l - s i s k < s j s l - s j s k
145 144 ex a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No i < s j k < s l i s l - s i s k < s j s l - s j s k
146 132 145 jca a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
147 146 ex a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
148 128 147 biimtrdi x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
149 148 impd x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
150 149 com12 y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
151 150 anassrs y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
152 151 ralrimivvva y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
153 152 ralrimivvva y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
154 153 a1i x On y x a No b No c No d No e No f No y = bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
155 113 154 tfis2 x On g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
156 fveq2 g = A bday g = bday A
157 156 oveq1d g = A bday g + bday h = bday A + bday h
158 157 uneq1d g = A bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k = bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k
159 158 eqeq2d g = A x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k x = bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k
160 oveq1 g = A g s h = A s h
161 160 eleq1d g = A g s h No A s h No
162 161 anbi1d g = A g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k A s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
163 159 162 imbi12d g = A x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k x = bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k A s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
164 fveq2 h = B bday h = bday B
165 164 oveq2d h = B bday A + bday h = bday A + bday B
166 165 uneq1d h = B bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k = bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k
167 166 eqeq2d h = B x = bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k x = bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k
168 oveq2 h = B A s h = A s B
169 168 eleq1d h = B A s h No A s B No
170 169 anbi1d h = B A s h No i < s j k < s l i s l - s i s k < s j s l - s j s k A s B No i < s j k < s l i s l - s i s k < s j s l - s j s k
171 167 170 imbi12d h = B x = bday A + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k A s h No i < s j k < s l i s l - s i s k < s j s l - s j s k x = bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k A s B No i < s j k < s l i s l - s i s k < s j s l - s j s k
172 fveq2 i = C bday i = bday C
173 172 oveq1d i = C bday i + bday k = bday C + bday k
174 173 uneq1d i = C bday i + bday k bday j + bday l = bday C + bday k bday j + bday l
175 172 oveq1d i = C bday i + bday l = bday C + bday l
176 175 uneq1d i = C bday i + bday l bday j + bday k = bday C + bday l bday j + bday k
177 174 176 uneq12d i = C bday i + bday k bday j + bday l bday i + bday l bday j + bday k = bday C + bday k bday j + bday l bday C + bday l bday j + bday k
178 177 uneq2d i = C bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k = bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k
179 178 eqeq2d i = C x = bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k x = bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k
180 breq1 i = C i < s j C < s j
181 180 anbi1d i = C i < s j k < s l C < s j k < s l
182 oveq1 i = C i s l = C s l
183 oveq1 i = C i s k = C s k
184 182 183 oveq12d i = C i s l - s i s k = C s l - s C s k
185 184 breq1d i = C i s l - s i s k < s j s l - s j s k C s l - s C s k < s j s l - s j s k
186 181 185 imbi12d i = C i < s j k < s l i s l - s i s k < s j s l - s j s k C < s j k < s l C s l - s C s k < s j s l - s j s k
187 186 anbi2d i = C A s B No i < s j k < s l i s l - s i s k < s j s l - s j s k A s B No C < s j k < s l C s l - s C s k < s j s l - s j s k
188 179 187 imbi12d i = C x = bday A + bday B bday i + bday k bday j + bday l bday i + bday l bday j + bday k A s B No i < s j k < s l i s l - s i s k < s j s l - s j s k x = bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k A s B No C < s j k < s l C s l - s C s k < s j s l - s j s k
189 fveq2 j = D bday j = bday D
190 189 oveq1d j = D bday j + bday l = bday D + bday l
191 190 uneq2d j = D bday C + bday k bday j + bday l = bday C + bday k bday D + bday l
192 189 oveq1d j = D bday j + bday k = bday D + bday k
193 192 uneq2d j = D bday C + bday l bday j + bday k = bday C + bday l bday D + bday k
194 191 193 uneq12d j = D bday C + bday k bday j + bday l bday C + bday l bday j + bday k = bday C + bday k bday D + bday l bday C + bday l bday D + bday k
195 194 uneq2d j = D bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k = bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k
196 195 eqeq2d j = D x = bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k x = bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k
197 breq2 j = D C < s j C < s D
198 197 anbi1d j = D C < s j k < s l C < s D k < s l
199 oveq1 j = D j s l = D s l
200 oveq1 j = D j s k = D s k
201 199 200 oveq12d j = D j s l - s j s k = D s l - s D s k
202 201 breq2d j = D C s l - s C s k < s j s l - s j s k C s l - s C s k < s D s l - s D s k
203 198 202 imbi12d j = D C < s j k < s l C s l - s C s k < s j s l - s j s k C < s D k < s l C s l - s C s k < s D s l - s D s k
204 203 anbi2d j = D A s B No C < s j k < s l C s l - s C s k < s j s l - s j s k A s B No C < s D k < s l C s l - s C s k < s D s l - s D s k
205 196 204 imbi12d j = D x = bday A + bday B bday C + bday k bday j + bday l bday C + bday l bday j + bday k A s B No C < s j k < s l C s l - s C s k < s j s l - s j s k x = bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k A s B No C < s D k < s l C s l - s C s k < s D s l - s D s k
206 fveq2 k = E bday k = bday E
207 206 oveq2d k = E bday C + bday k = bday C + bday E
208 207 uneq1d k = E bday C + bday k bday D + bday l = bday C + bday E bday D + bday l
209 206 oveq2d k = E bday D + bday k = bday D + bday E
210 209 uneq2d k = E bday C + bday l bday D + bday k = bday C + bday l bday D + bday E
211 208 210 uneq12d k = E bday C + bday k bday D + bday l bday C + bday l bday D + bday k = bday C + bday E bday D + bday l bday C + bday l bday D + bday E
212 211 uneq2d k = E bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k = bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E
213 212 eqeq2d k = E x = bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k x = bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E
214 breq1 k = E k < s l E < s l
215 214 anbi2d k = E C < s D k < s l C < s D E < s l
216 oveq2 k = E C s k = C s E
217 216 oveq2d k = E C s l - s C s k = C s l - s C s E
218 oveq2 k = E D s k = D s E
219 218 oveq2d k = E D s l - s D s k = D s l - s D s E
220 217 219 breq12d k = E C s l - s C s k < s D s l - s D s k C s l - s C s E < s D s l - s D s E
221 215 220 imbi12d k = E C < s D k < s l C s l - s C s k < s D s l - s D s k C < s D E < s l C s l - s C s E < s D s l - s D s E
222 221 anbi2d k = E A s B No C < s D k < s l C s l - s C s k < s D s l - s D s k A s B No C < s D E < s l C s l - s C s E < s D s l - s D s E
223 213 222 imbi12d k = E x = bday A + bday B bday C + bday k bday D + bday l bday C + bday l bday D + bday k A s B No C < s D k < s l C s l - s C s k < s D s l - s D s k x = bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E A s B No C < s D E < s l C s l - s C s E < s D s l - s D s E
224 fveq2 l = F bday l = bday F
225 224 oveq2d l = F bday D + bday l = bday D + bday F
226 225 uneq2d l = F bday C + bday E bday D + bday l = bday C + bday E bday D + bday F
227 224 oveq2d l = F bday C + bday l = bday C + bday F
228 227 uneq1d l = F bday C + bday l bday D + bday E = bday C + bday F bday D + bday E
229 226 228 uneq12d l = F bday C + bday E bday D + bday l bday C + bday l bday D + bday E = bday C + bday E bday D + bday F bday C + bday F bday D + bday E
230 229 uneq2d l = F bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
231 230 eqeq2d l = F x = bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
232 breq2 l = F E < s l E < s F
233 232 anbi2d l = F C < s D E < s l C < s D E < s F
234 oveq2 l = F C s l = C s F
235 234 oveq1d l = F C s l - s C s E = C s F - s C s E
236 oveq2 l = F D s l = D s F
237 236 oveq1d l = F D s l - s D s E = D s F - s D s E
238 235 237 breq12d l = F C s l - s C s E < s D s l - s D s E C s F - s C s E < s D s F - s D s E
239 233 238 imbi12d l = F C < s D E < s l C s l - s C s E < s D s l - s D s E C < s D E < s F C s F - s C s E < s D s F - s D s E
240 239 anbi2d l = F A s B No C < s D E < s l C s l - s C s E < s D s l - s D s E A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
241 231 240 imbi12d l = F x = bday A + bday B bday C + bday E bday D + bday l bday C + bday l bday D + bday E A s B No C < s D E < s l C s l - s C s E < s D s l - s D s E x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
242 163 171 188 205 223 241 rspc6v A No B No C No D No E No F No g No h No i No j No k No l No x = bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
243 155 242 syl5com x On A No B No C No D No E No F No x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
244 243 com23 x On x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E A No B No C No D No E No F No A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
245 244 rexlimiv x On x = bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E A No B No C No D No E No F No A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E
246 22 245 ax-mp A No B No C No D No E No F No A s B No C < s D E < s F C s F - s C s E < s D s F - s D s E