Metamath Proof Explorer


Theorem mulsproplem13

Description: Lemma for surreal multiplication. Remove the restriction on C and D from mulsproplem12 . (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
mulsproplem.2 φ C No
mulsproplem.3 φ D No
mulsproplem.4 φ E No
mulsproplem.5 φ F No
mulsproplem.6 φ C < s D
mulsproplem.7 φ E < s F
mulsproplem13.1 φ bday E bday F bday F bday E
Assertion mulsproplem13 φ C s F - s C s E < s D s F - s D s E

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 mulsproplem.2 φ C No
3 mulsproplem.3 φ D No
4 mulsproplem.4 φ E No
5 mulsproplem.5 φ F No
6 mulsproplem.6 φ C < s D
7 mulsproplem.7 φ E < s F
8 mulsproplem13.1 φ bday E bday F bday F bday E
9 1 adantr φ bday C bday D bday D bday C 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
10 2 adantr φ bday C bday D bday D bday C C No
11 3 adantr φ bday C bday D bday D bday C D No
12 4 adantr φ bday C bday D bday D bday C E No
13 5 adantr φ bday C bday D bday D bday C F No
14 6 adantr φ bday C bday D bday D bday C C < s D
15 7 adantr φ bday C bday D bday D bday C E < s F
16 simpr φ bday C bday D bday D bday C bday C bday D bday D bday C
17 8 adantr φ bday C bday D bday D bday C bday E bday F bday F bday E
18 9 10 11 12 13 14 15 16 17 mulsproplem12 φ bday C bday D bday D bday C C s F - s C s E < s D s F - s D s E
19 2 adantr φ bday C = bday D C No
20 3 adantr φ bday C = bday D D No
21 simpr φ bday C = bday D bday C = bday D
22 6 adantr φ bday C = bday D C < s D
23 nodense C No D No bday C = bday D C < s D x No bday x bday C C < s x x < s D
24 19 20 21 22 23 syl22anc φ bday C = bday D x No bday x bday C C < s x x < s D
25 unidm bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday 0 s + bday 0 s bday 0 s + bday 0 s
26 unidm bday 0 s + bday 0 s bday 0 s + bday 0 s = bday 0 s + bday 0 s
27 bday0s bday 0 s =
28 27 27 oveq12i bday 0 s + bday 0 s = +
29 0elon On
30 naddrid On + =
31 29 30 ax-mp + =
32 28 31 eqtri bday 0 s + bday 0 s =
33 25 26 32 3eqtri bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s =
34 33 uneq2i bday C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday C + bday F
35 un0 bday C + bday F = bday C + bday F
36 34 35 eqtri bday C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday C + bday F
37 ssun1 bday C + bday F bday C + bday F bday D + bday E
38 ssun2 bday C + bday F bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
39 37 38 sstri bday C + bday F bday C + bday E bday D + bday F bday C + bday F bday D + bday E
40 ssun2 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
41 39 40 sstri bday C + bday F bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
42 36 41 eqsstri bday C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
43 42 sseli bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
44 43 imim1i 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 bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
45 44 6ralimi 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 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 C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
46 1 45 syl φ 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 C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
47 46 2 5 mulsproplem11 φ C s F No
48 33 uneq2i bday C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday C + bday E
49 un0 bday C + bday E = bday C + bday E
50 48 49 eqtri bday C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday C + bday E
51 ssun1 bday C + bday E bday C + bday E bday D + bday F
52 ssun1 bday C + bday E bday D + bday F bday C + bday E bday D + bday F bday C + bday F bday D + bday E
53 51 52 sstri bday C + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
54 53 40 sstri bday C + bday E bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
55 50 54 eqsstri bday C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
56 55 sseli bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
57 56 imim1i 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 bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
58 57 6ralimi 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 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 C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
59 1 58 syl φ 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 C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
60 59 2 4 mulsproplem11 φ C s E No
61 47 60 subscld φ C s F - s C s E No
62 61 adantr φ bday C = bday D x No bday x bday C C < s x x < s D C s F - s C s E No
63 46 adantr φ bday C = bday D x No bday x bday C C < s x x < s D 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 C + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
64 simprr1 bday C = bday D x No bday x bday C C < s x x < s D bday x bday C
65 64 adantl φ bday C = bday D x No bday x bday C C < s x x < s D bday x bday C
66 bdayelon bday C On
67 simprrl φ bday C = bday D x No bday x bday C C < s x x < s D x No
68 oldbday bday C On x No x Old bday C bday x bday C
69 66 67 68 sylancr φ bday C = bday D x No bday x bday C C < s x x < s D x Old bday C bday x bday C
70 65 69 mpbird φ bday C = bday D x No bday x bday C C < s x x < s D x Old bday C
71 5 adantr φ bday C = bday D x No bday x bday C C < s x x < s D F No
72 63 70 71 mulsproplem2 φ bday C = bday D x No bday x bday C C < s x x < s D x s F No
73 59 adantr φ bday C = bday D x No bday x bday C C < s x x < s D 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 C + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
74 4 adantr φ bday C = bday D x No bday x bday C C < s x x < s D E No
75 73 70 74 mulsproplem2 φ bday C = bday D x No bday x bday C C < s x x < s D x s E No
76 72 75 subscld φ bday C = bday D x No bday x bday C C < s x x < s D x s F - s x s E No
77 33 uneq2i bday D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday D + bday F
78 un0 bday D + bday F = bday D + bday F
79 77 78 eqtri bday D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday D + bday F
80 ssun2 bday D + bday F bday C + bday E bday D + bday F
81 80 52 sstri bday D + bday F bday C + bday E bday D + bday F bday C + bday F bday D + bday E
82 81 40 sstri bday D + bday F bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
83 79 82 eqsstri bday D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
84 83 sseli bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
85 84 imim1i 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 bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
86 85 6ralimi 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 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 D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
87 1 86 syl φ 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 D + bday F bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
88 87 3 5 mulsproplem11 φ D s F No
89 33 uneq2i bday D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday D + bday E
90 un0 bday D + bday E = bday D + bday E
91 89 90 eqtri bday D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s = bday D + bday E
92 ssun2 bday D + bday E bday C + bday F bday D + bday E
93 92 38 sstri bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
94 93 40 sstri bday D + bday E bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
95 91 94 eqsstri bday D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
96 95 sseli bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
97 96 imim1i 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 bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
98 97 6ralimi 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 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 D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
99 1 98 syl φ 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 D + bday E bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s 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
100 99 3 4 mulsproplem11 φ D s E No
101 88 100 subscld φ D s F - s D s E No
102 101 adantr φ bday C = bday D x No bday x bday C C < s x x < s D D s F - s D s E No
103 1 mulsproplemcbv φ g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
104 103 adantr φ bday C = bday D x No bday x bday C C < s x x < s D g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
105 onelss bday C On bday x bday C bday x bday C
106 66 65 105 mpsyl φ bday C = bday D x No bday x bday C C < s x x < s D bday x bday C
107 simprl φ bday C = bday D x No bday x bday C C < s x x < s D bday C = bday D
108 106 107 sseqtrd φ bday C = bday D x No bday x bday C C < s x x < s D bday x bday D
109 bdayelon bday x On
110 bdayelon bday D On
111 bdayelon bday F On
112 naddss1 bday x On bday D On bday F On bday x bday D bday x + bday F bday D + bday F
113 109 110 111 112 mp3an bday x bday D bday x + bday F bday D + bday F
114 108 113 sylib φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday F bday D + bday F
115 unss2 bday x + bday F bday D + bday F bday C + bday E bday x + bday F bday C + bday E bday D + bday F
116 114 115 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday C + bday E bday x + bday F bday C + bday E bday D + bday F
117 bdayelon bday E On
118 naddss1 bday x On bday D On bday E On bday x bday D bday x + bday E bday D + bday E
119 109 110 117 118 mp3an bday x bday D bday x + bday E bday D + bday E
120 108 119 sylib φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday E bday D + bday E
121 unss2 bday x + bday E bday D + bday E bday C + bday F bday x + bday E bday C + bday F bday D + bday E
122 120 121 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday C + bday F bday x + bday E bday C + bday F bday D + bday E
123 unss12 bday C + bday E bday x + bday F bday C + bday E bday D + bday F bday C + bday F bday x + bday E bday C + bday F bday D + bday E bday C + bday E bday x + bday F bday C + bday F bday x + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
124 116 122 123 syl2anc φ bday C = bday D x No bday x bday C C < s x x < s D bday C + bday E bday x + bday F bday C + bday F bday x + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
125 unss2 bday C + bday E bday x + bday F bday C + bday F bday x + bday E 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 x + bday F bday C + bday F bday x + bday E bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
126 124 125 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday A + bday B bday C + bday E bday x + bday F bday C + bday F bday x + bday E bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
127 126 sseld φ bday C = bday D x No bday x bday C C < s x x < s D bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday x + bday F bday C + bday F bday x + bday E bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
128 127 imim1d φ bday C = bday D x No bday x bday C C < s x x < s D bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday x + bday F bday C + bday F bday x + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
129 128 ralimd6v φ bday C = bday D x No bday x bday C C < s x x < s D g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday x + bday F bday C + bday F bday x + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
130 104 129 mpd φ bday C = bday D x No bday x bday C C < s x x < s D g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday x + bday F bday C + bday F bday x + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
131 2 adantr φ bday C = bday D x No bday x bday C C < s x x < s D C No
132 simprr2 bday C = bday D x No bday x bday C C < s x x < s D C < s x
133 132 adantl φ bday C = bday D x No bday x bday C C < s x x < s D C < s x
134 7 adantr φ bday C = bday D x No bday x bday C C < s x x < s D E < s F
135 65 olcd φ bday C = bday D x No bday x bday C C < s x x < s D bday C bday x bday x bday C
136 8 adantr φ bday C = bday D x No bday x bday C C < s x x < s D bday E bday F bday F bday E
137 130 131 67 74 71 133 134 135 136 mulsproplem12 φ bday C = bday D x No bday x bday C C < s x x < s D C s F - s C s E < s x s F - s x s E
138 naddss1 bday x On bday C On bday E On bday x bday C bday x + bday E bday C + bday E
139 109 66 117 138 mp3an bday x bday C bday x + bday E bday C + bday E
140 106 139 sylib φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday E bday C + bday E
141 unss1 bday x + bday E bday C + bday E bday x + bday E bday D + bday F bday C + bday E bday D + bday F
142 140 141 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday E bday D + bday F bday C + bday E bday D + bday F
143 naddss1 bday x On bday C On bday F On bday x bday C bday x + bday F bday C + bday F
144 109 66 111 143 mp3an bday x bday C bday x + bday F bday C + bday F
145 106 144 sylib φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday F bday C + bday F
146 unss1 bday x + bday F bday C + bday F bday x + bday F bday D + bday E bday C + bday F bday D + bday E
147 145 146 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday F bday D + bday E bday C + bday F bday D + bday E
148 unss12 bday x + bday E bday D + bday F bday C + bday E bday D + bday F bday x + bday F bday D + bday E bday C + bday F bday D + bday E bday x + bday E bday D + bday F bday x + bday F bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
149 142 147 148 syl2anc φ bday C = bday D x No bday x bday C C < s x x < s D bday x + bday E bday D + bday F bday x + bday F bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
150 unss2 bday x + bday E bday D + bday F bday x + bday F bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday A + bday B bday x + bday E bday D + bday F bday x + 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
151 149 150 syl φ bday C = bday D x No bday x bday C C < s x x < s D bday A + bday B bday x + bday E bday D + bday F bday x + 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
152 151 sseld φ bday C = bday D x No bday x bday C C < s x x < s D bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday x + bday E bday D + bday F bday x + bday F bday D + bday E bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
153 152 imim1d φ bday C = bday D x No bday x bday C C < s x x < s D bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday x + bday E bday D + bday F bday x + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
154 153 ralimd6v φ bday C = bday D x No bday x bday C C < s x x < s D g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday x + bday E bday D + bday F bday x + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
155 104 154 mpd φ bday C = bday D x No bday x bday C C < s x x < s D g No h No i No j No k No l No bday g + bday h bday i + bday k bday j + bday l bday i + bday l bday j + bday k bday A + bday B bday x + bday E bday D + bday F bday x + bday F bday D + bday E g s h No i < s j k < s l i s l - s i s k < s j s l - s j s k
156 3 adantr φ bday C = bday D x No bday x bday C C < s x x < s D D No
157 simprr3 bday C = bday D x No bday x bday C C < s x x < s D x < s D
158 157 adantl φ bday C = bday D x No bday x bday C C < s x x < s D x < s D
159 65 107 eleqtrd φ bday C = bday D x No bday x bday C C < s x x < s D bday x bday D
160 159 orcd φ bday C = bday D x No bday x bday C C < s x x < s D bday x bday D bday D bday x
161 155 67 156 74 71 158 134 160 136 mulsproplem12 φ bday C = bday D x No bday x bday C C < s x x < s D x s F - s x s E < s D s F - s D s E
162 62 76 102 137 161 slttrd φ bday C = bday D x No bday x bday C C < s x x < s D C s F - s C s E < s D s F - s D s E
163 162 anassrs φ bday C = bday D x No bday x bday C C < s x x < s D C s F - s C s E < s D s F - s D s E
164 24 163 rexlimddv φ bday C = bday D C s F - s C s E < s D s F - s D s E
165 66 onordi Ord bday C
166 110 onordi Ord bday D
167 ordtri3or Ord bday C Ord bday D bday C bday D bday C = bday D bday D bday C
168 165 166 167 mp2an bday C bday D bday C = bday D bday D bday C
169 df-3or bday C bday D bday C = bday D bday D bday C bday C bday D bday C = bday D bday D bday C
170 or32 bday C bday D bday C = bday D bday D bday C bday C bday D bday D bday C bday C = bday D
171 169 170 bitri bday C bday D bday C = bday D bday D bday C bday C bday D bday D bday C bday C = bday D
172 168 171 mpbi bday C bday D bday D bday C bday C = bday D
173 172 a1i φ bday C bday D bday D bday C bday C = bday D
174 18 164 173 mpjaodan φ C s F - s C s E < s D s F - s D s E