Metamath Proof Explorer

Theorem mulsproplemcbv

Description: Lemma for surreal multiplication. Change some bound variables for later use. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 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
Assertion 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

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 fveq2 ⊢ a = g → bday ⁡ a = bday ⁡ g
3 2 oveq1d ⊢ a = g → bday ⁡ a + bday ⁡ b = bday ⁡ g + bday ⁡ b
4 3 uneq1d ⊢ a = g → bday ⁡ a + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ g + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e
5 4 eleq1d ⊢ a = g → 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 ⁡ g + 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
6 oveq1 ⊢ a = g → a ⋅ s b = g ⋅ s b
7 6 eleq1d ⊢ a = g → a ⋅ s b ∈ No ↔ g ⋅ s b ∈ No
8 7 anbi1d ⊢ a = g → 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 ↔ g ⋅ 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 5 8 imbi12d ⊢ a = g → 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 ⁡ g + 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 → g ⋅ 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 fveq2 ⊢ b = h → bday ⁡ b = bday ⁡ h
11 10 oveq2d ⊢ b = h → bday ⁡ g + bday ⁡ b = bday ⁡ g + bday ⁡ h
12 11 uneq1d ⊢ b = h → bday ⁡ g + bday ⁡ b ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ g + bday ⁡ h ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e
13 12 eleq1d ⊢ b = h → bday ⁡ g + 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 ⁡ g + bday ⁡ h ∪ 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
14 oveq2 ⊢ b = h → g ⋅ s b = g ⋅ s h
15 14 eleq1d ⊢ b = h → g ⋅ s b ∈ No ↔ g ⋅ s h ∈ No
16 15 anbi1d ⊢ b = h → g ⋅ s b ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ g ⋅ s h ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
17 13 16 imbi12d ⊢ b = h → bday ⁡ g + 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 → g ⋅ 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 ⁡ g + bday ⁡ h ∪ 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 → g ⋅ s h ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e
18 fveq2 ⊢ c = i → bday ⁡ c = bday ⁡ i
19 18 oveq1d ⊢ c = i → bday ⁡ c + bday ⁡ e = bday ⁡ i + bday ⁡ e
20 19 uneq1d ⊢ c = i → bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f = bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f
21 18 oveq1d ⊢ c = i → bday ⁡ c + bday ⁡ f = bday ⁡ i + bday ⁡ f
22 21 uneq1d ⊢ c = i → bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e
23 20 22 uneq12d ⊢ c = i → bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e
24 23 uneq2d ⊢ c = i → bday ⁡ g + bday ⁡ h ∪ bday ⁡ c + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ c + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e
25 24 eleq1d ⊢ c = i → bday ⁡ g + bday ⁡ h ∪ 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 ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + 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
26 breq1 ⊢ c = i → c < s d ↔ i < s d
27 26 anbi1d ⊢ c = i → c < s d ∧ e < s f ↔ i < s d ∧ e < s f
28 oveq1 ⊢ c = i → c ⋅ s f = i ⋅ s f
29 oveq1 ⊢ c = i → c ⋅ s e = i ⋅ s e
30 28 29 oveq12d ⊢ c = i → c ⋅ s f - s c ⋅ s e = i ⋅ s f - s i ⋅ s e
31 30 breq1d ⊢ c = i → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e
32 27 31 imbi12d ⊢ c = i → c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e
33 32 anbi2d ⊢ c = i → g ⋅ s h ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ g ⋅ s h ∈ No ∧ i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e
34 25 33 imbi12d ⊢ c = i → bday ⁡ g + bday ⁡ h ∪ 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 → g ⋅ s h ∈ No ∧ c < s d ∧ e < s f → c ⋅ s f - s c ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + 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 → g ⋅ s h ∈ No ∧ i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e
35 fveq2 ⊢ d = j → bday ⁡ d = bday ⁡ j
36 35 oveq1d ⊢ d = j → bday ⁡ d + bday ⁡ f = bday ⁡ j + bday ⁡ f
37 36 uneq2d ⊢ d = j → bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f = bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f
38 35 oveq1d ⊢ d = j → bday ⁡ d + bday ⁡ e = bday ⁡ j + bday ⁡ e
39 38 uneq2d ⊢ d = j → bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e
40 37 39 uneq12d ⊢ d = j → bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e
41 40 uneq2d ⊢ d = j → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ d + bday ⁡ e = bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e
42 41 eleq1d ⊢ d = j → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + 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 ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
43 breq2 ⊢ d = j → i < s d ↔ i < s j
44 43 anbi1d ⊢ d = j → i < s d ∧ e < s f ↔ i < s j ∧ e < s f
45 oveq1 ⊢ d = j → d ⋅ s f = j ⋅ s f
46 oveq1 ⊢ d = j → d ⋅ s e = j ⋅ s e
47 45 46 oveq12d ⊢ d = j → d ⋅ s f - s d ⋅ s e = j ⋅ s f - s j ⋅ s e
48 47 breq2d ⊢ d = j → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e
49 44 48 imbi12d ⊢ d = j → i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ i < s j ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e
50 49 anbi2d ⊢ d = j → g ⋅ s h ∈ No ∧ i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ g ⋅ s h ∈ No ∧ i < s j ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e
51 42 50 imbi12d ⊢ d = j → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ d + bday ⁡ f ∪ bday ⁡ i + 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 → g ⋅ s h ∈ No ∧ i < s d ∧ e < s f → i ⋅ s f - s i ⋅ s e < s d ⋅ s f - s d ⋅ s e ↔ bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e ∈ 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 ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e
52 fveq2 ⊢ e = k → bday ⁡ e = bday ⁡ k
53 52 oveq2d ⊢ e = k → bday ⁡ i + bday ⁡ e = bday ⁡ i + bday ⁡ k
54 53 uneq1d ⊢ e = k → bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f = bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f
55 52 oveq2d ⊢ e = k → bday ⁡ j + bday ⁡ e = bday ⁡ j + bday ⁡ k
56 55 uneq2d ⊢ e = k → bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e = bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k
57 54 56 uneq12d ⊢ e = k → bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e = bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k
58 57 uneq2d ⊢ e = k → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e = bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k
59 58 eleq1d ⊢ e = k → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E ↔ bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
60 breq1 ⊢ e = k → e < s f ↔ k < s f
61 60 anbi2d ⊢ e = k → i < s j ∧ e < s f ↔ i < s j ∧ k < s f
62 oveq2 ⊢ e = k → i ⋅ s e = i ⋅ s k
63 62 oveq2d ⊢ e = k → i ⋅ s f - s i ⋅ s e = i ⋅ s f - s i ⋅ s k
64 oveq2 ⊢ e = k → j ⋅ s e = j ⋅ s k
65 64 oveq2d ⊢ e = k → j ⋅ s f - s j ⋅ s e = j ⋅ s f - s j ⋅ s k
66 63 65 breq12d ⊢ e = k → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e ↔ i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k
67 61 66 imbi12d ⊢ e = k → i < s j ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e ↔ i < s j ∧ k < s f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k
68 67 anbi2d ⊢ e = k → g ⋅ s h ∈ No ∧ i < s j ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e ↔ g ⋅ s h ∈ No ∧ i < s j ∧ k < s f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k
69 59 68 imbi12d ⊢ e = k → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ e ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ e ∈ 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 ∧ e < s f → i ⋅ s f - s i ⋅ s e < s j ⋅ s f - s j ⋅ s e ↔ bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ 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 f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k
70 fveq2 ⊢ f = l → bday ⁡ f = bday ⁡ l
71 70 oveq2d ⊢ f = l → bday ⁡ j + bday ⁡ f = bday ⁡ j + bday ⁡ l
72 71 uneq2d ⊢ f = l → bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f = bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l
73 70 oveq2d ⊢ f = l → bday ⁡ i + bday ⁡ f = bday ⁡ i + bday ⁡ l
74 73 uneq1d ⊢ f = l → bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k = bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k
75 72 74 uneq12d ⊢ f = l → bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k = bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k
76 75 uneq2d ⊢ f = l → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k = bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ l ∪ bday ⁡ i + bday ⁡ l ∪ bday ⁡ j + bday ⁡ k
77 76 eleq1d ⊢ f = l → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ bday ⁡ j + bday ⁡ k ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + 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
78 breq2 ⊢ f = l → k < s f ↔ k < s l
79 78 anbi2d ⊢ f = l → i < s j ∧ k < s f ↔ i < s j ∧ k < s l
80 oveq2 ⊢ f = l → i ⋅ s f = i ⋅ s l
81 80 oveq1d ⊢ f = l → i ⋅ s f - s i ⋅ s k = i ⋅ s l - s i ⋅ s k
82 oveq2 ⊢ f = l → j ⋅ s f = j ⋅ s l
83 82 oveq1d ⊢ f = l → j ⋅ s f - s j ⋅ s k = j ⋅ s l - s j ⋅ s k
84 81 83 breq12d ⊢ f = l → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k ↔ i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
85 79 84 imbi12d ⊢ f = l → i < s j ∧ k < s f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k ↔ i < s j ∧ k < s l → i ⋅ s l - s i ⋅ s k < s j ⋅ s l - s j ⋅ s k
86 85 anbi2d ⊢ f = l → g ⋅ s h ∈ No ∧ i < s j ∧ k < s f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - s j ⋅ s k ↔ 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
87 77 86 imbi12d ⊢ f = l → bday ⁡ g + bday ⁡ h ∪ bday ⁡ i + bday ⁡ k ∪ bday ⁡ j + bday ⁡ f ∪ bday ⁡ i + bday ⁡ f ∪ 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 f → i ⋅ s f - s i ⋅ s k < s j ⋅ s f - 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 ⁡ 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
88 9 17 34 51 69 87 cbvral6vw ⊢ ∀ 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 ↔ ∀ 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
89 1 88 sylib ⊢ φ → ∀ 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