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