Metamath Proof Explorer


Theorem mulsproplem8

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 φ 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 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
mulsproplem8.1 φ A No
mulsproplem8.2 φ B No
mulsproplem8.3 φ R R A
mulsproplem8.4 φ S R B
mulsproplem8.5 φ V R A
mulsproplem8.6 φ W L B
Assertion mulsproplem8 φ R s B + s A s S - s R s S < s V s B + s A s W - s V s W

Proof

Step Hyp Ref Expression
1 mulsproplem.1 φ 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 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
2 mulsproplem8.1 φ A No
3 mulsproplem8.2 φ B No
4 mulsproplem8.3 φ R R A
5 mulsproplem8.4 φ S R B
6 mulsproplem8.5 φ V R A
7 mulsproplem8.6 φ W L B
8 rightssno R A No
9 8 4 sselid φ R No
10 8 6 sselid φ V No
11 sltlin R No V No R < s V R = V V < s R
12 9 10 11 syl2anc φ R < s V R = V V < s R
13 rightssold R A Old bday A
14 13 4 sselid φ R Old bday A
15 1 14 3 mulsproplem2 φ R s B No
16 rightssold R B Old bday B
17 16 5 sselid φ S Old bday B
18 1 2 17 mulsproplem3 φ A s S No
19 15 18 addscld φ R s B + s A s S No
20 1 14 17 mulsproplem4 φ R s S No
21 19 20 subscld φ R s B + s A s S - s R s S No
22 21 adantr φ R < s V R s B + s A s S - s R s S No
23 leftssold L B Old bday B
24 23 7 sselid φ W Old bday B
25 1 2 24 mulsproplem3 φ A s W No
26 15 25 addscld φ R s B + s A s W No
27 1 14 24 mulsproplem4 φ R s W No
28 26 27 subscld φ R s B + s A s W - s R s W No
29 28 adantr φ R < s V R s B + s A s W - s R s W No
30 13 6 sselid φ V Old bday A
31 1 30 3 mulsproplem2 φ V s B No
32 31 25 addscld φ V s B + s A s W No
33 1 30 24 mulsproplem4 φ V s W No
34 32 33 subscld φ V s B + s A s W - s V s W No
35 34 adantr φ R < s V V s B + s A s W - s V s W No
36 ssltright A No A s R A
37 2 36 syl φ A s R A
38 snidg A No A A
39 2 38 syl φ A A
40 37 39 4 ssltsepcd φ A < s R
41 lltropt L B s R B
42 41 a1i φ L B s R B
43 42 7 5 ssltsepcd φ W < s S
44 0sno 0 s No
45 44 a1i φ 0 s No
46 leftssno L B No
47 46 7 sselid φ W No
48 rightssno R B No
49 48 5 sselid φ S No
50 bday0s bday 0 s =
51 50 50 oveq12i bday 0 s + bday 0 s = +
52 0elon On
53 naddrid On + =
54 52 53 ax-mp + =
55 51 54 eqtri bday 0 s + bday 0 s =
56 55 uneq1i bday 0 s + bday 0 s bday A + bday W bday R + bday S bday A + bday S bday R + bday W = bday A + bday W bday R + bday S bday A + bday S bday R + bday W
57 0un bday A + bday W bday R + bday S bday A + bday S bday R + bday W = bday A + bday W bday R + bday S bday A + bday S bday R + bday W
58 56 57 eqtri bday 0 s + bday 0 s bday A + bday W bday R + bday S bday A + bday S bday R + bday W = bday A + bday W bday R + bday S bday A + bday S bday R + bday W
59 oldbdayim W Old bday B bday W bday B
60 24 59 syl φ bday W bday B
61 bdayelon bday W On
62 bdayelon bday B On
63 bdayelon bday A On
64 naddel2 bday W On bday B On bday A On bday W bday B bday A + bday W bday A + bday B
65 61 62 63 64 mp3an bday W bday B bday A + bday W bday A + bday B
66 60 65 sylib φ bday A + bday W bday A + bday B
67 oldbdayim R Old bday A bday R bday A
68 14 67 syl φ bday R bday A
69 oldbdayim S Old bday B bday S bday B
70 17 69 syl φ bday S bday B
71 naddel12 bday A On bday B On bday R bday A bday S bday B bday R + bday S bday A + bday B
72 63 62 71 mp2an bday R bday A bday S bday B bday R + bday S bday A + bday B
73 68 70 72 syl2anc φ bday R + bday S bday A + bday B
74 66 73 jca φ bday A + bday W bday A + bday B bday R + bday S bday A + bday B
75 bdayelon bday S On
76 naddel2 bday S On bday B On bday A On bday S bday B bday A + bday S bday A + bday B
77 75 62 63 76 mp3an bday S bday B bday A + bday S bday A + bday B
78 70 77 sylib φ bday A + bday S bday A + bday B
79 naddel12 bday A On bday B On bday R bday A bday W bday B bday R + bday W bday A + bday B
80 63 62 79 mp2an bday R bday A bday W bday B bday R + bday W bday A + bday B
81 68 60 80 syl2anc φ bday R + bday W bday A + bday B
82 78 81 jca φ bday A + bday S bday A + bday B bday R + bday W bday A + bday B
83 naddcl bday A On bday W On bday A + bday W On
84 63 61 83 mp2an bday A + bday W On
85 bdayelon bday R On
86 naddcl bday R On bday S On bday R + bday S On
87 85 75 86 mp2an bday R + bday S On
88 84 87 onun2i bday A + bday W bday R + bday S On
89 naddcl bday A On bday S On bday A + bday S On
90 63 75 89 mp2an bday A + bday S On
91 naddcl bday R On bday W On bday R + bday W On
92 85 61 91 mp2an bday R + bday W On
93 90 92 onun2i bday A + bday S bday R + bday W On
94 naddcl bday A On bday B On bday A + bday B On
95 63 62 94 mp2an bday A + bday B On
96 onunel bday A + bday W bday R + bday S On bday A + bday S bday R + bday W On bday A + bday B On bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday A + bday W bday R + bday S bday A + bday B bday A + bday S bday R + bday W bday A + bday B
97 88 93 95 96 mp3an bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday A + bday W bday R + bday S bday A + bday B bday A + bday S bday R + bday W bday A + bday B
98 onunel bday A + bday W On bday R + bday S On bday A + bday B On bday A + bday W bday R + bday S bday A + bday B bday A + bday W bday A + bday B bday R + bday S bday A + bday B
99 84 87 95 98 mp3an bday A + bday W bday R + bday S bday A + bday B bday A + bday W bday A + bday B bday R + bday S bday A + bday B
100 onunel bday A + bday S On bday R + bday W On bday A + bday B On bday A + bday S bday R + bday W bday A + bday B bday A + bday S bday A + bday B bday R + bday W bday A + bday B
101 90 92 95 100 mp3an bday A + bday S bday R + bday W bday A + bday B bday A + bday S bday A + bday B bday R + bday W bday A + bday B
102 99 101 anbi12i bday A + bday W bday R + bday S bday A + bday B bday A + bday S bday R + bday W bday A + bday B bday A + bday W bday A + bday B bday R + bday S bday A + bday B bday A + bday S bday A + bday B bday R + bday W bday A + bday B
103 97 102 bitri bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday A + bday W bday A + bday B bday R + bday S bday A + bday B bday A + bday S bday A + bday B bday R + bday W bday A + bday B
104 74 82 103 sylanbrc φ bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B
105 elun1 bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
106 104 105 syl φ bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
107 58 106 eqeltrid φ bday 0 s + bday 0 s bday A + bday W bday R + bday S bday A + bday S bday R + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
108 1 45 45 2 9 47 49 107 mulsproplem1 φ 0 s s 0 s No A < s R W < s S A s S - s A s W < s R s S - s R s W
109 108 simprd φ A < s R W < s S A s S - s A s W < s R s S - s R s W
110 40 43 109 mp2and φ A s S - s A s W < s R s S - s R s W
111 18 20 25 27 sltsubsubbd φ A s S - s A s W < s R s S - s R s W A s S - s R s S < s A s W - s R s W
112 18 20 subscld φ A s S - s R s S No
113 25 27 subscld φ A s W - s R s W No
114 112 113 15 sltadd2d φ A s S - s R s S < s A s W - s R s W R s B + s A s S - s R s S < s R s B + s A s W - s R s W
115 111 114 bitrd φ A s S - s A s W < s R s S - s R s W R s B + s A s S - s R s S < s R s B + s A s W - s R s W
116 110 115 mpbid φ R s B + s A s S - s R s S < s R s B + s A s W - s R s W
117 15 18 20 addsubsassd φ R s B + s A s S - s R s S = R s B + s A s S - s R s S
118 15 25 27 addsubsassd φ R s B + s A s W - s R s W = R s B + s A s W - s R s W
119 116 117 118 3brtr4d φ R s B + s A s S - s R s S < s R s B + s A s W - s R s W
120 119 adantr φ R < s V R s B + s A s S - s R s S < s R s B + s A s W - s R s W
121 ssltleft B No L B s B
122 3 121 syl φ L B s B
123 snidg B No B B
124 3 123 syl φ B B
125 122 7 124 ssltsepcd φ W < s B
126 55 uneq1i bday 0 s + bday 0 s bday R + bday W bday V + bday B bday R + bday B bday V + bday W = bday R + bday W bday V + bday B bday R + bday B bday V + bday W
127 0un bday R + bday W bday V + bday B bday R + bday B bday V + bday W = bday R + bday W bday V + bday B bday R + bday B bday V + bday W
128 126 127 eqtri bday 0 s + bday 0 s bday R + bday W bday V + bday B bday R + bday B bday V + bday W = bday R + bday W bday V + bday B bday R + bday B bday V + bday W
129 oldbdayim V Old bday A bday V bday A
130 30 129 syl φ bday V bday A
131 bdayelon bday V On
132 naddel1 bday V On bday A On bday B On bday V bday A bday V + bday B bday A + bday B
133 131 63 62 132 mp3an bday V bday A bday V + bday B bday A + bday B
134 130 133 sylib φ bday V + bday B bday A + bday B
135 81 134 jca φ bday R + bday W bday A + bday B bday V + bday B bday A + bday B
136 naddel1 bday R On bday A On bday B On bday R bday A bday R + bday B bday A + bday B
137 85 63 62 136 mp3an bday R bday A bday R + bday B bday A + bday B
138 68 137 sylib φ bday R + bday B bday A + bday B
139 naddel12 bday A On bday B On bday V bday A bday W bday B bday V + bday W bday A + bday B
140 63 62 139 mp2an bday V bday A bday W bday B bday V + bday W bday A + bday B
141 130 60 140 syl2anc φ bday V + bday W bday A + bday B
142 138 141 jca φ bday R + bday B bday A + bday B bday V + bday W bday A + bday B
143 naddcl bday V On bday B On bday V + bday B On
144 131 62 143 mp2an bday V + bday B On
145 92 144 onun2i bday R + bday W bday V + bday B On
146 naddcl bday R On bday B On bday R + bday B On
147 85 62 146 mp2an bday R + bday B On
148 naddcl bday V On bday W On bday V + bday W On
149 131 61 148 mp2an bday V + bday W On
150 147 149 onun2i bday R + bday B bday V + bday W On
151 onunel bday R + bday W bday V + bday B On bday R + bday B bday V + bday W On bday A + bday B On bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday R + bday W bday V + bday B bday A + bday B bday R + bday B bday V + bday W bday A + bday B
152 145 150 95 151 mp3an bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday R + bday W bday V + bday B bday A + bday B bday R + bday B bday V + bday W bday A + bday B
153 onunel bday R + bday W On bday V + bday B On bday A + bday B On bday R + bday W bday V + bday B bday A + bday B bday R + bday W bday A + bday B bday V + bday B bday A + bday B
154 92 144 95 153 mp3an bday R + bday W bday V + bday B bday A + bday B bday R + bday W bday A + bday B bday V + bday B bday A + bday B
155 onunel bday R + bday B On bday V + bday W On bday A + bday B On bday R + bday B bday V + bday W bday A + bday B bday R + bday B bday A + bday B bday V + bday W bday A + bday B
156 147 149 95 155 mp3an bday R + bday B bday V + bday W bday A + bday B bday R + bday B bday A + bday B bday V + bday W bday A + bday B
157 154 156 anbi12i bday R + bday W bday V + bday B bday A + bday B bday R + bday B bday V + bday W bday A + bday B bday R + bday W bday A + bday B bday V + bday B bday A + bday B bday R + bday B bday A + bday B bday V + bday W bday A + bday B
158 152 157 bitri bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday R + bday W bday A + bday B bday V + bday B bday A + bday B bday R + bday B bday A + bday B bday V + bday W bday A + bday B
159 135 142 158 sylanbrc φ bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B
160 elun1 bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
161 159 160 syl φ bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
162 128 161 eqeltrid φ bday 0 s + bday 0 s bday R + bday W bday V + bday B bday R + bday B bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
163 1 45 45 9 10 47 3 162 mulsproplem1 φ 0 s s 0 s No R < s V W < s B R s B - s R s W < s V s B - s V s W
164 163 simprd φ R < s V W < s B R s B - s R s W < s V s B - s V s W
165 125 164 mpan2d φ R < s V R s B - s R s W < s V s B - s V s W
166 165 imp φ R < s V R s B - s R s W < s V s B - s V s W
167 15 27 subscld φ R s B - s R s W No
168 31 33 subscld φ V s B - s V s W No
169 167 168 25 sltadd1d φ R s B - s R s W < s V s B - s V s W R s B - s R s W + s A s W < s V s B - s V s W + s A s W
170 169 adantr φ R < s V R s B - s R s W < s V s B - s V s W R s B - s R s W + s A s W < s V s B - s V s W + s A s W
171 166 170 mpbid φ R < s V R s B - s R s W + s A s W < s V s B - s V s W + s A s W
172 15 25 27 addsubsd φ R s B + s A s W - s R s W = R s B - s R s W + s A s W
173 172 adantr φ R < s V R s B + s A s W - s R s W = R s B - s R s W + s A s W
174 31 25 33 addsubsd φ V s B + s A s W - s V s W = V s B - s V s W + s A s W
175 174 adantr φ R < s V V s B + s A s W - s V s W = V s B - s V s W + s A s W
176 171 173 175 3brtr4d φ R < s V R s B + s A s W - s R s W < s V s B + s A s W - s V s W
177 22 29 35 120 176 slttrd φ R < s V R s B + s A s S - s R s S < s V s B + s A s W - s V s W
178 177 ex φ R < s V R s B + s A s S - s R s S < s V s B + s A s W - s V s W
179 37 39 6 ssltsepcd φ A < s V
180 55 uneq1i bday 0 s + bday 0 s bday A + bday W bday V + bday S bday A + bday S bday V + bday W = bday A + bday W bday V + bday S bday A + bday S bday V + bday W
181 0un bday A + bday W bday V + bday S bday A + bday S bday V + bday W = bday A + bday W bday V + bday S bday A + bday S bday V + bday W
182 180 181 eqtri bday 0 s + bday 0 s bday A + bday W bday V + bday S bday A + bday S bday V + bday W = bday A + bday W bday V + bday S bday A + bday S bday V + bday W
183 naddel12 bday A On bday B On bday V bday A bday S bday B bday V + bday S bday A + bday B
184 63 62 183 mp2an bday V bday A bday S bday B bday V + bday S bday A + bday B
185 130 70 184 syl2anc φ bday V + bday S bday A + bday B
186 66 185 jca φ bday A + bday W bday A + bday B bday V + bday S bday A + bday B
187 78 141 jca φ bday A + bday S bday A + bday B bday V + bday W bday A + bday B
188 naddcl bday V On bday S On bday V + bday S On
189 131 75 188 mp2an bday V + bday S On
190 84 189 onun2i bday A + bday W bday V + bday S On
191 90 149 onun2i bday A + bday S bday V + bday W On
192 onunel bday A + bday W bday V + bday S On bday A + bday S bday V + bday W On bday A + bday B On bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday A + bday W bday V + bday S bday A + bday B bday A + bday S bday V + bday W bday A + bday B
193 190 191 95 192 mp3an bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday A + bday W bday V + bday S bday A + bday B bday A + bday S bday V + bday W bday A + bday B
194 onunel bday A + bday W On bday V + bday S On bday A + bday B On bday A + bday W bday V + bday S bday A + bday B bday A + bday W bday A + bday B bday V + bday S bday A + bday B
195 84 189 95 194 mp3an bday A + bday W bday V + bday S bday A + bday B bday A + bday W bday A + bday B bday V + bday S bday A + bday B
196 onunel bday A + bday S On bday V + bday W On bday A + bday B On bday A + bday S bday V + bday W bday A + bday B bday A + bday S bday A + bday B bday V + bday W bday A + bday B
197 90 149 95 196 mp3an bday A + bday S bday V + bday W bday A + bday B bday A + bday S bday A + bday B bday V + bday W bday A + bday B
198 195 197 anbi12i bday A + bday W bday V + bday S bday A + bday B bday A + bday S bday V + bday W bday A + bday B bday A + bday W bday A + bday B bday V + bday S bday A + bday B bday A + bday S bday A + bday B bday V + bday W bday A + bday B
199 193 198 bitri bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday A + bday W bday A + bday B bday V + bday S bday A + bday B bday A + bday S bday A + bday B bday V + bday W bday A + bday B
200 186 187 199 sylanbrc φ bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B
201 elun1 bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
202 200 201 syl φ bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
203 182 202 eqeltrid φ bday 0 s + bday 0 s bday A + bday W bday V + bday S bday A + bday S bday V + bday W bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
204 1 45 45 2 10 47 49 203 mulsproplem1 φ 0 s s 0 s No A < s V W < s S A s S - s A s W < s V s S - s V s W
205 204 simprd φ A < s V W < s S A s S - s A s W < s V s S - s V s W
206 179 43 205 mp2and φ A s S - s A s W < s V s S - s V s W
207 1 30 17 mulsproplem4 φ V s S No
208 18 207 25 33 sltsubsubbd φ A s S - s A s W < s V s S - s V s W A s S - s V s S < s A s W - s V s W
209 18 207 subscld φ A s S - s V s S No
210 25 33 subscld φ A s W - s V s W No
211 209 210 31 sltadd2d φ A s S - s V s S < s A s W - s V s W V s B + s A s S - s V s S < s V s B + s A s W - s V s W
212 208 211 bitrd φ A s S - s A s W < s V s S - s V s W V s B + s A s S - s V s S < s V s B + s A s W - s V s W
213 206 212 mpbid φ V s B + s A s S - s V s S < s V s B + s A s W - s V s W
214 31 18 207 addsubsassd φ V s B + s A s S - s V s S = V s B + s A s S - s V s S
215 31 25 33 addsubsassd φ V s B + s A s W - s V s W = V s B + s A s W - s V s W
216 213 214 215 3brtr4d φ V s B + s A s S - s V s S < s V s B + s A s W - s V s W
217 oveq1 R = V R s B = V s B
218 217 oveq1d R = V R s B + s A s S = V s B + s A s S
219 oveq1 R = V R s S = V s S
220 218 219 oveq12d R = V R s B + s A s S - s R s S = V s B + s A s S - s V s S
221 220 breq1d R = V R s B + s A s S - s R s S < s V s B + s A s W - s V s W V s B + s A s S - s V s S < s V s B + s A s W - s V s W
222 216 221 syl5ibrcom φ R = V R s B + s A s S - s R s S < s V s B + s A s W - s V s W
223 21 adantr φ V < s R R s B + s A s S - s R s S No
224 31 18 addscld φ V s B + s A s S No
225 224 207 subscld φ V s B + s A s S - s V s S No
226 225 adantr φ V < s R V s B + s A s S - s V s S No
227 34 adantr φ V < s R V s B + s A s W - s V s W No
228 ssltright B No B s R B
229 3 228 syl φ B s R B
230 229 124 5 ssltsepcd φ B < s S
231 55 uneq1i bday 0 s + bday 0 s bday V + bday B bday R + bday S bday V + bday S bday R + bday B = bday V + bday B bday R + bday S bday V + bday S bday R + bday B
232 0un bday V + bday B bday R + bday S bday V + bday S bday R + bday B = bday V + bday B bday R + bday S bday V + bday S bday R + bday B
233 231 232 eqtri bday 0 s + bday 0 s bday V + bday B bday R + bday S bday V + bday S bday R + bday B = bday V + bday B bday R + bday S bday V + bday S bday R + bday B
234 134 73 jca φ bday V + bday B bday A + bday B bday R + bday S bday A + bday B
235 185 138 jca φ bday V + bday S bday A + bday B bday R + bday B bday A + bday B
236 144 87 onun2i bday V + bday B bday R + bday S On
237 189 147 onun2i bday V + bday S bday R + bday B On
238 onunel bday V + bday B bday R + bday S On bday V + bday S bday R + bday B On bday A + bday B On bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday V + bday B bday R + bday S bday A + bday B bday V + bday S bday R + bday B bday A + bday B
239 236 237 95 238 mp3an bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday V + bday B bday R + bday S bday A + bday B bday V + bday S bday R + bday B bday A + bday B
240 onunel bday V + bday B On bday R + bday S On bday A + bday B On bday V + bday B bday R + bday S bday A + bday B bday V + bday B bday A + bday B bday R + bday S bday A + bday B
241 144 87 95 240 mp3an bday V + bday B bday R + bday S bday A + bday B bday V + bday B bday A + bday B bday R + bday S bday A + bday B
242 onunel bday V + bday S On bday R + bday B On bday A + bday B On bday V + bday S bday R + bday B bday A + bday B bday V + bday S bday A + bday B bday R + bday B bday A + bday B
243 189 147 95 242 mp3an bday V + bday S bday R + bday B bday A + bday B bday V + bday S bday A + bday B bday R + bday B bday A + bday B
244 241 243 anbi12i bday V + bday B bday R + bday S bday A + bday B bday V + bday S bday R + bday B bday A + bday B bday V + bday B bday A + bday B bday R + bday S bday A + bday B bday V + bday S bday A + bday B bday R + bday B bday A + bday B
245 239 244 bitri bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday V + bday B bday A + bday B bday R + bday S bday A + bday B bday V + bday S bday A + bday B bday R + bday B bday A + bday B
246 234 235 245 sylanbrc φ bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B
247 elun1 bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
248 246 247 syl φ bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
249 233 248 eqeltrid φ bday 0 s + bday 0 s bday V + bday B bday R + bday S bday V + bday S bday R + bday B bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
250 1 45 45 10 9 3 49 249 mulsproplem1 φ 0 s s 0 s No V < s R B < s S V s S - s V s B < s R s S - s R s B
251 250 simprd φ V < s R B < s S V s S - s V s B < s R s S - s R s B
252 230 251 mpan2d φ V < s R V s S - s V s B < s R s S - s R s B
253 252 imp φ V < s R V s S - s V s B < s R s S - s R s B
254 207 31 20 15 sltsubsub2bd φ V s S - s V s B < s R s S - s R s B R s B - s R s S < s V s B - s V s S
255 15 20 subscld φ R s B - s R s S No
256 31 207 subscld φ V s B - s V s S No
257 255 256 18 sltadd1d φ R s B - s R s S < s V s B - s V s S R s B - s R s S + s A s S < s V s B - s V s S + s A s S
258 254 257 bitrd φ V s S - s V s B < s R s S - s R s B R s B - s R s S + s A s S < s V s B - s V s S + s A s S
259 258 adantr φ V < s R V s S - s V s B < s R s S - s R s B R s B - s R s S + s A s S < s V s B - s V s S + s A s S
260 253 259 mpbid φ V < s R R s B - s R s S + s A s S < s V s B - s V s S + s A s S
261 15 18 20 addsubsd φ R s B + s A s S - s R s S = R s B - s R s S + s A s S
262 261 adantr φ V < s R R s B + s A s S - s R s S = R s B - s R s S + s A s S
263 31 18 207 addsubsd φ V s B + s A s S - s V s S = V s B - s V s S + s A s S
264 263 adantr φ V < s R V s B + s A s S - s V s S = V s B - s V s S + s A s S
265 260 262 264 3brtr4d φ V < s R R s B + s A s S - s R s S < s V s B + s A s S - s V s S
266 216 adantr φ V < s R V s B + s A s S - s V s S < s V s B + s A s W - s V s W
267 223 226 227 265 266 slttrd φ V < s R R s B + s A s S - s R s S < s V s B + s A s W - s V s W
268 267 ex φ V < s R R s B + s A s S - s R s S < s V s B + s A s W - s V s W
269 178 222 268 3jaod φ R < s V R = V V < s R R s B + s A s S - s R s S < s V s B + s A s W - s V s W
270 12 269 mpd φ R s B + s A s S - s R s S < s V s B + s A s W - s V s W