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