Metamath Proof Explorer


Theorem mulsproplem1

Description: Lemma for surreal multiplication. Instantiate some variables. (Contributed by Scott Fenton, 4-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 φ a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
mulsproplem1.1 φ X No
mulsproplem1.2 φ Y No
mulsproplem1.3 φ Z No
mulsproplem1.4 φ W No
mulsproplem1.5 φ T No
mulsproplem1.6 φ U No
mulsproplem1.7 φ bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
Assertion mulsproplem1 φ X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T

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 mulsproplem1.1 φ X No
3 mulsproplem1.2 φ Y No
4 mulsproplem1.3 φ Z No
5 mulsproplem1.4 φ W No
6 mulsproplem1.5 φ T No
7 mulsproplem1.6 φ U No
8 mulsproplem1.7 φ bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
9 fveq2 a = X bday a = bday X
10 9 oveq1d a = X bday a + bday b = bday X + bday b
11 10 uneq1d a = X bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday X + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e
12 11 eleq1d a = X 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 bday X + 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
13 oveq1 a = X a s b = X s b
14 13 eleq1d a = X a s b No X s b No
15 14 anbi1d a = X 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 X s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
16 12 15 imbi12d a = X 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 X + 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 X s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
17 fveq2 b = Y bday b = bday Y
18 17 oveq2d b = Y bday X + bday b = bday X + bday Y
19 18 uneq1d b = Y bday X + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday X + bday Y bday c + bday e bday d + bday f bday c + bday f bday d + bday e
20 19 eleq1d b = Y bday X + 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 bday X + bday Y 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
21 oveq2 b = Y X s b = X s Y
22 21 eleq1d b = Y X s b No X s Y No
23 22 anbi1d b = Y X s b No c < s d e < s f c s f - s c s e < s d s f - s d s e X s Y No c < s d e < s f c s f - s c s e < s d s f - s d s e
24 20 23 imbi12d b = Y bday X + 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 X 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 X + bday Y 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 X s Y No c < s d e < s f c s f - s c s e < s d s f - s d s e
25 fveq2 c = Z bday c = bday Z
26 25 oveq1d c = Z bday c + bday e = bday Z + bday e
27 26 uneq1d c = Z bday c + bday e bday d + bday f = bday Z + bday e bday d + bday f
28 25 oveq1d c = Z bday c + bday f = bday Z + bday f
29 28 uneq1d c = Z bday c + bday f bday d + bday e = bday Z + bday f bday d + bday e
30 27 29 uneq12d c = Z bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday Z + bday e bday d + bday f bday Z + bday f bday d + bday e
31 30 uneq2d c = Z bday X + bday Y bday c + bday e bday d + bday f bday c + bday f bday d + bday e = bday X + bday Y bday Z + bday e bday d + bday f bday Z + bday f bday d + bday e
32 31 eleq1d c = Z bday X + bday Y 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 bday X + bday Y bday Z + bday e bday d + bday f bday Z + 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
33 breq1 c = Z c < s d Z < s d
34 33 anbi1d c = Z c < s d e < s f Z < s d e < s f
35 oveq1 c = Z c s f = Z s f
36 oveq1 c = Z c s e = Z s e
37 35 36 oveq12d c = Z c s f - s c s e = Z s f - s Z s e
38 37 breq1d c = Z c s f - s c s e < s d s f - s d s e Z s f - s Z s e < s d s f - s d s e
39 34 38 imbi12d c = Z c < s d e < s f c s f - s c s e < s d s f - s d s e Z < s d e < s f Z s f - s Z s e < s d s f - s d s e
40 39 anbi2d c = Z X s Y No c < s d e < s f c s f - s c s e < s d s f - s d s e X s Y No Z < s d e < s f Z s f - s Z s e < s d s f - s d s e
41 32 40 imbi12d c = Z bday X + bday Y 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 X s Y No c < s d e < s f c s f - s c s e < s d s f - s d s e bday X + bday Y bday Z + bday e bday d + bday f bday Z + 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 X s Y No Z < s d e < s f Z s f - s Z s e < s d s f - s d s e
42 fveq2 d = W bday d = bday W
43 42 oveq1d d = W bday d + bday f = bday W + bday f
44 43 uneq2d d = W bday Z + bday e bday d + bday f = bday Z + bday e bday W + bday f
45 42 oveq1d d = W bday d + bday e = bday W + bday e
46 45 uneq2d d = W bday Z + bday f bday d + bday e = bday Z + bday f bday W + bday e
47 44 46 uneq12d d = W bday Z + bday e bday d + bday f bday Z + bday f bday d + bday e = bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e
48 47 uneq2d d = W bday X + bday Y bday Z + bday e bday d + bday f bday Z + bday f bday d + bday e = bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e
49 48 eleq1d d = W bday X + bday Y bday Z + bday e bday d + bday f bday Z + 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 bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
50 breq2 d = W Z < s d Z < s W
51 50 anbi1d d = W Z < s d e < s f Z < s W e < s f
52 oveq1 d = W d s f = W s f
53 oveq1 d = W d s e = W s e
54 52 53 oveq12d d = W d s f - s d s e = W s f - s W s e
55 54 breq2d d = W Z s f - s Z s e < s d s f - s d s e Z s f - s Z s e < s W s f - s W s e
56 51 55 imbi12d d = W Z < s d e < s f Z s f - s Z s e < s d s f - s d s e Z < s W e < s f Z s f - s Z s e < s W s f - s W s e
57 56 anbi2d d = W X s Y No Z < s d e < s f Z s f - s Z s e < s d s f - s d s e X s Y No Z < s W e < s f Z s f - s Z s e < s W s f - s W s e
58 49 57 imbi12d d = W bday X + bday Y bday Z + bday e bday d + bday f bday Z + 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 X s Y No Z < s d e < s f Z s f - s Z s e < s d s f - s d s e bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W e < s f Z s f - s Z s e < s W s f - s W s e
59 fveq2 e = T bday e = bday T
60 59 oveq2d e = T bday Z + bday e = bday Z + bday T
61 60 uneq1d e = T bday Z + bday e bday W + bday f = bday Z + bday T bday W + bday f
62 59 oveq2d e = T bday W + bday e = bday W + bday T
63 62 uneq2d e = T bday Z + bday f bday W + bday e = bday Z + bday f bday W + bday T
64 61 63 uneq12d e = T bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e = bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T
65 64 uneq2d e = T bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e = bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T
66 65 eleq1d e = T bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
67 breq1 e = T e < s f T < s f
68 67 anbi2d e = T Z < s W e < s f Z < s W T < s f
69 oveq2 e = T Z s e = Z s T
70 69 oveq2d e = T Z s f - s Z s e = Z s f - s Z s T
71 oveq2 e = T W s e = W s T
72 71 oveq2d e = T W s f - s W s e = W s f - s W s T
73 70 72 breq12d e = T Z s f - s Z s e < s W s f - s W s e Z s f - s Z s T < s W s f - s W s T
74 68 73 imbi12d e = T Z < s W e < s f Z s f - s Z s e < s W s f - s W s e Z < s W T < s f Z s f - s Z s T < s W s f - s W s T
75 74 anbi2d e = T X s Y No Z < s W e < s f Z s f - s Z s e < s W s f - s W s e X s Y No Z < s W T < s f Z s f - s Z s T < s W s f - s W s T
76 66 75 imbi12d e = T bday X + bday Y bday Z + bday e bday W + bday f bday Z + bday f bday W + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W e < s f Z s f - s Z s e < s W s f - s W s e bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W T < s f Z s f - s Z s T < s W s f - s W s T
77 fveq2 f = U bday f = bday U
78 77 oveq2d f = U bday W + bday f = bday W + bday U
79 78 uneq2d f = U bday Z + bday T bday W + bday f = bday Z + bday T bday W + bday U
80 77 oveq2d f = U bday Z + bday f = bday Z + bday U
81 80 uneq1d f = U bday Z + bday f bday W + bday T = bday Z + bday U bday W + bday T
82 79 81 uneq12d f = U bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T = bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T
83 82 uneq2d f = U bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T = bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T
84 83 eleq1d f = U bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
85 breq2 f = U T < s f T < s U
86 85 anbi2d f = U Z < s W T < s f Z < s W T < s U
87 oveq2 f = U Z s f = Z s U
88 87 oveq1d f = U Z s f - s Z s T = Z s U - s Z s T
89 oveq2 f = U W s f = W s U
90 89 oveq1d f = U W s f - s W s T = W s U - s W s T
91 88 90 breq12d f = U Z s f - s Z s T < s W s f - s W s T Z s U - s Z s T < s W s U - s W s T
92 86 91 imbi12d f = U Z < s W T < s f Z s f - s Z s T < s W s f - s W s T Z < s W T < s U Z s U - s Z s T < s W s U - s W s T
93 92 anbi2d f = U X s Y No Z < s W T < s f Z s f - s Z s T < s W s f - s W s T X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T
94 84 93 imbi12d f = U bday X + bday Y bday Z + bday T bday W + bday f bday Z + bday f bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W T < s f Z s f - s Z s T < s W s f - s W s T bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T
95 16 24 41 58 76 94 rspc6v X No Y No Z No W No T No U No 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 bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T
96 2 3 4 5 6 7 95 syl222anc φ 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 bday X + bday Y bday Z + bday T bday W + bday U bday Z + bday U bday W + bday T bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T
97 1 8 96 mp2d φ X s Y No Z < s W T < s U Z s U - s Z s T < s W s U - s W s T