Metamath Proof Explorer


Theorem mulsproplem12

Description: Lemma for surreal multiplication. Demonstrate the second half of the inductive statement assuming C and D are not the same age and E and F are not the same age. (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
mulsproplem12.1 φ bday C bday D bday D bday C
mulsproplem12.2 φ bday E bday F bday F bday E
Assertion mulsproplem12 φ 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 mulsproplem12.1 φ bday C bday D bday D bday C
9 mulsproplem12.2 φ bday E bday F bday F bday E
10 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
11 unidm bday 0 s + bday 0 s bday 0 s + bday 0 s = bday 0 s + bday 0 s
12 bday0s bday 0 s =
13 12 12 oveq12i bday 0 s + bday 0 s = +
14 0elon On
15 naddrid On + =
16 14 15 ax-mp + =
17 13 16 eqtri bday 0 s + bday 0 s =
18 11 17 eqtri bday 0 s + bday 0 s bday 0 s + bday 0 s =
19 10 18 eqtri bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s bday 0 s + bday 0 s =
20 19 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
21 un0 bday D + bday F = bday D + bday F
22 20 21 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
23 ssun2 bday D + bday F bday C + bday E bday D + bday F
24 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
25 23 24 sstri bday D + bday F bday C + bday E bday D + bday F bday C + bday F bday D + bday E
26 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
27 25 26 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
28 22 27 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
29 28 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
30 29 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
31 30 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
32 1 31 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
33 32 3 5 mulsproplem10 φ D s F No g | p L D q L F g = p s F + s D s q - s p s q h | r R D s R F h = r s F + s D s s - s r s s s D s F D s F s i | t L D u R F i = t s F + s D s u - s t s u j | v R D w L F j = v s F + s D s w - s v s w
34 33 simp2d φ g | p L D q L F g = p s F + s D s q - s p s q h | r R D s R F h = r s F + s D s s - s r s s s D s F
35 34 adantr φ bday C bday D bday E bday F g | p L D q L F g = p s F + s D s q - s p s q h | r R D s R F h = r s F + s D s s - s r s s s D s F
36 simprl φ bday C bday D bday E bday F bday C bday D
37 bdayelon bday D On
38 2 adantr φ bday C bday D bday E bday F C No
39 oldbday bday D On C No C Old bday D bday C bday D
40 37 38 39 sylancr φ bday C bday D bday E bday F C Old bday D bday C bday D
41 36 40 mpbird φ bday C bday D bday E bday F C Old bday D
42 6 adantr φ bday C bday D bday E bday F C < s D
43 breq1 x = C x < s D C < s D
44 leftval L D = x Old bday D | x < s D
45 43 44 elrab2 C L D C Old bday D C < s D
46 41 42 45 sylanbrc φ bday C bday D bday E bday F C L D
47 simprr φ bday C bday D bday E bday F bday E bday F
48 bdayelon bday F On
49 4 adantr φ bday C bday D bday E bday F E No
50 oldbday bday F On E No E Old bday F bday E bday F
51 48 49 50 sylancr φ bday C bday D bday E bday F E Old bday F bday E bday F
52 47 51 mpbird φ bday C bday D bday E bday F E Old bday F
53 7 adantr φ bday C bday D bday E bday F E < s F
54 breq1 x = E x < s F E < s F
55 leftval L F = x Old bday F | x < s F
56 54 55 elrab2 E L F E Old bday F E < s F
57 52 53 56 sylanbrc φ bday C bday D bday E bday F E L F
58 eqid C s F + s D s E - s C s E = C s F + s D s E - s C s E
59 oveq1 p = C p s F = C s F
60 59 oveq1d p = C p s F + s D s q = C s F + s D s q
61 oveq1 p = C p s q = C s q
62 60 61 oveq12d p = C p s F + s D s q - s p s q = C s F + s D s q - s C s q
63 62 eqeq2d p = C C s F + s D s E - s C s E = p s F + s D s q - s p s q C s F + s D s E - s C s E = C s F + s D s q - s C s q
64 oveq2 q = E D s q = D s E
65 64 oveq2d q = E C s F + s D s q = C s F + s D s E
66 oveq2 q = E C s q = C s E
67 65 66 oveq12d q = E C s F + s D s q - s C s q = C s F + s D s E - s C s E
68 67 eqeq2d q = E C s F + s D s E - s C s E = C s F + s D s q - s C s q C s F + s D s E - s C s E = C s F + s D s E - s C s E
69 63 68 rspc2ev C L D E L F C s F + s D s E - s C s E = C s F + s D s E - s C s E p L D q L F C s F + s D s E - s C s E = p s F + s D s q - s p s q
70 58 69 mp3an3 C L D E L F p L D q L F C s F + s D s E - s C s E = p s F + s D s q - s p s q
71 46 57 70 syl2anc φ bday C bday D bday E bday F p L D q L F C s F + s D s E - s C s E = p s F + s D s q - s p s q
72 ovex C s F + s D s E - s C s E V
73 eqeq1 g = C s F + s D s E - s C s E g = p s F + s D s q - s p s q C s F + s D s E - s C s E = p s F + s D s q - s p s q
74 73 2rexbidv g = C s F + s D s E - s C s E p L D q L F g = p s F + s D s q - s p s q p L D q L F C s F + s D s E - s C s E = p s F + s D s q - s p s q
75 72 74 elab C s F + s D s E - s C s E g | p L D q L F g = p s F + s D s q - s p s q p L D q L F C s F + s D s E - s C s E = p s F + s D s q - s p s q
76 71 75 sylibr φ bday C bday D bday E bday F C s F + s D s E - s C s E g | p L D q L F g = p s F + s D s q - s p s q
77 elun1 C s F + s D s E - s C s E g | p L D q L F g = p s F + s D s q - s p s q C s F + s D s E - s C s E g | p L D q L F g = p s F + s D s q - s p s q h | r R D s R F h = r s F + s D s s - s r s s
78 76 77 syl φ bday C bday D bday E bday F C s F + s D s E - s C s E g | p L D q L F g = p s F + s D s q - s p s q h | r R D s R F h = r s F + s D s s - s r s s
79 ovex D s F V
80 79 snid D s F D s F
81 80 a1i φ bday C bday D bday E bday F D s F D s F
82 35 78 81 ssltsepcd φ bday C bday D bday E bday F C s F + s D s E - s C s E < s D s F
83 19 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
84 un0 bday C + bday F = bday C + bday F
85 83 84 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
86 ssun1 bday C + bday F bday C + bday F bday D + bday E
87 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
88 86 87 sstri bday C + bday F bday C + bday E bday D + bday F bday C + bday F bday D + bday E
89 88 26 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
90 85 89 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
91 90 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
92 91 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
93 92 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
94 1 93 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
95 94 2 5 mulsproplem10 φ C s F No g | p L C q L F g = p s F + s C s q - s p s q h | r R C s R F h = r s F + s C s s - s r s s s C s F C s F s i | t L C u R F i = t s F + s C s u - s t s u j | v R C w L F j = v s F + s C s w - s v s w
96 95 simp1d φ C s F No
97 19 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
98 un0 bday D + bday E = bday D + bday E
99 97 98 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
100 ssun2 bday D + bday E bday C + bday F bday D + bday E
101 100 87 sstri bday D + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
102 101 26 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
103 99 102 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
104 103 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
105 104 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
106 105 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
107 1 106 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
108 107 3 4 mulsproplem10 φ D s E No g | p L D q L E g = p s E + s D s q - s p s q h | r R D s R E h = r s E + s D s s - s r s s s D s E D s E s i | t L D u R E i = t s E + s D s u - s t s u j | v R D w L E j = v s E + s D s w - s v s w
109 108 simp1d φ D s E No
110 96 109 addscomd φ C s F + s D s E = D s E + s C s F
111 110 oveq1d φ C s F + s D s E - s C s E = D s E + s C s F - s C s E
112 19 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
113 un0 bday C + bday E = bday C + bday E
114 112 113 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
115 ssun1 bday C + bday E bday C + bday E bday D + bday F
116 115 24 sstri bday C + bday E bday C + bday E bday D + bday F bday C + bday F bday D + bday E
117 116 26 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
118 114 117 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
119 118 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
120 119 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
121 120 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
122 1 121 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
123 122 2 4 mulsproplem10 φ C s E No g | p L C q L E g = p s E + s C s q - s p s q h | r R C s R E h = r s E + s C s s - s r s s s C s E C s E s i | t L C u R E i = t s E + s C s u - s t s u j | v R C w L E j = v s E + s C s w - s v s w
124 123 simp1d φ C s E No
125 109 96 124 addsubsassd φ D s E + s C s F - s C s E = D s E + s C s F - s C s E
126 111 125 eqtrd φ C s F + s D s E - s C s E = D s E + s C s F - s C s E
127 126 breq1d φ C s F + s D s E - s C s E < s D s F D s E + s C s F - s C s E < s D s F
128 96 124 subscld φ C s F - s C s E No
129 33 simp1d φ D s F No
130 109 128 129 sltaddsub2d φ D s E + s C s F - s C s E < s D s F C s F - s C s E < s D s F - s D s E
131 127 130 bitrd φ C s F + s D s E - s C s E < s D s F C s F - s C s E < s D s F - s D s E
132 131 adantr φ bday C bday D bday E bday F C s F + s D s E - s C s E < s D s F C s F - s C s E < s D s F - s D s E
133 82 132 mpbid φ bday C bday D bday E bday F C s F - s C s E < s D s F - s D s E
134 133 anassrs φ bday C bday D bday E bday F C s F - s C s E < s D s F - s D s E
135 108 simp3d φ D s E s i | t L D u R E i = t s E + s D s u - s t s u j | v R D w L E j = v s E + s D s w - s v s w
136 135 adantr φ bday C bday D bday F bday E D s E s i | t L D u R E i = t s E + s D s u - s t s u j | v R D w L E j = v s E + s D s w - s v s w
137 ovex D s E V
138 137 snid D s E D s E
139 138 a1i φ bday C bday D bday F bday E D s E D s E
140 simprl φ bday C bday D bday F bday E bday C bday D
141 2 adantr φ bday C bday D bday F bday E C No
142 37 141 39 sylancr φ bday C bday D bday F bday E C Old bday D bday C bday D
143 140 142 mpbird φ bday C bday D bday F bday E C Old bday D
144 6 adantr φ bday C bday D bday F bday E C < s D
145 143 144 45 sylanbrc φ bday C bday D bday F bday E C L D
146 simprr φ bday C bday D bday F bday E bday F bday E
147 bdayelon bday E On
148 5 adantr φ bday C bday D bday F bday E F No
149 oldbday bday E On F No F Old bday E bday F bday E
150 147 148 149 sylancr φ bday C bday D bday F bday E F Old bday E bday F bday E
151 146 150 mpbird φ bday C bday D bday F bday E F Old bday E
152 7 adantr φ bday C bday D bday F bday E E < s F
153 breq2 x = F E < s x E < s F
154 rightval R E = x Old bday E | E < s x
155 153 154 elrab2 F R E F Old bday E E < s F
156 151 152 155 sylanbrc φ bday C bday D bday F bday E F R E
157 eqid C s E + s D s F - s C s F = C s E + s D s F - s C s F
158 oveq1 t = C t s E = C s E
159 158 oveq1d t = C t s E + s D s u = C s E + s D s u
160 oveq1 t = C t s u = C s u
161 159 160 oveq12d t = C t s E + s D s u - s t s u = C s E + s D s u - s C s u
162 161 eqeq2d t = C C s E + s D s F - s C s F = t s E + s D s u - s t s u C s E + s D s F - s C s F = C s E + s D s u - s C s u
163 oveq2 u = F D s u = D s F
164 163 oveq2d u = F C s E + s D s u = C s E + s D s F
165 oveq2 u = F C s u = C s F
166 164 165 oveq12d u = F C s E + s D s u - s C s u = C s E + s D s F - s C s F
167 166 eqeq2d u = F C s E + s D s F - s C s F = C s E + s D s u - s C s u C s E + s D s F - s C s F = C s E + s D s F - s C s F
168 162 167 rspc2ev C L D F R E C s E + s D s F - s C s F = C s E + s D s F - s C s F t L D u R E C s E + s D s F - s C s F = t s E + s D s u - s t s u
169 157 168 mp3an3 C L D F R E t L D u R E C s E + s D s F - s C s F = t s E + s D s u - s t s u
170 145 156 169 syl2anc φ bday C bday D bday F bday E t L D u R E C s E + s D s F - s C s F = t s E + s D s u - s t s u
171 ovex C s E + s D s F - s C s F V
172 eqeq1 i = C s E + s D s F - s C s F i = t s E + s D s u - s t s u C s E + s D s F - s C s F = t s E + s D s u - s t s u
173 172 2rexbidv i = C s E + s D s F - s C s F t L D u R E i = t s E + s D s u - s t s u t L D u R E C s E + s D s F - s C s F = t s E + s D s u - s t s u
174 171 173 elab C s E + s D s F - s C s F i | t L D u R E i = t s E + s D s u - s t s u t L D u R E C s E + s D s F - s C s F = t s E + s D s u - s t s u
175 170 174 sylibr φ bday C bday D bday F bday E C s E + s D s F - s C s F i | t L D u R E i = t s E + s D s u - s t s u
176 elun1 C s E + s D s F - s C s F i | t L D u R E i = t s E + s D s u - s t s u C s E + s D s F - s C s F i | t L D u R E i = t s E + s D s u - s t s u j | v R D w L E j = v s E + s D s w - s v s w
177 175 176 syl φ bday C bday D bday F bday E C s E + s D s F - s C s F i | t L D u R E i = t s E + s D s u - s t s u j | v R D w L E j = v s E + s D s w - s v s w
178 136 139 177 ssltsepcd φ bday C bday D bday F bday E D s E < s C s E + s D s F - s C s F
179 124 129 addscomd φ C s E + s D s F = D s F + s C s E
180 179 oveq1d φ C s E + s D s F - s C s F = D s F + s C s E - s C s F
181 129 124 96 addsubsassd φ D s F + s C s E - s C s F = D s F + s C s E - s C s F
182 180 181 eqtrd φ C s E + s D s F - s C s F = D s F + s C s E - s C s F
183 182 breq2d φ D s E < s C s E + s D s F - s C s F D s E < s D s F + s C s E - s C s F
184 124 96 subscld φ C s E - s C s F No
185 109 129 184 sltsubadd2d φ D s E - s D s F < s C s E - s C s F D s E < s D s F + s C s E - s C s F
186 183 185 bitr4d φ D s E < s C s E + s D s F - s C s F D s E - s D s F < s C s E - s C s F
187 109 129 124 96 sltsubsub2bd φ D s E - s D s F < s C s E - s C s F C s F - s C s E < s D s F - s D s E
188 186 187 bitrd φ 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
189 188 adantr φ bday C bday D bday F bday E 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
190 178 189 mpbid φ bday C bday D bday F bday E C s F - s C s E < s D s F - s D s E
191 190 anassrs φ bday C bday D bday F bday E C s F - s C s E < s D s F - s D s E
192 9 adantr φ bday C bday D bday E bday F bday F bday E
193 134 191 192 mpjaodan φ bday C bday D C s F - s C s E < s D s F - s D s E
194 95 simp3d φ C s F s i | t L C u R F i = t s F + s C s u - s t s u j | v R C w L F j = v s F + s C s w - s v s w
195 194 adantr φ bday D bday C bday E bday F C s F s i | t L C u R F i = t s F + s C s u - s t s u j | v R C w L F j = v s F + s C s w - s v s w
196 ovex C s F V
197 196 snid C s F C s F
198 197 a1i φ bday D bday C bday E bday F C s F C s F
199 simprl φ bday D bday C bday E bday F bday D bday C
200 bdayelon bday C On
201 3 adantr φ bday D bday C bday E bday F D No
202 oldbday bday C On D No D Old bday C bday D bday C
203 200 201 202 sylancr φ bday D bday C bday E bday F D Old bday C bday D bday C
204 199 203 mpbird φ bday D bday C bday E bday F D Old bday C
205 6 adantr φ bday D bday C bday E bday F C < s D
206 breq2 x = D C < s x C < s D
207 rightval R C = x Old bday C | C < s x
208 206 207 elrab2 D R C D Old bday C C < s D
209 204 205 208 sylanbrc φ bday D bday C bday E bday F D R C
210 simprr φ bday D bday C bday E bday F bday E bday F
211 4 adantr φ bday D bday C bday E bday F E No
212 48 211 50 sylancr φ bday D bday C bday E bday F E Old bday F bday E bday F
213 210 212 mpbird φ bday D bday C bday E bday F E Old bday F
214 7 adantr φ bday D bday C bday E bday F E < s F
215 213 214 56 sylanbrc φ bday D bday C bday E bday F E L F
216 eqid D s F + s C s E - s D s E = D s F + s C s E - s D s E
217 oveq1 v = D v s F = D s F
218 217 oveq1d v = D v s F + s C s w = D s F + s C s w
219 oveq1 v = D v s w = D s w
220 218 219 oveq12d v = D v s F + s C s w - s v s w = D s F + s C s w - s D s w
221 220 eqeq2d v = D D s F + s C s E - s D s E = v s F + s C s w - s v s w D s F + s C s E - s D s E = D s F + s C s w - s D s w
222 oveq2 w = E C s w = C s E
223 222 oveq2d w = E D s F + s C s w = D s F + s C s E
224 oveq2 w = E D s w = D s E
225 223 224 oveq12d w = E D s F + s C s w - s D s w = D s F + s C s E - s D s E
226 225 eqeq2d w = E D s F + s C s E - s D s E = D s F + s C s w - s D s w D s F + s C s E - s D s E = D s F + s C s E - s D s E
227 221 226 rspc2ev D R C E L F D s F + s C s E - s D s E = D s F + s C s E - s D s E v R C w L F D s F + s C s E - s D s E = v s F + s C s w - s v s w
228 216 227 mp3an3 D R C E L F v R C w L F D s F + s C s E - s D s E = v s F + s C s w - s v s w
229 209 215 228 syl2anc φ bday D bday C bday E bday F v R C w L F D s F + s C s E - s D s E = v s F + s C s w - s v s w
230 ovex D s F + s C s E - s D s E V
231 eqeq1 j = D s F + s C s E - s D s E j = v s F + s C s w - s v s w D s F + s C s E - s D s E = v s F + s C s w - s v s w
232 231 2rexbidv j = D s F + s C s E - s D s E v R C w L F j = v s F + s C s w - s v s w v R C w L F D s F + s C s E - s D s E = v s F + s C s w - s v s w
233 230 232 elab D s F + s C s E - s D s E j | v R C w L F j = v s F + s C s w - s v s w v R C w L F D s F + s C s E - s D s E = v s F + s C s w - s v s w
234 229 233 sylibr φ bday D bday C bday E bday F D s F + s C s E - s D s E j | v R C w L F j = v s F + s C s w - s v s w
235 elun2 D s F + s C s E - s D s E j | v R C w L F j = v s F + s C s w - s v s w D s F + s C s E - s D s E i | t L C u R F i = t s F + s C s u - s t s u j | v R C w L F j = v s F + s C s w - s v s w
236 234 235 syl φ bday D bday C bday E bday F D s F + s C s E - s D s E i | t L C u R F i = t s F + s C s u - s t s u j | v R C w L F j = v s F + s C s w - s v s w
237 195 198 236 ssltsepcd φ bday D bday C bday E bday F C s F < s D s F + s C s E - s D s E
238 129 124 addscomd φ D s F + s C s E = C s E + s D s F
239 238 oveq1d φ D s F + s C s E - s D s E = C s E + s D s F - s D s E
240 124 129 109 addsubsassd φ C s E + s D s F - s D s E = C s E + s D s F - s D s E
241 239 240 eqtrd φ D s F + s C s E - s D s E = C s E + s D s F - s D s E
242 241 breq2d φ C s F < s D s F + s C s E - s D s E C s F < s C s E + s D s F - s D s E
243 129 109 subscld φ D s F - s D s E No
244 96 124 243 sltsubadd2d φ C s F - s C s E < s D s F - s D s E C s F < s C s E + s D s F - s D s E
245 242 244 bitr4d φ C s F < s D s F + s C s E - s D s E C s F - s C s E < s D s F - s D s E
246 245 adantr φ bday D bday C bday E bday F C s F < s D s F + s C s E - s D s E C s F - s C s E < s D s F - s D s E
247 237 246 mpbid φ bday D bday C bday E bday F C s F - s C s E < s D s F - s D s E
248 247 anassrs φ bday D bday C bday E bday F C s F - s C s E < s D s F - s D s E
249 123 simp2d φ g | p L C q L E g = p s E + s C s q - s p s q h | r R C s R E h = r s E + s C s s - s r s s s C s E
250 249 adantr φ bday D bday C bday F bday E g | p L C q L E g = p s E + s C s q - s p s q h | r R C s R E h = r s E + s C s s - s r s s s C s E
251 simprl φ bday D bday C bday F bday E bday D bday C
252 3 adantr φ bday D bday C bday F bday E D No
253 200 252 202 sylancr φ bday D bday C bday F bday E D Old bday C bday D bday C
254 251 253 mpbird φ bday D bday C bday F bday E D Old bday C
255 6 adantr φ bday D bday C bday F bday E C < s D
256 254 255 208 sylanbrc φ bday D bday C bday F bday E D R C
257 simprr φ bday D bday C bday F bday E bday F bday E
258 5 adantr φ bday D bday C bday F bday E F No
259 147 258 149 sylancr φ bday D bday C bday F bday E F Old bday E bday F bday E
260 257 259 mpbird φ bday D bday C bday F bday E F Old bday E
261 7 adantr φ bday D bday C bday F bday E E < s F
262 260 261 155 sylanbrc φ bday D bday C bday F bday E F R E
263 eqid D s E + s C s F - s D s F = D s E + s C s F - s D s F
264 oveq1 r = D r s E = D s E
265 264 oveq1d r = D r s E + s C s s = D s E + s C s s
266 oveq1 r = D r s s = D s s
267 265 266 oveq12d r = D r s E + s C s s - s r s s = D s E + s C s s - s D s s
268 267 eqeq2d r = D D s E + s C s F - s D s F = r s E + s C s s - s r s s D s E + s C s F - s D s F = D s E + s C s s - s D s s
269 oveq2 s = F C s s = C s F
270 269 oveq2d s = F D s E + s C s s = D s E + s C s F
271 oveq2 s = F D s s = D s F
272 270 271 oveq12d s = F D s E + s C s s - s D s s = D s E + s C s F - s D s F
273 272 eqeq2d s = F D s E + s C s F - s D s F = D s E + s C s s - s D s s D s E + s C s F - s D s F = D s E + s C s F - s D s F
274 268 273 rspc2ev D R C F R E D s E + s C s F - s D s F = D s E + s C s F - s D s F r R C s R E D s E + s C s F - s D s F = r s E + s C s s - s r s s
275 263 274 mp3an3 D R C F R E r R C s R E D s E + s C s F - s D s F = r s E + s C s s - s r s s
276 256 262 275 syl2anc φ bday D bday C bday F bday E r R C s R E D s E + s C s F - s D s F = r s E + s C s s - s r s s
277 ovex D s E + s C s F - s D s F V
278 eqeq1 h = D s E + s C s F - s D s F h = r s E + s C s s - s r s s D s E + s C s F - s D s F = r s E + s C s s - s r s s
279 278 2rexbidv h = D s E + s C s F - s D s F r R C s R E h = r s E + s C s s - s r s s r R C s R E D s E + s C s F - s D s F = r s E + s C s s - s r s s
280 277 279 elab D s E + s C s F - s D s F h | r R C s R E h = r s E + s C s s - s r s s r R C s R E D s E + s C s F - s D s F = r s E + s C s s - s r s s
281 276 280 sylibr φ bday D bday C bday F bday E D s E + s C s F - s D s F h | r R C s R E h = r s E + s C s s - s r s s
282 elun2 D s E + s C s F - s D s F h | r R C s R E h = r s E + s C s s - s r s s D s E + s C s F - s D s F g | p L C q L E g = p s E + s C s q - s p s q h | r R C s R E h = r s E + s C s s - s r s s
283 281 282 syl φ bday D bday C bday F bday E D s E + s C s F - s D s F g | p L C q L E g = p s E + s C s q - s p s q h | r R C s R E h = r s E + s C s s - s r s s
284 ovex C s E V
285 284 snid C s E C s E
286 285 a1i φ bday D bday C bday F bday E C s E C s E
287 250 283 286 ssltsepcd φ bday D bday C bday F bday E D s E + s C s F - s D s F < s C s E
288 109 96 addscomd φ D s E + s C s F = C s F + s D s E
289 288 oveq1d φ D s E + s C s F - s D s F = C s F + s D s E - s D s F
290 96 109 129 addsubsassd φ C s F + s D s E - s D s F = C s F + s D s E - s D s F
291 289 290 eqtrd φ D s E + s C s F - s D s F = C s F + s D s E - s D s F
292 291 breq1d φ D s E + s C s F - s D s F < s C s E C s F + s D s E - s D s F < s C s E
293 109 129 subscld φ D s E - s D s F No
294 96 293 124 sltaddsub2d φ C s F + s D s E - s D s F < s C s E D s E - s D s F < s C s E - s C s F
295 292 294 bitrd φ D s E + s C s F - s D s F < s C s E D s E - s D s F < s C s E - s C s F
296 295 187 bitrd φ D s E + s C s F - s D s F < s C s E C s F - s C s E < s D s F - s D s E
297 296 adantr φ bday D bday C bday F bday E D s E + s C s F - s D s F < s C s E C s F - s C s E < s D s F - s D s E
298 287 297 mpbid φ bday D bday C bday F bday E C s F - s C s E < s D s F - s D s E
299 298 anassrs φ bday D bday C bday F bday E C s F - s C s E < s D s F - s D s E
300 9 adantr φ bday D bday C bday E bday F bday F bday E
301 248 299 300 mpjaodan φ bday D bday C C s F - s C s E < s D s F - s D s E
302 193 301 8 mpjaodan φ C s F - s C s E < s D s F - s D s E