Metamath Proof Explorer


Theorem mulsproplem7

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