Metamath Proof Explorer


Theorem mulsproplem6

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