Metamath Proof Explorer


Theorem mulsproplem14

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