Metamath Proof Explorer


Theorem mulsproplem5

Description: Lemma for surreal multiplication. Show one of the inequalities involved in surreal multiplication's cuts. (Contributed by Scott Fenton, 4-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
mulsproplem5.1 φ A No
mulsproplem5.2 φ B No
mulsproplem5.3 φ P L A
mulsproplem5.4 φ Q L B
mulsproplem5.5 φ T L A
mulsproplem5.6 φ U R B
Assertion mulsproplem5 φ P s B + s A s Q - s P s Q < s T s B + s A s U - s T s U

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